blanchet@55075: (*  Title:      HOL/Library/Countable_Set_Type.thy
blanchet@48975:     Author:     Andrei Popescu, TU Muenchen
blanchet@48975:     Copyright   2012
blanchet@48975: 
blanchet@54539: Type of (at most) countable sets.
blanchet@48975: *)
blanchet@48975: 
blanchet@54539: header {* Type of (at Most) Countable Sets *}
blanchet@48975: 
blanchet@54539: theory Countable_Set_Type
blanchet@55075: imports Countable_Set Cardinal_Notations
blanchet@48975: begin
blanchet@48975: 
blanchet@57398: abbreviation "Grp \<equiv> BNF_Def.Grp"
blanchet@55070: 
blanchet@55070: 
hoelzl@50144: subsection{* Cardinal stuff *}
blanchet@48975: 
hoelzl@50144: lemma countable_card_of_nat: "countable A \<longleftrightarrow> |A| \<le>o |UNIV::nat set|"
hoelzl@50144:   unfolding countable_def card_of_ordLeq[symmetric] by auto
blanchet@48975: 
hoelzl@50144: lemma countable_card_le_natLeq: "countable A \<longleftrightarrow> |A| \<le>o natLeq"
hoelzl@50144:   unfolding countable_card_of_nat using card_of_nat ordLeq_ordIso_trans ordIso_symmetric by blast
blanchet@48975: 
blanchet@48975: lemma countable_or_card_of:
blanchet@48975: assumes "countable A"
blanchet@48975: shows "(finite A \<and> |A| <o |UNIV::nat set| ) \<or>
blanchet@48975:        (infinite A  \<and> |A| =o |UNIV::nat set| )"
blanchet@55070: by (metis assms countable_card_of_nat infinite_iff_card_of_nat ordIso_iff_ordLeq
blanchet@55070:       ordLeq_iff_ordLess_or_ordIso)
blanchet@48975: 
hoelzl@50144: lemma countable_cases_card_of[elim]:
hoelzl@50144:   assumes "countable A"
hoelzl@50144:   obtains (Fin) "finite A" "|A| <o |UNIV::nat set|"
hoelzl@50144:         | (Inf) "infinite A" "|A| =o |UNIV::nat set|"
hoelzl@50144:   using assms countable_or_card_of by blast
blanchet@48975: 
hoelzl@50144: lemma countable_or:
hoelzl@50144:   "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:   by (elim countable_enum_cases) fastforce+
blanchet@48975: 
hoelzl@50144: lemma countable_cases[elim]:
hoelzl@50144:   assumes "countable A"
hoelzl@50144:   obtains (Fin) f :: "'a\<Rightarrow>nat" where "finite A" "inj_on f A"
hoelzl@50144:         | (Inf) f :: "'a\<Rightarrow>nat" where "infinite A" "bij_betw f A UNIV"
hoelzl@50144:   using assms countable_or by metis
blanchet@48975: 
blanchet@48975: lemma countable_ordLeq:
blanchet@48975: assumes "|A| \<le>o |B|" and "countable B"
blanchet@48975: shows "countable A"
blanchet@48975: using assms unfolding countable_card_of_nat by(rule ordLeq_transitive)
blanchet@48975: 
blanchet@48975: lemma countable_ordLess:
blanchet@48975: assumes AB: "|A| <o |B|" and B: "countable B"
blanchet@48975: shows "countable A"
blanchet@48975: using countable_ordLeq[OF ordLess_imp_ordLeq[OF AB] B] .
blanchet@48975: 
blanchet@54539: subsection {* The type of countable sets *}
blanchet@48975: 
traytel@52662: typedef 'a cset = "{A :: 'a set. countable A}" morphisms rcset acset
traytel@52662:   by (rule exI[of _ "{}"]) simp
blanchet@48975: 
traytel@52662: setup_lifting type_definition_cset
blanchet@48975: 
traytel@52662: declare
traytel@52662:   rcset_inverse[simp]
traytel@52662:   acset_inverse[Transfer.transferred, unfolded mem_Collect_eq, simp]
traytel@52662:   acset_inject[Transfer.transferred, unfolded mem_Collect_eq, simp]
traytel@52662:   rcset[Transfer.transferred, unfolded mem_Collect_eq, simp]
blanchet@48975: 
traytel@52662: lift_definition cin :: "'a \<Rightarrow> 'a cset \<Rightarrow> bool" is "op \<in>" parametric member_transfer
kuncar@55565:   .
traytel@52662: lift_definition cempty :: "'a cset" is "{}" parametric empty_transfer
traytel@52662:   by (rule countable_empty)
kuncar@53013: lift_definition cinsert :: "'a \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is insert parametric Lifting_Set.insert_transfer
traytel@52662:   by (rule countable_insert)
traytel@52662: lift_definition csingle :: "'a \<Rightarrow> 'a cset" is "\<lambda>x. {x}"
traytel@52662:   by (rule countable_insert[OF countable_empty])
traytel@52662: lift_definition cUn :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op \<union>" parametric union_transfer
traytel@52662:   by (rule countable_Un)
traytel@52662: lift_definition cInt :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op \<inter>" parametric inter_transfer
traytel@52662:   by (rule countable_Int1)
traytel@52662: lift_definition cDiff :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op -" parametric Diff_transfer
traytel@52662:   by (rule countable_Diff)
traytel@52662: lift_definition cimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a cset \<Rightarrow> 'b cset" is "op `" parametric image_transfer
traytel@52662:   by (rule countable_image)
blanchet@48975: 
blanchet@54539: subsection {* Registration as BNF *}
blanchet@54539: 
blanchet@54539: lemma card_of_countable_sets_range:
blanchet@54539: fixes A :: "'a set"
blanchet@54539: shows "|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |{f::nat \<Rightarrow> 'a. range f \<subseteq> A}|"
blanchet@54539: apply(rule card_of_ordLeqI[of from_nat_into]) using inj_on_from_nat_into
blanchet@54539: unfolding inj_on_def by auto
blanchet@54539: 
blanchet@54539: lemma card_of_countable_sets_Func:
blanchet@54539: "|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |A| ^c natLeq"
blanchet@54539: using card_of_countable_sets_range card_of_Func_UNIV[THEN ordIso_symmetric]
blanchet@54539: unfolding cexp_def Field_natLeq Field_card_of
blanchet@54539: by (rule ordLeq_ordIso_trans)
blanchet@54539: 
blanchet@54539: lemma ordLeq_countable_subsets:
blanchet@54539: "|A| \<le>o |{X. X \<subseteq> A \<and> countable X}|"
blanchet@54539: apply (rule card_of_ordLeqI[of "\<lambda> a. {a}"]) unfolding inj_on_def by auto
blanchet@54539: 
blanchet@54539: lemma finite_countable_subset:
blanchet@54539: "finite {X. X \<subseteq> A \<and> countable X} \<longleftrightarrow> finite A"
blanchet@54539: apply default
blanchet@54539:  apply (erule contrapos_pp)
blanchet@54539:  apply (rule card_of_ordLeq_infinite)
blanchet@54539:  apply (rule ordLeq_countable_subsets)
blanchet@54539:  apply assumption
blanchet@54539: apply (rule finite_Collect_conjI)
blanchet@54539: apply (rule disjI1)
blanchet@54539: by (erule finite_Collect_subsets)
blanchet@54539: 
blanchet@54539: lemma rcset_to_rcset: "countable A \<Longrightarrow> rcset (the_inv rcset A) = A"
blanchet@54539:   apply (rule f_the_inv_into_f[unfolded inj_on_def image_iff])
blanchet@54539:    apply transfer' apply simp
blanchet@54539:   apply transfer' apply simp
blanchet@54539:   done
blanchet@54539: 
blanchet@54539: lemma Collect_Int_Times:
blanchet@54539: "{(x, y). R x y} \<inter> A \<times> B = {(x, y). R x y \<and> x \<in> A \<and> y \<in> B}"
blanchet@54539: by auto
blanchet@54539: 
blanchet@55934: definition rel_cset :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a cset \<Rightarrow> 'b cset \<Rightarrow> bool" where
blanchet@55934: "rel_cset R a b \<longleftrightarrow>
blanchet@54539:  (\<forall>t \<in> rcset a. \<exists>u \<in> rcset b. R t u) \<and>
blanchet@54539:  (\<forall>t \<in> rcset b. \<exists>u \<in> rcset a. R u t)"
blanchet@54539: 
blanchet@55934: lemma rel_cset_aux:
blanchet@54539: "(\<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:  ((Grp {x. rcset x \<subseteq> {(a, b). R a b}} (cimage fst))\<inverse>\<inverse> OO
blanchet@54539:           Grp {x. rcset x \<subseteq> {(a, b). R a b}} (cimage snd)) a b" (is "?L = ?R")
blanchet@54539: proof
blanchet@54539:   assume ?L
blanchet@54539:   def R' \<equiv> "the_inv rcset (Collect (split R) \<inter> (rcset a \<times> rcset b))"
blanchet@54539:   (is "the_inv rcset ?L'")
blanchet@54539:   have L: "countable ?L'" by auto
blanchet@55070:   hence *: "rcset R' = ?L'" unfolding R'_def by (intro rcset_to_rcset)
blanchet@54539:   thus ?R unfolding Grp_def relcompp.simps conversep.simps
blanchet@55414:   proof (intro CollectI case_prodI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
blanchet@54539:     from * `?L` show "a = cimage fst R'" by transfer (auto simp: image_def Collect_Int_Times)
blanchet@54539:   next
blanchet@54539:     from * `?L` show "b = cimage snd R'" by transfer (auto simp: image_def Collect_Int_Times)
blanchet@54539:   qed simp_all
blanchet@54539: next
blanchet@54539:   assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps
blanchet@54539:     by transfer force
blanchet@54539: qed
blanchet@54539: 
blanchet@54539: bnf "'a cset"
blanchet@54539:   map: cimage
blanchet@54539:   sets: rcset
blanchet@54539:   bd: natLeq
blanchet@54539:   wits: "cempty"
blanchet@55934:   rel: rel_cset
blanchet@54539: proof -
blanchet@54539:   show "cimage id = id" by transfer' simp
blanchet@54539: next
blanchet@54539:   fix f g show "cimage (g \<circ> f) = cimage g \<circ> cimage f" by transfer' fastforce
blanchet@54539: next
blanchet@54539:   fix C f g assume eq: "\<And>a. a \<in> rcset C \<Longrightarrow> f a = g a"
blanchet@54539:   thus "cimage f C = cimage g C" by transfer force
blanchet@54539: next
blanchet@54539:   fix f show "rcset \<circ> cimage f = op ` f \<circ> rcset" by transfer' fastforce
blanchet@54539: next
blanchet@54539:   show "card_order natLeq" by (rule natLeq_card_order)
blanchet@54539: next
blanchet@54539:   show "cinfinite natLeq" by (rule natLeq_cinfinite)
blanchet@54539: next
blanchet@54539:   fix C show "|rcset C| \<le>o natLeq" by transfer (unfold countable_card_le_natLeq)
blanchet@54539: next
traytel@54841:   fix R S
blanchet@55934:   show "rel_cset R OO rel_cset S \<le> rel_cset (R OO S)"
blanchet@55934:     unfolding rel_cset_def[abs_def] by fast
blanchet@54539: next
blanchet@54539:   fix R
blanchet@55934:   show "rel_cset R =
blanchet@54539:         (Grp {x. rcset x \<subseteq> Collect (split R)} (cimage fst))\<inverse>\<inverse> OO
blanchet@54539:          Grp {x. rcset x \<subseteq> Collect (split R)} (cimage snd)"
blanchet@55934:   unfolding rel_cset_def[abs_def] rel_cset_aux by simp
blanchet@54539: qed (transfer, simp)
blanchet@54539: 
blanchet@48975: end