# HG changeset patch # User traytel # Date 1373983195 -7200 # Node ID c7cae5ce217d3614855ce3b9edc8817d101c01ed # Parent a3b04f0ab6a41b98c2b0014be38a069c61c7b9b1 use transfer/lifting for proving countable set and multisets being BNFs diff -r a3b04f0ab6a4 -r c7cae5ce217d src/HOL/BNF/Countable_Type.thy --- a/src/HOL/BNF/Countable_Type.thy Tue Jul 16 10:18:25 2013 +0200 +++ b/src/HOL/BNF/Countable_Type.thy Tue Jul 16 15:59:55 2013 +0200 @@ -8,7 +8,10 @@ header {* (At Most) Countable Sets *} theory Countable_Type -imports "../Cardinals/Cardinals" "~~/src/HOL/Library/Countable_Set" +imports + "~~/src/HOL/Cardinals/Cardinals" + "~~/src/HOL/Library/Countable_Set" + "~~/src/HOL/Library/Quotient_Set" begin subsection{* Cardinal stuff *} @@ -23,9 +26,12 @@ assumes "countable A" shows "(finite A \ |A| (infinite A \ |A| =o |UNIV::nat set| )" -apply (cases "finite A") - apply(metis finite_iff_cardOf_nat) - by (metis assms countable_card_of_nat infinite_iff_card_of_nat ordIso_iff_ordLeq) +proof (cases "finite A") + case True thus ?thesis by (metis finite_iff_cardOf_nat) +next + case False with assms show ?thesis + by (metis countable_card_of_nat infinite_iff_card_of_nat ordIso_iff_ordLeq) +qed lemma countable_cases_card_of[elim]: assumes "countable A" @@ -35,7 +41,7 @@ lemma countable_or: "countable A \ (\ f::'a\nat. finite A \ inj_on f A) \ (\ f::'a\nat. infinite A \ bij_betw f A UNIV)" - by (auto elim: countable_enum_cases) + by (elim countable_enum_cases) fastforce+ lemma countable_cases[elim]: assumes "countable A" @@ -55,48 +61,32 @@ subsection{* The type of countable sets *} -typedef 'a cset = "{A :: 'a set. countable A}" -apply(rule exI[of _ "{}"]) by simp +typedef 'a cset = "{A :: 'a set. countable A}" morphisms rcset acset + by (rule exI[of _ "{}"]) simp -abbreviation rcset where "rcset \ Rep_cset" -abbreviation acset where "acset \ Abs_cset" - -lemmas acset_rcset = Rep_cset_inverse -declare acset_rcset[simp] +setup_lifting type_definition_cset -lemma acset_surj: -"\ A. countable A \ acset A = C" -apply(cases rule: Abs_cset_cases[of C]) by auto - -lemma rcset_acset[simp]: -assumes "countable A" -shows "rcset (acset A) = A" -using Abs_cset_inverse assms by auto +declare + rcset_inverse[simp] + acset_inverse[Transfer.transferred, unfolded mem_Collect_eq, simp] + acset_inject[Transfer.transferred, unfolded mem_Collect_eq, simp] + rcset[Transfer.transferred, unfolded mem_Collect_eq, simp] -lemma acset_inj[simp]: -assumes "countable A" and "countable B" -shows "acset A = acset B \ A = B" -using assms Abs_cset_inject by auto - -lemma rcset[simp]: -"countable (rcset C)" -using Rep_cset by simp - -lemma rcset_surj: -assumes "countable A" -shows "\ C. rcset C = A" -apply(cases rule: Rep_cset_cases[of A]) -using assms by auto - -definition "cIn a C \ (a \ rcset C)" -definition "cEmp \ acset {}" -definition "cIns a C \ acset (insert a (rcset C))" -abbreviation cSingl where "cSingl a \ cIns a cEmp" -definition "cUn C D \ acset (rcset C \ rcset D)" -definition "cInt C D \ acset (rcset C \ rcset D)" -definition "cDif C D \ acset (rcset C - rcset D)" -definition "cIm f C \ acset (f ` rcset C)" -definition "cVim f D \ acset (f -` rcset D)" -(* TODO eventually: nice setup for these operations, copied from the set setup *) +lift_definition cin :: "'a \ 'a cset \ bool" is "op \" parametric member_transfer + .. +lift_definition cempty :: "'a cset" is "{}" parametric empty_transfer + by (rule countable_empty) +lift_definition cinsert :: "'a \ 'a cset \ 'a cset" is insert parametric insert_transfer + by (rule countable_insert) +lift_definition csingle :: "'a \ 'a cset" is "\x. {x}" + by (rule countable_insert[OF countable_empty]) +lift_definition cUn :: "'a cset \ 'a cset \ 'a cset" is "op \" parametric union_transfer + by (rule countable_Un) +lift_definition cInt :: "'a cset \ 'a cset \ 'a cset" is "op \" parametric inter_transfer + by (rule countable_Int1) +lift_definition cDiff :: "'a cset \ 'a cset \ 'a cset" is "op -" parametric Diff_transfer + by (rule countable_Diff) +lift_definition cimage :: "('a \ 'b) \ 'a cset \ 'b cset" is "op `" parametric image_transfer + by (rule countable_image) end diff -r a3b04f0ab6a4 -r c7cae5ce217d src/HOL/BNF/More_BNFs.thy --- a/src/HOL/BNF/More_BNFs.thy Tue Jul 16 10:18:25 2013 +0200 +++ b/src/HOL/BNF/More_BNFs.thy Tue Jul 16 15:59:55 2013 +0200 @@ -231,7 +231,7 @@ lemmas [simp] = fset.map_comp' fset.map_id' fset.set_map' lemma fset_rel_fset: "set_rel \ (fset A1) (fset A2) = fset_rel \ A1 A2" - unfolding fset_rel_def set_rel_def by auto + unfolding fset_rel_def set_rel_def by auto (* Countable sets *) @@ -263,16 +263,15 @@ by (erule finite_Collect_subsets) lemma rcset_to_rcset: "countable A \ rcset (the_inv rcset A) = A" -apply (rule f_the_inv_into_f) -unfolding inj_on_def Rep_cset_inject using rcset_surj by auto + apply (rule f_the_inv_into_f[unfolded inj_on_def image_iff]) + apply transfer' apply simp + apply transfer' apply simp + done lemma Collect_Int_Times: "{(x, y). R x y} \ A \ B = {(x, y). R x y \ x \ A \ y \ B}" by auto -lemma rcset_map': "rcset (cIm f x) = f ` rcset x" -unfolding cIm_def[abs_def] by simp - definition cset_rel :: "('a \ 'b \ bool) \ 'a cset \ 'b cset \ bool" where "cset_rel R a b \ (\t \ rcset a. \u \ rcset b. R t u) \ @@ -280,68 +279,55 @@ lemma cset_rel_aux: "(\t \ rcset a. \u \ rcset b. R t u) \ (\t \ rcset b. \u \ rcset a. R u t) \ - ((Grp {x. rcset x \ {(a, b). R a b}} (cIm fst))\\ OO - Grp {x. rcset x \ {(a, b). R a b}} (cIm snd)) a b" (is "?L = ?R") + ((Grp {x. rcset x \ {(a, b). R a b}} (cimage fst))\\ OO + Grp {x. rcset x \ {(a, b). R a b}} (cimage snd)) a b" (is "?L = ?R") proof assume ?L def R' \ "the_inv rcset (Collect (split R) \ (rcset a \ rcset b))" (is "the_inv rcset ?L'") - have "countable ?L'" by auto + have L: "countable ?L'" by auto hence *: "rcset R' = ?L'" unfolding R'_def using fset_to_fset by (intro rcset_to_rcset) - show ?R unfolding Grp_def relcompp.simps conversep.simps + thus ?R unfolding Grp_def relcompp.simps conversep.simps proof (intro CollectI prod_caseI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl) - have "rcset a = fst ` ({(x, y). R x y} \ rcset a \ rcset b)" (is "_ = ?A") - using conjunct1[OF `?L`] unfolding image_def by (auto simp add: Collect_Int_Times) - hence "a = acset ?A" by (metis acset_rcset) - thus "a = cIm fst R'" unfolding cIm_def * by auto - have "rcset b = snd ` ({(x, y). R x y} \ rcset a \ rcset b)" (is "_ = ?B") - using conjunct2[OF `?L`] unfolding image_def by (auto simp add: Collect_Int_Times) - hence "b = acset ?B" by (metis acset_rcset) - thus "b = cIm snd R'" unfolding cIm_def * by auto - qed (auto simp add: *) + from * `?L` show "a = cimage fst R'" by transfer (auto simp: image_def Collect_Int_Times) + next + from * `?L` show "b = cimage snd R'" by transfer (auto simp: image_def Collect_Int_Times) + qed simp_all next assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps - apply (simp add: subset_eq Ball_def) - apply (rule conjI) - apply (clarsimp, metis (lifting, no_types) rcset_map' image_iff surjective_pairing) - apply (clarsimp) - by (metis Domain.intros Range.simps rcset_map' fst_eq_Domain snd_eq_Range) + by transfer force qed -bnf cIm [rcset] "\_::'a cset. natLeq" ["cEmp"] cset_rel +bnf cimage [rcset] "\_::'a cset. natLeq" ["cempty"] cset_rel proof - - show "cIm id = id" unfolding cIm_def[abs_def] id_def by auto + show "cimage id = id" by transfer' simp next - fix f g show "cIm (g \ f) = cIm g \ cIm f" - unfolding cIm_def[abs_def] apply(rule ext) unfolding comp_def by auto + fix f g show "cimage (g \ f) = cimage g \ cimage f" by transfer' fastforce next fix C f g assume eq: "\a. a \ rcset C \ f a = g a" - thus "cIm f C = cIm g C" - unfolding cIm_def[abs_def] unfolding image_def by auto + thus "cimage f C = cimage g C" by transfer force next - fix f show "rcset \ cIm f = op ` f \ rcset" unfolding cIm_def[abs_def] by auto + fix f show "rcset \ cimage f = op ` f \ rcset" by transfer' fastforce next show "card_order natLeq" by (rule natLeq_card_order) next show "cinfinite natLeq" by (rule natLeq_cinfinite) next - fix C show "|rcset C| \o natLeq" using rcset unfolding countable_card_le_natLeq . + fix C show "|rcset C| \o natLeq" by transfer (unfold countable_card_le_natLeq) next fix A B1 B2 f1 f2 p1 p2 assume wp: "wpull A B1 B2 f1 f2 p1 p2" show "wpull {x. rcset x \ A} {x. rcset x \ B1} {x. rcset x \ B2} - (cIm f1) (cIm f2) (cIm p1) (cIm p2)" + (cimage f1) (cimage f2) (cimage p1) (cimage p2)" unfolding wpull_def proof safe fix y1 y2 assume Y1: "rcset y1 \ B1" and Y2: "rcset y2 \ B2" - assume "cIm f1 y1 = cIm f2 y2" - hence EQ: "f1 ` (rcset y1) = f2 ` (rcset y2)" - unfolding cIm_def by auto + assume "cimage f1 y1 = cimage f2 y2" + hence EQ: "f1 ` (rcset y1) = f2 ` (rcset y2)" by transfer with Y1 Y2 obtain X where X: "X \ A" and Y1: "p1 ` X = rcset y1" and Y2: "p2 ` X = rcset y2" - using wpull_image[OF wp] unfolding wpull_def Pow_def - unfolding Bex_def mem_Collect_eq apply - - apply(erule allE[of _ "rcset y1"], erule allE[of _ "rcset y2"]) by auto + using wpull_image[OF wp] unfolding wpull_def Pow_def Bex_def mem_Collect_eq + by (auto elim!: allE[of _ "rcset y1"] allE[of _ "rcset y2"]) have "\ y1' \ rcset y1. \ x. x \ X \ y1' = p1 x" using Y1 by auto then obtain q1 where q1: "\ y1' \ rcset y1. q1 y1' \ X \ y1' = p1 (q1 y1')" by metis have "\ y2' \ rcset y2. \ x. x \ X \ y2' = p2 x" using Y2 by auto @@ -350,16 +336,17 @@ have X': "X' \ A" and Y1: "p1 ` X' = rcset y1" and Y2: "p2 ` X' = rcset y2" using X Y1 Y2 q1 q2 unfolding X'_def by fast+ have fX': "countable X'" unfolding X'_def by simp - then obtain x where X'eq: "X' = rcset x" by (metis rcset_acset) - show "\x\{x. rcset x \ A}. cIm p1 x = y1 \ cIm p2 x = y2" - apply(intro bexI[of _ "x"]) using X' Y1 Y2 unfolding X'eq cIm_def by auto + then obtain x where X'eq: "X' = rcset x" by transfer blast + show "\x\{x. rcset x \ A}. cimage p1 x = y1 \ cimage p2 x = y2" + using X' Y1 Y2 unfolding X'eq by (intro bexI[of _ "x"]) (transfer, auto) qed next fix R show "cset_rel R = - (Grp {x. rcset x \ Collect (split R)} (cIm fst))\\ OO Grp {x. rcset x \ Collect (split R)} (cIm snd)" + (Grp {x. rcset x \ Collect (split R)} (cimage fst))\\ OO + Grp {x. rcset x \ Collect (split R)} (cimage snd)" unfolding cset_rel_def[abs_def] cset_rel_aux by simp -qed (unfold cEmp_def, auto) +qed (transfer, simp) (* Multisets *) @@ -375,108 +362,76 @@ finally show ?thesis . qed -(* *) -definition mmap :: "('a \ 'b) \ ('a \ nat) \ 'b \ nat" where -"mmap h f b = setsum f {a. h a = b \ f a > 0}" - -lemma mmap_id: "mmap id = id" -proof (rule ext)+ - fix f a show "mmap id f a = id f a" - proof(cases "f a = 0") - case False - hence 1: "{aa. aa = a \ 0 < f aa} = {a}" by auto - show ?thesis by (simp add: mmap_def id_apply 1) - qed(unfold mmap_def, auto) -qed - -lemma inj_on_setsum_inv: -assumes f: "f \ multiset" -and 1: "(0::nat) < setsum f {a. h a = b' \ 0 < f a}" (is "0 < setsum f ?A'") -and 2: "{a. h a = b \ 0 < f a} = {a. h a = b' \ 0 < f a}" (is "?A = ?A'") -shows "b = b'" -proof- - have "finite ?A'" using f unfolding multiset_def by auto - hence "?A' \ {}" using 1 by (auto simp add: setsum_gt_0_iff) - thus ?thesis using 2 by auto -qed - -lemma mmap_comp: -fixes h1 :: "'a \ 'b" and h2 :: "'b \ 'c" -assumes f: "f \ multiset" -shows "mmap (h2 o h1) f = (mmap h2 o mmap h1) f" -unfolding mmap_def[abs_def] comp_def proof(rule ext)+ - fix c :: 'c - let ?A = "{a. h2 (h1 a) = c \ 0 < f a}" - let ?As = "\ b. {a. h1 a = b \ 0 < f a}" - let ?B = "{b. h2 b = c \ 0 < setsum f (?As b)}" - have 0: "{?As b | b. b \ ?B} = ?As ` ?B" by auto - have "\ b. finite (?As b)" using f unfolding multiset_def by simp - hence "?B = {b. h2 b = c \ ?As b \ {}}" by (auto simp add: setsum_gt_0_iff) - hence A: "?A = \ {?As b | b. b \ ?B}" by auto - have "setsum f ?A = setsum (setsum f) {?As b | b. b \ ?B}" - unfolding A apply(rule setsum_Union_disjoint) - using f unfolding multiset_def by auto - also have "... = setsum (setsum f) (?As ` ?B)" unfolding 0 .. - also have "... = setsum (setsum f o ?As) ?B" apply(rule setsum_reindex) - unfolding inj_on_def apply auto using inj_on_setsum_inv[OF f, of h1] by blast - also have "... = setsum (\ b. setsum f (?As b)) ?B" unfolding comp_def .. - finally show "setsum f ?A = setsum (\ b. setsum f (?As b)) ?B" . -qed - -lemma mmap_comp1: -fixes h1 :: "'a \ 'b" and h2 :: "'b \ 'c" -assumes "f \ multiset" -shows "mmap (\ a. h2 (h1 a)) f = mmap h2 (mmap h1 f)" -using mmap_comp[OF assms] unfolding comp_def by auto - -lemma mmap: -assumes "f \ multiset" -shows "mmap h f \ multiset" -using assms unfolding mmap_def[abs_def] multiset_def proof safe +lift_definition mmap :: "('a \ 'b) \ 'a multiset \ 'b multiset" is + "\h f b. setsum f {a. h a = b \ f a > 0} :: nat" +unfolding multiset_def proof safe + fix h :: "'a \ 'b" and f :: "'a \ nat" assume fin: "finite {a. 0 < f a}" (is "finite ?A") show "finite {b. 0 < setsum f {a. h a = b \ 0 < f a}}" (is "finite {b. 0 < setsum f (?As b)}") proof- let ?B = "{b. 0 < setsum f (?As b)}" - have "\ b. finite (?As b)" using assms unfolding multiset_def by simp + have "\ b. finite (?As b)" using fin by simp hence B: "?B = {b. ?As b \ {}}" by (auto simp add: setsum_gt_0_iff) hence "?B \ h ` ?A" by auto thus ?thesis using finite_surj[OF fin] by auto qed qed -lemma mmap_cong: -assumes "\a. a \# M \ f a = g a" -shows "mmap f (count M) = mmap g (count M)" -using assms unfolding mmap_def[abs_def] by (intro ext, intro setsum_cong) auto - -abbreviation supp where "supp f \ {a. f a > 0}" - -lemma mmap_image_comp: -assumes f: "f \ multiset" -shows "(supp o mmap h) f = (image h o supp) f" -unfolding mmap_def[abs_def] comp_def proof- - have "\ b. finite {a. h a = b \ 0 < f a}" (is "\ b. finite (?As b)") - using f unfolding multiset_def by auto - thus "{b. 0 < setsum f (?As b)} = h ` {a. 0 < f a}" - by (auto simp add: setsum_gt_0_iff) +lemma mmap_id: "mmap id = id" +proof (intro ext multiset_eqI) + fix f a show "count (mmap id f) a = count (id f) a" + proof (cases "count f a = 0") + case False + hence 1: "{aa. aa = a \ aa \# f} = {a}" by auto + thus ?thesis by transfer auto + qed (transfer, simp) qed -lemma mmap_image: -assumes f: "f \ multiset" -shows "supp (mmap h f) = h ` (supp f)" -using mmap_image_comp[OF assms] unfolding comp_def . +lemma inj_on_setsum_inv: +assumes 1: "(0::nat) < setsum (count f) {a. h a = b' \ a \# f}" (is "0 < setsum (count f) ?A'") +and 2: "{a. h a = b \ a \# f} = {a. h a = b' \ a \# f}" (is "?A = ?A'") +shows "b = b'" +using assms by (auto simp add: setsum_gt_0_iff) -lemma set_of_Abs_multiset: -assumes f: "f \ multiset" -shows "set_of (Abs_multiset f) = supp f" -using assms unfolding set_of_def by (auto simp: Abs_multiset_inverse) +lemma mmap_comp: +fixes h1 :: "'a \ 'b" and h2 :: "'b \ 'c" +shows "mmap (h2 o h1) = mmap h2 o mmap h1" +proof (intro ext multiset_eqI) + fix f :: "'a multiset" fix c :: 'c + let ?A = "{a. h2 (h1 a) = c \ a \# f}" + let ?As = "\ b. {a. h1 a = b \ a \# f}" + let ?B = "{b. h2 b = c \ 0 < setsum (count f) (?As b)}" + have 0: "{?As b | b. b \ ?B} = ?As ` ?B" by auto + have "\ b. finite (?As b)" by transfer (simp add: multiset_def) + hence "?B = {b. h2 b = c \ ?As b \ {}}" by (auto simp add: setsum_gt_0_iff) + hence A: "?A = \ {?As b | b. b \ ?B}" by auto + have "setsum (count f) ?A = setsum (setsum (count f)) {?As b | b. b \ ?B}" + unfolding A by transfer (intro setsum_Union_disjoint, auto simp: multiset_def) + also have "... = setsum (setsum (count f)) (?As ` ?B)" unfolding 0 .. + also have "... = setsum (setsum (count f) o ?As) ?B" + by(intro setsum_reindex) (auto simp add: setsum_gt_0_iff inj_on_def) + also have "... = setsum (\ b. setsum (count f) (?As b)) ?B" unfolding comp_def .. + finally have "setsum (count f) ?A = setsum (\ b. setsum (count f) (?As b)) ?B" . + thus "count (mmap (h2 \ h1) f) c = count ((mmap h2 \ mmap h1) f) c" + by transfer (unfold o_apply, blast) +qed -lemma supp_count: -"supp (count M) = set_of M" -using assms unfolding set_of_def by auto +lemma mmap_cong: +assumes "\a. a \# M \ f a = g a" +shows "mmap f M = mmap g M" +using assms by transfer (auto intro!: setsum_cong) + +lemma set_of_transfer[transfer_rule]: "(pcr_multiset op = ===> op =) (\f. {a. 0 < f a}) set_of" + unfolding set_of_def pcr_multiset_def cr_multiset_def fun_rel_def by auto + +lemma set_of_mmap: "set_of o mmap h = image h o set_of" +proof (rule ext, unfold o_apply) + fix M show "set_of (mmap h M) = h ` set_of M" + by transfer (auto simp add: multiset_def setsum_gt_0_iff) +qed lemma multiset_of_surj: -"multiset_of ` {as. set as \ A} = {M. set_of M \ A}" + "multiset_of ` {as. set as \ A} = {M. set_of M \ A}" proof safe fix M assume M: "set_of M \ A" obtain as where eq: "M = multiset_of as" using surj_multiset_of unfolding surj_def by auto @@ -666,18 +621,11 @@ qed qed -lemma supp_vimage_mmap: -assumes "M \ multiset" -shows "supp M \ f -` (supp (mmap f M))" -using assms by (auto simp: mmap_image) +lemma supp_vimage_mmap: "set_of M \ f -` (set_of (mmap f M))" + by transfer (auto simp: multiset_def setsum_gt_0_iff) -lemma mmap_ge_0: -assumes "M \ multiset" -shows "0 < mmap f M b \ (\a. 0 < M a \ f a = b)" -proof- - have f: "finite {a. f a = b \ 0 < M a}" using assms unfolding multiset_def by auto - show ?thesis unfolding mmap_def setsum_gt_0_iff[OF f] by auto -qed +lemma mmap_ge_0: "b \# mmap f M \ (\a. a \# M \ f a = b)" + by transfer (auto simp: multiset_def setsum_gt_0_iff) lemma finite_twosets: assumes "finite B1" and "finite B2" @@ -687,74 +635,71 @@ show ?thesis unfolding A using finite_cartesian_product[OF assms] by auto qed -lemma wp_mmap: +lemma wpull_mmap: fixes A :: "'a set" and B1 :: "'b1 set" and B2 :: "'b2 set" assumes wp: "wpull A B1 B2 f1 f2 p1 p2" shows -"wpull {M. M \ multiset \ supp M \ A} - {N1. N1 \ multiset \ supp N1 \ B1} {N2. N2 \ multiset \ supp N2 \ B2} +"wpull {M. set_of M \ A} + {N1. set_of N1 \ B1} {N2. set_of N2 \ B2} (mmap f1) (mmap f2) (mmap p1) (mmap p2)" unfolding wpull_def proof (safe, unfold Bex_def mem_Collect_eq) - fix N1 :: "'b1 \ nat" and N2 :: "'b2 \ nat" + fix N1 :: "'b1 multiset" and N2 :: "'b2 multiset" assume mmap': "mmap f1 N1 = mmap f2 N2" - and N1[simp]: "N1 \ multiset" "supp N1 \ B1" - and N2[simp]: "N2 \ multiset" "supp N2 \ B2" - have mN1[simp]: "mmap f1 N1 \ multiset" using N1 by (auto simp: mmap) - have mN2[simp]: "mmap f2 N2 \ multiset" using N2 by (auto simp: mmap) + and N1[simp]: "set_of N1 \ B1" + and N2[simp]: "set_of N2 \ B2" def P \ "mmap f1 N1" have P1: "P = mmap f1 N1" and P2: "P = mmap f2 N2" unfolding P_def using mmap' by auto note P = P1 P2 - have P_mult[simp]: "P \ multiset" unfolding P_def using N1 by auto - have fin_N1[simp]: "finite (supp N1)" using N1(1) unfolding multiset_def by auto - have fin_N2[simp]: "finite (supp N2)" using N2(1) unfolding multiset_def by auto - have fin_P[simp]: "finite (supp P)" using P_mult unfolding multiset_def by auto + have fin_N1[simp]: "finite (set_of N1)" + and fin_N2[simp]: "finite (set_of N2)" + and fin_P[simp]: "finite (set_of P)" by auto (* *) - def set1 \ "\ c. {b1 \ supp N1. f1 b1 = c}" + def set1 \ "\ c. {b1 \ set_of N1. f1 b1 = c}" have set1[simp]: "\ c b1. b1 \ set1 c \ f1 b1 = c" unfolding set1_def by auto - have fin_set1: "\ c. c \ supp P \ finite (set1 c)" - using N1(1) unfolding set1_def multiset_def by auto - have set1_NE: "\ c. c \ supp P \ set1 c \ {}" - unfolding set1_def P1 mmap_ge_0[OF N1(1)] by auto - have supp_N1_set1: "supp N1 = (\ c \ supp P. set1 c)" - using supp_vimage_mmap[OF N1(1), of f1] unfolding set1_def P1 by auto - hence set1_inclN1: "\c. c \ supp P \ set1 c \ supp N1" by auto - hence set1_incl: "\ c. c \ supp P \ set1 c \ B1" using N1(2) by blast + have fin_set1: "\ c. c \ set_of P \ finite (set1 c)" + using N1(1) unfolding set1_def multiset_def by auto + have set1_NE: "\ c. c \ set_of P \ set1 c \ {}" + unfolding set1_def set_of_def P mmap_ge_0 by auto + have supp_N1_set1: "set_of N1 = (\ c \ set_of P. set1 c)" + using supp_vimage_mmap[of N1 f1] unfolding set1_def P1 by auto + hence set1_inclN1: "\c. c \ set_of P \ set1 c \ set_of N1" by auto + hence set1_incl: "\ c. c \ set_of P \ set1 c \ B1" using N1 by blast have set1_disj: "\ c c'. c \ c' \ set1 c \ set1 c' = {}" - unfolding set1_def by auto - have setsum_set1: "\ c. setsum N1 (set1 c) = P c" - unfolding P1 set1_def mmap_def apply(rule setsum_cong) by auto + unfolding set1_def by auto + have setsum_set1: "\ c. setsum (count N1) (set1 c) = count P c" + unfolding P1 set1_def by transfer (auto intro: setsum_cong) (* *) - def set2 \ "\ c. {b2 \ supp N2. f2 b2 = c}" + def set2 \ "\ c. {b2 \ set_of N2. f2 b2 = c}" have set2[simp]: "\ c b2. b2 \ set2 c \ f2 b2 = c" unfolding set2_def by auto - have fin_set2: "\ c. c \ supp P \ finite (set2 c)" + have fin_set2: "\ c. c \ set_of P \ finite (set2 c)" using N2(1) unfolding set2_def multiset_def by auto - have set2_NE: "\ c. c \ supp P \ set2 c \ {}" - unfolding set2_def P2 mmap_ge_0[OF N2(1)] by auto - have supp_N2_set2: "supp N2 = (\ c \ supp P. set2 c)" - using supp_vimage_mmap[OF N2(1), of f2] unfolding set2_def P2 by auto - hence set2_inclN2: "\c. c \ supp P \ set2 c \ supp N2" by auto - hence set2_incl: "\ c. c \ supp P \ set2 c \ B2" using N2(2) by blast + have set2_NE: "\ c. c \ set_of P \ set2 c \ {}" + unfolding set2_def P2 mmap_ge_0 set_of_def by auto + have supp_N2_set2: "set_of N2 = (\ c \ set_of P. set2 c)" + using supp_vimage_mmap[of N2 f2] unfolding set2_def P2 by auto + hence set2_inclN2: "\c. c \ set_of P \ set2 c \ set_of N2" by auto + hence set2_incl: "\ c. c \ set_of P \ set2 c \ B2" using N2 by blast have set2_disj: "\ c c'. c \ c' \ set2 c \ set2 c' = {}" - unfolding set2_def by auto - have setsum_set2: "\ c. setsum N2 (set2 c) = P c" - unfolding P2 set2_def mmap_def apply(rule setsum_cong) by auto + unfolding set2_def by auto + have setsum_set2: "\ c. setsum (count N2) (set2 c) = count P c" + unfolding P2 set2_def by transfer (auto intro: setsum_cong) (* *) - have ss: "\ c. c \ supp P \ setsum N1 (set1 c) = setsum N2 (set2 c)" - unfolding setsum_set1 setsum_set2 .. - have "\ c \ supp P. \ b1b2 \ (set1 c) \ (set2 c). + have ss: "\ c. c \ set_of P \ setsum (count N1) (set1 c) = setsum (count N2) (set2 c)" + unfolding setsum_set1 setsum_set2 .. + have "\ c \ set_of P. \ b1b2 \ (set1 c) \ (set2 c). \ a \ A. p1 a = fst b1b2 \ p2 a = snd b1b2" - using wp set1_incl set2_incl unfolding wpull_def Ball_def mem_Collect_eq - by simp (metis set1 set2 set_rev_mp) + using wp set1_incl set2_incl unfolding wpull_def Ball_def mem_Collect_eq + by simp (metis set1 set2 set_rev_mp) then obtain uu where uu: - "\ c \ supp P. \ b1b2 \ (set1 c) \ (set2 c). + "\ c \ set_of P. \ b1b2 \ (set1 c) \ (set2 c). uu c b1b2 \