generalized and augmented
authorhaftmann
Wed May 20 19:43:39 2020 +0000 (11 days ago)
changeset 7185134ecb540a079
parent 71850 f640380aaf86
child 71852 76784f47c60f
generalized and augmented
src/HOL/Lattices.thy
src/HOL/Nat.thy
src/HOL/Orderings.thy
     1.1 --- a/src/HOL/Lattices.thy	Wed May 20 22:07:41 2020 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Wed May 20 19:43:39 2020 +0000
     1.3 @@ -137,6 +137,12 @@
     1.4  sublocale ordering_top less_eq less "\<^bold>1"
     1.5    by standard (simp add: order_iff)
     1.6  
     1.7 +lemma eq_neutr_iff [simp]: \<open>a \<^bold>* b = \<^bold>1 \<longleftrightarrow> a = \<^bold>1 \<and> b = \<^bold>1\<close>
     1.8 +  by (simp add: eq_iff)
     1.9 +
    1.10 +lemma neutr_eq_iff [simp]: \<open>\<^bold>1 = a \<^bold>* b \<longleftrightarrow> a = \<^bold>1 \<and> b = \<^bold>1\<close>
    1.11 +  by (simp add: eq_iff)
    1.12 +
    1.13  end
    1.14  
    1.15  text \<open>Passive interpretations for boolean operators\<close>
    1.16 @@ -462,6 +468,18 @@
    1.17      by (rule inf_absorb1) simp
    1.18  qed
    1.19  
    1.20 +lemma inf_top_left: "\<top> \<sqinter> x = x"
    1.21 +  by (fact inf_top.left_neutral)
    1.22 +
    1.23 +lemma inf_top_right: "x \<sqinter> \<top> = x"
    1.24 +  by (fact inf_top.right_neutral)
    1.25 +
    1.26 +lemma inf_eq_top_iff: "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
    1.27 +  by (fact inf_top.eq_neutr_iff)
    1.28 +
    1.29 +lemma top_eq_inf_iff: "\<top> = x \<sqinter> y \<longleftrightarrow> x = \<top> \<and> y = \<top>"
    1.30 +  by (fact inf_top.neutr_eq_iff)
    1.31 +
    1.32  end
    1.33  
    1.34  class bounded_semilattice_sup_bot = semilattice_sup + order_bot
    1.35 @@ -474,6 +492,18 @@
    1.36      by (rule sup_absorb1) simp
    1.37  qed
    1.38  
    1.39 +lemma sup_bot_left: "\<bottom> \<squnion> x = x"
    1.40 +  by (fact sup_bot.left_neutral)
    1.41 +
    1.42 +lemma sup_bot_right: "x \<squnion> \<bottom> = x"
    1.43 +  by (fact sup_bot.right_neutral)
    1.44 +
    1.45 +lemma sup_eq_bot_iff: "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
    1.46 +  by (fact sup_bot.eq_neutr_iff)
    1.47 +
    1.48 +lemma bot_eq_sup_iff: "\<bottom> = x \<squnion> y \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
    1.49 +  by (fact sup_bot.neutr_eq_iff)
    1.50 +
    1.51  end
    1.52  
    1.53  class bounded_lattice_bot = lattice + order_bot
    1.54 @@ -487,18 +517,6 @@
    1.55  lemma inf_bot_right [simp]: "x \<sqinter> \<bottom> = \<bottom>"
    1.56    by (rule inf_absorb2) simp
    1.57  
    1.58 -lemma sup_bot_left: "\<bottom> \<squnion> x = x"
    1.59 -  by (fact sup_bot.left_neutral)
    1.60 -
    1.61 -lemma sup_bot_right: "x \<squnion> \<bottom> = x"
    1.62 -  by (fact sup_bot.right_neutral)
    1.63 -
    1.64 -lemma sup_eq_bot_iff [simp]: "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
    1.65 -  by (simp add: eq_iff)
    1.66 -
    1.67 -lemma bot_eq_sup_iff [simp]: "\<bottom> = x \<squnion> y \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
    1.68 -  by (simp add: eq_iff)
    1.69 -
    1.70  end
    1.71  
    1.72  class bounded_lattice_top = lattice + order_top
    1.73 @@ -512,15 +530,6 @@
    1.74  lemma sup_top_right [simp]: "x \<squnion> \<top> = \<top>"
    1.75    by (rule sup_absorb2) simp
    1.76  
    1.77 -lemma inf_top_left: "\<top> \<sqinter> x = x"
    1.78 -  by (fact inf_top.left_neutral)
    1.79 -
    1.80 -lemma inf_top_right: "x \<sqinter> \<top> = x"
    1.81 -  by (fact inf_top.right_neutral)
    1.82 -
    1.83 -lemma inf_eq_top_iff [simp]: "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
    1.84 -  by (simp add: eq_iff)
    1.85 -
    1.86  end
    1.87  
    1.88  class bounded_lattice = lattice + order_bot + order_top
     2.1 --- a/src/HOL/Nat.thy	Wed May 20 22:07:41 2020 +0200
     2.2 +++ b/src/HOL/Nat.thy	Wed May 20 19:43:39 2020 +0000
     2.3 @@ -863,6 +863,12 @@
     2.4  
     2.5  subsubsection \<open>\<^term>\<open>min\<close> and \<^term>\<open>max\<close>\<close>
     2.6  
     2.7 +global_interpretation bot_nat_0: ordering_top \<open>(\<ge>)\<close> \<open>(>)\<close> \<open>0::nat\<close>
     2.8 +  by standard simp
     2.9 +
    2.10 +global_interpretation max_nat: semilattice_neutr_order max \<open>0::nat\<close> \<open>(\<ge>)\<close> \<open>(>)\<close>
    2.11 +  by standard (simp add: max_def)
    2.12 +
    2.13  lemma mono_Suc: "mono Suc"
    2.14    by (rule monoI) simp
    2.15  
    2.16 @@ -885,11 +891,11 @@
    2.17  
    2.18  lemma max_0L [simp]: "max 0 n = n"
    2.19    for n :: nat
    2.20 -  by (rule max_absorb2) simp
    2.21 +  by (fact max_nat.left_neutral)
    2.22  
    2.23  lemma max_0R [simp]: "max n 0 = n"
    2.24    for n :: nat
    2.25 -  by (rule max_absorb1) simp
    2.26 +  by (fact max_nat.right_neutral)
    2.27  
    2.28  lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc (max m n)"
    2.29    by (simp add: mono_Suc max_of_mono)
    2.30 @@ -900,8 +906,8 @@
    2.31  lemma max_Suc2: "max m (Suc n) = (case m of 0 \<Rightarrow> Suc n | Suc m' \<Rightarrow> Suc (max m' n))"
    2.32    by (simp split: nat.split)
    2.33  
    2.34 -lemma max_0_iff[simp]: "max m n = (0::nat) \<longleftrightarrow> m = 0 \<and> n = 0"
    2.35 -by(cases m, auto simp: max_Suc1 split: nat.split)
    2.36 +lemma max_0_iff: "max m n = (0::nat) \<longleftrightarrow> m = 0 \<and> n = 0"
    2.37 +  by (fact max_nat.eq_neutr_iff)
    2.38  
    2.39  lemma nat_mult_min_left: "min m n * q = min (m * q) (n * q)"
    2.40    for m n q :: nat
     3.1 --- a/src/HOL/Orderings.thy	Wed May 20 22:07:41 2020 +0200
     3.2 +++ b/src/HOL/Orderings.thy	Wed May 20 19:43:39 2020 +0000
     3.3 @@ -58,6 +58,9 @@
     3.4    "a \<^bold>< b \<Longrightarrow> b \<^bold>< c \<Longrightarrow> a \<^bold>< c"
     3.5    by (auto intro: strict_trans1 strict_implies_order)
     3.6  
     3.7 +lemma eq_iff: "a = b \<longleftrightarrow> a \<^bold>\<le> b \<and> b \<^bold>\<le> a"
     3.8 +  by (auto simp add: refl intro: antisym)
     3.9 +
    3.10  end
    3.11  
    3.12  text \<open>Alternative introduction rule with bias towards strict order\<close>
    3.13 @@ -270,13 +273,13 @@
    3.14  text \<open>Asymmetry.\<close>
    3.15  
    3.16  lemma eq_iff: "x = y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
    3.17 -by (blast intro: antisym)
    3.18 +  by (fact order.eq_iff)
    3.19  
    3.20  lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x = y"
    3.21 -by (blast intro: antisym)
    3.22 +  by (simp add: eq_iff)
    3.23  
    3.24  lemma less_imp_neq: "x < y \<Longrightarrow> x \<noteq> y"
    3.25 -by (fact order.strict_implies_not_eq)
    3.26 +  by (fact order.strict_implies_not_eq)
    3.27  
    3.28  lemma antisym_conv1: "\<not> x < y \<Longrightarrow> x \<le> y \<longleftrightarrow> x = y"
    3.29    by (simp add: local.le_less)