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.