6 *) |
6 *) |
7 |
7 |
8 header {* More on Injections, Bijections and Inverses (FP) *} |
8 header {* More on Injections, Bijections and Inverses (FP) *} |
9 |
9 |
10 theory Fun_More_FP |
10 theory Fun_More_FP |
11 imports "~~/src/HOL/Library/Infinite_Set" |
11 imports Main |
12 begin |
12 begin |
13 |
13 |
14 |
14 |
15 text {* This section proves more facts (additional to those in @{text "Fun.thy"}, |
15 text {* This section proves more facts (additional to those in @{text "Fun.thy"}, |
16 @{text "Hilbert_Choice.thy"}, @{text "Finite_Set.thy"} and @{text "Infinite_Set.thy"}), |
16 @{text "Hilbert_Choice.thy"}, and @{text "Finite_Set.thy"}), |
17 mainly concerning injections, bijections, inverses and (numeric) cardinals of |
17 mainly concerning injections, bijections, inverses and (numeric) cardinals of |
18 finite sets. *} |
18 finite sets. *} |
19 |
19 |
20 |
20 |
21 subsection {* Purely functional properties *} |
21 subsection {* Purely functional properties *} |
95 |
95 |
96 |
96 |
97 (*3*)lemma inj_on_finite: |
97 (*3*)lemma inj_on_finite: |
98 assumes "inj_on f A" "f ` A \<le> B" "finite B" |
98 assumes "inj_on f A" "f ` A \<le> B" "finite B" |
99 shows "finite A" |
99 shows "finite A" |
100 using assms infinite_super by (fast dest: finite_imageD) |
100 using assms by (metis finite_imageD finite_subset) |
101 |
101 |
102 |
102 |
103 (*3*)lemma infinite_imp_bij_betw: |
103 (*3*)lemma infinite_imp_bij_betw: |
104 assumes INF: "infinite A" |
104 assumes INF: "\<not> finite A" |
105 shows "\<exists>h. bij_betw h A (A - {a})" |
105 shows "\<exists>h. bij_betw h A (A - {a})" |
106 proof(cases "a \<in> A") |
106 proof(cases "a \<in> A") |
107 assume Case1: "a \<notin> A" hence "A - {a} = A" by blast |
107 assume Case1: "a \<notin> A" hence "A - {a} = A" by blast |
108 thus ?thesis using bij_betw_id[of A] by auto |
108 thus ?thesis using bij_betw_id[of A] by auto |
109 next |
109 next |
110 assume Case2: "a \<in> A" |
110 assume Case2: "a \<in> A" |
111 have "infinite (A - {a})" using INF infinite_remove by auto |
111 find_theorems "\<not> finite _" |
|
112 have "\<not> finite (A - {a})" using INF by auto |
112 with infinite_iff_countable_subset[of "A - {a}"] obtain f::"nat \<Rightarrow> 'a" |
113 with infinite_iff_countable_subset[of "A - {a}"] obtain f::"nat \<Rightarrow> 'a" |
113 where 1: "inj f" and 2: "f ` UNIV \<le> A - {a}" by blast |
114 where 1: "inj f" and 2: "f ` UNIV \<le> A - {a}" by blast |
114 obtain g where g_def: "g = (\<lambda> n. if n = 0 then a else f (Suc n))" by blast |
115 obtain g where g_def: "g = (\<lambda> n. if n = 0 then a else f (Suc n))" by blast |
115 obtain A' where A'_def: "A' = g ` UNIV" by blast |
116 obtain A' where A'_def: "A' = g ` UNIV" by blast |
116 have temp: "\<forall>y. f y \<noteq> a" using 2 by blast |
117 have temp: "\<forall>y. f y \<noteq> a" using 2 by blast |
177 thus ?thesis by blast |
178 thus ?thesis by blast |
178 qed |
179 qed |
179 |
180 |
180 |
181 |
181 (*3*)lemma infinite_imp_bij_betw2: |
182 (*3*)lemma infinite_imp_bij_betw2: |
182 assumes INF: "infinite A" |
183 assumes INF: "\<not> finite A" |
183 shows "\<exists>h. bij_betw h A (A \<union> {a})" |
184 shows "\<exists>h. bij_betw h A (A \<union> {a})" |
184 proof(cases "a \<in> A") |
185 proof(cases "a \<in> A") |
185 assume Case1: "a \<in> A" hence "A \<union> {a} = A" by blast |
186 assume Case1: "a \<in> A" hence "A \<union> {a} = A" by blast |
186 thus ?thesis using bij_betw_id[of A] by auto |
187 thus ?thesis using bij_betw_id[of A] by auto |
187 next |
188 next |
188 let ?A' = "A \<union> {a}" |
189 let ?A' = "A \<union> {a}" |
189 assume Case2: "a \<notin> A" hence "A = ?A' - {a}" by blast |
190 assume Case2: "a \<notin> A" hence "A = ?A' - {a}" by blast |
190 moreover have "infinite ?A'" using INF by auto |
191 moreover have "\<not> finite ?A'" using INF by auto |
191 ultimately obtain f where "bij_betw f ?A' A" |
192 ultimately obtain f where "bij_betw f ?A' A" |
192 using infinite_imp_bij_betw[of ?A' a] by auto |
193 using infinite_imp_bij_betw[of ?A' a] by auto |
193 hence "bij_betw(inv_into ?A' f) A ?A'" using bij_betw_inv_into by blast |
194 hence "bij_betw(inv_into ?A' f) A ?A'" using bij_betw_inv_into by blast |
194 thus ?thesis by auto |
195 thus ?thesis by auto |
195 qed |
196 qed |