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