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