Как написать большой и большой клин на Изабель

Не все символы, показанные на вкладках «Символы» Isabelle / jEdit, имеют значение. Это символы, которые вы можете использовать в своем коде.

Исходя из соответствующего кода для сумм, я начал настройку, но не закончил (в частности, не поддерживается синтаксис ⋀t!=l. P t).

context comm_monoid_add
begin

sublocale bigvee: comm_monoid_set HOL.disj False
  defines bigvee = bigvee.F and bigvee' = bigvee.G
  by standard auto

abbreviation bigvee'' :: ‹bool set ⇒ bool› ("⋁")
  where "⋁ ≡ bigvee (λx. x)"

sublocale bigwedge: comm_monoid_set HOL.conj True
  defines bigwedge = bigwedge.F and bigwedge' = bigwedge.G
  by standard auto

abbreviation bigwedge'' :: ‹bool set ⇒ bool› ("⋀")
  where "⋀ ≡ bigwedge (λx. x)"

end
syntax
  "_bigwedge" :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b::comm_monoid_add"  ("(2⋀(_/∈_)./ _)" [0, 51, 10] 10)
translations ― ‹Beware of argument permutation!›
  "⋀i∈A. b" ⇌ "CONST bigwedge (λi. b) A"

syntax
  "_bigvee" :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b::comm_monoid_add"  ("(2⋁(_/∈_)./ _)" [0, 51, 10] 10)
translations ― ‹Beware of argument permutation!›
  "⋁i∈A. b" ⇌ "CONST bigvee (λi. b) A"

instantiation bool :: comm_monoid_add
begin
definition zero_bool where
[simp]: ‹zero_bool = False›
definition plus_bool where
[simp]: ‹plus_bool = (∨)›
instance
  by standard auto
end
thm bigvee_def

lemma ‹finite A ⟹ (⋁i∈A. f i) ⟷ (∃i ∈ A. f i)›
  apply (induction rule: finite_induct)
  apply (auto simp: )
  done

lemma ‹finite A ⟹ (⋀i∈A. f i) ⟷ A = {} ∨ (∀i ∈ A. f i)›
  apply (induction rule: finite_induct)
  apply (auto simp: )[2]
  done

lemma ‹infinite A ⟹ (⋀i∈A. f i) ⟷ True›
  by auto

lemma test1:
  ‹(⋀j∈L. ⋀u∈U. ⋀t∈T. ⋀l∈L. ⋀l⇩1∈L⇩1. ¬P j u t l⇩1) ∨
   (⋁i∈I. ⋁v∈V. ⋀k∈K. ⋁h∈H. Q i ∨ k h) ⟹
   (⋁i∈I. ⋁v∈V. ⋀k∈K. ⋁h∈H. Q i ∨ k h) ∨ (⋀j∈J. ⋀u∈U. ⋀t∈T. ⋀l⇩1∈L⇩1. ¬P j u t l⇩1)›
  apply auto
  

Возможна полная настройка. Но я не уверен, что это хорошая идея ... Вам понадобится много лемм, чтобы все работало хорошо, и я не уверен, что поведение для бесконечных множеств правильное.