--- 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 ***
--- 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)
--- 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"
--- 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
--- 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:
--- 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>
--- 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)
--- 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)"
--- 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
--- 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"
--- 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
--- 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)"
--- 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
--- 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>.
--- 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
--- 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"
--- 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
--- 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] =
--- 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)"
--- 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>
--- 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
--- 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
--- 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)
--- 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
--- 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
--- 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)
--- 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)