如何在Isabelle中写bigvee和big wedge

Question

我正在尝试使用 Isabelle 进行自动证明。但是，我遇到了在 Isabelle 中指定公式的问题。例如，我有一个这样的公式然后，我定义集合并在 Isabelle 中使用 big_wedge 和 big_vee 符号，如下所示：结果是“内部词法错误⌂无法解析 prop”。你能解释一下这里出了什么问题吗？非常感谢。

Answer 1

并非 Isabelle/jEdit 的符号选项卡中显示的所有符号都有意义。这些是您可以在代码中使用的符号。

根据sums对应的代码，我开始设置，但我没有完成（特别是不支持语法⋀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

可以进行完整设置。但我不确定这是个好主意......你需要很多引理才能使事情顺利进行，而且我不确定无限集的行为是否正确。

如何在Isabelle中写bigvee和big wedge

How to write bigvee and big wedge in Isabelle

set

logic

higher-order-functions

isabelle

formal-methods