# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1569244129 -3600
# Node ID cf7b5020c207bbba7bfbfe8b8fb2e5a7dd3c0644
# Parent  be8e617b6eb34498cf6cc9bed317fdd7c766c80f
Generalisation of many theorems to a more abstract type class (suggested by Mr Anonymous)

diff -r be8e617b6eb3 -r cf7b5020c207 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Mon Sep 23 08:43:52 2019 +0200
+++ b/src/HOL/Set_Interval.thy	Mon Sep 23 14:08:49 2019 +0100
@@ -1,7 +1,5 @@
 (*  Title:      HOL/Set_Interval.thy
-    Author:     Tobias Nipkow
-    Author:     Clemens Ballarin
-    Author:     Jeremy Avigad
+    Author:     Tobias Nipkow, Clemens Ballarin, Jeremy Avigad
 
 lessThan, greaterThan, atLeast, atMost and two-sided intervals
 
@@ -92,7 +90,7 @@
     "!!k:: 'a::linorder. -lessThan k = atLeast k"
   by (auto simp add: lessThan_def atLeast_def)
 
-lemma single_Diff_lessThan [simp]: "!!k:: 'a::order. {k} - lessThan k = {k}"
+lemma single_Diff_lessThan [simp]: "!!k:: 'a::preorder. {k} - lessThan k = {k}"
   by auto
 
 lemma (in ord) greaterThan_iff [iff]: "(i \<in> greaterThan k) = (k<i)"
@@ -134,11 +132,11 @@
   by auto
 
 lemma atLeast_subset_iff [iff]:
-     "(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::order))"
+     "(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::preorder))"
 by (blast intro: order_trans)
 
 lemma atLeast_eq_iff [iff]:
-     "(atLeast x = atLeast y) = (x = (y::'a::linorder))"
+     "(atLeast x = atLeast y) = (x = (y::'a::order))"
 by (blast intro: order_antisym order_trans)
 
 lemma greaterThan_subset_iff [iff]:
@@ -149,10 +147,10 @@
      "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))"
   by (auto simp: elim!: equalityE)
 
-lemma atMost_subset_iff [iff]: "(atMost x \<subseteq> atMost y) = (x \<le> (y::'a::order))"
+lemma atMost_subset_iff [iff]: "(atMost x \<subseteq> atMost y) = (x \<le> (y::'a::preorder))"
   by (blast intro: order_trans)
 
-lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))"
+lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::order))"
   by (blast intro: order_antisym order_trans)
 
 lemma lessThan_subset_iff [iff]:
@@ -213,63 +211,85 @@
 
 subsubsection\<open>Emptyness, singletons, subset\<close>
 
+context preorder
+begin
+
+lemma atLeastatMost_empty_iff[simp]:
+  "{a..b} = {} \<longleftrightarrow> (\<not> a \<le> b)"
+  by auto (blast intro: order_trans)
+
+lemma atLeastatMost_empty_iff2[simp]:
+  "{} = {a..b} \<longleftrightarrow> (\<not> a \<le> b)"
+  by auto (blast intro: order_trans)
+
+lemma atLeastLessThan_empty_iff[simp]:
+  "{a..<b} = {} \<longleftrightarrow> (\<not> a < b)"
+  by auto (blast intro: le_less_trans)
+
+lemma atLeastLessThan_empty_iff2[simp]:
+  "{} = {a..<b} \<longleftrightarrow> (\<not> a < b)"
+  by auto (blast intro: le_less_trans)
+
+lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \<longleftrightarrow> \<not> k < l"
+  by auto (blast intro: less_le_trans)
+
+lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \<longleftrightarrow> \<not> k < l"
+  by auto (blast intro: less_le_trans)
+
+lemma atLeastatMost_subset_iff[simp]:
+  "{a..b} \<le> {c..d} \<longleftrightarrow> (\<not> a \<le> b) \<or> c \<le> a \<and> b \<le> d"
+  unfolding atLeastAtMost_def atLeast_def atMost_def
+  by (blast intro: order_trans)
+
+lemma atLeastatMost_psubset_iff:
+  "{a..b} < {c..d} \<longleftrightarrow>
+   ((\<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 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)
+
+lemma Icc_subset_Iic_iff[simp]:
+  "{l..h} \<subseteq> {..h'} = (\<not> l\<le>h \<or> h\<le>h')"
+  by(auto simp: subset_eq intro: order_trans)
+
+lemma not_Ici_eq_empty[simp]: "{l..} \<noteq> {}"
+  by(auto simp: set_eq_iff)
+
+lemma not_Iic_eq_empty[simp]: "{..h} \<noteq> {}"
+  by(auto simp: set_eq_iff)
+
+lemmas not_empty_eq_Ici_eq_empty[simp] = not_Ici_eq_empty[symmetric]
+lemmas not_empty_eq_Iic_eq_empty[simp] = not_Iic_eq_empty[symmetric]
+
+end
+
 context order
 begin
 
 lemma atLeastatMost_empty[simp]:
   "b < a \<Longrightarrow> {a..b} = {}"
-by(auto simp: atLeastAtMost_def atLeast_def atMost_def)
-
-lemma atLeastatMost_empty_iff[simp]:
-  "{a..b} = {} \<longleftrightarrow> (\<not> a \<le> b)"
-by auto (blast intro: order_trans)
-
-lemma atLeastatMost_empty_iff2[simp]:
-  "{} = {a..b} \<longleftrightarrow> (\<not> a \<le> b)"
-by auto (blast intro: order_trans)
+  by(auto simp: atLeastAtMost_def atLeast_def atMost_def)
 
 lemma atLeastLessThan_empty[simp]:
-  "b <= a \<Longrightarrow> {a..<b} = {}"
-by(auto simp: atLeastLessThan_def)
-
-lemma atLeastLessThan_empty_iff[simp]:
-  "{a..<b} = {} \<longleftrightarrow> (\<not> a < b)"
-by auto (blast intro: le_less_trans)
-
-lemma atLeastLessThan_empty_iff2[simp]:
-  "{} = {a..<b} \<longleftrightarrow> (\<not> a < b)"
-by auto (blast intro: le_less_trans)
+  "b \<le> a \<Longrightarrow> {a..<b} = {}"
+  by(auto simp: atLeastLessThan_def)
 
 lemma greaterThanAtMost_empty[simp]: "l \<le> k ==> {k<..l} = {}"
-by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)
-
-lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \<longleftrightarrow> \<not> k < l"
-by auto (blast intro: less_le_trans)
-
-lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \<longleftrightarrow> \<not> k < l"
-by auto (blast intro: less_le_trans)
+  by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def)
 
 lemma greaterThanLessThan_empty[simp]:"l \<le> k ==> {k<..<l} = {}"
-by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def)
+  by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def)
 
 lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}"
-by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)
+  by (auto simp add: atLeastAtMost_def atMost_def atLeast_def)
 
 lemma atLeastAtMost_singleton': "a = b \<Longrightarrow> {a .. b} = {a}" by simp
 
-lemma atLeastatMost_subset_iff[simp]:
-  "{a..b} \<le> {c..d} \<longleftrightarrow> (\<not> a \<le> b) \<or> c \<le> a \<and> b \<le> d"
-unfolding atLeastAtMost_def atLeast_def atMost_def
-by (blast intro: order_trans)
-
-lemma atLeastatMost_psubset_iff:
-  "{a..b} < {c..d} \<longleftrightarrow>
-   ((\<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 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.eq_iff)(auto intro: order_trans)
 
 lemma atLeastAtMost_singleton_iff[simp]:
   "{a .. b} = {c} \<longleftrightarrow> a = b \<and> b = c"
@@ -280,23 +300,6 @@
   with * show "a = b \<and> b = c" by auto
 qed simp
 
-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)
-
-lemma Icc_subset_Iic_iff[simp]:
-  "{l..h} \<subseteq> {..h'} = (\<not> l\<le>h \<or> h\<le>h')"
-by(auto simp: subset_eq intro: order_trans)
-
-lemma not_Ici_eq_empty[simp]: "{l..} \<noteq> {}"
-by(auto simp: set_eq_iff)
-
-lemma not_Iic_eq_empty[simp]: "{..h} \<noteq> {}"
-by(auto simp: set_eq_iff)
-
-lemmas not_empty_eq_Ici_eq_empty[simp] = not_Ici_eq_empty[symmetric]
-lemmas not_empty_eq_Iic_eq_empty[simp] = not_Iic_eq_empty[symmetric]
-
 end
 
 context no_top
@@ -811,7 +814,7 @@
 text \<open>The analogous result is useful on \<^typ>\<open>int\<close>:\<close>
 (* here, because we don't have an own int section *)
 lemma atLeastAtMostPlus1_int_conv:
-  "m <= 1+n \<Longrightarrow> {m..1+n} = insert (1+n) {m..n::int}"
+  "m \<le> 1+n \<Longrightarrow> {m..1+n} = insert (1+n) {m..n::int}"
   by (auto intro: set_eqI)
 
 lemma atLeastLessThan_add_Un: "i \<le> j \<Longrightarrow> {i..<j+k} = {i..<j} \<union> {j..<j+k::nat}"
@@ -1224,7 +1227,7 @@
   next
     case (insert b A)
     hence *: "b \<notin> A" by auto
-    with insert have "A <= {k..<k + card A}" and "b = k + card A"
+    with insert have "A \<le> {k..<k + card A}" and "b = k + card A"
       by fastforce+
     with insert * show ?case by auto
   qed
@@ -2483,6 +2486,6 @@
     by (simp add: prod.eq_fold fold_atLeastAtMost_nat o_def)
 qed
 
-(* TODO: Add support for more kinds of intervals here *)
+(* TODO: Add support for folding over more kinds of intervals here *)
 
 end