Generalisation of many theorems to a more abstract type class (suggested by Mr Anonymous)
authorpaulson <lp15@cam.ac.uk>
Mon Sep 23 14:08:49 2019 +0100 (4 weeks ago ago)
changeset 70937cf7b5020c207
parent 70935 be8e617b6eb3
child 70938 b3b84b71e398
Generalisation of many theorems to a more abstract type class (suggested by Mr Anonymous)
src/HOL/Set_Interval.thy
     1.1 --- a/src/HOL/Set_Interval.thy	Mon Sep 23 08:43:52 2019 +0200
     1.2 +++ b/src/HOL/Set_Interval.thy	Mon Sep 23 14:08:49 2019 +0100
     1.3 @@ -1,7 +1,5 @@
     1.4  (*  Title:      HOL/Set_Interval.thy
     1.5 -    Author:     Tobias Nipkow
     1.6 -    Author:     Clemens Ballarin
     1.7 -    Author:     Jeremy Avigad
     1.8 +    Author:     Tobias Nipkow, Clemens Ballarin, Jeremy Avigad
     1.9  
    1.10  lessThan, greaterThan, atLeast, atMost and two-sided intervals
    1.11  
    1.12 @@ -92,7 +90,7 @@
    1.13      "!!k:: 'a::linorder. -lessThan k = atLeast k"
    1.14    by (auto simp add: lessThan_def atLeast_def)
    1.15  
    1.16 -lemma single_Diff_lessThan [simp]: "!!k:: 'a::order. {k} - lessThan k = {k}"
    1.17 +lemma single_Diff_lessThan [simp]: "!!k:: 'a::preorder. {k} - lessThan k = {k}"
    1.18    by auto
    1.19  
    1.20  lemma (in ord) greaterThan_iff [iff]: "(i \<in> greaterThan k) = (k<i)"
    1.21 @@ -134,11 +132,11 @@
    1.22    by auto
    1.23  
    1.24  lemma atLeast_subset_iff [iff]:
    1.25 -     "(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::order))"
    1.26 +     "(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::preorder))"
    1.27  by (blast intro: order_trans)
    1.28  
    1.29  lemma atLeast_eq_iff [iff]:
    1.30 -     "(atLeast x = atLeast y) = (x = (y::'a::linorder))"
    1.31 +     "(atLeast x = atLeast y) = (x = (y::'a::order))"
    1.32  by (blast intro: order_antisym order_trans)
    1.33  
    1.34  lemma greaterThan_subset_iff [iff]:
    1.35 @@ -149,10 +147,10 @@
    1.36       "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))"
    1.37    by (auto simp: elim!: equalityE)
    1.38  
    1.39 -lemma atMost_subset_iff [iff]: "(atMost x \<subseteq> atMost y) = (x \<le> (y::'a::order))"
    1.40 +lemma atMost_subset_iff [iff]: "(atMost x \<subseteq> atMost y) = (x \<le> (y::'a::preorder))"
    1.41    by (blast intro: order_trans)
    1.42  
    1.43 -lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))"
    1.44 +lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::order))"
    1.45    by (blast intro: order_antisym order_trans)
    1.46  
    1.47  lemma lessThan_subset_iff [iff]:
    1.48 @@ -213,63 +211,85 @@
    1.49  
    1.50  subsubsection\<open>Emptyness, singletons, subset\<close>
    1.51  
    1.52 +context preorder
    1.53 +begin
    1.54 +
    1.55 +lemma atLeastatMost_empty_iff[simp]:
    1.56 +  "{a..b} = {} \<longleftrightarrow> (\<not> a \<le> b)"
    1.57 +  by auto (blast intro: order_trans)
    1.58 +
    1.59 +lemma atLeastatMost_empty_iff2[simp]:
    1.60 +  "{} = {a..b} \<longleftrightarrow> (\<not> a \<le> b)"
    1.61 +  by auto (blast intro: order_trans)
    1.62 +
    1.63 +lemma atLeastLessThan_empty_iff[simp]:
    1.64 +  "{a..<b} = {} \<longleftrightarrow> (\<not> a < b)"
    1.65 +  by auto (blast intro: le_less_trans)
    1.66 +
    1.67 +lemma atLeastLessThan_empty_iff2[simp]:
    1.68 +  "{} = {a..<b} \<longleftrightarrow> (\<not> a < b)"
    1.69 +  by auto (blast intro: le_less_trans)
    1.70 +
    1.71 +lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \<longleftrightarrow> \<not> k < l"
    1.72 +  by auto (blast intro: less_le_trans)
    1.73 +
    1.74 +lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \<longleftrightarrow> \<not> k < l"
    1.75 +  by auto (blast intro: less_le_trans)
    1.76 +
    1.77 +lemma atLeastatMost_subset_iff[simp]:
    1.78 +  "{a..b} \<le> {c..d} \<longleftrightarrow> (\<not> a \<le> b) \<or> c \<le> a \<and> b \<le> d"
    1.79 +  unfolding atLeastAtMost_def atLeast_def atMost_def
    1.80 +  by (blast intro: order_trans)
    1.81 +
    1.82 +lemma atLeastatMost_psubset_iff:
    1.83 +  "{a..b} < {c..d} \<longleftrightarrow>
    1.84 +   ((\<not> a \<le> b) \<or> c \<le> a \<and> b \<le> d \<and> (c < a \<or> b < d)) \<and> c \<le> d"
    1.85 +  by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans)
    1.86 +
    1.87 +lemma Icc_subset_Ici_iff[simp]:
    1.88 +  "{l..h} \<subseteq> {l'..} = (\<not> l\<le>h \<or> l\<ge>l')"
    1.89 +  by(auto simp: subset_eq intro: order_trans)
    1.90 +
    1.91 +lemma Icc_subset_Iic_iff[simp]:
    1.92 +  "{l..h} \<subseteq> {..h'} = (\<not> l\<le>h \<or> h\<le>h')"
    1.93 +  by(auto simp: subset_eq intro: order_trans)
    1.94 +
    1.95 +lemma not_Ici_eq_empty[simp]: "{l..} \<noteq> {}"
    1.96 +  by(auto simp: set_eq_iff)
    1.97 +
    1.98 +lemma not_Iic_eq_empty[simp]: "{..h} \<noteq> {}"
    1.99 +  by(auto simp: set_eq_iff)
   1.100 +
   1.101 +lemmas not_empty_eq_Ici_eq_empty[simp] = not_Ici_eq_empty[symmetric]
   1.102 +lemmas not_empty_eq_Iic_eq_empty[simp] = not_Iic_eq_empty[symmetric]
   1.103 +
   1.104 +end
   1.105 +
   1.106  context order
   1.107  begin
   1.108  
   1.109  lemma atLeastatMost_empty[simp]:
   1.110    "b < a \<Longrightarrow> {a..b} = {}"
   1.111 -by(auto simp: atLeastAtMost_def atLeast_def atMost_def)
   1.112 -
   1.113 -lemma atLeastatMost_empty_iff[simp]:
   1.114 -  "{a..b} = {} \<longleftrightarrow> (\<not> a \<le> b)"
   1.115 -by auto (blast intro: order_trans)
   1.116 -
   1.117 -lemma atLeastatMost_empty_iff2[simp]:
   1.118 -  "{} = {a..b} \<longleftrightarrow> (\<not> a \<le> b)"
   1.119 -by auto (blast intro: order_trans)
   1.120 +  by(auto simp: atLeastAtMost_def atLeast_def atMost_def)
   1.121  
   1.122  lemma atLeastLessThan_empty[simp]:
   1.123 -  "b <= a \<Longrightarrow> {a..<b} = {}"
   1.124 -by(auto simp: atLeastLessThan_def)
   1.125 -
   1.126 -lemma atLeastLessThan_empty_iff[simp]:
   1.127 -  "{a..<b} = {} \<longleftrightarrow> (\<not> a < b)"
   1.128 -by auto (blast intro: le_less_trans)
   1.129 -
   1.130 -lemma atLeastLessThan_empty_iff2[simp]:
   1.131 -  "{} = {a..<b} \<longleftrightarrow> (\<not> a < b)"
   1.132 -by auto (blast intro: le_less_trans)
   1.133 +  "b \<le> a \<Longrightarrow> {a..<b} = {}"
   1.134 +  by(auto simp: atLeastLessThan_def)
   1.135  
   1.136  lemma greaterThanAtMost_empty[simp]: "l \<le> k ==> {k<..l} = {}"
   1.137 -by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)
   1.138 -
   1.139 -lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \<longleftrightarrow> \<not> k < l"
   1.140 -by auto (blast intro: less_le_trans)
   1.141 -
   1.142 -lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \<longleftrightarrow> \<not> k < l"
   1.143 -by auto (blast intro: less_le_trans)
   1.144 +  by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)
   1.145  
   1.146  lemma greaterThanLessThan_empty[simp]:"l \<le> k ==> {k<..<l} = {}"
   1.147 -by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def)
   1.148 +  by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def)
   1.149  
   1.150  lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}"
   1.151 -by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)
   1.152 +  by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)
   1.153  
   1.154  lemma atLeastAtMost_singleton': "a = b \<Longrightarrow> {a .. b} = {a}" by simp
   1.155  
   1.156 -lemma atLeastatMost_subset_iff[simp]:
   1.157 -  "{a..b} \<le> {c..d} \<longleftrightarrow> (\<not> a \<le> b) \<or> c \<le> a \<and> b \<le> d"
   1.158 -unfolding atLeastAtMost_def atLeast_def atMost_def
   1.159 -by (blast intro: order_trans)
   1.160 -
   1.161 -lemma atLeastatMost_psubset_iff:
   1.162 -  "{a..b} < {c..d} \<longleftrightarrow>
   1.163 -   ((\<not> a \<le> b) \<or> c \<le> a \<and> b \<le> d \<and> (c < a \<or> b < d)) \<and> c \<le> d"
   1.164 -by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans)
   1.165 -
   1.166  lemma Icc_eq_Icc[simp]:
   1.167    "{l..h} = {l'..h'} = (l=l' \<and> h=h' \<or> \<not> l\<le>h \<and> \<not> l'\<le>h')"
   1.168 -by(simp add: order_class.eq_iff)(auto intro: order_trans)
   1.169 +  by(simp add: order_class.eq_iff)(auto intro: order_trans)
   1.170  
   1.171  lemma atLeastAtMost_singleton_iff[simp]:
   1.172    "{a .. b} = {c} \<longleftrightarrow> a = b \<and> b = c"
   1.173 @@ -280,23 +300,6 @@
   1.174    with * show "a = b \<and> b = c" by auto
   1.175  qed simp
   1.176  
   1.177 -lemma Icc_subset_Ici_iff[simp]:
   1.178 -  "{l..h} \<subseteq> {l'..} = (\<not> l\<le>h \<or> l\<ge>l')"
   1.179 -by(auto simp: subset_eq intro: order_trans)
   1.180 -
   1.181 -lemma Icc_subset_Iic_iff[simp]:
   1.182 -  "{l..h} \<subseteq> {..h'} = (\<not> l\<le>h \<or> h\<le>h')"
   1.183 -by(auto simp: subset_eq intro: order_trans)
   1.184 -
   1.185 -lemma not_Ici_eq_empty[simp]: "{l..} \<noteq> {}"
   1.186 -by(auto simp: set_eq_iff)
   1.187 -
   1.188 -lemma not_Iic_eq_empty[simp]: "{..h} \<noteq> {}"
   1.189 -by(auto simp: set_eq_iff)
   1.190 -
   1.191 -lemmas not_empty_eq_Ici_eq_empty[simp] = not_Ici_eq_empty[symmetric]
   1.192 -lemmas not_empty_eq_Iic_eq_empty[simp] = not_Iic_eq_empty[symmetric]
   1.193 -
   1.194  end
   1.195  
   1.196  context no_top
   1.197 @@ -811,7 +814,7 @@
   1.198  text \<open>The analogous result is useful on \<^typ>\<open>int\<close>:\<close>
   1.199  (* here, because we don't have an own int section *)
   1.200  lemma atLeastAtMostPlus1_int_conv:
   1.201 -  "m <= 1+n \<Longrightarrow> {m..1+n} = insert (1+n) {m..n::int}"
   1.202 +  "m \<le> 1+n \<Longrightarrow> {m..1+n} = insert (1+n) {m..n::int}"
   1.203    by (auto intro: set_eqI)
   1.204  
   1.205  lemma atLeastLessThan_add_Un: "i \<le> j \<Longrightarrow> {i..<j+k} = {i..<j} \<union> {j..<j+k::nat}"
   1.206 @@ -1224,7 +1227,7 @@
   1.207    next
   1.208      case (insert b A)
   1.209      hence *: "b \<notin> A" by auto
   1.210 -    with insert have "A <= {k..<k + card A}" and "b = k + card A"
   1.211 +    with insert have "A \<le> {k..<k + card A}" and "b = k + card A"
   1.212        by fastforce+
   1.213      with insert * show ?case by auto
   1.214    qed
   1.215 @@ -2483,6 +2486,6 @@
   1.216      by (simp add: prod.eq_fold fold_atLeastAtMost_nat o_def)
   1.217  qed
   1.218  
   1.219 -(* TODO: Add support for more kinds of intervals here *)
   1.220 +(* TODO: Add support for folding over more kinds of intervals here *)
   1.221  
   1.222  end