# HG changeset patch
# User nipkow
# Date 1569334234 -7200
# Node ID 401cd34711b5124289102abddccd009ba5946975
# Parent  5d06b7bb9d229af3534deb61fed2734e9b4a3a92# Parent  fd9614c98dd677626454823cea1510d053cbb1e9
merged

diff -r fd9614c98dd6 -r 401cd34711b5 src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy
--- a/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy	Tue Sep 24 16:10:27 2019 +0200
+++ b/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy	Tue Sep 24 16:10:34 2019 +0200
@@ -198,7 +198,7 @@
   apply (rule ccontr)
   apply auto
   apply (drule injf_max_order_preserving2)
-  apply (metis linorder_antisym_conv3 order_less_le)
+  apply (metis antisym_conv3 order_less_le)
   done
 
 lemma infinite_set_has_order_preserving_inj:
diff -r fd9614c98dd6 -r 401cd34711b5 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Tue Sep 24 16:10:27 2019 +0200
+++ b/src/HOL/Orderings.thy	Tue Sep 24 16:10:34 2019 +0200
@@ -278,6 +278,14 @@
 lemma less_imp_neq: "x < y \<Longrightarrow> x \<noteq> y"
 by (fact order.strict_implies_not_eq)
 
+lemma antisym_conv1: "\<not> x < y \<Longrightarrow> x \<le> y \<longleftrightarrow> x = y"
+  by (simp add: local.le_less)
+
+lemma antisym_conv2: "x \<le> y \<Longrightarrow> \<not> x < y \<longleftrightarrow> x = y"
+  by (simp add: local.less_le)
+
+lemma leD: "y \<le> x \<Longrightarrow> \<not> x < y"
+  by (auto simp: less_le antisym)
 
 text \<open>Least value operator\<close>
 
@@ -390,20 +398,15 @@
   by (cases rule: le_cases[of a b]) blast+
 
 lemma not_less: "\<not> x < y \<longleftrightarrow> y \<le> x"
-apply (simp add: less_le)
-using linear apply (blast intro: antisym)
-done
+  unfolding less_le
+  using linear by (blast intro: antisym)
 
-lemma not_less_iff_gr_or_eq:
- "\<not>(x < y) \<longleftrightarrow> (x > y \<or> x = y)"
-apply(simp add:not_less le_less)
-apply blast
-done
+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"
-apply (simp add: less_le)
-using linear apply (blast intro: antisym)
-done
+  unfolding less_le
+  using linear by (blast intro: 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)
@@ -411,21 +414,12 @@
 lemma neqE: "x \<noteq> y \<Longrightarrow> (x < y \<Longrightarrow> R) \<Longrightarrow> (y < x \<Longrightarrow> R) \<Longrightarrow> R"
 by (simp add: neq_iff) blast
 
-lemma antisym_conv1: "\<not> x < y \<Longrightarrow> x \<le> y \<longleftrightarrow> x = y"
-by (blast intro: antisym dest: not_less [THEN iffD1])
-
-lemma antisym_conv2: "x \<le> y \<Longrightarrow> \<not> x < y \<longleftrightarrow> x = y"
-by (blast intro: antisym dest: not_less [THEN iffD1])
-
 lemma antisym_conv3: "\<not> y < x \<Longrightarrow> \<not> x < y \<longleftrightarrow> x = y"
 by (blast intro: antisym dest: not_less [THEN iffD1])
 
 lemma leI: "\<not> x < y \<Longrightarrow> y \<le> x"
 unfolding not_less .
 
-lemma leD: "y \<le> x \<Longrightarrow> \<not> x < y"
-unfolding not_less .
-
 lemma not_le_imp_less: "\<not> y \<le> x \<Longrightarrow> x < y"
 unfolding not_le .
 
@@ -688,7 +682,7 @@
             let val t = HOLogic.mk_Trueprop(HOLogic.Not $ (less $ r $ s)) in
               (case find_first (prp t) prems of
                 NONE => NONE
-              | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv1})))
+              | SOME thm => SOME(mk_meta_eq(thm RS @{thm antisym_conv1})))
              end
          | SOME thm => SOME (mk_meta_eq (thm RS @{thm order_class.antisym_conv})))
       end handle THM _ => NONE)
@@ -709,7 +703,7 @@
                 NONE => NONE
               | SOME thm => SOME (mk_meta_eq(thm RS @{thm linorder_class.antisym_conv3})))
             end
-        | SOME thm => SOME (mk_meta_eq (thm RS @{thm linorder_class.antisym_conv2})))
+        | SOME thm => SOME (mk_meta_eq (thm RS @{thm antisym_conv2})))
       end handle THM _ => NONE)
   | _ => NONE);
 
@@ -1744,8 +1738,5 @@
 lemmas linorder_not_le = linorder_class.not_le
 lemmas linorder_neq_iff = linorder_class.neq_iff
 lemmas linorder_neqE = linorder_class.neqE
-lemmas linorder_antisym_conv1 = linorder_class.antisym_conv1
-lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
-lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
 
 end
diff -r fd9614c98dd6 -r 401cd34711b5 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Tue Sep 24 16:10:27 2019 +0200
+++ b/src/HOL/Set_Interval.thy	Tue Sep 24 16:10:34 2019 +0200
@@ -246,6 +246,10 @@
    ((\<not> a \<le> b) \<or> c \<le> a \<and> b \<le> d \<and> (c < a \<or> b < d)) \<and> c \<le> d"
   by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans)
 
+lemma atLeastAtMost_subseteq_atLeastLessThan_iff:
+  "{a..b} \<subseteq> {c ..< d} \<longleftrightarrow> (a \<le> b \<longrightarrow> c \<le> a \<and> b < d)" 
+  by auto (blast intro: local.order_trans local.le_less_trans elim: )+
+
 lemma Icc_subset_Ici_iff[simp]:
   "{l..h} \<subseteq> {l'..} = (\<not> l\<le>h \<or> l\<ge>l')"
   by(auto simp: subset_eq intro: order_trans)
@@ -408,11 +412,6 @@
   using dense[of "a" "min c b"] dense[of "max a d" "b"]
   by (force simp: subset_eq Ball_def not_less[symmetric])
 
-lemma atLeastAtMost_subseteq_atLeastLessThan_iff:
-  "{a .. b} \<subseteq> { c ..< d } \<longleftrightarrow> (a \<le> b \<longrightarrow> c \<le> a \<and> b < d)"
-  using dense[of "max a d" "b"]
-  by (force simp: subset_eq Ball_def not_less[symmetric])
-
 lemma greaterThanLessThan_subseteq_greaterThanLessThan:
   "{a <..< b} \<subseteq> {c <..< d} \<longleftrightarrow> (a < b \<longrightarrow> a \<ge> c \<and> b \<le> d)"
   using dense[of "a" "min c b"] dense[of "max a d" "b"]
@@ -463,7 +462,7 @@
   fixes a b c d :: "'a::linorder"
   assumes eq: "{a ..< b} = {c ..< d}" and "a < b" "c < d"
   shows "a = c" "b = d"
-using assms by (metis atLeastLessThan_subset_iff eq less_le_not_le linorder_antisym_conv2 subset_refl)+
+using assms by (metis atLeastLessThan_subset_iff eq less_le_not_le antisym_conv2 subset_refl)+
 
 lemma atLeastLessThan_eq_iff:
   fixes a b c d :: "'a::linorder"
diff -r fd9614c98dd6 -r 401cd34711b5 src/HOL/Tools/SMT/smt_replay.ML
--- a/src/HOL/Tools/SMT/smt_replay.ML	Tue Sep 24 16:10:27 2019 +0200
+++ b/src/HOL/Tools/SMT/smt_replay.ML	Tue Sep 24 16:10:34 2019 +0200
@@ -99,8 +99,8 @@
 
 local
   val antisym_le1 = mk_meta_eq @{thm order_class.antisym_conv}
-  val antisym_le2 = mk_meta_eq @{thm linorder_class.antisym_conv2}
-  val antisym_less1 = mk_meta_eq @{thm linorder_class.antisym_conv1}
+  val antisym_le2 = mk_meta_eq @{thm order_class.antisym_conv2}
+  val antisym_less1 = mk_meta_eq @{thm order_class.antisym_conv1}
   val antisym_less2 = mk_meta_eq @{thm linorder_class.antisym_conv3}
 
   fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm
diff -r fd9614c98dd6 -r 401cd34711b5 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Tue Sep 24 16:10:27 2019 +0200
+++ b/src/HOL/Topological_Spaces.thy	Tue Sep 24 16:10:34 2019 +0200
@@ -286,7 +286,7 @@
     by (simp add: closed_Int)
 qed
 
-lemma (in linorder) less_separate:
+lemma (in order) less_separate:
   assumes "x < y"
   shows "\<exists>a b. x \<in> {..< a} \<and> y \<in> {b <..} \<and> {..< a} \<inter> {b <..} = {}"
 proof (cases "\<exists>z. x < z \<and> z < y")
@@ -3673,11 +3673,7 @@
   have "(\<lambda>(x,y). d y x) = (\<lambda>(x,y). d x y) \<circ> prod.swap"
     by force
   then show ?thesis
-    apply (rule ssubst)
-    apply (rule continuous_on_compose)
-     apply (force intro: continuous_on_subset [OF continuous_on_swap])
-    apply (force intro: continuous_on_subset [OF assms])
-    done
+    by (metis assms continuous_on_compose continuous_on_swap product_swap)
 qed
 
 lemma isCont_fst [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a"
diff -r fd9614c98dd6 -r 401cd34711b5 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Tue Sep 24 16:10:27 2019 +0200
+++ b/src/HOL/Transitive_Closure.thy	Tue Sep 24 16:10:34 2019 +0200
@@ -1177,7 +1177,7 @@
 lemma acyclicI: "\<forall>x. (x, x) \<notin> r\<^sup>+ \<Longrightarrow> acyclic r"
   by (simp add: acyclic_def)
 
-lemma (in order) acyclicI_order:
+lemma (in preorder) acyclicI_order:
   assumes *: "\<And>a b. (a, b) \<in> r \<Longrightarrow> f b < f a"
   shows "acyclic r"
 proof -
diff -r fd9614c98dd6 -r 401cd34711b5 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Tue Sep 24 16:10:27 2019 +0200
+++ b/src/HOL/Word/Word.thy	Tue Sep 24 16:10:34 2019 +0200
@@ -640,7 +640,7 @@
   by (metis bintr_uint bintrunc_mod2p int_mod_lem zless2p)
 
 lemma uint_le_0_iff [simp]: "uint x \<le> 0 \<longleftrightarrow> uint x = 0"
-  by (fact uint_ge_0 [THEN leD, THEN linorder_antisym_conv1])
+  by (fact uint_ge_0 [THEN leD, THEN antisym_conv1])
 
 lemma uint_nat: "uint w = int (unat w)"
   by (auto simp: unat_def)
@@ -1682,7 +1682,7 @@
 subsection \<open>Arithmetic type class instantiations\<close>
 
 lemmas word_le_0_iff [simp] =
-  word_zero_le [THEN leD, THEN linorder_antisym_conv1]
+  word_zero_le [THEN leD, THEN antisym_conv1]
 
 lemma word_of_int_nat: "0 \<le> x \<Longrightarrow> word_of_int x = of_nat (nat x)"
   by (simp add: word_of_int)