equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 header {* More on Injections, Bijections and Inverses *} |
8 header {* More on Injections, Bijections and Inverses *} |
9 |
9 |
10 theory Fun_More |
10 theory Fun_More |
11 imports Fun_More_FP |
11 imports Fun_More_FP Main |
12 begin |
12 begin |
13 |
13 |
14 |
14 |
15 subsection {* Purely functional properties *} |
15 subsection {* Purely functional properties *} |
16 |
16 |
168 "bij_betw f {0 ..< m::nat} {0 ..< n} \<Longrightarrow> m = n" |
168 "bij_betw f {0 ..< m::nat} {0 ..< n} \<Longrightarrow> m = n" |
169 using finite_atLeastLessThan[of m] finite_atLeastLessThan[of n] |
169 using finite_atLeastLessThan[of m] finite_atLeastLessThan[of n] |
170 card_atLeastLessThan[of m] card_atLeastLessThan[of n] |
170 card_atLeastLessThan[of m] card_atLeastLessThan[of n] |
171 bij_betw_iff_card[of "{0 ..< m}" "{0 ..< n}"] by auto |
171 bij_betw_iff_card[of "{0 ..< m}" "{0 ..< n}"] by auto |
172 |
172 |
|
173 |
|
174 (*2*)lemma atLeastLessThan_less_eq: |
|
175 "({0..<m} \<le> {0..<n}) = ((m::nat) \<le> n)" |
|
176 unfolding ivl_subset by arith |
|
177 |
|
178 |
|
179 (*2*)lemma atLeastLessThan_less_eq2: |
|
180 assumes "inj_on f {0..<(m::nat)} \<and> f ` {0..<m} \<le> {0..<n}" |
|
181 shows "m \<le> n" |
|
182 using assms |
|
183 using finite_atLeastLessThan[of m] finite_atLeastLessThan[of n] |
|
184 card_atLeastLessThan[of m] card_atLeastLessThan[of n] |
|
185 card_inj_on_le[of f "{0 ..< m}" "{0 ..< n}"] by fastforce |
|
186 |
173 (* unused *) |
187 (* unused *) |
174 (*2*)lemma atLeastLessThan_less_eq3: |
188 (*2*)lemma atLeastLessThan_less_eq3: |
175 "(\<exists>f. inj_on f {0..<(m::nat)} \<and> f ` {0..<m} \<le> {0..<n}) = (m \<le> n)" |
189 "(\<exists>f. inj_on f {0..<(m::nat)} \<and> f ` {0..<m} \<le> {0..<n}) = (m \<le> n)" |
176 using atLeastLessThan_less_eq2 |
190 using atLeastLessThan_less_eq2 |
177 proof(auto) |
191 proof(auto) |