1 (* Title: HOL/Cardinals/Fun_More_FP.thy |
|
2 Author: Andrei Popescu, TU Muenchen |
|
3 Copyright 2012 |
|
4 |
|
5 More on injections, bijections and inverses (FP). |
|
6 *) |
|
7 |
|
8 header {* More on Injections, Bijections and Inverses (FP) *} |
|
9 |
|
10 theory Fun_More_FP |
|
11 imports Hilbert_Choice |
|
12 begin |
|
13 |
|
14 |
|
15 text {* This section proves more facts (additional to those in @{text "Fun.thy"}, |
|
16 @{text "Hilbert_Choice.thy"}, and @{text "Finite_Set.thy"}), |
|
17 mainly concerning injections, bijections, inverses and (numeric) cardinals of |
|
18 finite sets. *} |
|
19 |
|
20 |
|
21 subsection {* Properties involving finite and infinite sets *} |
|
22 |
|
23 |
|
24 lemma inj_on_finite: |
|
25 assumes "inj_on f A" "f ` A \<le> B" "finite B" |
|
26 shows "finite A" |
|
27 using assms by (metis finite_imageD finite_subset) |
|
28 |
|
29 |
|
30 lemma infinite_imp_bij_betw: |
|
31 assumes INF: "\<not> finite A" |
|
32 shows "\<exists>h. bij_betw h A (A - {a})" |
|
33 proof(cases "a \<in> A") |
|
34 assume Case1: "a \<notin> A" hence "A - {a} = A" by blast |
|
35 thus ?thesis using bij_betw_id[of A] by auto |
|
36 next |
|
37 assume Case2: "a \<in> A" |
|
38 find_theorems "\<not> finite _" |
|
39 have "\<not> finite (A - {a})" using INF by auto |
|
40 with infinite_iff_countable_subset[of "A - {a}"] obtain f::"nat \<Rightarrow> 'a" |
|
41 where 1: "inj f" and 2: "f ` UNIV \<le> A - {a}" by blast |
|
42 obtain g where g_def: "g = (\<lambda> n. if n = 0 then a else f (Suc n))" by blast |
|
43 obtain A' where A'_def: "A' = g ` UNIV" by blast |
|
44 have temp: "\<forall>y. f y \<noteq> a" using 2 by blast |
|
45 have 3: "inj_on g UNIV \<and> g ` UNIV \<le> A \<and> a \<in> g ` UNIV" |
|
46 proof(auto simp add: Case2 g_def, unfold inj_on_def, intro ballI impI, |
|
47 case_tac "x = 0", auto simp add: 2) |
|
48 fix y assume "a = (if y = 0 then a else f (Suc y))" |
|
49 thus "y = 0" using temp by (case_tac "y = 0", auto) |
|
50 next |
|
51 fix x y |
|
52 assume "f (Suc x) = (if y = 0 then a else f (Suc y))" |
|
53 thus "x = y" using 1 temp unfolding inj_on_def by (case_tac "y = 0", auto) |
|
54 next |
|
55 fix n show "f (Suc n) \<in> A" using 2 by blast |
|
56 qed |
|
57 hence 4: "bij_betw g UNIV A' \<and> a \<in> A' \<and> A' \<le> A" |
|
58 using inj_on_imp_bij_betw[of g] unfolding A'_def by auto |
|
59 hence 5: "bij_betw (inv g) A' UNIV" |
|
60 by (auto simp add: bij_betw_inv_into) |
|
61 (* *) |
|
62 obtain n where "g n = a" using 3 by auto |
|
63 hence 6: "bij_betw g (UNIV - {n}) (A' - {a})" |
|
64 using 3 4 unfolding A'_def |
|
65 by clarify (rule bij_betw_subset, auto simp: image_set_diff) |
|
66 (* *) |
|
67 obtain v where v_def: "v = (\<lambda> m. if m < n then m else Suc m)" by blast |
|
68 have 7: "bij_betw v UNIV (UNIV - {n})" |
|
69 proof(unfold bij_betw_def inj_on_def, intro conjI, clarify) |
|
70 fix m1 m2 assume "v m1 = v m2" |
|
71 thus "m1 = m2" |
|
72 by(case_tac "m1 < n", case_tac "m2 < n", |
|
73 auto simp add: inj_on_def v_def, case_tac "m2 < n", auto) |
|
74 next |
|
75 show "v ` UNIV = UNIV - {n}" |
|
76 proof(auto simp add: v_def) |
|
77 fix m assume *: "m \<noteq> n" and **: "m \<notin> Suc ` {m'. \<not> m' < n}" |
|
78 {assume "n \<le> m" with * have 71: "Suc n \<le> m" by auto |
|
79 then obtain m' where 72: "m = Suc m'" using Suc_le_D by auto |
|
80 with 71 have "n \<le> m'" by auto |
|
81 with 72 ** have False by auto |
|
82 } |
|
83 thus "m < n" by force |
|
84 qed |
|
85 qed |
|
86 (* *) |
|
87 obtain h' where h'_def: "h' = g o v o (inv g)" by blast |
|
88 hence 8: "bij_betw h' A' (A' - {a})" using 5 7 6 |
|
89 by (auto simp add: bij_betw_trans) |
|
90 (* *) |
|
91 obtain h where h_def: "h = (\<lambda> b. if b \<in> A' then h' b else b)" by blast |
|
92 have "\<forall>b \<in> A'. h b = h' b" unfolding h_def by auto |
|
93 hence "bij_betw h A' (A' - {a})" using 8 bij_betw_cong[of A' h] by auto |
|
94 moreover |
|
95 {have "\<forall>b \<in> A - A'. h b = b" unfolding h_def by auto |
|
96 hence "bij_betw h (A - A') (A - A')" |
|
97 using bij_betw_cong[of "A - A'" h id] bij_betw_id[of "A - A'"] by auto |
|
98 } |
|
99 moreover |
|
100 have "(A' Int (A - A') = {} \<and> A' \<union> (A - A') = A) \<and> |
|
101 ((A' - {a}) Int (A - A') = {} \<and> (A' - {a}) \<union> (A - A') = A - {a})" |
|
102 using 4 by blast |
|
103 ultimately have "bij_betw h A (A - {a})" |
|
104 using bij_betw_combine[of h A' "A' - {a}" "A - A'" "A - A'"] by simp |
|
105 thus ?thesis by blast |
|
106 qed |
|
107 |
|
108 |
|
109 lemma infinite_imp_bij_betw2: |
|
110 assumes INF: "\<not> finite A" |
|
111 shows "\<exists>h. bij_betw h A (A \<union> {a})" |
|
112 proof(cases "a \<in> A") |
|
113 assume Case1: "a \<in> A" hence "A \<union> {a} = A" by blast |
|
114 thus ?thesis using bij_betw_id[of A] by auto |
|
115 next |
|
116 let ?A' = "A \<union> {a}" |
|
117 assume Case2: "a \<notin> A" hence "A = ?A' - {a}" by blast |
|
118 moreover have "\<not> finite ?A'" using INF by auto |
|
119 ultimately obtain f where "bij_betw f ?A' A" |
|
120 using infinite_imp_bij_betw[of ?A' a] by auto |
|
121 hence "bij_betw(inv_into ?A' f) A ?A'" using bij_betw_inv_into by blast |
|
122 thus ?thesis by auto |
|
123 qed |
|
124 |
|
125 |
|
126 subsection {* Properties involving Hilbert choice *} |
|
127 |
|
128 |
|
129 lemma bij_betw_inv_into_left: |
|
130 assumes BIJ: "bij_betw f A A'" and IN: "a \<in> A" |
|
131 shows "(inv_into A f) (f a) = a" |
|
132 using assms unfolding bij_betw_def |
|
133 by clarify (rule inv_into_f_f) |
|
134 |
|
135 lemma bij_betw_inv_into_right: |
|
136 assumes "bij_betw f A A'" "a' \<in> A'" |
|
137 shows "f(inv_into A f a') = a'" |
|
138 using assms unfolding bij_betw_def using f_inv_into_f by force |
|
139 |
|
140 |
|
141 lemma bij_betw_inv_into_subset: |
|
142 assumes BIJ: "bij_betw f A A'" and |
|
143 SUB: "B \<le> A" and IM: "f ` B = B'" |
|
144 shows "bij_betw (inv_into A f) B' B" |
|
145 using assms unfolding bij_betw_def |
|
146 by (auto intro: inj_on_inv_into) |
|
147 |
|
148 |
|
149 |
|
150 end |
|