# HG changeset patch
# User haftmann
# Date 1615446338 0
# Node ID 1f13669662965fc80ae82b1d561bc7b0d0bdd6a0
# Parent  7b59d2945e546575ca2444cd2a03d0b4ca8de2fa
avoid name clash

diff -r 7b59d2945e54 -r 1f1366966296 NEWS
--- a/NEWS	Thu Mar 11 07:05:29 2021 +0000
+++ b/NEWS	Thu Mar 11 07:05:38 2021 +0000
@@ -58,6 +58,14 @@
 * Lemma "permutes_induct" has been given named premises.
 INCOMPATIBILITY.
 
+* Theorems "antisym" and "eq_iff" in class "order" have been renamed to
+"order.antisym" and "order.eq_iff", to coexist locally with "antisym"
+and "eq_iff" from locale "ordering".  INCOMPATIBILITY: significant
+potential for change can be avoided if interpretations of type class
+"order" are replaced or augmented by interpretations of locale
+"ordering".
+
+
 
 *** ML ***
 
diff -r 7b59d2945e54 -r 1f1366966296 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/Complete_Lattices.thy	Thu Mar 11 07:05:38 2021 +0000
@@ -119,11 +119,11 @@
 
 lemma Sup_eqI:
   "(\<And>y. y \<in> A \<Longrightarrow> y \<le> x) \<Longrightarrow> (\<And>y. (\<And>z. z \<in> A \<Longrightarrow> z \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> \<Squnion>A = x"
-  by (blast intro: antisym Sup_least Sup_upper)
+  by (blast intro: order.antisym Sup_least Sup_upper)
 
 lemma Inf_eqI:
   "(\<And>i. i \<in> A \<Longrightarrow> x \<le> i) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> i) \<Longrightarrow> y \<le> x) \<Longrightarrow> \<Sqinter>A = x"
-  by (blast intro: antisym Inf_greatest Inf_lower)
+  by (blast intro: order.antisym Inf_greatest Inf_lower)
 
 lemma SUP_eqI:
   "(\<And>i. i \<in> A \<Longrightarrow> f i \<le> x) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> (\<Squnion>i\<in>A. f i) = x"
@@ -170,13 +170,13 @@
   using Sup_le_iff [of "f ` A"] by simp
 
 lemma Inf_insert [simp]: "\<Sqinter>(insert a A) = a \<sqinter> \<Sqinter>A"
-  by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
+  by (auto intro: le_infI le_infI1 le_infI2 order.antisym Inf_greatest Inf_lower)
 
 lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> \<Sqinter>(f ` A)"
   by simp
 
 lemma Sup_insert [simp]: "\<Squnion>(insert a A) = a \<squnion> \<Squnion>A"
-  by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
+  by (auto intro: le_supI le_supI1 le_supI2 order.antisym Sup_least Sup_upper)
 
 lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> \<Squnion>(f ` A)"
   by simp
@@ -188,16 +188,16 @@
   by simp
 
 lemma Inf_UNIV [simp]: "\<Sqinter>UNIV = \<bottom>"
-  by (auto intro!: antisym Inf_lower)
+  by (auto intro!: order.antisym Inf_lower)
 
 lemma Sup_UNIV [simp]: "\<Squnion>UNIV = \<top>"
-  by (auto intro!: antisym Sup_upper)
+  by (auto intro!: order.antisym Sup_upper)
 
 lemma Inf_eq_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<le> a}"
-  by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
+  by (auto intro: order.antisym Inf_lower Inf_greatest Sup_upper Sup_least)
 
 lemma Sup_eq_Inf:  "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<le> b}"
-  by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
+  by (auto intro: order.antisym Inf_lower Inf_greatest Sup_upper Sup_least)
 
 lemma Inf_superset_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<le> \<Sqinter>B"
   by (auto intro: Inf_greatest Inf_lower)
@@ -268,13 +268,13 @@
   assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<ge> g j"
     and "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<ge> f i"
   shows "\<Sqinter>(f ` A) = \<Sqinter>(g ` B)"
-  by (intro antisym INF_greatest) (blast intro: INF_lower2 dest: assms)+
+  by (intro order.antisym INF_greatest) (blast intro: INF_lower2 dest: assms)+
 
 lemma SUP_eq:
   assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<le> g j"
     and "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<le> f i"
   shows "\<Squnion>(f ` A) = \<Squnion>(g ` B)"
-  by (intro antisym SUP_least) (blast intro: SUP_upper2 dest: assms)+
+  by (intro order.antisym SUP_least) (blast intro: SUP_upper2 dest: assms)+
 
 lemma less_eq_Inf_inter: "\<Sqinter>A \<squnion> \<Sqinter>B \<le> \<Sqinter>(A \<inter> B)"
   by (auto intro: Inf_greatest Inf_lower)
@@ -283,23 +283,23 @@
   by (auto intro: Sup_least Sup_upper)
 
 lemma Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"
-  by (rule antisym) (auto intro: Inf_greatest Inf_lower le_infI1 le_infI2)
+  by (rule order.antisym) (auto intro: Inf_greatest Inf_lower le_infI1 le_infI2)
 
 lemma INF_union: "(\<Sqinter>i \<in> A \<union> B. M i) = (\<Sqinter>i \<in> A. M i) \<sqinter> (\<Sqinter>i\<in>B. M i)"
-  by (auto intro!: antisym INF_mono intro: le_infI1 le_infI2 INF_greatest INF_lower)
+  by (auto intro!: order.antisym INF_mono intro: le_infI1 le_infI2 INF_greatest INF_lower)
 
 lemma Sup_union_distrib: "\<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B"
-  by (rule antisym) (auto intro: Sup_least Sup_upper le_supI1 le_supI2)
+  by (rule order.antisym) (auto intro: Sup_least Sup_upper le_supI1 le_supI2)
 
 lemma SUP_union: "(\<Squnion>i \<in> A \<union> B. M i) = (\<Squnion>i \<in> A. M i) \<squnion> (\<Squnion>i\<in>B. M i)"
-  by (auto intro!: antisym SUP_mono intro: le_supI1 le_supI2 SUP_least SUP_upper)
+  by (auto intro!: order.antisym SUP_mono intro: le_supI1 le_supI2 SUP_least SUP_upper)
 
 lemma INF_inf_distrib: "(\<Sqinter>a\<in>A. f a) \<sqinter> (\<Sqinter>a\<in>A. g a) = (\<Sqinter>a\<in>A. f a \<sqinter> g a)"
-  by (rule antisym) (rule INF_greatest, auto intro: le_infI1 le_infI2 INF_lower INF_mono)
+  by (rule order.antisym) (rule INF_greatest, auto intro: le_infI1 le_infI2 INF_lower INF_mono)
 
 lemma SUP_sup_distrib: "(\<Squnion>a\<in>A. f a) \<squnion> (\<Squnion>a\<in>A. g a) = (\<Squnion>a\<in>A. f a \<squnion> g a)"
   (is "?L = ?R")
-proof (rule antisym)
+proof (rule order.antisym)
   show "?L \<le> ?R"
     by (auto intro: le_supI1 le_supI2 SUP_upper SUP_mono)
   show "?R \<le> ?L"
@@ -344,11 +344,17 @@
   "\<bottom> = (\<Squnion>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
   using Sup_bot_conv [of "B ` A"] by simp_all
 
+lemma INF_constant: "(\<Sqinter>y\<in>A. c) = (if A = {} then \<top> else c)"
+  by (auto intro: order.antisym INF_lower INF_greatest)
+
+lemma SUP_constant: "(\<Squnion>y\<in>A. c) = (if A = {} then \<bottom> else c)"
+  by (auto intro: order.antisym SUP_upper SUP_least)
+
 lemma INF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. f) = f"
-  by (auto intro: antisym INF_lower INF_greatest)
+  by (simp add: INF_constant)
 
 lemma SUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. f) = f"
-  by (auto intro: antisym SUP_upper SUP_least)
+  by (simp add: SUP_constant)
 
 lemma INF_top [simp]: "(\<Sqinter>x\<in>A. \<top>) = \<top>"
   by (cases "A = {}") simp_all
@@ -357,10 +363,10 @@
   by (cases "A = {}") simp_all
 
 lemma INF_commute: "(\<Sqinter>i\<in>A. \<Sqinter>j\<in>B. f i j) = (\<Sqinter>j\<in>B. \<Sqinter>i\<in>A. f i j)"
-  by (iprover intro: INF_lower INF_greatest order_trans antisym)
+  by (iprover intro: INF_lower INF_greatest order_trans order.antisym)
 
 lemma SUP_commute: "(\<Squnion>i\<in>A. \<Squnion>j\<in>B. f i j) = (\<Squnion>j\<in>B. \<Squnion>i\<in>A. f i j)"
-  by (iprover intro: SUP_upper SUP_least order_trans antisym)
+  by (iprover intro: SUP_upper SUP_least order_trans order.antisym)
 
 lemma INF_absorb:
   assumes "k \<in> I"
@@ -379,18 +385,12 @@
 qed
 
 lemma INF_inf_const1: "I \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>I. inf x (f i)) = inf x (\<Sqinter>i\<in>I. f i)"
-  by (intro antisym INF_greatest inf_mono order_refl INF_lower)
+  by (intro order.antisym INF_greatest inf_mono order_refl INF_lower)
      (auto intro: INF_lower2 le_infI2 intro!: INF_mono)
 
 lemma INF_inf_const2: "I \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>I. inf (f i) x) = inf (\<Sqinter>i\<in>I. f i) x"
   using INF_inf_const1[of I x f] by (simp add: inf_commute)
 
-lemma INF_constant: "(\<Sqinter>y\<in>A. c) = (if A = {} then \<top> else c)"
-  by simp
-
-lemma SUP_constant: "(\<Squnion>y\<in>A. c) = (if A = {} then \<bottom> else c)"
-  by simp
-
 lemma less_INF_D:
   assumes "y < (\<Sqinter>i\<in>A. f i)" "i \<in> A"
   shows "y < f i"
@@ -430,10 +430,10 @@
   by (auto intro: SUP_eqI)
 
 lemma INF_eq_iff: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<le> c) \<Longrightarrow> \<Sqinter>(f ` I) = c \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
-  by (auto intro: INF_eq_const INF_lower antisym)
+  by (auto intro: INF_eq_const INF_lower order.antisym)
 
 lemma SUP_eq_iff: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> c \<le> f i) \<Longrightarrow> \<Squnion>(f ` I) = c \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
-  by (auto intro: SUP_eq_const SUP_upper antisym)
+  by (auto intro: SUP_eq_const SUP_upper order.antisym)
 
 end
 
@@ -448,13 +448,13 @@
 begin
   
 lemma Inf_Sup: "Inf (Sup ` A) = Sup (Inf ` {f ` A | f . (\<forall> Y \<in> A . f Y \<in> Y)})"
-  by (rule antisym, rule Inf_Sup_le, rule Sup_Inf_le)
+  by (rule order.antisym, rule Inf_Sup_le, rule Sup_Inf_le)
 
 subclass distrib_lattice
 proof
   fix a b c
   show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)"
-  proof (rule antisym, simp_all, safe)
+  proof (rule order.antisym, simp_all, safe)
     show "b \<sqinter> c \<le> a \<squnion> b"
       by (rule le_infI1, simp)
     show "b \<sqinter> c \<le> a \<squnion> c"
@@ -500,7 +500,7 @@
 begin
 
 lemma uminus_Inf: "- (\<Sqinter>A) = \<Squnion>(uminus ` A)"
-proof (rule antisym)
+proof (rule order.antisym)
   show "- \<Sqinter>A \<le> \<Squnion>(uminus ` A)"
     by (rule compl_le_swap2, rule Inf_greatest, rule compl_le_swap2, rule Sup_upper) simp
   show "\<Squnion>(uminus ` A) \<le> - \<Sqinter>A"
@@ -530,10 +530,10 @@
   by (rule class.complete_linorder.intro, rule dual_complete_lattice, rule dual_linorder)
 
 lemma complete_linorder_inf_min: "inf = min"
-  by (auto intro: antisym simp add: min_def fun_eq_iff)
+  by (auto intro: order.antisym simp add: min_def fun_eq_iff)
 
 lemma complete_linorder_sup_max: "sup = max"
-  by (auto intro: antisym simp add: max_def fun_eq_iff)
+  by (auto intro: order.antisym simp add: max_def fun_eq_iff)
 
 lemma Inf_less_iff: "\<Sqinter>S < a \<longleftrightarrow> (\<exists>x\<in>S. x < a)"
   by (simp add: not_le [symmetric] le_Inf_iff)
diff -r 7b59d2945e54 -r 1f1366966296 src/HOL/Complete_Partial_Order.thy
--- a/src/HOL/Complete_Partial_Order.thy	Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/Complete_Partial_Order.thy	Thu Mar 11 07:05:38 2021 +0000
@@ -80,7 +80,7 @@
   by (rule chainI) simp
 
 lemma ccpo_Sup_singleton [simp]: "\<Squnion>{x} = x"
-  by (rule antisym) (auto intro: ccpo_Sup_least ccpo_Sup_upper simp add: chain_singleton)
+  by (rule order.antisym) (auto intro: ccpo_Sup_least ccpo_Sup_upper simp add: chain_singleton)
 
 
 subsection \<open>Transfinite iteration of a function\<close>
@@ -164,7 +164,7 @@
 lemma fixp_unfold:
   assumes f: "monotone (\<le>) (\<le>) f"
   shows "fixp f = f (fixp f)"
-proof (rule antisym)
+proof (rule order.antisym)
   show "fixp f \<le> f (fixp f)"
     by (intro iterates_le_f iterates_fixp f)
   have "f (fixp f) \<le> Sup (iterates f)"
@@ -321,7 +321,7 @@
   qed
   moreover
   have "Sup A = Sup {x \<in> A. P x}" if "\<And>x. x\<in>A \<Longrightarrow> \<exists>y\<in>A. x \<le> y \<and> P y" for P
-  proof (rule antisym)
+  proof (rule order.antisym)
     have chain_P: "chain (\<le>) {x \<in> A. P x}"
       by (rule chain_compr [OF chain])
     show "Sup A \<le> Sup {x \<in> A. P x}"
@@ -358,7 +358,7 @@
 lemma lfp_eq_fixp:
   assumes mono: "mono f"
   shows "lfp f = fixp f"
-proof (rule antisym)
+proof (rule order.antisym)
   from mono have f': "monotone (\<le>) (\<le>) f"
     unfolding mono_def monotone_def .
   show "lfp f \<le> fixp f"
diff -r 7b59d2945e54 -r 1f1366966296 src/HOL/Complex_Main.thy
--- a/src/HOL/Complex_Main.thy	Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/Complex_Main.thy	Thu Mar 11 07:05:38 2021 +0000
@@ -6,4 +6,4 @@
   MacLaurin
 begin
 
-end
+end
\ No newline at end of file
diff -r 7b59d2945e54 -r 1f1366966296 src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Thu Mar 11 07:05:38 2021 +0000
@@ -257,10 +257,10 @@
   by (metis cInf_greatest cInf_lower subsetD)
 
 lemma cSup_eq_maximum: "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X = z"
-  by (intro antisym cSup_upper[of z X] cSup_least[of X z]) auto
+  by (intro order.antisym cSup_upper[of z X] cSup_least[of X z]) auto
 
 lemma cInf_eq_minimum: "z \<in> X \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X = z"
-  by (intro antisym cInf_lower[of z X] cInf_greatest[of X z]) auto
+  by (intro order.antisym cInf_lower[of z X] cInf_greatest[of X z]) auto
 
 lemma cSup_le_iff: "S \<noteq> {} \<Longrightarrow> bdd_above S \<Longrightarrow> Sup S \<le> a \<longleftrightarrow> (\<forall>x\<in>S. x \<le> a)"
   by (metis order_trans cSup_upper cSup_least)
@@ -273,14 +273,14 @@
   assumes 2: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a"
   assumes 3: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y"
   shows "Sup X = a"
-  by (intro 3 1 antisym cSup_least) (auto intro: 2 1 cSup_upper)
+  by (intro 3 1 order.antisym cSup_least) (auto intro: 2 1 cSup_upper)
 
 lemma cInf_eq_non_empty:
   assumes 1: "X \<noteq> {}"
   assumes 2: "\<And>x. x \<in> X \<Longrightarrow> a \<le> x"
   assumes 3: "\<And>y. (\<And>x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a"
   shows "Inf X = a"
-  by (intro 3 1 antisym cInf_greatest) (auto intro: 2 1 cInf_lower)
+  by (intro 3 1 order.antisym cInf_greatest) (auto intro: 2 1 cInf_lower)
 
 lemma cInf_cSup: "S \<noteq> {} \<Longrightarrow> bdd_below S \<Longrightarrow> Inf S = Sup {x. \<forall>s\<in>S. x \<le> s}"
   by (rule cInf_eq_non_empty) (auto intro!: cSup_upper cSup_least simp: bdd_below_def)
@@ -361,10 +361,10 @@
   by (auto intro: cSUP_upper order_trans)
 
 lemma cSUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>x\<in>A. c) = c"
-  by (intro antisym cSUP_least) (auto intro: cSUP_upper)
+  by (intro order.antisym cSUP_least) (auto intro: cSUP_upper)
 
 lemma cINF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>x\<in>A. c) = c"
-  by (intro antisym cINF_greatest) (auto intro: cINF_lower)
+  by (intro order.antisym cINF_greatest) (auto intro: cINF_lower)
 
 lemma le_cINF_iff: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> u \<le> \<Sqinter>(f ` A) \<longleftrightarrow> (\<forall>x\<in>A. u \<le> f x)"
   by (metis cINF_greatest cINF_lower order_trans)
@@ -404,23 +404,23 @@
   by (metis cSup_subset_mono lattice_class.inf_sup_ord(1) le_supI1)
 
 lemma cInf_union_distrib: "A \<noteq> {} \<Longrightarrow> bdd_below A \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_below B \<Longrightarrow> Inf (A \<union> B) = inf (Inf A) (Inf B)"
-  by (intro antisym le_infI cInf_greatest cInf_lower) (auto intro: le_infI1 le_infI2 cInf_lower)
+  by (intro order.antisym le_infI cInf_greatest cInf_lower) (auto intro: le_infI1 le_infI2 cInf_lower)
 
 lemma cINF_union: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_below (f ` B) \<Longrightarrow> \<Sqinter> (f ` (A \<union> B)) = \<Sqinter> (f ` A) \<sqinter> \<Sqinter> (f ` B)"
   using cInf_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un)
 
 lemma cSup_union_distrib: "A \<noteq> {} \<Longrightarrow> bdd_above A \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_above B \<Longrightarrow> Sup (A \<union> B) = sup (Sup A) (Sup B)"
-  by (intro antisym le_supI cSup_least cSup_upper) (auto intro: le_supI1 le_supI2 cSup_upper)
+  by (intro order.antisym le_supI cSup_least cSup_upper) (auto intro: le_supI1 le_supI2 cSup_upper)
 
 lemma cSUP_union: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> B \<noteq> {} \<Longrightarrow> bdd_above (f ` B) \<Longrightarrow> \<Squnion> (f ` (A \<union> B)) = \<Squnion> (f ` A) \<squnion> \<Squnion> (f ` B)"
   using cSup_union_distrib [of "f ` A" "f ` B"] by (simp add: image_Un)
 
 lemma cINF_inf_distrib: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> bdd_below (g`A) \<Longrightarrow> \<Sqinter> (f ` A) \<sqinter> \<Sqinter> (g ` A) = (\<Sqinter>a\<in>A. inf (f a) (g a))"
-  by (intro antisym le_infI cINF_greatest cINF_lower2)
+  by (intro order.antisym le_infI cINF_greatest cINF_lower2)
      (auto intro: le_infI1 le_infI2 cINF_greatest cINF_lower le_infI)
 
 lemma SUP_sup_distrib: "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> bdd_above (g`A) \<Longrightarrow> \<Squnion> (f ` A) \<squnion> \<Squnion> (g ` A) = (\<Squnion>a\<in>A. sup (f a) (g a))"
-  by (intro antisym le_supI cSUP_least cSUP_upper2)
+  by (intro order.antisym le_supI cSUP_least cSUP_upper2)
      (auto intro: le_supI1 le_supI2 cSUP_least cSUP_upper le_supI)
 
 lemma cInf_le_cSup:
diff -r 7b59d2945e54 -r 1f1366966296 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/Fields.thy	Thu Mar 11 07:05:38 2021 +0000
@@ -1128,7 +1128,7 @@
     and minus_divide_le_eq: "- (b / c) \<le> a \<longleftrightarrow> (if 0 < c then - b \<le> a * c else if c < 0 then a * c \<le> - b else 0 \<le> a)"
     and less_minus_divide_eq: "a < - (b / c) \<longleftrightarrow> (if 0 < c then a * c < - b else if c < 0 then - b < a * c else  a < 0)"
     and minus_divide_less_eq: "- (b / c) < a \<longleftrightarrow> (if 0 < c then - b < a * c else if c < 0 then a * c < - b else 0 < a)"
-  by (auto simp: field_simps not_less dest: antisym)
+  by (auto simp: field_simps not_less dest: order.antisym)
 
 text \<open>Division and Signs\<close>
 
diff -r 7b59d2945e54 -r 1f1366966296 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/Groups.thy	Thu Mar 11 07:05:38 2021 +0000
@@ -1047,7 +1047,7 @@
     then have "b \<le> a" by (simp add: linorder_not_le)
     then have "c + b \<le> c + a" by (rule add_left_mono)
     then have "c + a = c + b"
-      using le1 by (iprover intro: antisym)
+      using le1 by (iprover intro: order.antisym)
     then have "a = b"
       by simp
     with * show False
@@ -1181,7 +1181,7 @@
 lemma abs_of_nonneg [simp]:
   assumes nonneg: "0 \<le> a"
   shows "\<bar>a\<bar> = a"
-proof (rule antisym)
+proof (rule order.antisym)
   show "a \<le> \<bar>a\<bar>" by (rule abs_ge_self)
   from nonneg le_imp_neg_le have "- a \<le> 0" by simp
   from this nonneg have "- a \<le> a" by (rule order_trans)
@@ -1189,12 +1189,12 @@
 qed
 
 lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
-  by (rule antisym) (auto intro!: abs_ge_self abs_leI order_trans [of "- \<bar>a\<bar>" 0 "\<bar>a\<bar>"])
+  by (rule order.antisym) (auto intro!: abs_ge_self abs_leI order_trans [of "- \<bar>a\<bar>" 0 "\<bar>a\<bar>"])
 
 lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
 proof -
   have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0"
-  proof (rule antisym)
+  proof (rule order.antisym)
     assume zero: "\<bar>a\<bar> = 0"
     with abs_ge_self show "a \<le> 0" by auto
     from zero have "\<bar>-a\<bar> = 0" by simp
@@ -1216,7 +1216,7 @@
 lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0"
 proof
   assume "\<bar>a\<bar> \<le> 0"
-  then have "\<bar>a\<bar> = 0" by (rule antisym) simp
+  then have "\<bar>a\<bar> = 0" by (rule order.antisym) simp
   then show "a = 0" by simp
 next
   assume "a = 0"
@@ -1319,7 +1319,7 @@
 
 lemma abs_add_abs [simp]: "\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>"
   (is "?L = ?R")
-proof (rule antisym)
+proof (rule order.antisym)
   show "?L \<ge> ?R" by (rule abs_ge_self)
   have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by (rule abs_triangle_ineq)
   also have "\<dots> = ?R" by simp
@@ -1362,7 +1362,7 @@
   by (auto simp: le_iff_add)
 
 lemma le_zero_eq[simp]: "n \<le> 0 \<longleftrightarrow> n = 0"
-  by (auto intro: antisym)
+  by (auto intro: order.antisym)
 
 lemma not_less_zero[simp]: "\<not> n < 0"
   by (auto simp: less_le)
diff -r 7b59d2945e54 -r 1f1366966296 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/Hilbert_Choice.thy	Thu Mar 11 07:05:38 2021 +0000
@@ -938,7 +938,7 @@
 begin
 
 lemma Sup_Inf: "\<Squnion> (Inf ` A) = \<Sqinter> (Sup ` {f ` A |f. \<forall>B\<in>A. f B \<in> B})"
-proof (rule antisym)
+proof (rule order.antisym)
   show "\<Squnion> (Inf ` A) \<le> \<Sqinter> (Sup ` {f ` A |f. \<forall>B\<in>A. f B \<in> B})"
     using Inf_lower2 Sup_upper
     by (fastforce simp add: intro: Sup_least INF_greatest)
@@ -985,7 +985,7 @@
                 class.complete_distrib_lattice_axioms_def Sup_Inf)
 
 lemma sup_Inf: "a \<squnion> \<Sqinter>B = \<Sqinter>((\<squnion>) a ` B)"
-proof (rule antisym)
+proof (rule order.antisym)
   show "a \<squnion> \<Sqinter>B \<le> \<Sqinter>((\<squnion>) a ` B)"
     using Inf_lower sup.mono by (fastforce intro: INF_greatest)
 next
@@ -1002,7 +1002,7 @@
   by (rule complete_distrib_lattice.sup_Inf)
 
 lemma INF_SUP: "(\<Sqinter>y. \<Squnion>x. P x y) = (\<Squnion>f. \<Sqinter>x. P (f x) x)"
-proof (rule antisym)
+proof (rule order.antisym)
   show "(SUP x. INF y. P (x y) y) \<le> (INF y. SUP x. P x y)"
     by (rule SUP_least, rule INF_greatest, rule SUP_upper2, simp_all, rule INF_lower2, simp, blast)
 next
@@ -1044,7 +1044,7 @@
 
 lemma INF_SUP_set: "(\<Sqinter>B\<in>A. \<Squnion>(g ` B)) = (\<Squnion>B\<in>{f ` A |f. \<forall>C\<in>A. f C \<in> C}. \<Sqinter>(g ` B))"
                     (is "_ = (\<Squnion>B\<in>?F. _)")
-proof (rule antisym)
+proof (rule order.antisym)
   have "\<Sqinter> ((g \<circ> f) ` A) \<le> \<Squnion> (g ` B)" if "\<And>B. B \<in> A \<Longrightarrow> f B \<in> B" "B \<in> A" for f B
     using that by (auto intro: SUP_upper2 INF_lower2)
   then show "(\<Squnion>x\<in>?F. \<Sqinter>a\<in>x. g a) \<le> (\<Sqinter>x\<in>A. \<Squnion>a\<in>x. g a)"
diff -r 7b59d2945e54 -r 1f1366966296 src/HOL/IMP/Abs_Int3.thy
--- a/src/HOL/IMP/Abs_Int3.thy	Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/IMP/Abs_Int3.thy	Thu Mar 11 07:05:38 2021 +0000
@@ -20,7 +20,7 @@
 begin
 
 lemma narrowid[simp]: "x \<triangle> x = x"
-by (metis eq_iff narrow1 narrow2)
+by (rule order.antisym) (simp_all add: narrow1 narrow2)
 
 end
 
diff -r 7b59d2945e54 -r 1f1366966296 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/Lattices.thy	Thu Mar 11 07:05:38 2021 +0000
@@ -209,7 +209,7 @@
   by (blast intro: le_infI elim: le_infE)
 
 lemma le_iff_inf: "x \<le> y \<longleftrightarrow> x \<sqinter> y = x"
-  by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1] simp add: le_inf_iff)
+  by (auto intro: le_infI1 order.antisym dest: order.eq_iff [THEN iffD1] simp add: le_inf_iff)
 
 lemma inf_mono: "a \<le> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<sqinter> b \<le> c \<sqinter> d"
   by (fast intro: inf_greatest le_infI1 le_infI2)
@@ -238,7 +238,7 @@
   by (blast intro: le_supI elim: le_supE)
 
 lemma le_iff_sup: "x \<le> y \<longleftrightarrow> x \<squnion> y = y"
-  by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1] simp add: le_sup_iff)
+  by (auto intro: le_supI2 order.antisym dest: order.eq_iff [THEN iffD1] simp add: le_sup_iff)
 
 lemma sup_mono: "a \<le> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<squnion> b \<le> c \<squnion> d"
   by (fast intro: sup_least le_supI1 le_supI2)
@@ -258,11 +258,11 @@
 proof
   fix a b c
   show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)"
-    by (rule antisym) (auto intro: le_infI1 le_infI2 simp add: le_inf_iff)
+    by (rule order.antisym) (auto intro: le_infI1 le_infI2 simp add: le_inf_iff)
   show "a \<sqinter> b = b \<sqinter> a"
-    by (rule antisym) (auto simp add: le_inf_iff)
+    by (rule order.antisym) (auto simp add: le_inf_iff)
   show "a \<sqinter> a = a"
-    by (rule antisym) (auto simp add: le_inf_iff)
+    by (rule order.antisym) (auto simp add: le_inf_iff)
 qed
 
 sublocale inf: semilattice_order inf less_eq less
@@ -287,10 +287,10 @@
   by (fact inf.right_idem) (* already simp *)
 
 lemma inf_absorb1: "x \<le> y \<Longrightarrow> x \<sqinter> y = x"
-  by (rule antisym) auto
+  by (rule order.antisym) auto
 
 lemma inf_absorb2: "y \<le> x \<Longrightarrow> x \<sqinter> y = y"
-  by (rule antisym) auto
+  by (rule order.antisym) auto
 
 lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem
 
@@ -303,11 +303,11 @@
 proof
   fix a b c
   show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"
-    by (rule antisym) (auto intro: le_supI1 le_supI2 simp add: le_sup_iff)
+    by (rule order.antisym) (auto intro: le_supI1 le_supI2 simp add: le_sup_iff)
   show "a \<squnion> b = b \<squnion> a"
-    by (rule antisym) (auto simp add: le_sup_iff)
+    by (rule order.antisym) (auto simp add: le_sup_iff)
   show "a \<squnion> a = a"
-    by (rule antisym) (auto simp add: le_sup_iff)
+    by (rule order.antisym) (auto simp add: le_sup_iff)
 qed
 
 sublocale sup: semilattice_order sup greater_eq greater
@@ -329,10 +329,10 @@
   by (fact sup.left_idem)
 
 lemma sup_absorb1: "y \<le> x \<Longrightarrow> x \<squnion> y = x"
-  by (rule antisym) auto
+  by (rule order.antisym) auto
 
 lemma sup_absorb2: "x \<le> y \<Longrightarrow> x \<squnion> y = y"
-  by (rule antisym) auto
+  by (rule order.antisym) auto
 
 lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem
 
@@ -349,10 +349,10 @@
     (unfold_locales, auto)
 
 lemma inf_sup_absorb [simp]: "x \<sqinter> (x \<squnion> y) = x"
-  by (blast intro: antisym inf_le1 inf_greatest sup_ge1)
+  by (blast intro: order.antisym inf_le1 inf_greatest sup_ge1)
 
 lemma sup_inf_absorb [simp]: "x \<squnion> (x \<sqinter> y) = x"
-  by (blast intro: antisym sup_ge1 sup_least inf_le1)
+  by (blast intro: order.antisym sup_ge1 sup_least inf_le1)
 
 lemmas inf_sup_aci = inf_aci sup_aci
 
@@ -817,7 +817,7 @@
     and le2: "\<And>x y. x \<triangle> y \<le> y"
     and greatest: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z"
   shows "x \<sqinter> y = x \<triangle> y"
-proof (rule antisym)
+proof (rule order.antisym)
   show "x \<triangle> y \<le> x \<sqinter> y"
     by (rule le_infI) (rule le1, rule le2)
   have leI: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z"
@@ -832,7 +832,7 @@
     and ge2: "\<And>x y. y \<le> x \<nabla> y"
     and least: "\<And>x y z. y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<nabla> z \<le> x"
   shows "x \<squnion> y = x \<nabla> y"
-proof (rule antisym)
+proof (rule order.antisym)
   show "x \<squnion> y \<le> x \<nabla> y"
     by (rule le_supI) (rule ge1, rule ge2)
   have leI: "\<And>x y z. x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<nabla> y \<le> z"
diff -r 7b59d2945e54 -r 1f1366966296 src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/Lattices_Big.thy	Thu Mar 11 07:05:38 2021 +0000
@@ -581,7 +581,7 @@
   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x"
     and "x \<in> A"
   shows "Min A = x"
-proof (rule antisym)
+proof (rule order.antisym)
   from \<open>x \<in> A\<close> have "A \<noteq> {}" by auto
   with assms show "Min A \<ge> x" by simp
 next
@@ -593,7 +593,7 @@
   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
     and "x \<in> A"
   shows "Max A = x"
-proof (rule antisym)
+proof (rule order.antisym)
   from \<open>x \<in> A\<close> have "A \<noteq> {}" by auto
   with assms show "Max A \<le> x" by simp
 next
@@ -602,19 +602,19 @@
 
 lemma eq_Min_iff:
   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> m = Min A  \<longleftrightarrow>  m \<in> A \<and> (\<forall>a \<in> A. m \<le> a)"
-by (meson Min_in Min_le antisym)
+by (meson Min_in Min_le order.antisym)
 
 lemma Min_eq_iff:
   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A = m  \<longleftrightarrow>  m \<in> A \<and> (\<forall>a \<in> A. m \<le> a)"
-by (meson Min_in Min_le antisym)
+by (meson Min_in Min_le order.antisym)
 
 lemma eq_Max_iff:
   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> m = Max A  \<longleftrightarrow>  m \<in> A \<and> (\<forall>a \<in> A. a \<le> m)"
-by (meson Max_in Max_ge antisym)
+by (meson Max_in Max_ge order.antisym)
 
 lemma Max_eq_iff:
   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Max A = m  \<longleftrightarrow>  m \<in> A \<and> (\<forall>a \<in> A. a \<le> m)"
-by (meson Max_in Max_ge antisym)
+by (meson Max_in Max_ge order.antisym)
 
 context
   fixes A :: "'a set"
@@ -662,7 +662,7 @@
   assume "A = {}" thus ?thesis using assms by simp
 next
   assume "A \<noteq> {}" thus ?thesis using assms
-    by(blast intro: antisym Max_in Max_ge_iff[THEN iffD2])
+    by(blast intro: order.antisym Max_in Max_ge_iff[THEN iffD2])
 qed
 
 lemma Min_antimono:
@@ -814,7 +814,7 @@
   shows "Min ((\<lambda>x. f x + k) ` S) = Min(f ` S) + k"
 proof -
   have m: "\<And>x y. min x y + k = min (x+k) (y+k)"
-    by(simp add: min_def antisym add_right_mono)
+    by (simp add: min_def order.antisym add_right_mono)
   have "(\<lambda>x. f x + k) ` S = (\<lambda>y. y + k) ` (f ` S)" by auto
   also have "Min \<dots> = Min (f ` S) + k"
     using assms hom_Min_commute [of "\<lambda>y. y+k" "f ` S", OF m, symmetric] by simp
@@ -827,7 +827,7 @@
   shows "Max ((\<lambda>x. f x + k) ` S) = Max(f ` S) + k"
 proof -
   have m: "\<And>x y. max x y + k = max (x+k) (y+k)"
-    by(simp add: max_def antisym add_right_mono)
+    by (simp add: max_def order.antisym add_right_mono)
   have "(\<lambda>x. f x + k) ` S = (\<lambda>y. y + k) ` (f ` S)" by auto
   also have "Max \<dots> = Max (f ` S) + k"
     using assms hom_Max_commute [of "\<lambda>y. y+k" "f ` S", OF m, symmetric] by simp
diff -r 7b59d2945e54 -r 1f1366966296 src/HOL/Library/Complete_Partial_Order2.thy
--- a/src/HOL/Library/Complete_Partial_Order2.thy	Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/Library/Complete_Partial_Order2.thy	Thu Mar 11 07:05:38 2021 +0000
@@ -49,7 +49,7 @@
 
 lemma ccpo_fun: "class.ccpo (fun_lub Sup) (fun_ord (\<le>)) (mk_less (fun_ord (\<le>)))"
   by standard (auto 4 3 simp add: mk_less_def fun_ord_def fun_lub_apply
-    intro: order.trans antisym chain_imageI ccpo_Sup_upper ccpo_Sup_least)
+    intro: order.trans order.antisym chain_imageI ccpo_Sup_upper ccpo_Sup_least)
 
 lemma ccpo_Sup_below_iff: "Complete_Partial_Order.chain (\<le>) Y \<Longrightarrow> Sup Y \<le> x \<longleftrightarrow> (\<forall>y\<in>Y. y \<le> x)"
 by(fast intro: order_trans[OF ccpo_Sup_upper] ccpo_Sup_least)
@@ -58,7 +58,7 @@
   assumes chain: "Complete_Partial_Order.chain (\<le>) A"
   shows "\<Squnion>(A - {\<Squnion>{}}) = \<Squnion>A"
     (is "?lhs = ?rhs")
-proof (rule antisym)
+proof (rule order.antisym)
   show "?lhs \<le> ?rhs"
     by (blast intro: ccpo_Sup_least chain_Diff[OF chain] ccpo_Sup_upper[OF chain])
   show "?rhs \<le> ?lhs"
@@ -117,7 +117,7 @@
 qed(rule x)
 
 lemma diag_Sup: "\<Squnion>((\<lambda>x. \<Squnion>(f x ` Y)) ` Y) = \<Squnion>((\<lambda>x. f x x) ` Y)" (is "?lhs = ?rhs")
-proof(rule antisym)
+proof(rule order.antisym)
   have chain1: "Complete_Partial_Order.chain (\<le>) ((\<lambda>x. \<Squnion>(f x ` Y)) ` Y)"
     using chain by(rule chain_imageI)(rule Sup_mono)
   have chain2: "\<And>y'. y' \<in> Y \<Longrightarrow> Complete_Partial_Order.chain (\<le>) (f y' ` Y)" using chain
@@ -264,7 +264,8 @@
     qed
     finally show "x \<le> ?lhs" .
   qed
-  ultimately show "?lhs = ?rhs" by(rule antisym)
+  ultimately show "?lhs = ?rhs"
+    by (rule order.antisym)
 qed
 
 lemma fixp_mono:
@@ -715,7 +716,7 @@
         thus ?thesis by(rule order_trans)(auto intro: ccpo_Sup_upper[OF chain'] simp add: y ybound)
       qed(auto intro: ccpo_Sup_upper[OF chain'] simp add: x)
     qed
-    hence "\<Squnion>Y = \<Squnion>?Y" by(rule antisym)(blast intro: ccpo_Sup_least[OF chain'] ccpo_Sup_upper[OF chain])
+    hence "\<Squnion>Y = \<Squnion>?Y" by(rule order.antisym)(blast intro: ccpo_Sup_least[OF chain'] ccpo_Sup_upper[OF chain])
     hence "f (\<Squnion>Y) = f (\<Squnion>?Y)" by simp
     also have "f (\<Squnion>?Y) = \<Or>(f ` ?Y)" using chain' by(rule cont)(insert y ybound, auto)
     also have "\<Or>(f ` ?Y) = \<Or>(?g ` Y)"
@@ -732,7 +733,7 @@
       hence "\<Or>(insert bot (f ` ?Y)) \<sqsubseteq> \<Or>(f ` ?Y)" using chain''
         by(auto intro: c.ccpo_Sup_least c.ccpo_Sup_upper[OF chain''']) 
       with _ have "\<dots> = \<Or>(insert bot (f ` ?Y))"
-        by(rule c.antisym)(blast intro: c.ccpo_Sup_least[OF chain'''] c.ccpo_Sup_upper[OF chain''])
+        by(rule c.order.antisym)(blast intro: c.ccpo_Sup_least[OF chain'''] c.ccpo_Sup_upper[OF chain''])
       also have "insert bot (f ` ?Y) = ?g ` Y" using False by auto
       finally show ?thesis .
     qed
@@ -1473,7 +1474,7 @@
   shows "cont lub ord Sup (\<le>) (\<lambda>x. \<Squnion>f x)"
 apply(rule contI)
 apply(simp add: contD[OF assms])
-apply(blast intro: Sup_least Sup_upper order_trans antisym)
+apply(blast intro: Sup_least Sup_upper order_trans order.antisym)
 done
 
 lemma mcont_Sup: "mcont lub ord Union (\<subseteq>) f \<Longrightarrow> mcont lub ord Sup (\<le>) (\<lambda>x. \<Squnion>f x)"
@@ -1496,7 +1497,7 @@
   assume chain: "Complete_Partial_Order.chain ord Y"
     and Y: "Y \<noteq> {}"
   show "\<Squnion>(g (lub Y) ` f (lub Y)) = \<Squnion>((\<lambda>x. \<Squnion>(g x ` f x)) ` Y)" (is "?lhs = ?rhs")
-  proof(rule antisym)
+  proof(rule order.antisym)
     show "?lhs \<le> ?rhs"
     proof(rule Sup_least)
       fix x
@@ -1616,7 +1617,7 @@
     by(rule ab.fixp_induct)(auto simp add: f g step bot)
   also have "ccpo.fixp (prod_lub luba lubb) (rel_prod orda ordb) (map_prod f g) = 
             (ccpo.fixp luba orda f, ccpo.fixp lubb ordb g)" (is "?lhs = (?rhs1, ?rhs2)")
-  proof(rule ab.antisym)
+  proof(rule ab.order.antisym)
     have "ccpo.admissible ?lub ?ord (\<lambda>xy. ?ord xy (?rhs1, ?rhs2))"
       by(rule admissible_leI[OF ccpo_rel_prodI])(auto simp add: prod_lub_def chain_empty intro: a.ccpo_Sup_least b.ccpo_Sup_least)
     thus "?ord ?lhs (?rhs1, ?rhs2)"
diff -r 7b59d2945e54 -r 1f1366966296 src/HOL/Library/Countable_Complete_Lattices.thy
--- a/src/HOL/Library/Countable_Complete_Lattices.thy	Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/Library/Countable_Complete_Lattices.thy	Thu Mar 11 07:05:38 2021 +0000
@@ -64,13 +64,13 @@
   using ccSup_le_iff [of "f ` A"] by simp
 
 lemma ccInf_insert [simp]: "countable A \<Longrightarrow> Inf (insert a A) = inf a (Inf A)"
-  by (force intro: le_infI le_infI1 le_infI2 antisym ccInf_greatest ccInf_lower)
+  by (force intro: le_infI le_infI1 le_infI2 order.antisym ccInf_greatest ccInf_lower)
 
 lemma ccINF_insert [simp]: "countable A \<Longrightarrow> (INF x\<in>insert a A. f x) = inf (f a) (Inf (f ` A))"
   unfolding image_insert by simp
 
 lemma ccSup_insert [simp]: "countable A \<Longrightarrow> Sup (insert a A) = sup a (Sup A)"
-  by (force intro: le_supI le_supI1 le_supI2 antisym ccSup_least ccSup_upper)
+  by (force intro: le_supI le_supI1 le_supI2 order.antisym ccSup_least ccSup_upper)
 
 lemma ccSUP_insert [simp]: "countable A \<Longrightarrow> (SUP x\<in>insert a A. f x) = sup (f a) (Sup (f ` A))"
   unfolding image_insert by simp
@@ -133,24 +133,24 @@
   by (auto intro: ccSup_least ccSup_upper)
 
 lemma ccInf_union_distrib: "countable A \<Longrightarrow> countable B \<Longrightarrow> Inf (A \<union> B) = inf (Inf A) (Inf B)"
-  by (rule antisym) (auto intro: ccInf_greatest ccInf_lower le_infI1 le_infI2)
+  by (rule order.antisym) (auto intro: ccInf_greatest ccInf_lower le_infI1 le_infI2)
 
 lemma ccINF_union:
   "countable A \<Longrightarrow> countable B \<Longrightarrow> (INF i\<in>A \<union> B. M i) = inf (INF i\<in>A. M i) (INF i\<in>B. M i)"
-  by (auto intro!: antisym ccINF_mono intro: le_infI1 le_infI2 ccINF_greatest ccINF_lower)
+  by (auto intro!: order.antisym ccINF_mono intro: le_infI1 le_infI2 ccINF_greatest ccINF_lower)
 
 lemma ccSup_union_distrib: "countable A \<Longrightarrow> countable B \<Longrightarrow> Sup (A \<union> B) = sup (Sup A) (Sup B)"
-  by (rule antisym) (auto intro: ccSup_least ccSup_upper le_supI1 le_supI2)
+  by (rule order.antisym) (auto intro: ccSup_least ccSup_upper le_supI1 le_supI2)
 
 lemma ccSUP_union:
   "countable A \<Longrightarrow> countable B \<Longrightarrow> (SUP i\<in>A \<union> B. M i) = sup (SUP i\<in>A. M i) (SUP i\<in>B. M i)"
-  by (auto intro!: antisym ccSUP_mono intro: le_supI1 le_supI2 ccSUP_least ccSUP_upper)
+  by (auto intro!: order.antisym ccSUP_mono intro: le_supI1 le_supI2 ccSUP_least ccSUP_upper)
 
 lemma ccINF_inf_distrib: "countable A \<Longrightarrow> inf (INF a\<in>A. f a) (INF a\<in>A. g a) = (INF a\<in>A. inf (f a) (g a))"
-  by (rule antisym) (rule ccINF_greatest, auto intro: le_infI1 le_infI2 ccINF_lower ccINF_mono)
+  by (rule order.antisym) (rule ccINF_greatest, auto intro: le_infI1 le_infI2 ccINF_lower ccINF_mono)
 
 lemma ccSUP_sup_distrib: "countable A \<Longrightarrow> sup (SUP a\<in>A. f a) (SUP a\<in>A. g a) = (SUP a\<in>A. sup (f a) (g a))"
-  by (rule antisym[rotated]) (rule ccSUP_least, auto intro: le_supI1 le_supI2 ccSUP_upper ccSUP_mono)
+  by (rule order.antisym[rotated]) (rule ccSUP_least, auto intro: le_supI1 le_supI2 ccSUP_upper ccSUP_mono)
 
 lemma ccINF_const [simp]: "A \<noteq> {} \<Longrightarrow> (INF i \<in> A. f) = f"
   unfolding image_constant_conv by auto
@@ -165,10 +165,10 @@
   by (cases "A = {}") simp_all
 
 lemma ccINF_commute: "countable A \<Longrightarrow> countable B \<Longrightarrow> (INF i\<in>A. INF j\<in>B. f i j) = (INF j\<in>B. INF i\<in>A. f i j)"
-  by (iprover intro: ccINF_lower ccINF_greatest order_trans antisym)
+  by (iprover intro: ccINF_lower ccINF_greatest order_trans order.antisym)
 
 lemma ccSUP_commute: "countable A \<Longrightarrow> countable B \<Longrightarrow> (SUP i\<in>A. SUP j\<in>B. f i j) = (SUP j\<in>B. SUP i\<in>A. f i j)"
-  by (iprover intro: ccSUP_upper ccSUP_least order_trans antisym)
+  by (iprover intro: ccSUP_upper ccSUP_least order_trans order.antisym)
 
 end
 
diff -r 7b59d2945e54 -r 1f1366966296 src/HOL/Library/DAList_Multiset.thy
--- a/src/HOL/Library/DAList_Multiset.thy	Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/Library/DAList_Multiset.thy	Thu Mar 11 07:05:38 2021 +0000
@@ -200,7 +200,7 @@
 
 
 lemma mset_eq [code]: "HOL.equal (m1::'a::equal multiset) m2 \<longleftrightarrow> m1 \<subseteq># m2 \<and> m2 \<subseteq># m1"
-  by (metis equal_multiset_def subset_mset.eq_iff)
+  by (metis equal_multiset_def subset_mset.order_eq_iff)
 
 text \<open>By default the code for \<open><\<close> is \<^prop>\<open>xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> xs = ys\<close>.
 With equality implemented by \<open>\<le>\<close>, this leads to three calls of  \<open>\<le>\<close>.
diff -r 7b59d2945e54 -r 1f1366966296 src/HOL/Library/Lattice_Algebras.thy
--- a/src/HOL/Library/Lattice_Algebras.thy	Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/Library/Lattice_Algebras.thy	Thu Mar 11 07:05:38 2021 +0000
@@ -10,7 +10,7 @@
 begin
 
 lemma add_inf_distrib_left: "a + inf b c = inf (a + b) (a + c)"
-  apply (rule antisym)
+  apply (rule order.antisym)
    apply (simp_all add: le_infI)
   apply (rule add_le_imp_le_left [of "uminus a"])
   apply (simp only: add.assoc [symmetric], simp add: diff_le_eq add.commute)
@@ -30,7 +30,7 @@
 begin
 
 lemma add_sup_distrib_left: "a + sup b c = sup (a + b) (a + c)"
-  apply (rule antisym)
+  apply (rule order.antisym)
    apply (rule add_le_imp_le_left [of "uminus a"])
    apply (simp only: add.assoc [symmetric], simp)
    apply (simp add: le_diff_eq add.commute)
@@ -231,7 +231,7 @@
 qed
 
 lemma double_zero [simp]: "a + a = 0 \<longleftrightarrow> a = 0"
-  using add_nonneg_eq_0_iff eq_iff by auto
+  using add_nonneg_eq_0_iff order.eq_iff by auto
 
 lemma zero_less_double_add_iff_zero_less_single_add [simp]: "0 < a + a \<longleftrightarrow> 0 < a"
   by (meson le_less_trans less_add_same_cancel2 less_le_not_le
diff -r 7b59d2945e54 -r 1f1366966296 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/Library/Multiset.thy	Thu Mar 11 07:05:38 2021 +0000
@@ -520,6 +520,9 @@
   supseteq_mset  (infix ">=#" 50) and
   supset_mset  (infix ">#" 50)
 
+global_interpretation subset_mset: ordering \<open>(\<subseteq>#)\<close> \<open>(\<subset>#)\<close>
+  by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order.trans order.antisym)
+
 interpretation subset_mset: ordered_ab_semigroup_add_imp_le "(+)" "(-)" "(\<subseteq>#)" "(\<subset>#)"
   by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)
     \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
@@ -3113,7 +3116,8 @@
   show "OFCLASS('a multiset, order_class)"
     by standard (auto simp add: less_eq_multiset_def irrefl dest: trans)
 qed
-end \<comment> \<open>FIXME avoid junk stemming from type class interpretation\<close>
+
+end
 
 lemma mset_le_irrefl [elim!]:
   fixes M :: "'a::preorder multiset"
diff -r 7b59d2945e54 -r 1f1366966296 src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy	Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/Library/Sublist.thy	Thu Mar 11 07:05:38 2021 +0000
@@ -18,9 +18,15 @@
 definition strict_prefix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   where "strict_prefix xs ys \<longleftrightarrow> prefix xs ys \<and> xs \<noteq> ys"
 
+global_interpretation prefix_order: ordering prefix strict_prefix
+  by standard (auto simp add: prefix_def strict_prefix_def)
+
 interpretation prefix_order: order prefix strict_prefix
   by standard (auto simp: prefix_def strict_prefix_def)
 
+global_interpretation prefix_bot: ordering_top \<open>\<lambda>xs ys. prefix ys xs\<close> \<open>\<lambda>xs ys. strict_prefix ys xs\<close> \<open>[]\<close>
+  by standard (simp add: prefix_def)
+
 interpretation prefix_bot: order_bot Nil prefix strict_prefix
   by standard (simp add: prefix_def)
 
@@ -74,7 +80,7 @@
 next
   assume "xs = ys @ [y] \<or> prefix xs ys"
   then show "prefix xs (ys @ [y])"
-    by (metis prefix_order.eq_iff prefix_order.order_trans prefixI)
+    by auto (metis append.assoc prefix_def) 
 qed
 
 lemma Cons_prefix_Cons [simp]: "prefix (x # xs) (y # ys) = (x = y \<and> prefix xs ys)"
@@ -90,7 +96,7 @@
   by (induct xs) simp_all
 
 lemma same_prefix_nil [simp]: "prefix (xs @ ys) xs = (ys = [])"
-  by (metis append_Nil2 append_self_conv prefix_order.eq_iff prefixI)
+  by (simp add: prefix_def) 
 
 lemma prefix_prefix [simp]: "prefix xs ys \<Longrightarrow> prefix xs (ys @ zs)"
   unfolding prefix_def by fastforce
@@ -390,10 +396,13 @@
   qed
 qed
 
-lemma Longest_common_prefix_unique: "L \<noteq> {} \<Longrightarrow>
-  \<exists>! ps. (\<forall>xs \<in> L. prefix ps xs) \<and> (\<forall>qs. (\<forall>xs \<in> L. prefix qs xs) \<longrightarrow> size qs \<le> size ps)"
-by(rule ex_ex1I[OF Longest_common_prefix_ex];
-   meson equals0I prefix_length_prefix prefix_order.antisym)
+lemma Longest_common_prefix_unique:
+  \<open>\<exists>! ps. (\<forall>xs \<in> L. prefix ps xs) \<and> (\<forall>qs. (\<forall>xs \<in> L. prefix qs xs) \<longrightarrow> length qs \<le> length ps)\<close>
+  if \<open>L \<noteq> {}\<close>
+  using that apply (rule ex_ex1I[OF Longest_common_prefix_ex])
+  using that apply (auto simp add: prefix_def)
+  apply (metis append_eq_append_conv_if order.antisym)
+  done
 
 lemma Longest_common_prefix_eq:
  "\<lbrakk> L \<noteq> {};  \<forall>xs \<in> L. prefix ps xs;
@@ -516,9 +525,15 @@
 definition strict_suffix :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   where "strict_suffix xs ys \<longleftrightarrow> suffix xs ys \<and> xs \<noteq> ys"
 
+global_interpretation suffix_order: ordering suffix strict_suffix
+  by standard (auto simp: suffix_def strict_suffix_def)
+
 interpretation suffix_order: order suffix strict_suffix
   by standard (auto simp: suffix_def strict_suffix_def)
 
+global_interpretation suffix_bot: ordering_top \<open>\<lambda>xs ys. suffix ys xs\<close> \<open>\<lambda>xs ys. strict_suffix ys xs\<close> \<open>[]\<close>
+  by standard (simp add: suffix_def)
+
 interpretation suffix_bot: order_bot Nil suffix strict_suffix
   by standard (simp add: suffix_def)
 
@@ -1020,28 +1035,34 @@
 
 lemma subseq_append': "subseq (zs @ xs) (zs @ ys) \<longleftrightarrow> subseq xs ys"
   by (induct zs) simp_all
-    
-interpretation subseq_order: order subseq strict_subseq
+
+global_interpretation subseq_order: ordering subseq strict_subseq
 proof
-  fix xs ys :: "'a list"
-  {
-    assume "subseq xs ys" and "subseq ys xs"
-    thus "xs = ys"
-    proof (induct)
-      case list_emb_Nil
-      from list_emb_Nil2 [OF this] show ?case by simp
-    next
-      case list_emb_Cons2
-      thus ?case by simp
-    next
-      case list_emb_Cons
-      hence False using subseq_Cons' by fastforce
-      thus ?case ..
-    qed
-  }
-  thus "strict_subseq xs ys \<longleftrightarrow> (subseq xs ys \<and> \<not>subseq ys xs)"
+  show \<open>subseq xs xs\<close> for xs :: \<open>'a list\<close>
+    using refl by (rule list_emb_refl)
+  show \<open>subseq xs zs\<close> if \<open>subseq xs ys\<close> and \<open>subseq ys zs\<close>
+    for xs ys zs :: \<open>'a list\<close>
+    using trans [OF refl] that by (rule list_emb_trans) simp
+  show \<open>xs = ys\<close> if \<open>subseq xs ys\<close> and \<open>subseq ys xs\<close>
+    for xs ys :: \<open>'a list\<close>
+  using that proof induction
+    case list_emb_Nil
+    from list_emb_Nil2 [OF this] show ?case by simp
+  next
+    case list_emb_Cons2
+    then show ?case by simp
+  next
+    case list_emb_Cons
+    hence False using subseq_Cons' by fastforce
+    then show ?case ..
+  qed
+  show \<open>strict_subseq xs ys \<longleftrightarrow> subseq xs ys \<and> xs \<noteq> ys\<close>
+    for xs ys :: \<open>'a list\<close>
     by (auto simp: strict_subseq_def)
-qed (auto simp: list_emb_refl intro: list_emb_trans)
+qed
+
+interpretation subseq_order: order subseq strict_subseq
+  by (rule ordering_orderI) standard
 
 lemma in_set_subseqs [simp]: "xs \<in> set (subseqs ys) \<longleftrightarrow> subseq xs ys"
 proof
diff -r 7b59d2945e54 -r 1f1366966296 src/HOL/Library/Subseq_Order.thy
--- a/src/HOL/Library/Subseq_Order.thy	Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/Library/Subseq_Order.thy	Thu Mar 11 07:05:38 2021 +0000
@@ -35,9 +35,11 @@
   show "xs \<le> xs"
     by (simp add: less_eq_list_def)
   show "xs = ys" if "xs \<le> ys" and "ys \<le> xs"
-    using that unfolding less_eq_list_def by (rule subseq_order.antisym)
+    using that unfolding less_eq_list_def
+    by (rule subseq_order.antisym)
   show "xs \<le> zs" if "xs \<le> ys" and "ys \<le> zs"
-    using that unfolding less_eq_list_def by (rule subseq_order.order_trans)
+    using that unfolding less_eq_list_def
+    by (rule subseq_order.order_trans)
 qed
 
 lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =
diff -r 7b59d2945e54 -r 1f1366966296 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/List.thy	Thu Mar 11 07:05:38 2021 +0000
@@ -5620,7 +5620,9 @@
   proof(induct rule:list_induct2[OF 1])
     case 1 show ?case by simp
   next
-    case 2 thus ?case by simp (metis Diff_insert_absorb antisym insertE insert_iff)
+    case (2 x xs y ys)
+    then show ?case
+      by (cases \<open>x = y\<close>) (auto simp add: insert_eq_iff)
   qed
 qed
 
@@ -5739,7 +5741,7 @@
 lemma insort_key_left_comm:
   assumes "f x \<noteq> f y"
   shows "insort_key f y (insort_key f x xs) = insort_key f x (insort_key f y xs)"
-by (induct xs) (auto simp add: assms dest: antisym)
+by (induct xs) (auto simp add: assms dest: order.antisym)
 
 lemma insort_left_comm:
   "insort x (insort y xs) = insort y (insort x xs)"
diff -r 7b59d2945e54 -r 1f1366966296 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/Nat.thy	Thu Mar 11 07:05:38 2021 +0000
@@ -1805,7 +1805,7 @@
 text \<open>Every \<open>linordered_nonzero_semiring\<close> has characteristic zero.\<close>
 
 subclass semiring_char_0
-  by standard (auto intro!: injI simp add: eq_iff)
+  by standard (auto intro!: injI simp add: order.eq_iff)
 
 text \<open>Special cases where either operand is zero\<close>
 
diff -r 7b59d2945e54 -r 1f1366966296 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/Orderings.thy	Thu Mar 11 07:05:38 2021 +0000
@@ -282,22 +282,24 @@
 subsection \<open>Partial orders\<close>
 
 class order = preorder +
-  assumes antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
+  assumes order_antisym: "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
 begin
 
 lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
-  by (auto simp add: less_le_not_le intro: antisym)
+  by (auto simp add: less_le_not_le intro: order_antisym)
 
 sublocale order: ordering less_eq less + dual_order: ordering greater_eq greater
 proof -
   interpret ordering less_eq less
-    by standard (auto intro: antisym order_trans simp add: less_le)
+    by standard (auto intro: order_antisym order_trans simp add: less_le)
   show "ordering less_eq less"
     by (fact ordering_axioms)
   then show "ordering greater_eq greater"
     by (rule ordering_dualI)
 qed
 
+print_theorems
+
 text \<open>Reflexivity.\<close>
 
 lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x = y"
@@ -328,11 +330,11 @@
 
 text \<open>Asymmetry.\<close>
 
-lemma eq_iff: "x = y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
+lemma order_eq_iff: "x = y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
   by (fact order.eq_iff)
 
 lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x = y"
-  by (simp add: eq_iff)
+  by (simp add: order.eq_iff)
 
 lemma less_imp_neq: "x < y \<Longrightarrow> x \<noteq> y"
   by (fact order.strict_implies_not_eq)
@@ -344,7 +346,7 @@
   by (simp add: local.less_le)
 
 lemma leD: "y \<le> x \<Longrightarrow> \<not> x < y"
-  by (auto simp: less_le antisym)
+  by (auto simp: less_le order.antisym)
 
 text \<open>Least value operator\<close>
 
@@ -357,7 +359,7 @@
     and "\<And>y. P y \<Longrightarrow> x \<le> y"
   shows "Least P = x"
 unfolding Least_def by (rule the_equality)
-  (blast intro: assms antisym)+
+  (blast intro: assms order.antisym)+
 
 lemma LeastI2_order:
   assumes "P x"
@@ -365,7 +367,7 @@
     and "\<And>x. P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> x \<le> y \<Longrightarrow> Q x"
   shows "Q (Least P)"
 unfolding Least_def by (rule theI2)
-  (blast intro: assms antisym)+
+  (blast intro: assms order.antisym)+
 
 lemma Least_ex1:
   assumes   "\<exists>!x. P x \<and> (\<forall>y. P y \<longrightarrow> x \<le> y)"
@@ -385,12 +387,12 @@
     \<And>x. \<lbrakk> P x; \<forall>y. P y \<longrightarrow> x \<ge> y \<rbrakk> \<Longrightarrow> Q x \<rbrakk>
   \<Longrightarrow> Q (Greatest P)"
 unfolding Greatest_def
-by (rule theI2) (blast intro: antisym)+
+by (rule theI2) (blast intro: order.antisym)+
 
 lemma Greatest_equality:
   "\<lbrakk> P x;  \<And>y. P y \<Longrightarrow> x \<ge> y \<rbrakk> \<Longrightarrow> Greatest P = x"
 unfolding Greatest_def
-by (rule the_equality) (blast intro: antisym)+
+by (rule the_equality) (blast intro: order.antisym)+
 
 end
 
@@ -458,14 +460,14 @@
 
 lemma not_less: "\<not> x < y \<longleftrightarrow> y \<le> x"
   unfolding less_le
-  using linear by (blast intro: antisym)
+  using linear by (blast intro: order.antisym)
 
 lemma not_less_iff_gr_or_eq: "\<not>(x < y) \<longleftrightarrow> (x > y \<or> x = y)"
   by (auto simp add:not_less le_less)
 
 lemma not_le: "\<not> x \<le> y \<longleftrightarrow> y < x"
   unfolding less_le
-  using linear by (blast intro: antisym)
+  using linear by (blast intro: order.antisym)
 
 lemma neq_iff: "x \<noteq> y \<longleftrightarrow> x < y \<or> y < x"
 by (cut_tac x = x and y = y in less_linear, auto)
@@ -474,7 +476,7 @@
 by (simp add: neq_iff) blast
 
 lemma antisym_conv3: "\<not> y < x \<Longrightarrow> \<not> x < y \<longleftrightarrow> x = y"
-by (blast intro: antisym dest: not_less [THEN iffD1])
+by (blast intro: order.antisym dest: not_less [THEN iffD1])
 
 lemma leI: "\<not> x < y \<Longrightarrow> y \<le> x"
 unfolding not_less .
@@ -643,7 +645,7 @@
 
 declare less_imp_le [order add less_imp_le: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
 
-declare antisym [order add eqI: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
+declare order.antisym [order add eqI: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
 
 declare eq_refl [order add eqD1: order "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
 
@@ -688,7 +690,7 @@
 
 declare not_le [THEN iffD1, order add not_leD: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
 
-declare antisym [order add eqI: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
+declare order.antisym [order add eqI: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
 
 declare eq_refl [order add eqD1: linorder "(=) :: 'a => 'a => bool" "(<=)" "(<)"]
 
@@ -1024,7 +1026,7 @@
   order_trans
 
 lemmas (in order) [trans] =
-  antisym
+  order.antisym
 
 lemmas (in ord) [trans] =
   ord_le_eq_trans
@@ -1059,7 +1061,7 @@
   le_less_trans
   less_le_trans
   order_trans
-  antisym
+  order.antisym
   ord_le_eq_trans
   ord_eq_le_trans
   ord_less_eq_trans
@@ -1647,10 +1649,10 @@
 
 instance "fun" :: (type, preorder) preorder proof
 qed (auto simp add: le_fun_def less_fun_def
-  intro: order_trans antisym)
+  intro: order_trans order.antisym)
 
 instance "fun" :: (type, order) order proof
-qed (auto simp add: le_fun_def intro: antisym)
+qed (auto simp add: le_fun_def intro: order.antisym)
 
 instantiation "fun" :: (type, bot) bot
 begin
@@ -1766,6 +1768,9 @@
 
 subsection \<open>Name duplicates\<close>
 
+lemmas antisym = order.antisym
+lemmas eq_iff = order.eq_iff
+
 lemmas order_eq_refl = preorder_class.eq_refl
 lemmas order_less_irrefl = preorder_class.less_irrefl
 lemmas order_less_imp_le = preorder_class.less_imp_le
@@ -1785,8 +1790,7 @@
 lemmas order_less_imp_not_eq2 = order_class.less_imp_not_eq2
 lemmas order_neq_le_trans = order_class.neq_le_trans
 lemmas order_le_neq_trans = order_class.le_neq_trans
-lemmas order_antisym = order_class.antisym
-lemmas order_eq_iff = order_class.eq_iff
+lemmas order_eq_iff = order_class.order.eq_iff
 lemmas order_antisym_conv = order_class.antisym_conv
 
 lemmas linorder_linear = linorder_class.linear
diff -r 7b59d2945e54 -r 1f1366966296 src/HOL/Partial_Function.thy
--- a/src/HOL/Partial_Function.thy	Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/Partial_Function.thy	Thu Mar 11 07:05:38 2021 +0000
@@ -35,13 +35,13 @@
       have "\<Squnion>(insert x A) \<le> \<Squnion>A" using chain
         by(rule ccpo_Sup_least)(auto simp add: True intro: ccpo_Sup_upper[OF chain'])
       hence "\<Squnion>(insert x A) = \<Squnion>A"
-        by(rule antisym)(blast intro: ccpo_Sup_upper[OF chain] ccpo_Sup_least[OF chain'])
+        by(rule order.antisym)(blast intro: ccpo_Sup_upper[OF chain] ccpo_Sup_least[OF chain'])
       with \<open>\<Squnion>A \<in> A\<close> show ?thesis by simp
     next
       case False
       with chainD[OF chain, of x "\<Squnion>A"] \<open>\<Squnion>A \<in> A\<close>
       have "\<Squnion>(insert x A) = x"
-        by(auto intro: antisym ccpo_Sup_least[OF chain] order_trans[OF ccpo_Sup_upper[OF chain']] ccpo_Sup_upper[OF chain])
+        by(auto intro: order.antisym ccpo_Sup_least[OF chain] order_trans[OF ccpo_Sup_upper[OF chain']] ccpo_Sup_upper[OF chain])
       thus ?thesis by simp
     qed
   qed
diff -r 7b59d2945e54 -r 1f1366966296 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/Power.thy	Thu Mar 11 07:05:38 2021 +0000
@@ -480,8 +480,9 @@
   by (induct n) auto
 
 text \<open>Surely we can strengthen this? It holds for \<open>0<a<1\<close> too.\<close>
-lemma power_inject_exp [simp]: "1 < a \<Longrightarrow> a ^ m = a ^ n \<longleftrightarrow> m = n"
-  by (force simp add: order_antisym power_le_imp_le_exp)
+lemma power_inject_exp [simp]:
+  \<open>a ^ m = a ^ n \<longleftrightarrow> m = n\<close> if \<open>1 < a\<close>
+  using that by (force simp add: order_class.order.antisym power_le_imp_le_exp)
 
 text \<open>
   Can relax the first premise to \<^term>\<open>0<a\<close> in the case of the
@@ -609,7 +610,7 @@
 qed
 
 lemma power_inject_base: "a ^ Suc n = b ^ Suc n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a = b"
-  by (blast intro: power_le_imp_le_base antisym eq_refl sym)
+  by (blast intro: power_le_imp_le_base order.antisym eq_refl sym)
 
 lemma power_eq_imp_eq_base: "a ^ n = b ^ n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 < n \<Longrightarrow> a = b"
   by (cases n) (simp_all del: power_Suc, rule power_inject_base)
diff -r 7b59d2945e54 -r 1f1366966296 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/Real_Vector_Spaces.thy	Thu Mar 11 07:05:38 2021 +0000
@@ -553,7 +553,9 @@
 
 lemma scaleR_image_atLeastAtMost: "c > 0 \<Longrightarrow> scaleR c ` {x..y} = {c *\<^sub>R x..c *\<^sub>R y}"
   apply (auto intro!: scaleR_left_mono simp: image_iff Bex_def)
-  by (meson local.eq_iff pos_divideR_le_eq pos_le_divideR_eq)
+  using pos_divideR_le_eq [of c] pos_le_divideR_eq [of c]
+  apply (meson local.order_eq_iff) 
+  done
 
 end
 
diff -r 7b59d2945e54 -r 1f1366966296 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/Set_Interval.thy	Thu Mar 11 07:05:38 2021 +0000
@@ -300,7 +300,7 @@
 
 lemma Icc_eq_Icc[simp]:
   "{l..h} = {l'..h'} = (l=l' \<and> h=h' \<or> \<not> l\<le>h \<and> \<not> l'\<le>h')"
-  by(simp add: order_class.eq_iff)(auto intro: order_trans)
+  by (simp add: order_class.order.eq_iff) (auto intro: order_trans)
 
 lemma atLeastAtMost_singleton_iff[simp]:
   "{a .. b} = {c} \<longleftrightarrow> a = b \<and> b = c"
@@ -477,8 +477,19 @@
   shows "{a ..< b} = {c ..< d} \<longleftrightarrow> a = c \<and> b = d"
   using atLeastLessThan_inj assms by auto
 
-lemma (in linorder) Ioc_inj: "{a <.. b} = {c <.. d} \<longleftrightarrow> (b \<le> a \<and> d \<le> c) \<or> a = c \<and> b = d"
-  by (metis eq_iff greaterThanAtMost_empty_iff2 greaterThanAtMost_iff le_cases not_le)
+lemma (in linorder) Ioc_inj: 
+  \<open>{a <.. b} = {c <.. d} \<longleftrightarrow> (b \<le> a \<and> d \<le> c) \<or> a = c \<and> b = d\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+proof
+  assume ?Q
+  then show ?P
+    by auto
+next
+  assume ?P
+  then have \<open>a < x \<and> x \<le> b \<longleftrightarrow> c < x \<and> x \<le> d\<close> for x
+    by (simp add: set_eq_iff)
+  from this [of a] this [of b] this [of c] this [of d] show ?Q
+    by auto
+qed
 
 lemma (in order) Iio_Int_singleton: "{..<k} \<inter> {x} = (if x < k then {x} else {})"
   by auto
diff -r 7b59d2945e54 -r 1f1366966296 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/Topological_Spaces.thy	Thu Mar 11 07:05:38 2021 +0000
@@ -853,7 +853,7 @@
     and at_within_Icc_at_left:  "at b within {a..b} = at_left b"
   using order_tendstoD(2)[OF tendsto_ident_at assms, of "{a<..}"]
   using order_tendstoD(1)[OF tendsto_ident_at assms, of "{..<b}"]
-  by (auto intro!: order_class.antisym filter_leI
+  by (auto intro!: order_class.order_antisym filter_leI
       simp: eventually_at_filter less_le
       elim: eventually_elim2)
 
diff -r 7b59d2945e54 -r 1f1366966296 src/HOL/ex/Radix_Sort.thy
--- a/src/HOL/ex/Radix_Sort.thy	Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/ex/Radix_Sort.thy	Thu Mar 11 07:05:38 2021 +0000
@@ -70,7 +70,7 @@
     show "sorted_col i (xs2 # xss)" using "3.prems"(3) by simp
     show "\<And>x. sorted_from (i+1) [ys\<leftarrow>xs2 # xss . ys ! i = x]"
       using "3.prems"(4)
-        sorted_antimono_suffix[OF map_mono_suffix[OF filter_mono_suffix[OF suffix_ConsI[OF suffix_order.order.refl]]]]
+        sorted_antimono_suffix[OF map_mono_suffix[OF filter_mono_suffix[OF suffix_ConsI[OF suffix_order.refl]]]]
       by fastforce
   qed
   with * show ?case by (auto)