1.1 --- a/src/HOL/BNF/BNF.thy	Wed Nov 20 18:58:00 2013 +0100
     1.2 +++ b/src/HOL/BNF/BNF.thy	Wed Nov 20 20:18:53 2013 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  header {* Bounded Natural Functors for (Co)datatypes *}
     1.5  
     1.6  theory BNF
     1.7 -imports More_BNFs BNF_LFP BNF_GFP Coinduction
     1.8 +imports Countable_Set_Type BNF_LFP BNF_GFP Coinduction
     1.9  begin
    1.10  
    1.11  hide_const (open) image2 image2p vimage2p Gr Grp collect fsts snds setl setr 

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/BNF/Countable_Set_Type.thy	Wed Nov 20 20:18:53 2013 +0100
     2.3 @@ -0,0 +1,212 @@
     2.4 +(*  Title:      HOL/BNF/Countable_Set_Type.thy
     2.5 +    Author:     Andrei Popescu, TU Muenchen
     2.6 +    Copyright   2012
     2.7 +
     2.8 +Type of (at most) countable sets.
     2.9 +*)
    2.10 +
    2.11 +header {* Type of (at Most) Countable Sets *}
    2.12 +
    2.13 +theory Countable_Set_Type
    2.14 +imports
    2.15 +  More_BNFs
    2.16 +  "~~/src/HOL/Cardinals/Cardinals"
    2.17 +  "~~/src/HOL/Library/Countable_Set"
    2.18 +begin
    2.19 +
    2.20 +subsection{* Cardinal stuff *}
    2.21 +
    2.22 +lemma countable_card_of_nat: "countable A \<longleftrightarrow> |A| \<le>o |UNIV::nat set|"
    2.23 +  unfolding countable_def card_of_ordLeq[symmetric] by auto
    2.24 +
    2.25 +lemma countable_card_le_natLeq: "countable A \<longleftrightarrow> |A| \<le>o natLeq"
    2.26 +  unfolding countable_card_of_nat using card_of_nat ordLeq_ordIso_trans ordIso_symmetric by blast
    2.27 +
    2.28 +lemma countable_or_card_of:
    2.29 +assumes "countable A"
    2.30 +shows "(finite A \<and> |A| <o |UNIV::nat set| ) \<or>
    2.31 +       (infinite A  \<and> |A| =o |UNIV::nat set| )"
    2.32 +proof (cases "finite A")
    2.33 +  case True thus ?thesis by (metis finite_iff_cardOf_nat)
    2.34 +next
    2.35 +  case False with assms show ?thesis
    2.36 +    by (metis countable_card_of_nat infinite_iff_card_of_nat ordIso_iff_ordLeq)
    2.37 +qed
    2.38 +
    2.39 +lemma countable_cases_card_of[elim]:
    2.40 +  assumes "countable A"
    2.41 +  obtains (Fin) "finite A" "|A| <o |UNIV::nat set|"
    2.42 +        | (Inf) "infinite A" "|A| =o |UNIV::nat set|"
    2.43 +  using assms countable_or_card_of by blast
    2.44 +
    2.45 +lemma countable_or:
    2.46 +  "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)"
    2.47 +  by (elim countable_enum_cases) fastforce+
    2.48 +
    2.49 +lemma countable_cases[elim]:
    2.50 +  assumes "countable A"
    2.51 +  obtains (Fin) f :: "'a\<Rightarrow>nat" where "finite A" "inj_on f A"
    2.52 +        | (Inf) f :: "'a\<Rightarrow>nat" where "infinite A" "bij_betw f A UNIV"
    2.53 +  using assms countable_or by metis
    2.54 +
    2.55 +lemma countable_ordLeq:
    2.56 +assumes "|A| \<le>o |B|" and "countable B"
    2.57 +shows "countable A"
    2.58 +using assms unfolding countable_card_of_nat by(rule ordLeq_transitive)
    2.59 +
    2.60 +lemma countable_ordLess:
    2.61 +assumes AB: "|A| <o |B|" and B: "countable B"
    2.62 +shows "countable A"
    2.63 +using countable_ordLeq[OF ordLess_imp_ordLeq[OF AB] B] .
    2.64 +
    2.65 +subsection {* The type of countable sets *}
    2.66 +
    2.67 +typedef 'a cset = "{A :: 'a set. countable A}" morphisms rcset acset
    2.68 +  by (rule exI[of _ "{}"]) simp
    2.69 +
    2.70 +setup_lifting type_definition_cset
    2.71 +
    2.72 +declare
    2.73 +  rcset_inverse[simp]
    2.74 +  acset_inverse[Transfer.transferred, unfolded mem_Collect_eq, simp]
    2.75 +  acset_inject[Transfer.transferred, unfolded mem_Collect_eq, simp]
    2.76 +  rcset[Transfer.transferred, unfolded mem_Collect_eq, simp]
    2.77 +
    2.78 +lift_definition cin :: "'a \<Rightarrow> 'a cset \<Rightarrow> bool" is "op \<in>" parametric member_transfer
    2.79 +  ..
    2.80 +lift_definition cempty :: "'a cset" is "{}" parametric empty_transfer
    2.81 +  by (rule countable_empty)
    2.82 +lift_definition cinsert :: "'a \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is insert parametric Lifting_Set.insert_transfer
    2.83 +  by (rule countable_insert)
    2.84 +lift_definition csingle :: "'a \<Rightarrow> 'a cset" is "\<lambda>x. {x}"
    2.85 +  by (rule countable_insert[OF countable_empty])
    2.86 +lift_definition cUn :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op \<union>" parametric union_transfer
    2.87 +  by (rule countable_Un)
    2.88 +lift_definition cInt :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op \<inter>" parametric inter_transfer
    2.89 +  by (rule countable_Int1)
    2.90 +lift_definition cDiff :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op -" parametric Diff_transfer
    2.91 +  by (rule countable_Diff)
    2.92 +lift_definition cimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a cset \<Rightarrow> 'b cset" is "op `" parametric image_transfer
    2.93 +  by (rule countable_image)
    2.94 +
    2.95 +subsection {* Registration as BNF *}
    2.96 +
    2.97 +lemma card_of_countable_sets_range:
    2.98 +fixes A :: "'a set"
    2.99 +shows "|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |{f::nat \<Rightarrow> 'a. range f \<subseteq> A}|"
   2.100 +apply(rule card_of_ordLeqI[of from_nat_into]) using inj_on_from_nat_into
   2.101 +unfolding inj_on_def by auto
   2.102 +
   2.103 +lemma card_of_countable_sets_Func:
   2.104 +"|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |A| ^c natLeq"
   2.105 +using card_of_countable_sets_range card_of_Func_UNIV[THEN ordIso_symmetric]
   2.106 +unfolding cexp_def Field_natLeq Field_card_of
   2.107 +by (rule ordLeq_ordIso_trans)
   2.108 +
   2.109 +lemma ordLeq_countable_subsets:
   2.110 +"|A| \<le>o |{X. X \<subseteq> A \<and> countable X}|"
   2.111 +apply (rule card_of_ordLeqI[of "\<lambda> a. {a}"]) unfolding inj_on_def by auto
   2.112 +
   2.113 +lemma finite_countable_subset:
   2.114 +"finite {X. X \<subseteq> A \<and> countable X} \<longleftrightarrow> finite A"
   2.115 +apply default
   2.116 + apply (erule contrapos_pp)
   2.117 + apply (rule card_of_ordLeq_infinite)
   2.118 + apply (rule ordLeq_countable_subsets)
   2.119 + apply assumption
   2.120 +apply (rule finite_Collect_conjI)
   2.121 +apply (rule disjI1)
   2.122 +by (erule finite_Collect_subsets)
   2.123 +
   2.124 +lemma rcset_to_rcset: "countable A \<Longrightarrow> rcset (the_inv rcset A) = A"
   2.125 +  apply (rule f_the_inv_into_f[unfolded inj_on_def image_iff])
   2.126 +   apply transfer' apply simp
   2.127 +  apply transfer' apply simp
   2.128 +  done
   2.129 +
   2.130 +lemma Collect_Int_Times:
   2.131 +"{(x, y). R x y} \<inter> A \<times> B = {(x, y). R x y \<and> x \<in> A \<and> y \<in> B}"
   2.132 +by auto
   2.133 +
   2.134 +definition cset_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a cset \<Rightarrow> 'b cset \<Rightarrow> bool" where
   2.135 +"cset_rel R a b \<longleftrightarrow>
   2.136 + (\<forall>t \<in> rcset a. \<exists>u \<in> rcset b. R t u) \<and>
   2.137 + (\<forall>t \<in> rcset b. \<exists>u \<in> rcset a. R u t)"
   2.138 +
   2.139 +lemma cset_rel_aux:
   2.140 +"(\<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>
   2.141 + ((Grp {x. rcset x \<subseteq> {(a, b). R a b}} (cimage fst))\<inverse>\<inverse> OO
   2.142 +          Grp {x. rcset x \<subseteq> {(a, b). R a b}} (cimage snd)) a b" (is "?L = ?R")
   2.143 +proof
   2.144 +  assume ?L
   2.145 +  def R' \<equiv> "the_inv rcset (Collect (split R) \<inter> (rcset a \<times> rcset b))"
   2.146 +  (is "the_inv rcset ?L'")
   2.147 +  have L: "countable ?L'" by auto
   2.148 +  hence *: "rcset R' = ?L'" unfolding R'_def using fset_to_fset by (intro rcset_to_rcset)
   2.149 +  thus ?R unfolding Grp_def relcompp.simps conversep.simps
   2.150 +  proof (intro CollectI prod_caseI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
   2.151 +    from * `?L` show "a = cimage fst R'" by transfer (auto simp: image_def Collect_Int_Times)
   2.152 +  next
   2.153 +    from * `?L` show "b = cimage snd R'" by transfer (auto simp: image_def Collect_Int_Times)
   2.154 +  qed simp_all
   2.155 +next
   2.156 +  assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps
   2.157 +    by transfer force
   2.158 +qed
   2.159 +
   2.160 +bnf "'a cset"
   2.161 +  map: cimage
   2.162 +  sets: rcset
   2.163 +  bd: natLeq
   2.164 +  wits: "cempty"
   2.165 +  rel: cset_rel
   2.166 +proof -
   2.167 +  show "cimage id = id" by transfer' simp
   2.168 +next
   2.169 +  fix f g show "cimage (g \<circ> f) = cimage g \<circ> cimage f" by transfer' fastforce
   2.170 +next
   2.171 +  fix C f g assume eq: "\<And>a. a \<in> rcset C \<Longrightarrow> f a = g a"
   2.172 +  thus "cimage f C = cimage g C" by transfer force
   2.173 +next
   2.174 +  fix f show "rcset \<circ> cimage f = op ` f \<circ> rcset" by transfer' fastforce
   2.175 +next
   2.176 +  show "card_order natLeq" by (rule natLeq_card_order)
   2.177 +next
   2.178 +  show "cinfinite natLeq" by (rule natLeq_cinfinite)
   2.179 +next
   2.180 +  fix C show "|rcset C| \<le>o natLeq" by transfer (unfold countable_card_le_natLeq)
   2.181 +next
   2.182 +  fix A B1 B2 f1 f2 p1 p2
   2.183 +  assume wp: "wpull A B1 B2 f1 f2 p1 p2"
   2.184 +  show "wpull {x. rcset x \<subseteq> A} {x. rcset x \<subseteq> B1} {x. rcset x \<subseteq> B2}
   2.185 +              (cimage f1) (cimage f2) (cimage p1) (cimage p2)"
   2.186 +  unfolding wpull_def proof safe
   2.187 +    fix y1 y2
   2.188 +    assume Y1: "rcset y1 \<subseteq> B1" and Y2: "rcset y2 \<subseteq> B2"
   2.189 +    assume "cimage f1 y1 = cimage f2 y2"
   2.190 +    hence EQ: "f1 ` (rcset y1) = f2 ` (rcset y2)" by transfer
   2.191 +    with Y1 Y2 obtain X where X: "X \<subseteq> A"
   2.192 +    and Y1: "p1 ` X = rcset y1" and Y2: "p2 ` X = rcset y2"
   2.193 +    using wpull_image[OF wp] unfolding wpull_def Pow_def Bex_def mem_Collect_eq
   2.194 +      by (auto elim!: allE[of _ "rcset y1"] allE[of _ "rcset y2"])
   2.195 +    have "\<forall> y1' \<in> rcset y1. \<exists> x. x \<in> X \<and> y1' = p1 x" using Y1 by auto
   2.196 +    then obtain q1 where q1: "\<forall> y1' \<in> rcset y1. q1 y1' \<in> X \<and> y1' = p1 (q1 y1')" by metis
   2.197 +    have "\<forall> y2' \<in> rcset y2. \<exists> x. x \<in> X \<and> y2' = p2 x" using Y2 by auto
   2.198 +    then obtain q2 where q2: "\<forall> y2' \<in> rcset y2. q2 y2' \<in> X \<and> y2' = p2 (q2 y2')" by metis
   2.199 +    def X' \<equiv> "q1 ` (rcset y1) \<union> q2 ` (rcset y2)"
   2.200 +    have X': "X' \<subseteq> A" and Y1: "p1 ` X' = rcset y1" and Y2: "p2 ` X' = rcset y2"
   2.201 +    using X Y1 Y2 q1 q2 unfolding X'_def by fast+
   2.202 +    have fX': "countable X'" unfolding X'_def by simp
   2.203 +    then obtain x where X'eq: "X' = rcset x" by transfer blast
   2.204 +    show "\<exists>x\<in>{x. rcset x \<subseteq> A}. cimage p1 x = y1 \<and> cimage p2 x = y2"
   2.205 +      using X' Y1 Y2 unfolding X'eq by (intro bexI[of _ "x"]) (transfer, auto)
   2.206 +  qed
   2.207 +next
   2.208 +  fix R
   2.209 +  show "cset_rel R =
   2.210 +        (Grp {x. rcset x \<subseteq> Collect (split R)} (cimage fst))\<inverse>\<inverse> OO
   2.211 +         Grp {x. rcset x \<subseteq> Collect (split R)} (cimage snd)"
   2.212 +  unfolding cset_rel_def[abs_def] cset_rel_aux by simp
   2.213 +qed (transfer, simp)
   2.214 +
   2.215 +end

     3.1 --- a/src/HOL/BNF/Countable_Type.thy	Wed Nov 20 18:58:00 2013 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,91 +0,0 @@
     3.4 -(*  Title:      HOL/BNF/Countable_Type.thy
     3.5 -    Author:     Andrei Popescu, TU Muenchen
     3.6 -    Copyright   2012
     3.7 -
     3.8 -(At most) countable sets.
     3.9 -*)
    3.10 -
    3.11 -header {* (At Most) Countable Sets *}
    3.12 -
    3.13 -theory Countable_Type
    3.14 -imports
    3.15 -  "~~/src/HOL/Cardinals/Cardinals"
    3.16 -  "~~/src/HOL/Library/Countable_Set"
    3.17 -begin
    3.18 -
    3.19 -subsection{* Cardinal stuff *}
    3.20 -
    3.21 -lemma countable_card_of_nat: "countable A \<longleftrightarrow> |A| \<le>o |UNIV::nat set|"
    3.22 -  unfolding countable_def card_of_ordLeq[symmetric] by auto
    3.23 -
    3.24 -lemma countable_card_le_natLeq: "countable A \<longleftrightarrow> |A| \<le>o natLeq"
    3.25 -  unfolding countable_card_of_nat using card_of_nat ordLeq_ordIso_trans ordIso_symmetric by blast
    3.26 -
    3.27 -lemma countable_or_card_of:
    3.28 -assumes "countable A"
    3.29 -shows "(finite A \<and> |A| <o |UNIV::nat set| ) \<or>
    3.30 -       (infinite A  \<and> |A| =o |UNIV::nat set| )"
    3.31 -proof (cases "finite A")
    3.32 -  case True thus ?thesis by (metis finite_iff_cardOf_nat)
    3.33 -next
    3.34 -  case False with assms show ?thesis
    3.35 -    by (metis countable_card_of_nat infinite_iff_card_of_nat ordIso_iff_ordLeq)
    3.36 -qed
    3.37 -
    3.38 -lemma countable_cases_card_of[elim]:
    3.39 -  assumes "countable A"
    3.40 -  obtains (Fin) "finite A" "|A| <o |UNIV::nat set|"
    3.41 -        | (Inf) "infinite A" "|A| =o |UNIV::nat set|"
    3.42 -  using assms countable_or_card_of by blast
    3.43 -
    3.44 -lemma countable_or:
    3.45 -  "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)"
    3.46 -  by (elim countable_enum_cases) fastforce+
    3.47 -
    3.48 -lemma countable_cases[elim]:
    3.49 -  assumes "countable A"
    3.50 -  obtains (Fin) f :: "'a\<Rightarrow>nat" where "finite A" "inj_on f A"
    3.51 -        | (Inf) f :: "'a\<Rightarrow>nat" where "infinite A" "bij_betw f A UNIV"
    3.52 -  using assms countable_or by metis
    3.53 -
    3.54 -lemma countable_ordLeq:
    3.55 -assumes "|A| \<le>o |B|" and "countable B"
    3.56 -shows "countable A"
    3.57 -using assms unfolding countable_card_of_nat by(rule ordLeq_transitive)
    3.58 -
    3.59 -lemma countable_ordLess:
    3.60 -assumes AB: "|A| <o |B|" and B: "countable B"
    3.61 -shows "countable A"
    3.62 -using countable_ordLeq[OF ordLess_imp_ordLeq[OF AB] B] .
    3.63 -
    3.64 -subsection{*  The type of countable sets *}
    3.65 -
    3.66 -typedef 'a cset = "{A :: 'a set. countable A}" morphisms rcset acset
    3.67 -  by (rule exI[of _ "{}"]) simp
    3.68 -
    3.69 -setup_lifting type_definition_cset
    3.70 -
    3.71 -declare
    3.72 -  rcset_inverse[simp]
    3.73 -  acset_inverse[Transfer.transferred, unfolded mem_Collect_eq, simp]
    3.74 -  acset_inject[Transfer.transferred, unfolded mem_Collect_eq, simp]
    3.75 -  rcset[Transfer.transferred, unfolded mem_Collect_eq, simp]
    3.76 -
    3.77 -lift_definition cin :: "'a \<Rightarrow> 'a cset \<Rightarrow> bool" is "op \<in>" parametric member_transfer
    3.78 -  ..
    3.79 -lift_definition cempty :: "'a cset" is "{}" parametric empty_transfer
    3.80 -  by (rule countable_empty)
    3.81 -lift_definition cinsert :: "'a \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is insert parametric Lifting_Set.insert_transfer
    3.82 -  by (rule countable_insert)
    3.83 -lift_definition csingle :: "'a \<Rightarrow> 'a cset" is "\<lambda>x. {x}"
    3.84 -  by (rule countable_insert[OF countable_empty])
    3.85 -lift_definition cUn :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op \<union>" parametric union_transfer
    3.86 -  by (rule countable_Un)
    3.87 -lift_definition cInt :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op \<inter>" parametric inter_transfer
    3.88 -  by (rule countable_Int1)
    3.89 -lift_definition cDiff :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op -" parametric Diff_transfer
    3.90 -  by (rule countable_Diff)
    3.91 -lift_definition cimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a cset \<Rightarrow> 'b cset" is "op `" parametric image_transfer
    3.92 -  by (rule countable_image)
    3.93 -
    3.94 -end

     4.1 --- a/src/HOL/BNF/More_BNFs.thy	Wed Nov 20 18:58:00 2013 +0100
     4.2 +++ b/src/HOL/BNF/More_BNFs.thy	Wed Nov 20 20:18:53 2013 +0100
     4.3 @@ -15,7 +15,6 @@
     4.4    Basic_BNFs
     4.5    "~~/src/HOL/Library/FSet"
     4.6    "~~/src/HOL/Library/Multiset"
     4.7 -  Countable_Type
     4.8  begin
     4.9  
    4.10  lemma option_rec_conv_option_case: "option_rec = option_case"
    4.11 @@ -134,6 +133,7 @@
    4.12      by (force simp: zip_map_fst_snd)
    4.13  qed (simp add: wpull_map)+
    4.14  
    4.15 +
    4.16  (* Finite sets *)
    4.17  
    4.18  lemma wpull_image:
    4.19 @@ -257,126 +257,6 @@
    4.20  
    4.21  lemmas [simp] = fset.map_comp fset.map_id fset.set_map
    4.22  
    4.23 -(* Countable sets *)
    4.24 -
    4.25 -lemma card_of_countable_sets_range:
    4.26 -fixes A :: "'a set"
    4.27 -shows "|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |{f::nat \<Rightarrow> 'a. range f \<subseteq> A}|"
    4.28 -apply(rule card_of_ordLeqI[of from_nat_into]) using inj_on_from_nat_into
    4.29 -unfolding inj_on_def by auto
    4.30 -
    4.31 -lemma card_of_countable_sets_Func:
    4.32 -"|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |A| ^c natLeq"
    4.33 -using card_of_countable_sets_range card_of_Func_UNIV[THEN ordIso_symmetric]
    4.34 -unfolding cexp_def Field_natLeq Field_card_of
    4.35 -by (rule ordLeq_ordIso_trans)
    4.36 -
    4.37 -lemma ordLeq_countable_subsets:
    4.38 -"|A| \<le>o |{X. X \<subseteq> A \<and> countable X}|"
    4.39 -apply (rule card_of_ordLeqI[of "\<lambda> a. {a}"]) unfolding inj_on_def by auto
    4.40 -
    4.41 -lemma finite_countable_subset:
    4.42 -"finite {X. X \<subseteq> A \<and> countable X} \<longleftrightarrow> finite A"
    4.43 -apply default
    4.44 - apply (erule contrapos_pp)
    4.45 - apply (rule card_of_ordLeq_infinite)
    4.46 - apply (rule ordLeq_countable_subsets)
    4.47 - apply assumption
    4.48 -apply (rule finite_Collect_conjI)
    4.49 -apply (rule disjI1)
    4.50 -by (erule finite_Collect_subsets)
    4.51 -
    4.52 -lemma rcset_to_rcset: "countable A \<Longrightarrow> rcset (the_inv rcset A) = A"
    4.53 -  apply (rule f_the_inv_into_f[unfolded inj_on_def image_iff])
    4.54 -   apply transfer' apply simp
    4.55 -  apply transfer' apply simp
    4.56 -  done
    4.57 -
    4.58 -lemma Collect_Int_Times:
    4.59 -"{(x, y). R x y} \<inter> A \<times> B = {(x, y). R x y \<and> x \<in> A \<and> y \<in> B}"
    4.60 -by auto
    4.61 -
    4.62 -definition cset_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a cset \<Rightarrow> 'b cset \<Rightarrow> bool" where
    4.63 -"cset_rel R a b \<longleftrightarrow>
    4.64 - (\<forall>t \<in> rcset a. \<exists>u \<in> rcset b. R t u) \<and>
    4.65 - (\<forall>t \<in> rcset b. \<exists>u \<in> rcset a. R u t)"
    4.66 -
    4.67 -lemma cset_rel_aux:
    4.68 -"(\<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>
    4.69 - ((Grp {x. rcset x \<subseteq> {(a, b). R a b}} (cimage fst))\<inverse>\<inverse> OO
    4.70 -          Grp {x. rcset x \<subseteq> {(a, b). R a b}} (cimage snd)) a b" (is "?L = ?R")
    4.71 -proof
    4.72 -  assume ?L
    4.73 -  def R' \<equiv> "the_inv rcset (Collect (split R) \<inter> (rcset a \<times> rcset b))"
    4.74 -  (is "the_inv rcset ?L'")
    4.75 -  have L: "countable ?L'" by auto
    4.76 -  hence *: "rcset R' = ?L'" unfolding R'_def using fset_to_fset by (intro rcset_to_rcset)
    4.77 -  thus ?R unfolding Grp_def relcompp.simps conversep.simps
    4.78 -  proof (intro CollectI prod_caseI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
    4.79 -    from * `?L` show "a = cimage fst R'" by transfer (auto simp: image_def Collect_Int_Times)
    4.80 -  next
    4.81 -    from * `?L` show "b = cimage snd R'" by transfer (auto simp: image_def Collect_Int_Times)
    4.82 -  qed simp_all
    4.83 -next
    4.84 -  assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps
    4.85 -    by transfer force
    4.86 -qed
    4.87 -
    4.88 -bnf "'a cset"
    4.89 -  map: cimage
    4.90 -  sets: rcset
    4.91 -  bd: natLeq
    4.92 -  wits: "cempty"
    4.93 -  rel: cset_rel
    4.94 -proof -
    4.95 -  show "cimage id = id" by transfer' simp
    4.96 -next
    4.97 -  fix f g show "cimage (g \<circ> f) = cimage g \<circ> cimage f" by transfer' fastforce
    4.98 -next
    4.99 -  fix C f g assume eq: "\<And>a. a \<in> rcset C \<Longrightarrow> f a = g a"
   4.100 -  thus "cimage f C = cimage g C" by transfer force
   4.101 -next
   4.102 -  fix f show "rcset \<circ> cimage f = op ` f \<circ> rcset" by transfer' fastforce
   4.103 -next
   4.104 -  show "card_order natLeq" by (rule natLeq_card_order)
   4.105 -next
   4.106 -  show "cinfinite natLeq" by (rule natLeq_cinfinite)
   4.107 -next
   4.108 -  fix C show "|rcset C| \<le>o natLeq" by transfer (unfold countable_card_le_natLeq)
   4.109 -next
   4.110 -  fix A B1 B2 f1 f2 p1 p2
   4.111 -  assume wp: "wpull A B1 B2 f1 f2 p1 p2"
   4.112 -  show "wpull {x. rcset x \<subseteq> A} {x. rcset x \<subseteq> B1} {x. rcset x \<subseteq> B2}
   4.113 -              (cimage f1) (cimage f2) (cimage p1) (cimage p2)"
   4.114 -  unfolding wpull_def proof safe
   4.115 -    fix y1 y2
   4.116 -    assume Y1: "rcset y1 \<subseteq> B1" and Y2: "rcset y2 \<subseteq> B2"
   4.117 -    assume "cimage f1 y1 = cimage f2 y2"
   4.118 -    hence EQ: "f1 ` (rcset y1) = f2 ` (rcset y2)" by transfer
   4.119 -    with Y1 Y2 obtain X where X: "X \<subseteq> A"
   4.120 -    and Y1: "p1 ` X = rcset y1" and Y2: "p2 ` X = rcset y2"
   4.121 -    using wpull_image[OF wp] unfolding wpull_def Pow_def Bex_def mem_Collect_eq
   4.122 -      by (auto elim!: allE[of _ "rcset y1"] allE[of _ "rcset y2"])
   4.123 -    have "\<forall> y1' \<in> rcset y1. \<exists> x. x \<in> X \<and> y1' = p1 x" using Y1 by auto
   4.124 -    then obtain q1 where q1: "\<forall> y1' \<in> rcset y1. q1 y1' \<in> X \<and> y1' = p1 (q1 y1')" by metis
   4.125 -    have "\<forall> y2' \<in> rcset y2. \<exists> x. x \<in> X \<and> y2' = p2 x" using Y2 by auto
   4.126 -    then obtain q2 where q2: "\<forall> y2' \<in> rcset y2. q2 y2' \<in> X \<and> y2' = p2 (q2 y2')" by metis
   4.127 -    def X' \<equiv> "q1 ` (rcset y1) \<union> q2 ` (rcset y2)"
   4.128 -    have X': "X' \<subseteq> A" and Y1: "p1 ` X' = rcset y1" and Y2: "p2 ` X' = rcset y2"
   4.129 -    using X Y1 Y2 q1 q2 unfolding X'_def by fast+
   4.130 -    have fX': "countable X'" unfolding X'_def by simp
   4.131 -    then obtain x where X'eq: "X' = rcset x" by transfer blast
   4.132 -    show "\<exists>x\<in>{x. rcset x \<subseteq> A}. cimage p1 x = y1 \<and> cimage p2 x = y2"
   4.133 -      using X' Y1 Y2 unfolding X'eq by (intro bexI[of _ "x"]) (transfer, auto)
   4.134 -  qed
   4.135 -next
   4.136 -  fix R
   4.137 -  show "cset_rel R =
   4.138 -        (Grp {x. rcset x \<subseteq> Collect (split R)} (cimage fst))\<inverse>\<inverse> OO
   4.139 -         Grp {x. rcset x \<subseteq> Collect (split R)} (cimage snd)"
   4.140 -  unfolding cset_rel_def[abs_def] cset_rel_aux by simp
   4.141 -qed (transfer, simp)
   4.142 -
   4.143  
   4.144  (* Multisets *)
   4.145  
   4.146 @@ -1115,7 +995,6 @@
   4.147           rel_multiset'.induct[unfolded rel_multiset_rel_multiset'[symmetric]]
   4.148  
   4.149  
   4.150 -
   4.151  (* Advanced relator customization *)
   4.152  
   4.153  (* Set vs. sum relators: *)