1.1 --- a/src/HOL/BNF/Countable_Type.thy	Thu Dec 05 17:52:12 2013 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,91 +0,0 @@
     1.4 -(*  Title:      HOL/BNF/Countable_Type.thy
     1.5 -    Author:     Andrei Popescu, TU Muenchen
     1.6 -    Copyright   2012
     1.7 -
     1.8 -(At most) countable sets.
     1.9 -*)
    1.10 -
    1.11 -header {* (At Most) Countable Sets *}
    1.12 -
    1.13 -theory Countable_Type
    1.14 -imports
    1.15 -  "~~/src/HOL/Cardinals/Cardinals"
    1.16 -  "~~/src/HOL/Library/Countable_Set"
    1.17 -begin
    1.18 -
    1.19 -subsection{* Cardinal stuff *}
    1.20 -
    1.21 -lemma countable_card_of_nat: "countable A \<longleftrightarrow> |A| \<le>o |UNIV::nat set|"
    1.22 -  unfolding countable_def card_of_ordLeq[symmetric] by auto
    1.23 -
    1.24 -lemma countable_card_le_natLeq: "countable A \<longleftrightarrow> |A| \<le>o natLeq"
    1.25 -  unfolding countable_card_of_nat using card_of_nat ordLeq_ordIso_trans ordIso_symmetric by blast
    1.26 -
    1.27 -lemma countable_or_card_of:
    1.28 -assumes "countable A"
    1.29 -shows "(finite A \<and> |A| <o |UNIV::nat set| ) \<or>
    1.30 -       (infinite A  \<and> |A| =o |UNIV::nat set| )"
    1.31 -proof (cases "finite A")
    1.32 -  case True thus ?thesis by (metis finite_iff_cardOf_nat)
    1.33 -next
    1.34 -  case False with assms show ?thesis
    1.35 -    by (metis countable_card_of_nat infinite_iff_card_of_nat ordIso_iff_ordLeq)
    1.36 -qed
    1.37 -
    1.38 -lemma countable_cases_card_of[elim]:
    1.39 -  assumes "countable A"
    1.40 -  obtains (Fin) "finite A" "|A| <o |UNIV::nat set|"
    1.41 -        | (Inf) "infinite A" "|A| =o |UNIV::nat set|"
    1.42 -  using assms countable_or_card_of by blast
    1.43 -
    1.44 -lemma countable_or:
    1.45 -  "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.46 -  by (elim countable_enum_cases) fastforce+
    1.47 -
    1.48 -lemma countable_cases[elim]:
    1.49 -  assumes "countable A"
    1.50 -  obtains (Fin) f :: "'a\<Rightarrow>nat" where "finite A" "inj_on f A"
    1.51 -        | (Inf) f :: "'a\<Rightarrow>nat" where "infinite A" "bij_betw f A UNIV"
    1.52 -  using assms countable_or by metis
    1.53 -
    1.54 -lemma countable_ordLeq:
    1.55 -assumes "|A| \<le>o |B|" and "countable B"
    1.56 -shows "countable A"
    1.57 -using assms unfolding countable_card_of_nat by(rule ordLeq_transitive)
    1.58 -
    1.59 -lemma countable_ordLess:
    1.60 -assumes AB: "|A| <o |B|" and B: "countable B"
    1.61 -shows "countable A"
    1.62 -using countable_ordLeq[OF ordLess_imp_ordLeq[OF AB] B] .
    1.63 -
    1.64 -subsection{*  The type of countable sets *}
    1.65 -
    1.66 -typedef 'a cset = "{A :: 'a set. countable A}" morphisms rcset acset
    1.67 -  by (rule exI[of _ "{}"]) simp
    1.68 -
    1.69 -setup_lifting type_definition_cset
    1.70 -
    1.71 -declare
    1.72 -  rcset_inverse[simp]
    1.73 -  acset_inverse[Transfer.transferred, unfolded mem_Collect_eq, simp]
    1.74 -  acset_inject[Transfer.transferred, unfolded mem_Collect_eq, simp]
    1.75 -  rcset[Transfer.transferred, unfolded mem_Collect_eq, simp]
    1.76 -
    1.77 -lift_definition cin :: "'a \<Rightarrow> 'a cset \<Rightarrow> bool" is "op \<in>" parametric member_transfer
    1.78 -  ..
    1.79 -lift_definition cempty :: "'a cset" is "{}" parametric empty_transfer
    1.80 -  by (rule countable_empty)
    1.81 -lift_definition cinsert :: "'a \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is insert parametric Lifting_Set.insert_transfer
    1.82 -  by (rule countable_insert)
    1.83 -lift_definition csingle :: "'a \<Rightarrow> 'a cset" is "\<lambda>x. {x}"
    1.84 -  by (rule countable_insert[OF countable_empty])
    1.85 -lift_definition cUn :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op \<union>" parametric union_transfer
    1.86 -  by (rule countable_Un)
    1.87 -lift_definition cInt :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op \<inter>" parametric inter_transfer
    1.88 -  by (rule countable_Int1)
    1.89 -lift_definition cDiff :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op -" parametric Diff_transfer
    1.90 -  by (rule countable_Diff)
    1.91 -lift_definition cimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a cset \<Rightarrow> 'b cset" is "op `" parametric image_transfer
    1.92 -  by (rule countable_image)
    1.93 -
    1.94 -end