--- a/src/HOL/Analysis/Abstract_Topology.thy Sun May 24 21:01:51 2020 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy Sun May 24 21:11:23 2020 +0200
@@ -2673,7 +2673,8 @@
then have "False"
using homeomorphic_map_closure_of [OF hom] hom
unfolding homeomorphic_eq_everything_map
- by (metis (no_types, lifting) Diff_subset S closure_of_subset_topspace inj_on_image_mem_iff_alt inj_on_image_set_diff) }
+ by (metis Diff_subset S closure_of_subset_topspace inj_on_image_mem_iff inj_on_image_set_diff)
+ }
ultimately show ?thesis
by (auto simp: interior_of_closure_of)
qed
@@ -2700,7 +2701,7 @@
then have "y \<in> topspace X"
by (simp add: in_closure_of)
then have "f y \<notin> f ` (X interior_of S)"
- by (meson hom homeomorphic_eq_everything_map inj_on_image_mem_iff_alt interior_of_subset_topspace y(3))
+ by (meson hom homeomorphic_map_def inj_on_image_mem_iff interior_of_subset_topspace y(3))
then show "x \<notin> Y interior_of f ` S"
using S hom homeomorphic_map_interior_of y(1) by blast
qed
--- a/src/HOL/Analysis/Starlike.thy Sun May 24 21:01:51 2020 +0200
+++ b/src/HOL/Analysis/Starlike.thy Sun May 24 21:11:23 2020 +0200
@@ -3519,7 +3519,7 @@
ultimately have "f a \<in> f ` closed_segment c b"
by blast
then have a: "a \<in> closed_segment c b"
- by (meson ends_in_segment inj_on_image_mem_iff_alt injf subset_closed_segment that)
+ by (meson ends_in_segment inj_on_image_mem_iff injf subset_closed_segment that)
have cb: "closed_segment c b \<subseteq> closed_segment a b"
by (simp add: closed_segment_subset that)
show "f a = f c"
@@ -3539,7 +3539,7 @@
ultimately have "f b \<in> f ` closed_segment a c"
by blast
then have b: "b \<in> closed_segment a c"
- by (meson ends_in_segment inj_on_image_mem_iff_alt injf subset_closed_segment that)
+ by (meson ends_in_segment inj_on_image_mem_iff injf subset_closed_segment that)
have ca: "closed_segment a c \<subseteq> closed_segment a b"
by (simp add: closed_segment_subset that)
show "f b = f c"
--- a/src/HOL/BNF_Wellorder_Embedding.thy Sun May 24 21:01:51 2020 +0200
+++ b/src/HOL/BNF_Wellorder_Embedding.thy Sun May 24 21:11:23 2020 +0200
@@ -1003,55 +1003,29 @@
with * show "iso r r' f" unfolding iso_def by auto
qed
-lemma iso_iff2:
-assumes "Well_order r"
-shows "iso r r' f = (bij_betw f (Field r) (Field r') \<and>
- (\<forall>a \<in> Field r. \<forall>b \<in> Field r.
- (((a,b) \<in> r) = ((f a, f b) \<in> r'))))"
-using assms
-proof(auto simp add: iso_def)
- fix a b
- assume "embed r r' f"
- hence "compat r r' f" using embed_compat[of r] by auto
- moreover assume "(a,b) \<in> r"
- ultimately show "(f a, f b) \<in> r'" using compat_def[of r] by auto
-next
- let ?f' = "inv_into (Field r) f"
- assume "embed r r' f" and 1: "bij_betw f (Field r) (Field r')"
- hence "embed r' r ?f'" using assms
- by (auto simp add: inv_into_Field_embed_bij_betw)
- hence 2: "compat r' r ?f'" using embed_compat[of r'] by auto
- fix a b assume *: "a \<in> Field r" "b \<in> Field r" and **: "(f a,f b) \<in> r'"
- hence "?f'(f a) = a \<and> ?f'(f b) = b" using 1
- by (auto simp add: bij_betw_inv_into_left)
- thus "(a,b) \<in> r" using ** 2 compat_def[of r' r ?f'] by fastforce
+lemma iso_iff2: "iso r r' f \<longleftrightarrow>
+ bij_betw f (Field r) (Field r') \<and>
+ (\<forall>a \<in> Field r. \<forall>b \<in> Field r. (a, b) \<in> r \<longleftrightarrow> (f a, f b) \<in> r')"
+ (is "?lhs = ?rhs")
+proof
+ assume L: ?lhs
+ then have "bij_betw f (Field r) (Field r')" and emb: "embed r r' f"
+ by (auto simp: bij_betw_def iso_def)
+ then obtain g where g: "\<And>x. x \<in> Field r \<Longrightarrow> g (f x) = x"
+ by (auto simp: bij_betw_iff_bijections)
+ moreover
+ have "(a, b) \<in> r" if "a \<in> Field r" "b \<in> Field r" "(f a, f b) \<in> r'" for a b
+ using that emb g g [OF FieldI1] \<comment>\<open>yes it's weird\<close>
+ by (force simp add: embed_def under_def bij_betw_iff_bijections)
+ ultimately show ?rhs
+ using L by (auto simp: compat_def iso_def dest: embed_compat)
next
- assume *: "bij_betw f (Field r) (Field r')" and
- **: "\<forall>a\<in>Field r. \<forall>b\<in>Field r. ((a, b) \<in> r) = ((f a, f b) \<in> r')"
- have 1: "\<And> a. under r a \<le> Field r \<and> under r' (f a) \<le> Field r'"
- by (auto simp add: under_Field)
- have 2: "inj_on f (Field r)" using * by (auto simp add: bij_betw_def)
- {fix a assume ***: "a \<in> Field r"
- have "bij_betw f (under r a) (under r' (f a))"
- proof(unfold bij_betw_def, auto)
- show "inj_on f (under r a)" using 1 2 subset_inj_on by blast
- next
- fix b assume "b \<in> under r a"
- hence "a \<in> Field r \<and> b \<in> Field r \<and> (b,a) \<in> r"
- unfolding under_def by (auto simp add: Field_def Range_def Domain_def)
- with 1 ** show "f b \<in> under r' (f a)"
- unfolding under_def by auto
- next
- fix b' assume "b' \<in> under r' (f a)"
- hence 3: "(b',f a) \<in> r'" unfolding under_def by simp
- hence "b' \<in> Field r'" unfolding Field_def by auto
- with * obtain b where "b \<in> Field r \<and> f b = b'"
- unfolding bij_betw_def by force
- with 3 ** ***
- show "b' \<in> f ` (under r a)" unfolding under_def by blast
- qed
- }
- thus "embed r r' f" unfolding embed_def using * by auto
+ assume R: ?rhs
+ then show ?lhs
+ apply (clarsimp simp add: iso_def embed_def under_def bij_betw_iff_bijections)
+ apply (rule_tac x="g" in exI)
+ apply (fastforce simp add: intro: FieldI1)+
+ done
qed
lemma iso_iff3:
--- a/src/HOL/Data_Structures/Balance.thy Sun May 24 21:01:51 2020 +0200
+++ b/src/HOL/Data_Structures/Balance.thy Sun May 24 21:11:23 2020 +0200
@@ -42,23 +42,23 @@
lemma bal_inorder:
"\<lbrakk> n \<le> length xs; bal n xs = (t,zs) \<rbrakk>
\<Longrightarrow> xs = inorder t @ zs \<and> size t = n"
-proof(induction n xs arbitrary: t zs rule: bal.induct)
- case (1 n xs) show ?case
+proof(induction n arbitrary: xs t zs rule: less_induct)
+ case (less n) show ?case
proof cases
- assume "n = 0" thus ?thesis using 1 by (simp add: bal_simps)
+ assume "n = 0" thus ?thesis using less.prems by (simp add: bal_simps)
next
assume [arith]: "n \<noteq> 0"
let ?m = "n div 2" let ?m' = "n - 1 - ?m"
- from "1.prems"(2) obtain l r ys where
+ from less.prems(2) obtain l r ys where
b1: "bal ?m xs = (l,ys)" and
b2: "bal ?m' (tl ys) = (r,zs)" and
t: "t = \<langle>l, hd ys, r\<rangle>"
by(auto simp: bal_simps split: prod.splits)
have IH1: "xs = inorder l @ ys \<and> size l = ?m"
- using b1 "1.prems"(1) by(intro "1.IH"(1)) auto
+ using b1 less.prems(1) by(intro less.IH) auto
have IH2: "tl ys = inorder r @ zs \<and> size r = ?m'"
- using b1 b2 IH1 "1.prems"(1) by(intro "1.IH"(2)) auto
- show ?thesis using t IH1 IH2 "1.prems"(1) hd_Cons_tl[of ys] by fastforce
+ using b2 IH1 less.prems(1) by(intro less.IH) auto
+ show ?thesis using t IH1 IH2 less.prems(1) hd_Cons_tl[of ys] by fastforce
qed
qed
@@ -102,24 +102,24 @@
lemma min_height_bal:
"\<lbrakk> n \<le> length xs; bal n xs = (t,zs) \<rbrakk> \<Longrightarrow> min_height t = nat(\<lfloor>log 2 (n + 1)\<rfloor>)"
-proof(induction n xs arbitrary: t zs rule: bal.induct)
- case (1 n xs)
+proof(induction n arbitrary: xs t zs rule: less_induct)
+ case (less n)
show ?case
proof cases
- assume "n = 0" thus ?thesis using "1.prems"(2) by (simp add: bal_simps)
+ assume "n = 0" thus ?thesis using less.prems(2) by (simp add: bal_simps)
next
assume [arith]: "n \<noteq> 0"
let ?m = "n div 2" let ?m' = "n - 1 - ?m"
- from "1.prems" obtain l r ys where
+ from less.prems obtain l r ys where
b1: "bal ?m xs = (l,ys)" and
b2: "bal ?m' (tl ys) = (r,zs)" and
t: "t = \<langle>l, hd ys, r\<rangle>"
by(auto simp: bal_simps split: prod.splits)
let ?hl = "nat (floor(log 2 (?m + 1)))"
let ?hr = "nat (floor(log 2 (?m' + 1)))"
- have IH1: "min_height l = ?hl" using "1.IH"(1) b1 "1.prems"(1) by simp
+ have IH1: "min_height l = ?hl" using less.IH[OF _ _ b1] less.prems(1) by simp
have IH2: "min_height r = ?hr"
- using "1.prems"(1) bal_length[OF _ b1] b1 b2 by(intro "1.IH"(2)) auto
+ using less.prems(1) bal_length[OF _ b1] b2 by(intro less.IH) auto
have "(n+1) div 2 \<ge> 1" by arith
hence 0: "log 2 ((n+1) div 2) \<ge> 0" by simp
have "?m' \<le> ?m" by arith
@@ -138,24 +138,24 @@
lemma height_bal:
"\<lbrakk> n \<le> length xs; bal n xs = (t,zs) \<rbrakk> \<Longrightarrow> height t = nat \<lceil>log 2 (n + 1)\<rceil>"
-proof(induction n xs arbitrary: t zs rule: bal.induct)
- case (1 n xs) show ?case
+proof(induction n arbitrary: xs t zs rule: less_induct)
+ case (less n) show ?case
proof cases
assume "n = 0" thus ?thesis
- using "1.prems" by (simp add: bal_simps)
+ using less.prems by (simp add: bal_simps)
next
assume [arith]: "n \<noteq> 0"
let ?m = "n div 2" let ?m' = "n - 1 - ?m"
- from "1.prems" obtain l r ys where
+ from less.prems obtain l r ys where
b1: "bal ?m xs = (l,ys)" and
b2: "bal ?m' (tl ys) = (r,zs)" and
t: "t = \<langle>l, hd ys, r\<rangle>"
by(auto simp: bal_simps split: prod.splits)
let ?hl = "nat \<lceil>log 2 (?m + 1)\<rceil>"
let ?hr = "nat \<lceil>log 2 (?m' + 1)\<rceil>"
- have IH1: "height l = ?hl" using "1.IH"(1) b1 "1.prems"(1) by simp
+ have IH1: "height l = ?hl" using less.IH[OF _ _ b1] less.prems(1) by simp
have IH2: "height r = ?hr"
- using b1 b2 bal_length[OF _ b1] "1.prems"(1) by(intro "1.IH"(2)) auto
+ using b2 bal_length[OF _ b1] less.prems(1) by(intro less.IH) auto
have 0: "log 2 (?m + 1) \<ge> 0" by simp
have "?m' \<le> ?m" by arith
hence le: "?hr \<le> ?hl"
@@ -205,23 +205,23 @@
by (simp add: balance_tree_def)
lemma wbalanced_bal: "\<lbrakk> n \<le> length xs; bal n xs = (t,ys) \<rbrakk> \<Longrightarrow> wbalanced t"
-proof(induction n xs arbitrary: t ys rule: bal.induct)
- case (1 n xs)
+proof(induction n arbitrary: xs t ys rule: less_induct)
+ case (less n)
show ?case
proof cases
assume "n = 0"
- thus ?thesis using "1.prems"(2) by(simp add: bal_simps)
+ thus ?thesis using less.prems(2) by(simp add: bal_simps)
next
assume [arith]: "n \<noteq> 0"
- with "1.prems" obtain l ys r zs where
+ with less.prems obtain l ys r zs where
rec1: "bal (n div 2) xs = (l, ys)" and
rec2: "bal (n - 1 - n div 2) (tl ys) = (r, zs)" and
t: "t = \<langle>l, hd ys, r\<rangle>"
by(auto simp add: bal_simps split: prod.splits)
- have l: "wbalanced l" using "1.IH"(1)[OF \<open>n\<noteq>0\<close> refl _ rec1] "1.prems"(1) by linarith
+ have l: "wbalanced l" using less.IH[OF _ _ rec1] less.prems(1) by linarith
have "wbalanced r"
- using rec1 rec2 bal_length[OF _ rec1] "1.prems"(1) by(intro "1.IH"(2)) auto
- with l t bal_length[OF _ rec1] "1.prems"(1) bal_inorder[OF _ rec1] bal_inorder[OF _ rec2]
+ using rec1 rec2 bal_length[OF _ rec1] less.prems(1) by(intro less.IH) auto
+ with l t bal_length[OF _ rec1] less.prems(1) bal_inorder[OF _ rec1] bal_inorder[OF _ rec2]
show ?thesis by auto
qed
qed
--- a/src/HOL/Fun.thy Sun May 24 21:01:51 2020 +0200
+++ b/src/HOL/Fun.thy Sun May 24 21:11:23 2020 +0200
@@ -507,10 +507,6 @@
lemma inj_on_image_mem_iff: "inj_on f B \<Longrightarrow> a \<in> B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> f a \<in> f ` A \<longleftrightarrow> a \<in> A"
by (auto simp: inj_on_def)
-(*FIXME DELETE*)
-lemma inj_on_image_mem_iff_alt: "inj_on f B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> f a \<in> f ` A \<Longrightarrow> a \<in> B \<Longrightarrow> a \<in> A"
- by (blast dest: inj_onD)
-
lemma inj_image_mem_iff: "inj f \<Longrightarrow> f a \<in> f ` A \<longleftrightarrow> a \<in> A"
by (blast dest: injD)
@@ -614,7 +610,20 @@
using * bij_betw_subset[of f "A \<union> {b}" _ A] by blast
qed
-text \<open>Important examples\<close>
+lemma inj_on_disjoint_Un:
+ assumes "inj_on f A" and "inj_on g B"
+ and "f ` A \<inter> g ` B = {}"
+ shows "inj_on (\<lambda>x. if x \<in> A then f x else g x) (A \<union> B)"
+ using assms by (simp add: inj_on_def disjoint_iff) (blast)
+
+lemma bij_betw_disjoint_Un:
+ assumes "bij_betw f A C" and "bij_betw g B D"
+ and "A \<inter> B = {}"
+ and "C \<inter> D = {}"
+ shows "bij_betw (\<lambda>x. if x \<in> A then f x else g x) (A \<union> B) (C \<union> D)"
+ using assms by (auto simp: inj_on_disjoint_Un bij_betw_def)
+
+subsubsection \<open>Important examples\<close>
context cancel_semigroup_add
begin
@@ -859,27 +868,18 @@
unfolding the_inv_into_def inj_on_def by blast
lemma f_the_inv_into_f: "inj_on f A \<Longrightarrow> y \<in> f ` A \<Longrightarrow> f (the_inv_into A f y) = y"
- apply (simp add: the_inv_into_def)
- apply (rule the1I2)
- apply (blast dest: inj_onD)
- apply blast
- done
+ unfolding the_inv_into_def
+ by (rule the1I2; blast dest: inj_onD)
lemma the_inv_into_into: "inj_on f A \<Longrightarrow> x \<in> f ` A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> the_inv_into A f x \<in> B"
- apply (simp add: the_inv_into_def)
- apply (rule the1I2)
- apply (blast dest: inj_onD)
- apply blast
- done
+ unfolding the_inv_into_def
+ by (rule the1I2; blast dest: inj_onD)
lemma the_inv_into_onto [simp]: "inj_on f A \<Longrightarrow> the_inv_into A f ` (f ` A) = A"
by (fast intro: the_inv_into_into the_inv_into_f_f [symmetric])
lemma the_inv_into_f_eq: "inj_on f A \<Longrightarrow> f x = y \<Longrightarrow> x \<in> A \<Longrightarrow> the_inv_into A f y = x"
- apply (erule subst)
- apply (erule the_inv_into_f_f)
- apply assumption
- done
+ by (force simp add: the_inv_into_f_f)
lemma the_inv_into_comp:
"inj_on f (g ` A) \<Longrightarrow> inj_on g A \<Longrightarrow> x \<in> f ` g ` A \<Longrightarrow>
@@ -896,6 +896,17 @@
lemma bij_betw_the_inv_into: "bij_betw f A B \<Longrightarrow> bij_betw (the_inv_into A f) B A"
by (auto simp add: bij_betw_def inj_on_the_inv_into the_inv_into_into)
+lemma bij_betw_iff_bijections:
+ "bij_betw f A B \<longleftrightarrow> (\<exists>g. (\<forall>x \<in> A. f x \<in> B \<and> g(f x) = x) \<and> (\<forall>y \<in> B. g y \<in> A \<and> f(g y) = y))"
+ (is "?lhs = ?rhs")
+proof
+ assume L: ?lhs
+ then show ?rhs
+ apply (rule_tac x="the_inv_into A f" in exI)
+ apply (auto simp: bij_betw_def f_the_inv_into_f the_inv_into_f_f the_inv_into_into)
+ done
+qed (force intro: bij_betw_byWitness)
+
abbreviation the_inv :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a)"
where "the_inv f \<equiv> the_inv_into UNIV f"
--- a/src/HOL/Library/Equipollence.thy Sun May 24 21:01:51 2020 +0200
+++ b/src/HOL/Library/Equipollence.thy Sun May 24 21:11:23 2020 +0200
@@ -98,21 +98,6 @@
by (auto simp: inj_on_def)
qed auto
-lemma bij_betw_iff_bijections:
- "bij_betw f A B \<longleftrightarrow> (\<exists>g. (\<forall>x \<in> A. f x \<in> B \<and> g(f x) = x) \<and> (\<forall>y \<in> B. g y \<in> A \<and> f(g y) = y))"
- (is "?lhs = ?rhs")
-proof
- assume L: ?lhs
- then show ?rhs
- apply (rule_tac x="the_inv_into A f" in exI)
- apply (auto simp: bij_betw_def f_the_inv_into_f the_inv_into_f_f the_inv_into_into)
- done
-next
- assume ?rhs
- then show ?lhs
- by (auto simp: bij_betw_def inj_on_def image_def; metis)
-qed
-
lemma eqpoll_iff_bijections:
"A \<approx> B \<longleftrightarrow> (\<exists>f g. (\<forall>x \<in> A. f x \<in> B \<and> g(f x) = x) \<and> (\<forall>y \<in> B. g y \<in> A \<and> f(g y) = y))"
by (auto simp: eqpoll_def bij_betw_iff_bijections)
--- a/src/HOL/List.thy Sun May 24 21:01:51 2020 +0200
+++ b/src/HOL/List.thy Sun May 24 21:11:23 2020 +0200
@@ -365,8 +365,6 @@
"sorted_wrt P [] = True" |
"sorted_wrt P (x # ys) = ((\<forall>y \<in> set ys. P x y) \<and> sorted_wrt P ys)"
-(* FIXME: define sorted in terms of sorted_wrt *)
-
text \<open>A class-based sorted predicate:\<close>
context linorder
@@ -412,6 +410,9 @@
"stable_sort_key sk =
(\<forall>f xs k. filter (\<lambda>y. f y = k) (sk f xs) = filter (\<lambda>y. f y = k) xs)"
+lemma strict_sorted_iff: "strict_sorted l \<longleftrightarrow> sorted l \<and> distinct l"
+by (induction l) (auto iff: antisym_conv1)
+
end
@@ -6049,6 +6050,13 @@
case False thus ?thesis by simp
qed
+lemma length_sorted_list_of_set [simp]: "length (sorted_list_of_set A) = card A"
+proof (cases "finite A")
+ case True
+ then show ?thesis
+ by(metis distinct_card distinct_sorted_list_of_set set_sorted_list_of_set)
+qed auto
+
lemmas sorted_list_of_set = set_sorted_list_of_set sorted_sorted_list_of_set distinct_sorted_list_of_set
lemma sorted_list_of_set_sort_remdups [code]:
@@ -6069,28 +6077,18 @@
with assms show ?thesis by simp
qed
-end
-
-lemma sorted_list_of_set_range [simp]:
- "sorted_list_of_set {m..<n} = [m..<n]"
-by (rule sorted_distinct_set_unique) simp_all
-
-lemma strict_sorted_iff: "strict_sorted l \<longleftrightarrow> sorted l \<and> distinct l"
- by (induction l) (use less_le in auto)
-
lemma strict_sorted_list_of_set [simp]: "strict_sorted (sorted_list_of_set A)"
by (simp add: strict_sorted_iff)
lemma finite_set_strict_sorted:
- fixes A :: "'a::linorder set"
assumes "finite A"
- obtains l where "strict_sorted l" "List.set l = A" "length l = card A"
+ obtains l where "strict_sorted l" "set l = A" "length l = card A"
by (metis assms distinct_card distinct_sorted_list_of_set set_sorted_list_of_set strict_sorted_list_of_set)
lemma strict_sorted_equal:
assumes "strict_sorted xs"
and "strict_sorted ys"
- and "list.set ys = list.set xs"
+ and "set ys = set xs"
shows "ys = xs"
using assms
proof (induction xs arbitrary: ys)
@@ -6111,9 +6109,63 @@
qed
qed auto
-lemma strict_sorted_equal_Uniq: "\<exists>\<^sub>\<le>\<^sub>1xs. strict_sorted xs \<and> list.set xs = A"
+lemma strict_sorted_equal_Uniq: "\<exists>\<^sub>\<le>\<^sub>1xs. strict_sorted xs \<and> set xs = A"
by (simp add: Uniq_def strict_sorted_equal)
+lemma sorted_list_of_set_inject:
+ assumes "sorted_list_of_set A = sorted_list_of_set B" "finite A" "finite B"
+ shows "A = B"
+ using assms set_sorted_list_of_set by fastforce
+
+lemma sorted_list_of_set_unique:
+ assumes "finite A"
+ shows "strict_sorted l \<and> set l = A \<and> length l = card A \<longleftrightarrow> sorted_list_of_set A = l"
+ using assms strict_sorted_equal by force
+
+end
+
+lemma sorted_list_of_set_range [simp]:
+ "sorted_list_of_set {m..<n} = [m..<n]"
+by (rule sorted_distinct_set_unique) simp_all
+
+lemma sorted_list_of_set_lessThan_Suc [simp]:
+ "sorted_list_of_set {..<Suc k} = sorted_list_of_set {..<k} @ [k]"
+proof -
+ have "sorted_wrt (<) (sorted_list_of_set {..<k} @ [k])"
+ unfolding sorted_wrt_append by (auto simp flip: strict_sorted_sorted_wrt)
+ then show ?thesis
+ by (simp add: lessThan_atLeast0)
+qed
+
+lemma sorted_list_of_set_atMost_Suc [simp]:
+ "sorted_list_of_set {..Suc k} = sorted_list_of_set {..k} @ [Suc k]"
+ using lessThan_Suc_atMost sorted_list_of_set_lessThan_Suc by fastforce
+
+lemma sorted_list_of_set_greaterThanLessThan:
+ assumes "Suc i < j"
+ shows "sorted_list_of_set {i<..<j} = Suc i # sorted_list_of_set {Suc i<..<j}"
+proof -
+ have "{i<..<j} = insert (Suc i) {Suc i<..<j}"
+ using assms by auto
+ then show ?thesis
+ by (metis assms atLeastSucLessThan_greaterThanLessThan sorted_list_of_set_range upt_conv_Cons)
+qed
+
+lemma sorted_list_of_set_greaterThanAtMost:
+ assumes "Suc i \<le> j"
+ shows "sorted_list_of_set {i<..j} = Suc i # sorted_list_of_set {Suc i<..j}"
+ using sorted_list_of_set_greaterThanLessThan [of i "Suc j"]
+ by (metis assms greaterThanAtMost_def greaterThanLessThan_eq le_imp_less_Suc lessThan_Suc_atMost)
+
+lemma nth_sorted_list_of_set_greaterThanLessThan:
+ "n < j - Suc i \<Longrightarrow> sorted_list_of_set {i<..<j} ! n = Suc (i+n)"
+ by (induction n arbitrary: i) (auto simp: sorted_list_of_set_greaterThanLessThan)
+
+lemma nth_sorted_list_of_set_greaterThanAtMost:
+ "n < j - i \<Longrightarrow> sorted_list_of_set {i<..j} ! n = Suc (i+n)"
+ using nth_sorted_list_of_set_greaterThanLessThan [of n "Suc j" i]
+ by (simp add: greaterThanAtMost_def greaterThanLessThan_eq lessThan_Suc_atMost)
+
subsubsection \<open>\<open>lists\<close>: the list-forming operator over sets\<close>