src/HOL/BNF/Countable_Set_Type.thy
author blanchet
Wed Nov 20 20:18:53 2013 +0100 (2013-11-20)
changeset 54539 bbab2ebda234
parent 53013 src/HOL/BNF/Countable_Type.thy@3fbcfa911863
child 54841 af71b753c459
permissions -rw-r--r--
move registration of countable set type as BNF to its own theory file (+ renamed theory)
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
blanchet@54539
   179
  fix A B1 B2 f1 f2 p1 p2
blanchet@54539
   180
  assume wp: "wpull A B1 B2 f1 f2 p1 p2"
blanchet@54539
   181
  show "wpull {x. rcset x \<subseteq> A} {x. rcset x \<subseteq> B1} {x. rcset x \<subseteq> B2}
blanchet@54539
   182
              (cimage f1) (cimage f2) (cimage p1) (cimage p2)"
blanchet@54539
   183
  unfolding wpull_def proof safe
blanchet@54539
   184
    fix y1 y2
blanchet@54539
   185
    assume Y1: "rcset y1 \<subseteq> B1" and Y2: "rcset y2 \<subseteq> B2"
blanchet@54539
   186
    assume "cimage f1 y1 = cimage f2 y2"
blanchet@54539
   187
    hence EQ: "f1 ` (rcset y1) = f2 ` (rcset y2)" by transfer
blanchet@54539
   188
    with Y1 Y2 obtain X where X: "X \<subseteq> A"
blanchet@54539
   189
    and Y1: "p1 ` X = rcset y1" and Y2: "p2 ` X = rcset y2"
blanchet@54539
   190
    using wpull_image[OF wp] unfolding wpull_def Pow_def Bex_def mem_Collect_eq
blanchet@54539
   191
      by (auto elim!: allE[of _ "rcset y1"] allE[of _ "rcset y2"])
blanchet@54539
   192
    have "\<forall> y1' \<in> rcset y1. \<exists> x. x \<in> X \<and> y1' = p1 x" using Y1 by auto
blanchet@54539
   193
    then obtain q1 where q1: "\<forall> y1' \<in> rcset y1. q1 y1' \<in> X \<and> y1' = p1 (q1 y1')" by metis
blanchet@54539
   194
    have "\<forall> y2' \<in> rcset y2. \<exists> x. x \<in> X \<and> y2' = p2 x" using Y2 by auto
blanchet@54539
   195
    then obtain q2 where q2: "\<forall> y2' \<in> rcset y2. q2 y2' \<in> X \<and> y2' = p2 (q2 y2')" by metis
blanchet@54539
   196
    def X' \<equiv> "q1 ` (rcset y1) \<union> q2 ` (rcset y2)"
blanchet@54539
   197
    have X': "X' \<subseteq> A" and Y1: "p1 ` X' = rcset y1" and Y2: "p2 ` X' = rcset y2"
blanchet@54539
   198
    using X Y1 Y2 q1 q2 unfolding X'_def by fast+
blanchet@54539
   199
    have fX': "countable X'" unfolding X'_def by simp
blanchet@54539
   200
    then obtain x where X'eq: "X' = rcset x" by transfer blast
blanchet@54539
   201
    show "\<exists>x\<in>{x. rcset x \<subseteq> A}. cimage p1 x = y1 \<and> cimage p2 x = y2"
blanchet@54539
   202
      using X' Y1 Y2 unfolding X'eq by (intro bexI[of _ "x"]) (transfer, auto)
blanchet@54539
   203
  qed
blanchet@54539
   204
next
blanchet@54539
   205
  fix R
blanchet@54539
   206
  show "cset_rel R =
blanchet@54539
   207
        (Grp {x. rcset x \<subseteq> Collect (split R)} (cimage fst))\<inverse>\<inverse> OO
blanchet@54539
   208
         Grp {x. rcset x \<subseteq> Collect (split R)} (cimage snd)"
blanchet@54539
   209
  unfolding cset_rel_def[abs_def] cset_rel_aux by simp
blanchet@54539
   210
qed (transfer, simp)
blanchet@54539
   211
blanchet@48975
   212
end