moved lemmas about sup on bool to Lattices.thy
authorhaftmann
Wed Sep 30 17:16:01 2009 +0200 (2009-09-30)
changeset 3278119c01bd7f6ae
parent 32780 be337ec31268
child 32782 faf347097852
moved lemmas about sup on bool to Lattices.thy
src/HOL/Lattices.thy
     1.1 --- a/src/HOL/Lattices.thy	Wed Sep 30 17:09:06 2009 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Wed Sep 30 17:16:01 2009 +0200
     1.3 @@ -535,6 +535,18 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma sup_boolI1:
     1.8 +  "P \<Longrightarrow> P \<squnion> Q"
     1.9 +  by (simp add: sup_bool_eq)
    1.10 +
    1.11 +lemma sup_boolI2:
    1.12 +  "Q \<Longrightarrow> P \<squnion> Q"
    1.13 +  by (simp add: sup_bool_eq)
    1.14 +
    1.15 +lemma sup_boolE:
    1.16 +  "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
    1.17 +  by (auto simp add: sup_bool_eq)
    1.18 +
    1.19  
    1.20  subsection {* Fun as lattice *}
    1.21