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
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
traytel@52662
    11
imports
traytel@52662
    12
  "~~/src/HOL/Cardinals/Cardinals"
traytel@52662
    13
  "~~/src/HOL/Library/Countable_Set"
blanchet@48975
    14
begin
blanchet@48975
    15
hoelzl@50144
    16
subsection{* Cardinal stuff *}
blanchet@48975
    17
hoelzl@50144
    18
lemma countable_card_of_nat: "countable A \<longleftrightarrow> |A| \<le>o |UNIV::nat set|"
hoelzl@50144
    19
  unfolding countable_def card_of_ordLeq[symmetric] by auto
blanchet@48975
    20
hoelzl@50144
    21
lemma countable_card_le_natLeq: "countable A \<longleftrightarrow> |A| \<le>o natLeq"
hoelzl@50144
    22
  unfolding countable_card_of_nat using card_of_nat ordLeq_ordIso_trans ordIso_symmetric by blast
blanchet@48975
    23
blanchet@48975
    24
lemma countable_or_card_of:
blanchet@48975
    25
assumes "countable A"
blanchet@48975
    26
shows "(finite A \<and> |A| <o |UNIV::nat set| ) \<or>
blanchet@48975
    27
       (infinite A  \<and> |A| =o |UNIV::nat set| )"
traytel@52662
    28
proof (cases "finite A")
traytel@52662
    29
  case True thus ?thesis by (metis finite_iff_cardOf_nat)
traytel@52662
    30
next
traytel@52662
    31
  case False with assms show ?thesis
traytel@52662
    32
    by (metis countable_card_of_nat infinite_iff_card_of_nat ordIso_iff_ordLeq)
traytel@52662
    33
qed
blanchet@48975
    34
hoelzl@50144
    35
lemma countable_cases_card_of[elim]:
hoelzl@50144
    36
  assumes "countable A"
hoelzl@50144
    37
  obtains (Fin) "finite A" "|A| <o |UNIV::nat set|"
hoelzl@50144
    38
        | (Inf) "infinite A" "|A| =o |UNIV::nat set|"
hoelzl@50144
    39
  using assms countable_or_card_of by blast
blanchet@48975
    40
hoelzl@50144
    41
lemma countable_or:
hoelzl@50144
    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)"
traytel@52662
    43
  by (elim countable_enum_cases) fastforce+
blanchet@48975
    44
hoelzl@50144
    45
lemma countable_cases[elim]:
hoelzl@50144
    46
  assumes "countable A"
hoelzl@50144
    47
  obtains (Fin) f :: "'a\<Rightarrow>nat" where "finite A" "inj_on f A"
hoelzl@50144
    48
        | (Inf) f :: "'a\<Rightarrow>nat" where "infinite A" "bij_betw f A UNIV"
hoelzl@50144
    49
  using assms countable_or by metis
blanchet@48975
    50
blanchet@48975
    51
lemma countable_ordLeq:
blanchet@48975
    52
assumes "|A| \<le>o |B|" and "countable B"
blanchet@48975
    53
shows "countable A"
blanchet@48975
    54
using assms unfolding countable_card_of_nat by(rule ordLeq_transitive)
blanchet@48975
    55
blanchet@48975
    56
lemma countable_ordLess:
blanchet@48975
    57
assumes AB: "|A| <o |B|" and B: "countable B"
blanchet@48975
    58
shows "countable A"
blanchet@48975
    59
using countable_ordLeq[OF ordLess_imp_ordLeq[OF AB] B] .
blanchet@48975
    60
blanchet@48975
    61
subsection{*  The type of countable sets *}
blanchet@48975
    62
traytel@52662
    63
typedef 'a cset = "{A :: 'a set. countable A}" morphisms rcset acset
traytel@52662
    64
  by (rule exI[of _ "{}"]) simp
blanchet@48975
    65
traytel@52662
    66
setup_lifting type_definition_cset
blanchet@48975
    67
traytel@52662
    68
declare
traytel@52662
    69
  rcset_inverse[simp]
traytel@52662
    70
  acset_inverse[Transfer.transferred, unfolded mem_Collect_eq, simp]
traytel@52662
    71
  acset_inject[Transfer.transferred, unfolded mem_Collect_eq, simp]
traytel@52662
    72
  rcset[Transfer.transferred, unfolded mem_Collect_eq, simp]
blanchet@48975
    73
traytel@52662
    74
lift_definition cin :: "'a \<Rightarrow> 'a cset \<Rightarrow> bool" is "op \<in>" parametric member_transfer
traytel@52662
    75
  ..
traytel@52662
    76
lift_definition cempty :: "'a cset" is "{}" parametric empty_transfer
traytel@52662
    77
  by (rule countable_empty)
kuncar@53013
    78
lift_definition cinsert :: "'a \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is insert parametric Lifting_Set.insert_transfer
traytel@52662
    79
  by (rule countable_insert)
traytel@52662
    80
lift_definition csingle :: "'a \<Rightarrow> 'a cset" is "\<lambda>x. {x}"
traytel@52662
    81
  by (rule countable_insert[OF countable_empty])
traytel@52662
    82
lift_definition cUn :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op \<union>" parametric union_transfer
traytel@52662
    83
  by (rule countable_Un)
traytel@52662
    84
lift_definition cInt :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op \<inter>" parametric inter_transfer
traytel@52662
    85
  by (rule countable_Int1)
traytel@52662
    86
lift_definition cDiff :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op -" parametric Diff_transfer
traytel@52662
    87
  by (rule countable_Diff)
traytel@52662
    88
lift_definition cimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a cset \<Rightarrow> 'b cset" is "op `" parametric image_transfer
traytel@52662
    89
  by (rule countable_image)
blanchet@48975
    90
blanchet@48975
    91
end