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