More type class generalisations. Note that linorder_antisym_conv1 and linorder_antisym_conv2 no longer exist.
authorpaulson <lp15@cam.ac.uk>
Tue Sep 24 12:56:10 2019 +0100 (4 weeks ago ago)
changeset 709405d06b7bb9d22
parent 70938 b3b84b71e398
child 70941 401cd34711b5
child 70942 07673e7cb5e6
More type class generalisations. Note that linorder_antisym_conv1 and linorder_antisym_conv2 no longer exist.
src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy
src/HOL/Orderings.thy
src/HOL/Set_Interval.thy
src/HOL/Tools/SMT/smt_replay.ML
src/HOL/Topological_Spaces.thy
src/HOL/Transitive_Closure.thy
src/HOL/Word/Word.thy
     1.1 --- a/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy	Mon Sep 23 17:15:44 2019 +0200
     1.2 +++ b/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy	Tue Sep 24 12:56:10 2019 +0100
     1.3 @@ -198,7 +198,7 @@
     1.4    apply (rule ccontr)
     1.5    apply auto
     1.6    apply (drule injf_max_order_preserving2)
     1.7 -  apply (metis linorder_antisym_conv3 order_less_le)
     1.8 +  apply (metis antisym_conv3 order_less_le)
     1.9    done
    1.10  
    1.11  lemma infinite_set_has_order_preserving_inj:
     2.1 --- a/src/HOL/Orderings.thy	Mon Sep 23 17:15:44 2019 +0200
     2.2 +++ b/src/HOL/Orderings.thy	Tue Sep 24 12:56:10 2019 +0100
     2.3 @@ -278,6 +278,14 @@
     2.4  lemma less_imp_neq: "x < y \<Longrightarrow> x \<noteq> y"
     2.5  by (fact order.strict_implies_not_eq)
     2.6  
     2.7 +lemma antisym_conv1: "\<not> x < y \<Longrightarrow> x \<le> y \<longleftrightarrow> x = y"
     2.8 +  by (simp add: local.le_less)
     2.9 +
    2.10 +lemma antisym_conv2: "x \<le> y \<Longrightarrow> \<not> x < y \<longleftrightarrow> x = y"
    2.11 +  by (simp add: local.less_le)
    2.12 +
    2.13 +lemma leD: "y \<le> x \<Longrightarrow> \<not> x < y"
    2.14 +  by (auto simp: less_le antisym)
    2.15  
    2.16  text \<open>Least value operator\<close>
    2.17  
    2.18 @@ -390,20 +398,15 @@
    2.19    by (cases rule: le_cases[of a b]) blast+
    2.20  
    2.21  lemma not_less: "\<not> x < y \<longleftrightarrow> y \<le> x"
    2.22 -apply (simp add: less_le)
    2.23 -using linear apply (blast intro: antisym)
    2.24 -done
    2.25 +  unfolding less_le
    2.26 +  using linear by (blast intro: antisym)
    2.27  
    2.28 -lemma not_less_iff_gr_or_eq:
    2.29 - "\<not>(x < y) \<longleftrightarrow> (x > y \<or> x = y)"
    2.30 -apply(simp add:not_less le_less)
    2.31 -apply blast
    2.32 -done
    2.33 +lemma not_less_iff_gr_or_eq: "\<not>(x < y) \<longleftrightarrow> (x > y \<or> x = y)"
    2.34 +  by (auto simp add:not_less le_less)
    2.35  
    2.36  lemma not_le: "\<not> x \<le> y \<longleftrightarrow> y < x"
    2.37 -apply (simp add: less_le)
    2.38 -using linear apply (blast intro: antisym)
    2.39 -done
    2.40 +  unfolding less_le
    2.41 +  using linear by (blast intro: antisym)
    2.42  
    2.43  lemma neq_iff: "x \<noteq> y \<longleftrightarrow> x < y \<or> y < x"
    2.44  by (cut_tac x = x and y = y in less_linear, auto)
    2.45 @@ -411,21 +414,12 @@
    2.46  lemma neqE: "x \<noteq> y \<Longrightarrow> (x < y \<Longrightarrow> R) \<Longrightarrow> (y < x \<Longrightarrow> R) \<Longrightarrow> R"
    2.47  by (simp add: neq_iff) blast
    2.48  
    2.49 -lemma antisym_conv1: "\<not> x < y \<Longrightarrow> x \<le> y \<longleftrightarrow> x = y"
    2.50 -by (blast intro: antisym dest: not_less [THEN iffD1])
    2.51 -
    2.52 -lemma antisym_conv2: "x \<le> y \<Longrightarrow> \<not> x < y \<longleftrightarrow> x = y"
    2.53 -by (blast intro: antisym dest: not_less [THEN iffD1])
    2.54 -
    2.55  lemma antisym_conv3: "\<not> y < x \<Longrightarrow> \<not> x < y \<longleftrightarrow> x = y"
    2.56  by (blast intro: antisym dest: not_less [THEN iffD1])
    2.57  
    2.58  lemma leI: "\<not> x < y \<Longrightarrow> y \<le> x"
    2.59  unfolding not_less .
    2.60  
    2.61 -lemma leD: "y \<le> x \<Longrightarrow> \<not> x < y"
    2.62 -unfolding not_less .
    2.63 -
    2.64  lemma not_le_imp_less: "\<not> y \<le> x \<Longrightarrow> x < y"
    2.65  unfolding not_le .
    2.66  
    2.67 @@ -688,7 +682,7 @@
    2.68              let val t = HOLogic.mk_Trueprop(HOLogic.Not $ (less $ r $ s)) in
    2.69                (case find_first (prp t) prems of
    2.70                  NONE => NONE
    2.71 -              | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_class.antisym_conv1})))
    2.72 +              | SOME thm => SOME(mk_meta_eq(thm RS @{thm antisym_conv1})))
    2.73               end
    2.74           | SOME thm => SOME (mk_meta_eq (thm RS @{thm order_class.antisym_conv})))
    2.75        end handle THM _ => NONE)
    2.76 @@ -709,7 +703,7 @@
    2.77                  NONE => NONE
    2.78                | SOME thm => SOME (mk_meta_eq(thm RS @{thm linorder_class.antisym_conv3})))
    2.79              end
    2.80 -        | SOME thm => SOME (mk_meta_eq (thm RS @{thm linorder_class.antisym_conv2})))
    2.81 +        | SOME thm => SOME (mk_meta_eq (thm RS @{thm antisym_conv2})))
    2.82        end handle THM _ => NONE)
    2.83    | _ => NONE);
    2.84  
    2.85 @@ -1744,8 +1738,5 @@
    2.86  lemmas linorder_not_le = linorder_class.not_le
    2.87  lemmas linorder_neq_iff = linorder_class.neq_iff
    2.88  lemmas linorder_neqE = linorder_class.neqE
    2.89 -lemmas linorder_antisym_conv1 = linorder_class.antisym_conv1
    2.90 -lemmas linorder_antisym_conv2 = linorder_class.antisym_conv2
    2.91 -lemmas linorder_antisym_conv3 = linorder_class.antisym_conv3
    2.92  
    2.93  end
     3.1 --- a/src/HOL/Set_Interval.thy	Mon Sep 23 17:15:44 2019 +0200
     3.2 +++ b/src/HOL/Set_Interval.thy	Tue Sep 24 12:56:10 2019 +0100
     3.3 @@ -246,6 +246,10 @@
     3.4     ((\<not> a \<le> b) \<or> c \<le> a \<and> b \<le> d \<and> (c < a \<or> b < d)) \<and> c \<le> d"
     3.5    by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans)
     3.6  
     3.7 +lemma atLeastAtMost_subseteq_atLeastLessThan_iff:
     3.8 +  "{a..b} \<subseteq> {c ..< d} \<longleftrightarrow> (a \<le> b \<longrightarrow> c \<le> a \<and> b < d)" 
     3.9 +  by auto (blast intro: local.order_trans local.le_less_trans elim: )+
    3.10 +
    3.11  lemma Icc_subset_Ici_iff[simp]:
    3.12    "{l..h} \<subseteq> {l'..} = (\<not> l\<le>h \<or> l\<ge>l')"
    3.13    by(auto simp: subset_eq intro: order_trans)
    3.14 @@ -408,11 +412,6 @@
    3.15    using dense[of "a" "min c b"] dense[of "max a d" "b"]
    3.16    by (force simp: subset_eq Ball_def not_less[symmetric])
    3.17  
    3.18 -lemma atLeastAtMost_subseteq_atLeastLessThan_iff:
    3.19 -  "{a .. b} \<subseteq> { c ..< d } \<longleftrightarrow> (a \<le> b \<longrightarrow> c \<le> a \<and> b < d)"
    3.20 -  using dense[of "max a d" "b"]
    3.21 -  by (force simp: subset_eq Ball_def not_less[symmetric])
    3.22 -
    3.23  lemma greaterThanLessThan_subseteq_greaterThanLessThan:
    3.24    "{a <..< b} \<subseteq> {c <..< d} \<longleftrightarrow> (a < b \<longrightarrow> a \<ge> c \<and> b \<le> d)"
    3.25    using dense[of "a" "min c b"] dense[of "max a d" "b"]
    3.26 @@ -463,7 +462,7 @@
    3.27    fixes a b c d :: "'a::linorder"
    3.28    assumes eq: "{a ..< b} = {c ..< d}" and "a < b" "c < d"
    3.29    shows "a = c" "b = d"
    3.30 -using assms by (metis atLeastLessThan_subset_iff eq less_le_not_le linorder_antisym_conv2 subset_refl)+
    3.31 +using assms by (metis atLeastLessThan_subset_iff eq less_le_not_le antisym_conv2 subset_refl)+
    3.32  
    3.33  lemma atLeastLessThan_eq_iff:
    3.34    fixes a b c d :: "'a::linorder"
     4.1 --- a/src/HOL/Tools/SMT/smt_replay.ML	Mon Sep 23 17:15:44 2019 +0200
     4.2 +++ b/src/HOL/Tools/SMT/smt_replay.ML	Tue Sep 24 12:56:10 2019 +0100
     4.3 @@ -99,8 +99,8 @@
     4.4  
     4.5  local
     4.6    val antisym_le1 = mk_meta_eq @{thm order_class.antisym_conv}
     4.7 -  val antisym_le2 = mk_meta_eq @{thm linorder_class.antisym_conv2}
     4.8 -  val antisym_less1 = mk_meta_eq @{thm linorder_class.antisym_conv1}
     4.9 +  val antisym_le2 = mk_meta_eq @{thm order_class.antisym_conv2}
    4.10 +  val antisym_less1 = mk_meta_eq @{thm order_class.antisym_conv1}
    4.11    val antisym_less2 = mk_meta_eq @{thm linorder_class.antisym_conv3}
    4.12  
    4.13    fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm
     5.1 --- a/src/HOL/Topological_Spaces.thy	Mon Sep 23 17:15:44 2019 +0200
     5.2 +++ b/src/HOL/Topological_Spaces.thy	Tue Sep 24 12:56:10 2019 +0100
     5.3 @@ -286,7 +286,7 @@
     5.4      by (simp add: closed_Int)
     5.5  qed
     5.6  
     5.7 -lemma (in linorder) less_separate:
     5.8 +lemma (in order) less_separate:
     5.9    assumes "x < y"
    5.10    shows "\<exists>a b. x \<in> {..< a} \<and> y \<in> {b <..} \<and> {..< a} \<inter> {b <..} = {}"
    5.11  proof (cases "\<exists>z. x < z \<and> z < y")
    5.12 @@ -3673,11 +3673,7 @@
    5.13    have "(\<lambda>(x,y). d y x) = (\<lambda>(x,y). d x y) \<circ> prod.swap"
    5.14      by force
    5.15    then show ?thesis
    5.16 -    apply (rule ssubst)
    5.17 -    apply (rule continuous_on_compose)
    5.18 -     apply (force intro: continuous_on_subset [OF continuous_on_swap])
    5.19 -    apply (force intro: continuous_on_subset [OF assms])
    5.20 -    done
    5.21 +    by (metis assms continuous_on_compose continuous_on_swap product_swap)
    5.22  qed
    5.23  
    5.24  lemma isCont_fst [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a"
     6.1 --- a/src/HOL/Transitive_Closure.thy	Mon Sep 23 17:15:44 2019 +0200
     6.2 +++ b/src/HOL/Transitive_Closure.thy	Tue Sep 24 12:56:10 2019 +0100
     6.3 @@ -1177,7 +1177,7 @@
     6.4  lemma acyclicI: "\<forall>x. (x, x) \<notin> r\<^sup>+ \<Longrightarrow> acyclic r"
     6.5    by (simp add: acyclic_def)
     6.6  
     6.7 -lemma (in order) acyclicI_order:
     6.8 +lemma (in preorder) acyclicI_order:
     6.9    assumes *: "\<And>a b. (a, b) \<in> r \<Longrightarrow> f b < f a"
    6.10    shows "acyclic r"
    6.11  proof -
     7.1 --- a/src/HOL/Word/Word.thy	Mon Sep 23 17:15:44 2019 +0200
     7.2 +++ b/src/HOL/Word/Word.thy	Tue Sep 24 12:56:10 2019 +0100
     7.3 @@ -640,7 +640,7 @@
     7.4    by (metis bintr_uint bintrunc_mod2p int_mod_lem zless2p)
     7.5  
     7.6  lemma uint_le_0_iff [simp]: "uint x \<le> 0 \<longleftrightarrow> uint x = 0"
     7.7 -  by (fact uint_ge_0 [THEN leD, THEN linorder_antisym_conv1])
     7.8 +  by (fact uint_ge_0 [THEN leD, THEN antisym_conv1])
     7.9  
    7.10  lemma uint_nat: "uint w = int (unat w)"
    7.11    by (auto simp: unat_def)
    7.12 @@ -1682,7 +1682,7 @@
    7.13  subsection \<open>Arithmetic type class instantiations\<close>
    7.14  
    7.15  lemmas word_le_0_iff [simp] =
    7.16 -  word_zero_le [THEN leD, THEN linorder_antisym_conv1]
    7.17 +  word_zero_le [THEN leD, THEN antisym_conv1]
    7.18  
    7.19  lemma word_of_int_nat: "0 \<le> x \<Longrightarrow> word_of_int x = of_nat (nat x)"
    7.20    by (simp add: word_of_int)