1 (* Title: HOL/Ordinals_and_Cardinals/Fun_More_Base.thy |
|
2 Author: Andrei Popescu, TU Muenchen |
|
3 Copyright 2012 |
|
4 |
|
5 More on injections, bijections and inverses (base). |
|
6 *) |
|
7 |
|
8 header {* More on Injections, Bijections and Inverses (Base) *} |
|
9 |
|
10 theory Fun_More_Base |
|
11 imports "~~/src/HOL/Library/Infinite_Set" |
|
12 begin |
|
13 |
|
14 |
|
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"}), |
|
17 mainly concerning injections, bijections, inverses and (numeric) cardinals of |
|
18 finite sets. *} |
|
19 |
|
20 |
|
21 subsection {* Purely functional properties *} |
|
22 |
|
23 |
|
24 (*2*)lemma bij_betw_id_iff: |
|
25 "(A = B) = (bij_betw id A B)" |
|
26 by(simp add: bij_betw_def) |
|
27 |
|
28 |
|
29 (*2*)lemma bij_betw_byWitness: |
|
30 assumes LEFT: "\<forall>a \<in> A. f'(f a) = a" and |
|
31 RIGHT: "\<forall>a' \<in> A'. f(f' a') = a'" and |
|
32 IM1: "f ` A \<le> A'" and IM2: "f' ` A' \<le> A" |
|
33 shows "bij_betw f A A'" |
|
34 using assms |
|
35 proof(unfold bij_betw_def inj_on_def, auto) |
|
36 fix a b assume *: "a \<in> A" "b \<in> A" and **: "f a = f b" |
|
37 have "a = f'(f a) \<and> b = f'(f b)" using * LEFT by simp |
|
38 with ** show "a = b" by simp |
|
39 next |
|
40 fix a' assume *: "a' \<in> A'" |
|
41 hence "f' a' \<in> A" using IM2 by blast |
|
42 moreover |
|
43 have "a' = f(f' a')" using * RIGHT by simp |
|
44 ultimately show "a' \<in> f ` A" by blast |
|
45 qed |
|
46 |
|
47 |
|
48 (*3*)corollary notIn_Un_bij_betw: |
|
49 assumes NIN: "b \<notin> A" and NIN': "f b \<notin> A'" and |
|
50 BIJ: "bij_betw f A A'" |
|
51 shows "bij_betw f (A \<union> {b}) (A' \<union> {f b})" |
|
52 proof- |
|
53 have "bij_betw f {b} {f b}" |
|
54 unfolding bij_betw_def inj_on_def by simp |
|
55 with assms show ?thesis |
|
56 using bij_betw_combine[of f A A' "{b}" "{f b}"] by blast |
|
57 qed |
|
58 |
|
59 |
|
60 (*1*)lemma notIn_Un_bij_betw3: |
|
61 assumes NIN: "b \<notin> A" and NIN': "f b \<notin> A'" |
|
62 shows "bij_betw f A A' = bij_betw f (A \<union> {b}) (A' \<union> {f b})" |
|
63 proof |
|
64 assume "bij_betw f A A'" |
|
65 thus "bij_betw f (A \<union> {b}) (A' \<union> {f b})" |
|
66 using assms notIn_Un_bij_betw[of b A f A'] by blast |
|
67 next |
|
68 assume *: "bij_betw f (A \<union> {b}) (A' \<union> {f b})" |
|
69 have "f ` A = A'" |
|
70 proof(auto) |
|
71 fix a assume **: "a \<in> A" |
|
72 hence "f a \<in> A' \<union> {f b}" using * unfolding bij_betw_def by blast |
|
73 moreover |
|
74 {assume "f a = f b" |
|
75 hence "a = b" using * ** unfolding bij_betw_def inj_on_def by blast |
|
76 with NIN ** have False by blast |
|
77 } |
|
78 ultimately show "f a \<in> A'" by blast |
|
79 next |
|
80 fix a' assume **: "a' \<in> A'" |
|
81 hence "a' \<in> f`(A \<union> {b})" |
|
82 using * by (auto simp add: bij_betw_def) |
|
83 then obtain a where 1: "a \<in> A \<union> {b} \<and> f a = a'" by blast |
|
84 moreover |
|
85 {assume "a = b" with 1 ** NIN' have False by blast |
|
86 } |
|
87 ultimately have "a \<in> A" by blast |
|
88 with 1 show "a' \<in> f ` A" by blast |
|
89 qed |
|
90 thus "bij_betw f A A'" using * bij_betw_subset[of f "A \<union> {b}" _ A] by blast |
|
91 qed |
|
92 |
|
93 |
|
94 subsection {* Properties involving finite and infinite sets *} |
|
95 |
|
96 |
|
97 (*3*)lemma inj_on_finite: |
|
98 assumes "inj_on f A" "f ` A \<le> B" "finite B" |
|
99 shows "finite A" |
|
100 using assms infinite_super by (fast dest: finite_imageD) |
|
101 |
|
102 |
|
103 (*3*)lemma infinite_imp_bij_betw: |
|
104 assumes INF: "infinite A" |
|
105 shows "\<exists>h. bij_betw h A (A - {a})" |
|
106 proof(cases "a \<in> A") |
|
107 assume Case1: "a \<notin> A" hence "A - {a} = A" by blast |
|
108 thus ?thesis using bij_betw_id[of A] by auto |
|
109 next |
|
110 assume Case2: "a \<in> A" |
|
111 have "infinite (A - {a})" using INF infinite_remove by auto |
|
112 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 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 have temp: "\<forall>y. f y \<noteq> a" using 2 by blast |
|
117 have 3: "inj_on g UNIV \<and> g ` UNIV \<le> A \<and> a \<in> g ` UNIV" |
|
118 proof(auto simp add: Case2 g_def, unfold inj_on_def, intro ballI impI, |
|
119 case_tac "x = 0", auto simp add: 2) |
|
120 fix y assume "a = (if y = 0 then a else f (Suc y))" |
|
121 thus "y = 0" using temp by (case_tac "y = 0", auto) |
|
122 next |
|
123 fix x y |
|
124 assume "f (Suc x) = (if y = 0 then a else f (Suc y))" |
|
125 thus "x = y" using 1 temp unfolding inj_on_def by (case_tac "y = 0", auto) |
|
126 next |
|
127 fix n show "f (Suc n) \<in> A" using 2 by blast |
|
128 qed |
|
129 hence 4: "bij_betw g UNIV A' \<and> a \<in> A' \<and> A' \<le> A" |
|
130 using inj_on_imp_bij_betw[of g] unfolding A'_def by auto |
|
131 hence 5: "bij_betw (inv g) A' UNIV" |
|
132 by (auto simp add: bij_betw_inv_into) |
|
133 (* *) |
|
134 obtain n where "g n = a" using 3 by auto |
|
135 hence 6: "bij_betw g (UNIV - {n}) (A' - {a})" |
|
136 using 3 4 unfolding A'_def |
|
137 by clarify (rule bij_betw_subset, auto simp: image_set_diff) |
|
138 (* *) |
|
139 obtain v where v_def: "v = (\<lambda> m. if m < n then m else Suc m)" by blast |
|
140 have 7: "bij_betw v UNIV (UNIV - {n})" |
|
141 proof(unfold bij_betw_def inj_on_def, intro conjI, clarify) |
|
142 fix m1 m2 assume "v m1 = v m2" |
|
143 thus "m1 = m2" |
|
144 by(case_tac "m1 < n", case_tac "m2 < n", |
|
145 auto simp add: inj_on_def v_def, case_tac "m2 < n", auto) |
|
146 next |
|
147 show "v ` UNIV = UNIV - {n}" |
|
148 proof(auto simp add: v_def) |
|
149 fix m assume *: "m \<noteq> n" and **: "m \<notin> Suc ` {m'. \<not> m' < n}" |
|
150 {assume "n \<le> m" with * have 71: "Suc n \<le> m" by auto |
|
151 then obtain m' where 72: "m = Suc m'" using Suc_le_D by auto |
|
152 with 71 have "n \<le> m'" by auto |
|
153 with 72 ** have False by auto |
|
154 } |
|
155 thus "m < n" by force |
|
156 qed |
|
157 qed |
|
158 (* *) |
|
159 obtain h' where h'_def: "h' = g o v o (inv g)" by blast |
|
160 hence 8: "bij_betw h' A' (A' - {a})" using 5 7 6 |
|
161 by (auto simp add: bij_betw_trans) |
|
162 (* *) |
|
163 obtain h where h_def: "h = (\<lambda> b. if b \<in> A' then h' b else b)" by blast |
|
164 have "\<forall>b \<in> A'. h b = h' b" unfolding h_def by auto |
|
165 hence "bij_betw h A' (A' - {a})" using 8 bij_betw_cong[of A' h] by auto |
|
166 moreover |
|
167 {have "\<forall>b \<in> A - A'. h b = b" unfolding h_def by auto |
|
168 hence "bij_betw h (A - A') (A - A')" |
|
169 using bij_betw_cong[of "A - A'" h id] bij_betw_id[of "A - A'"] by auto |
|
170 } |
|
171 moreover |
|
172 have "(A' Int (A - A') = {} \<and> A' \<union> (A - A') = A) \<and> |
|
173 ((A' - {a}) Int (A - A') = {} \<and> (A' - {a}) \<union> (A - A') = A - {a})" |
|
174 using 4 by blast |
|
175 ultimately have "bij_betw h A (A - {a})" |
|
176 using bij_betw_combine[of h A' "A' - {a}" "A - A'" "A - A'"] by simp |
|
177 thus ?thesis by blast |
|
178 qed |
|
179 |
|
180 |
|
181 (*3*)lemma infinite_imp_bij_betw2: |
|
182 assumes INF: "infinite A" |
|
183 shows "\<exists>h. bij_betw h A (A \<union> {a})" |
|
184 proof(cases "a \<in> A") |
|
185 assume Case1: "a \<in> A" hence "A \<union> {a} = A" by blast |
|
186 thus ?thesis using bij_betw_id[of A] by auto |
|
187 next |
|
188 let ?A' = "A \<union> {a}" |
|
189 assume Case2: "a \<notin> A" hence "A = ?A' - {a}" by blast |
|
190 moreover have "infinite ?A'" using INF by auto |
|
191 ultimately obtain f where "bij_betw f ?A' A" |
|
192 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 thus ?thesis by auto |
|
195 qed |
|
196 |
|
197 |
|
198 subsection {* Properties involving Hilbert choice *} |
|
199 |
|
200 |
|
201 (*2*)lemma bij_betw_inv_into_left: |
|
202 assumes BIJ: "bij_betw f A A'" and IN: "a \<in> A" |
|
203 shows "(inv_into A f) (f a) = a" |
|
204 using assms unfolding bij_betw_def |
|
205 by clarify (rule inv_into_f_f) |
|
206 |
|
207 (*2*)lemma bij_betw_inv_into_right: |
|
208 assumes "bij_betw f A A'" "a' \<in> A'" |
|
209 shows "f(inv_into A f a') = a'" |
|
210 using assms unfolding bij_betw_def using f_inv_into_f by force |
|
211 |
|
212 |
|
213 (*1*)lemma bij_betw_inv_into_LEFT: |
|
214 assumes BIJ: "bij_betw f A A'" and SUB: "B \<le> A" |
|
215 shows "(inv_into A f)`(f ` B) = B" |
|
216 using assms unfolding bij_betw_def using inv_into_image_cancel by force |
|
217 |
|
218 |
|
219 (*1*)lemma bij_betw_inv_into_LEFT_RIGHT: |
|
220 assumes BIJ: "bij_betw f A A'" and SUB: "B \<le> A" and |
|
221 IM: "f ` B = B'" |
|
222 shows "(inv_into A f) ` B' = B" |
|
223 using assms bij_betw_inv_into_LEFT[of f A A' B] by fast |
|
224 |
|
225 |
|
226 (*1*)lemma bij_betw_inv_into_subset: |
|
227 assumes BIJ: "bij_betw f A A'" and |
|
228 SUB: "B \<le> A" and IM: "f ` B = B'" |
|
229 shows "bij_betw (inv_into A f) B' B" |
|
230 using assms unfolding bij_betw_def |
|
231 by (auto intro: inj_on_inv_into) |
|
232 |
|
233 |
|
234 subsection {* Other facts *} |
|
235 |
|
236 |
|
237 (*2*)lemma atLeastLessThan_less_eq: |
|
238 "({0..<m} \<le> {0..<n}) = ((m::nat) \<le> n)" |
|
239 unfolding ivl_subset by arith |
|
240 |
|
241 |
|
242 (*2*)lemma atLeastLessThan_less_eq2: |
|
243 assumes "inj_on f {0..<(m::nat)} \<and> f ` {0..<m} \<le> {0..<n}" |
|
244 shows "m \<le> n" |
|
245 using assms |
|
246 using finite_atLeastLessThan[of m] finite_atLeastLessThan[of n] |
|
247 card_atLeastLessThan[of m] card_atLeastLessThan[of n] |
|
248 card_inj_on_le[of f "{0 ..< m}" "{0 ..< n}"] by auto |
|
249 |
|
250 |
|
251 |
|
252 end |
|