# HG changeset patch
# User wenzelm
# Date 1590347483 -7200
# Node ID 45f85e283ce075981e52f02f612dbcd796e96d27
# Parent  86cfb9fa3da82b14c3bcb5e2a247ae422b9d01d6# Parent  2bf0283fc9755a9d6b8e868f116c4ae0574f5c64
merged

diff -r 2bf0283fc975 -r 45f85e283ce0 src/HOL/Analysis/Abstract_Topology.thy
--- 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
diff -r 2bf0283fc975 -r 45f85e283ce0 src/HOL/Analysis/Starlike.thy
--- 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"
diff -r 2bf0283fc975 -r 45f85e283ce0 src/HOL/BNF_Wellorder_Embedding.thy
--- 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:
diff -r 2bf0283fc975 -r 45f85e283ce0 src/HOL/Data_Structures/Balance.thy
--- 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
diff -r 2bf0283fc975 -r 45f85e283ce0 src/HOL/Fun.thy
--- 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"
 
diff -r 2bf0283fc975 -r 45f85e283ce0 src/HOL/Library/Equipollence.thy
--- 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)
diff -r 2bf0283fc975 -r 45f85e283ce0 src/HOL/List.thy
--- 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>