1 (* Title: HOL/Ordinals_and_Cardinals/Fun_More.thy |
|
2 Author: Andrei Popescu, TU Muenchen |
|
3 Copyright 2012 |
|
4 |
|
5 More on injections, bijections and inverses. |
|
6 *) |
|
7 |
|
8 header {* More on Injections, Bijections and Inverses *} |
|
9 |
|
10 theory Fun_More |
|
11 imports Fun_More_Base |
|
12 begin |
|
13 |
|
14 |
|
15 subsection {* Purely functional properties *} |
|
16 |
|
17 (* unused *) |
|
18 (*1*)lemma notIn_Un_bij_betw2: |
|
19 assumes NIN: "b \<notin> A" and NIN': "b' \<notin> A'" and |
|
20 BIJ: "bij_betw f A A'" |
|
21 shows "bij_betw f (A \<union> {b}) (A' \<union> {b'}) = (f b = b')" |
|
22 proof |
|
23 assume "f b = b'" |
|
24 thus "bij_betw f (A \<union> {b}) (A' \<union> {b'})" |
|
25 using assms notIn_Un_bij_betw[of b A f A'] by auto |
|
26 next |
|
27 assume *: "bij_betw f (A \<union> {b}) (A' \<union> {b'})" |
|
28 hence "f b \<in> A' \<union> {b'}" |
|
29 unfolding bij_betw_def by auto |
|
30 moreover |
|
31 {assume "f b \<in> A'" |
|
32 then obtain b1 where 1: "b1 \<in> A" and 2: "f b1 = f b" using BIJ |
|
33 by (auto simp add: bij_betw_def) |
|
34 hence "b = b1" using * |
|
35 by (auto simp add: bij_betw_def inj_on_def) |
|
36 with 1 NIN have False by auto |
|
37 } |
|
38 ultimately show "f b = b'" by blast |
|
39 qed |
|
40 |
|
41 (* unused *) |
|
42 (*1*)lemma bij_betw_ball: |
|
43 assumes BIJ: "bij_betw f A B" |
|
44 shows "(\<forall>b \<in> B. phi b) = (\<forall>a \<in> A. phi(f a))" |
|
45 using assms unfolding bij_betw_def inj_on_def by blast |
|
46 |
|
47 (* unused *) |
|
48 (*1*)lemma bij_betw_diff_singl: |
|
49 assumes BIJ: "bij_betw f A A'" and IN: "a \<in> A" |
|
50 shows "bij_betw f (A - {a}) (A' - {f a})" |
|
51 proof- |
|
52 let ?B = "A - {a}" let ?B' = "A' - {f a}" |
|
53 have "f a \<in> A'" using IN BIJ unfolding bij_betw_def by blast |
|
54 hence "a \<notin> ?B \<and> f a \<notin> ?B' \<and> A = ?B \<union> {a} \<and> A' = ?B' \<union> {f a}" |
|
55 using IN by blast |
|
56 thus ?thesis using notIn_Un_bij_betw3[of a ?B f ?B'] BIJ by simp |
|
57 qed |
|
58 |
|
59 |
|
60 subsection {* Properties involving finite and infinite sets *} |
|
61 |
|
62 (*3*)lemma inj_on_image_Pow: |
|
63 assumes "inj_on f A" |
|
64 shows "inj_on (image f) (Pow A)" |
|
65 unfolding Pow_def inj_on_def proof(clarsimp) |
|
66 fix X Y assume *: "X \<le> A" and **: "Y \<le> A" and |
|
67 ***: "f ` X = f ` Y" |
|
68 show "X = Y" |
|
69 proof(auto) |
|
70 fix x assume ****: "x \<in> X" |
|
71 with *** obtain y where "y \<in> Y \<and> f x = f y" by blast |
|
72 with **** * ** assms show "x \<in> Y" |
|
73 unfolding inj_on_def by auto |
|
74 next |
|
75 fix y assume ****: "y \<in> Y" |
|
76 with *** obtain x where "x \<in> X \<and> f x = f y" by force |
|
77 with **** * ** assms show "y \<in> X" |
|
78 unfolding inj_on_def by auto |
|
79 qed |
|
80 qed |
|
81 |
|
82 (*2*)lemma bij_betw_image_Pow: |
|
83 assumes "bij_betw f A B" |
|
84 shows "bij_betw (image f) (Pow A) (Pow B)" |
|
85 using assms unfolding bij_betw_def |
|
86 by (auto simp add: inj_on_image_Pow image_Pow_surj) |
|
87 |
|
88 (* unused *) |
|
89 (*1*)lemma bij_betw_inv_into_RIGHT: |
|
90 assumes BIJ: "bij_betw f A A'" and SUB: "B' \<le> A'" |
|
91 shows "f `((inv_into A f)`B') = B'" |
|
92 using assms |
|
93 proof(auto simp add: bij_betw_inv_into_right) |
|
94 let ?f' = "(inv_into A f)" |
|
95 fix a' assume *: "a' \<in> B'" |
|
96 hence "a' \<in> A'" using SUB by auto |
|
97 hence "a' = f (?f' a')" |
|
98 using BIJ by (auto simp add: bij_betw_inv_into_right) |
|
99 thus "a' \<in> f ` (?f' ` B')" using * by blast |
|
100 qed |
|
101 |
|
102 (* unused *) |
|
103 (*1*)lemma bij_betw_inv_into_RIGHT_LEFT: |
|
104 assumes BIJ: "bij_betw f A A'" and SUB: "B' \<le> A'" and |
|
105 IM: "(inv_into A f) ` B' = B" |
|
106 shows "f ` B = B'" |
|
107 proof- |
|
108 have "f`((inv_into A f)` B') = B'" |
|
109 using assms bij_betw_inv_into_RIGHT[of f A A' B'] by auto |
|
110 thus ?thesis using IM by auto |
|
111 qed |
|
112 |
|
113 (* unused *) |
|
114 (*2*)lemma bij_betw_inv_into_twice: |
|
115 assumes "bij_betw f A A'" |
|
116 shows "\<forall>a \<in> A. inv_into A' (inv_into A f) a = f a" |
|
117 proof |
|
118 let ?f' = "inv_into A f" let ?f'' = "inv_into A' ?f'" |
|
119 have 1: "bij_betw ?f' A' A" using assms |
|
120 by (auto simp add: bij_betw_inv_into) |
|
121 fix a assume *: "a \<in> A" |
|
122 then obtain a' where 2: "a' \<in> A'" and 3: "?f' a' = a" |
|
123 using 1 unfolding bij_betw_def by force |
|
124 hence "?f'' a = a'" |
|
125 using * 1 3 by (auto simp add: bij_betw_inv_into_left) |
|
126 moreover have "f a = a'" using assms 2 3 |
|
127 by (auto simp add: bij_betw_inv_into_right) |
|
128 ultimately show "?f'' a = f a" by simp |
|
129 qed |
|
130 |
|
131 |
|
132 subsection {* Properties involving Hilbert choice *} |
|
133 |
|
134 |
|
135 subsection {* Other facts *} |
|
136 |
|
137 (*3*)lemma atLeastLessThan_injective: |
|
138 assumes "{0 ..< m::nat} = {0 ..< n}" |
|
139 shows "m = n" |
|
140 proof- |
|
141 {assume "m < n" |
|
142 hence "m \<in> {0 ..< n}" by auto |
|
143 hence "{0 ..< m} < {0 ..< n}" by auto |
|
144 hence False using assms by blast |
|
145 } |
|
146 moreover |
|
147 {assume "n < m" |
|
148 hence "n \<in> {0 ..< m}" by auto |
|
149 hence "{0 ..< n} < {0 ..< m}" by auto |
|
150 hence False using assms by blast |
|
151 } |
|
152 ultimately show ?thesis by force |
|
153 qed |
|
154 |
|
155 (*2*)lemma atLeastLessThan_injective2: |
|
156 "bij_betw f {0 ..< m::nat} {0 ..< n} \<Longrightarrow> m = n" |
|
157 using finite_atLeastLessThan[of m] finite_atLeastLessThan[of n] |
|
158 card_atLeastLessThan[of m] card_atLeastLessThan[of n] |
|
159 bij_betw_iff_card[of "{0 ..< m}" "{0 ..< n}"] by auto |
|
160 |
|
161 (* unused *) |
|
162 (*2*)lemma atLeastLessThan_less_eq3: |
|
163 "(\<exists>f. inj_on f {0..<(m::nat)} \<and> f ` {0..<m} \<le> {0..<n}) = (m \<le> n)" |
|
164 using atLeastLessThan_less_eq2 |
|
165 proof(auto) |
|
166 assume "m \<le> n" |
|
167 hence "inj_on id {0..<m} \<and> id ` {0..<m} \<subseteq> {0..<n}" unfolding inj_on_def by force |
|
168 thus "\<exists>f. inj_on f {0..<m} \<and> f ` {0..<m} \<subseteq> {0..<n}" by blast |
|
169 qed |
|
170 |
|
171 (* unused *) |
|
172 (*3*)lemma atLeastLessThan_less: |
|
173 "({0..<m} < {0..<n}) = ((m::nat) < n)" |
|
174 proof- |
|
175 have "({0..<m} < {0..<n}) = ({0..<m} \<le> {0..<n} \<and> {0..<m} ~= {0..<n})" |
|
176 using subset_iff_psubset_eq by blast |
|
177 also have "\<dots> = (m \<le> n \<and> m ~= n)" |
|
178 using atLeastLessThan_less_eq atLeastLessThan_injective by blast |
|
179 also have "\<dots> = (m < n)" by auto |
|
180 finally show ?thesis . |
|
181 qed |
|
182 |
|
183 end |
|