# HG changeset patch
# User nipkow
# Date 1701359804 -3600
# Node ID 05a753360b25897998de8373c93e11e745e28a89
# Parent  722937a213efddf9e871304d4fe956629e6f0a9b
added and removed [simp]s

diff -r 722937a213ef -r 05a753360b25 src/HOL/Boolean_Algebras.thy
--- a/src/HOL/Boolean_Algebras.thy	Wed Nov 29 21:29:00 2023 +0100
+++ b/src/HOL/Boolean_Algebras.thy	Thu Nov 30 16:56:44 2023 +0100
@@ -549,9 +549,12 @@
   using inf_shunt [of \<open>- x\<close> \<open>- y\<close>, symmetric] 
   by (simp flip: compl_sup compl_top_eq)
 
-lemma diff_shunt_var: "(x - y = \<bottom>) \<longleftrightarrow> (x \<le> y)"
+lemma diff_shunt_var[simp]: "(x - y = \<bottom>) \<longleftrightarrow> (x \<le> y)"
   by (simp add: diff_eq inf_shunt)
 
+lemma diff_shunt[simp]: "(\<bottom> = x - y) \<longleftrightarrow> (x \<le> y)"
+  by (auto simp flip: diff_shunt_var)
+
 lemma sup_neg_inf:
   \<open>p \<le> q \<squnion> r \<longleftrightarrow> p \<sqinter> -q \<le> r\<close>  (is \<open>?P \<longleftrightarrow> ?Q\<close>)
 proof
diff -r 722937a213ef -r 05a753360b25 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Wed Nov 29 21:29:00 2023 +0100
+++ b/src/HOL/Lattices.thy	Thu Nov 30 16:56:44 2023 +0100
@@ -212,7 +212,7 @@
   by (blast intro: order_trans inf_le1 inf_le2)
 
 lemma le_inf_iff: "x \<le> y \<sqinter> z \<longleftrightarrow> x \<le> y \<and> x \<le> z"
-  by (blast intro: le_infI elim: le_infE)
+  by (blast intro: le_infI elim: le_infE) (* [simp] via bounded_iff *)
 
 lemma le_iff_inf: "x \<le> y \<longleftrightarrow> x \<sqinter> y = x"
   by (auto intro: le_infI1 order.antisym dest: order.eq_iff [THEN iffD1] simp add: le_inf_iff)
@@ -238,7 +238,7 @@
   by (blast intro: order_trans sup_ge1 sup_ge2)
 
 lemma le_sup_iff: "x \<squnion> y \<le> z \<longleftrightarrow> x \<le> z \<and> y \<le> z"
-  by (blast intro: le_supI elim: le_supE)
+  by (blast intro: le_supI elim: le_supE) (* [simp] via bounded_iff *)
 
 lemma le_iff_sup: "x \<le> y \<longleftrightarrow> x \<squnion> y = y"
   by (auto intro: le_supI2 order.antisym dest: order.eq_iff [THEN iffD1] simp add: le_sup_iff)
diff -r 722937a213ef -r 05a753360b25 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Nov 29 21:29:00 2023 +0100
+++ b/src/HOL/Set.thy	Thu Nov 30 16:56:44 2023 +0100
@@ -1268,11 +1268,11 @@
 lemma Int_Un_distrib2: "(B \<union> C) \<inter> A = (B \<inter> A) \<union> (C \<inter> A)"
   by (fact inf_sup_distrib2)
 
-lemma Int_UNIV [simp]: "A \<inter> B = UNIV \<longleftrightarrow> A = UNIV \<and> B = UNIV"
+lemma Int_UNIV: "A \<inter> B = UNIV \<longleftrightarrow> A = UNIV \<and> B = UNIV"
   by (fact inf_eq_top_iff) (* already simp *)
 
-lemma Int_subset_iff [simp]: "C \<subseteq> A \<inter> B \<longleftrightarrow> C \<subseteq> A \<and> C \<subseteq> B"
-  by (fact le_inf_iff)
+lemma Int_subset_iff: "C \<subseteq> A \<inter> B \<longleftrightarrow> C \<subseteq> A \<and> C \<subseteq> B"
+  by (fact le_inf_iff) (* already simp *)
 
 lemma Int_Collect: "x \<in> A \<inter> {x. P x} \<longleftrightarrow> x \<in> A \<and> P x"
   by blast
@@ -1355,8 +1355,8 @@
 lemma Un_empty [iff]: "A \<union> B = {} \<longleftrightarrow> A = {} \<and> B = {}"
   by (fact sup_eq_bot_iff) (* FIXME: already simp *)
 
-lemma Un_subset_iff [simp]: "A \<union> B \<subseteq> C \<longleftrightarrow> A \<subseteq> C \<and> B \<subseteq> C"
-  by (fact le_sup_iff)
+lemma Un_subset_iff: "A \<union> B \<subseteq> C \<longleftrightarrow> A \<subseteq> C \<and> B \<subseteq> C"
+  by (fact le_sup_iff) (* already simp *)
 
 lemma Un_Diff_Int: "(A - B) \<union> (A \<inter> B) = A"
   by blast
@@ -1440,10 +1440,10 @@
 text \<open>\<^medskip> Set difference.\<close>
 
 lemma Diff_eq: "A - B = A \<inter> (- B)"
-  by blast
-
-lemma Diff_eq_empty_iff [simp]: "A - B = {} \<longleftrightarrow> A \<subseteq> B"
-  by blast
+  by(rule boolean_algebra_class.diff_eq)
+
+lemma Diff_eq_empty_iff: "A - B = {} \<longleftrightarrow> A \<subseteq> B"
+  by(rule boolean_algebra_class.diff_shunt_var) (* already simp *)
 
 lemma Diff_cancel [simp]: "A - A = {}"
   by blast