src/HOL/BNF/Countable_Type.thy
author hoelzl
Tue Nov 05 09:44:57 2013 +0100 (2013-11-05)
changeset 54257 5c7a3b6b05a9
parent 53013 3fbcfa911863
permissions -rw-r--r--
generalize SUP and INF to the syntactic type classes Sup and Inf
     1 (*  Title:      HOL/BNF/Countable_Type.thy
     2     Author:     Andrei Popescu, TU Muenchen
     3     Copyright   2012
     4 
     5 (At most) countable sets.
     6 *)
     7 
     8 header {* (At Most) Countable Sets *}
     9 
    10 theory Countable_Type
    11 imports
    12   "~~/src/HOL/Cardinals/Cardinals"
    13   "~~/src/HOL/Library/Countable_Set"
    14 begin
    15 
    16 subsection{* Cardinal stuff *}
    17 
    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
    20 
    21 lemma countable_card_le_natLeq: "countable A \<longleftrightarrow> |A| \<le>o natLeq"
    22   unfolding countable_card_of_nat using card_of_nat ordLeq_ordIso_trans ordIso_symmetric by blast
    23 
    24 lemma countable_or_card_of:
    25 assumes "countable A"
    26 shows "(finite A \<and> |A| <o |UNIV::nat set| ) \<or>
    27        (infinite A  \<and> |A| =o |UNIV::nat set| )"
    28 proof (cases "finite A")
    29   case True thus ?thesis by (metis finite_iff_cardOf_nat)
    30 next
    31   case False with assms show ?thesis
    32     by (metis countable_card_of_nat infinite_iff_card_of_nat ordIso_iff_ordLeq)
    33 qed
    34 
    35 lemma countable_cases_card_of[elim]:
    36   assumes "countable A"
    37   obtains (Fin) "finite A" "|A| <o |UNIV::nat set|"
    38         | (Inf) "infinite A" "|A| =o |UNIV::nat set|"
    39   using assms countable_or_card_of by blast
    40 
    41 lemma countable_or:
    42   "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)"
    43   by (elim countable_enum_cases) fastforce+
    44 
    45 lemma countable_cases[elim]:
    46   assumes "countable A"
    47   obtains (Fin) f :: "'a\<Rightarrow>nat" where "finite A" "inj_on f A"
    48         | (Inf) f :: "'a\<Rightarrow>nat" where "infinite A" "bij_betw f A UNIV"
    49   using assms countable_or by metis
    50 
    51 lemma countable_ordLeq:
    52 assumes "|A| \<le>o |B|" and "countable B"
    53 shows "countable A"
    54 using assms unfolding countable_card_of_nat by(rule ordLeq_transitive)
    55 
    56 lemma countable_ordLess:
    57 assumes AB: "|A| <o |B|" and B: "countable B"
    58 shows "countable A"
    59 using countable_ordLeq[OF ordLess_imp_ordLeq[OF AB] B] .
    60 
    61 subsection{*  The type of countable sets *}
    62 
    63 typedef 'a cset = "{A :: 'a set. countable A}" morphisms rcset acset
    64   by (rule exI[of _ "{}"]) simp
    65 
    66 setup_lifting type_definition_cset
    67 
    68 declare
    69   rcset_inverse[simp]
    70   acset_inverse[Transfer.transferred, unfolded mem_Collect_eq, simp]
    71   acset_inject[Transfer.transferred, unfolded mem_Collect_eq, simp]
    72   rcset[Transfer.transferred, unfolded mem_Collect_eq, simp]
    73 
    74 lift_definition cin :: "'a \<Rightarrow> 'a cset \<Rightarrow> bool" is "op \<in>" parametric member_transfer
    75   ..
    76 lift_definition cempty :: "'a cset" is "{}" parametric empty_transfer
    77   by (rule countable_empty)
    78 lift_definition cinsert :: "'a \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is insert parametric Lifting_Set.insert_transfer
    79   by (rule countable_insert)
    80 lift_definition csingle :: "'a \<Rightarrow> 'a cset" is "\<lambda>x. {x}"
    81   by (rule countable_insert[OF countable_empty])
    82 lift_definition cUn :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op \<union>" parametric union_transfer
    83   by (rule countable_Un)
    84 lift_definition cInt :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op \<inter>" parametric inter_transfer
    85   by (rule countable_Int1)
    86 lift_definition cDiff :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op -" parametric Diff_transfer
    87   by (rule countable_Diff)
    88 lift_definition cimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a cset \<Rightarrow> 'b cset" is "op `" parametric image_transfer
    89   by (rule countable_image)
    90 
    91 end