# HG changeset patch # User haftmann # Date 1590003819 0 # Node ID 34ecb540a07970c700ddf6344a4dc47e6bac9d46 # Parent f640380aaf86fa4581ef897a4df9d15c12722c36 generalized and augmented diff -r f640380aaf86 -r 34ecb540a079 src/HOL/Lattices.thy --- 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]: \a \<^bold>* b = \<^bold>1 \ a = \<^bold>1 \ b = \<^bold>1\ + by (simp add: eq_iff) + +lemma neutr_eq_iff [simp]: \\<^bold>1 = a \<^bold>* b \ a = \<^bold>1 \ b = \<^bold>1\ + by (simp add: eq_iff) + end text \Passive interpretations for boolean operators\ @@ -462,6 +468,18 @@ by (rule inf_absorb1) simp qed +lemma inf_top_left: "\ \ x = x" + by (fact inf_top.left_neutral) + +lemma inf_top_right: "x \ \ = x" + by (fact inf_top.right_neutral) + +lemma inf_eq_top_iff: "x \ y = \ \ x = \ \ y = \" + by (fact inf_top.eq_neutr_iff) + +lemma top_eq_inf_iff: "\ = x \ y \ x = \ \ y = \" + 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: "\ \ x = x" + by (fact sup_bot.left_neutral) + +lemma sup_bot_right: "x \ \ = x" + by (fact sup_bot.right_neutral) + +lemma sup_eq_bot_iff: "x \ y = \ \ x = \ \ y = \" + by (fact sup_bot.eq_neutr_iff) + +lemma bot_eq_sup_iff: "\ = x \ y \ x = \ \ y = \" + 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 \ \ = \" by (rule inf_absorb2) simp -lemma sup_bot_left: "\ \ x = x" - by (fact sup_bot.left_neutral) - -lemma sup_bot_right: "x \ \ = x" - by (fact sup_bot.right_neutral) - -lemma sup_eq_bot_iff [simp]: "x \ y = \ \ x = \ \ y = \" - by (simp add: eq_iff) - -lemma bot_eq_sup_iff [simp]: "\ = x \ y \ x = \ \ y = \" - by (simp add: eq_iff) - end class bounded_lattice_top = lattice + order_top @@ -512,15 +530,6 @@ lemma sup_top_right [simp]: "x \ \ = \" by (rule sup_absorb2) simp -lemma inf_top_left: "\ \ x = x" - by (fact inf_top.left_neutral) - -lemma inf_top_right: "x \ \ = x" - by (fact inf_top.right_neutral) - -lemma inf_eq_top_iff [simp]: "x \ y = \ \ x = \ \ y = \" - by (simp add: eq_iff) - end class bounded_lattice = lattice + order_bot + order_top diff -r f640380aaf86 -r 34ecb540a079 src/HOL/Nat.thy --- 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 \\<^term>\min\ and \<^term>\max\\ +global_interpretation bot_nat_0: ordering_top \(\)\ \(>)\ \0::nat\ + by standard simp + +global_interpretation max_nat: semilattice_neutr_order max \0::nat\ \(\)\ \(>)\ + 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 \ Suc n | Suc m' \ Suc (max m' n))" by (simp split: nat.split) -lemma max_0_iff[simp]: "max m n = (0::nat) \ m = 0 \ n = 0" -by(cases m, auto simp: max_Suc1 split: nat.split) +lemma max_0_iff: "max m n = (0::nat) \ m = 0 \ 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 diff -r f640380aaf86 -r 34ecb540a079 src/HOL/Orderings.thy --- 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 \ b \<^bold>< c \ a \<^bold>< c" by (auto intro: strict_trans1 strict_implies_order) +lemma eq_iff: "a = b \ a \<^bold>\ b \ b \<^bold>\ a" + by (auto simp add: refl intro: antisym) + end text \Alternative introduction rule with bias towards strict order\ @@ -270,13 +273,13 @@ text \Asymmetry.\ lemma eq_iff: "x = y \ x \ y \ y \ x" -by (blast intro: antisym) + by (fact order.eq_iff) lemma antisym_conv: "y \ x \ x \ y \ x = y" -by (blast intro: antisym) + by (simp add: eq_iff) lemma less_imp_neq: "x < y \ x \ y" -by (fact order.strict_implies_not_eq) + by (fact order.strict_implies_not_eq) lemma antisym_conv1: "\ x < y \ x \ y \ x = y" by (simp add: local.le_less)