--- 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
--- 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"
--- 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:
--- 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"
--- 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)
--- 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