1.1 --- a/src/HOL/BNF/Countable_Type.thy Tue Jul 16 10:18:25 2013 +0200
1.2 +++ b/src/HOL/BNF/Countable_Type.thy Tue Jul 16 15:59:55 2013 +0200
1.3 @@ -8,7 +8,10 @@
1.4 header {* (At Most) Countable Sets *}
1.5
1.6 theory Countable_Type
1.7 -imports "../Cardinals/Cardinals" "~~/src/HOL/Library/Countable_Set"
1.8 +imports
1.9 + "~~/src/HOL/Cardinals/Cardinals"
1.10 + "~~/src/HOL/Library/Countable_Set"
1.11 + "~~/src/HOL/Library/Quotient_Set"
1.12 begin
1.13
1.14 subsection{* Cardinal stuff *}
1.15 @@ -23,9 +26,12 @@
1.16 assumes "countable A"
1.17 shows "(finite A \<and> |A| <o |UNIV::nat set| ) \<or>
1.18 (infinite A \<and> |A| =o |UNIV::nat set| )"
1.19 -apply (cases "finite A")
1.20 - apply(metis finite_iff_cardOf_nat)
1.21 - by (metis assms countable_card_of_nat infinite_iff_card_of_nat ordIso_iff_ordLeq)
1.22 +proof (cases "finite A")
1.23 + case True thus ?thesis by (metis finite_iff_cardOf_nat)
1.24 +next
1.25 + case False with assms show ?thesis
1.26 + by (metis countable_card_of_nat infinite_iff_card_of_nat ordIso_iff_ordLeq)
1.27 +qed
1.28
1.29 lemma countable_cases_card_of[elim]:
1.30 assumes "countable A"
1.31 @@ -35,7 +41,7 @@
1.32
1.33 lemma countable_or:
1.34 "countable A \<Longrightarrow> (\<exists> f::'a\<Rightarrow>nat. finite A \<and> inj_on f A) \<or> (\<exists> f::'a\<Rightarrow>nat. infinite A \<and> bij_betw f A UNIV)"
1.35 - by (auto elim: countable_enum_cases)
1.36 + by (elim countable_enum_cases) fastforce+
1.37
1.38 lemma countable_cases[elim]:
1.39 assumes "countable A"
1.40 @@ -55,48 +61,32 @@
1.41
1.42 subsection{* The type of countable sets *}
1.43
1.44 -typedef 'a cset = "{A :: 'a set. countable A}"
1.45 -apply(rule exI[of _ "{}"]) by simp
1.46 +typedef 'a cset = "{A :: 'a set. countable A}" morphisms rcset acset
1.47 + by (rule exI[of _ "{}"]) simp
1.48
1.49 -abbreviation rcset where "rcset \<equiv> Rep_cset"
1.50 -abbreviation acset where "acset \<equiv> Abs_cset"
1.51 +setup_lifting type_definition_cset
1.52
1.53 -lemmas acset_rcset = Rep_cset_inverse
1.54 -declare acset_rcset[simp]
1.55 +declare
1.56 + rcset_inverse[simp]
1.57 + acset_inverse[Transfer.transferred, unfolded mem_Collect_eq, simp]
1.58 + acset_inject[Transfer.transferred, unfolded mem_Collect_eq, simp]
1.59 + rcset[Transfer.transferred, unfolded mem_Collect_eq, simp]
1.60
1.61 -lemma acset_surj:
1.62 -"\<exists> A. countable A \<and> acset A = C"
1.63 -apply(cases rule: Abs_cset_cases[of C]) by auto
1.64 -
1.65 -lemma rcset_acset[simp]:
1.66 -assumes "countable A"
1.67 -shows "rcset (acset A) = A"
1.68 -using Abs_cset_inverse assms by auto
1.69 -
1.70 -lemma acset_inj[simp]:
1.71 -assumes "countable A" and "countable B"
1.72 -shows "acset A = acset B \<longleftrightarrow> A = B"
1.73 -using assms Abs_cset_inject by auto
1.74 -
1.75 -lemma rcset[simp]:
1.76 -"countable (rcset C)"
1.77 -using Rep_cset by simp
1.78 -
1.79 -lemma rcset_surj:
1.80 -assumes "countable A"
1.81 -shows "\<exists> C. rcset C = A"
1.82 -apply(cases rule: Rep_cset_cases[of A])
1.83 -using assms by auto
1.84 -
1.85 -definition "cIn a C \<equiv> (a \<in> rcset C)"
1.86 -definition "cEmp \<equiv> acset {}"
1.87 -definition "cIns a C \<equiv> acset (insert a (rcset C))"
1.88 -abbreviation cSingl where "cSingl a \<equiv> cIns a cEmp"
1.89 -definition "cUn C D \<equiv> acset (rcset C \<union> rcset D)"
1.90 -definition "cInt C D \<equiv> acset (rcset C \<inter> rcset D)"
1.91 -definition "cDif C D \<equiv> acset (rcset C - rcset D)"
1.92 -definition "cIm f C \<equiv> acset (f ` rcset C)"
1.93 -definition "cVim f D \<equiv> acset (f -` rcset D)"
1.94 -(* TODO eventually: nice setup for these operations, copied from the set setup *)
1.95 +lift_definition cin :: "'a \<Rightarrow> 'a cset \<Rightarrow> bool" is "op \<in>" parametric member_transfer
1.96 + ..
1.97 +lift_definition cempty :: "'a cset" is "{}" parametric empty_transfer
1.98 + by (rule countable_empty)
1.99 +lift_definition cinsert :: "'a \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is insert parametric insert_transfer
1.100 + by (rule countable_insert)
1.101 +lift_definition csingle :: "'a \<Rightarrow> 'a cset" is "\<lambda>x. {x}"
1.102 + by (rule countable_insert[OF countable_empty])
1.103 +lift_definition cUn :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op \<union>" parametric union_transfer
1.104 + by (rule countable_Un)
1.105 +lift_definition cInt :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op \<inter>" parametric inter_transfer
1.106 + by (rule countable_Int1)
1.107 +lift_definition cDiff :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op -" parametric Diff_transfer
1.108 + by (rule countable_Diff)
1.109 +lift_definition cimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a cset \<Rightarrow> 'b cset" is "op `" parametric image_transfer
1.110 + by (rule countable_image)
1.111
1.112 end