src/HOL/BNF/Countable_Type.thy
author hoelzl
Wed Nov 21 12:05:05 2012 +0100 (2012-11-21)
changeset 50144 885deccc264e
parent 49834 src/HOL/BNF/Countable_Set.thy@b27bbb021df1
child 52659 58b87aa4dc3b
permissions -rw-r--r--
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl@50144
     1
(*  Title:      HOL/BNF/Countable_Type.thy
blanchet@48975
     2
    Author:     Andrei Popescu, TU Muenchen
blanchet@48975
     3
    Copyright   2012
blanchet@48975
     4
blanchet@48975
     5
(At most) countable sets.
blanchet@48975
     6
*)
blanchet@48975
     7
blanchet@48975
     8
header {* (At Most) Countable Sets *}
blanchet@48975
     9
hoelzl@50144
    10
theory Countable_Type
hoelzl@50144
    11
imports "../Cardinals/Cardinals" "~~/src/HOL/Library/Countable_Set"
blanchet@48975
    12
begin
blanchet@48975
    13
hoelzl@50144
    14
subsection{* Cardinal stuff *}
blanchet@48975
    15
hoelzl@50144
    16
lemma countable_card_of_nat: "countable A \<longleftrightarrow> |A| \<le>o |UNIV::nat set|"
hoelzl@50144
    17
  unfolding countable_def card_of_ordLeq[symmetric] by auto
blanchet@48975
    18
hoelzl@50144
    19
lemma countable_card_le_natLeq: "countable A \<longleftrightarrow> |A| \<le>o natLeq"
hoelzl@50144
    20
  unfolding countable_card_of_nat using card_of_nat ordLeq_ordIso_trans ordIso_symmetric by blast
blanchet@48975
    21
blanchet@48975
    22
lemma countable_or_card_of:
blanchet@48975
    23
assumes "countable A"
blanchet@48975
    24
shows "(finite A \<and> |A| <o |UNIV::nat set| ) \<or>
blanchet@48975
    25
       (infinite A  \<and> |A| =o |UNIV::nat set| )"
blanchet@48975
    26
apply (cases "finite A")
blanchet@48975
    27
  apply(metis finite_iff_cardOf_nat)
blanchet@48975
    28
  by (metis assms countable_card_of_nat infinite_iff_card_of_nat ordIso_iff_ordLeq)
blanchet@48975
    29
hoelzl@50144
    30
lemma countable_cases_card_of[elim]:
hoelzl@50144
    31
  assumes "countable A"
hoelzl@50144
    32
  obtains (Fin) "finite A" "|A| <o |UNIV::nat set|"
hoelzl@50144
    33
        | (Inf) "infinite A" "|A| =o |UNIV::nat set|"
hoelzl@50144
    34
  using assms countable_or_card_of by blast
blanchet@48975
    35
hoelzl@50144
    36
lemma countable_or:
hoelzl@50144
    37
  "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)"
hoelzl@50144
    38
  by (auto elim: countable_enum_cases)
blanchet@48975
    39
hoelzl@50144
    40
lemma countable_cases[elim]:
hoelzl@50144
    41
  assumes "countable A"
hoelzl@50144
    42
  obtains (Fin) f :: "'a\<Rightarrow>nat" where "finite A" "inj_on f A"
hoelzl@50144
    43
        | (Inf) f :: "'a\<Rightarrow>nat" where "infinite A" "bij_betw f A UNIV"
hoelzl@50144
    44
  using assms countable_or by metis
blanchet@48975
    45
blanchet@48975
    46
lemma countable_ordLeq:
blanchet@48975
    47
assumes "|A| \<le>o |B|" and "countable B"
blanchet@48975
    48
shows "countable A"
blanchet@48975
    49
using assms unfolding countable_card_of_nat by(rule ordLeq_transitive)
blanchet@48975
    50
blanchet@48975
    51
lemma countable_ordLess:
blanchet@48975
    52
assumes AB: "|A| <o |B|" and B: "countable B"
blanchet@48975
    53
shows "countable A"
blanchet@48975
    54
using countable_ordLeq[OF ordLess_imp_ordLeq[OF AB] B] .
blanchet@48975
    55
blanchet@49514
    56
lemma ordLeq_countable:
popescua@49440
    57
assumes "|A| \<le>o |B|" and "countable B"
popescua@49440
    58
shows "countable A"
hoelzl@50144
    59
using assms unfolding countable_card_of_nat by(rule ordLeq_transitive)
popescua@49440
    60
blanchet@49514
    61
lemma ordLess_countable:
popescua@49440
    62
assumes A: "|A| <o |B|" and B: "countable B"
popescua@49440
    63
shows "countable A"
popescua@49440
    64
by (rule ordLeq_countable[OF ordLess_imp_ordLeq[OF A] B])
popescua@49440
    65
blanchet@48975
    66
subsection{*  The type of countable sets *}
blanchet@48975
    67
wenzelm@49834
    68
typedef 'a cset = "{A :: 'a set. countable A}"
blanchet@48975
    69
apply(rule exI[of _ "{}"]) by simp
blanchet@48975
    70
blanchet@48975
    71
abbreviation rcset where "rcset \<equiv> Rep_cset"
blanchet@48975
    72
abbreviation acset where "acset \<equiv> Abs_cset"
blanchet@48975
    73
blanchet@48975
    74
lemmas acset_rcset = Rep_cset_inverse
blanchet@48975
    75
declare acset_rcset[simp]
blanchet@48975
    76
blanchet@48975
    77
lemma acset_surj:
blanchet@48975
    78
"\<exists> A. countable A \<and> acset A = C"
blanchet@48975
    79
apply(cases rule: Abs_cset_cases[of C]) by auto
blanchet@48975
    80
blanchet@48975
    81
lemma rcset_acset[simp]:
blanchet@48975
    82
assumes "countable A"
blanchet@48975
    83
shows "rcset (acset A) = A"
blanchet@48975
    84
using Abs_cset_inverse assms by auto
blanchet@48975
    85
blanchet@48975
    86
lemma acset_inj[simp]:
blanchet@48975
    87
assumes "countable A" and "countable B"
blanchet@48975
    88
shows "acset A = acset B \<longleftrightarrow> A = B"
blanchet@48975
    89
using assms Abs_cset_inject by auto
blanchet@48975
    90
blanchet@48975
    91
lemma rcset[simp]:
blanchet@48975
    92
"countable (rcset C)"
blanchet@48975
    93
using Rep_cset by simp
blanchet@48975
    94
blanchet@48975
    95
lemma rcset_inj[simp]:
blanchet@48975
    96
"rcset C = rcset D \<longleftrightarrow> C = D"
blanchet@48975
    97
by (metis acset_rcset)
blanchet@48975
    98
blanchet@48975
    99
lemma rcset_surj:
blanchet@48975
   100
assumes "countable A"
blanchet@48975
   101
shows "\<exists> C. rcset C = A"
blanchet@48975
   102
apply(cases rule: Rep_cset_cases[of A])
blanchet@48975
   103
using assms by auto
blanchet@48975
   104
blanchet@48975
   105
definition "cIn a C \<equiv> (a \<in> rcset C)"
blanchet@48975
   106
definition "cEmp \<equiv> acset {}"
blanchet@48975
   107
definition "cIns a C \<equiv> acset (insert a (rcset C))"
blanchet@48975
   108
abbreviation cSingl where "cSingl a \<equiv> cIns a cEmp"
blanchet@48975
   109
definition "cUn C D \<equiv> acset (rcset C \<union> rcset D)"
blanchet@48975
   110
definition "cInt C D \<equiv> acset (rcset C \<inter> rcset D)"
blanchet@48975
   111
definition "cDif C D \<equiv> acset (rcset C - rcset D)"
blanchet@48975
   112
definition "cIm f C \<equiv> acset (f ` rcset C)"
blanchet@48975
   113
definition "cVim f D \<equiv> acset (f -` rcset D)"
blanchet@48975
   114
(* TODO eventually: nice setup for these operations, copied from the set setup *)
blanchet@48975
   115
blanchet@48975
   116
end