--- a/src/HOL/Lattices.thy Thu Aug 05 07:12:49 2021 +0000
+++ b/src/HOL/Lattices.thy Thu Aug 05 07:12:49 2021 +0000
@@ -462,7 +462,7 @@
end
-subsection \<open>Bounded lattices and boolean algebras\<close>
+subsection \<open>Bounded lattices\<close>
class bounded_semilattice_inf_top = semilattice_inf + order_top
begin
@@ -549,196 +549,6 @@
end
-class boolean_algebra = distrib_lattice + bounded_lattice + minus + uminus +
- assumes inf_compl_bot: "x \<sqinter> - x = \<bottom>"
- and sup_compl_top: "x \<squnion> - x = \<top>"
- assumes diff_eq: "x - y = x \<sqinter> - y"
-begin
-
-lemma dual_boolean_algebra:
- "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus sup greater_eq greater inf \<top> \<bottom>"
- by (rule class.boolean_algebra.intro,
- rule dual_bounded_lattice,
- rule dual_distrib_lattice)
- (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
-
-lemma compl_inf_bot [simp]: "- x \<sqinter> x = \<bottom>"
- by (simp add: inf_commute inf_compl_bot)
-
-lemma compl_sup_top [simp]: "- x \<squnion> x = \<top>"
- by (simp add: sup_commute sup_compl_top)
-
-lemma compl_unique:
- assumes "x \<sqinter> y = \<bottom>"
- and "x \<squnion> y = \<top>"
- shows "- x = y"
-proof -
- have "(x \<sqinter> - x) \<squnion> (- x \<sqinter> y) = (x \<sqinter> y) \<squnion> (- x \<sqinter> y)"
- using inf_compl_bot assms(1) by simp
- then have "(- x \<sqinter> x) \<squnion> (- x \<sqinter> y) = (y \<sqinter> x) \<squnion> (y \<sqinter> - x)"
- by (simp add: inf_commute)
- then have "- x \<sqinter> (x \<squnion> y) = y \<sqinter> (x \<squnion> - x)"
- by (simp add: inf_sup_distrib1)
- then have "- x \<sqinter> \<top> = y \<sqinter> \<top>"
- using sup_compl_top assms(2) by simp
- then show "- x = y" by simp
-qed
-
-lemma double_compl [simp]: "- (- x) = x"
- using compl_inf_bot compl_sup_top by (rule compl_unique)
-
-lemma compl_eq_compl_iff [simp]: "- x = - y \<longleftrightarrow> x = y"
-proof
- assume "- x = - y"
- then have "- (- x) = - (- y)" by (rule arg_cong)
- then show "x = y" by simp
-next
- assume "x = y"
- then show "- x = - y" by simp
-qed
-
-lemma compl_bot_eq [simp]: "- \<bottom> = \<top>"
-proof -
- from sup_compl_top have "\<bottom> \<squnion> - \<bottom> = \<top>" .
- then show ?thesis by simp
-qed
-
-lemma compl_top_eq [simp]: "- \<top> = \<bottom>"
-proof -
- from inf_compl_bot have "\<top> \<sqinter> - \<top> = \<bottom>" .
- then show ?thesis by simp
-qed
-
-lemma compl_inf [simp]: "- (x \<sqinter> y) = - x \<squnion> - y"
-proof (rule compl_unique)
- have "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = (y \<sqinter> (x \<sqinter> - x)) \<squnion> (x \<sqinter> (y \<sqinter> - y))"
- by (simp only: inf_sup_distrib inf_aci)
- then show "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = \<bottom>"
- by (simp add: inf_compl_bot)
-next
- have "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = (- y \<squnion> (x \<squnion> - x)) \<sqinter> (- x \<squnion> (y \<squnion> - y))"
- by (simp only: sup_inf_distrib sup_aci)
- then show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = \<top>"
- by (simp add: sup_compl_top)
-qed
-
-lemma compl_sup [simp]: "- (x \<squnion> y) = - x \<sqinter> - y"
- using dual_boolean_algebra
- by (rule boolean_algebra.compl_inf)
-
-lemma compl_mono:
- assumes "x \<le> y"
- shows "- y \<le> - x"
-proof -
- from assms have "x \<squnion> y = y" by (simp only: le_iff_sup)
- then have "- (x \<squnion> y) = - y" by simp
- then have "- x \<sqinter> - y = - y" by simp
- then have "- y \<sqinter> - x = - y" by (simp only: inf_commute)
- then show ?thesis by (simp only: le_iff_inf)
-qed
-
-lemma compl_le_compl_iff [simp]: "- x \<le> - y \<longleftrightarrow> y \<le> x"
- by (auto dest: compl_mono)
-
-lemma compl_le_swap1:
- assumes "y \<le> - x"
- shows "x \<le> -y"
-proof -
- from assms have "- (- x) \<le> - y" by (simp only: compl_le_compl_iff)
- then show ?thesis by simp
-qed
-
-lemma compl_le_swap2:
- assumes "- y \<le> x"
- shows "- x \<le> y"
-proof -
- from assms have "- x \<le> - (- y)" by (simp only: compl_le_compl_iff)
- then show ?thesis by simp
-qed
-
-lemma compl_less_compl_iff [simp]: "- x < - y \<longleftrightarrow> y < x"
- by (auto simp add: less_le)
-
-lemma compl_less_swap1:
- assumes "y < - x"
- shows "x < - y"
-proof -
- from assms have "- (- x) < - y" by (simp only: compl_less_compl_iff)
- then show ?thesis by simp
-qed
-
-lemma compl_less_swap2:
- assumes "- y < x"
- shows "- x < y"
-proof -
- from assms have "- x < - (- y)"
- by (simp only: compl_less_compl_iff)
- then show ?thesis by simp
-qed
-
-lemma sup_cancel_left1: "sup (sup x a) (sup (- x) b) = top"
- by (simp add: ac_simps sup_compl_top)
-
-lemma sup_cancel_left2: "sup (sup (- x) a) (sup x b) = top"
- by (simp add: ac_simps sup_compl_top)
-
-lemma inf_cancel_left1: "inf (inf x a) (inf (- x) b) = bot"
- by (simp add: ac_simps inf_compl_bot)
-
-lemma inf_cancel_left2: "inf (inf (- x) a) (inf x b) = bot"
- by (simp add: ac_simps inf_compl_bot)
-
-declare inf_compl_bot [simp]
- and sup_compl_top [simp]
-
-lemma sup_compl_top_left1 [simp]: "sup (- x) (sup x y) = top"
- by (simp add: sup_assoc[symmetric])
-
-lemma sup_compl_top_left2 [simp]: "sup x (sup (- x) y) = top"
- using sup_compl_top_left1[of "- x" y] by simp
-
-lemma inf_compl_bot_left1 [simp]: "inf (- x) (inf x y) = bot"
- by (simp add: inf_assoc[symmetric])
-
-lemma inf_compl_bot_left2 [simp]: "inf x (inf (- x) y) = bot"
- using inf_compl_bot_left1[of "- x" y] by simp
-
-lemma inf_compl_bot_right [simp]: "inf x (inf y (- x)) = bot"
- by (subst inf_left_commute) simp
-
-end
-
-locale boolean_algebra_cancel
-begin
-
-lemma sup1: "(A::'a::semilattice_sup) \<equiv> sup k a \<Longrightarrow> sup A b \<equiv> sup k (sup a b)"
- by (simp only: ac_simps)
-
-lemma sup2: "(B::'a::semilattice_sup) \<equiv> sup k b \<Longrightarrow> sup a B \<equiv> sup k (sup a b)"
- by (simp only: ac_simps)
-
-lemma sup0: "(a::'a::bounded_semilattice_sup_bot) \<equiv> sup a bot"
- by simp
-
-lemma inf1: "(A::'a::semilattice_inf) \<equiv> inf k a \<Longrightarrow> inf A b \<equiv> inf k (inf a b)"
- by (simp only: ac_simps)
-
-lemma inf2: "(B::'a::semilattice_inf) \<equiv> inf k b \<Longrightarrow> inf a B \<equiv> inf k (inf a b)"
- by (simp only: ac_simps)
-
-lemma inf0: "(a::'a::bounded_semilattice_inf_top) \<equiv> inf a top"
- by simp
-
-end
-
-ML_file \<open>Tools/boolean_algebra_cancel.ML\<close>
-
-simproc_setup boolean_algebra_cancel_sup ("sup a b::'a::boolean_algebra") =
- \<open>fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_sup_conv\<close>
-
-simproc_setup boolean_algebra_cancel_inf ("inf a b::'a::boolean_algebra") =
- \<open>fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_inf_conv\<close>
-
subsection \<open>\<open>min/max\<close> as special case of lattice\<close>
@@ -853,33 +663,6 @@
qed
-subsection \<open>Lattice on \<^typ>\<open>bool\<close>\<close>
-
-instantiation bool :: boolean_algebra
-begin
-
-definition bool_Compl_def [simp]: "uminus = Not"
-
-definition bool_diff_def [simp]: "A - B \<longleftrightarrow> A \<and> \<not> B"
-
-definition [simp]: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
-
-definition [simp]: "P \<squnion> Q \<longleftrightarrow> P \<or> Q"
-
-instance by standard auto
-
-end
-
-lemma sup_boolI1: "P \<Longrightarrow> P \<squnion> Q"
- by simp
-
-lemma sup_boolI2: "Q \<Longrightarrow> P \<squnion> Q"
- by simp
-
-lemma sup_boolE: "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
- by auto
-
-
subsection \<open>Lattice on \<^typ>\<open>_ \<Rightarrow> _\<close>\<close>
instantiation "fun" :: (type, semilattice_sup) semilattice_sup
@@ -938,60 +721,4 @@
end
-instance "fun" :: (type, boolean_algebra) boolean_algebra
- by standard (rule ext, simp_all add: inf_compl_bot sup_compl_top diff_eq)+
-
-
-subsection \<open>Lattice on unary and binary predicates\<close>
-
-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 (rule inf1E)
-
-lemma inf2D1: "(A \<sqinter> B) x y \<Longrightarrow> A x y"
- by (rule inf2E)
-
-lemma inf1D2: "(A \<sqinter> B) x \<Longrightarrow> B x"
- by (rule inf1E)
-
-lemma inf2D2: "(A \<sqinter> B) x y \<Longrightarrow> B x y"
- by (rule inf2E)
-
-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 \<open> \<^medskip> Classical introduction rule: no commitment to \<open>A\<close> vs \<open>B\<close>.\<close>
-
-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)
-
end