formal passive interpretation proofs for conj and disj
authorhaftmann
Wed Aug 10 18:57:20 2016 +0200 (2016-08-10)
changeset 6366192e037803666
parent 63660 76302202a92d
child 63662 5cdcd51a4dad
formal passive interpretation proofs for conj and disj
src/HOL/Lattices.thy
     1.1 --- a/src/HOL/Lattices.thy	Mon Aug 08 14:01:49 2016 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Wed Aug 10 18:57:20 2016 +0200
     1.3 @@ -139,6 +139,16 @@
     1.4  
     1.5  end
     1.6  
     1.7 +text \<open>Passive interpretations for boolean operators\<close>
     1.8 +
     1.9 +lemma semilattice_neutr_and:
    1.10 +  "semilattice_neutr HOL.conj True"
    1.11 +  by standard auto
    1.12 +
    1.13 +lemma semilattice_neutr_or:
    1.14 +  "semilattice_neutr HOL.disj False"
    1.15 +  by standard auto
    1.16 +
    1.17  
    1.18  subsection \<open>Syntactic infimum and supremum operations\<close>
    1.19