src/HOL/BNF/Countable_Set_Type.thy
author blanchet
Mon Jan 20 18:24:56 2014 +0100 (2014-01-20)
changeset 55070 235c7661a96b
parent 54841 af71b753c459
permissions -rw-r--r--
rationalized dependencies
blanchet@54539
     1
(*  Title:      HOL/BNF/Countable_Set_Type.thy
blanchet@48975
     2
    Author:     Andrei Popescu, TU Muenchen
blanchet@48975
     3
    Copyright   2012
blanchet@48975
     4
blanchet@54539
     5
Type of (at most) countable sets.
blanchet@48975
     6
*)
blanchet@48975
     7
blanchet@54539
     8
header {* Type of (at Most) Countable Sets *}
blanchet@48975
     9
blanchet@54539
    10
theory Countable_Set_Type
traytel@52662
    11
imports
blanchet@55070
    12
  "~~/src/HOL/Cardinals/Cardinal_Notations"
traytel@52662
    13
  "~~/src/HOL/Library/Countable_Set"
blanchet@48975
    14
begin
blanchet@48975
    15
blanchet@55070
    16
abbreviation "Grp \<equiv> BNF_Util.Grp"
blanchet@55070
    17
blanchet@55070
    18
hoelzl@50144
    19
subsection{* Cardinal stuff *}
blanchet@48975
    20
hoelzl@50144
    21
lemma countable_card_of_nat: "countable A \<longleftrightarrow> |A| \<le>o |UNIV::nat set|"
hoelzl@50144
    22
  unfolding countable_def card_of_ordLeq[symmetric] by auto
blanchet@48975
    23
hoelzl@50144
    24
lemma countable_card_le_natLeq: "countable A \<longleftrightarrow> |A| \<le>o natLeq"
hoelzl@50144
    25
  unfolding countable_card_of_nat using card_of_nat ordLeq_ordIso_trans ordIso_symmetric by blast
blanchet@48975
    26
blanchet@48975
    27
lemma countable_or_card_of:
blanchet@48975
    28
assumes "countable A"
blanchet@48975
    29
shows "(finite A \<and> |A| <o |UNIV::nat set| ) \<or>
blanchet@48975
    30
       (infinite A  \<and> |A| =o |UNIV::nat set| )"
blanchet@55070
    31
by (metis assms countable_card_of_nat infinite_iff_card_of_nat ordIso_iff_ordLeq
blanchet@55070
    32
      ordLeq_iff_ordLess_or_ordIso)
blanchet@48975
    33
hoelzl@50144
    34
lemma countable_cases_card_of[elim]:
hoelzl@50144
    35
  assumes "countable A"
hoelzl@50144
    36
  obtains (Fin) "finite A" "|A| <o |UNIV::nat set|"
hoelzl@50144
    37
        | (Inf) "infinite A" "|A| =o |UNIV::nat set|"
hoelzl@50144
    38
  using assms countable_or_card_of by blast
blanchet@48975
    39
hoelzl@50144
    40
lemma countable_or:
hoelzl@50144
    41
  "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
    42
  by (elim countable_enum_cases) fastforce+
blanchet@48975
    43
hoelzl@50144
    44
lemma countable_cases[elim]:
hoelzl@50144
    45
  assumes "countable A"
hoelzl@50144
    46
  obtains (Fin) f :: "'a\<Rightarrow>nat" where "finite A" "inj_on f A"
hoelzl@50144
    47
        | (Inf) f :: "'a\<Rightarrow>nat" where "infinite A" "bij_betw f A UNIV"
hoelzl@50144
    48
  using assms countable_or by metis
blanchet@48975
    49
blanchet@48975
    50
lemma countable_ordLeq:
blanchet@48975
    51
assumes "|A| \<le>o |B|" and "countable B"
blanchet@48975
    52
shows "countable A"
blanchet@48975
    53
using assms unfolding countable_card_of_nat by(rule ordLeq_transitive)
blanchet@48975
    54
blanchet@48975
    55
lemma countable_ordLess:
blanchet@48975
    56
assumes AB: "|A| <o |B|" and B: "countable B"
blanchet@48975
    57
shows "countable A"
blanchet@48975
    58
using countable_ordLeq[OF ordLess_imp_ordLeq[OF AB] B] .
blanchet@48975
    59
blanchet@54539
    60
subsection {* The type of countable sets *}
blanchet@48975
    61
traytel@52662
    62
typedef 'a cset = "{A :: 'a set. countable A}" morphisms rcset acset
traytel@52662
    63
  by (rule exI[of _ "{}"]) simp
blanchet@48975
    64
traytel@52662
    65
setup_lifting type_definition_cset
blanchet@48975
    66
traytel@52662
    67
declare
traytel@52662
    68
  rcset_inverse[simp]
traytel@52662
    69
  acset_inverse[Transfer.transferred, unfolded mem_Collect_eq, simp]
traytel@52662
    70
  acset_inject[Transfer.transferred, unfolded mem_Collect_eq, simp]
traytel@52662
    71
  rcset[Transfer.transferred, unfolded mem_Collect_eq, simp]
blanchet@48975
    72
traytel@52662
    73
lift_definition cin :: "'a \<Rightarrow> 'a cset \<Rightarrow> bool" is "op \<in>" parametric member_transfer
traytel@52662
    74
  ..
traytel@52662
    75
lift_definition cempty :: "'a cset" is "{}" parametric empty_transfer
traytel@52662
    76
  by (rule countable_empty)
kuncar@53013
    77
lift_definition cinsert :: "'a \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is insert parametric Lifting_Set.insert_transfer
traytel@52662
    78
  by (rule countable_insert)
traytel@52662
    79
lift_definition csingle :: "'a \<Rightarrow> 'a cset" is "\<lambda>x. {x}"
traytel@52662
    80
  by (rule countable_insert[OF countable_empty])
traytel@52662
    81
lift_definition cUn :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op \<union>" parametric union_transfer
traytel@52662
    82
  by (rule countable_Un)
traytel@52662
    83
lift_definition cInt :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op \<inter>" parametric inter_transfer
traytel@52662
    84
  by (rule countable_Int1)
traytel@52662
    85
lift_definition cDiff :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op -" parametric Diff_transfer
traytel@52662
    86
  by (rule countable_Diff)
traytel@52662
    87
lift_definition cimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a cset \<Rightarrow> 'b cset" is "op `" parametric image_transfer
traytel@52662
    88
  by (rule countable_image)
blanchet@48975
    89
blanchet@54539
    90
subsection {* Registration as BNF *}
blanchet@54539
    91
blanchet@54539
    92
lemma card_of_countable_sets_range:
blanchet@54539
    93
fixes A :: "'a set"
blanchet@54539
    94
shows "|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |{f::nat \<Rightarrow> 'a. range f \<subseteq> A}|"
blanchet@54539
    95
apply(rule card_of_ordLeqI[of from_nat_into]) using inj_on_from_nat_into
blanchet@54539
    96
unfolding inj_on_def by auto
blanchet@54539
    97
blanchet@54539
    98
lemma card_of_countable_sets_Func:
blanchet@54539
    99
"|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |A| ^c natLeq"
blanchet@54539
   100
using card_of_countable_sets_range card_of_Func_UNIV[THEN ordIso_symmetric]
blanchet@54539
   101
unfolding cexp_def Field_natLeq Field_card_of
blanchet@54539
   102
by (rule ordLeq_ordIso_trans)
blanchet@54539
   103
blanchet@54539
   104
lemma ordLeq_countable_subsets:
blanchet@54539
   105
"|A| \<le>o |{X. X \<subseteq> A \<and> countable X}|"
blanchet@54539
   106
apply (rule card_of_ordLeqI[of "\<lambda> a. {a}"]) unfolding inj_on_def by auto
blanchet@54539
   107
blanchet@54539
   108
lemma finite_countable_subset:
blanchet@54539
   109
"finite {X. X \<subseteq> A \<and> countable X} \<longleftrightarrow> finite A"
blanchet@54539
   110
apply default
blanchet@54539
   111
 apply (erule contrapos_pp)
blanchet@54539
   112
 apply (rule card_of_ordLeq_infinite)
blanchet@54539
   113
 apply (rule ordLeq_countable_subsets)
blanchet@54539
   114
 apply assumption
blanchet@54539
   115
apply (rule finite_Collect_conjI)
blanchet@54539
   116
apply (rule disjI1)
blanchet@54539
   117
by (erule finite_Collect_subsets)
blanchet@54539
   118
blanchet@54539
   119
lemma rcset_to_rcset: "countable A \<Longrightarrow> rcset (the_inv rcset A) = A"
blanchet@54539
   120
  apply (rule f_the_inv_into_f[unfolded inj_on_def image_iff])
blanchet@54539
   121
   apply transfer' apply simp
blanchet@54539
   122
  apply transfer' apply simp
blanchet@54539
   123
  done
blanchet@54539
   124
blanchet@54539
   125
lemma Collect_Int_Times:
blanchet@54539
   126
"{(x, y). R x y} \<inter> A \<times> B = {(x, y). R x y \<and> x \<in> A \<and> y \<in> B}"
blanchet@54539
   127
by auto
blanchet@54539
   128
blanchet@54539
   129
definition cset_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a cset \<Rightarrow> 'b cset \<Rightarrow> bool" where
blanchet@54539
   130
"cset_rel R a b \<longleftrightarrow>
blanchet@54539
   131
 (\<forall>t \<in> rcset a. \<exists>u \<in> rcset b. R t u) \<and>
blanchet@54539
   132
 (\<forall>t \<in> rcset b. \<exists>u \<in> rcset a. R u t)"
blanchet@54539
   133
blanchet@54539
   134
lemma cset_rel_aux:
blanchet@54539
   135
"(\<forall>t \<in> rcset a. \<exists>u \<in> rcset b. R t u) \<and> (\<forall>t \<in> rcset b. \<exists>u \<in> rcset a. R u t) \<longleftrightarrow>
blanchet@54539
   136
 ((Grp {x. rcset x \<subseteq> {(a, b). R a b}} (cimage fst))\<inverse>\<inverse> OO
blanchet@54539
   137
          Grp {x. rcset x \<subseteq> {(a, b). R a b}} (cimage snd)) a b" (is "?L = ?R")
blanchet@54539
   138
proof
blanchet@54539
   139
  assume ?L
blanchet@54539
   140
  def R' \<equiv> "the_inv rcset (Collect (split R) \<inter> (rcset a \<times> rcset b))"
blanchet@54539
   141
  (is "the_inv rcset ?L'")
blanchet@54539
   142
  have L: "countable ?L'" by auto
blanchet@55070
   143
  hence *: "rcset R' = ?L'" unfolding R'_def by (intro rcset_to_rcset)
blanchet@54539
   144
  thus ?R unfolding Grp_def relcompp.simps conversep.simps
blanchet@54539
   145
  proof (intro CollectI prod_caseI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
blanchet@54539
   146
    from * `?L` show "a = cimage fst R'" by transfer (auto simp: image_def Collect_Int_Times)
blanchet@54539
   147
  next
blanchet@54539
   148
    from * `?L` show "b = cimage snd R'" by transfer (auto simp: image_def Collect_Int_Times)
blanchet@54539
   149
  qed simp_all
blanchet@54539
   150
next
blanchet@54539
   151
  assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps
blanchet@54539
   152
    by transfer force
blanchet@54539
   153
qed
blanchet@54539
   154
blanchet@54539
   155
bnf "'a cset"
blanchet@54539
   156
  map: cimage
blanchet@54539
   157
  sets: rcset
blanchet@54539
   158
  bd: natLeq
blanchet@54539
   159
  wits: "cempty"
blanchet@54539
   160
  rel: cset_rel
blanchet@54539
   161
proof -
blanchet@54539
   162
  show "cimage id = id" by transfer' simp
blanchet@54539
   163
next
blanchet@54539
   164
  fix f g show "cimage (g \<circ> f) = cimage g \<circ> cimage f" by transfer' fastforce
blanchet@54539
   165
next
blanchet@54539
   166
  fix C f g assume eq: "\<And>a. a \<in> rcset C \<Longrightarrow> f a = g a"
blanchet@54539
   167
  thus "cimage f C = cimage g C" by transfer force
blanchet@54539
   168
next
blanchet@54539
   169
  fix f show "rcset \<circ> cimage f = op ` f \<circ> rcset" by transfer' fastforce
blanchet@54539
   170
next
blanchet@54539
   171
  show "card_order natLeq" by (rule natLeq_card_order)
blanchet@54539
   172
next
blanchet@54539
   173
  show "cinfinite natLeq" by (rule natLeq_cinfinite)
blanchet@54539
   174
next
blanchet@54539
   175
  fix C show "|rcset C| \<le>o natLeq" by transfer (unfold countable_card_le_natLeq)
blanchet@54539
   176
next
traytel@54841
   177
  fix R S
traytel@54841
   178
  show "cset_rel R OO cset_rel S \<le> cset_rel (R OO S)"
traytel@54841
   179
    unfolding cset_rel_def[abs_def] by fast
blanchet@54539
   180
next
blanchet@54539
   181
  fix R
blanchet@54539
   182
  show "cset_rel R =
blanchet@54539
   183
        (Grp {x. rcset x \<subseteq> Collect (split R)} (cimage fst))\<inverse>\<inverse> OO
blanchet@54539
   184
         Grp {x. rcset x \<subseteq> Collect (split R)} (cimage snd)"
blanchet@54539
   185
  unfolding cset_rel_def[abs_def] cset_rel_aux by simp
blanchet@54539
   186
qed (transfer, simp)
blanchet@54539
   187
blanchet@48975
   188
end