Search code examples
setlogichigher-order-functionsisabelleformal-methods

How to write bigvee and big wedge in Isabelle

I'm trying to use Isabelle to do auto-prove. However, I got a problem of specifying formulas in Isabelle. For example, I have a formulas like this enter image description here Then, I define sets and use big_wedge and big_vee symbols in Isabelle as follows: enter image description here And the result is "Inner lexical error⌂ Failed to parse prop". Could you explain what is wrong here, please? Thank you very much.

Solution

  • Not all symbols shown in Isabelle/jEdit's Symbol tabs have a meaning. These are the symbols you can use in your code.

    Based on the corresponding code for sums, I started the setup, but I did not finish it (in particular, the syntax ⋀t!=l. P t is not supported).

    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

    The full setup is possible. But I am not certain that this is a good idea... You will need a lot of lemmas to make things work nicely and I am not certain the behaviour for infinite sets is the right one.