# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1590265473 -3600
# Node ID d73955442df51236fdc5448daa886148aa7c22db
# Parent  e9df7895e3310bec8a39c0e287d4aea9c357b0c3
a few new lemmas about functions

diff -r e9df7895e331 -r d73955442df5 src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Fri May 22 19:21:16 2020 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Sat May 23 21:24:33 2020 +0100
@@ -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 e9df7895e331 -r d73955442df5 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Fri May 22 19:21:16 2020 +0200
+++ b/src/HOL/Analysis/Starlike.thy	Sat May 23 21:24:33 2020 +0100
@@ -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 e9df7895e331 -r d73955442df5 src/HOL/BNF_Wellorder_Embedding.thy
--- a/src/HOL/BNF_Wellorder_Embedding.thy	Fri May 22 19:21:16 2020 +0200
+++ b/src/HOL/BNF_Wellorder_Embedding.thy	Sat May 23 21:24:33 2020 +0100
@@ -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 e9df7895e331 -r d73955442df5 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Fri May 22 19:21:16 2020 +0200
+++ b/src/HOL/Fun.thy	Sat May 23 21:24:33 2020 +0100
@@ -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 e9df7895e331 -r d73955442df5 src/HOL/Library/Equipollence.thy
--- a/src/HOL/Library/Equipollence.thy	Fri May 22 19:21:16 2020 +0200
+++ b/src/HOL/Library/Equipollence.thy	Sat May 23 21:24:33 2020 +0100
@@ -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 e9df7895e331 -r d73955442df5 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri May 22 19:21:16 2020 +0200
+++ b/src/HOL/List.thy	Sat May 23 21:24:33 2020 +0100
@@ -6117,6 +6117,67 @@
   by (simp add: Uniq_def strict_sorted_equal)
 
 
+lemma length_sorted_list_of_set [simp]:
+  fixes A :: "'a::linorder set" 
+  shows "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
+
+lemma sorted_list_of_set_inject:
+  fixes A :: "'a::linorder set" 
+  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:
+  fixes A :: "'a::linorder set" 
+  assumes "finite A"
+  shows "strict_sorted l \<and> List.set l = A \<and> length l = card A \<longleftrightarrow> sorted_list_of_set A = l"
+  using assms strict_sorted_equal by force
+
+
+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>
 
 inductive_set