moved lemmas about sup on bool to Lattices.thy
authorhaftmann
Wed Sep 30 17:23:00 2009 +0200 (2009-09-30)
changeset 32782faf347097852
parent 32781 19c01bd7f6ae
child 32783 e43d761a742d
moved lemmas about sup on bool to Lattices.thy
src/HOL/Predicate.thy
     1.1 --- a/src/HOL/Predicate.thy	Wed Sep 30 17:16:01 2009 +0200
     1.2 +++ b/src/HOL/Predicate.thy	Wed Sep 30 17:23:00 2009 +0200
     1.3 @@ -19,21 +19,6 @@
     1.4  
     1.5  subsection {* Predicates as (complete) lattices *}
     1.6  
     1.7 -subsubsection {* @{const sup} on @{typ bool} *}
     1.8 -
     1.9 -lemma sup_boolI1:
    1.10 -  "P \<Longrightarrow> P \<squnion> Q"
    1.11 -  by (simp add: sup_bool_eq)
    1.12 -
    1.13 -lemma sup_boolI2:
    1.14 -  "Q \<Longrightarrow> P \<squnion> Q"
    1.15 -  by (simp add: sup_bool_eq)
    1.16 -
    1.17 -lemma sup_boolE:
    1.18 -  "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
    1.19 -  by (auto simp add: sup_bool_eq)
    1.20 -
    1.21 -
    1.22  subsubsection {* Equality *}
    1.23  
    1.24  lemma pred_equals_eq: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) = (R = S)"