src/HOL/Lattices.thy

 
 lemmas max_ac = min_max.sup_assoc min_max.sup_commute
   min_max.sup.left_commute
 
 
-subsection {* Bool as lattice *}
+subsection {* Lattice on @{typ bool} *}
 
 instantiation bool :: boolean_algebra
 begin
 
 definition

 lemma sup_boolE:
   "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
   by auto
 
 
-subsection {* Fun as lattice *}
+subsection {* Lattice on @{typ "_ \<Rightarrow> _"} *}
 
 instantiation "fun" :: (type, lattice) lattice
 begin
 
 definition

 
 end
 
 instance "fun" :: (type, boolean_algebra) boolean_algebra proof
 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)+
+
+
+subsection {* Lattice on unary and binary predicates *}
+
+lemma inf1I: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x"
+  by (simp add: inf_fun_def)
+
+lemma inf2I: "A x y \<Longrightarrow> B x y \<Longrightarrow> (A \<sqinter> B) x y"
+  by (simp add: inf_fun_def)
+
+lemma inf1E: "(A \<sqinter> B) x \<Longrightarrow> (A x \<Longrightarrow> B x \<Longrightarrow> P) \<Longrightarrow> P"
+  by (simp add: inf_fun_def)
+
+lemma inf2E: "(A \<sqinter> B) x y \<Longrightarrow> (A x y \<Longrightarrow> B x y \<Longrightarrow> P) \<Longrightarrow> P"
+  by (simp add: inf_fun_def)
+
+lemma inf1D1: "(A \<sqinter> B) x \<Longrightarrow> A x"
+  by (simp add: inf_fun_def)
+
+lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y"
+  by (simp add: inf_fun_def)
+
+lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x"
+  by (simp add: inf_fun_def)
+
+lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y"
+  by (simp add: inf_fun_def)
+
+lemma sup1I1: "A x \<Longrightarrow> (A \<squnion> B) x"
+  by (simp add: sup_fun_def)
+
+lemma sup2I1: "A x y \<Longrightarrow> (A \<squnion> B) x y"
+  by (simp add: sup_fun_def)
+
+lemma sup1I2: "B x \<Longrightarrow> (A \<squnion> B) x"
+  by (simp add: sup_fun_def)
+
+lemma sup2I2: "B x y \<Longrightarrow> (A \<squnion> B) x y"
+  by (simp add: sup_fun_def)
+
+lemma sup1E: "(A \<squnion> B) x \<Longrightarrow> (A x \<Longrightarrow> P) \<Longrightarrow> (B x \<Longrightarrow> P) \<Longrightarrow> P"
+  by (simp add: sup_fun_def) iprover
+
+lemma sup2E: "(A \<squnion> B) x y \<Longrightarrow> (A x y \<Longrightarrow> P) \<Longrightarrow> (B x y \<Longrightarrow> P) \<Longrightarrow> P"
+  by (simp add: sup_fun_def) iprover
+
+text {*
+  \medskip Classical introduction rule: no commitment to @{text A} vs
+  @{text B}.
+*}
+
+lemma sup1CI: "(\<not> B x \<Longrightarrow> A x) \<Longrightarrow> (A \<squnion> B) x"
+  by (auto simp add: sup_fun_def)
+
+lemma sup2CI: "(\<not> B x y \<Longrightarrow> A x y) \<Longrightarrow> (A \<squnion> B) x y"
+  by (auto simp add: sup_fun_def)
+
 
 no_notation
   less_eq  (infix "\<sqsubseteq>" 50) and
   less (infix "\<sqsubset>" 50) and
   inf  (infixl "\<sqinter>" 70) and
   sup  (infixl "\<squnion>" 65) and
   top ("\<top>") and
   bot ("\<bottom>")
 
 end
+