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
```