generalized and augmented

--- a/src/HOL/Lattices.thy	Wed May 20 22:07:41 2020 +0200
+++ b/src/HOL/Lattices.thy	Wed May 20 19:43:39 2020 +0000
@@ -137,6 +137,12 @@
 sublocale ordering_top less_eq less "\<^bold>1"
   by standard (simp add: order_iff)
 
+lemma eq_neutr_iff [simp]: \<open>a \<^bold>* b = \<^bold>1 \<longleftrightarrow> a = \<^bold>1 \<and> b = \<^bold>1\<close>
+  by (simp add: eq_iff)
+
+lemma neutr_eq_iff [simp]: \<open>\<^bold>1 = a \<^bold>* b \<longleftrightarrow> a = \<^bold>1 \<and> b = \<^bold>1\<close>
+  by (simp add: eq_iff)
+
 end
 
 text \<open>Passive interpretations for boolean operators\<close>
@@ -462,6 +468,18 @@
     by (rule inf_absorb1) simp
 qed
 
+lemma inf_top_left: "\<top> \<sqinter> x = x"
+  by (fact inf_top.left_neutral)
+
+lemma inf_top_right: "x \<sqinter> \<top> = x"
+  by (fact inf_top.right_neutral)
+
+lemma inf_eq_top_iff: "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
+  by (fact inf_top.eq_neutr_iff)
+
+lemma top_eq_inf_iff: "\<top> = x \<sqinter> y \<longleftrightarrow> x = \<top> \<and> y = \<top>"
+  by (fact inf_top.neutr_eq_iff)
+
 end
 
 class bounded_semilattice_sup_bot = semilattice_sup + order_bot
@@ -474,6 +492,18 @@
     by (rule sup_absorb1) simp
 qed
 
+lemma sup_bot_left: "\<bottom> \<squnion> x = x"
+  by (fact sup_bot.left_neutral)
+
+lemma sup_bot_right: "x \<squnion> \<bottom> = x"
+  by (fact sup_bot.right_neutral)
+
+lemma sup_eq_bot_iff: "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
+  by (fact sup_bot.eq_neutr_iff)
+
+lemma bot_eq_sup_iff: "\<bottom> = x \<squnion> y \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
+  by (fact sup_bot.neutr_eq_iff)
+
 end
 
 class bounded_lattice_bot = lattice + order_bot
@@ -487,18 +517,6 @@
 lemma inf_bot_right [simp]: "x \<sqinter> \<bottom> = \<bottom>"
   by (rule inf_absorb2) simp
 
-lemma sup_bot_left: "\<bottom> \<squnion> x = x"
-  by (fact sup_bot.left_neutral)
-
-lemma sup_bot_right: "x \<squnion> \<bottom> = x"
-  by (fact sup_bot.right_neutral)
-
-lemma sup_eq_bot_iff [simp]: "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
-  by (simp add: eq_iff)
-
-lemma bot_eq_sup_iff [simp]: "\<bottom> = x \<squnion> y \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
-  by (simp add: eq_iff)
-
 end
 
 class bounded_lattice_top = lattice + order_top
@@ -512,15 +530,6 @@
 lemma sup_top_right [simp]: "x \<squnion> \<top> = \<top>"
   by (rule sup_absorb2) simp
 
-lemma inf_top_left: "\<top> \<sqinter> x = x"
-  by (fact inf_top.left_neutral)
-
-lemma inf_top_right: "x \<sqinter> \<top> = x"
-  by (fact inf_top.right_neutral)
-
-lemma inf_eq_top_iff [simp]: "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
-  by (simp add: eq_iff)
-
 end
 
 class bounded_lattice = lattice + order_bot + order_top

--- a/src/HOL/Nat.thy	Wed May 20 22:07:41 2020 +0200
+++ b/src/HOL/Nat.thy	Wed May 20 19:43:39 2020 +0000
@@ -863,6 +863,12 @@
 
 subsubsection \<open>\<^term>\<open>min\<close> and \<^term>\<open>max\<close>\<close>
 
+global_interpretation bot_nat_0: ordering_top \<open>(\<ge>)\<close> \<open>(>)\<close> \<open>0::nat\<close>
+  by standard simp
+
+global_interpretation max_nat: semilattice_neutr_order max \<open>0::nat\<close> \<open>(\<ge>)\<close> \<open>(>)\<close>
+  by standard (simp add: max_def)
+
 lemma mono_Suc: "mono Suc"
   by (rule monoI) simp
 
@@ -885,11 +891,11 @@
 
 lemma max_0L [simp]: "max 0 n = n"
   for n :: nat
-  by (rule max_absorb2) simp
+  by (fact max_nat.left_neutral)
 
 lemma max_0R [simp]: "max n 0 = n"
   for n :: nat
-  by (rule max_absorb1) simp
+  by (fact max_nat.right_neutral)
 
 lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc (max m n)"
   by (simp add: mono_Suc max_of_mono)
@@ -900,8 +906,8 @@
 lemma max_Suc2: "max m (Suc n) = (case m of 0 \<Rightarrow> Suc n | Suc m' \<Rightarrow> Suc (max m' n))"
   by (simp split: nat.split)
 
-lemma max_0_iff[simp]: "max m n = (0::nat) \<longleftrightarrow> m = 0 \<and> n = 0"
-by(cases m, auto simp: max_Suc1 split: nat.split)
+lemma max_0_iff: "max m n = (0::nat) \<longleftrightarrow> m = 0 \<and> n = 0"
+  by (fact max_nat.eq_neutr_iff)
 
 lemma nat_mult_min_left: "min m n * q = min (m * q) (n * q)"
   for m n q :: nat

--- a/src/HOL/Orderings.thy	Wed May 20 22:07:41 2020 +0200
+++ b/src/HOL/Orderings.thy	Wed May 20 19:43:39 2020 +0000
@@ -58,6 +58,9 @@
   "a \<^bold>< b \<Longrightarrow> b \<^bold>< c \<Longrightarrow> a \<^bold>< c"
   by (auto intro: strict_trans1 strict_implies_order)
 
+lemma eq_iff: "a = b \<longleftrightarrow> a \<^bold>\<le> b \<and> b \<^bold>\<le> a"
+  by (auto simp add: refl intro: antisym)
+
 end
 
 text \<open>Alternative introduction rule with bias towards strict order\<close>
@@ -270,13 +273,13 @@
 text \<open>Asymmetry.\<close>
 
 lemma eq_iff: "x = y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
-by (blast intro: antisym)
+  by (fact order.eq_iff)
 
 lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x = y"
-by (blast intro: antisym)
+  by (simp add: eq_iff)
 
 lemma less_imp_neq: "x < y \<Longrightarrow> x \<noteq> y"
-by (fact order.strict_implies_not_eq)
+  by (fact order.strict_implies_not_eq)
 
 lemma antisym_conv1: "\<not> x < y \<Longrightarrow> x \<le> y \<longleftrightarrow> x = y"
   by (simp add: local.le_less)