split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
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