locales for abstract orders
authorhaftmann
Sat Mar 23 17:11:06 2013 +0100 (2013-03-23)
changeset 51487f4bfdee99304
parent 51486 0a0c9a45d294
child 51488 3c886fe611b8
locales for abstract orders
CONTRIBUTORS
NEWS
src/HOL/Finite_Set.thy
src/HOL/Lattices.thy
src/HOL/Orderings.thy
     1.1 --- a/CONTRIBUTORS	Sat Mar 23 07:30:53 2013 +0100
     1.2 +++ b/CONTRIBUTORS	Sat Mar 23 17:11:06 2013 +0100
     1.3 @@ -6,6 +6,9 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* March 2013: Florian Haftmann, TUM
     1.8 +  Algebraic locale hierarchy for orderings and (semi)lattices.
     1.9 +
    1.10  * Feb. 2013: Florian Haftmann, TUM
    1.11    Reworking and consolidation of code generation for target
    1.12    language numerals.
     2.1 --- a/NEWS	Sat Mar 23 07:30:53 2013 +0100
     2.2 +++ b/NEWS	Sat Mar 23 17:11:06 2013 +0100
     2.3 @@ -33,6 +33,8 @@
     2.4  
     2.5  *** HOL ***
     2.6  
     2.7 +* Locale hierarchy for abstract orderings and (semi)lattices.
     2.8 +
     2.9  * Discontinued theory src/HOL/Library/Eval_Witness.
    2.10  INCOMPATIBILITY.
    2.11  
     3.1 --- a/src/HOL/Finite_Set.thy	Sat Mar 23 07:30:53 2013 +0100
     3.2 +++ b/src/HOL/Finite_Set.thy	Sat Mar 23 17:11:06 2013 +0100
     3.3 @@ -1280,8 +1280,16 @@
     3.4  
     3.5  end
     3.6  
     3.7 +class ab_semigroup_idem_mult = ab_semigroup_mult +
     3.8 +  assumes mult_idem: "x * x = x"
     3.9 +
    3.10 +sublocale ab_semigroup_idem_mult < times!: semilattice times proof
    3.11 +qed (fact mult_idem)
    3.12 +
    3.13  context ab_semigroup_idem_mult
    3.14  begin
    3.15 + 
    3.16 +lemmas mult_left_idem = times.left_idem
    3.17  
    3.18  lemma comp_fun_idem: "comp_fun_idem (op *)"
    3.19    by default (simp_all add: fun_eq_iff mult_left_commute)
     4.1 --- a/src/HOL/Lattices.thy	Sat Mar 23 07:30:53 2013 +0100
     4.2 +++ b/src/HOL/Lattices.thy	Sat Mar 23 17:11:06 2013 +0100
     4.3 @@ -11,39 +11,134 @@
     4.4  subsection {* Abstract semilattice *}
     4.5  
     4.6  text {*
     4.7 -  This locales provide a basic structure for interpretation into
     4.8 +  These locales provide a basic structure for interpretation into
     4.9    bigger structures;  extensions require careful thinking, otherwise
    4.10    undesired effects may occur due to interpretation.
    4.11  *}
    4.12  
    4.13 +no_notation times (infixl "*" 70)
    4.14 +no_notation Groups.one ("1")
    4.15 +
    4.16  locale semilattice = abel_semigroup +
    4.17 -  assumes idem [simp]: "f a a = a"
    4.18 +  assumes idem [simp]: "a * a = a"
    4.19  begin
    4.20  
    4.21 -lemma left_idem [simp]: "f a (f a b) = f a b"
    4.22 +lemma left_idem [simp]: "a * (a * b) = a * b"
    4.23  by (simp add: assoc [symmetric])
    4.24  
    4.25 -lemma right_idem [simp]: "f (f a b) b = f a b"
    4.26 +lemma right_idem [simp]: "(a * b) * b = a * b"
    4.27  by (simp add: assoc)
    4.28  
    4.29  end
    4.30  
    4.31 +locale semilattice_neutr = semilattice + comm_monoid
    4.32  
    4.33 -subsection {* Idempotent semigroup *}
    4.34 +locale semilattice_order = semilattice +
    4.35 +  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<preceq>" 50)
    4.36 +    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<prec>" 50)
    4.37 +  assumes order_iff: "a \<preceq> b \<longleftrightarrow> a = a * b"
    4.38 +    and semilattice_strict_iff_order: "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
    4.39 +begin
    4.40 +
    4.41 +lemma orderI:
    4.42 +  "a = a * b \<Longrightarrow> a \<preceq> b"
    4.43 +  by (simp add: order_iff)
    4.44 +
    4.45 +lemma orderE:
    4.46 +  assumes "a \<preceq> b"
    4.47 +  obtains "a = a * b"
    4.48 +  using assms by (unfold order_iff)
    4.49 +
    4.50 +end
    4.51  
    4.52 -class ab_semigroup_idem_mult = ab_semigroup_mult +
    4.53 -  assumes mult_idem: "x * x = x"
    4.54 +sublocale semilattice_order < ordering less_eq less
    4.55 +proof
    4.56 +  fix a b
    4.57 +  show "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
    4.58 +    by (fact semilattice_strict_iff_order)
    4.59 +next
    4.60 +  fix a
    4.61 +  show "a \<preceq> a"
    4.62 +    by (simp add: order_iff)
    4.63 +next
    4.64 +  fix a b
    4.65 +  assume "a \<preceq> b" "b \<preceq> a"
    4.66 +  then have "a = a * b" "a * b = b"
    4.67 +    by (simp_all add: order_iff commute)
    4.68 +  then show "a = b" by simp
    4.69 +next
    4.70 +  fix a b c
    4.71 +  assume "a \<preceq> b" "b \<preceq> c"
    4.72 +  then have "a = a * b" "b = b * c"
    4.73 +    by (simp_all add: order_iff commute)
    4.74 +  then have "a = a * (b * c)"
    4.75 +    by simp
    4.76 +  then have "a = (a * b) * c"
    4.77 +    by (simp add: assoc)
    4.78 +  with `a = a * b` [symmetric] have "a = a * c" by simp
    4.79 +  then show "a \<preceq> c" by (rule orderI)
    4.80 +qed
    4.81  
    4.82 -sublocale ab_semigroup_idem_mult < times!: semilattice times proof
    4.83 -qed (fact mult_idem)
    4.84 -
    4.85 -context ab_semigroup_idem_mult
    4.86 +context semilattice_order
    4.87  begin
    4.88  
    4.89 -lemmas mult_left_idem = times.left_idem
    4.90 +lemma cobounded1 [simp]:
    4.91 +  "a * b \<preceq> a"
    4.92 +  by (simp add: order_iff commute)  
    4.93 +
    4.94 +lemma cobounded2 [simp]:
    4.95 +  "a * b \<preceq> b"
    4.96 +  by (simp add: order_iff)
    4.97 +
    4.98 +lemma boundedI:
    4.99 +  assumes "a \<preceq> b" and "a \<preceq> c"
   4.100 +  shows "a \<preceq> b * c"
   4.101 +proof (rule orderI)
   4.102 +  from assms obtain "a * b = a" and "a * c = a" by (auto elim!: orderE)
   4.103 +  then show "a = a * (b * c)" by (simp add: assoc [symmetric])
   4.104 +qed
   4.105 +
   4.106 +lemma boundedE:
   4.107 +  assumes "a \<preceq> b * c"
   4.108 +  obtains "a \<preceq> b" and "a \<preceq> c"
   4.109 +  using assms by (blast intro: trans cobounded1 cobounded2)
   4.110 +
   4.111 +lemma bounded_iff:
   4.112 +  "a \<preceq> b * c \<longleftrightarrow> a \<preceq> b \<and> a \<preceq> c"
   4.113 +  by (blast intro: boundedI elim: boundedE)
   4.114 +
   4.115 +lemma strict_boundedE:
   4.116 +  assumes "a \<prec> b * c"
   4.117 +  obtains "a \<prec> b" and "a \<prec> c"
   4.118 +  using assms by (auto simp add: commute strict_iff_order bounded_iff elim: orderE intro!: that)+
   4.119 +
   4.120 +lemma coboundedI1:
   4.121 +  "a \<preceq> c \<Longrightarrow> a * b \<preceq> c"
   4.122 +  by (rule trans) auto
   4.123 +
   4.124 +lemma coboundedI2:
   4.125 +  "b \<preceq> c \<Longrightarrow> a * b \<preceq> c"
   4.126 +  by (rule trans) auto
   4.127 +
   4.128 +lemma mono: "a \<preceq> c \<Longrightarrow> b \<preceq> d \<Longrightarrow> a * b \<preceq> c * d"
   4.129 +  by (blast intro: boundedI coboundedI1 coboundedI2)
   4.130 +
   4.131 +lemma absorb1: "a \<preceq> b \<Longrightarrow> a * b = a"
   4.132 +  by (rule antisym) (auto simp add: refl bounded_iff)
   4.133 +
   4.134 +lemma absorb2: "b \<preceq> a \<Longrightarrow> a * b = b"
   4.135 +  by (rule antisym) (auto simp add: refl bounded_iff)
   4.136  
   4.137  end
   4.138  
   4.139 +locale semilattice_neutr_order = semilattice_neutr + semilattice_order
   4.140 +
   4.141 +sublocale semilattice_neutr_order < ordering_top less_eq less 1
   4.142 +  by default (simp add: order_iff)
   4.143 +
   4.144 +notation times (infixl "*" 70)
   4.145 +notation Groups.one ("1")
   4.146 +
   4.147  
   4.148  subsection {* Syntactic infimum and supremum operations *}
   4.149  
   4.150 @@ -171,6 +266,23 @@
   4.151      by (rule antisym) auto
   4.152  qed
   4.153  
   4.154 +sublocale semilattice_sup < sup!: semilattice sup
   4.155 +proof
   4.156 +  fix a b c
   4.157 +  show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"
   4.158 +    by (rule antisym) (auto intro: le_supI1 le_supI2)
   4.159 +  show "a \<squnion> b = b \<squnion> a"
   4.160 +    by (rule antisym) auto
   4.161 +  show "a \<squnion> a = a"
   4.162 +    by (rule antisym) auto
   4.163 +qed
   4.164 +
   4.165 +sublocale semilattice_inf < inf!: semilattice_order inf less_eq less
   4.166 +  by default (auto simp add: le_iff_inf less_le)
   4.167 +
   4.168 +sublocale semilattice_sup < sup!: semilattice_order sup greater_eq greater
   4.169 +  by default (auto simp add: le_iff_sup sup.commute less_le)
   4.170 +
   4.171  context semilattice_inf
   4.172  begin
   4.173  
   4.174 @@ -202,17 +314,6 @@
   4.175  
   4.176  end
   4.177  
   4.178 -sublocale semilattice_sup < sup!: semilattice sup
   4.179 -proof
   4.180 -  fix a b c
   4.181 -  show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"
   4.182 -    by (rule antisym) (auto intro: le_supI1 le_supI2)
   4.183 -  show "a \<squnion> b = b \<squnion> a"
   4.184 -    by (rule antisym) auto
   4.185 -  show "a \<squnion> a = a"
   4.186 -    by (rule antisym) auto
   4.187 -qed
   4.188 -
   4.189  context semilattice_sup
   4.190  begin
   4.191  
   4.192 @@ -367,9 +468,33 @@
   4.193  
   4.194  subsection {* Bounded lattices and boolean algebras *}
   4.195  
   4.196 +class bounded_semilattice_inf_top = semilattice_inf + top
   4.197 +
   4.198 +sublocale bounded_semilattice_inf_top < inf_top!: semilattice_neutr inf top
   4.199 +proof
   4.200 +  fix x
   4.201 +  show "x \<sqinter> \<top> = x"
   4.202 +    by (rule inf_absorb1) simp
   4.203 +qed
   4.204 +
   4.205 +sublocale bounded_semilattice_inf_top < inf_top!: semilattice_neutr_order inf top less_eq less ..
   4.206 +
   4.207 +class bounded_semilattice_sup_bot = semilattice_sup + bot
   4.208 +
   4.209 +sublocale bounded_semilattice_sup_bot < sup_bot!: semilattice_neutr sup bot
   4.210 +proof
   4.211 +  fix x
   4.212 +  show "x \<squnion> \<bottom> = x"
   4.213 +    by (rule sup_absorb1) simp
   4.214 +qed
   4.215 +
   4.216 +sublocale bounded_semilattice_sup_bot < sup_bot!: semilattice_neutr_order sup bot greater_eq greater ..
   4.217 +
   4.218  class bounded_lattice_bot = lattice + bot
   4.219  begin
   4.220  
   4.221 +subclass bounded_semilattice_sup_bot ..
   4.222 +
   4.223  lemma inf_bot_left [simp]:
   4.224    "\<bottom> \<sqinter> x = \<bottom>"
   4.225    by (rule inf_absorb1) simp
   4.226 @@ -378,13 +503,13 @@
   4.227    "x \<sqinter> \<bottom> = \<bottom>"
   4.228    by (rule inf_absorb2) simp
   4.229  
   4.230 -lemma sup_bot_left [simp]:
   4.231 +lemma sup_bot_left:
   4.232    "\<bottom> \<squnion> x = x"
   4.233 -  by (rule sup_absorb2) simp
   4.234 +  by (fact sup_bot.left_neutral)
   4.235  
   4.236 -lemma sup_bot_right [simp]:
   4.237 +lemma sup_bot_right:
   4.238    "x \<squnion> \<bottom> = x"
   4.239 -  by (rule sup_absorb1) simp
   4.240 +  by (fact sup_bot.right_neutral)
   4.241  
   4.242  lemma sup_eq_bot_iff [simp]:
   4.243    "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
   4.244 @@ -395,6 +520,8 @@
   4.245  class bounded_lattice_top = lattice + top
   4.246  begin
   4.247  
   4.248 +subclass bounded_semilattice_inf_top ..
   4.249 +
   4.250  lemma sup_top_left [simp]:
   4.251    "\<top> \<squnion> x = \<top>"
   4.252    by (rule sup_absorb1) simp
   4.253 @@ -403,13 +530,13 @@
   4.254    "x \<squnion> \<top> = \<top>"
   4.255    by (rule sup_absorb2) simp
   4.256  
   4.257 -lemma inf_top_left [simp]:
   4.258 +lemma inf_top_left:
   4.259    "\<top> \<sqinter> x = x"
   4.260 -  by (rule inf_absorb2) simp
   4.261 +  by (fact inf_top.left_neutral)
   4.262  
   4.263 -lemma inf_top_right [simp]:
   4.264 +lemma inf_top_right:
   4.265    "x \<sqinter> \<top> = x"
   4.266 -  by (rule inf_absorb1) simp
   4.267 +  by (fact inf_top.right_neutral)
   4.268  
   4.269  lemma inf_eq_top_iff [simp]:
   4.270    "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
   4.271 @@ -417,9 +544,12 @@
   4.272  
   4.273  end
   4.274  
   4.275 -class bounded_lattice = bounded_lattice_bot + bounded_lattice_top
   4.276 +class bounded_lattice = lattice + bot + top
   4.277  begin
   4.278  
   4.279 +subclass bounded_lattice_bot ..
   4.280 +subclass bounded_lattice_top ..
   4.281 +
   4.282  lemma dual_bounded_lattice:
   4.283    "class.bounded_lattice sup greater_eq greater inf \<top> \<bottom>"
   4.284    by unfold_locales (auto simp add: less_le_not_le)
     5.1 --- a/src/HOL/Orderings.thy	Sat Mar 23 07:30:53 2013 +0100
     5.2 +++ b/src/HOL/Orderings.thy	Sat Mar 23 17:11:06 2013 +0100
     5.3 @@ -12,6 +12,79 @@
     5.4  ML_file "~~/src/Provers/order.ML"
     5.5  ML_file "~~/src/Provers/quasi.ML"  (* FIXME unused? *)
     5.6  
     5.7 +subsection {* Abstract ordering *}
     5.8 +
     5.9 +locale ordering =
    5.10 +  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<preceq>" 50)
    5.11 +   and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<prec>" 50)
    5.12 +  assumes strict_iff_order: "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
    5.13 +  assumes refl: "a \<preceq> a" -- {* not @{text iff}: makes problems due to multiple (dual) interpretations *}
    5.14 +    and antisym: "a \<preceq> b \<Longrightarrow> b \<preceq> a \<Longrightarrow> a = b"
    5.15 +    and trans: "a \<preceq> b \<Longrightarrow> b \<preceq> c \<Longrightarrow> a \<preceq> c"
    5.16 +begin
    5.17 +
    5.18 +lemma strict_implies_order:
    5.19 +  "a \<prec> b \<Longrightarrow> a \<preceq> b"
    5.20 +  by (simp add: strict_iff_order)
    5.21 +
    5.22 +lemma strict_implies_not_eq:
    5.23 +  "a \<prec> b \<Longrightarrow> a \<noteq> b"
    5.24 +  by (simp add: strict_iff_order)
    5.25 +
    5.26 +lemma not_eq_order_implies_strict:
    5.27 +  "a \<noteq> b \<Longrightarrow> a \<preceq> b \<Longrightarrow> a \<prec> b"
    5.28 +  by (simp add: strict_iff_order)
    5.29 +
    5.30 +lemma order_iff_strict:
    5.31 +  "a \<preceq> b \<longleftrightarrow> a \<prec> b \<or> a = b"
    5.32 +  by (auto simp add: strict_iff_order refl)
    5.33 +
    5.34 +lemma irrefl: -- {* not @{text iff}: makes problems due to multiple (dual) interpretations *}
    5.35 +  "\<not> a \<prec> a"
    5.36 +  by (simp add: strict_iff_order)
    5.37 +
    5.38 +lemma asym:
    5.39 +  "a \<prec> b \<Longrightarrow> b \<prec> a \<Longrightarrow> False"
    5.40 +  by (auto simp add: strict_iff_order intro: antisym)
    5.41 +
    5.42 +lemma strict_trans1:
    5.43 +  "a \<preceq> b \<Longrightarrow> b \<prec> c \<Longrightarrow> a \<prec> c"
    5.44 +  by (auto simp add: strict_iff_order intro: trans antisym)
    5.45 +
    5.46 +lemma strict_trans2:
    5.47 +  "a \<prec> b \<Longrightarrow> b \<preceq> c \<Longrightarrow> a \<prec> c"
    5.48 +  by (auto simp add: strict_iff_order intro: trans antisym)
    5.49 +
    5.50 +lemma strict_trans:
    5.51 +  "a \<prec> b \<Longrightarrow> b \<prec> c \<Longrightarrow> a \<prec> c"
    5.52 +  by (auto intro: strict_trans1 strict_implies_order)
    5.53 +
    5.54 +end
    5.55 +
    5.56 +locale ordering_top = ordering +
    5.57 +  fixes top :: "'a"
    5.58 +  assumes extremum [simp]: "a \<preceq> top"
    5.59 +begin
    5.60 +
    5.61 +lemma extremum_uniqueI:
    5.62 +  "top \<preceq> a \<Longrightarrow> a = top"
    5.63 +  by (rule antisym) auto
    5.64 +
    5.65 +lemma extremum_unique:
    5.66 +  "top \<preceq> a \<longleftrightarrow> a = top"
    5.67 +  by (auto intro: antisym)
    5.68 +
    5.69 +lemma extremum_strict [simp]:
    5.70 +  "\<not> (top \<prec> a)"
    5.71 +  using extremum [of a] by (auto simp add: order_iff_strict intro: asym irrefl)
    5.72 +
    5.73 +lemma not_eq_extremum:
    5.74 +  "a \<noteq> top \<longleftrightarrow> a \<prec> top"
    5.75 +  by (auto simp add: order_iff_strict intro: not_eq_order_implies_strict extremum)
    5.76 +
    5.77 +end  
    5.78 +
    5.79 +
    5.80  subsection {* Syntactic orders *}
    5.81  
    5.82  class ord =
    5.83 @@ -119,10 +192,21 @@
    5.84    assumes antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
    5.85  begin
    5.86  
    5.87 -text {* Reflexivity. *}
    5.88 +lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
    5.89 +  by (auto simp add: less_le_not_le intro: antisym)
    5.90 +
    5.91 +end
    5.92 +
    5.93 +sublocale order < order!: ordering less_eq less
    5.94 +  by default (auto intro: antisym order_trans simp add: less_le)
    5.95  
    5.96 -lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
    5.97 -by (auto simp add: less_le_not_le intro: antisym)
    5.98 +sublocale order < dual_order!: ordering greater_eq greater
    5.99 +  by default (auto intro: antisym order_trans simp add: less_le)
   5.100 +
   5.101 +context order
   5.102 +begin
   5.103 +
   5.104 +text {* Reflexivity. *}
   5.105  
   5.106  lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x = y"
   5.107      -- {* NOT suitable for iff, since it can cause PROOF FAILED. *}
   5.108 @@ -1089,46 +1173,59 @@
   5.109  
   5.110  class bot = order +
   5.111    fixes bot :: 'a ("\<bottom>")
   5.112 -  assumes bot_least [simp]: "\<bottom> \<le> a"
   5.113 +  assumes bot_least: "\<bottom> \<le> a"
   5.114 +
   5.115 +sublocale bot < bot!: ordering_top greater_eq greater bot
   5.116 +proof
   5.117 +qed (fact bot_least)
   5.118 +
   5.119 +context bot
   5.120  begin
   5.121  
   5.122  lemma le_bot:
   5.123    "a \<le> \<bottom> \<Longrightarrow> a = \<bottom>"
   5.124 -  by (auto intro: antisym)
   5.125 +  by (fact bot.extremum_uniqueI)
   5.126  
   5.127  lemma bot_unique:
   5.128    "a \<le> \<bottom> \<longleftrightarrow> a = \<bottom>"
   5.129 -  by (auto intro: antisym)
   5.130 +  by (fact bot.extremum_unique)
   5.131  
   5.132 -lemma not_less_bot [simp]:
   5.133 -  "\<not> (a < \<bottom>)"
   5.134 -  using bot_least [of a] by (auto simp: le_less)
   5.135 +lemma not_less_bot:
   5.136 +  "\<not> a < \<bottom>"
   5.137 +  by (fact bot.extremum_strict)
   5.138  
   5.139  lemma bot_less:
   5.140    "a \<noteq> \<bottom> \<longleftrightarrow> \<bottom> < a"
   5.141 -  by (auto simp add: less_le_not_le intro!: antisym)
   5.142 +  by (fact bot.not_eq_extremum)
   5.143  
   5.144  end
   5.145  
   5.146  class top = order +
   5.147    fixes top :: 'a ("\<top>")
   5.148 -  assumes top_greatest [simp]: "a \<le> \<top>"
   5.149 +  assumes top_greatest: "a \<le> \<top>"
   5.150 +
   5.151 +sublocale top < top!: ordering_top less_eq less top
   5.152 +proof
   5.153 +qed (fact top_greatest)
   5.154 +
   5.155 +context top
   5.156  begin
   5.157  
   5.158  lemma top_le:
   5.159    "\<top> \<le> a \<Longrightarrow> a = \<top>"
   5.160 -  by (rule antisym) auto
   5.161 +  by (fact top.extremum_uniqueI)
   5.162  
   5.163  lemma top_unique:
   5.164    "\<top> \<le> a \<longleftrightarrow> a = \<top>"
   5.165 -  by (auto intro: antisym)
   5.166 +  by (fact top.extremum_unique)
   5.167  
   5.168 -lemma not_top_less [simp]: "\<not> (\<top> < a)"
   5.169 -  using top_greatest [of a] by (auto simp: le_less)
   5.170 +lemma not_top_less:
   5.171 +  "\<not> \<top> < a"
   5.172 +  by (fact top.extremum_strict)
   5.173  
   5.174  lemma less_top:
   5.175    "a \<noteq> \<top> \<longleftrightarrow> a < \<top>"
   5.176 -  by (auto simp add: less_le_not_le intro!: antisym)
   5.177 +  by (fact top.not_eq_extremum)
   5.178  
   5.179  end
   5.180  
   5.181 @@ -1489,3 +1586,4 @@
   5.182  lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
   5.183  
   5.184  end
   5.185 +