author paulson Mon Sep 23 14:08:49 2019 +0100 (4 weeks ago ago) changeset 70937 cf7b5020c207 parent 70935 be8e617b6eb3 child 70938 b3b84b71e398
Generalisation of many theorems to a more abstract type class (suggested by Mr Anonymous)
```     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.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
```