如何在伊莎贝尔Isabelle中写bigvee和big楔子

问题描述

我正在尝试使用Isabelle进行自动验证。但是，我遇到了在Isabelle中指定公式的问题。例如，我有一个这样的公式

然后，我定义集合并在Isabelle中使用 big_wedge 和 big_vee 符号，如下所示：

结果为“ 内部词法错误⌂无法解析prop ”。 你能解释一下这是怎么回事吗？ 非常感谢。

解决方法

并非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,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
  

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