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