9 |
9 |
10 theory Cardinal_Arithmetic_FP |
10 theory Cardinal_Arithmetic_FP |
11 imports Cardinal_Order_Relation_FP |
11 imports Cardinal_Order_Relation_FP |
12 begin |
12 begin |
13 |
13 |
14 (*library candidate*) |
|
15 lemma dir_image: "\<lbrakk>\<And>x y. (f x = f y) = (x = y); Card_order r\<rbrakk> \<Longrightarrow> r =o dir_image r f" |
14 lemma dir_image: "\<lbrakk>\<And>x y. (f x = f y) = (x = y); Card_order r\<rbrakk> \<Longrightarrow> r =o dir_image r f" |
16 by (rule dir_image_ordIso) (auto simp add: inj_on_def card_order_on_def) |
15 by (rule dir_image_ordIso) (auto simp add: inj_on_def card_order_on_def) |
17 |
16 |
18 (*should supersede a weaker lemma from the library*) |
17 (*should supersede a weaker lemma from the library*) |
19 lemma dir_image_Field: "Field (dir_image r f) = f ` Field r" |
18 lemma dir_image_Field: "Field (dir_image r f) = f ` Field r" |
29 with co have "Card_order (dir_image r f)" |
28 with co have "Card_order (dir_image r f)" |
30 using card_order_on_Card_order[of UNIV r] Card_order_ordIso2[OF _ dir_image] by blast |
29 using card_order_on_Card_order[of UNIV r] Card_order_ordIso2[OF _ dir_image] by blast |
31 ultimately show ?thesis by auto |
30 ultimately show ?thesis by auto |
32 qed |
31 qed |
33 |
32 |
34 (*library candidate*) |
|
35 lemma ordIso_refl: "Card_order r \<Longrightarrow> r =o r" |
33 lemma ordIso_refl: "Card_order r \<Longrightarrow> r =o r" |
36 by (rule card_order_on_ordIso) |
34 by (rule card_order_on_ordIso) |
37 |
35 |
38 (*library candidate*) |
|
39 lemma ordLeq_refl: "Card_order r \<Longrightarrow> r \<le>o r" |
36 lemma ordLeq_refl: "Card_order r \<Longrightarrow> r \<le>o r" |
40 by (rule ordIso_imp_ordLeq, rule card_order_on_ordIso) |
37 by (rule ordIso_imp_ordLeq, rule card_order_on_ordIso) |
41 |
38 |
42 (*library candidate*) |
|
43 lemma card_of_ordIso_subst: "A = B \<Longrightarrow> |A| =o |B|" |
39 lemma card_of_ordIso_subst: "A = B \<Longrightarrow> |A| =o |B|" |
44 by (simp only: ordIso_refl card_of_Card_order) |
40 by (simp only: ordIso_refl card_of_Card_order) |
45 |
41 |
46 (*library candidate*) |
|
47 lemma Field_card_order: "card_order r \<Longrightarrow> Field r = UNIV" |
42 lemma Field_card_order: "card_order r \<Longrightarrow> Field r = UNIV" |
48 using card_order_on_Card_order[of UNIV r] by simp |
43 using card_order_on_Card_order[of UNIV r] by simp |
49 |
44 |
50 (*library candidate*) |
|
51 lemma card_of_Times_Plus_distrib: |
45 lemma card_of_Times_Plus_distrib: |
52 "|A <*> (B <+> C)| =o |A <*> B <+> A <*> C|" (is "|?RHS| =o |?LHS|") |
46 "|A <*> (B <+> C)| =o |A <*> B <+> A <*> C|" (is "|?RHS| =o |?LHS|") |
53 proof - |
47 proof - |
54 let ?f = "\<lambda>(a, bc). case bc of Inl b \<Rightarrow> Inl (a, b) | Inr c \<Rightarrow> Inr (a, c)" |
48 let ?f = "\<lambda>(a, bc). case bc of Inl b \<Rightarrow> Inl (a, b) | Inr c \<Rightarrow> Inr (a, c)" |
55 have "bij_betw ?f ?RHS ?LHS" unfolding bij_betw_def inj_on_def by force |
49 have "bij_betw ?f ?RHS ?LHS" unfolding bij_betw_def inj_on_def by force |
56 thus ?thesis using card_of_ordIso by blast |
50 thus ?thesis using card_of_ordIso by blast |
57 qed |
51 qed |
58 |
52 |
59 (*library candidate*) |
|
60 lemma Func_Times_Range: |
53 lemma Func_Times_Range: |
61 "|Func A (B <*> C)| =o |Func A B <*> Func A C|" (is "|?LHS| =o |?RHS|") |
54 "|Func A (B <*> C)| =o |Func A B <*> Func A C|" (is "|?LHS| =o |?RHS|") |
62 proof - |
55 proof - |
63 let ?F = "\<lambda>fg. (\<lambda>x. if x \<in> A then fst (fg x) else undefined, |
56 let ?F = "\<lambda>fg. (\<lambda>x. if x \<in> A then fst (fg x) else undefined, |
64 \<lambda>x. if x \<in> A then snd (fg x) else undefined)" |
57 \<lambda>x. if x \<in> A then snd (fg x) else undefined)" |
275 |
268 |
276 lemma cone_ordLeq_Cnotzero: "Cnotzero r \<Longrightarrow> cone \<le>o r" |
269 lemma cone_ordLeq_Cnotzero: "Cnotzero r \<Longrightarrow> cone \<le>o r" |
277 unfolding cone_def by (metis Card_order_singl_ordLeq czeroI) |
270 unfolding cone_def by (metis Card_order_singl_ordLeq czeroI) |
278 |
271 |
279 |
272 |
280 subsection{* Two *} |
273 subsection {* Two *} |
281 |
274 |
282 definition ctwo where |
275 definition ctwo where |
283 "ctwo = |UNIV :: bool set|" |
276 "ctwo = |UNIV :: bool set|" |
284 |
277 |
285 lemma Card_order_ctwo: "Card_order ctwo" |
278 lemma Card_order_ctwo: "Card_order ctwo" |