split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
authorblanchet
Wed Sep 12 05:21:47 2012 +0200 (2012-09-12)
changeset 49309f20b24214ac2
parent 49308 6190b701e4f4
child 49310 6e30078de4f0
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
src/HOL/Codatatype/BNF_Comp.thy
src/HOL/Codatatype/BNF_Def.thy
src/HOL/Codatatype/BNF_FP.thy
src/HOL/Codatatype/BNF_GFP.thy
src/HOL/Codatatype/BNF_LFP.thy
src/HOL/Codatatype/BNF_Util.thy
src/HOL/Codatatype/BNF_Wrap.thy
src/HOL/Codatatype/Basic_BNFs.thy
src/HOL/Codatatype/Codatatype.thy
src/HOL/Codatatype/More_BNFs.thy
     1.1 --- a/src/HOL/Codatatype/BNF_Comp.thy	Wed Sep 12 05:03:18 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/BNF_Comp.thy	Wed Sep 12 05:21:47 2012 +0200
     1.3 @@ -9,9 +9,9 @@
     1.4  
     1.5  theory BNF_Comp
     1.6  imports Basic_BNFs
     1.7 -uses
     1.8 -  "Tools/bnf_comp_tactics.ML"
     1.9 -  "Tools/bnf_comp.ML"
    1.10  begin
    1.11  
    1.12 +ML_file "Tools/bnf_comp_tactics.ML"
    1.13 +ML_file "Tools/bnf_comp.ML"
    1.14 +
    1.15  end
     2.1 --- a/src/HOL/Codatatype/BNF_Def.thy	Wed Sep 12 05:03:18 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/BNF_Def.thy	Wed Sep 12 05:21:47 2012 +0200
     2.3 @@ -12,9 +12,9 @@
     2.4  keywords
     2.5    "print_bnfs" :: diag and
     2.6    "bnf_def" :: thy_goal
     2.7 -uses
     2.8 -  "Tools/bnf_def_tactics.ML"
     2.9 -  "Tools/bnf_def.ML"
    2.10  begin
    2.11  
    2.12 +ML_file "Tools/bnf_def_tactics.ML"
    2.13 +ML_file"Tools/bnf_def.ML"
    2.14 +
    2.15  end
     3.1 --- a/src/HOL/Codatatype/BNF_FP.thy	Wed Sep 12 05:03:18 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/BNF_FP.thy	Wed Sep 12 05:21:47 2012 +0200
     3.3 @@ -12,10 +12,10 @@
     3.4  imports BNF_Comp BNF_Wrap
     3.5  keywords
     3.6    "defaults"
     3.7 -uses
     3.8 -  "Tools/bnf_fp_util.ML"
     3.9 -  "Tools/bnf_fp_sugar_tactics.ML"
    3.10 -  "Tools/bnf_fp_sugar.ML"
    3.11  begin
    3.12  
    3.13 +ML_file "Tools/bnf_fp_util.ML"
    3.14 +ML_file "Tools/bnf_fp_sugar_tactics.ML"
    3.15 +ML_file "Tools/bnf_fp_sugar.ML"
    3.16 +
    3.17  end
     4.1 --- a/src/HOL/Codatatype/BNF_GFP.thy	Wed Sep 12 05:03:18 2012 +0200
     4.2 +++ b/src/HOL/Codatatype/BNF_GFP.thy	Wed Sep 12 05:21:47 2012 +0200
     4.3 @@ -12,10 +12,10 @@
     4.4  keywords
     4.5    "codata_raw" :: thy_decl and
     4.6    "codata" :: thy_decl
     4.7 -uses
     4.8 -  "Tools/bnf_gfp_util.ML"
     4.9 -  "Tools/bnf_gfp_tactics.ML"
    4.10 -  "Tools/bnf_gfp.ML"
    4.11  begin
    4.12  
    4.13 +ML_file "Tools/bnf_gfp_util.ML"
    4.14 +ML_file "Tools/bnf_gfp_tactics.ML"
    4.15 +ML_file "Tools/bnf_gfp.ML"
    4.16 +
    4.17  end
     5.1 --- a/src/HOL/Codatatype/BNF_LFP.thy	Wed Sep 12 05:03:18 2012 +0200
     5.2 +++ b/src/HOL/Codatatype/BNF_LFP.thy	Wed Sep 12 05:21:47 2012 +0200
     5.3 @@ -12,10 +12,10 @@
     5.4  keywords
     5.5    "data_raw" :: thy_decl and
     5.6    "data" :: thy_decl
     5.7 -uses
     5.8 -  "Tools/bnf_lfp_util.ML"
     5.9 -  "Tools/bnf_lfp_tactics.ML"
    5.10 -  "Tools/bnf_lfp.ML"
    5.11  begin
    5.12  
    5.13 +ML_file "Tools/bnf_lfp_util.ML"
    5.14 +ML_file "Tools/bnf_lfp_tactics.ML"
    5.15 +ML_file "Tools/bnf_lfp.ML"
    5.16 +
    5.17  end
     6.1 --- a/src/HOL/Codatatype/BNF_Util.thy	Wed Sep 12 05:03:18 2012 +0200
     6.2 +++ b/src/HOL/Codatatype/BNF_Util.thy	Wed Sep 12 05:21:47 2012 +0200
     6.3 @@ -13,8 +13,6 @@
     6.4    "../Ordinals_and_Cardinals/Cardinal_Arithmetic"
     6.5    "~~/src/HOL/Library/Prefix_Order"
     6.6    Equiv_Relations_More
     6.7 -uses
     6.8 -  ("Tools/bnf_util.ML")
     6.9  begin
    6.10  
    6.11  lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
     7.1 --- a/src/HOL/Codatatype/BNF_Wrap.thy	Wed Sep 12 05:03:18 2012 +0200
     7.2 +++ b/src/HOL/Codatatype/BNF_Wrap.thy	Wed Sep 12 05:21:47 2012 +0200
     7.3 @@ -12,9 +12,9 @@
     7.4  keywords
     7.5    "wrap_data" :: thy_goal and
     7.6    "no_dests"
     7.7 -uses
     7.8 -  "Tools/bnf_wrap_tactics.ML"
     7.9 -  "Tools/bnf_wrap.ML"
    7.10  begin
    7.11  
    7.12 +ML_file "Tools/bnf_wrap_tactics.ML"
    7.13 +ML_file "Tools/bnf_wrap.ML"
    7.14 +
    7.15  end
     8.1 --- a/src/HOL/Codatatype/Basic_BNFs.thy	Wed Sep 12 05:03:18 2012 +0200
     8.2 +++ b/src/HOL/Codatatype/Basic_BNFs.thy	Wed Sep 12 05:21:47 2012 +0200
     8.3 @@ -4,10 +4,10 @@
     8.4      Author:     Jasmin Blanchette, TU Muenchen
     8.5      Copyright   2012
     8.6  
     8.7 -Registration of various types as bounded natural functors.
     8.8 +Registration of basic types as bounded natural functors.
     8.9  *)
    8.10  
    8.11 -header {* Registration of Various Types as Bounded Natural Functors *}
    8.12 +header {* Registration of Basic Types as Bounded Natural Functors *}
    8.13  
    8.14  theory Basic_BNFs
    8.15  imports BNF_Def "~~/src/HOL/Quotient_Examples/FSet" "~~/src/HOL/Library/Multiset" Countable_Set
    8.16 @@ -71,7 +71,6 @@
    8.17  unfolding DEADID_pred_def DEADID.rel_Id by simp
    8.18  
    8.19  ML {*
    8.20 -
    8.21  signature BASIC_BNFS =
    8.22  sig
    8.23    val ID_bnf: BNF_Def.BNF
    8.24 @@ -84,13 +83,12 @@
    8.25  structure Basic_BNFs : BASIC_BNFS =
    8.26  struct
    8.27  
    8.28 -  val ID_bnf = the (BNF_Def.bnf_of @{context} "ID");
    8.29 -  val DEADID_bnf = the (BNF_Def.bnf_of @{context} "DEADID");
    8.30 +val ID_bnf = the (BNF_Def.bnf_of @{context} "ID");
    8.31 +val DEADID_bnf = the (BNF_Def.bnf_of @{context} "DEADID");
    8.32  
    8.33 -  val rel_def = BNF_Def.rel_def_of_bnf ID_bnf;
    8.34 -  val ID_rel_def = rel_def RS sym;
    8.35 -  val ID_pred_def =
    8.36 -    Local_Defs.unfold @{context} [rel_def] (BNF_Def.pred_def_of_bnf ID_bnf) RS sym;
    8.37 +val rel_def = BNF_Def.rel_def_of_bnf ID_bnf;
    8.38 +val ID_rel_def = rel_def RS sym;
    8.39 +val ID_pred_def = Local_Defs.unfold @{context} [rel_def] (BNF_Def.pred_def_of_bnf ID_bnf) RS sym;
    8.40  
    8.41  end;
    8.42  *}
    8.43 @@ -422,1103 +420,4 @@
    8.44  unfolding fun_rel_def fun_pred_def Gr_def relcomp_unfold converse_unfold
    8.45  by (auto intro!: exI dest!: in_mono)
    8.46  
    8.47 -lemma card_of_list_in:
    8.48 -  "|{xs. set xs \<subseteq> A}| \<le>o |Pfunc (UNIV :: nat set) A|" (is "|?LHS| \<le>o |?RHS|")
    8.49 -proof -
    8.50 -  let ?f = "%xs. %i. if i < length xs \<and> set xs \<subseteq> A then Some (nth xs i) else None"
    8.51 -  have "inj_on ?f ?LHS" unfolding inj_on_def fun_eq_iff
    8.52 -  proof safe
    8.53 -    fix xs :: "'a list" and ys :: "'a list"
    8.54 -    assume su: "set xs \<subseteq> A" "set ys \<subseteq> A" and eq: "\<forall>i. ?f xs i = ?f ys i"
    8.55 -    hence *: "length xs = length ys"
    8.56 -    by (metis linorder_cases option.simps(2) order_less_irrefl)
    8.57 -    thus "xs = ys" by (rule nth_equalityI) (metis * eq su option.inject)
    8.58 -  qed
    8.59 -  moreover have "?f ` ?LHS \<subseteq> ?RHS" unfolding Pfunc_def by fastforce
    8.60 -  ultimately show ?thesis using card_of_ordLeq by blast
    8.61 -qed
    8.62 -
    8.63 -lemma list_in_empty: "A = {} \<Longrightarrow> {x. set x \<subseteq> A} = {[]}"
    8.64 -by simp
    8.65 -
    8.66 -lemma card_of_Func: "|Func A B| =o |B| ^c |A|"
    8.67 -unfolding cexp_def Field_card_of by (rule card_of_refl)
    8.68 -
    8.69 -lemma not_emp_czero_notIn_ordIso_Card_order:
    8.70 -"A \<noteq> {} \<Longrightarrow> ( |A|, czero) \<notin> ordIso \<and> Card_order |A|"
    8.71 -  apply (rule conjI)
    8.72 -  apply (metis Field_card_of czeroE)
    8.73 -  by (rule card_of_Card_order)
    8.74 -
    8.75 -lemma list_in_bd: "|{x. set x \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq"
    8.76 -proof -
    8.77 -  fix A :: "'a set"
    8.78 -  show "|{x. set x \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq"
    8.79 -  proof (cases "A = {}")
    8.80 -    case False thus ?thesis
    8.81 -      apply -
    8.82 -      apply (rule ordLeq_transitive)
    8.83 -      apply (rule card_of_list_in)
    8.84 -      apply (rule ordLeq_transitive)
    8.85 -      apply (erule card_of_Pfunc_Pow_Func)
    8.86 -      apply (rule ordIso_ordLeq_trans)
    8.87 -      apply (rule Times_cprod)
    8.88 -      apply (rule cprod_cinfinite_bound)
    8.89 -      apply (rule ordIso_ordLeq_trans)
    8.90 -      apply (rule Pow_cexp_ctwo)
    8.91 -      apply (rule ordIso_ordLeq_trans)
    8.92 -      apply (rule cexp_cong2)
    8.93 -      apply (rule card_of_nat)
    8.94 -      apply (rule Card_order_ctwo)
    8.95 -      apply (rule card_of_Card_order)
    8.96 -      apply (rule natLeq_Card_order)
    8.97 -      apply (rule disjI1)
    8.98 -      apply (rule ctwo_Cnotzero)
    8.99 -      apply (rule cexp_mono1)
   8.100 -      apply (rule ordLeq_csum2)
   8.101 -      apply (rule Card_order_ctwo)
   8.102 -      apply (rule disjI1)
   8.103 -      apply (rule ctwo_Cnotzero)
   8.104 -      apply (rule natLeq_Card_order)
   8.105 -      apply (rule ordIso_ordLeq_trans)
   8.106 -      apply (rule card_of_Func)
   8.107 -      apply (rule ordIso_ordLeq_trans)
   8.108 -      apply (rule cexp_cong2)
   8.109 -      apply (rule card_of_nat)
   8.110 -      apply (rule card_of_Card_order)
   8.111 -      apply (rule card_of_Card_order)
   8.112 -      apply (rule natLeq_Card_order)
   8.113 -      apply (rule disjI1)
   8.114 -      apply (erule not_emp_czero_notIn_ordIso_Card_order)
   8.115 -      apply (rule cexp_mono1)
   8.116 -      apply (rule ordLeq_csum1)
   8.117 -      apply (rule card_of_Card_order)
   8.118 -      apply (rule disjI1)
   8.119 -      apply (erule not_emp_czero_notIn_ordIso_Card_order)
   8.120 -      apply (rule natLeq_Card_order)
   8.121 -      apply (rule card_of_Card_order)
   8.122 -      apply (rule card_of_Card_order)
   8.123 -      apply (rule Cinfinite_cexp)
   8.124 -      apply (rule ordLeq_csum2)
   8.125 -      apply (rule Card_order_ctwo)
   8.126 -      apply (rule conjI)
   8.127 -      apply (rule natLeq_cinfinite)
   8.128 -      by (rule natLeq_Card_order)
   8.129 -  next
   8.130 -    case True thus ?thesis
   8.131 -      apply -
   8.132 -      apply (rule ordIso_ordLeq_trans)
   8.133 -      apply (rule card_of_ordIso_subst)
   8.134 -      apply (erule list_in_empty)
   8.135 -      apply (rule ordIso_ordLeq_trans)
   8.136 -      apply (rule single_cone)
   8.137 -      apply (rule cone_ordLeq_cexp)
   8.138 -      apply (rule ordLeq_transitive)
   8.139 -      apply (rule cone_ordLeq_ctwo)
   8.140 -      apply (rule ordLeq_csum2)
   8.141 -      by (rule Card_order_ctwo)
   8.142 -  qed
   8.143 -qed
   8.144 -
   8.145 -bnf_def list = map [set] "\<lambda>_::'a list. natLeq" ["[]"]
   8.146 -proof -
   8.147 -  show "map id = id" by (rule List.map.id)
   8.148 -next
   8.149 -  fix f g
   8.150 -  show "map (g o f) = map g o map f" by (rule List.map.comp[symmetric])
   8.151 -next
   8.152 -  fix x f g
   8.153 -  assume "\<And>z. z \<in> set x \<Longrightarrow> f z = g z"
   8.154 -  thus "map f x = map g x" by simp
   8.155 -next
   8.156 -  fix f
   8.157 -  show "set o map f = image f o set" by (rule ext, unfold o_apply, rule set_map)
   8.158 -next
   8.159 -  show "card_order natLeq" by (rule natLeq_card_order)
   8.160 -next
   8.161 -  show "cinfinite natLeq" by (rule natLeq_cinfinite)
   8.162 -next
   8.163 -  fix x
   8.164 -  show "|set x| \<le>o natLeq"
   8.165 -    apply (rule ordLess_imp_ordLeq)
   8.166 -    apply (rule finite_ordLess_infinite[OF _ natLeq_Well_order])
   8.167 -    unfolding Field_natLeq Field_card_of by (auto simp: card_of_well_order_on)
   8.168 -next
   8.169 -  fix A :: "'a set"
   8.170 -  show "|{x. set x \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" by (rule list_in_bd)
   8.171 -next
   8.172 -  fix A B1 B2 f1 f2 p1 p2
   8.173 -  assume "wpull A B1 B2 f1 f2 p1 p2"
   8.174 -  hence pull: "\<And>b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<Longrightarrow> \<exists>a \<in> A. p1 a = b1 \<and> p2 a = b2"
   8.175 -    unfolding wpull_def by auto
   8.176 -  show "wpull {x. set x \<subseteq> A} {x. set x \<subseteq> B1} {x. set x \<subseteq> B2} (map f1) (map f2) (map p1) (map p2)"
   8.177 -    (is "wpull ?A ?B1 ?B2 _ _ _ _")
   8.178 -  proof (unfold wpull_def)
   8.179 -    { fix as bs assume *: "as \<in> ?B1" "bs \<in> ?B2" "map f1 as = map f2 bs"
   8.180 -      hence "length as = length bs" by (metis length_map)
   8.181 -      hence "\<exists>zs \<in> ?A. map p1 zs = as \<and> map p2 zs = bs" using *
   8.182 -      proof (induct as bs rule: list_induct2)
   8.183 -        case (Cons a as b bs)
   8.184 -        hence "a \<in> B1" "b \<in> B2" "f1 a = f2 b" by auto
   8.185 -        with pull obtain z where "z \<in> A" "p1 z = a" "p2 z = b" by blast
   8.186 -        moreover
   8.187 -        from Cons obtain zs where "zs \<in> ?A" "map p1 zs = as" "map p2 zs = bs" by auto
   8.188 -        ultimately have "z # zs \<in> ?A" "map p1 (z # zs) = a # as \<and> map p2 (z # zs) = b # bs" by auto
   8.189 -        thus ?case by (rule_tac x = "z # zs" in bexI)
   8.190 -      qed simp
   8.191 -    }
   8.192 -    thus "\<forall>as bs. as \<in> ?B1 \<and> bs \<in> ?B2 \<and> map f1 as = map f2 bs \<longrightarrow>
   8.193 -      (\<exists>zs \<in> ?A. map p1 zs = as \<and> map p2 zs = bs)" by blast
   8.194 -  qed
   8.195 -qed auto
   8.196 -
   8.197 -(* Finite sets *)
   8.198 -abbreviation afset where "afset \<equiv> abs_fset"
   8.199 -abbreviation rfset where "rfset \<equiv> rep_fset"
   8.200 -
   8.201 -lemma fset_fset_member:
   8.202 -"fset A = {a. a |\<in>| A}"
   8.203 -unfolding fset_def fset_member_def by auto
   8.204 -
   8.205 -lemma afset_rfset:
   8.206 -"afset (rfset x) = x"
   8.207 -by (rule Quotient_fset[unfolded Quotient_def, THEN conjunct1, rule_format])
   8.208 -
   8.209 -lemma afset_rfset_id:
   8.210 -"afset o rfset = id"
   8.211 -unfolding comp_def afset_rfset id_def ..
   8.212 -
   8.213 -lemma rfset:
   8.214 -"rfset A = rfset B \<longleftrightarrow> A = B"
   8.215 -by (metis afset_rfset)
   8.216 -
   8.217 -lemma afset_set:
   8.218 -"afset as = afset bs \<longleftrightarrow> set as = set bs"
   8.219 -using Quotient_fset unfolding Quotient_def list_eq_def by auto
   8.220 -
   8.221 -lemma surj_afset:
   8.222 -"\<exists> as. A = afset as"
   8.223 -by (metis afset_rfset)
   8.224 -
   8.225 -lemma fset_def2:
   8.226 -"fset = set o rfset"
   8.227 -unfolding fset_def map_fun_def[abs_def] by simp
   8.228 -
   8.229 -lemma fset_def2_raw:
   8.230 -"fset A = set (rfset A)"
   8.231 -unfolding fset_def2 by simp
   8.232 -
   8.233 -lemma fset_comp_afset:
   8.234 -"fset o afset = set"
   8.235 -unfolding fset_def2 comp_def apply(rule ext)
   8.236 -unfolding afset_set[symmetric] afset_rfset ..
   8.237 -
   8.238 -lemma fset_afset:
   8.239 -"fset (afset as) = set as"
   8.240 -unfolding fset_comp_afset[symmetric] by simp
   8.241 -
   8.242 -lemma set_rfset_afset:
   8.243 -"set (rfset (afset as)) = set as"
   8.244 -unfolding afset_set[symmetric] afset_rfset ..
   8.245 -
   8.246 -lemma map_fset_comp_afset:
   8.247 -"(map_fset f) o afset = afset o (map f)"
   8.248 -unfolding map_fset_def map_fun_def[abs_def] comp_def apply(rule ext)
   8.249 -unfolding afset_set set_map set_rfset_afset id_apply ..
   8.250 -
   8.251 -lemma map_fset_afset:
   8.252 -"(map_fset f) (afset as) = afset (map f as)"
   8.253 -using map_fset_comp_afset unfolding comp_def fun_eq_iff by auto
   8.254 -
   8.255 -lemma fset_map_fset:
   8.256 -"fset (map_fset f A) = (image f) (fset A)"
   8.257 -apply(subst afset_rfset[symmetric, of A])
   8.258 -unfolding map_fset_afset fset_afset set_map
   8.259 -unfolding fset_def2_raw ..
   8.260 -
   8.261 -lemma map_fset_def2:
   8.262 -"map_fset f = afset o (map f) o rfset"
   8.263 -unfolding map_fset_def map_fun_def[abs_def] by simp
   8.264 -
   8.265 -lemma map_fset_def2_raw:
   8.266 -"map_fset f A = afset (map f (rfset A))"
   8.267 -unfolding map_fset_def2 by simp
   8.268 -
   8.269 -lemma finite_ex_fset:
   8.270 -assumes "finite A"
   8.271 -shows "\<exists> B. fset B = A"
   8.272 -by (metis assms finite_list fset_afset)
   8.273 -
   8.274 -lemma wpull_image:
   8.275 -assumes "wpull A B1 B2 f1 f2 p1 p2"
   8.276 -shows "wpull (Pow A) (Pow B1) (Pow B2) (image f1) (image f2) (image p1) (image p2)"
   8.277 -unfolding wpull_def Pow_def Bex_def mem_Collect_eq proof clarify
   8.278 -  fix Y1 Y2 assume Y1: "Y1 \<subseteq> B1" and Y2: "Y2 \<subseteq> B2" and EQ: "f1 ` Y1 = f2 ` Y2"
   8.279 -  def X \<equiv> "{a \<in> A. p1 a \<in> Y1 \<and> p2 a \<in> Y2}"
   8.280 -  show "\<exists>X\<subseteq>A. p1 ` X = Y1 \<and> p2 ` X = Y2"
   8.281 -  proof (rule exI[of _ X], intro conjI)
   8.282 -    show "p1 ` X = Y1"
   8.283 -    proof
   8.284 -      show "Y1 \<subseteq> p1 ` X"
   8.285 -      proof safe
   8.286 -        fix y1 assume y1: "y1 \<in> Y1"
   8.287 -        then obtain y2 where y2: "y2 \<in> Y2" and eq: "f1 y1 = f2 y2" using EQ by auto
   8.288 -        then obtain x where "x \<in> A" and "p1 x = y1" and "p2 x = y2"
   8.289 -        using assms y1 Y1 Y2 unfolding wpull_def by blast
   8.290 -        thus "y1 \<in> p1 ` X" unfolding X_def using y1 y2 by auto
   8.291 -      qed
   8.292 -    qed(unfold X_def, auto)
   8.293 -    show "p2 ` X = Y2"
   8.294 -    proof
   8.295 -      show "Y2 \<subseteq> p2 ` X"
   8.296 -      proof safe
   8.297 -        fix y2 assume y2: "y2 \<in> Y2"
   8.298 -        then obtain y1 where y1: "y1 \<in> Y1" and eq: "f1 y1 = f2 y2" using EQ by force
   8.299 -        then obtain x where "x \<in> A" and "p1 x = y1" and "p2 x = y2"
   8.300 -        using assms y2 Y1 Y2 unfolding wpull_def by blast
   8.301 -        thus "y2 \<in> p2 ` X" unfolding X_def using y1 y2 by auto
   8.302 -      qed
   8.303 -    qed(unfold X_def, auto)
   8.304 -  qed(unfold X_def, auto)
   8.305 -qed
   8.306 -
   8.307 -lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A"
   8.308 -by (rule f_the_inv_into_f) (auto simp: inj_on_def fset_cong dest!: finite_ex_fset)
   8.309 -
   8.310 -bnf_def fset = map_fset [fset] "\<lambda>_::'a fset. natLeq" ["{||}"]
   8.311 -proof -
   8.312 -  show "map_fset id = id"
   8.313 -  unfolding map_fset_def2 map_id o_id afset_rfset_id ..
   8.314 -next
   8.315 -  fix f g
   8.316 -  show "map_fset (g o f) = map_fset g o map_fset f"
   8.317 -  unfolding map_fset_def2 map.comp[symmetric] comp_def apply(rule ext)
   8.318 -  unfolding afset_set set_map fset_def2_raw[symmetric] image_image[symmetric]
   8.319 -  unfolding map_fset_afset[symmetric] map_fset_image afset_rfset
   8.320 -  by (rule refl)
   8.321 -next
   8.322 -  fix x f g
   8.323 -  assume "\<And>z. z \<in> fset x \<Longrightarrow> f z = g z"
   8.324 -  hence "map f (rfset x) = map g (rfset x)"
   8.325 -  apply(intro map_cong) unfolding fset_def2_raw by auto
   8.326 -  thus "map_fset f x = map_fset g x" unfolding map_fset_def2_raw
   8.327 -  by (rule arg_cong)
   8.328 -next
   8.329 -  fix f
   8.330 -  show "fset o map_fset f = image f o fset"
   8.331 -  unfolding comp_def fset_map_fset ..
   8.332 -next
   8.333 -  show "card_order natLeq" by (rule natLeq_card_order)
   8.334 -next
   8.335 -  show "cinfinite natLeq" by (rule natLeq_cinfinite)
   8.336 -next
   8.337 -  fix x
   8.338 -  show "|fset x| \<le>o natLeq"
   8.339 -  unfolding fset_def2_raw
   8.340 -  apply (rule ordLess_imp_ordLeq)
   8.341 -  apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
   8.342 -  by (rule finite_set)
   8.343 -next
   8.344 -  fix A :: "'a set"
   8.345 -  have "|{x. fset x \<subseteq> A}| \<le>o |afset ` {as. set as \<subseteq> A}|"
   8.346 -  apply(rule card_of_mono1) unfolding fset_def2_raw apply auto
   8.347 -  apply (rule image_eqI)
   8.348 -  by (auto simp: afset_rfset)
   8.349 -  also have "|afset ` {as. set as \<subseteq> A}| \<le>o |{as. set as \<subseteq> A}|" using card_of_image .
   8.350 -  also have "|{as. set as \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" by (rule list_in_bd)
   8.351 -  finally show "|{x. fset x \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" .
   8.352 -next
   8.353 -  fix A B1 B2 f1 f2 p1 p2
   8.354 -  assume wp: "wpull A B1 B2 f1 f2 p1 p2"
   8.355 -  hence "wpull (Pow A) (Pow B1) (Pow B2) (image f1) (image f2) (image p1) (image p2)"
   8.356 -  by(rule wpull_image)
   8.357 -  show "wpull {x. fset x \<subseteq> A} {x. fset x \<subseteq> B1} {x. fset x \<subseteq> B2}
   8.358 -              (map_fset f1) (map_fset f2) (map_fset p1) (map_fset p2)"
   8.359 -  unfolding wpull_def Pow_def Bex_def mem_Collect_eq proof clarify
   8.360 -    fix y1 y2
   8.361 -    assume Y1: "fset y1 \<subseteq> B1" and Y2: "fset y2 \<subseteq> B2"
   8.362 -    assume "map_fset f1 y1 = map_fset f2 y2"
   8.363 -    hence EQ: "f1 ` (fset y1) = f2 ` (fset y2)" unfolding map_fset_def2_raw
   8.364 -    unfolding afset_set set_map fset_def2_raw .
   8.365 -    with Y1 Y2 obtain X where X: "X \<subseteq> A"
   8.366 -    and Y1: "p1 ` X = fset y1" and Y2: "p2 ` X = fset y2"
   8.367 -    using wpull_image[OF wp] unfolding wpull_def Pow_def
   8.368 -    unfolding Bex_def mem_Collect_eq apply -
   8.369 -    apply(erule allE[of _ "fset y1"], erule allE[of _ "fset y2"]) by auto
   8.370 -    have "\<forall> y1' \<in> fset y1. \<exists> x. x \<in> X \<and> y1' = p1 x" using Y1 by auto
   8.371 -    then obtain q1 where q1: "\<forall> y1' \<in> fset y1. q1 y1' \<in> X \<and> y1' = p1 (q1 y1')" by metis
   8.372 -    have "\<forall> y2' \<in> fset y2. \<exists> x. x \<in> X \<and> y2' = p2 x" using Y2 by auto
   8.373 -    then obtain q2 where q2: "\<forall> y2' \<in> fset y2. q2 y2' \<in> X \<and> y2' = p2 (q2 y2')" by metis
   8.374 -    def X' \<equiv> "q1 ` (fset y1) \<union> q2 ` (fset y2)"
   8.375 -    have X': "X' \<subseteq> A" and Y1: "p1 ` X' = fset y1" and Y2: "p2 ` X' = fset y2"
   8.376 -    using X Y1 Y2 q1 q2 unfolding X'_def by auto
   8.377 -    have fX': "finite X'" unfolding X'_def by simp
   8.378 -    then obtain x where X'eq: "X' = fset x" by (auto dest: finite_ex_fset)
   8.379 -    show "\<exists>x. fset x \<subseteq> A \<and> map_fset p1 x = y1 \<and> map_fset p2 x = y2"
   8.380 -    apply(intro exI[of _ "x"]) using X' Y1 Y2
   8.381 -    unfolding X'eq map_fset_def2_raw fset_def2_raw set_map[symmetric]
   8.382 -    afset_set[symmetric] afset_rfset by simp
   8.383 -  qed
   8.384 -qed auto
   8.385 -
   8.386 -lemma fset_pred[simp]: "fset_pred R a b \<longleftrightarrow>
   8.387 -  ((\<forall>t \<in> fset a. (\<exists>u \<in> fset b. R t u)) \<and>
   8.388 -   (\<forall>t \<in> fset b. (\<exists>u \<in> fset a. R u t)))" (is "?L = ?R")
   8.389 -proof
   8.390 -  assume ?L thus ?R unfolding fset_rel_def fset_pred_def
   8.391 -    Gr_def relcomp_unfold converse_unfold
   8.392 -  apply (simp add: subset_eq Ball_def)
   8.393 -  apply (rule conjI)
   8.394 -  apply (clarsimp, metis snd_conv)
   8.395 -  by (clarsimp, metis fst_conv)
   8.396 -next
   8.397 -  assume ?R
   8.398 -  def R' \<equiv> "the_inv fset (Collect (split R) \<inter> (fset a \<times> fset b))" (is "the_inv fset ?R'")
   8.399 -  have "finite ?R'" by (intro finite_Int[OF disjI2] finite_cartesian_product) auto
   8.400 -  hence *: "fset R' = ?R'" unfolding R'_def by (intro fset_to_fset)
   8.401 -  show ?L unfolding fset_rel_def fset_pred_def Gr_def relcomp_unfold converse_unfold
   8.402 -  proof (intro CollectI prod_caseI exI conjI)
   8.403 -    from * show "(R', a) = (R', map_fset fst R')" using conjunct1[OF `?R`]
   8.404 -      by (auto simp add: fset_cong[symmetric] image_def Int_def split: prod.splits)
   8.405 -    from * show "(R', b) = (R', map_fset snd R')" using conjunct2[OF `?R`]
   8.406 -      by (auto simp add: fset_cong[symmetric] image_def Int_def split: prod.splits)
   8.407 -  qed (auto simp add: *)
   8.408 -qed
   8.409 -
   8.410 -(* Countable sets *)
   8.411 -
   8.412 -lemma card_of_countable_sets_range:
   8.413 -fixes A :: "'a set"
   8.414 -shows "|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |{f::nat \<Rightarrow> 'a. range f \<subseteq> A}|"
   8.415 -apply(rule card_of_ordLeqI[of fromNat]) using inj_on_fromNat
   8.416 -unfolding inj_on_def by auto
   8.417 -
   8.418 -lemma card_of_countable_sets_Func:
   8.419 -"|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |A| ^c natLeq"
   8.420 -using card_of_countable_sets_range card_of_Func_UNIV[THEN ordIso_symmetric]
   8.421 -unfolding cexp_def Field_natLeq Field_card_of
   8.422 -by(rule ordLeq_ordIso_trans)
   8.423 -
   8.424 -lemma ordLeq_countable_subsets:
   8.425 -"|A| \<le>o |{X. X \<subseteq> A \<and> countable X}|"
   8.426 -apply(rule card_of_ordLeqI[of "\<lambda> a. {a}"]) unfolding inj_on_def by auto
   8.427 -
   8.428 -lemma finite_countable_subset:
   8.429 -"finite {X. X \<subseteq> A \<and> countable X} \<longleftrightarrow> finite A"
   8.430 -apply default
   8.431 - apply (erule contrapos_pp)
   8.432 - apply (rule card_of_ordLeq_infinite)
   8.433 - apply (rule ordLeq_countable_subsets)
   8.434 - apply assumption
   8.435 -apply (rule finite_Collect_conjI)
   8.436 -apply (rule disjI1)
   8.437 -by (erule finite_Collect_subsets)
   8.438 -
   8.439 -lemma card_of_countable_sets:
   8.440 -"|{X. X \<subseteq> A \<and> countable X}| \<le>o ( |A| +c ctwo) ^c natLeq"
   8.441 -(is "|?L| \<le>o _")
   8.442 -proof(cases "finite A")
   8.443 -  let ?R = "Func (UNIV::nat set) (A <+> (UNIV::bool set))"
   8.444 -  case True hence "finite ?L" by simp
   8.445 -  moreover have "infinite ?R"
   8.446 -  apply(rule infinite_Func[of _ "Inr True" "Inr False"]) by auto
   8.447 -  ultimately show ?thesis unfolding cexp_def csum_def ctwo_def Field_natLeq Field_card_of
   8.448 -  apply(intro ordLess_imp_ordLeq) by (rule finite_ordLess_infinite2)
   8.449 -next
   8.450 -  case False
   8.451 -  hence "|{X. X \<subseteq> A \<and> countable X}| =o |{X. X \<subseteq> A \<and> countable X} - {{}}|"
   8.452 -  by (intro card_of_infinite_diff_finitte finite.emptyI finite.insertI ordIso_symmetric)
   8.453 -     (unfold finite_countable_subset)
   8.454 -  also have "|{X. X \<subseteq> A \<and> countable X} - {{}}| \<le>o |A| ^c natLeq"
   8.455 -  using card_of_countable_sets_Func[of A] unfolding set_diff_eq by auto
   8.456 -  also have "|A| ^c natLeq \<le>o ( |A| +c ctwo) ^c natLeq"
   8.457 -  apply(rule cexp_mono1_cone_ordLeq)
   8.458 -    apply(rule ordLeq_csum1, rule card_of_Card_order)
   8.459 -    apply (rule cone_ordLeq_cexp)
   8.460 -    apply (rule cone_ordLeq_Cnotzero)
   8.461 -    using csum_Cnotzero2 ctwo_Cnotzero apply blast
   8.462 -    by (rule natLeq_Card_order)
   8.463 -  finally show ?thesis .
   8.464 -qed
   8.465 -
   8.466 -bnf_def cset = cIm [rcset] "\<lambda>_::'a cset. natLeq" ["cEmp"]
   8.467 -proof -
   8.468 -  show "cIm id = id" unfolding cIm_def[abs_def] id_def by auto
   8.469 -next
   8.470 -  fix f g show "cIm (g \<circ> f) = cIm g \<circ> cIm f"
   8.471 -  unfolding cIm_def[abs_def] apply(rule ext) unfolding comp_def by auto
   8.472 -next
   8.473 -  fix C f g assume eq: "\<And>a. a \<in> rcset C \<Longrightarrow> f a = g a"
   8.474 -  thus "cIm f C = cIm g C"
   8.475 -  unfolding cIm_def[abs_def] unfolding image_def by auto
   8.476 -next
   8.477 -  fix f show "rcset \<circ> cIm f = op ` f \<circ> rcset" unfolding cIm_def[abs_def] by auto
   8.478 -next
   8.479 -  show "card_order natLeq" by (rule natLeq_card_order)
   8.480 -next
   8.481 -  show "cinfinite natLeq" by (rule natLeq_cinfinite)
   8.482 -next
   8.483 -  fix C show "|rcset C| \<le>o natLeq" using rcset unfolding countable_def .
   8.484 -next
   8.485 -  fix A :: "'a set"
   8.486 -  have "|{Z. rcset Z \<subseteq> A}| \<le>o |acset ` {X. X \<subseteq> A \<and> countable X}|"
   8.487 -  apply(rule card_of_mono1) unfolding Pow_def image_def
   8.488 -  proof (rule Collect_mono, clarsimp)
   8.489 -    fix x
   8.490 -    assume "rcset x \<subseteq> A"
   8.491 -    hence "rcset x \<subseteq> A \<and> countable (rcset x) \<and> x = acset (rcset x)"
   8.492 -    using acset_rcset[of x] rcset[of x] by force
   8.493 -    thus "\<exists>y \<subseteq> A. countable y \<and> x = acset y" by blast
   8.494 -  qed
   8.495 -  also have "|acset ` {X. X \<subseteq> A \<and> countable X}| \<le>o |{X. X \<subseteq> A \<and> countable X}|"
   8.496 -  using card_of_image .
   8.497 -  also have "|{X. X \<subseteq> A \<and> countable X}| \<le>o ( |A| +c ctwo) ^c natLeq"
   8.498 -  using card_of_countable_sets .
   8.499 -  finally show "|{Z. rcset Z \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" .
   8.500 -next
   8.501 -  fix A B1 B2 f1 f2 p1 p2
   8.502 -  assume wp: "wpull A B1 B2 f1 f2 p1 p2"
   8.503 -  show "wpull {x. rcset x \<subseteq> A} {x. rcset x \<subseteq> B1} {x. rcset x \<subseteq> B2}
   8.504 -              (cIm f1) (cIm f2) (cIm p1) (cIm p2)"
   8.505 -  unfolding wpull_def proof safe
   8.506 -    fix y1 y2
   8.507 -    assume Y1: "rcset y1 \<subseteq> B1" and Y2: "rcset y2 \<subseteq> B2"
   8.508 -    assume "cIm f1 y1 = cIm f2 y2"
   8.509 -    hence EQ: "f1 ` (rcset y1) = f2 ` (rcset y2)"
   8.510 -    unfolding cIm_def by auto
   8.511 -    with Y1 Y2 obtain X where X: "X \<subseteq> A"
   8.512 -    and Y1: "p1 ` X = rcset y1" and Y2: "p2 ` X = rcset y2"
   8.513 -    using wpull_image[OF wp] unfolding wpull_def Pow_def
   8.514 -    unfolding Bex_def mem_Collect_eq apply -
   8.515 -    apply(erule allE[of _ "rcset y1"], erule allE[of _ "rcset y2"]) by auto
   8.516 -    have "\<forall> y1' \<in> rcset y1. \<exists> x. x \<in> X \<and> y1' = p1 x" using Y1 by auto
   8.517 -    then obtain q1 where q1: "\<forall> y1' \<in> rcset y1. q1 y1' \<in> X \<and> y1' = p1 (q1 y1')" by metis
   8.518 -    have "\<forall> y2' \<in> rcset y2. \<exists> x. x \<in> X \<and> y2' = p2 x" using Y2 by auto
   8.519 -    then obtain q2 where q2: "\<forall> y2' \<in> rcset y2. q2 y2' \<in> X \<and> y2' = p2 (q2 y2')" by metis
   8.520 -    def X' \<equiv> "q1 ` (rcset y1) \<union> q2 ` (rcset y2)"
   8.521 -    have X': "X' \<subseteq> A" and Y1: "p1 ` X' = rcset y1" and Y2: "p2 ` X' = rcset y2"
   8.522 -    using X Y1 Y2 q1 q2 unfolding X'_def by fast+
   8.523 -    have fX': "countable X'" unfolding X'_def by simp
   8.524 -    then obtain x where X'eq: "X' = rcset x" by (metis rcset_acset)
   8.525 -    show "\<exists>x\<in>{x. rcset x \<subseteq> A}. cIm p1 x = y1 \<and> cIm p2 x = y2"
   8.526 -    apply(intro bexI[of _ "x"]) using X' Y1 Y2 unfolding X'eq cIm_def by auto
   8.527 -  qed
   8.528 -qed (unfold cEmp_def, auto)
   8.529 -
   8.530 -
   8.531 -(* Multisets *)
   8.532 -
   8.533 -lemma setsum_gt_0_iff:
   8.534 -fixes f :: "'a \<Rightarrow> nat" assumes "finite A"
   8.535 -shows "setsum f A > 0 \<longleftrightarrow> (\<exists> a \<in> A. f a > 0)"
   8.536 -(is "?L \<longleftrightarrow> ?R")
   8.537 -proof-
   8.538 -  have "?L \<longleftrightarrow> \<not> setsum f A = 0" by fast
   8.539 -  also have "... \<longleftrightarrow> (\<exists> a \<in> A. f a \<noteq> 0)" using assms by simp
   8.540 -  also have "... \<longleftrightarrow> ?R" by simp
   8.541 -  finally show ?thesis .
   8.542 -qed
   8.543 -
   8.544 -(*   *)
   8.545 -definition mmap :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> 'b \<Rightarrow> nat" where
   8.546 -"mmap h f b = setsum f {a. h a = b \<and> f a > 0}"
   8.547 -
   8.548 -lemma mmap_id: "mmap id = id"
   8.549 -proof (rule ext)+
   8.550 -  fix f a show "mmap id f a = id f a"
   8.551 -  proof(cases "f a = 0")
   8.552 -    case False
   8.553 -    hence 1: "{aa. aa = a \<and> 0 < f aa} = {a}" by auto
   8.554 -    show ?thesis by (simp add: mmap_def id_apply 1)
   8.555 -  qed(unfold mmap_def, auto)
   8.556 -qed
   8.557 -
   8.558 -lemma inj_on_setsum_inv:
   8.559 -assumes f: "f \<in> multiset"
   8.560 -and 1: "(0::nat) < setsum f {a. h a = b' \<and> 0 < f a}" (is "0 < setsum f ?A'")
   8.561 -and 2: "{a. h a = b \<and> 0 < f a} = {a. h a = b' \<and> 0 < f a}" (is "?A = ?A'")
   8.562 -shows "b = b'"
   8.563 -proof-
   8.564 -  have "finite ?A'" using f unfolding multiset_def by auto
   8.565 -  hence "?A' \<noteq> {}" using 1 setsum_gt_0_iff by auto
   8.566 -  thus ?thesis using 2 by auto
   8.567 -qed
   8.568 -
   8.569 -lemma mmap_comp:
   8.570 -fixes h1 :: "'a \<Rightarrow> 'b" and h2 :: "'b \<Rightarrow> 'c"
   8.571 -assumes f: "f \<in> multiset"
   8.572 -shows "mmap (h2 o h1) f = (mmap h2 o mmap h1) f"
   8.573 -unfolding mmap_def[abs_def] comp_def proof(rule ext)+
   8.574 -  fix c :: 'c
   8.575 -  let ?A = "{a. h2 (h1 a) = c \<and> 0 < f a}"
   8.576 -  let ?As = "\<lambda> b. {a. h1 a = b \<and> 0 < f a}"
   8.577 -  let ?B = "{b. h2 b = c \<and> 0 < setsum f (?As b)}"
   8.578 -  have 0: "{?As b | b.  b \<in> ?B} = ?As ` ?B" by auto
   8.579 -  have "\<And> b. finite (?As b)" using f unfolding multiset_def by simp
   8.580 -  hence "?B = {b. h2 b = c \<and> ?As b \<noteq> {}}" using setsum_gt_0_iff by auto
   8.581 -  hence A: "?A = \<Union> {?As b | b.  b \<in> ?B}" by auto
   8.582 -  have "setsum f ?A = setsum (setsum f) {?As b | b.  b \<in> ?B}"
   8.583 -  unfolding A apply(rule setsum_Union_disjoint)
   8.584 -  using f unfolding multiset_def by auto
   8.585 -  also have "... = setsum (setsum f) (?As ` ?B)" unfolding 0 ..
   8.586 -  also have "... = setsum (setsum f o ?As) ?B" apply(rule setsum_reindex)
   8.587 -  unfolding inj_on_def apply auto using inj_on_setsum_inv[OF f, of h1] by blast
   8.588 -  also have "... = setsum (\<lambda> b. setsum f (?As b)) ?B" unfolding comp_def ..
   8.589 -  finally show "setsum f ?A = setsum (\<lambda> b. setsum f (?As b)) ?B" .
   8.590 -qed
   8.591 -
   8.592 -lemma mmap_comp1:
   8.593 -fixes h1 :: "'a \<Rightarrow> 'b" and h2 :: "'b \<Rightarrow> 'c"
   8.594 -assumes "f \<in> multiset"
   8.595 -shows "mmap (\<lambda> a. h2 (h1 a)) f = mmap h2 (mmap h1 f)"
   8.596 -using mmap_comp[OF assms] unfolding comp_def by auto
   8.597 -
   8.598 -lemma mmap:
   8.599 -assumes "f \<in> multiset"
   8.600 -shows "mmap h f \<in> multiset"
   8.601 -using assms unfolding mmap_def[abs_def] multiset_def proof safe
   8.602 -  assume fin: "finite {a. 0 < f a}"  (is "finite ?A")
   8.603 -  show "finite {b. 0 < setsum f {a. h a = b \<and> 0 < f a}}"
   8.604 -  (is "finite {b. 0 < setsum f (?As b)}")
   8.605 -  proof- let ?B = "{b. 0 < setsum f (?As b)}"
   8.606 -    have "\<And> b. finite (?As b)" using assms unfolding multiset_def by simp
   8.607 -    hence B: "?B = {b. ?As b \<noteq> {}}" using setsum_gt_0_iff by auto
   8.608 -    hence "?B \<subseteq> h ` ?A" by auto
   8.609 -    thus ?thesis using finite_surj[OF fin] by auto
   8.610 -  qed
   8.611 -qed
   8.612 -
   8.613 -lemma mmap_cong:
   8.614 -assumes "\<And>a. a \<in># M \<Longrightarrow> f a = g a"
   8.615 -shows "mmap f (count M) = mmap g (count M)"
   8.616 -using assms unfolding mmap_def[abs_def] by (intro ext, intro setsum_cong) auto
   8.617 -
   8.618 -abbreviation supp where "supp f \<equiv> {a. f a > 0}"
   8.619 -
   8.620 -lemma mmap_image_comp:
   8.621 -assumes f: "f \<in> multiset"
   8.622 -shows "(supp o mmap h) f = (image h o supp) f"
   8.623 -unfolding mmap_def[abs_def] comp_def proof-
   8.624 -  have "\<And> b. finite {a. h a = b \<and> 0 < f a}" (is "\<And> b. finite (?As b)")
   8.625 -  using f unfolding multiset_def by auto
   8.626 -  thus "{b. 0 < setsum f (?As b)} = h ` {a. 0 < f a}"
   8.627 -  using setsum_gt_0_iff by auto
   8.628 -qed
   8.629 -
   8.630 -lemma mmap_image:
   8.631 -assumes f: "f \<in> multiset"
   8.632 -shows "supp (mmap h f) = h ` (supp f)"
   8.633 -using mmap_image_comp[OF assms] unfolding comp_def .
   8.634 -
   8.635 -lemma set_of_Abs_multiset:
   8.636 -assumes f: "f \<in> multiset"
   8.637 -shows "set_of (Abs_multiset f) = supp f"
   8.638 -using assms unfolding set_of_def by (auto simp: Abs_multiset_inverse)
   8.639 -
   8.640 -lemma supp_count:
   8.641 -"supp (count M) = set_of M"
   8.642 -using assms unfolding set_of_def by auto
   8.643 -
   8.644 -lemma multiset_of_surj:
   8.645 -"multiset_of ` {as. set as \<subseteq> A} = {M. set_of M \<subseteq> A}"
   8.646 -proof safe
   8.647 -  fix M assume M: "set_of M \<subseteq> A"
   8.648 -  obtain as where eq: "M = multiset_of as" using surj_multiset_of unfolding surj_def by auto
   8.649 -  hence "set as \<subseteq> A" using M by auto
   8.650 -  thus "M \<in> multiset_of ` {as. set as \<subseteq> A}" using eq by auto
   8.651 -next
   8.652 -  show "\<And>x xa xb. \<lbrakk>set xa \<subseteq> A; xb \<in> set_of (multiset_of xa)\<rbrakk> \<Longrightarrow> xb \<in> A"
   8.653 -  by (erule set_mp) (unfold set_of_multiset_of)
   8.654 -qed
   8.655 -
   8.656 -lemma card_of_set_of:
   8.657 -"|{M. set_of M \<subseteq> A}| \<le>o |{as. set as \<subseteq> A}|"
   8.658 -apply(rule card_of_ordLeqI2[of _ multiset_of]) using multiset_of_surj by auto
   8.659 -
   8.660 -lemma nat_sum_induct:
   8.661 -assumes "\<And>n1 n2. (\<And> m1 m2. m1 + m2 < n1 + n2 \<Longrightarrow> phi m1 m2) \<Longrightarrow> phi n1 n2"
   8.662 -shows "phi (n1::nat) (n2::nat)"
   8.663 -proof-
   8.664 -  let ?chi = "\<lambda> n1n2 :: nat * nat. phi (fst n1n2) (snd n1n2)"
   8.665 -  have "?chi (n1,n2)"
   8.666 -  apply(induct rule: measure_induct[of "\<lambda> n1n2. fst n1n2 + snd n1n2" ?chi])
   8.667 -  using assms by (metis fstI sndI)
   8.668 -  thus ?thesis by simp
   8.669 -qed
   8.670 -
   8.671 -lemma matrix_count:
   8.672 -fixes ct1 ct2 :: "nat \<Rightarrow> nat"
   8.673 -assumes "setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2}"
   8.674 -shows
   8.675 -"\<exists> ct. (\<forall> i1 \<le> n1. setsum (\<lambda> i2. ct i1 i2) {..<Suc n2} = ct1 i1) \<and>
   8.676 -       (\<forall> i2 \<le> n2. setsum (\<lambda> i1. ct i1 i2) {..<Suc n1} = ct2 i2)"
   8.677 -(is "?phi ct1 ct2 n1 n2")
   8.678 -proof-
   8.679 -  have "\<forall> ct1 ct2 :: nat \<Rightarrow> nat.
   8.680 -        setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2} \<longrightarrow> ?phi ct1 ct2 n1 n2"
   8.681 -  proof(induct rule: nat_sum_induct[of
   8.682 -"\<lambda> n1 n2. \<forall> ct1 ct2 :: nat \<Rightarrow> nat.
   8.683 -     setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2} \<longrightarrow> ?phi ct1 ct2 n1 n2"],
   8.684 -      clarify)
   8.685 -  fix n1 n2 :: nat and ct1 ct2 :: "nat \<Rightarrow> nat"
   8.686 -  assume IH: "\<And> m1 m2. m1 + m2 < n1 + n2 \<Longrightarrow>
   8.687 -                \<forall> dt1 dt2 :: nat \<Rightarrow> nat.
   8.688 -                setsum dt1 {..<Suc m1} = setsum dt2 {..<Suc m2} \<longrightarrow> ?phi dt1 dt2 m1 m2"
   8.689 -  and ss: "setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2}"
   8.690 -  show "?phi ct1 ct2 n1 n2"
   8.691 -  proof(cases n1)
   8.692 -    case 0 note n1 = 0
   8.693 -    show ?thesis
   8.694 -    proof(cases n2)
   8.695 -      case 0 note n2 = 0
   8.696 -      let ?ct = "\<lambda> i1 i2. ct2 0"
   8.697 -      show ?thesis apply(rule exI[of _ ?ct]) using n1 n2 ss by simp
   8.698 -    next
   8.699 -      case (Suc m2) note n2 = Suc
   8.700 -      let ?ct = "\<lambda> i1 i2. ct2 i2"
   8.701 -      show ?thesis apply(rule exI[of _ ?ct]) using n1 n2 ss by auto
   8.702 -    qed
   8.703 -  next
   8.704 -    case (Suc m1) note n1 = Suc
   8.705 -    show ?thesis
   8.706 -    proof(cases n2)
   8.707 -      case 0 note n2 = 0
   8.708 -      let ?ct = "\<lambda> i1 i2. ct1 i1"
   8.709 -      show ?thesis apply(rule exI[of _ ?ct]) using n1 n2 ss by auto
   8.710 -    next
   8.711 -      case (Suc m2) note n2 = Suc
   8.712 -      show ?thesis
   8.713 -      proof(cases "ct1 n1 \<le> ct2 n2")
   8.714 -        case True
   8.715 -        def dt2 \<equiv> "\<lambda> i2. if i2 = n2 then ct2 i2 - ct1 n1 else ct2 i2"
   8.716 -        have "setsum ct1 {..<Suc m1} = setsum dt2 {..<Suc n2}"
   8.717 -        unfolding dt2_def using ss n1 True by auto
   8.718 -        hence "?phi ct1 dt2 m1 n2" using IH[of m1 n2] n1 by simp
   8.719 -        then obtain dt where
   8.720 -        1: "\<And> i1. i1 \<le> m1 \<Longrightarrow> setsum (\<lambda> i2. dt i1 i2) {..<Suc n2} = ct1 i1" and
   8.721 -        2: "\<And> i2. i2 \<le> n2 \<Longrightarrow> setsum (\<lambda> i1. dt i1 i2) {..<Suc m1} = dt2 i2" by auto
   8.722 -        let ?ct = "\<lambda> i1 i2. if i1 = n1 then (if i2 = n2 then ct1 n1 else 0)
   8.723 -                                       else dt i1 i2"
   8.724 -        show ?thesis apply(rule exI[of _ ?ct])
   8.725 -        using n1 n2 1 2 True unfolding dt2_def by simp
   8.726 -      next
   8.727 -        case False
   8.728 -        hence False: "ct2 n2 < ct1 n1" by simp
   8.729 -        def dt1 \<equiv> "\<lambda> i1. if i1 = n1 then ct1 i1 - ct2 n2 else ct1 i1"
   8.730 -        have "setsum dt1 {..<Suc n1} = setsum ct2 {..<Suc m2}"
   8.731 -        unfolding dt1_def using ss n2 False by auto
   8.732 -        hence "?phi dt1 ct2 n1 m2" using IH[of n1 m2] n2 by simp
   8.733 -        then obtain dt where
   8.734 -        1: "\<And> i1. i1 \<le> n1 \<Longrightarrow> setsum (\<lambda> i2. dt i1 i2) {..<Suc m2} = dt1 i1" and
   8.735 -        2: "\<And> i2. i2 \<le> m2 \<Longrightarrow> setsum (\<lambda> i1. dt i1 i2) {..<Suc n1} = ct2 i2" by force
   8.736 -        let ?ct = "\<lambda> i1 i2. if i2 = n2 then (if i1 = n1 then ct2 n2 else 0)
   8.737 -                                       else dt i1 i2"
   8.738 -        show ?thesis apply(rule exI[of _ ?ct])
   8.739 -        using n1 n2 1 2 False unfolding dt1_def by simp
   8.740 -      qed
   8.741 -    qed
   8.742 -  qed
   8.743 -  qed
   8.744 -  thus ?thesis using assms by auto
   8.745 -qed
   8.746 -
   8.747 -definition
   8.748 -"inj2 u B1 B2 \<equiv>
   8.749 - \<forall> b1 b1' b2 b2'. {b1,b1'} \<subseteq> B1 \<and> {b2,b2'} \<subseteq> B2 \<and> u b1 b2 = u b1' b2'
   8.750 -                  \<longrightarrow> b1 = b1' \<and> b2 = b2'"
   8.751 -
   8.752 -lemma matrix_count_finite:
   8.753 -assumes B1: "B1 \<noteq> {}" "finite B1" and B2: "B2 \<noteq> {}" "finite B2" and u: "inj2 u B1 B2"
   8.754 -and ss: "setsum N1 B1 = setsum N2 B2"
   8.755 -shows "\<exists> M :: 'a \<Rightarrow> nat.
   8.756 -            (\<forall> b1 \<in> B1. setsum (\<lambda> b2. M (u b1 b2)) B2 = N1 b1) \<and>
   8.757 -            (\<forall> b2 \<in> B2. setsum (\<lambda> b1. M (u b1 b2)) B1 = N2 b2)"
   8.758 -proof-
   8.759 -  obtain n1 where "card B1 = Suc n1" using B1 by (metis card_insert finite.simps)
   8.760 -  then obtain e1 where e1: "bij_betw e1 {..<Suc n1} B1"
   8.761 -  using ex_bij_betw_finite_nat[OF B1(2)] by (metis atLeast0LessThan bij_betw_the_inv_into)
   8.762 -  hence e1_inj: "inj_on e1 {..<Suc n1}" and e1_surj: "e1 ` {..<Suc n1} = B1"
   8.763 -  unfolding bij_betw_def by auto
   8.764 -  def f1 \<equiv> "inv_into {..<Suc n1} e1"
   8.765 -  have f1: "bij_betw f1 B1 {..<Suc n1}"
   8.766 -  and f1e1[simp]: "\<And> i1. i1 < Suc n1 \<Longrightarrow> f1 (e1 i1) = i1"
   8.767 -  and e1f1[simp]: "\<And> b1. b1 \<in> B1 \<Longrightarrow> e1 (f1 b1) = b1" unfolding f1_def
   8.768 -  apply (metis bij_betw_inv_into e1, metis bij_betw_inv_into_left e1 lessThan_iff)
   8.769 -  by (metis e1_surj f_inv_into_f)
   8.770 -  (*  *)
   8.771 -  obtain n2 where "card B2 = Suc n2" using B2 by (metis card_insert finite.simps)
   8.772 -  then obtain e2 where e2: "bij_betw e2 {..<Suc n2} B2"
   8.773 -  using ex_bij_betw_finite_nat[OF B2(2)] by (metis atLeast0LessThan bij_betw_the_inv_into)
   8.774 -  hence e2_inj: "inj_on e2 {..<Suc n2}" and e2_surj: "e2 ` {..<Suc n2} = B2"
   8.775 -  unfolding bij_betw_def by auto
   8.776 -  def f2 \<equiv> "inv_into {..<Suc n2} e2"
   8.777 -  have f2: "bij_betw f2 B2 {..<Suc n2}"
   8.778 -  and f2e2[simp]: "\<And> i2. i2 < Suc n2 \<Longrightarrow> f2 (e2 i2) = i2"
   8.779 -  and e2f2[simp]: "\<And> b2. b2 \<in> B2 \<Longrightarrow> e2 (f2 b2) = b2" unfolding f2_def
   8.780 -  apply (metis bij_betw_inv_into e2, metis bij_betw_inv_into_left e2 lessThan_iff)
   8.781 -  by (metis e2_surj f_inv_into_f)
   8.782 -  (*  *)
   8.783 -  let ?ct1 = "N1 o e1"  let ?ct2 = "N2 o e2"
   8.784 -  have ss: "setsum ?ct1 {..<Suc n1} = setsum ?ct2 {..<Suc n2}"
   8.785 -  unfolding setsum_reindex[OF e1_inj, symmetric] setsum_reindex[OF e2_inj, symmetric]
   8.786 -  e1_surj e2_surj using ss .
   8.787 -  obtain ct where
   8.788 -  ct1: "\<And> i1. i1 \<le> n1 \<Longrightarrow> setsum (\<lambda> i2. ct i1 i2) {..<Suc n2} = ?ct1 i1" and
   8.789 -  ct2: "\<And> i2. i2 \<le> n2 \<Longrightarrow> setsum (\<lambda> i1. ct i1 i2) {..<Suc n1} = ?ct2 i2"
   8.790 -  using matrix_count[OF ss] by blast
   8.791 -  (*  *)
   8.792 -  def A \<equiv> "{u b1 b2 | b1 b2. b1 \<in> B1 \<and> b2 \<in> B2}"
   8.793 -  have "\<forall> a \<in> A. \<exists> b1b2 \<in> B1 <*> B2. u (fst b1b2) (snd b1b2) = a"
   8.794 -  unfolding A_def Ball_def mem_Collect_eq by auto
   8.795 -  then obtain h1h2 where h12:
   8.796 -  "\<And>a. a \<in> A \<Longrightarrow> u (fst (h1h2 a)) (snd (h1h2 a)) = a \<and> h1h2 a \<in> B1 <*> B2" by metis
   8.797 -  def h1 \<equiv> "fst o h1h2"  def h2 \<equiv> "snd o h1h2"
   8.798 -  have h12[simp]: "\<And>a. a \<in> A \<Longrightarrow> u (h1 a) (h2 a) = a"
   8.799 -                  "\<And> a. a \<in> A \<Longrightarrow> h1 a \<in> B1"  "\<And> a. a \<in> A \<Longrightarrow> h2 a \<in> B2"
   8.800 -  using h12 unfolding h1_def h2_def by force+
   8.801 -  {fix b1 b2 assume b1: "b1 \<in> B1" and b2: "b2 \<in> B2"
   8.802 -   hence inA: "u b1 b2 \<in> A" unfolding A_def by auto
   8.803 -   hence "u b1 b2 = u (h1 (u b1 b2)) (h2 (u b1 b2))" by auto
   8.804 -   moreover have "h1 (u b1 b2) \<in> B1" "h2 (u b1 b2) \<in> B2" using inA by auto
   8.805 -   ultimately have "h1 (u b1 b2) = b1 \<and> h2 (u b1 b2) = b2"
   8.806 -   using u b1 b2 unfolding inj2_def by fastforce
   8.807 -  }
   8.808 -  hence h1[simp]: "\<And> b1 b2. \<lbrakk>b1 \<in> B1; b2 \<in> B2\<rbrakk> \<Longrightarrow> h1 (u b1 b2) = b1" and
   8.809 -        h2[simp]: "\<And> b1 b2. \<lbrakk>b1 \<in> B1; b2 \<in> B2\<rbrakk> \<Longrightarrow> h2 (u b1 b2) = b2" by auto
   8.810 -  def M \<equiv> "\<lambda> a. ct (f1 (h1 a)) (f2 (h2 a))"
   8.811 -  show ?thesis
   8.812 -  apply(rule exI[of _ M]) proof safe
   8.813 -    fix b1 assume b1: "b1 \<in> B1"
   8.814 -    hence f1b1: "f1 b1 \<le> n1" using f1 unfolding bij_betw_def
   8.815 -    by (metis bij_betwE f1 lessThan_iff less_Suc_eq_le)
   8.816 -    have "(\<Sum>b2\<in>B2. M (u b1 b2)) = (\<Sum>i2<Suc n2. ct (f1 b1) (f2 (e2 i2)))"
   8.817 -    unfolding e2_surj[symmetric] setsum_reindex[OF e2_inj]
   8.818 -    unfolding M_def comp_def apply(intro setsum_cong) apply force
   8.819 -    by (metis e2_surj b1 h1 h2 imageI)
   8.820 -    also have "... = N1 b1" using b1 ct1[OF f1b1] by simp
   8.821 -    finally show "(\<Sum>b2\<in>B2. M (u b1 b2)) = N1 b1" .
   8.822 -  next
   8.823 -    fix b2 assume b2: "b2 \<in> B2"
   8.824 -    hence f2b2: "f2 b2 \<le> n2" using f2 unfolding bij_betw_def
   8.825 -    by (metis bij_betwE f2 lessThan_iff less_Suc_eq_le)
   8.826 -    have "(\<Sum>b1\<in>B1. M (u b1 b2)) = (\<Sum>i1<Suc n1. ct (f1 (e1 i1)) (f2 b2))"
   8.827 -    unfolding e1_surj[symmetric] setsum_reindex[OF e1_inj]
   8.828 -    unfolding M_def comp_def apply(intro setsum_cong) apply force
   8.829 -    by (metis e1_surj b2 h1 h2 imageI)
   8.830 -    also have "... = N2 b2" using b2 ct2[OF f2b2] by simp
   8.831 -    finally show "(\<Sum>b1\<in>B1. M (u b1 b2)) = N2 b2" .
   8.832 -  qed
   8.833 -qed
   8.834 -
   8.835 -lemma supp_vimage_mmap:
   8.836 -assumes "M \<in> multiset"
   8.837 -shows "supp M \<subseteq> f -` (supp (mmap f M))"
   8.838 -using assms by (auto simp: mmap_image)
   8.839 -
   8.840 -lemma mmap_ge_0:
   8.841 -assumes "M \<in> multiset"
   8.842 -shows "0 < mmap f M b \<longleftrightarrow> (\<exists>a. 0 < M a \<and> f a = b)"
   8.843 -proof-
   8.844 -  have f: "finite {a. f a = b \<and> 0 < M a}" using assms unfolding multiset_def by auto
   8.845 -  show ?thesis unfolding mmap_def setsum_gt_0_iff[OF f] by auto
   8.846 -qed
   8.847 -
   8.848 -lemma finite_twosets:
   8.849 -assumes "finite B1" and "finite B2"
   8.850 -shows "finite {u b1 b2 |b1 b2. b1 \<in> B1 \<and> b2 \<in> B2}"  (is "finite ?A")
   8.851 -proof-
   8.852 -  have A: "?A = (\<lambda> b1b2. u (fst b1b2) (snd b1b2)) ` (B1 <*> B2)" by force
   8.853 -  show ?thesis unfolding A using finite_cartesian_product[OF assms] by auto
   8.854 -qed
   8.855 -
   8.856 -lemma wp_mmap:
   8.857 -fixes A :: "'a set" and B1 :: "'b1 set" and B2 :: "'b2 set"
   8.858 -assumes wp: "wpull A B1 B2 f1 f2 p1 p2"
   8.859 -shows
   8.860 -"wpull {M. M \<in> multiset \<and> supp M \<subseteq> A}
   8.861 -       {N1. N1 \<in> multiset \<and> supp N1 \<subseteq> B1} {N2. N2 \<in> multiset \<and> supp N2 \<subseteq> B2}
   8.862 -       (mmap f1) (mmap f2) (mmap p1) (mmap p2)"
   8.863 -unfolding wpull_def proof (safe, unfold Bex_def mem_Collect_eq)
   8.864 -  fix N1 :: "'b1 \<Rightarrow> nat" and N2 :: "'b2 \<Rightarrow> nat"
   8.865 -  assume mmap': "mmap f1 N1 = mmap f2 N2"
   8.866 -  and N1[simp]: "N1 \<in> multiset" "supp N1 \<subseteq> B1"
   8.867 -  and N2[simp]: "N2 \<in> multiset" "supp N2 \<subseteq> B2"
   8.868 -  have mN1[simp]: "mmap f1 N1 \<in> multiset" using N1 by (auto simp: mmap)
   8.869 -  have mN2[simp]: "mmap f2 N2 \<in> multiset" using N2 by (auto simp: mmap)
   8.870 -  def P \<equiv> "mmap f1 N1"
   8.871 -  have P1: "P = mmap f1 N1" and P2: "P = mmap f2 N2" unfolding P_def using mmap' by auto
   8.872 -  note P = P1 P2
   8.873 -  have P_mult[simp]: "P \<in> multiset" unfolding P_def using N1 by auto
   8.874 -  have fin_N1[simp]: "finite (supp N1)" using N1(1) unfolding multiset_def by auto
   8.875 -  have fin_N2[simp]: "finite (supp N2)" using N2(1) unfolding multiset_def by auto
   8.876 -  have fin_P[simp]: "finite (supp P)" using P_mult unfolding multiset_def by auto
   8.877 -  (*  *)
   8.878 -  def set1 \<equiv> "\<lambda> c. {b1 \<in> supp N1. f1 b1 = c}"
   8.879 -  have set1[simp]: "\<And> c b1. b1 \<in> set1 c \<Longrightarrow> f1 b1 = c" unfolding set1_def by auto
   8.880 -  have fin_set1: "\<And> c. c \<in> supp P \<Longrightarrow> finite (set1 c)"
   8.881 -  using N1(1) unfolding set1_def multiset_def by auto
   8.882 -  have set1_NE: "\<And> c. c \<in> supp P \<Longrightarrow> set1 c \<noteq> {}"
   8.883 -  unfolding set1_def P1 mmap_ge_0[OF N1(1)] by auto
   8.884 -  have supp_N1_set1: "supp N1 = (\<Union> c \<in> supp P. set1 c)"
   8.885 -  using supp_vimage_mmap[OF N1(1), of f1] unfolding set1_def P1 by auto
   8.886 -  hence set1_inclN1: "\<And>c. c \<in> supp P \<Longrightarrow> set1 c \<subseteq> supp N1" by auto
   8.887 -  hence set1_incl: "\<And> c. c \<in> supp P \<Longrightarrow> set1 c \<subseteq> B1" using N1(2) by blast
   8.888 -  have set1_disj: "\<And> c c'. c \<noteq> c' \<Longrightarrow> set1 c \<inter> set1 c' = {}"
   8.889 -  unfolding set1_def by auto
   8.890 -  have setsum_set1: "\<And> c. setsum N1 (set1 c) = P c"
   8.891 -  unfolding P1 set1_def mmap_def apply(rule setsum_cong) by auto
   8.892 -  (*  *)
   8.893 -  def set2 \<equiv> "\<lambda> c. {b2 \<in> supp N2. f2 b2 = c}"
   8.894 -  have set2[simp]: "\<And> c b2. b2 \<in> set2 c \<Longrightarrow> f2 b2 = c" unfolding set2_def by auto
   8.895 -  have fin_set2: "\<And> c. c \<in> supp P \<Longrightarrow> finite (set2 c)"
   8.896 -  using N2(1) unfolding set2_def multiset_def by auto
   8.897 -  have set2_NE: "\<And> c. c \<in> supp P \<Longrightarrow> set2 c \<noteq> {}"
   8.898 -  unfolding set2_def P2 mmap_ge_0[OF N2(1)] by auto
   8.899 -  have supp_N2_set2: "supp N2 = (\<Union> c \<in> supp P. set2 c)"
   8.900 -  using supp_vimage_mmap[OF N2(1), of f2] unfolding set2_def P2 by auto
   8.901 -  hence set2_inclN2: "\<And>c. c \<in> supp P \<Longrightarrow> set2 c \<subseteq> supp N2" by auto
   8.902 -  hence set2_incl: "\<And> c. c \<in> supp P \<Longrightarrow> set2 c \<subseteq> B2" using N2(2) by blast
   8.903 -  have set2_disj: "\<And> c c'. c \<noteq> c' \<Longrightarrow> set2 c \<inter> set2 c' = {}"
   8.904 -  unfolding set2_def by auto
   8.905 -  have setsum_set2: "\<And> c. setsum N2 (set2 c) = P c"
   8.906 -  unfolding P2 set2_def mmap_def apply(rule setsum_cong) by auto
   8.907 -  (*  *)
   8.908 -  have ss: "\<And> c. c \<in> supp P \<Longrightarrow> setsum N1 (set1 c) = setsum N2 (set2 c)"
   8.909 -  unfolding setsum_set1 setsum_set2 ..
   8.910 -  have "\<forall> c \<in> supp P. \<forall> b1b2 \<in> (set1 c) \<times> (set2 c).
   8.911 -          \<exists> a \<in> A. p1 a = fst b1b2 \<and> p2 a = snd b1b2"
   8.912 -  using wp set1_incl set2_incl unfolding wpull_def Ball_def mem_Collect_eq
   8.913 -  by simp (metis set1 set2 set_rev_mp)
   8.914 -  then obtain uu where uu:
   8.915 -  "\<forall> c \<in> supp P. \<forall> b1b2 \<in> (set1 c) \<times> (set2 c).
   8.916 -     uu c b1b2 \<in> A \<and> p1 (uu c b1b2) = fst b1b2 \<and> p2 (uu c b1b2) = snd b1b2" by metis
   8.917 -  def u \<equiv> "\<lambda> c b1 b2. uu c (b1,b2)"
   8.918 -  have u[simp]:
   8.919 -  "\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk> \<Longrightarrow> u c b1 b2 \<in> A"
   8.920 -  "\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk> \<Longrightarrow> p1 (u c b1 b2) = b1"
   8.921 -  "\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk> \<Longrightarrow> p2 (u c b1 b2) = b2"
   8.922 -  using uu unfolding u_def by auto
   8.923 -  {fix c assume c: "c \<in> supp P"
   8.924 -   have "inj2 (u c) (set1 c) (set2 c)" unfolding inj2_def proof clarify
   8.925 -     fix b1 b1' b2 b2'
   8.926 -     assume "{b1, b1'} \<subseteq> set1 c" "{b2, b2'} \<subseteq> set2 c" and 0: "u c b1 b2 = u c b1' b2'"
   8.927 -     hence "p1 (u c b1 b2) = b1 \<and> p2 (u c b1 b2) = b2 \<and>
   8.928 -            p1 (u c b1' b2') = b1' \<and> p2 (u c b1' b2') = b2'"
   8.929 -     using u(2)[OF c] u(3)[OF c] by simp metis
   8.930 -     thus "b1 = b1' \<and> b2 = b2'" using 0 by auto
   8.931 -   qed
   8.932 -  } note inj = this
   8.933 -  def sset \<equiv> "\<lambda> c. {u c b1 b2 | b1 b2. b1 \<in> set1 c \<and> b2 \<in> set2 c}"
   8.934 -  have fin_sset[simp]: "\<And> c. c \<in> supp P \<Longrightarrow> finite (sset c)" unfolding sset_def
   8.935 -  using fin_set1 fin_set2 finite_twosets by blast
   8.936 -  have sset_A: "\<And> c. c \<in> supp P \<Longrightarrow> sset c \<subseteq> A" unfolding sset_def by auto
   8.937 -  {fix c a assume c: "c \<in> supp P" and ac: "a \<in> sset c"
   8.938 -   then obtain b1 b2 where b1: "b1 \<in> set1 c" and b2: "b2 \<in> set2 c"
   8.939 -   and a: "a = u c b1 b2" unfolding sset_def by auto
   8.940 -   have "p1 a \<in> set1 c" and p2a: "p2 a \<in> set2 c"
   8.941 -   using ac a b1 b2 c u(2) u(3) by simp+
   8.942 -   hence "u c (p1 a) (p2 a) = a" unfolding a using b1 b2 inj[OF c]
   8.943 -   unfolding inj2_def by (metis c u(2) u(3))
   8.944 -  } note u_p12[simp] = this
   8.945 -  {fix c a assume c: "c \<in> supp P" and ac: "a \<in> sset c"
   8.946 -   hence "p1 a \<in> set1 c" unfolding sset_def by auto
   8.947 -  }note p1[simp] = this
   8.948 -  {fix c a assume c: "c \<in> supp P" and ac: "a \<in> sset c"
   8.949 -   hence "p2 a \<in> set2 c" unfolding sset_def by auto
   8.950 -  }note p2[simp] = this
   8.951 -  (*  *)
   8.952 -  {fix c assume c: "c \<in> supp P"
   8.953 -   hence "\<exists> M. (\<forall> b1 \<in> set1 c. setsum (\<lambda> b2. M (u c b1 b2)) (set2 c) = N1 b1) \<and>
   8.954 -               (\<forall> b2 \<in> set2 c. setsum (\<lambda> b1. M (u c b1 b2)) (set1 c) = N2 b2)"
   8.955 -   unfolding sset_def
   8.956 -   using matrix_count_finite[OF set1_NE[OF c] fin_set1[OF c]
   8.957 -                                set2_NE[OF c] fin_set2[OF c] inj[OF c] ss[OF c]] by auto
   8.958 -  }
   8.959 -  then obtain Ms where
   8.960 -  ss1: "\<And> c b1. \<lbrakk>c \<in> supp P; b1 \<in> set1 c\<rbrakk> \<Longrightarrow>
   8.961 -                   setsum (\<lambda> b2. Ms c (u c b1 b2)) (set2 c) = N1 b1" and
   8.962 -  ss2: "\<And> c b2. \<lbrakk>c \<in> supp P; b2 \<in> set2 c\<rbrakk> \<Longrightarrow>
   8.963 -                   setsum (\<lambda> b1. Ms c (u c b1 b2)) (set1 c) = N2 b2"
   8.964 -  by metis
   8.965 -  def SET \<equiv> "\<Union> c \<in> supp P. sset c"
   8.966 -  have fin_SET[simp]: "finite SET" unfolding SET_def apply(rule finite_UN_I) by auto
   8.967 -  have SET_A: "SET \<subseteq> A" unfolding SET_def using sset_A by auto
   8.968 -  have u_SET[simp]: "\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk> \<Longrightarrow> u c b1 b2 \<in> SET"
   8.969 -  unfolding SET_def sset_def by blast
   8.970 -  {fix c a assume c: "c \<in> supp P" and a: "a \<in> SET" and p1a: "p1 a \<in> set1 c"
   8.971 -   then obtain c' where c': "c' \<in> supp P" and ac': "a \<in> sset c'"
   8.972 -   unfolding SET_def by auto
   8.973 -   hence "p1 a \<in> set1 c'" unfolding sset_def by auto
   8.974 -   hence eq: "c = c'" using p1a c c' set1_disj by auto
   8.975 -   hence "a \<in> sset c" using ac' by simp
   8.976 -  } note p1_rev = this
   8.977 -  {fix c a assume c: "c \<in> supp P" and a: "a \<in> SET" and p2a: "p2 a \<in> set2 c"
   8.978 -   then obtain c' where c': "c' \<in> supp P" and ac': "a \<in> sset c'"
   8.979 -   unfolding SET_def by auto
   8.980 -   hence "p2 a \<in> set2 c'" unfolding sset_def by auto
   8.981 -   hence eq: "c = c'" using p2a c c' set2_disj by auto
   8.982 -   hence "a \<in> sset c" using ac' by simp
   8.983 -  } note p2_rev = this
   8.984 -  (*  *)
   8.985 -  have "\<forall> a \<in> SET. \<exists> c \<in> supp P. a \<in> sset c" unfolding SET_def by auto
   8.986 -  then obtain h where h: "\<forall> a \<in> SET. h a \<in> supp P \<and> a \<in> sset (h a)" by metis
   8.987 -  have h_u[simp]: "\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk>
   8.988 -                      \<Longrightarrow> h (u c b1 b2) = c"
   8.989 -  by (metis h p2 set2 u(3) u_SET)
   8.990 -  have h_u1: "\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk>
   8.991 -                      \<Longrightarrow> h (u c b1 b2) = f1 b1"
   8.992 -  using h unfolding sset_def by auto
   8.993 -  have h_u2: "\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk>
   8.994 -                      \<Longrightarrow> h (u c b1 b2) = f2 b2"
   8.995 -  using h unfolding sset_def by auto
   8.996 -  def M \<equiv> "\<lambda> a. if a \<in> SET \<and> p1 a \<in> supp N1 \<and> p2 a \<in> supp N2 then Ms (h a) a else 0"
   8.997 -  have sM: "supp M \<subseteq> SET" "supp M \<subseteq> p1 -` (supp N1)" "supp M \<subseteq> p2 -` (supp N2)"
   8.998 -  unfolding M_def by auto
   8.999 -  show "\<exists>M. (M \<in> multiset \<and> supp M \<subseteq> A) \<and> mmap p1 M = N1 \<and> mmap p2 M = N2"
  8.1000 -  proof(rule exI[of _ M], safe)
  8.1001 -    show "M \<in> multiset"
  8.1002 -    unfolding multiset_def using finite_subset[OF sM(1) fin_SET] by simp
  8.1003 -  next
  8.1004 -    fix a assume "0 < M a"
  8.1005 -    thus "a \<in> A" unfolding M_def using SET_A by (cases "a \<in> SET") auto
  8.1006 -  next
  8.1007 -    show "mmap p1 M = N1"
  8.1008 -    unfolding mmap_def[abs_def] proof(rule ext)
  8.1009 -      fix b1
  8.1010 -      let ?K = "{a. p1 a = b1 \<and> 0 < M a}"
  8.1011 -      show "setsum M ?K = N1 b1"
  8.1012 -      proof(cases "b1 \<in> supp N1")
  8.1013 -        case False
  8.1014 -        hence "?K = {}" using sM(2) by auto
  8.1015 -        thus ?thesis using False by auto
  8.1016 -      next
  8.1017 -        case True
  8.1018 -        def c \<equiv> "f1 b1"
  8.1019 -        have c: "c \<in> supp P" and b1: "b1 \<in> set1 c"
  8.1020 -        unfolding set1_def c_def P1 using True by (auto simp: mmap_image)
  8.1021 -        have "setsum M ?K = setsum M {a. p1 a = b1 \<and> a \<in> SET}"
  8.1022 -        apply(rule setsum_mono_zero_cong_left) unfolding M_def by auto
  8.1023 -        also have "... = setsum M ((\<lambda> b2. u c b1 b2) ` (set2 c))"
  8.1024 -        apply(rule setsum_cong) using c b1 proof safe
  8.1025 -          fix a assume p1a: "p1 a \<in> set1 c" and "0 < P c" and "a \<in> SET"
  8.1026 -          hence ac: "a \<in> sset c" using p1_rev by auto
  8.1027 -          hence "a = u c (p1 a) (p2 a)" using c by auto
  8.1028 -          moreover have "p2 a \<in> set2 c" using ac c by auto
  8.1029 -          ultimately show "a \<in> u c (p1 a) ` set2 c" by auto
  8.1030 -        next
  8.1031 -          fix b2 assume b1: "b1 \<in> set1 c" and b2: "b2 \<in> set2 c"
  8.1032 -          hence "u c b1 b2 \<in> SET" using c by auto
  8.1033 -        qed auto
  8.1034 -        also have "... = setsum (\<lambda> b2. M (u c b1 b2)) (set2 c)"
  8.1035 -        unfolding comp_def[symmetric] apply(rule setsum_reindex)
  8.1036 -        using inj unfolding inj_on_def inj2_def using b1 c u(3) by blast
  8.1037 -        also have "... = N1 b1" unfolding ss1[OF c b1, symmetric]
  8.1038 -          apply(rule setsum_cong[OF refl]) unfolding M_def
  8.1039 -          using True h_u[OF c b1] set2_def u(2,3)[OF c b1] u_SET[OF c b1] by fastforce
  8.1040 -        finally show ?thesis .
  8.1041 -      qed
  8.1042 -    qed
  8.1043 -  next
  8.1044 -    show "mmap p2 M = N2"
  8.1045 -    unfolding mmap_def[abs_def] proof(rule ext)
  8.1046 -      fix b2
  8.1047 -      let ?K = "{a. p2 a = b2 \<and> 0 < M a}"
  8.1048 -      show "setsum M ?K = N2 b2"
  8.1049 -      proof(cases "b2 \<in> supp N2")
  8.1050 -        case False
  8.1051 -        hence "?K = {}" using sM(3) by auto
  8.1052 -        thus ?thesis using False by auto
  8.1053 -      next
  8.1054 -        case True
  8.1055 -        def c \<equiv> "f2 b2"
  8.1056 -        have c: "c \<in> supp P" and b2: "b2 \<in> set2 c"
  8.1057 -        unfolding set2_def c_def P2 using True by (auto simp: mmap_image)
  8.1058 -        have "setsum M ?K = setsum M {a. p2 a = b2 \<and> a \<in> SET}"
  8.1059 -        apply(rule setsum_mono_zero_cong_left) unfolding M_def by auto
  8.1060 -        also have "... = setsum M ((\<lambda> b1. u c b1 b2) ` (set1 c))"
  8.1061 -        apply(rule setsum_cong) using c b2 proof safe
  8.1062 -          fix a assume p2a: "p2 a \<in> set2 c" and "0 < P c" and "a \<in> SET"
  8.1063 -          hence ac: "a \<in> sset c" using p2_rev by auto
  8.1064 -          hence "a = u c (p1 a) (p2 a)" using c by auto
  8.1065 -          moreover have "p1 a \<in> set1 c" using ac c by auto
  8.1066 -          ultimately show "a \<in> (\<lambda>b1. u c b1 (p2 a)) ` set1 c" by auto
  8.1067 -        next
  8.1068 -          fix b2 assume b1: "b1 \<in> set1 c" and b2: "b2 \<in> set2 c"
  8.1069 -          hence "u c b1 b2 \<in> SET" using c by auto
  8.1070 -        qed auto
  8.1071 -        also have "... = setsum (M o (\<lambda> b1. u c b1 b2)) (set1 c)"
  8.1072 -        apply(rule setsum_reindex)
  8.1073 -        using inj unfolding inj_on_def inj2_def using b2 c u(2) by blast
  8.1074 -        also have "... = setsum (\<lambda> b1. M (u c b1 b2)) (set1 c)"
  8.1075 -        unfolding comp_def[symmetric] by simp
  8.1076 -        also have "... = N2 b2" unfolding ss2[OF c b2, symmetric]
  8.1077 -          apply(rule setsum_cong[OF refl]) unfolding M_def set2_def
  8.1078 -          using True h_u1[OF c _ b2] u(2,3)[OF c _ b2] u_SET[OF c _ b2]
  8.1079 -          unfolding set1_def by fastforce
  8.1080 -        finally show ?thesis .
  8.1081 -      qed
  8.1082 -    qed
  8.1083 -  qed
  8.1084 -qed
  8.1085 -
  8.1086 -definition mset_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
  8.1087 -"mset_map h = Abs_multiset \<circ> mmap h \<circ> count"
  8.1088 -
  8.1089 -bnf_def mset = mset_map [set_of] "\<lambda>_::'a multiset. natLeq" ["{#}"]
  8.1090 -unfolding mset_map_def
  8.1091 -proof -
  8.1092 -  show "Abs_multiset \<circ> mmap id \<circ> count = id" unfolding mmap_id by (auto simp: count_inverse)
  8.1093 -next
  8.1094 -  fix f g
  8.1095 -  show "Abs_multiset \<circ> mmap (g \<circ> f) \<circ> count =
  8.1096 -        Abs_multiset \<circ> mmap g \<circ> count \<circ> (Abs_multiset \<circ> mmap f \<circ> count)"
  8.1097 -  unfolding comp_def apply(rule ext)
  8.1098 -  by (auto simp: Abs_multiset_inverse count mmap_comp1 mmap)
  8.1099 -next
  8.1100 -  fix M f g assume eq: "\<And>a. a \<in> set_of M \<Longrightarrow> f a = g a"
  8.1101 -  thus "(Abs_multiset \<circ> mmap f \<circ> count) M = (Abs_multiset \<circ> mmap g \<circ> count) M" apply auto
  8.1102 -  unfolding cIm_def[abs_def] image_def
  8.1103 -  by (auto intro!: mmap_cong simp: Abs_multiset_inject count mmap)
  8.1104 -next
  8.1105 -  fix f show "set_of \<circ> (Abs_multiset \<circ> mmap f \<circ> count) = op ` f \<circ> set_of"
  8.1106 -  by (auto simp: count mmap mmap_image set_of_Abs_multiset supp_count)
  8.1107 -next
  8.1108 -  show "card_order natLeq" by (rule natLeq_card_order)
  8.1109 -next
  8.1110 -  show "cinfinite natLeq" by (rule natLeq_cinfinite)
  8.1111 -next
  8.1112 -  fix M show "|set_of M| \<le>o natLeq"
  8.1113 -  apply(rule ordLess_imp_ordLeq)
  8.1114 -  unfolding finite_iff_ordLess_natLeq[symmetric] using finite_set_of .
  8.1115 -next
  8.1116 -  fix A :: "'a set"
  8.1117 -  have "|{M. set_of M \<subseteq> A}| \<le>o |{as. set as \<subseteq> A}|" using card_of_set_of .
  8.1118 -  also have "|{as. set as \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq"
  8.1119 -  by (rule list_in_bd)
  8.1120 -  finally show "|{M. set_of M \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" .
  8.1121 -next
  8.1122 -  fix A B1 B2 f1 f2 p1 p2
  8.1123 -  let ?map = "\<lambda> f. Abs_multiset \<circ> mmap f \<circ> count"
  8.1124 -  assume wp: "wpull A B1 B2 f1 f2 p1 p2"
  8.1125 -  show "wpull {x. set_of x \<subseteq> A} {x. set_of x \<subseteq> B1} {x. set_of x \<subseteq> B2}
  8.1126 -              (?map f1) (?map f2) (?map p1) (?map p2)"
  8.1127 -  unfolding wpull_def proof safe
  8.1128 -    fix y1 y2
  8.1129 -    assume y1: "set_of y1 \<subseteq> B1" and y2: "set_of y2 \<subseteq> B2"
  8.1130 -    and m: "?map f1 y1 = ?map f2 y2"
  8.1131 -    def N1 \<equiv> "count y1"  def N2 \<equiv> "count y2"
  8.1132 -    have "N1 \<in> multiset \<and> supp N1 \<subseteq> B1" and "N2 \<in> multiset \<and> supp N2 \<subseteq> B2"
  8.1133 -    and "mmap f1 N1 = mmap f2 N2"
  8.1134 -    using y1 y2 m unfolding N1_def N2_def
  8.1135 -    by (auto simp: Abs_multiset_inject count mmap)
  8.1136 -    then obtain M where M: "M \<in> multiset \<and> supp M \<subseteq> A"
  8.1137 -    and N1: "mmap p1 M = N1" and N2: "mmap p2 M = N2"
  8.1138 -    using wp_mmap[OF wp] unfolding wpull_def by auto
  8.1139 -    def x \<equiv> "Abs_multiset M"
  8.1140 -    show "\<exists>x\<in>{x. set_of x \<subseteq> A}. ?map p1 x = y1 \<and> ?map p2 x = y2"
  8.1141 -    apply(intro bexI[of _ x]) using M N1 N2 unfolding N1_def N2_def x_def
  8.1142 -    by (auto simp: count_inverse Abs_multiset_inverse)
  8.1143 -  qed
  8.1144 -qed (unfold set_of_empty, auto)
  8.1145 -
  8.1146  end
     9.1 --- a/src/HOL/Codatatype/Codatatype.thy	Wed Sep 12 05:03:18 2012 +0200
     9.2 +++ b/src/HOL/Codatatype/Codatatype.thy	Wed Sep 12 05:21:47 2012 +0200
     9.3 @@ -10,7 +10,7 @@
     9.4  header {* The (Co)datatype Package *}
     9.5  
     9.6  theory Codatatype
     9.7 -imports BNF_LFP BNF_GFP
     9.8 +imports More_BNFs
     9.9  begin
    9.10  
    9.11  end
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Codatatype/More_BNFs.thy	Wed Sep 12 05:21:47 2012 +0200
    10.3 @@ -0,0 +1,1180 @@
    10.4 +(*  Title:      HOL/Codatatype/More_BNFs.thy
    10.5 +    Author:     Dmitriy Traytel, TU Muenchen
    10.6 +    Author:     Andrei Popescu, TU Muenchen
    10.7 +    Author:     Andreas Lochbihler, Karlsruhe Institute of Technology
    10.8 +    Author:     Jasmin Blanchette, TU Muenchen
    10.9 +    Copyright   2012
   10.10 +
   10.11 +Registration of various types as bounded natural functors.
   10.12 +*)
   10.13 +
   10.14 +header {* Registration of Various Types as Bounded Natural Functors *}
   10.15 +
   10.16 +theory More_BNFs
   10.17 +imports BNF_LFP BNF_GFP
   10.18 +begin
   10.19 +
   10.20 +lemma option_rec_conv_option_case: "option_rec = option_case"
   10.21 +by (simp add: fun_eq_iff split: option.split)
   10.22 +
   10.23 +bnf_def option = Option.map [Option.set] "\<lambda>_::'a option. natLeq" ["None"]
   10.24 +proof -
   10.25 +  show "Option.map id = id" by (simp add: fun_eq_iff Option.map_def split: option.split)
   10.26 +next
   10.27 +  fix f g
   10.28 +  show "Option.map (g \<circ> f) = Option.map g \<circ> Option.map f"
   10.29 +    by (auto simp add: fun_eq_iff Option.map_def split: option.split)
   10.30 +next
   10.31 +  fix f g x
   10.32 +  assume "\<And>z. z \<in> Option.set x \<Longrightarrow> f z = g z"
   10.33 +  thus "Option.map f x = Option.map g x"
   10.34 +    by (simp cong: Option.map_cong)
   10.35 +next
   10.36 +  fix f
   10.37 +  show "Option.set \<circ> Option.map f = op ` f \<circ> Option.set"
   10.38 +    by fastforce
   10.39 +next
   10.40 +  show "card_order natLeq" by (rule natLeq_card_order)
   10.41 +next
   10.42 +  show "cinfinite natLeq" by (rule natLeq_cinfinite)
   10.43 +next
   10.44 +  fix x
   10.45 +  show "|Option.set x| \<le>o natLeq"
   10.46 +    by (cases x) (simp_all add: ordLess_imp_ordLeq finite_iff_ordLess_natLeq[symmetric])
   10.47 +next
   10.48 +  fix A
   10.49 +  have unfold: "{x. Option.set x \<subseteq> A} = Some ` A \<union> {None}"
   10.50 +    by (auto simp add: option_rec_conv_option_case Option.set_def split: option.split_asm)
   10.51 +  show "|{x. Option.set x \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq"
   10.52 +    apply (rule ordIso_ordLeq_trans)
   10.53 +    apply (rule card_of_ordIso_subst[OF unfold])
   10.54 +    apply (rule ordLeq_transitive)
   10.55 +    apply (rule Un_csum)
   10.56 +    apply (rule ordLeq_transitive)
   10.57 +    apply (rule csum_mono)
   10.58 +    apply (rule card_of_image)
   10.59 +    apply (rule ordIso_ordLeq_trans)
   10.60 +    apply (rule single_cone)
   10.61 +    apply (rule cone_ordLeq_ctwo)
   10.62 +    apply (rule ordLeq_cexp1)
   10.63 +    apply (simp_all add: natLeq_cinfinite natLeq_Card_order cinfinite_not_czero Card_order_csum)
   10.64 +    done
   10.65 +next
   10.66 +  fix A B1 B2 f1 f2 p1 p2
   10.67 +  assume wpull: "wpull A B1 B2 f1 f2 p1 p2"
   10.68 +  show "wpull {x. Option.set x \<subseteq> A} {x. Option.set x \<subseteq> B1} {x. Option.set x \<subseteq> B2}
   10.69 +    (Option.map f1) (Option.map f2) (Option.map p1) (Option.map p2)"
   10.70 +    (is "wpull ?A ?B1 ?B2 ?f1 ?f2 ?p1 ?p2")
   10.71 +    unfolding wpull_def
   10.72 +  proof (intro strip, elim conjE)
   10.73 +    fix b1 b2
   10.74 +    assume "b1 \<in> ?B1" "b2 \<in> ?B2" "?f1 b1 = ?f2 b2"
   10.75 +    thus "\<exists>a \<in> ?A. ?p1 a = b1 \<and> ?p2 a = b2" using wpull
   10.76 +      unfolding wpull_def by (cases b2) (auto 4 5)
   10.77 +  qed
   10.78 +next
   10.79 +  fix z
   10.80 +  assume "z \<in> Option.set None"
   10.81 +  thus False by simp
   10.82 +qed
   10.83 +
   10.84 +lemma card_of_list_in:
   10.85 +  "|{xs. set xs \<subseteq> A}| \<le>o |Pfunc (UNIV :: nat set) A|" (is "|?LHS| \<le>o |?RHS|")
   10.86 +proof -
   10.87 +  let ?f = "%xs. %i. if i < length xs \<and> set xs \<subseteq> A then Some (nth xs i) else None"
   10.88 +  have "inj_on ?f ?LHS" unfolding inj_on_def fun_eq_iff
   10.89 +  proof safe
   10.90 +    fix xs :: "'a list" and ys :: "'a list"
   10.91 +    assume su: "set xs \<subseteq> A" "set ys \<subseteq> A" and eq: "\<forall>i. ?f xs i = ?f ys i"
   10.92 +    hence *: "length xs = length ys"
   10.93 +    by (metis linorder_cases option.simps(2) order_less_irrefl)
   10.94 +    thus "xs = ys" by (rule nth_equalityI) (metis * eq su option.inject)
   10.95 +  qed
   10.96 +  moreover have "?f ` ?LHS \<subseteq> ?RHS" unfolding Pfunc_def by fastforce
   10.97 +  ultimately show ?thesis using card_of_ordLeq by blast
   10.98 +qed
   10.99 +
  10.100 +lemma list_in_empty: "A = {} \<Longrightarrow> {x. set x \<subseteq> A} = {[]}"
  10.101 +by simp
  10.102 +
  10.103 +lemma card_of_Func: "|Func A B| =o |B| ^c |A|"
  10.104 +unfolding cexp_def Field_card_of by (rule card_of_refl)
  10.105 +
  10.106 +lemma not_emp_czero_notIn_ordIso_Card_order:
  10.107 +"A \<noteq> {} \<Longrightarrow> ( |A|, czero) \<notin> ordIso \<and> Card_order |A|"
  10.108 +  apply (rule conjI)
  10.109 +  apply (metis Field_card_of czeroE)
  10.110 +  by (rule card_of_Card_order)
  10.111 +
  10.112 +lemma list_in_bd: "|{x. set x \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq"
  10.113 +proof -
  10.114 +  fix A :: "'a set"
  10.115 +  show "|{x. set x \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq"
  10.116 +  proof (cases "A = {}")
  10.117 +    case False thus ?thesis
  10.118 +      apply -
  10.119 +      apply (rule ordLeq_transitive)
  10.120 +      apply (rule card_of_list_in)
  10.121 +      apply (rule ordLeq_transitive)
  10.122 +      apply (erule card_of_Pfunc_Pow_Func)
  10.123 +      apply (rule ordIso_ordLeq_trans)
  10.124 +      apply (rule Times_cprod)
  10.125 +      apply (rule cprod_cinfinite_bound)
  10.126 +      apply (rule ordIso_ordLeq_trans)
  10.127 +      apply (rule Pow_cexp_ctwo)
  10.128 +      apply (rule ordIso_ordLeq_trans)
  10.129 +      apply (rule cexp_cong2)
  10.130 +      apply (rule card_of_nat)
  10.131 +      apply (rule Card_order_ctwo)
  10.132 +      apply (rule card_of_Card_order)
  10.133 +      apply (rule natLeq_Card_order)
  10.134 +      apply (rule disjI1)
  10.135 +      apply (rule ctwo_Cnotzero)
  10.136 +      apply (rule cexp_mono1)
  10.137 +      apply (rule ordLeq_csum2)
  10.138 +      apply (rule Card_order_ctwo)
  10.139 +      apply (rule disjI1)
  10.140 +      apply (rule ctwo_Cnotzero)
  10.141 +      apply (rule natLeq_Card_order)
  10.142 +      apply (rule ordIso_ordLeq_trans)
  10.143 +      apply (rule card_of_Func)
  10.144 +      apply (rule ordIso_ordLeq_trans)
  10.145 +      apply (rule cexp_cong2)
  10.146 +      apply (rule card_of_nat)
  10.147 +      apply (rule card_of_Card_order)
  10.148 +      apply (rule card_of_Card_order)
  10.149 +      apply (rule natLeq_Card_order)
  10.150 +      apply (rule disjI1)
  10.151 +      apply (erule not_emp_czero_notIn_ordIso_Card_order)
  10.152 +      apply (rule cexp_mono1)
  10.153 +      apply (rule ordLeq_csum1)
  10.154 +      apply (rule card_of_Card_order)
  10.155 +      apply (rule disjI1)
  10.156 +      apply (erule not_emp_czero_notIn_ordIso_Card_order)
  10.157 +      apply (rule natLeq_Card_order)
  10.158 +      apply (rule card_of_Card_order)
  10.159 +      apply (rule card_of_Card_order)
  10.160 +      apply (rule Cinfinite_cexp)
  10.161 +      apply (rule ordLeq_csum2)
  10.162 +      apply (rule Card_order_ctwo)
  10.163 +      apply (rule conjI)
  10.164 +      apply (rule natLeq_cinfinite)
  10.165 +      by (rule natLeq_Card_order)
  10.166 +  next
  10.167 +    case True thus ?thesis
  10.168 +      apply -
  10.169 +      apply (rule ordIso_ordLeq_trans)
  10.170 +      apply (rule card_of_ordIso_subst)
  10.171 +      apply (erule list_in_empty)
  10.172 +      apply (rule ordIso_ordLeq_trans)
  10.173 +      apply (rule single_cone)
  10.174 +      apply (rule cone_ordLeq_cexp)
  10.175 +      apply (rule ordLeq_transitive)
  10.176 +      apply (rule cone_ordLeq_ctwo)
  10.177 +      apply (rule ordLeq_csum2)
  10.178 +      by (rule Card_order_ctwo)
  10.179 +  qed
  10.180 +qed
  10.181 +
  10.182 +bnf_def list = map [set] "\<lambda>_::'a list. natLeq" ["[]"]
  10.183 +proof -
  10.184 +  show "map id = id" by (rule List.map.id)
  10.185 +next
  10.186 +  fix f g
  10.187 +  show "map (g o f) = map g o map f" by (rule List.map.comp[symmetric])
  10.188 +next
  10.189 +  fix x f g
  10.190 +  assume "\<And>z. z \<in> set x \<Longrightarrow> f z = g z"
  10.191 +  thus "map f x = map g x" by simp
  10.192 +next
  10.193 +  fix f
  10.194 +  show "set o map f = image f o set" by (rule ext, unfold o_apply, rule set_map)
  10.195 +next
  10.196 +  show "card_order natLeq" by (rule natLeq_card_order)
  10.197 +next
  10.198 +  show "cinfinite natLeq" by (rule natLeq_cinfinite)
  10.199 +next
  10.200 +  fix x
  10.201 +  show "|set x| \<le>o natLeq"
  10.202 +    apply (rule ordLess_imp_ordLeq)
  10.203 +    apply (rule finite_ordLess_infinite[OF _ natLeq_Well_order])
  10.204 +    unfolding Field_natLeq Field_card_of by (auto simp: card_of_well_order_on)
  10.205 +next
  10.206 +  fix A :: "'a set"
  10.207 +  show "|{x. set x \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" by (rule list_in_bd)
  10.208 +next
  10.209 +  fix A B1 B2 f1 f2 p1 p2
  10.210 +  assume "wpull A B1 B2 f1 f2 p1 p2"
  10.211 +  hence pull: "\<And>b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<Longrightarrow> \<exists>a \<in> A. p1 a = b1 \<and> p2 a = b2"
  10.212 +    unfolding wpull_def by auto
  10.213 +  show "wpull {x. set x \<subseteq> A} {x. set x \<subseteq> B1} {x. set x \<subseteq> B2} (map f1) (map f2) (map p1) (map p2)"
  10.214 +    (is "wpull ?A ?B1 ?B2 _ _ _ _")
  10.215 +  proof (unfold wpull_def)
  10.216 +    { fix as bs assume *: "as \<in> ?B1" "bs \<in> ?B2" "map f1 as = map f2 bs"
  10.217 +      hence "length as = length bs" by (metis length_map)
  10.218 +      hence "\<exists>zs \<in> ?A. map p1 zs = as \<and> map p2 zs = bs" using *
  10.219 +      proof (induct as bs rule: list_induct2)
  10.220 +        case (Cons a as b bs)
  10.221 +        hence "a \<in> B1" "b \<in> B2" "f1 a = f2 b" by auto
  10.222 +        with pull obtain z where "z \<in> A" "p1 z = a" "p2 z = b" by blast
  10.223 +        moreover
  10.224 +        from Cons obtain zs where "zs \<in> ?A" "map p1 zs = as" "map p2 zs = bs" by auto
  10.225 +        ultimately have "z # zs \<in> ?A" "map p1 (z # zs) = a # as \<and> map p2 (z # zs) = b # bs" by auto
  10.226 +        thus ?case by (rule_tac x = "z # zs" in bexI)
  10.227 +      qed simp
  10.228 +    }
  10.229 +    thus "\<forall>as bs. as \<in> ?B1 \<and> bs \<in> ?B2 \<and> map f1 as = map f2 bs \<longrightarrow>
  10.230 +      (\<exists>zs \<in> ?A. map p1 zs = as \<and> map p2 zs = bs)" by blast
  10.231 +  qed
  10.232 +qed auto
  10.233 +
  10.234 +(* Finite sets *)
  10.235 +abbreviation afset where "afset \<equiv> abs_fset"
  10.236 +abbreviation rfset where "rfset \<equiv> rep_fset"
  10.237 +
  10.238 +lemma fset_fset_member:
  10.239 +"fset A = {a. a |\<in>| A}"
  10.240 +unfolding fset_def fset_member_def by auto
  10.241 +
  10.242 +lemma afset_rfset:
  10.243 +"afset (rfset x) = x"
  10.244 +by (rule Quotient_fset[unfolded Quotient_def, THEN conjunct1, rule_format])
  10.245 +
  10.246 +lemma afset_rfset_id:
  10.247 +"afset o rfset = id"
  10.248 +unfolding comp_def afset_rfset id_def ..
  10.249 +
  10.250 +lemma rfset:
  10.251 +"rfset A = rfset B \<longleftrightarrow> A = B"
  10.252 +by (metis afset_rfset)
  10.253 +
  10.254 +lemma afset_set:
  10.255 +"afset as = afset bs \<longleftrightarrow> set as = set bs"
  10.256 +using Quotient_fset unfolding Quotient_def list_eq_def by auto
  10.257 +
  10.258 +lemma surj_afset:
  10.259 +"\<exists> as. A = afset as"
  10.260 +by (metis afset_rfset)
  10.261 +
  10.262 +lemma fset_def2:
  10.263 +"fset = set o rfset"
  10.264 +unfolding fset_def map_fun_def[abs_def] by simp
  10.265 +
  10.266 +lemma fset_def2_raw:
  10.267 +"fset A = set (rfset A)"
  10.268 +unfolding fset_def2 by simp
  10.269 +
  10.270 +lemma fset_comp_afset:
  10.271 +"fset o afset = set"
  10.272 +unfolding fset_def2 comp_def apply(rule ext)
  10.273 +unfolding afset_set[symmetric] afset_rfset ..
  10.274 +
  10.275 +lemma fset_afset:
  10.276 +"fset (afset as) = set as"
  10.277 +unfolding fset_comp_afset[symmetric] by simp
  10.278 +
  10.279 +lemma set_rfset_afset:
  10.280 +"set (rfset (afset as)) = set as"
  10.281 +unfolding afset_set[symmetric] afset_rfset ..
  10.282 +
  10.283 +lemma map_fset_comp_afset:
  10.284 +"(map_fset f) o afset = afset o (map f)"
  10.285 +unfolding map_fset_def map_fun_def[abs_def] comp_def apply(rule ext)
  10.286 +unfolding afset_set set_map set_rfset_afset id_apply ..
  10.287 +
  10.288 +lemma map_fset_afset:
  10.289 +"(map_fset f) (afset as) = afset (map f as)"
  10.290 +using map_fset_comp_afset unfolding comp_def fun_eq_iff by auto
  10.291 +
  10.292 +lemma fset_map_fset:
  10.293 +"fset (map_fset f A) = (image f) (fset A)"
  10.294 +apply(subst afset_rfset[symmetric, of A])
  10.295 +unfolding map_fset_afset fset_afset set_map
  10.296 +unfolding fset_def2_raw ..
  10.297 +
  10.298 +lemma map_fset_def2:
  10.299 +"map_fset f = afset o (map f) o rfset"
  10.300 +unfolding map_fset_def map_fun_def[abs_def] by simp
  10.301 +
  10.302 +lemma map_fset_def2_raw:
  10.303 +"map_fset f A = afset (map f (rfset A))"
  10.304 +unfolding map_fset_def2 by simp
  10.305 +
  10.306 +lemma finite_ex_fset:
  10.307 +assumes "finite A"
  10.308 +shows "\<exists> B. fset B = A"
  10.309 +by (metis assms finite_list fset_afset)
  10.310 +
  10.311 +lemma wpull_image:
  10.312 +assumes "wpull A B1 B2 f1 f2 p1 p2"
  10.313 +shows "wpull (Pow A) (Pow B1) (Pow B2) (image f1) (image f2) (image p1) (image p2)"
  10.314 +unfolding wpull_def Pow_def Bex_def mem_Collect_eq proof clarify
  10.315 +  fix Y1 Y2 assume Y1: "Y1 \<subseteq> B1" and Y2: "Y2 \<subseteq> B2" and EQ: "f1 ` Y1 = f2 ` Y2"
  10.316 +  def X \<equiv> "{a \<in> A. p1 a \<in> Y1 \<and> p2 a \<in> Y2}"
  10.317 +  show "\<exists>X\<subseteq>A. p1 ` X = Y1 \<and> p2 ` X = Y2"
  10.318 +  proof (rule exI[of _ X], intro conjI)
  10.319 +    show "p1 ` X = Y1"
  10.320 +    proof
  10.321 +      show "Y1 \<subseteq> p1 ` X"
  10.322 +      proof safe
  10.323 +        fix y1 assume y1: "y1 \<in> Y1"
  10.324 +        then obtain y2 where y2: "y2 \<in> Y2" and eq: "f1 y1 = f2 y2" using EQ by auto
  10.325 +        then obtain x where "x \<in> A" and "p1 x = y1" and "p2 x = y2"
  10.326 +        using assms y1 Y1 Y2 unfolding wpull_def by blast
  10.327 +        thus "y1 \<in> p1 ` X" unfolding X_def using y1 y2 by auto
  10.328 +      qed
  10.329 +    qed(unfold X_def, auto)
  10.330 +    show "p2 ` X = Y2"
  10.331 +    proof
  10.332 +      show "Y2 \<subseteq> p2 ` X"
  10.333 +      proof safe
  10.334 +        fix y2 assume y2: "y2 \<in> Y2"
  10.335 +        then obtain y1 where y1: "y1 \<in> Y1" and eq: "f1 y1 = f2 y2" using EQ by force
  10.336 +        then obtain x where "x \<in> A" and "p1 x = y1" and "p2 x = y2"
  10.337 +        using assms y2 Y1 Y2 unfolding wpull_def by blast
  10.338 +        thus "y2 \<in> p2 ` X" unfolding X_def using y1 y2 by auto
  10.339 +      qed
  10.340 +    qed(unfold X_def, auto)
  10.341 +  qed(unfold X_def, auto)
  10.342 +qed
  10.343 +
  10.344 +lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A"
  10.345 +by (rule f_the_inv_into_f) (auto simp: inj_on_def fset_cong dest!: finite_ex_fset)
  10.346 +
  10.347 +bnf_def fset = map_fset [fset] "\<lambda>_::'a fset. natLeq" ["{||}"]
  10.348 +proof -
  10.349 +  show "map_fset id = id"
  10.350 +  unfolding map_fset_def2 map_id o_id afset_rfset_id ..
  10.351 +next
  10.352 +  fix f g
  10.353 +  show "map_fset (g o f) = map_fset g o map_fset f"
  10.354 +  unfolding map_fset_def2 map.comp[symmetric] comp_def apply(rule ext)
  10.355 +  unfolding afset_set set_map fset_def2_raw[symmetric] image_image[symmetric]
  10.356 +  unfolding map_fset_afset[symmetric] map_fset_image afset_rfset
  10.357 +  by (rule refl)
  10.358 +next
  10.359 +  fix x f g
  10.360 +  assume "\<And>z. z \<in> fset x \<Longrightarrow> f z = g z"
  10.361 +  hence "map f (rfset x) = map g (rfset x)"
  10.362 +  apply(intro map_cong) unfolding fset_def2_raw by auto
  10.363 +  thus "map_fset f x = map_fset g x" unfolding map_fset_def2_raw
  10.364 +  by (rule arg_cong)
  10.365 +next
  10.366 +  fix f
  10.367 +  show "fset o map_fset f = image f o fset"
  10.368 +  unfolding comp_def fset_map_fset ..
  10.369 +next
  10.370 +  show "card_order natLeq" by (rule natLeq_card_order)
  10.371 +next
  10.372 +  show "cinfinite natLeq" by (rule natLeq_cinfinite)
  10.373 +next
  10.374 +  fix x
  10.375 +  show "|fset x| \<le>o natLeq"
  10.376 +  unfolding fset_def2_raw
  10.377 +  apply (rule ordLess_imp_ordLeq)
  10.378 +  apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
  10.379 +  by (rule finite_set)
  10.380 +next
  10.381 +  fix A :: "'a set"
  10.382 +  have "|{x. fset x \<subseteq> A}| \<le>o |afset ` {as. set as \<subseteq> A}|"
  10.383 +  apply(rule card_of_mono1) unfolding fset_def2_raw apply auto
  10.384 +  apply (rule image_eqI)
  10.385 +  by (auto simp: afset_rfset)
  10.386 +  also have "|afset ` {as. set as \<subseteq> A}| \<le>o |{as. set as \<subseteq> A}|" using card_of_image .
  10.387 +  also have "|{as. set as \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" by (rule list_in_bd)
  10.388 +  finally show "|{x. fset x \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" .
  10.389 +next
  10.390 +  fix A B1 B2 f1 f2 p1 p2
  10.391 +  assume wp: "wpull A B1 B2 f1 f2 p1 p2"
  10.392 +  hence "wpull (Pow A) (Pow B1) (Pow B2) (image f1) (image f2) (image p1) (image p2)"
  10.393 +  by (rule wpull_image)
  10.394 +  show "wpull {x. fset x \<subseteq> A} {x. fset x \<subseteq> B1} {x. fset x \<subseteq> B2}
  10.395 +              (map_fset f1) (map_fset f2) (map_fset p1) (map_fset p2)"
  10.396 +  unfolding wpull_def Pow_def Bex_def mem_Collect_eq proof clarify
  10.397 +    fix y1 y2
  10.398 +    assume Y1: "fset y1 \<subseteq> B1" and Y2: "fset y2 \<subseteq> B2"
  10.399 +    assume "map_fset f1 y1 = map_fset f2 y2"
  10.400 +    hence EQ: "f1 ` (fset y1) = f2 ` (fset y2)" unfolding map_fset_def2_raw
  10.401 +    unfolding afset_set set_map fset_def2_raw .
  10.402 +    with Y1 Y2 obtain X where X: "X \<subseteq> A"
  10.403 +    and Y1: "p1 ` X = fset y1" and Y2: "p2 ` X = fset y2"
  10.404 +    using wpull_image[OF wp] unfolding wpull_def Pow_def
  10.405 +    unfolding Bex_def mem_Collect_eq apply -
  10.406 +    apply(erule allE[of _ "fset y1"], erule allE[of _ "fset y2"]) by auto
  10.407 +    have "\<forall> y1' \<in> fset y1. \<exists> x. x \<in> X \<and> y1' = p1 x" using Y1 by auto
  10.408 +    then obtain q1 where q1: "\<forall> y1' \<in> fset y1. q1 y1' \<in> X \<and> y1' = p1 (q1 y1')" by metis
  10.409 +    have "\<forall> y2' \<in> fset y2. \<exists> x. x \<in> X \<and> y2' = p2 x" using Y2 by auto
  10.410 +    then obtain q2 where q2: "\<forall> y2' \<in> fset y2. q2 y2' \<in> X \<and> y2' = p2 (q2 y2')" by metis
  10.411 +    def X' \<equiv> "q1 ` (fset y1) \<union> q2 ` (fset y2)"
  10.412 +    have X': "X' \<subseteq> A" and Y1: "p1 ` X' = fset y1" and Y2: "p2 ` X' = fset y2"
  10.413 +    using X Y1 Y2 q1 q2 unfolding X'_def by auto
  10.414 +    have fX': "finite X'" unfolding X'_def by simp
  10.415 +    then obtain x where X'eq: "X' = fset x" by (auto dest: finite_ex_fset)
  10.416 +    show "\<exists>x. fset x \<subseteq> A \<and> map_fset p1 x = y1 \<and> map_fset p2 x = y2"
  10.417 +    apply(intro exI[of _ "x"]) using X' Y1 Y2
  10.418 +    unfolding X'eq map_fset_def2_raw fset_def2_raw set_map[symmetric]
  10.419 +    afset_set[symmetric] afset_rfset by simp
  10.420 +  qed
  10.421 +qed auto
  10.422 +
  10.423 +lemma fset_pred[simp]: "fset_pred R a b \<longleftrightarrow>
  10.424 +  ((\<forall>t \<in> fset a. (\<exists>u \<in> fset b. R t u)) \<and>
  10.425 +   (\<forall>t \<in> fset b. (\<exists>u \<in> fset a. R u t)))" (is "?L = ?R")
  10.426 +proof
  10.427 +  assume ?L thus ?R unfolding fset_rel_def fset_pred_def
  10.428 +    Gr_def relcomp_unfold converse_unfold
  10.429 +  apply (simp add: subset_eq Ball_def)
  10.430 +  apply (rule conjI)
  10.431 +  apply (clarsimp, metis snd_conv)
  10.432 +  by (clarsimp, metis fst_conv)
  10.433 +next
  10.434 +  assume ?R
  10.435 +  def R' \<equiv> "the_inv fset (Collect (split R) \<inter> (fset a \<times> fset b))" (is "the_inv fset ?R'")
  10.436 +  have "finite ?R'" by (intro finite_Int[OF disjI2] finite_cartesian_product) auto
  10.437 +  hence *: "fset R' = ?R'" unfolding R'_def by (intro fset_to_fset)
  10.438 +  show ?L unfolding fset_rel_def fset_pred_def Gr_def relcomp_unfold converse_unfold
  10.439 +  proof (intro CollectI prod_caseI exI conjI)
  10.440 +    from * show "(R', a) = (R', map_fset fst R')" using conjunct1[OF `?R`]
  10.441 +      by (auto simp add: fset_cong[symmetric] image_def Int_def split: prod.splits)
  10.442 +    from * show "(R', b) = (R', map_fset snd R')" using conjunct2[OF `?R`]
  10.443 +      by (auto simp add: fset_cong[symmetric] image_def Int_def split: prod.splits)
  10.444 +  qed (auto simp add: *)
  10.445 +qed
  10.446 +
  10.447 +(* Countable sets *)
  10.448 +
  10.449 +lemma card_of_countable_sets_range:
  10.450 +fixes A :: "'a set"
  10.451 +shows "|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |{f::nat \<Rightarrow> 'a. range f \<subseteq> A}|"
  10.452 +apply(rule card_of_ordLeqI[of fromNat]) using inj_on_fromNat
  10.453 +unfolding inj_on_def by auto
  10.454 +
  10.455 +lemma card_of_countable_sets_Func:
  10.456 +"|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |A| ^c natLeq"
  10.457 +using card_of_countable_sets_range card_of_Func_UNIV[THEN ordIso_symmetric]
  10.458 +unfolding cexp_def Field_natLeq Field_card_of
  10.459 +by (rule ordLeq_ordIso_trans)
  10.460 +
  10.461 +lemma ordLeq_countable_subsets:
  10.462 +"|A| \<le>o |{X. X \<subseteq> A \<and> countable X}|"
  10.463 +apply (rule card_of_ordLeqI[of "\<lambda> a. {a}"]) unfolding inj_on_def by auto
  10.464 +
  10.465 +lemma finite_countable_subset:
  10.466 +"finite {X. X \<subseteq> A \<and> countable X} \<longleftrightarrow> finite A"
  10.467 +apply default
  10.468 + apply (erule contrapos_pp)
  10.469 + apply (rule card_of_ordLeq_infinite)
  10.470 + apply (rule ordLeq_countable_subsets)
  10.471 + apply assumption
  10.472 +apply (rule finite_Collect_conjI)
  10.473 +apply (rule disjI1)
  10.474 +by (erule finite_Collect_subsets)
  10.475 +
  10.476 +lemma card_of_countable_sets:
  10.477 +"|{X. X \<subseteq> A \<and> countable X}| \<le>o ( |A| +c ctwo) ^c natLeq"
  10.478 +(is "|?L| \<le>o _")
  10.479 +proof(cases "finite A")
  10.480 +  let ?R = "Func (UNIV::nat set) (A <+> (UNIV::bool set))"
  10.481 +  case True hence "finite ?L" by simp
  10.482 +  moreover have "infinite ?R"
  10.483 +  apply(rule infinite_Func[of _ "Inr True" "Inr False"]) by auto
  10.484 +  ultimately show ?thesis unfolding cexp_def csum_def ctwo_def Field_natLeq Field_card_of
  10.485 +  apply(intro ordLess_imp_ordLeq) by (rule finite_ordLess_infinite2)
  10.486 +next
  10.487 +  case False
  10.488 +  hence "|{X. X \<subseteq> A \<and> countable X}| =o |{X. X \<subseteq> A \<and> countable X} - {{}}|"
  10.489 +  by (intro card_of_infinite_diff_finitte finite.emptyI finite.insertI ordIso_symmetric)
  10.490 +     (unfold finite_countable_subset)
  10.491 +  also have "|{X. X \<subseteq> A \<and> countable X} - {{}}| \<le>o |A| ^c natLeq"
  10.492 +  using card_of_countable_sets_Func[of A] unfolding set_diff_eq by auto
  10.493 +  also have "|A| ^c natLeq \<le>o ( |A| +c ctwo) ^c natLeq"
  10.494 +  apply(rule cexp_mono1_cone_ordLeq)
  10.495 +    apply(rule ordLeq_csum1, rule card_of_Card_order)
  10.496 +    apply (rule cone_ordLeq_cexp)
  10.497 +    apply (rule cone_ordLeq_Cnotzero)
  10.498 +    using csum_Cnotzero2 ctwo_Cnotzero apply blast
  10.499 +    by (rule natLeq_Card_order)
  10.500 +  finally show ?thesis .
  10.501 +qed
  10.502 +
  10.503 +bnf_def cset = cIm [rcset] "\<lambda>_::'a cset. natLeq" ["cEmp"]
  10.504 +proof -
  10.505 +  show "cIm id = id" unfolding cIm_def[abs_def] id_def by auto
  10.506 +next
  10.507 +  fix f g show "cIm (g \<circ> f) = cIm g \<circ> cIm f"
  10.508 +  unfolding cIm_def[abs_def] apply(rule ext) unfolding comp_def by auto
  10.509 +next
  10.510 +  fix C f g assume eq: "\<And>a. a \<in> rcset C \<Longrightarrow> f a = g a"
  10.511 +  thus "cIm f C = cIm g C"
  10.512 +  unfolding cIm_def[abs_def] unfolding image_def by auto
  10.513 +next
  10.514 +  fix f show "rcset \<circ> cIm f = op ` f \<circ> rcset" unfolding cIm_def[abs_def] by auto
  10.515 +next
  10.516 +  show "card_order natLeq" by (rule natLeq_card_order)
  10.517 +next
  10.518 +  show "cinfinite natLeq" by (rule natLeq_cinfinite)
  10.519 +next
  10.520 +  fix C show "|rcset C| \<le>o natLeq" using rcset unfolding countable_def .
  10.521 +next
  10.522 +  fix A :: "'a set"
  10.523 +  have "|{Z. rcset Z \<subseteq> A}| \<le>o |acset ` {X. X \<subseteq> A \<and> countable X}|"
  10.524 +  apply(rule card_of_mono1) unfolding Pow_def image_def
  10.525 +  proof (rule Collect_mono, clarsimp)
  10.526 +    fix x
  10.527 +    assume "rcset x \<subseteq> A"
  10.528 +    hence "rcset x \<subseteq> A \<and> countable (rcset x) \<and> x = acset (rcset x)"
  10.529 +    using acset_rcset[of x] rcset[of x] by force
  10.530 +    thus "\<exists>y \<subseteq> A. countable y \<and> x = acset y" by blast
  10.531 +  qed
  10.532 +  also have "|acset ` {X. X \<subseteq> A \<and> countable X}| \<le>o |{X. X \<subseteq> A \<and> countable X}|"
  10.533 +  using card_of_image .
  10.534 +  also have "|{X. X \<subseteq> A \<and> countable X}| \<le>o ( |A| +c ctwo) ^c natLeq"
  10.535 +  using card_of_countable_sets .
  10.536 +  finally show "|{Z. rcset Z \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" .
  10.537 +next
  10.538 +  fix A B1 B2 f1 f2 p1 p2
  10.539 +  assume wp: "wpull A B1 B2 f1 f2 p1 p2"
  10.540 +  show "wpull {x. rcset x \<subseteq> A} {x. rcset x \<subseteq> B1} {x. rcset x \<subseteq> B2}
  10.541 +              (cIm f1) (cIm f2) (cIm p1) (cIm p2)"
  10.542 +  unfolding wpull_def proof safe
  10.543 +    fix y1 y2
  10.544 +    assume Y1: "rcset y1 \<subseteq> B1" and Y2: "rcset y2 \<subseteq> B2"
  10.545 +    assume "cIm f1 y1 = cIm f2 y2"
  10.546 +    hence EQ: "f1 ` (rcset y1) = f2 ` (rcset y2)"
  10.547 +    unfolding cIm_def by auto
  10.548 +    with Y1 Y2 obtain X where X: "X \<subseteq> A"
  10.549 +    and Y1: "p1 ` X = rcset y1" and Y2: "p2 ` X = rcset y2"
  10.550 +    using wpull_image[OF wp] unfolding wpull_def Pow_def
  10.551 +    unfolding Bex_def mem_Collect_eq apply -
  10.552 +    apply(erule allE[of _ "rcset y1"], erule allE[of _ "rcset y2"]) by auto
  10.553 +    have "\<forall> y1' \<in> rcset y1. \<exists> x. x \<in> X \<and> y1' = p1 x" using Y1 by auto
  10.554 +    then obtain q1 where q1: "\<forall> y1' \<in> rcset y1. q1 y1' \<in> X \<and> y1' = p1 (q1 y1')" by metis
  10.555 +    have "\<forall> y2' \<in> rcset y2. \<exists> x. x \<in> X \<and> y2' = p2 x" using Y2 by auto
  10.556 +    then obtain q2 where q2: "\<forall> y2' \<in> rcset y2. q2 y2' \<in> X \<and> y2' = p2 (q2 y2')" by metis
  10.557 +    def X' \<equiv> "q1 ` (rcset y1) \<union> q2 ` (rcset y2)"
  10.558 +    have X': "X' \<subseteq> A" and Y1: "p1 ` X' = rcset y1" and Y2: "p2 ` X' = rcset y2"
  10.559 +    using X Y1 Y2 q1 q2 unfolding X'_def by fast+
  10.560 +    have fX': "countable X'" unfolding X'_def by simp
  10.561 +    then obtain x where X'eq: "X' = rcset x" by (metis rcset_acset)
  10.562 +    show "\<exists>x\<in>{x. rcset x \<subseteq> A}. cIm p1 x = y1 \<and> cIm p2 x = y2"
  10.563 +    apply(intro bexI[of _ "x"]) using X' Y1 Y2 unfolding X'eq cIm_def by auto
  10.564 +  qed
  10.565 +qed (unfold cEmp_def, auto)
  10.566 +
  10.567 +
  10.568 +(* Multisets *)
  10.569 +
  10.570 +lemma setsum_gt_0_iff:
  10.571 +fixes f :: "'a \<Rightarrow> nat" assumes "finite A"
  10.572 +shows "setsum f A > 0 \<longleftrightarrow> (\<exists> a \<in> A. f a > 0)"
  10.573 +(is "?L \<longleftrightarrow> ?R")
  10.574 +proof-
  10.575 +  have "?L \<longleftrightarrow> \<not> setsum f A = 0" by fast
  10.576 +  also have "... \<longleftrightarrow> (\<exists> a \<in> A. f a \<noteq> 0)" using assms by simp
  10.577 +  also have "... \<longleftrightarrow> ?R" by simp
  10.578 +  finally show ?thesis .
  10.579 +qed
  10.580 +
  10.581 +(*   *)
  10.582 +definition mmap :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> 'b \<Rightarrow> nat" where
  10.583 +"mmap h f b = setsum f {a. h a = b \<and> f a > 0}"
  10.584 +
  10.585 +lemma mmap_id: "mmap id = id"
  10.586 +proof (rule ext)+
  10.587 +  fix f a show "mmap id f a = id f a"
  10.588 +  proof(cases "f a = 0")
  10.589 +    case False
  10.590 +    hence 1: "{aa. aa = a \<and> 0 < f aa} = {a}" by auto
  10.591 +    show ?thesis by (simp add: mmap_def id_apply 1)
  10.592 +  qed(unfold mmap_def, auto)
  10.593 +qed
  10.594 +
  10.595 +lemma inj_on_setsum_inv:
  10.596 +assumes f: "f \<in> multiset"
  10.597 +and 1: "(0::nat) < setsum f {a. h a = b' \<and> 0 < f a}" (is "0 < setsum f ?A'")
  10.598 +and 2: "{a. h a = b \<and> 0 < f a} = {a. h a = b' \<and> 0 < f a}" (is "?A = ?A'")
  10.599 +shows "b = b'"
  10.600 +proof-
  10.601 +  have "finite ?A'" using f unfolding multiset_def by auto
  10.602 +  hence "?A' \<noteq> {}" using 1 setsum_gt_0_iff by auto
  10.603 +  thus ?thesis using 2 by auto
  10.604 +qed
  10.605 +
  10.606 +lemma mmap_comp:
  10.607 +fixes h1 :: "'a \<Rightarrow> 'b" and h2 :: "'b \<Rightarrow> 'c"
  10.608 +assumes f: "f \<in> multiset"
  10.609 +shows "mmap (h2 o h1) f = (mmap h2 o mmap h1) f"
  10.610 +unfolding mmap_def[abs_def] comp_def proof(rule ext)+
  10.611 +  fix c :: 'c
  10.612 +  let ?A = "{a. h2 (h1 a) = c \<and> 0 < f a}"
  10.613 +  let ?As = "\<lambda> b. {a. h1 a = b \<and> 0 < f a}"
  10.614 +  let ?B = "{b. h2 b = c \<and> 0 < setsum f (?As b)}"
  10.615 +  have 0: "{?As b | b.  b \<in> ?B} = ?As ` ?B" by auto
  10.616 +  have "\<And> b. finite (?As b)" using f unfolding multiset_def by simp
  10.617 +  hence "?B = {b. h2 b = c \<and> ?As b \<noteq> {}}" using setsum_gt_0_iff by auto
  10.618 +  hence A: "?A = \<Union> {?As b | b.  b \<in> ?B}" by auto
  10.619 +  have "setsum f ?A = setsum (setsum f) {?As b | b.  b \<in> ?B}"
  10.620 +  unfolding A apply(rule setsum_Union_disjoint)
  10.621 +  using f unfolding multiset_def by auto
  10.622 +  also have "... = setsum (setsum f) (?As ` ?B)" unfolding 0 ..
  10.623 +  also have "... = setsum (setsum f o ?As) ?B" apply(rule setsum_reindex)
  10.624 +  unfolding inj_on_def apply auto using inj_on_setsum_inv[OF f, of h1] by blast
  10.625 +  also have "... = setsum (\<lambda> b. setsum f (?As b)) ?B" unfolding comp_def ..
  10.626 +  finally show "setsum f ?A = setsum (\<lambda> b. setsum f (?As b)) ?B" .
  10.627 +qed
  10.628 +
  10.629 +lemma mmap_comp1:
  10.630 +fixes h1 :: "'a \<Rightarrow> 'b" and h2 :: "'b \<Rightarrow> 'c"
  10.631 +assumes "f \<in> multiset"
  10.632 +shows "mmap (\<lambda> a. h2 (h1 a)) f = mmap h2 (mmap h1 f)"
  10.633 +using mmap_comp[OF assms] unfolding comp_def by auto
  10.634 +
  10.635 +lemma mmap:
  10.636 +assumes "f \<in> multiset"
  10.637 +shows "mmap h f \<in> multiset"
  10.638 +using assms unfolding mmap_def[abs_def] multiset_def proof safe
  10.639 +  assume fin: "finite {a. 0 < f a}"  (is "finite ?A")
  10.640 +  show "finite {b. 0 < setsum f {a. h a = b \<and> 0 < f a}}"
  10.641 +  (is "finite {b. 0 < setsum f (?As b)}")
  10.642 +  proof- let ?B = "{b. 0 < setsum f (?As b)}"
  10.643 +    have "\<And> b. finite (?As b)" using assms unfolding multiset_def by simp
  10.644 +    hence B: "?B = {b. ?As b \<noteq> {}}" using setsum_gt_0_iff by auto
  10.645 +    hence "?B \<subseteq> h ` ?A" by auto
  10.646 +    thus ?thesis using finite_surj[OF fin] by auto
  10.647 +  qed
  10.648 +qed
  10.649 +
  10.650 +lemma mmap_cong:
  10.651 +assumes "\<And>a. a \<in># M \<Longrightarrow> f a = g a"
  10.652 +shows "mmap f (count M) = mmap g (count M)"
  10.653 +using assms unfolding mmap_def[abs_def] by (intro ext, intro setsum_cong) auto
  10.654 +
  10.655 +abbreviation supp where "supp f \<equiv> {a. f a > 0}"
  10.656 +
  10.657 +lemma mmap_image_comp:
  10.658 +assumes f: "f \<in> multiset"
  10.659 +shows "(supp o mmap h) f = (image h o supp) f"
  10.660 +unfolding mmap_def[abs_def] comp_def proof-
  10.661 +  have "\<And> b. finite {a. h a = b \<and> 0 < f a}" (is "\<And> b. finite (?As b)")
  10.662 +  using f unfolding multiset_def by auto
  10.663 +  thus "{b. 0 < setsum f (?As b)} = h ` {a. 0 < f a}"
  10.664 +  using setsum_gt_0_iff by auto
  10.665 +qed
  10.666 +
  10.667 +lemma mmap_image:
  10.668 +assumes f: "f \<in> multiset"
  10.669 +shows "supp (mmap h f) = h ` (supp f)"
  10.670 +using mmap_image_comp[OF assms] unfolding comp_def .
  10.671 +
  10.672 +lemma set_of_Abs_multiset:
  10.673 +assumes f: "f \<in> multiset"
  10.674 +shows "set_of (Abs_multiset f) = supp f"
  10.675 +using assms unfolding set_of_def by (auto simp: Abs_multiset_inverse)
  10.676 +
  10.677 +lemma supp_count:
  10.678 +"supp (count M) = set_of M"
  10.679 +using assms unfolding set_of_def by auto
  10.680 +
  10.681 +lemma multiset_of_surj:
  10.682 +"multiset_of ` {as. set as \<subseteq> A} = {M. set_of M \<subseteq> A}"
  10.683 +proof safe
  10.684 +  fix M assume M: "set_of M \<subseteq> A"
  10.685 +  obtain as where eq: "M = multiset_of as" using surj_multiset_of unfolding surj_def by auto
  10.686 +  hence "set as \<subseteq> A" using M by auto
  10.687 +  thus "M \<in> multiset_of ` {as. set as \<subseteq> A}" using eq by auto
  10.688 +next
  10.689 +  show "\<And>x xa xb. \<lbrakk>set xa \<subseteq> A; xb \<in> set_of (multiset_of xa)\<rbrakk> \<Longrightarrow> xb \<in> A"
  10.690 +  by (erule set_mp) (unfold set_of_multiset_of)
  10.691 +qed
  10.692 +
  10.693 +lemma card_of_set_of:
  10.694 +"|{M. set_of M \<subseteq> A}| \<le>o |{as. set as \<subseteq> A}|"
  10.695 +apply(rule card_of_ordLeqI2[of _ multiset_of]) using multiset_of_surj by auto
  10.696 +
  10.697 +lemma nat_sum_induct:
  10.698 +assumes "\<And>n1 n2. (\<And> m1 m2. m1 + m2 < n1 + n2 \<Longrightarrow> phi m1 m2) \<Longrightarrow> phi n1 n2"
  10.699 +shows "phi (n1::nat) (n2::nat)"
  10.700 +proof-
  10.701 +  let ?chi = "\<lambda> n1n2 :: nat * nat. phi (fst n1n2) (snd n1n2)"
  10.702 +  have "?chi (n1,n2)"
  10.703 +  apply(induct rule: measure_induct[of "\<lambda> n1n2. fst n1n2 + snd n1n2" ?chi])
  10.704 +  using assms by (metis fstI sndI)
  10.705 +  thus ?thesis by simp
  10.706 +qed
  10.707 +
  10.708 +lemma matrix_count:
  10.709 +fixes ct1 ct2 :: "nat \<Rightarrow> nat"
  10.710 +assumes "setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2}"
  10.711 +shows
  10.712 +"\<exists> ct. (\<forall> i1 \<le> n1. setsum (\<lambda> i2. ct i1 i2) {..<Suc n2} = ct1 i1) \<and>
  10.713 +       (\<forall> i2 \<le> n2. setsum (\<lambda> i1. ct i1 i2) {..<Suc n1} = ct2 i2)"
  10.714 +(is "?phi ct1 ct2 n1 n2")
  10.715 +proof-
  10.716 +  have "\<forall> ct1 ct2 :: nat \<Rightarrow> nat.
  10.717 +        setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2} \<longrightarrow> ?phi ct1 ct2 n1 n2"
  10.718 +  proof(induct rule: nat_sum_induct[of
  10.719 +"\<lambda> n1 n2. \<forall> ct1 ct2 :: nat \<Rightarrow> nat.
  10.720 +     setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2} \<longrightarrow> ?phi ct1 ct2 n1 n2"],
  10.721 +      clarify)
  10.722 +  fix n1 n2 :: nat and ct1 ct2 :: "nat \<Rightarrow> nat"
  10.723 +  assume IH: "\<And> m1 m2. m1 + m2 < n1 + n2 \<Longrightarrow>
  10.724 +                \<forall> dt1 dt2 :: nat \<Rightarrow> nat.
  10.725 +                setsum dt1 {..<Suc m1} = setsum dt2 {..<Suc m2} \<longrightarrow> ?phi dt1 dt2 m1 m2"
  10.726 +  and ss: "setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2}"
  10.727 +  show "?phi ct1 ct2 n1 n2"
  10.728 +  proof(cases n1)
  10.729 +    case 0 note n1 = 0
  10.730 +    show ?thesis
  10.731 +    proof(cases n2)
  10.732 +      case 0 note n2 = 0
  10.733 +      let ?ct = "\<lambda> i1 i2. ct2 0"
  10.734 +      show ?thesis apply(rule exI[of _ ?ct]) using n1 n2 ss by simp
  10.735 +    next
  10.736 +      case (Suc m2) note n2 = Suc
  10.737 +      let ?ct = "\<lambda> i1 i2. ct2 i2"
  10.738 +      show ?thesis apply(rule exI[of _ ?ct]) using n1 n2 ss by auto
  10.739 +    qed
  10.740 +  next
  10.741 +    case (Suc m1) note n1 = Suc
  10.742 +    show ?thesis
  10.743 +    proof(cases n2)
  10.744 +      case 0 note n2 = 0
  10.745 +      let ?ct = "\<lambda> i1 i2. ct1 i1"
  10.746 +      show ?thesis apply(rule exI[of _ ?ct]) using n1 n2 ss by auto
  10.747 +    next
  10.748 +      case (Suc m2) note n2 = Suc
  10.749 +      show ?thesis
  10.750 +      proof(cases "ct1 n1 \<le> ct2 n2")
  10.751 +        case True
  10.752 +        def dt2 \<equiv> "\<lambda> i2. if i2 = n2 then ct2 i2 - ct1 n1 else ct2 i2"
  10.753 +        have "setsum ct1 {..<Suc m1} = setsum dt2 {..<Suc n2}"
  10.754 +        unfolding dt2_def using ss n1 True by auto
  10.755 +        hence "?phi ct1 dt2 m1 n2" using IH[of m1 n2] n1 by simp
  10.756 +        then obtain dt where
  10.757 +        1: "\<And> i1. i1 \<le> m1 \<Longrightarrow> setsum (\<lambda> i2. dt i1 i2) {..<Suc n2} = ct1 i1" and
  10.758 +        2: "\<And> i2. i2 \<le> n2 \<Longrightarrow> setsum (\<lambda> i1. dt i1 i2) {..<Suc m1} = dt2 i2" by auto
  10.759 +        let ?ct = "\<lambda> i1 i2. if i1 = n1 then (if i2 = n2 then ct1 n1 else 0)
  10.760 +                                       else dt i1 i2"
  10.761 +        show ?thesis apply(rule exI[of _ ?ct])
  10.762 +        using n1 n2 1 2 True unfolding dt2_def by simp
  10.763 +      next
  10.764 +        case False
  10.765 +        hence False: "ct2 n2 < ct1 n1" by simp
  10.766 +        def dt1 \<equiv> "\<lambda> i1. if i1 = n1 then ct1 i1 - ct2 n2 else ct1 i1"
  10.767 +        have "setsum dt1 {..<Suc n1} = setsum ct2 {..<Suc m2}"
  10.768 +        unfolding dt1_def using ss n2 False by auto
  10.769 +        hence "?phi dt1 ct2 n1 m2" using IH[of n1 m2] n2 by simp
  10.770 +        then obtain dt where
  10.771 +        1: "\<And> i1. i1 \<le> n1 \<Longrightarrow> setsum (\<lambda> i2. dt i1 i2) {..<Suc m2} = dt1 i1" and
  10.772 +        2: "\<And> i2. i2 \<le> m2 \<Longrightarrow> setsum (\<lambda> i1. dt i1 i2) {..<Suc n1} = ct2 i2" by force
  10.773 +        let ?ct = "\<lambda> i1 i2. if i2 = n2 then (if i1 = n1 then ct2 n2 else 0)
  10.774 +                                       else dt i1 i2"
  10.775 +        show ?thesis apply(rule exI[of _ ?ct])
  10.776 +        using n1 n2 1 2 False unfolding dt1_def by simp
  10.777 +      qed
  10.778 +    qed
  10.779 +  qed
  10.780 +  qed
  10.781 +  thus ?thesis using assms by auto
  10.782 +qed
  10.783 +
  10.784 +definition
  10.785 +"inj2 u B1 B2 \<equiv>
  10.786 + \<forall> b1 b1' b2 b2'. {b1,b1'} \<subseteq> B1 \<and> {b2,b2'} \<subseteq> B2 \<and> u b1 b2 = u b1' b2'
  10.787 +                  \<longrightarrow> b1 = b1' \<and> b2 = b2'"
  10.788 +
  10.789 +lemma matrix_count_finite:
  10.790 +assumes B1: "B1 \<noteq> {}" "finite B1" and B2: "B2 \<noteq> {}" "finite B2" and u: "inj2 u B1 B2"
  10.791 +and ss: "setsum N1 B1 = setsum N2 B2"
  10.792 +shows "\<exists> M :: 'a \<Rightarrow> nat.
  10.793 +            (\<forall> b1 \<in> B1. setsum (\<lambda> b2. M (u b1 b2)) B2 = N1 b1) \<and>
  10.794 +            (\<forall> b2 \<in> B2. setsum (\<lambda> b1. M (u b1 b2)) B1 = N2 b2)"
  10.795 +proof-
  10.796 +  obtain n1 where "card B1 = Suc n1" using B1 by (metis card_insert finite.simps)
  10.797 +  then obtain e1 where e1: "bij_betw e1 {..<Suc n1} B1"
  10.798 +  using ex_bij_betw_finite_nat[OF B1(2)] by (metis atLeast0LessThan bij_betw_the_inv_into)
  10.799 +  hence e1_inj: "inj_on e1 {..<Suc n1}" and e1_surj: "e1 ` {..<Suc n1} = B1"
  10.800 +  unfolding bij_betw_def by auto
  10.801 +  def f1 \<equiv> "inv_into {..<Suc n1} e1"
  10.802 +  have f1: "bij_betw f1 B1 {..<Suc n1}"
  10.803 +  and f1e1[simp]: "\<And> i1. i1 < Suc n1 \<Longrightarrow> f1 (e1 i1) = i1"
  10.804 +  and e1f1[simp]: "\<And> b1. b1 \<in> B1 \<Longrightarrow> e1 (f1 b1) = b1" unfolding f1_def
  10.805 +  apply (metis bij_betw_inv_into e1, metis bij_betw_inv_into_left e1 lessThan_iff)
  10.806 +  by (metis e1_surj f_inv_into_f)
  10.807 +  (*  *)
  10.808 +  obtain n2 where "card B2 = Suc n2" using B2 by (metis card_insert finite.simps)
  10.809 +  then obtain e2 where e2: "bij_betw e2 {..<Suc n2} B2"
  10.810 +  using ex_bij_betw_finite_nat[OF B2(2)] by (metis atLeast0LessThan bij_betw_the_inv_into)
  10.811 +  hence e2_inj: "inj_on e2 {..<Suc n2}" and e2_surj: "e2 ` {..<Suc n2} = B2"
  10.812 +  unfolding bij_betw_def by auto
  10.813 +  def f2 \<equiv> "inv_into {..<Suc n2} e2"
  10.814 +  have f2: "bij_betw f2 B2 {..<Suc n2}"
  10.815 +  and f2e2[simp]: "\<And> i2. i2 < Suc n2 \<Longrightarrow> f2 (e2 i2) = i2"
  10.816 +  and e2f2[simp]: "\<And> b2. b2 \<in> B2 \<Longrightarrow> e2 (f2 b2) = b2" unfolding f2_def
  10.817 +  apply (metis bij_betw_inv_into e2, metis bij_betw_inv_into_left e2 lessThan_iff)
  10.818 +  by (metis e2_surj f_inv_into_f)
  10.819 +  (*  *)
  10.820 +  let ?ct1 = "N1 o e1"  let ?ct2 = "N2 o e2"
  10.821 +  have ss: "setsum ?ct1 {..<Suc n1} = setsum ?ct2 {..<Suc n2}"
  10.822 +  unfolding setsum_reindex[OF e1_inj, symmetric] setsum_reindex[OF e2_inj, symmetric]
  10.823 +  e1_surj e2_surj using ss .
  10.824 +  obtain ct where
  10.825 +  ct1: "\<And> i1. i1 \<le> n1 \<Longrightarrow> setsum (\<lambda> i2. ct i1 i2) {..<Suc n2} = ?ct1 i1" and
  10.826 +  ct2: "\<And> i2. i2 \<le> n2 \<Longrightarrow> setsum (\<lambda> i1. ct i1 i2) {..<Suc n1} = ?ct2 i2"
  10.827 +  using matrix_count[OF ss] by blast
  10.828 +  (*  *)
  10.829 +  def A \<equiv> "{u b1 b2 | b1 b2. b1 \<in> B1 \<and> b2 \<in> B2}"
  10.830 +  have "\<forall> a \<in> A. \<exists> b1b2 \<in> B1 <*> B2. u (fst b1b2) (snd b1b2) = a"
  10.831 +  unfolding A_def Ball_def mem_Collect_eq by auto
  10.832 +  then obtain h1h2 where h12:
  10.833 +  "\<And>a. a \<in> A \<Longrightarrow> u (fst (h1h2 a)) (snd (h1h2 a)) = a \<and> h1h2 a \<in> B1 <*> B2" by metis
  10.834 +  def h1 \<equiv> "fst o h1h2"  def h2 \<equiv> "snd o h1h2"
  10.835 +  have h12[simp]: "\<And>a. a \<in> A \<Longrightarrow> u (h1 a) (h2 a) = a"
  10.836 +                  "\<And> a. a \<in> A \<Longrightarrow> h1 a \<in> B1"  "\<And> a. a \<in> A \<Longrightarrow> h2 a \<in> B2"
  10.837 +  using h12 unfolding h1_def h2_def by force+
  10.838 +  {fix b1 b2 assume b1: "b1 \<in> B1" and b2: "b2 \<in> B2"
  10.839 +   hence inA: "u b1 b2 \<in> A" unfolding A_def by auto
  10.840 +   hence "u b1 b2 = u (h1 (u b1 b2)) (h2 (u b1 b2))" by auto
  10.841 +   moreover have "h1 (u b1 b2) \<in> B1" "h2 (u b1 b2) \<in> B2" using inA by auto
  10.842 +   ultimately have "h1 (u b1 b2) = b1 \<and> h2 (u b1 b2) = b2"
  10.843 +   using u b1 b2 unfolding inj2_def by fastforce
  10.844 +  }
  10.845 +  hence h1[simp]: "\<And> b1 b2. \<lbrakk>b1 \<in> B1; b2 \<in> B2\<rbrakk> \<Longrightarrow> h1 (u b1 b2) = b1" and
  10.846 +        h2[simp]: "\<And> b1 b2. \<lbrakk>b1 \<in> B1; b2 \<in> B2\<rbrakk> \<Longrightarrow> h2 (u b1 b2) = b2" by auto
  10.847 +  def M \<equiv> "\<lambda> a. ct (f1 (h1 a)) (f2 (h2 a))"
  10.848 +  show ?thesis
  10.849 +  apply(rule exI[of _ M]) proof safe
  10.850 +    fix b1 assume b1: "b1 \<in> B1"
  10.851 +    hence f1b1: "f1 b1 \<le> n1" using f1 unfolding bij_betw_def
  10.852 +    by (metis bij_betwE f1 lessThan_iff less_Suc_eq_le)
  10.853 +    have "(\<Sum>b2\<in>B2. M (u b1 b2)) = (\<Sum>i2<Suc n2. ct (f1 b1) (f2 (e2 i2)))"
  10.854 +    unfolding e2_surj[symmetric] setsum_reindex[OF e2_inj]
  10.855 +    unfolding M_def comp_def apply(intro setsum_cong) apply force
  10.856 +    by (metis e2_surj b1 h1 h2 imageI)
  10.857 +    also have "... = N1 b1" using b1 ct1[OF f1b1] by simp
  10.858 +    finally show "(\<Sum>b2\<in>B2. M (u b1 b2)) = N1 b1" .
  10.859 +  next
  10.860 +    fix b2 assume b2: "b2 \<in> B2"
  10.861 +    hence f2b2: "f2 b2 \<le> n2" using f2 unfolding bij_betw_def
  10.862 +    by (metis bij_betwE f2 lessThan_iff less_Suc_eq_le)
  10.863 +    have "(\<Sum>b1\<in>B1. M (u b1 b2)) = (\<Sum>i1<Suc n1. ct (f1 (e1 i1)) (f2 b2))"
  10.864 +    unfolding e1_surj[symmetric] setsum_reindex[OF e1_inj]
  10.865 +    unfolding M_def comp_def apply(intro setsum_cong) apply force
  10.866 +    by (metis e1_surj b2 h1 h2 imageI)
  10.867 +    also have "... = N2 b2" using b2 ct2[OF f2b2] by simp
  10.868 +    finally show "(\<Sum>b1\<in>B1. M (u b1 b2)) = N2 b2" .
  10.869 +  qed
  10.870 +qed
  10.871 +
  10.872 +lemma supp_vimage_mmap:
  10.873 +assumes "M \<in> multiset"
  10.874 +shows "supp M \<subseteq> f -` (supp (mmap f M))"
  10.875 +using assms by (auto simp: mmap_image)
  10.876 +
  10.877 +lemma mmap_ge_0:
  10.878 +assumes "M \<in> multiset"
  10.879 +shows "0 < mmap f M b \<longleftrightarrow> (\<exists>a. 0 < M a \<and> f a = b)"
  10.880 +proof-
  10.881 +  have f: "finite {a. f a = b \<and> 0 < M a}" using assms unfolding multiset_def by auto
  10.882 +  show ?thesis unfolding mmap_def setsum_gt_0_iff[OF f] by auto
  10.883 +qed
  10.884 +
  10.885 +lemma finite_twosets:
  10.886 +assumes "finite B1" and "finite B2"
  10.887 +shows "finite {u b1 b2 |b1 b2. b1 \<in> B1 \<and> b2 \<in> B2}"  (is "finite ?A")
  10.888 +proof-
  10.889 +  have A: "?A = (\<lambda> b1b2. u (fst b1b2) (snd b1b2)) ` (B1 <*> B2)" by force
  10.890 +  show ?thesis unfolding A using finite_cartesian_product[OF assms] by auto
  10.891 +qed
  10.892 +
  10.893 +lemma wp_mmap:
  10.894 +fixes A :: "'a set" and B1 :: "'b1 set" and B2 :: "'b2 set"
  10.895 +assumes wp: "wpull A B1 B2 f1 f2 p1 p2"
  10.896 +shows
  10.897 +"wpull {M. M \<in> multiset \<and> supp M \<subseteq> A}
  10.898 +       {N1. N1 \<in> multiset \<and> supp N1 \<subseteq> B1} {N2. N2 \<in> multiset \<and> supp N2 \<subseteq> B2}
  10.899 +       (mmap f1) (mmap f2) (mmap p1) (mmap p2)"
  10.900 +unfolding wpull_def proof (safe, unfold Bex_def mem_Collect_eq)
  10.901 +  fix N1 :: "'b1 \<Rightarrow> nat" and N2 :: "'b2 \<Rightarrow> nat"
  10.902 +  assume mmap': "mmap f1 N1 = mmap f2 N2"
  10.903 +  and N1[simp]: "N1 \<in> multiset" "supp N1 \<subseteq> B1"
  10.904 +  and N2[simp]: "N2 \<in> multiset" "supp N2 \<subseteq> B2"
  10.905 +  have mN1[simp]: "mmap f1 N1 \<in> multiset" using N1 by (auto simp: mmap)
  10.906 +  have mN2[simp]: "mmap f2 N2 \<in> multiset" using N2 by (auto simp: mmap)
  10.907 +  def P \<equiv> "mmap f1 N1"
  10.908 +  have P1: "P = mmap f1 N1" and P2: "P = mmap f2 N2" unfolding P_def using mmap' by auto
  10.909 +  note P = P1 P2
  10.910 +  have P_mult[simp]: "P \<in> multiset" unfolding P_def using N1 by auto
  10.911 +  have fin_N1[simp]: "finite (supp N1)" using N1(1) unfolding multiset_def by auto
  10.912 +  have fin_N2[simp]: "finite (supp N2)" using N2(1) unfolding multiset_def by auto
  10.913 +  have fin_P[simp]: "finite (supp P)" using P_mult unfolding multiset_def by auto
  10.914 +  (*  *)
  10.915 +  def set1 \<equiv> "\<lambda> c. {b1 \<in> supp N1. f1 b1 = c}"
  10.916 +  have set1[simp]: "\<And> c b1. b1 \<in> set1 c \<Longrightarrow> f1 b1 = c" unfolding set1_def by auto
  10.917 +  have fin_set1: "\<And> c. c \<in> supp P \<Longrightarrow> finite (set1 c)"
  10.918 +  using N1(1) unfolding set1_def multiset_def by auto
  10.919 +  have set1_NE: "\<And> c. c \<in> supp P \<Longrightarrow> set1 c \<noteq> {}"
  10.920 +  unfolding set1_def P1 mmap_ge_0[OF N1(1)] by auto
  10.921 +  have supp_N1_set1: "supp N1 = (\<Union> c \<in> supp P. set1 c)"
  10.922 +  using supp_vimage_mmap[OF N1(1), of f1] unfolding set1_def P1 by auto
  10.923 +  hence set1_inclN1: "\<And>c. c \<in> supp P \<Longrightarrow> set1 c \<subseteq> supp N1" by auto
  10.924 +  hence set1_incl: "\<And> c. c \<in> supp P \<Longrightarrow> set1 c \<subseteq> B1" using N1(2) by blast
  10.925 +  have set1_disj: "\<And> c c'. c \<noteq> c' \<Longrightarrow> set1 c \<inter> set1 c' = {}"
  10.926 +  unfolding set1_def by auto
  10.927 +  have setsum_set1: "\<And> c. setsum N1 (set1 c) = P c"
  10.928 +  unfolding P1 set1_def mmap_def apply(rule setsum_cong) by auto
  10.929 +  (*  *)
  10.930 +  def set2 \<equiv> "\<lambda> c. {b2 \<in> supp N2. f2 b2 = c}"
  10.931 +  have set2[simp]: "\<And> c b2. b2 \<in> set2 c \<Longrightarrow> f2 b2 = c" unfolding set2_def by auto
  10.932 +  have fin_set2: "\<And> c. c \<in> supp P \<Longrightarrow> finite (set2 c)"
  10.933 +  using N2(1) unfolding set2_def multiset_def by auto
  10.934 +  have set2_NE: "\<And> c. c \<in> supp P \<Longrightarrow> set2 c \<noteq> {}"
  10.935 +  unfolding set2_def P2 mmap_ge_0[OF N2(1)] by auto
  10.936 +  have supp_N2_set2: "supp N2 = (\<Union> c \<in> supp P. set2 c)"
  10.937 +  using supp_vimage_mmap[OF N2(1), of f2] unfolding set2_def P2 by auto
  10.938 +  hence set2_inclN2: "\<And>c. c \<in> supp P \<Longrightarrow> set2 c \<subseteq> supp N2" by auto
  10.939 +  hence set2_incl: "\<And> c. c \<in> supp P \<Longrightarrow> set2 c \<subseteq> B2" using N2(2) by blast
  10.940 +  have set2_disj: "\<And> c c'. c \<noteq> c' \<Longrightarrow> set2 c \<inter> set2 c' = {}"
  10.941 +  unfolding set2_def by auto
  10.942 +  have setsum_set2: "\<And> c. setsum N2 (set2 c) = P c"
  10.943 +  unfolding P2 set2_def mmap_def apply(rule setsum_cong) by auto
  10.944 +  (*  *)
  10.945 +  have ss: "\<And> c. c \<in> supp P \<Longrightarrow> setsum N1 (set1 c) = setsum N2 (set2 c)"
  10.946 +  unfolding setsum_set1 setsum_set2 ..
  10.947 +  have "\<forall> c \<in> supp P. \<forall> b1b2 \<in> (set1 c) \<times> (set2 c).
  10.948 +          \<exists> a \<in> A. p1 a = fst b1b2 \<and> p2 a = snd b1b2"
  10.949 +  using wp set1_incl set2_incl unfolding wpull_def Ball_def mem_Collect_eq
  10.950 +  by simp (metis set1 set2 set_rev_mp)
  10.951 +  then obtain uu where uu:
  10.952 +  "\<forall> c \<in> supp P. \<forall> b1b2 \<in> (set1 c) \<times> (set2 c).
  10.953 +     uu c b1b2 \<in> A \<and> p1 (uu c b1b2) = fst b1b2 \<and> p2 (uu c b1b2) = snd b1b2" by metis
  10.954 +  def u \<equiv> "\<lambda> c b1 b2. uu c (b1,b2)"
  10.955 +  have u[simp]:
  10.956 +  "\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk> \<Longrightarrow> u c b1 b2 \<in> A"
  10.957 +  "\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk> \<Longrightarrow> p1 (u c b1 b2) = b1"
  10.958 +  "\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk> \<Longrightarrow> p2 (u c b1 b2) = b2"
  10.959 +  using uu unfolding u_def by auto
  10.960 +  {fix c assume c: "c \<in> supp P"
  10.961 +   have "inj2 (u c) (set1 c) (set2 c)" unfolding inj2_def proof clarify
  10.962 +     fix b1 b1' b2 b2'
  10.963 +     assume "{b1, b1'} \<subseteq> set1 c" "{b2, b2'} \<subseteq> set2 c" and 0: "u c b1 b2 = u c b1' b2'"
  10.964 +     hence "p1 (u c b1 b2) = b1 \<and> p2 (u c b1 b2) = b2 \<and>
  10.965 +            p1 (u c b1' b2') = b1' \<and> p2 (u c b1' b2') = b2'"
  10.966 +     using u(2)[OF c] u(3)[OF c] by simp metis
  10.967 +     thus "b1 = b1' \<and> b2 = b2'" using 0 by auto
  10.968 +   qed
  10.969 +  } note inj = this
  10.970 +  def sset \<equiv> "\<lambda> c. {u c b1 b2 | b1 b2. b1 \<in> set1 c \<and> b2 \<in> set2 c}"
  10.971 +  have fin_sset[simp]: "\<And> c. c \<in> supp P \<Longrightarrow> finite (sset c)" unfolding sset_def
  10.972 +  using fin_set1 fin_set2 finite_twosets by blast
  10.973 +  have sset_A: "\<And> c. c \<in> supp P \<Longrightarrow> sset c \<subseteq> A" unfolding sset_def by auto
  10.974 +  {fix c a assume c: "c \<in> supp P" and ac: "a \<in> sset c"
  10.975 +   then obtain b1 b2 where b1: "b1 \<in> set1 c" and b2: "b2 \<in> set2 c"
  10.976 +   and a: "a = u c b1 b2" unfolding sset_def by auto
  10.977 +   have "p1 a \<in> set1 c" and p2a: "p2 a \<in> set2 c"
  10.978 +   using ac a b1 b2 c u(2) u(3) by simp+
  10.979 +   hence "u c (p1 a) (p2 a) = a" unfolding a using b1 b2 inj[OF c]
  10.980 +   unfolding inj2_def by (metis c u(2) u(3))
  10.981 +  } note u_p12[simp] = this
  10.982 +  {fix c a assume c: "c \<in> supp P" and ac: "a \<in> sset c"
  10.983 +   hence "p1 a \<in> set1 c" unfolding sset_def by auto
  10.984 +  }note p1[simp] = this
  10.985 +  {fix c a assume c: "c \<in> supp P" and ac: "a \<in> sset c"
  10.986 +   hence "p2 a \<in> set2 c" unfolding sset_def by auto
  10.987 +  }note p2[simp] = this
  10.988 +  (*  *)
  10.989 +  {fix c assume c: "c \<in> supp P"
  10.990 +   hence "\<exists> M. (\<forall> b1 \<in> set1 c. setsum (\<lambda> b2. M (u c b1 b2)) (set2 c) = N1 b1) \<and>
  10.991 +               (\<forall> b2 \<in> set2 c. setsum (\<lambda> b1. M (u c b1 b2)) (set1 c) = N2 b2)"
  10.992 +   unfolding sset_def
  10.993 +   using matrix_count_finite[OF set1_NE[OF c] fin_set1[OF c]
  10.994 +                                set2_NE[OF c] fin_set2[OF c] inj[OF c] ss[OF c]] by auto
  10.995 +  }
  10.996 +  then obtain Ms where
  10.997 +  ss1: "\<And> c b1. \<lbrakk>c \<in> supp P; b1 \<in> set1 c\<rbrakk> \<Longrightarrow>
  10.998 +                   setsum (\<lambda> b2. Ms c (u c b1 b2)) (set2 c) = N1 b1" and
  10.999 +  ss2: "\<And> c b2. \<lbrakk>c \<in> supp P; b2 \<in> set2 c\<rbrakk> \<Longrightarrow>
 10.1000 +                   setsum (\<lambda> b1. Ms c (u c b1 b2)) (set1 c) = N2 b2"
 10.1001 +  by metis
 10.1002 +  def SET \<equiv> "\<Union> c \<in> supp P. sset c"
 10.1003 +  have fin_SET[simp]: "finite SET" unfolding SET_def apply(rule finite_UN_I) by auto
 10.1004 +  have SET_A: "SET \<subseteq> A" unfolding SET_def using sset_A by auto
 10.1005 +  have u_SET[simp]: "\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk> \<Longrightarrow> u c b1 b2 \<in> SET"
 10.1006 +  unfolding SET_def sset_def by blast
 10.1007 +  {fix c a assume c: "c \<in> supp P" and a: "a \<in> SET" and p1a: "p1 a \<in> set1 c"
 10.1008 +   then obtain c' where c': "c' \<in> supp P" and ac': "a \<in> sset c'"
 10.1009 +   unfolding SET_def by auto
 10.1010 +   hence "p1 a \<in> set1 c'" unfolding sset_def by auto
 10.1011 +   hence eq: "c = c'" using p1a c c' set1_disj by auto
 10.1012 +   hence "a \<in> sset c" using ac' by simp
 10.1013 +  } note p1_rev = this
 10.1014 +  {fix c a assume c: "c \<in> supp P" and a: "a \<in> SET" and p2a: "p2 a \<in> set2 c"
 10.1015 +   then obtain c' where c': "c' \<in> supp P" and ac': "a \<in> sset c'"
 10.1016 +   unfolding SET_def by auto
 10.1017 +   hence "p2 a \<in> set2 c'" unfolding sset_def by auto
 10.1018 +   hence eq: "c = c'" using p2a c c' set2_disj by auto
 10.1019 +   hence "a \<in> sset c" using ac' by simp
 10.1020 +  } note p2_rev = this
 10.1021 +  (*  *)
 10.1022 +  have "\<forall> a \<in> SET. \<exists> c \<in> supp P. a \<in> sset c" unfolding SET_def by auto
 10.1023 +  then obtain h where h: "\<forall> a \<in> SET. h a \<in> supp P \<and> a \<in> sset (h a)" by metis
 10.1024 +  have h_u[simp]: "\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk>
 10.1025 +                      \<Longrightarrow> h (u c b1 b2) = c"
 10.1026 +  by (metis h p2 set2 u(3) u_SET)
 10.1027 +  have h_u1: "\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk>
 10.1028 +                      \<Longrightarrow> h (u c b1 b2) = f1 b1"
 10.1029 +  using h unfolding sset_def by auto
 10.1030 +  have h_u2: "\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk>
 10.1031 +                      \<Longrightarrow> h (u c b1 b2) = f2 b2"
 10.1032 +  using h unfolding sset_def by auto
 10.1033 +  def M \<equiv> "\<lambda> a. if a \<in> SET \<and> p1 a \<in> supp N1 \<and> p2 a \<in> supp N2 then Ms (h a) a else 0"
 10.1034 +  have sM: "supp M \<subseteq> SET" "supp M \<subseteq> p1 -` (supp N1)" "supp M \<subseteq> p2 -` (supp N2)"
 10.1035 +  unfolding M_def by auto
 10.1036 +  show "\<exists>M. (M \<in> multiset \<and> supp M \<subseteq> A) \<and> mmap p1 M = N1 \<and> mmap p2 M = N2"
 10.1037 +  proof(rule exI[of _ M], safe)
 10.1038 +    show "M \<in> multiset"
 10.1039 +    unfolding multiset_def using finite_subset[OF sM(1) fin_SET] by simp
 10.1040 +  next
 10.1041 +    fix a assume "0 < M a"
 10.1042 +    thus "a \<in> A" unfolding M_def using SET_A by (cases "a \<in> SET") auto
 10.1043 +  next
 10.1044 +    show "mmap p1 M = N1"
 10.1045 +    unfolding mmap_def[abs_def] proof(rule ext)
 10.1046 +      fix b1
 10.1047 +      let ?K = "{a. p1 a = b1 \<and> 0 < M a}"
 10.1048 +      show "setsum M ?K = N1 b1"
 10.1049 +      proof(cases "b1 \<in> supp N1")
 10.1050 +        case False
 10.1051 +        hence "?K = {}" using sM(2) by auto
 10.1052 +        thus ?thesis using False by auto
 10.1053 +      next
 10.1054 +        case True
 10.1055 +        def c \<equiv> "f1 b1"
 10.1056 +        have c: "c \<in> supp P" and b1: "b1 \<in> set1 c"
 10.1057 +        unfolding set1_def c_def P1 using True by (auto simp: mmap_image)
 10.1058 +        have "setsum M ?K = setsum M {a. p1 a = b1 \<and> a \<in> SET}"
 10.1059 +        apply(rule setsum_mono_zero_cong_left) unfolding M_def by auto
 10.1060 +        also have "... = setsum M ((\<lambda> b2. u c b1 b2) ` (set2 c))"
 10.1061 +        apply(rule setsum_cong) using c b1 proof safe
 10.1062 +          fix a assume p1a: "p1 a \<in> set1 c" and "0 < P c" and "a \<in> SET"
 10.1063 +          hence ac: "a \<in> sset c" using p1_rev by auto
 10.1064 +          hence "a = u c (p1 a) (p2 a)" using c by auto
 10.1065 +          moreover have "p2 a \<in> set2 c" using ac c by auto
 10.1066 +          ultimately show "a \<in> u c (p1 a) ` set2 c" by auto
 10.1067 +        next
 10.1068 +          fix b2 assume b1: "b1 \<in> set1 c" and b2: "b2 \<in> set2 c"
 10.1069 +          hence "u c b1 b2 \<in> SET" using c by auto
 10.1070 +        qed auto
 10.1071 +        also have "... = setsum (\<lambda> b2. M (u c b1 b2)) (set2 c)"
 10.1072 +        unfolding comp_def[symmetric] apply(rule setsum_reindex)
 10.1073 +        using inj unfolding inj_on_def inj2_def using b1 c u(3) by blast
 10.1074 +        also have "... = N1 b1" unfolding ss1[OF c b1, symmetric]
 10.1075 +          apply(rule setsum_cong[OF refl]) unfolding M_def
 10.1076 +          using True h_u[OF c b1] set2_def u(2,3)[OF c b1] u_SET[OF c b1] by fastforce
 10.1077 +        finally show ?thesis .
 10.1078 +      qed
 10.1079 +    qed
 10.1080 +  next
 10.1081 +    show "mmap p2 M = N2"
 10.1082 +    unfolding mmap_def[abs_def] proof(rule ext)
 10.1083 +      fix b2
 10.1084 +      let ?K = "{a. p2 a = b2 \<and> 0 < M a}"
 10.1085 +      show "setsum M ?K = N2 b2"
 10.1086 +      proof(cases "b2 \<in> supp N2")
 10.1087 +        case False
 10.1088 +        hence "?K = {}" using sM(3) by auto
 10.1089 +        thus ?thesis using False by auto
 10.1090 +      next
 10.1091 +        case True
 10.1092 +        def c \<equiv> "f2 b2"
 10.1093 +        have c: "c \<in> supp P" and b2: "b2 \<in> set2 c"
 10.1094 +        unfolding set2_def c_def P2 using True by (auto simp: mmap_image)
 10.1095 +        have "setsum M ?K = setsum M {a. p2 a = b2 \<and> a \<in> SET}"
 10.1096 +        apply(rule setsum_mono_zero_cong_left) unfolding M_def by auto
 10.1097 +        also have "... = setsum M ((\<lambda> b1. u c b1 b2) ` (set1 c))"
 10.1098 +        apply(rule setsum_cong) using c b2 proof safe
 10.1099 +          fix a assume p2a: "p2 a \<in> set2 c" and "0 < P c" and "a \<in> SET"
 10.1100 +          hence ac: "a \<in> sset c" using p2_rev by auto
 10.1101 +          hence "a = u c (p1 a) (p2 a)" using c by auto
 10.1102 +          moreover have "p1 a \<in> set1 c" using ac c by auto
 10.1103 +          ultimately show "a \<in> (\<lambda>b1. u c b1 (p2 a)) ` set1 c" by auto
 10.1104 +        next
 10.1105 +          fix b2 assume b1: "b1 \<in> set1 c" and b2: "b2 \<in> set2 c"
 10.1106 +          hence "u c b1 b2 \<in> SET" using c by auto
 10.1107 +        qed auto
 10.1108 +        also have "... = setsum (M o (\<lambda> b1. u c b1 b2)) (set1 c)"
 10.1109 +        apply(rule setsum_reindex)
 10.1110 +        using inj unfolding inj_on_def inj2_def using b2 c u(2) by blast
 10.1111 +        also have "... = setsum (\<lambda> b1. M (u c b1 b2)) (set1 c)"
 10.1112 +        unfolding comp_def[symmetric] by simp
 10.1113 +        also have "... = N2 b2" unfolding ss2[OF c b2, symmetric]
 10.1114 +          apply(rule setsum_cong[OF refl]) unfolding M_def set2_def
 10.1115 +          using True h_u1[OF c _ b2] u(2,3)[OF c _ b2] u_SET[OF c _ b2]
 10.1116 +          unfolding set1_def by fastforce
 10.1117 +        finally show ?thesis .
 10.1118 +      qed
 10.1119 +    qed
 10.1120 +  qed
 10.1121 +qed
 10.1122 +
 10.1123 +definition mset_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
 10.1124 +"mset_map h = Abs_multiset \<circ> mmap h \<circ> count"
 10.1125 +
 10.1126 +bnf_def mset = mset_map [set_of] "\<lambda>_::'a multiset. natLeq" ["{#}"]
 10.1127 +unfolding mset_map_def
 10.1128 +proof -
 10.1129 +  show "Abs_multiset \<circ> mmap id \<circ> count = id" unfolding mmap_id by (auto simp: count_inverse)
 10.1130 +next
 10.1131 +  fix f g
 10.1132 +  show "Abs_multiset \<circ> mmap (g \<circ> f) \<circ> count =
 10.1133 +        Abs_multiset \<circ> mmap g \<circ> count \<circ> (Abs_multiset \<circ> mmap f \<circ> count)"
 10.1134 +  unfolding comp_def apply(rule ext)
 10.1135 +  by (auto simp: Abs_multiset_inverse count mmap_comp1 mmap)
 10.1136 +next
 10.1137 +  fix M f g assume eq: "\<And>a. a \<in> set_of M \<Longrightarrow> f a = g a"
 10.1138 +  thus "(Abs_multiset \<circ> mmap f \<circ> count) M = (Abs_multiset \<circ> mmap g \<circ> count) M" apply auto
 10.1139 +  unfolding cIm_def[abs_def] image_def
 10.1140 +  by (auto intro!: mmap_cong simp: Abs_multiset_inject count mmap)
 10.1141 +next
 10.1142 +  fix f show "set_of \<circ> (Abs_multiset \<circ> mmap f \<circ> count) = op ` f \<circ> set_of"
 10.1143 +  by (auto simp: count mmap mmap_image set_of_Abs_multiset supp_count)
 10.1144 +next
 10.1145 +  show "card_order natLeq" by (rule natLeq_card_order)
 10.1146 +next
 10.1147 +  show "cinfinite natLeq" by (rule natLeq_cinfinite)
 10.1148 +next
 10.1149 +  fix M show "|set_of M| \<le>o natLeq"
 10.1150 +  apply(rule ordLess_imp_ordLeq)
 10.1151 +  unfolding finite_iff_ordLess_natLeq[symmetric] using finite_set_of .
 10.1152 +next
 10.1153 +  fix A :: "'a set"
 10.1154 +  have "|{M. set_of M \<subseteq> A}| \<le>o |{as. set as \<subseteq> A}|" using card_of_set_of .
 10.1155 +  also have "|{as. set as \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq"
 10.1156 +  by (rule list_in_bd)
 10.1157 +  finally show "|{M. set_of M \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" .
 10.1158 +next
 10.1159 +  fix A B1 B2 f1 f2 p1 p2
 10.1160 +  let ?map = "\<lambda> f. Abs_multiset \<circ> mmap f \<circ> count"
 10.1161 +  assume wp: "wpull A B1 B2 f1 f2 p1 p2"
 10.1162 +  show "wpull {x. set_of x \<subseteq> A} {x. set_of x \<subseteq> B1} {x. set_of x \<subseteq> B2}
 10.1163 +              (?map f1) (?map f2) (?map p1) (?map p2)"
 10.1164 +  unfolding wpull_def proof safe
 10.1165 +    fix y1 y2
 10.1166 +    assume y1: "set_of y1 \<subseteq> B1" and y2: "set_of y2 \<subseteq> B2"
 10.1167 +    and m: "?map f1 y1 = ?map f2 y2"
 10.1168 +    def N1 \<equiv> "count y1"  def N2 \<equiv> "count y2"
 10.1169 +    have "N1 \<in> multiset \<and> supp N1 \<subseteq> B1" and "N2 \<in> multiset \<and> supp N2 \<subseteq> B2"
 10.1170 +    and "mmap f1 N1 = mmap f2 N2"
 10.1171 +    using y1 y2 m unfolding N1_def N2_def
 10.1172 +    by (auto simp: Abs_multiset_inject count mmap)
 10.1173 +    then obtain M where M: "M \<in> multiset \<and> supp M \<subseteq> A"
 10.1174 +    and N1: "mmap p1 M = N1" and N2: "mmap p2 M = N2"
 10.1175 +    using wp_mmap[OF wp] unfolding wpull_def by auto
 10.1176 +    def x \<equiv> "Abs_multiset M"
 10.1177 +    show "\<exists>x\<in>{x. set_of x \<subseteq> A}. ?map p1 x = y1 \<and> ?map p2 x = y2"
 10.1178 +    apply(intro bexI[of _ x]) using M N1 N2 unfolding N1_def N2_def x_def
 10.1179 +    by (auto simp: count_inverse Abs_multiset_inverse)
 10.1180 +  qed
 10.1181 +qed (unfold set_of_empty, auto)
 10.1182 +
 10.1183 +end