equal
deleted
inserted
replaced
40 apply (rule natLeq_Card_order) |
40 apply (rule natLeq_Card_order) |
41 apply (rule card_of_Card_order) |
41 apply (rule card_of_Card_order) |
42 apply (rule cexp_mono1) |
42 apply (rule cexp_mono1) |
43 apply (rule ordLeq_csum1) |
43 apply (rule ordLeq_csum1) |
44 apply (rule card_of_Card_order) |
44 apply (rule card_of_Card_order) |
45 apply (rule disjI2) |
|
46 apply (rule cone_ordLeq_cexp) |
|
47 apply (rule ordLeq_transitive) |
|
48 apply (rule cone_ordLeq_ctwo) |
|
49 apply (rule ordLeq_csum2) |
|
50 apply (rule Card_order_ctwo) |
|
51 apply (rule natLeq_Card_order) |
45 apply (rule natLeq_Card_order) |
52 done |
46 done |
53 |
47 |
54 bnf_def DEADID: "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"] |
48 bnf_def DEADID: "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"] |
55 "op =::'a \<Rightarrow> 'a \<Rightarrow> bool" |
49 "op =::'a \<Rightarrow> 'a \<Rightarrow> bool" |
275 apply (rule ordLeq_cprod1) |
269 apply (rule ordLeq_cprod1) |
276 apply (rule Card_order_ctwo) |
270 apply (rule Card_order_ctwo) |
277 apply (rule Cinfinite_Cnotzero) |
271 apply (rule Cinfinite_Cnotzero) |
278 apply (rule conjI[OF _ natLeq_Card_order]) |
272 apply (rule conjI[OF _ natLeq_Card_order]) |
279 apply (rule natLeq_cinfinite) |
273 apply (rule natLeq_cinfinite) |
280 apply (rule disjI2) |
|
281 apply (rule cone_ordLeq_cexp) |
|
282 apply (rule ordLeq_transitive) |
|
283 apply (rule cone_ordLeq_ctwo) |
|
284 apply (rule ordLeq_csum2) |
|
285 apply (rule Card_order_ctwo) |
|
286 apply (rule notE) |
274 apply (rule notE) |
287 apply (rule ctwo_not_czero) |
275 apply (rule ctwo_not_czero) |
288 apply assumption |
276 apply assumption |
289 by (rule Card_order_ctwo) |
277 by (rule Card_order_ctwo) |
290 next |
278 next |
376 also have "|B| ^c |UNIV :: 'd set| \<le>o |
364 also have "|B| ^c |UNIV :: 'd set| \<le>o |
377 ( |B| +c ctwo) ^c (natLeq +c |UNIV :: 'd set| )" |
365 ( |B| +c ctwo) ^c (natLeq +c |UNIV :: 'd set| )" |
378 apply (rule cexp_mono) |
366 apply (rule cexp_mono) |
379 apply (rule ordLeq_csum1) apply (rule card_of_Card_order) |
367 apply (rule ordLeq_csum1) apply (rule card_of_Card_order) |
380 apply (rule ordLeq_csum2) apply (rule card_of_Card_order) |
368 apply (rule ordLeq_csum2) apply (rule card_of_Card_order) |
381 apply (rule disjI2) apply (rule cone_ordLeq_cexp) |
|
382 apply (rule ordLeq_transitive) apply (rule cone_ordLeq_ctwo) apply (rule ordLeq_csum2) |
|
383 apply (rule Card_order_ctwo) |
|
384 apply (rule notE) apply (rule conjunct1) apply (rule Cnotzero_UNIV) apply blast |
369 apply (rule notE) apply (rule conjunct1) apply (rule Cnotzero_UNIV) apply blast |
385 apply (rule card_of_Card_order) |
370 apply (rule card_of_Card_order) |
386 done |
371 done |
387 finally |
372 finally |
388 show "|{f::'d => 'a. range f \<subseteq> B}| \<le>o |
373 show "|{f::'d => 'a. range f \<subseteq> B}| \<le>o |