src/HOL/Lattices.thy
changeset 46553 50a7e97fe653
parent 44921 58eef4843641
child 46557 ae926869a311
     1.1 --- a/src/HOL/Lattices.thy	Mon Feb 20 15:17:03 2012 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Sun Feb 19 15:30:35 2012 +0100
     1.3 @@ -701,6 +701,63 @@
     1.4  instance "fun" :: (type, boolean_algebra) boolean_algebra proof
     1.5  qed (rule ext, simp_all add: inf_apply sup_apply bot_apply top_apply uminus_apply minus_apply inf_compl_bot sup_compl_top diff_eq)+
     1.6  
     1.7 +
     1.8 +subsection {* Unary and binary predicates as lattice *}
     1.9 +
    1.10 +lemma inf1I [intro!]: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x"
    1.11 +  by (simp add: inf_fun_def)
    1.12 +
    1.13 +lemma inf2I [intro!]: "A x y \<Longrightarrow> B x y \<Longrightarrow> (A \<sqinter> B) x y"
    1.14 +  by (simp add: inf_fun_def)
    1.15 +
    1.16 +lemma inf1E [elim!]: "(A \<sqinter> B) x \<Longrightarrow> (A x \<Longrightarrow> B x \<Longrightarrow> P) \<Longrightarrow> P"
    1.17 +  by (simp add: inf_fun_def)
    1.18 +
    1.19 +lemma inf2E [elim!]: "(A \<sqinter> B) x y \<Longrightarrow> (A x y \<Longrightarrow> B x y \<Longrightarrow> P) \<Longrightarrow> P"
    1.20 +  by (simp add: inf_fun_def)
    1.21 +
    1.22 +lemma inf1D1: "(A \<sqinter> B) x \<Longrightarrow> A x"
    1.23 +  by (simp add: inf_fun_def)
    1.24 +
    1.25 +lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y"
    1.26 +  by (simp add: inf_fun_def)
    1.27 +
    1.28 +lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x"
    1.29 +  by (simp add: inf_fun_def)
    1.30 +
    1.31 +lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y"
    1.32 +  by (simp add: inf_fun_def)
    1.33 +
    1.34 +lemma sup1I1 [intro?]: "A x \<Longrightarrow> (A \<squnion> B) x"
    1.35 +  by (simp add: sup_fun_def)
    1.36 +
    1.37 +lemma sup2I1 [intro?]: "A x y \<Longrightarrow> (A \<squnion> B) x y"
    1.38 +  by (simp add: sup_fun_def)
    1.39 +
    1.40 +lemma sup1I2 [intro?]: "B x \<Longrightarrow> (A \<squnion> B) x"
    1.41 +  by (simp add: sup_fun_def)
    1.42 +
    1.43 +lemma sup2I2 [intro?]: "B x y \<Longrightarrow> (A \<squnion> B) x y"
    1.44 +  by (simp add: sup_fun_def)
    1.45 +
    1.46 +lemma sup1E [elim!]: "(A \<squnion> B) x \<Longrightarrow> (A x \<Longrightarrow> P) \<Longrightarrow> (B x \<Longrightarrow> P) \<Longrightarrow> P"
    1.47 +  by (simp add: sup_fun_def) iprover
    1.48 +
    1.49 +lemma sup2E [elim!]: "(A \<squnion> B) x y \<Longrightarrow> (A x y \<Longrightarrow> P) \<Longrightarrow> (B x y \<Longrightarrow> P) \<Longrightarrow> P"
    1.50 +  by (simp add: sup_fun_def) iprover
    1.51 +
    1.52 +text {*
    1.53 +  \medskip Classical introduction rule: no commitment to @{text A} vs
    1.54 +  @{text B}.
    1.55 +*}
    1.56 +
    1.57 +lemma sup1CI [intro!]: "(\<not> B x \<Longrightarrow> A x) \<Longrightarrow> (A \<squnion> B) x"
    1.58 +  by (auto simp add: sup_fun_def)
    1.59 +
    1.60 +lemma sup2CI [intro!]: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y"
    1.61 +  by (auto simp add: sup_fun_def)
    1.62 +
    1.63 +
    1.64  no_notation
    1.65    less_eq  (infix "\<sqsubseteq>" 50) and
    1.66    less (infix "\<sqsubset>" 50) and
    1.67 @@ -710,3 +767,4 @@
    1.68    bot ("\<bottom>")
    1.69  
    1.70  end
    1.71 +