equal
deleted
inserted
replaced
4 Copyright 2012 |
4 Copyright 2012 |
5 |
5 |
6 Type of (at most) countable sets. |
6 Type of (at most) countable sets. |
7 *) |
7 *) |
8 |
8 |
9 section {* Type of (at Most) Countable Sets *} |
9 section \<open>Type of (at Most) Countable Sets\<close> |
10 |
10 |
11 theory Countable_Set_Type |
11 theory Countable_Set_Type |
12 imports Countable_Set Cardinal_Notations Conditionally_Complete_Lattices |
12 imports Countable_Set Cardinal_Notations Conditionally_Complete_Lattices |
13 begin |
13 begin |
14 |
14 |
15 |
15 |
16 subsection{* Cardinal stuff *} |
16 subsection\<open>Cardinal stuff\<close> |
17 |
17 |
18 lemma countable_card_of_nat: "countable A \<longleftrightarrow> |A| \<le>o |UNIV::nat set|" |
18 lemma countable_card_of_nat: "countable A \<longleftrightarrow> |A| \<le>o |UNIV::nat set|" |
19 unfolding countable_def card_of_ordLeq[symmetric] by auto |
19 unfolding countable_def card_of_ordLeq[symmetric] by auto |
20 |
20 |
21 lemma countable_card_le_natLeq: "countable A \<longleftrightarrow> |A| \<le>o natLeq" |
21 lemma countable_card_le_natLeq: "countable A \<longleftrightarrow> |A| \<le>o natLeq" |
52 lemma countable_ordLess: |
52 lemma countable_ordLess: |
53 assumes AB: "|A| <o |B|" and B: "countable B" |
53 assumes AB: "|A| <o |B|" and B: "countable B" |
54 shows "countable A" |
54 shows "countable A" |
55 using countable_ordLeq[OF ordLess_imp_ordLeq[OF AB] B] . |
55 using countable_ordLeq[OF ordLess_imp_ordLeq[OF AB] B] . |
56 |
56 |
57 subsection {* The type of countable sets *} |
57 subsection \<open>The type of countable sets\<close> |
58 |
58 |
59 typedef 'a cset = "{A :: 'a set. countable A}" morphisms rcset acset |
59 typedef 'a cset = "{A :: 'a set. countable A}" morphisms rcset acset |
60 by (rule exI[of _ "{}"]) simp |
60 by (rule exI[of _ "{}"]) simp |
61 |
61 |
62 setup_lifting type_definition_cset |
62 setup_lifting type_definition_cset |
364 lemmas cUn_eq_cUN = Un_eq_UN[Transfer.transferred] |
364 lemmas cUn_eq_cUN = Un_eq_UN[Transfer.transferred] |
365 lemmas cUN_mono = UN_mono[Transfer.transferred] |
365 lemmas cUN_mono = UN_mono[Transfer.transferred] |
366 lemmas cimage_cUN = image_UN[Transfer.transferred] |
366 lemmas cimage_cUN = image_UN[Transfer.transferred] |
367 lemmas cUN_csingleton [simp] = UN_singleton[Transfer.transferred] |
367 lemmas cUN_csingleton [simp] = UN_singleton[Transfer.transferred] |
368 |
368 |
369 subsection {* Additional lemmas*} |
369 subsection \<open>Additional lemmas\<close> |
370 |
370 |
371 subsubsection {* @{text cempty} *} |
371 subsubsection \<open>@{text cempty}\<close> |
372 |
372 |
373 lemma cemptyE [elim!]: "cin a cempty \<Longrightarrow> P" by simp |
373 lemma cemptyE [elim!]: "cin a cempty \<Longrightarrow> P" by simp |
374 |
374 |
375 subsubsection {* @{text cinsert} *} |
375 subsubsection \<open>@{text cinsert}\<close> |
376 |
376 |
377 lemma countable_insert_iff: "countable (insert x A) \<longleftrightarrow> countable A" |
377 lemma countable_insert_iff: "countable (insert x A) \<longleftrightarrow> countable A" |
378 by (metis Diff_eq_empty_iff countable_empty countable_insert subset_insertI uncountable_minus_countable) |
378 by (metis Diff_eq_empty_iff countable_empty countable_insert subset_insertI uncountable_minus_countable) |
379 |
379 |
380 lemma set_cinsert: |
380 lemma set_cinsert: |
383 using assms by transfer(erule Set.set_insert, simp add: countable_insert_iff) |
383 using assms by transfer(erule Set.set_insert, simp add: countable_insert_iff) |
384 |
384 |
385 lemma mk_disjoint_cinsert: "cin a A \<Longrightarrow> \<exists>B. A = cinsert a B \<and> \<not> cin a B" |
385 lemma mk_disjoint_cinsert: "cin a A \<Longrightarrow> \<exists>B. A = cinsert a B \<and> \<not> cin a B" |
386 by (rule exI[where x = "cDiff A (csingle a)"]) blast |
386 by (rule exI[where x = "cDiff A (csingle a)"]) blast |
387 |
387 |
388 subsubsection {* @{text cimage} *} |
388 subsubsection \<open>@{text cimage}\<close> |
389 |
389 |
390 lemma subset_cimage_iff: "csubset_eq B (cimage f A) \<longleftrightarrow> (\<exists>AA. csubset_eq AA A \<and> B = cimage f AA)" |
390 lemma subset_cimage_iff: "csubset_eq B (cimage f A) \<longleftrightarrow> (\<exists>AA. csubset_eq AA A \<and> B = cimage f AA)" |
391 by transfer (metis countable_subset image_mono mem_Collect_eq subset_imageE) |
391 by transfer (metis countable_subset image_mono mem_Collect_eq subset_imageE) |
392 |
392 |
393 subsubsection {* bounded quantification *} |
393 subsubsection \<open>bounded quantification\<close> |
394 |
394 |
395 lemma cBex_simps [simp, no_atp]: |
395 lemma cBex_simps [simp, no_atp]: |
396 "\<And>A P Q. cBex A (\<lambda>x. P x \<and> Q) = (cBex A P \<and> Q)" |
396 "\<And>A P Q. cBex A (\<lambda>x. P x \<and> Q) = (cBex A P \<and> Q)" |
397 "\<And>A P Q. cBex A (\<lambda>x. P \<and> Q x) = (P \<and> cBex A Q)" |
397 "\<And>A P Q. cBex A (\<lambda>x. P \<and> Q x) = (P \<and> cBex A Q)" |
398 "\<And>P. cBex cempty P = False" |
398 "\<And>P. cBex cempty P = False" |
416 "(\<And>x. cin x A ==> P x) == Trueprop (cBall A (\<lambda>x. P x))" |
416 "(\<And>x. cin x A ==> P x) == Trueprop (cBall A (\<lambda>x. P x))" |
417 apply (simp only: atomize_all atomize_imp) |
417 apply (simp only: atomize_all atomize_imp) |
418 apply (rule equal_intr_rule) |
418 apply (rule equal_intr_rule) |
419 by (transfer, simp)+ |
419 by (transfer, simp)+ |
420 |
420 |
421 subsubsection {* @{const cUnion} *} |
421 subsubsection \<open>@{const cUnion}\<close> |
422 |
422 |
423 lemma cUNION_cimage: "cUNION (cimage f A) g = cUNION A (g \<circ> f)" |
423 lemma cUNION_cimage: "cUNION (cimage f A) g = cUNION A (g \<circ> f)" |
424 including cset.lifting by transfer auto |
424 including cset.lifting by transfer auto |
425 |
425 |
426 |
426 |
427 subsection {* Setup for Lifting/Transfer *} |
427 subsection \<open>Setup for Lifting/Transfer\<close> |
428 |
428 |
429 subsubsection {* Relator and predicator properties *} |
429 subsubsection \<open>Relator and predicator properties\<close> |
430 |
430 |
431 lift_definition rel_cset :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a cset \<Rightarrow> 'b cset \<Rightarrow> bool" |
431 lift_definition rel_cset :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a cset \<Rightarrow> 'b cset \<Rightarrow> bool" |
432 is rel_set parametric rel_set_transfer . |
432 is rel_set parametric rel_set_transfer . |
433 |
433 |
434 lemma rel_cset_alt_def: |
434 lemma rel_cset_alt_def: |
449 unfolding rel_fun_def by transfer(erule rel_set_UNION, simp add: rel_fun_def) |
449 unfolding rel_fun_def by transfer(erule rel_set_UNION, simp add: rel_fun_def) |
450 |
450 |
451 lemma rel_cset_csingle_iff [simp]: "rel_cset R (csingle x) (csingle y) \<longleftrightarrow> R x y" |
451 lemma rel_cset_csingle_iff [simp]: "rel_cset R (csingle x) (csingle y) \<longleftrightarrow> R x y" |
452 by transfer(auto simp add: rel_set_def) |
452 by transfer(auto simp add: rel_set_def) |
453 |
453 |
454 subsubsection {* Transfer rules for the Transfer package *} |
454 subsubsection \<open>Transfer rules for the Transfer package\<close> |
455 |
455 |
456 text {* Unconditional transfer rules *} |
456 text \<open>Unconditional transfer rules\<close> |
457 |
457 |
458 context begin interpretation lifting_syntax . |
458 context begin interpretation lifting_syntax . |
459 |
459 |
460 lemmas cempty_parametric [transfer_rule] = empty_transfer[Transfer.transferred] |
460 lemmas cempty_parametric [transfer_rule] = empty_transfer[Transfer.transferred] |
461 |
461 |
487 "((A ===> B ===> op =) ===> rel_cset A ===> rel_cset B ===> op =) rel_cset rel_cset" |
487 "((A ===> B ===> op =) ===> rel_cset A ===> rel_cset B ===> op =) rel_cset rel_cset" |
488 unfolding rel_fun_def |
488 unfolding rel_fun_def |
489 using rel_set_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred, where A = A and B = B] |
489 using rel_set_transfer[unfolded rel_fun_def, rule_format, Transfer.transferred, where A = A and B = B] |
490 by simp |
490 by simp |
491 |
491 |
492 text {* Rules requiring bi-unique, bi-total or right-total relations *} |
492 text \<open>Rules requiring bi-unique, bi-total or right-total relations\<close> |
493 |
493 |
494 lemma cin_parametric [transfer_rule]: |
494 lemma cin_parametric [transfer_rule]: |
495 "bi_unique A \<Longrightarrow> (A ===> rel_cset A ===> op =) cin cin" |
495 "bi_unique A \<Longrightarrow> (A ===> rel_cset A ===> op =) cin cin" |
496 unfolding rel_fun_def rel_cset_iff bi_unique_def by metis |
496 unfolding rel_fun_def rel_cset_iff bi_unique_def by metis |
497 |
497 |
514 end |
514 end |
515 |
515 |
516 lifting_update cset.lifting |
516 lifting_update cset.lifting |
517 lifting_forget cset.lifting |
517 lifting_forget cset.lifting |
518 |
518 |
519 subsection {* Registration as BNF *} |
519 subsection \<open>Registration as BNF\<close> |
520 |
520 |
521 lemma card_of_countable_sets_range: |
521 lemma card_of_countable_sets_range: |
522 fixes A :: "'a set" |
522 fixes A :: "'a set" |
523 shows "|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |{f::nat \<Rightarrow> 'a. range f \<subseteq> A}|" |
523 shows "|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |{f::nat \<Rightarrow> 'a. range f \<subseteq> A}|" |
524 apply(rule card_of_ordLeqI[of from_nat_into]) using inj_on_from_nat_into |
524 apply(rule card_of_ordLeqI[of from_nat_into]) using inj_on_from_nat_into |
566 (is "the_inv rcset ?L'") |
566 (is "the_inv rcset ?L'") |
567 have L: "countable ?L'" by auto |
567 have L: "countable ?L'" by auto |
568 hence *: "rcset R' = ?L'" unfolding R'_def by (intro rcset_to_rcset) |
568 hence *: "rcset R' = ?L'" unfolding R'_def by (intro rcset_to_rcset) |
569 thus ?R unfolding Grp_def relcompp.simps conversep.simps including cset.lifting |
569 thus ?R unfolding Grp_def relcompp.simps conversep.simps including cset.lifting |
570 proof (intro CollectI case_prodI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl) |
570 proof (intro CollectI case_prodI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl) |
571 from * `?L` show "a = cimage fst R'" by transfer (auto simp: image_def Collect_Int_Times) |
571 from * \<open>?L\<close> show "a = cimage fst R'" by transfer (auto simp: image_def Collect_Int_Times) |
572 from * `?L` show "b = cimage snd R'" by transfer (auto simp: image_def Collect_Int_Times) |
572 from * \<open>?L\<close> show "b = cimage snd R'" by transfer (auto simp: image_def Collect_Int_Times) |
573 qed simp_all |
573 qed simp_all |
574 next |
574 next |
575 assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps |
575 assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps |
576 by (simp add: subset_eq Ball_def)(transfer, auto simp add: cimage.rep_eq, metis snd_conv, metis fst_conv) |
576 by (simp add: subset_eq Ball_def)(transfer, auto simp add: cimage.rep_eq, metis snd_conv, metis fst_conv) |
577 qed |
577 qed |