# HG changeset patch # User blanchet # Date 1390238696 -3600 # Node ID b3d0a02a756de5bd69d0727bb44824d3beecb4ba # Parent 2b0b6f69b148f3ca104e79de29392105f67bce38 dissolved BNF session diff -r 2b0b6f69b148 -r b3d0a02a756d src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Mon Jan 20 18:24:56 2014 +0100 +++ b/src/Doc/Datatypes/Datatypes.thy Mon Jan 20 18:24:56 2014 +0100 @@ -10,8 +10,8 @@ theory Datatypes imports Setup - "~~/src/HOL/BNF/BNF_Decl" - "~~/src/HOL/BNF/More_BNFs" + "~~/src/HOL/Library/BNF_Decl" + "~~/src/HOL/Library/More_BNFs" "~~/src/HOL/Library/Simps_Case_Conv" begin @@ -80,7 +80,7 @@ The package is part of @{theory Main}. Additional functionality is provided by the theories @{theory BNF_Decl} and @{theory More_BNFs}, located in the -@{text "~~/src/HOL/BNF"} directory. +directory \verb|~~/src/HOL/Library|. The package, like its predecessor, fully adheres to the LCF philosophy \cite{mgordon79}: The characteristic theorems associated with the specified @@ -1023,7 +1023,7 @@ text {* Primitive recursion is illustrated through concrete examples based on the datatypes defined in Section~\ref{ssec:datatype-introductory-examples}. More -examples can be found in the directory \verb|~~/src/HOL/BNF/Examples|. +examples can be found in the directory \verb|~~/src/HOL/BNF_Examples|. *} @@ -1715,7 +1715,7 @@ \keyw{prim\-corec\-ursive} commands, which support primitive corecursion, or using the more general \keyw{partial\_function} command. Here, the focus is on the first two. More examples can be found in the directory -\verb|~~/src/HOL/BNF/Examples|. +\verb|~~/src/HOL/BNF_Examples|. Whereas recursive functions consume datatypes one constructor at a time, corecursive functions construct codatatypes one constructor at a time. @@ -1759,7 +1759,7 @@ text {* Primitive corecursion is illustrated through concrete examples based on the codatatypes defined in Section~\ref{ssec:codatatype-introductory-examples}. More -examples can be found in the directory \verb|~~/src/HOL/BNF/Examples|. The code +examples can be found in the directory \verb|~~/src/HOL/BNF_Examples|. The code view is favored in the examples below. Sections \ref{ssec:primrec-constructor-view} and \ref{ssec:primrec-destructor-view} present the same examples expressed using the constructor and destructor views. @@ -2297,8 +2297,8 @@ \label{ssec:bnf-introductory-example} *} text {* -More examples in \verb|~~/src/HOL/BNF/Basic_BNFs.thy| and -\verb|~~/src/HOL/BNF/More_BNFs.thy|. +More examples in \verb|~~/src/HOL/Basic_BNFs.thy| and +\verb|~~/src/HOL/Library/More_BNFs.thy|. %Mention distinction between live and dead type arguments; % * and existence of map, set for those diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/BNF/BNF.thy --- a/src/HOL/BNF/BNF.thy Mon Jan 20 18:24:56 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,16 +0,0 @@ -(* Title: HOL/BNF/BNF.thy - Author: Dmitriy Traytel, TU Muenchen - Author: Andrei Popescu, TU Muenchen - Author: Jasmin Blanchette, TU Muenchen - Copyright 2012 - -Bounded natural functors for (co)datatypes. -*) - -header {* Bounded Natural Functors for (Co)datatypes *} - -theory BNF -imports More_BNFs Countable_Set_Type BNF_Decl -begin - -end diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/BNF/BNF_Decl.thy --- a/src/HOL/BNF/BNF_Decl.thy Mon Jan 20 18:24:56 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,18 +0,0 @@ -(* Title: HOL/BNF/BNF_Decl.thy - Author: Dmitriy Traytel, TU Muenchen - Copyright 2013 - -Axiomatic declaration of bounded natural functors. -*) - -header {* Axiomatic declaration of Bounded Natural Functors *} - -theory BNF_Decl -imports BNF_Def -keywords - "bnf_decl" :: thy_decl -begin - -ML_file "Tools/bnf_decl.ML" - -end diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/BNF/Countable_Set_Type.thy --- a/src/HOL/BNF/Countable_Set_Type.thy Mon Jan 20 18:24:56 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,188 +0,0 @@ -(* Title: HOL/BNF/Countable_Set_Type.thy - Author: Andrei Popescu, TU Muenchen - Copyright 2012 - -Type of (at most) countable sets. -*) - -header {* Type of (at Most) Countable Sets *} - -theory Countable_Set_Type -imports - "~~/src/HOL/Cardinals/Cardinal_Notations" - "~~/src/HOL/Library/Countable_Set" -begin - -abbreviation "Grp \ BNF_Util.Grp" - - -subsection{* Cardinal stuff *} - -lemma countable_card_of_nat: "countable A \ |A| \o |UNIV::nat set|" - unfolding countable_def card_of_ordLeq[symmetric] by auto - -lemma countable_card_le_natLeq: "countable A \ |A| \o natLeq" - unfolding countable_card_of_nat using card_of_nat ordLeq_ordIso_trans ordIso_symmetric by blast - -lemma countable_or_card_of: -assumes "countable A" -shows "(finite A \ |A| - (infinite A \ |A| =o |UNIV::nat set| )" -by (metis assms countable_card_of_nat infinite_iff_card_of_nat ordIso_iff_ordLeq - ordLeq_iff_ordLess_or_ordIso) - -lemma countable_cases_card_of[elim]: - assumes "countable A" - obtains (Fin) "finite A" "|A| (\ f::'a\nat. finite A \ inj_on f A) \ (\ f::'a\nat. infinite A \ bij_betw f A UNIV)" - by (elim countable_enum_cases) fastforce+ - -lemma countable_cases[elim]: - assumes "countable A" - obtains (Fin) f :: "'a\nat" where "finite A" "inj_on f A" - | (Inf) f :: "'a\nat" where "infinite A" "bij_betw f A UNIV" - using assms countable_or by metis - -lemma countable_ordLeq: -assumes "|A| \o |B|" and "countable B" -shows "countable A" -using assms unfolding countable_card_of_nat by(rule ordLeq_transitive) - -lemma countable_ordLess: -assumes AB: "|A| '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 Lifting_Set.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) - -subsection {* Registration as BNF *} - -lemma card_of_countable_sets_range: -fixes A :: "'a set" -shows "|{X. X \ A \ countable X \ X \ {}}| \o |{f::nat \ 'a. range f \ A}|" -apply(rule card_of_ordLeqI[of from_nat_into]) using inj_on_from_nat_into -unfolding inj_on_def by auto - -lemma card_of_countable_sets_Func: -"|{X. X \ A \ countable X \ X \ {}}| \o |A| ^c natLeq" -using card_of_countable_sets_range card_of_Func_UNIV[THEN ordIso_symmetric] -unfolding cexp_def Field_natLeq Field_card_of -by (rule ordLeq_ordIso_trans) - -lemma ordLeq_countable_subsets: -"|A| \o |{X. X \ A \ countable X}|" -apply (rule card_of_ordLeqI[of "\ a. {a}"]) unfolding inj_on_def by auto - -lemma finite_countable_subset: -"finite {X. X \ A \ countable X} \ finite A" -apply default - apply (erule contrapos_pp) - apply (rule card_of_ordLeq_infinite) - apply (rule ordLeq_countable_subsets) - apply assumption -apply (rule finite_Collect_conjI) -apply (rule disjI1) -by (erule finite_Collect_subsets) - -lemma rcset_to_rcset: "countable A \ rcset (the_inv rcset A) = A" - apply (rule f_the_inv_into_f[unfolded inj_on_def image_iff]) - apply transfer' apply simp - apply transfer' apply simp - done - -lemma Collect_Int_Times: -"{(x, y). R x y} \ A \ B = {(x, y). R x y \ x \ A \ y \ B}" -by auto - -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) \ - (\t \ rcset b. \u \ rcset a. R u t)" - -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}} (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 L: "countable ?L'" by auto - hence *: "rcset R' = ?L'" unfolding R'_def by (intro rcset_to_rcset) - thus ?R unfolding Grp_def relcompp.simps conversep.simps - proof (intro CollectI prod_caseI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl) - from * `?L` show "a = cimage fst R'" by transfer (auto simp: image_def Collect_Int_Times) - next - from * `?L` show "b = cimage snd R'" by transfer (auto simp: image_def Collect_Int_Times) - qed simp_all -next - assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps - by transfer force -qed - -bnf "'a cset" - map: cimage - sets: rcset - bd: natLeq - wits: "cempty" - rel: cset_rel -proof - - show "cimage id = id" by transfer' simp -next - fix f g show "cimage (g \ f) = cimage g \ cimage f" by transfer' fastforce -next - fix C f g assume eq: "\a. a \ rcset C \ f a = g a" - thus "cimage f C = cimage g C" by transfer force -next - 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" by transfer (unfold countable_card_le_natLeq) -next - fix R S - show "cset_rel R OO cset_rel S \ cset_rel (R OO S)" - unfolding cset_rel_def[abs_def] by fast -next - fix R - show "cset_rel R = - (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 (transfer, simp) - -end diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/BNF/More_BNFs.thy --- a/src/HOL/BNF/More_BNFs.thy Mon Jan 20 18:24:56 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1053 +0,0 @@ -(* Title: HOL/BNF/More_BNFs.thy - Author: Dmitriy Traytel, TU Muenchen - Author: Andrei Popescu, TU Muenchen - Author: Andreas Lochbihler, Karlsruhe Institute of Technology - Author: Jasmin Blanchette, TU Muenchen - Copyright 2012 - -Registration of various types as bounded natural functors. -*) - -header {* Registration of Various Types as Bounded Natural Functors *} - -theory More_BNFs -imports - "~~/src/HOL/Cardinals/Cardinal_Notations" - "~~/src/HOL/Library/FSet" - "~~/src/HOL/Library/Multiset" -begin - -abbreviation "Grp \ BNF_Util.Grp" -abbreviation "fstOp \ BNF_Def.fstOp" -abbreviation "sndOp \ BNF_Def.sndOp" - -lemma option_rec_conv_option_case: "option_rec = option_case" -by (simp add: fun_eq_iff split: option.split) - -bnf "'a option" - map: Option.map - sets: Option.set - bd: natLeq - wits: None - rel: option_rel -proof - - show "Option.map id = id" by (simp add: fun_eq_iff Option.map_def split: option.split) -next - fix f g - show "Option.map (g \ f) = Option.map g \ Option.map f" - by (auto simp add: fun_eq_iff Option.map_def split: option.split) -next - fix f g x - assume "\z. z \ Option.set x \ f z = g z" - thus "Option.map f x = Option.map g x" - by (simp cong: Option.map_cong) -next - fix f - show "Option.set \ Option.map f = op ` f \ Option.set" - by fastforce -next - show "card_order natLeq" by (rule natLeq_card_order) -next - show "cinfinite natLeq" by (rule natLeq_cinfinite) -next - fix x - show "|Option.set x| \o natLeq" - by (cases x) (simp_all add: ordLess_imp_ordLeq finite_iff_ordLess_natLeq[symmetric]) -next - fix R S - show "option_rel R OO option_rel S \ option_rel (R OO S)" - by (auto simp: option_rel_def split: option.splits) -next - fix z - assume "z \ Option.set None" - thus False by simp -next - fix R - show "option_rel R = - (Grp {x. Option.set x \ Collect (split R)} (Option.map fst))\\ OO - Grp {x. Option.set x \ Collect (split R)} (Option.map snd)" - unfolding option_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff prod.cases - by (auto simp: trans[OF eq_commute option_map_is_None] trans[OF eq_commute option_map_eq_Some] - split: option.splits) -qed - -bnf "'a list" - map: map - sets: set - bd: natLeq - wits: Nil - rel: list_all2 -proof - - show "map id = id" by (rule List.map.id) -next - fix f g - show "map (g o f) = map g o map f" by (rule List.map.comp[symmetric]) -next - fix x f g - assume "\z. z \ set x \ f z = g z" - thus "map f x = map g x" by simp -next - fix f - show "set o map f = image f o set" by (rule ext, unfold comp_apply, rule set_map) -next - show "card_order natLeq" by (rule natLeq_card_order) -next - show "cinfinite natLeq" by (rule natLeq_cinfinite) -next - fix x - show "|set x| \o natLeq" - by (metis List.finite_set finite_iff_ordLess_natLeq ordLess_imp_ordLeq) -next - fix R S - show "list_all2 R OO list_all2 S \ list_all2 (R OO S)" - by (metis list_all2_OO order_refl) -next - fix R - show "list_all2 R = - (Grp {x. set x \ {(x, y). R x y}} (map fst))\\ OO - Grp {x. set x \ {(x, y). R x y}} (map snd)" - unfolding list_all2_def[abs_def] Grp_def fun_eq_iff relcompp.simps conversep.simps - by (force simp: zip_map_fst_snd) -qed simp_all - - -(* Finite sets *) - -context -includes fset.lifting -begin - -lemma fset_rel_alt: "fset_rel R a b \ (\t \ fset a. \u \ fset b. R t u) \ - (\t \ fset b. \u \ fset a. R u t)" - by transfer (simp add: set_rel_def) - -lemma fset_to_fset: "finite A \ fset (the_inv fset A) = A" - apply (rule f_the_inv_into_f[unfolded inj_on_def]) - apply (simp add: fset_inject) apply (rule range_eqI Abs_fset_inverse[symmetric] CollectI)+ - . - -lemma fset_rel_aux: -"(\t \ fset a. \u \ fset b. R t u) \ (\u \ fset b. \t \ fset a. R t u) \ - ((Grp {a. fset a \ {(a, b). R a b}} (fimage fst))\\ OO - Grp {a. fset a \ {(a, b). R a b}} (fimage snd)) a b" (is "?L = ?R") -proof - assume ?L - def R' \ "the_inv fset (Collect (split R) \ (fset a \ fset b))" (is "the_inv fset ?L'") - have "finite ?L'" by (intro finite_Int[OF disjI2] finite_cartesian_product) (transfer, simp)+ - hence *: "fset R' = ?L'" unfolding R'_def by (intro fset_to_fset) - show ?R unfolding Grp_def relcompp.simps conversep.simps - proof (intro CollectI prod_caseI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl) - from * show "a = fimage fst R'" using conjunct1[OF `?L`] - by (transfer, auto simp add: image_def Int_def split: prod.splits) - from * show "b = fimage snd R'" using conjunct2[OF `?L`] - by (transfer, auto simp add: image_def Int_def split: prod.splits) - qed (auto simp add: *) -next - assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps - apply (simp add: subset_eq Ball_def) - apply (rule conjI) - apply (transfer, clarsimp, metis snd_conv) - by (transfer, clarsimp, metis fst_conv) -qed - -bnf "'a fset" - map: fimage - sets: fset - bd: natLeq - wits: "{||}" - rel: fset_rel -apply - - apply transfer' apply simp - apply transfer' apply force - apply transfer apply force - apply transfer' apply force - apply (rule natLeq_card_order) - apply (rule natLeq_cinfinite) - apply transfer apply (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq) - apply (fastforce simp: fset_rel_alt) - apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff fset_rel_alt fset_rel_aux) -apply transfer apply simp -done - -lemma fset_rel_fset: "set_rel \ (fset A1) (fset A2) = fset_rel \ A1 A2" - by transfer (rule refl) - -end - -lemmas [simp] = fset.map_comp fset.map_id fset.set_map - - -(* Multisets *) - -lemma setsum_gt_0_iff: -fixes f :: "'a \ nat" assumes "finite A" -shows "setsum f A > 0 \ (\ a \ A. f a > 0)" -(is "?L \ ?R") -proof- - have "?L \ \ setsum f A = 0" by fast - also have "... \ (\ a \ A. f a \ 0)" using assms by simp - also have "... \ ?R" by simp - finally show ?thesis . -qed - -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 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_id0: "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 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 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 comp_apply, blast) -qed - -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) - -context -begin -interpretation lifting_syntax . - -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 - -end - -lemma set_of_mmap: "set_of o mmap h = image h o set_of" -proof (rule ext, unfold comp_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}" -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 - hence "set as \ A" using M by auto - thus "M \ multiset_of ` {as. set as \ A}" using eq by auto -next - show "\x xa xb. \set xa \ A; xb \ set_of (multiset_of xa)\ \ xb \ A" - by (erule set_mp) (unfold set_of_multiset_of) -qed - -lemma card_of_set_of: -"|{M. set_of M \ A}| \o |{as. set as \ A}|" -apply(rule card_of_ordLeqI2[of _ multiset_of]) using multiset_of_surj by auto - -lemma nat_sum_induct: -assumes "\n1 n2. (\ m1 m2. m1 + m2 < n1 + n2 \ phi m1 m2) \ phi n1 n2" -shows "phi (n1::nat) (n2::nat)" -proof- - let ?chi = "\ n1n2 :: nat * nat. phi (fst n1n2) (snd n1n2)" - have "?chi (n1,n2)" - apply(induct rule: measure_induct[of "\ n1n2. fst n1n2 + snd n1n2" ?chi]) - using assms by (metis fstI sndI) - thus ?thesis by simp -qed - -lemma matrix_count: -fixes ct1 ct2 :: "nat \ nat" -assumes "setsum ct1 {.. ct. (\ i1 \ n1. setsum (\ i2. ct i1 i2) {.. - (\ i2 \ n2. setsum (\ i1. ct i1 i2) {.. ct1 ct2 :: nat \ nat. - setsum ct1 {.. ?phi ct1 ct2 n1 n2" - proof(induct rule: nat_sum_induct[of -"\ n1 n2. \ ct1 ct2 :: nat \ nat. - setsum ct1 {.. ?phi ct1 ct2 n1 n2"], - clarify) - fix n1 n2 :: nat and ct1 ct2 :: "nat \ nat" - assume IH: "\ m1 m2. m1 + m2 < n1 + n2 \ - \ dt1 dt2 :: nat \ nat. - setsum dt1 {.. ?phi dt1 dt2 m1 m2" - and ss: "setsum ct1 {.. ct2 n2") - case True - def dt2 \ "\ i2. if i2 = n2 then ct2 i2 - ct1 n1 else ct2 i2" - have "setsum ct1 {.. i1. i1 \ m1 \ setsum (\ i2. dt i1 i2) {.. i2. i2 \ n2 \ setsum (\ i1. dt i1 i2) {.. "\ i1. if i1 = n1 then ct1 i1 - ct2 n2 else ct1 i1" - have "setsum dt1 {.. i1. i1 \ n1 \ setsum (\ i2. dt i1 i2) {.. i2. i2 \ m2 \ setsum (\ i1. dt i1 i2) {.. - \ b1 b1' b2 b2'. {b1,b1'} \ B1 \ {b2,b2'} \ B2 \ u b1 b2 = u b1' b2' - \ b1 = b1' \ b2 = b2'" - -lemma matrix_setsum_finite: -assumes B1: "B1 \ {}" "finite B1" and B2: "B2 \ {}" "finite B2" and u: "inj2 u B1 B2" -and ss: "setsum N1 B1 = setsum N2 B2" -shows "\ M :: 'a \ nat. - (\ b1 \ B1. setsum (\ b2. M (u b1 b2)) B2 = N1 b1) \ - (\ b2 \ B2. setsum (\ b1. M (u b1 b2)) B1 = N2 b2)" -proof- - obtain n1 where "card B1 = Suc n1" using B1 by (metis card_insert finite.simps) - then obtain e1 where e1: "bij_betw e1 {.. "inv_into {.. i1. i1 < Suc n1 \ f1 (e1 i1) = i1" - and e1f1[simp]: "\ b1. b1 \ B1 \ e1 (f1 b1) = b1" unfolding f1_def - apply (metis bij_betw_inv_into e1, metis bij_betw_inv_into_left e1 lessThan_iff) - by (metis e1_surj f_inv_into_f) - (* *) - obtain n2 where "card B2 = Suc n2" using B2 by (metis card_insert finite.simps) - then obtain e2 where e2: "bij_betw e2 {.. "inv_into {.. i2. i2 < Suc n2 \ f2 (e2 i2) = i2" - and e2f2[simp]: "\ b2. b2 \ B2 \ e2 (f2 b2) = b2" unfolding f2_def - apply (metis bij_betw_inv_into e2, metis bij_betw_inv_into_left e2 lessThan_iff) - by (metis e2_surj f_inv_into_f) - (* *) - let ?ct1 = "N1 o e1" let ?ct2 = "N2 o e2" - have ss: "setsum ?ct1 {.. i1. i1 \ n1 \ setsum (\ i2. ct i1 i2) {.. i2. i2 \ n2 \ setsum (\ i1. ct i1 i2) {.. "{u b1 b2 | b1 b2. b1 \ B1 \ b2 \ B2}" - have "\ a \ A. \ b1b2 \ B1 <*> B2. u (fst b1b2) (snd b1b2) = a" - unfolding A_def Ball_def mem_Collect_eq by auto - then obtain h1h2 where h12: - "\a. a \ A \ u (fst (h1h2 a)) (snd (h1h2 a)) = a \ h1h2 a \ B1 <*> B2" by metis - def h1 \ "fst o h1h2" def h2 \ "snd o h1h2" - have h12[simp]: "\a. a \ A \ u (h1 a) (h2 a) = a" - "\ a. a \ A \ h1 a \ B1" "\ a. a \ A \ h2 a \ B2" - using h12 unfolding h1_def h2_def by force+ - {fix b1 b2 assume b1: "b1 \ B1" and b2: "b2 \ B2" - hence inA: "u b1 b2 \ A" unfolding A_def by auto - hence "u b1 b2 = u (h1 (u b1 b2)) (h2 (u b1 b2))" by auto - moreover have "h1 (u b1 b2) \ B1" "h2 (u b1 b2) \ B2" using inA by auto - ultimately have "h1 (u b1 b2) = b1 \ h2 (u b1 b2) = b2" - using u b1 b2 unfolding inj2_def by fastforce - } - hence h1[simp]: "\ b1 b2. \b1 \ B1; b2 \ B2\ \ h1 (u b1 b2) = b1" and - h2[simp]: "\ b1 b2. \b1 \ B1; b2 \ B2\ \ h2 (u b1 b2) = b2" by auto - def M \ "\ a. ct (f1 (h1 a)) (f2 (h2 a))" - show ?thesis - apply(rule exI[of _ M]) proof safe - fix b1 assume b1: "b1 \ B1" - hence f1b1: "f1 b1 \ n1" using f1 unfolding bij_betw_def - by (metis image_eqI lessThan_iff less_Suc_eq_le) - have "(\b2\B2. M (u b1 b2)) = (\i2b2\B2. M (u b1 b2)) = N1 b1" . - next - fix b2 assume b2: "b2 \ B2" - hence f2b2: "f2 b2 \ n2" using f2 unfolding bij_betw_def - by (metis image_eqI lessThan_iff less_Suc_eq_le) - have "(\b1\B1. M (u b1 b2)) = (\i1b1\B1. M (u b1 b2)) = N2 b2" . - qed -qed - -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: "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" -shows "finite {u b1 b2 |b1 b2. b1 \ B1 \ b2 \ B2}" (is "finite ?A") -proof- - have A: "?A = (\ b1b2. u (fst b1b2) (snd b1b2)) ` (B1 <*> B2)" by force - show ?thesis unfolding A using finite_cartesian_product[OF assms] by auto -qed - -(* Weak pullbacks: *) -definition wpull where -"wpull A B1 B2 f1 f2 p1 p2 \ - (\ b1 b2. b1 \ B1 \ b2 \ B2 \ f1 b1 = f2 b2 \ (\ a \ A. p1 a = b1 \ p2 a = b2))" - -(* Weak pseudo-pullbacks *) -definition wppull where -"wppull A B1 B2 f1 f2 e1 e2 p1 p2 \ - (\ b1 b2. b1 \ B1 \ b2 \ B2 \ f1 b1 = f2 b2 \ - (\ a \ A. e1 (p1 a) = e1 b1 \ e2 (p2 a) = e2 b2))" - - -(* The pullback of sets *) -definition thePull where -"thePull B1 B2 f1 f2 = {(b1,b2). b1 \ B1 \ b2 \ B2 \ f1 b1 = f2 b2}" - -lemma wpull_thePull: -"wpull (thePull B1 B2 f1 f2) B1 B2 f1 f2 fst snd" -unfolding wpull_def thePull_def by auto - -lemma wppull_thePull: -assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2" -shows -"\ j. \ a' \ thePull B1 B2 f1 f2. - j a' \ A \ - e1 (p1 (j a')) = e1 (fst a') \ e2 (p2 (j a')) = e2 (snd a')" -(is "\ j. \ a' \ ?A'. ?phi a' (j a')") -proof(rule bchoice[of ?A' ?phi], default) - fix a' assume a': "a' \ ?A'" - hence "fst a' \ B1" unfolding thePull_def by auto - moreover - from a' have "snd a' \ B2" unfolding thePull_def by auto - moreover have "f1 (fst a') = f2 (snd a')" - using a' unfolding csquare_def thePull_def by auto - ultimately show "\ ja'. ?phi a' ja'" - using assms unfolding wppull_def by blast -qed - -lemma wpull_wppull: -assumes wp: "wpull A' B1 B2 f1 f2 p1' p2'" and -1: "\ a' \ A'. j a' \ A \ e1 (p1 (j a')) = e1 (p1' a') \ e2 (p2 (j a')) = e2 (p2' a')" -shows "wppull A B1 B2 f1 f2 e1 e2 p1 p2" -unfolding wppull_def proof safe - fix b1 b2 - assume b1: "b1 \ B1" and b2: "b2 \ B2" and f: "f1 b1 = f2 b2" - then obtain a' where a': "a' \ A'" and b1: "b1 = p1' a'" and b2: "b2 = p2' a'" - using wp unfolding wpull_def by blast - show "\a\A. e1 (p1 a) = e1 b1 \ e2 (p2 a) = e2 b2" - apply (rule bexI[of _ "j a'"]) unfolding b1 b2 using a' 1 by auto -qed - -lemma wppull_fstOp_sndOp: -shows "wppull (Collect (split (P OO Q))) (Collect (split P)) (Collect (split Q)) - snd fst fst snd (fstOp P Q) (sndOp P Q)" -using pick_middlep unfolding wppull_def fstOp_def sndOp_def relcompp.simps by auto - -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. 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 multiset" and N2 :: "'b2 multiset" - assume mmap': "mmap f1 N1 = mmap f2 N2" - 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 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 \ 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 \ 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 (count N1) (set1 c) = count P c" - unfolding P1 set1_def by transfer (auto intro: setsum_cong) - (* *) - 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 \ set_of P \ finite (set2 c)" - using N2(1) unfolding set2_def multiset_def by auto - 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 (count N2) (set2 c) = count P c" - unfolding P2 set2_def by transfer (auto intro: setsum_cong) - (* *) - 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) - then obtain uu where uu: - "\ c \ set_of P. \ b1b2 \ (set1 c) \ (set2 c). - uu c b1b2 \ A \ p1 (uu c b1b2) = fst b1b2 \ p2 (uu c b1b2) = snd b1b2" by metis - def u \ "\ c b1 b2. uu c (b1,b2)" - have u[simp]: - "\ c b1 b2. \c \ set_of P; b1 \ set1 c; b2 \ set2 c\ \ u c b1 b2 \ A" - "\ c b1 b2. \c \ set_of P; b1 \ set1 c; b2 \ set2 c\ \ p1 (u c b1 b2) = b1" - "\ c b1 b2. \c \ set_of P; b1 \ set1 c; b2 \ set2 c\ \ p2 (u c b1 b2) = b2" - using uu unfolding u_def by auto - {fix c assume c: "c \ set_of P" - have "inj2 (u c) (set1 c) (set2 c)" unfolding inj2_def proof clarify - fix b1 b1' b2 b2' - assume "{b1, b1'} \ set1 c" "{b2, b2'} \ set2 c" and 0: "u c b1 b2 = u c b1' b2'" - hence "p1 (u c b1 b2) = b1 \ p2 (u c b1 b2) = b2 \ - p1 (u c b1' b2') = b1' \ p2 (u c b1' b2') = b2'" - using u(2)[OF c] u(3)[OF c] by simp metis - thus "b1 = b1' \ b2 = b2'" using 0 by auto - qed - } note inj = this - def sset \ "\ c. {u c b1 b2 | b1 b2. b1 \ set1 c \ b2 \ set2 c}" - have fin_sset[simp]: "\ c. c \ set_of P \ finite (sset c)" unfolding sset_def - using fin_set1 fin_set2 finite_twosets by blast - have sset_A: "\ c. c \ set_of P \ sset c \ A" unfolding sset_def by auto - {fix c a assume c: "c \ set_of P" and ac: "a \ sset c" - then obtain b1 b2 where b1: "b1 \ set1 c" and b2: "b2 \ set2 c" - and a: "a = u c b1 b2" unfolding sset_def by auto - have "p1 a \ set1 c" and p2a: "p2 a \ set2 c" - using ac a b1 b2 c u(2) u(3) by simp+ - hence "u c (p1 a) (p2 a) = a" unfolding a using b1 b2 inj[OF c] - unfolding inj2_def by (metis c u(2) u(3)) - } note u_p12[simp] = this - {fix c a assume c: "c \ set_of P" and ac: "a \ sset c" - hence "p1 a \ set1 c" unfolding sset_def by auto - }note p1[simp] = this - {fix c a assume c: "c \ set_of P" and ac: "a \ sset c" - hence "p2 a \ set2 c" unfolding sset_def by auto - }note p2[simp] = this - (* *) - {fix c assume c: "c \ set_of P" - hence "\ M. (\ b1 \ set1 c. setsum (\ b2. M (u c b1 b2)) (set2 c) = count N1 b1) \ - (\ b2 \ set2 c. setsum (\ b1. M (u c b1 b2)) (set1 c) = count N2 b2)" - unfolding sset_def - using matrix_setsum_finite[OF set1_NE[OF c] fin_set1[OF c] - set2_NE[OF c] fin_set2[OF c] inj[OF c] ss[OF c]] by auto - } - then obtain Ms where - ss1: "\ c b1. \c \ set_of P; b1 \ set1 c\ \ - setsum (\ b2. Ms c (u c b1 b2)) (set2 c) = count N1 b1" and - ss2: "\ c b2. \c \ set_of P; b2 \ set2 c\ \ - setsum (\ b1. Ms c (u c b1 b2)) (set1 c) = count N2 b2" - by metis - def SET \ "\ c \ set_of P. sset c" - have fin_SET[simp]: "finite SET" unfolding SET_def apply(rule finite_UN_I) by auto - have SET_A: "SET \ A" unfolding SET_def using sset_A by blast - have u_SET[simp]: "\ c b1 b2. \c \ set_of P; b1 \ set1 c; b2 \ set2 c\ \ u c b1 b2 \ SET" - unfolding SET_def sset_def by blast - {fix c a assume c: "c \ set_of P" and a: "a \ SET" and p1a: "p1 a \ set1 c" - then obtain c' where c': "c' \ set_of P" and ac': "a \ sset c'" - unfolding SET_def by auto - hence "p1 a \ set1 c'" unfolding sset_def by auto - hence eq: "c = c'" using p1a c c' set1_disj by auto - hence "a \ sset c" using ac' by simp - } note p1_rev = this - {fix c a assume c: "c \ set_of P" and a: "a \ SET" and p2a: "p2 a \ set2 c" - then obtain c' where c': "c' \ set_of P" and ac': "a \ sset c'" - unfolding SET_def by auto - hence "p2 a \ set2 c'" unfolding sset_def by auto - hence eq: "c = c'" using p2a c c' set2_disj by auto - hence "a \ sset c" using ac' by simp - } note p2_rev = this - (* *) - have "\ a \ SET. \ c \ set_of P. a \ sset c" unfolding SET_def by auto - then obtain h where h: "\ a \ SET. h a \ set_of P \ a \ sset (h a)" by metis - have h_u[simp]: "\ c b1 b2. \c \ set_of P; b1 \ set1 c; b2 \ set2 c\ - \ h (u c b1 b2) = c" - by (metis h p2 set2 u(3) u_SET) - have h_u1: "\ c b1 b2. \c \ set_of P; b1 \ set1 c; b2 \ set2 c\ - \ h (u c b1 b2) = f1 b1" - using h unfolding sset_def by auto - have h_u2: "\ c b1 b2. \c \ set_of P; b1 \ set1 c; b2 \ set2 c\ - \ h (u c b1 b2) = f2 b2" - using h unfolding sset_def by auto - def M \ - "Abs_multiset (\ a. if a \ SET \ p1 a \ set_of N1 \ p2 a \ set_of N2 then Ms (h a) a else 0)" - have "(\ a. if a \ SET \ p1 a \ set_of N1 \ p2 a \ set_of N2 then Ms (h a) a else 0) \ multiset" - unfolding multiset_def by auto - hence [transfer_rule]: "pcr_multiset op = (\ a. if a \ SET \ p1 a \ set_of N1 \ p2 a \ set_of N2 then Ms (h a) a else 0) M" - unfolding M_def pcr_multiset_def cr_multiset_def by (auto simp: Abs_multiset_inverse) - have sM: "set_of M \ SET" "set_of M \ p1 -` (set_of N1)" "set_of M \ p2 -` set_of N2" - by (transfer, auto split: split_if_asm)+ - show "\M. set_of M \ A \ mmap p1 M = N1 \ mmap p2 M = N2" - proof(rule exI[of _ M], safe) - fix a assume *: "a \ set_of M" - from SET_A show "a \ A" - proof (cases "a \ SET") - case False thus ?thesis using * by transfer' auto - qed blast - next - show "mmap p1 M = N1" - proof(intro multiset_eqI) - fix b1 - let ?K = "{a. p1 a = b1 \ a \# M}" - have "setsum (count M) ?K = count N1 b1" - proof(cases "b1 \ set_of N1") - case False - hence "?K = {}" using sM(2) by auto - thus ?thesis using False by auto - next - case True - def c \ "f1 b1" - have c: "c \ set_of P" and b1: "b1 \ set1 c" - unfolding set1_def c_def P1 using True by (auto simp: comp_eq_dest[OF set_of_mmap]) - with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p1 a = b1 \ a \ SET}" - by transfer (force intro: setsum_mono_zero_cong_left split: split_if_asm) - also have "... = setsum (count M) ((\ b2. u c b1 b2) ` (set2 c))" - apply(rule setsum_cong) using c b1 proof safe - fix a assume p1a: "p1 a \ set1 c" and "c \ set_of P" and "a \ SET" - hence ac: "a \ sset c" using p1_rev by auto - hence "a = u c (p1 a) (p2 a)" using c by auto - moreover have "p2 a \ set2 c" using ac c by auto - ultimately show "a \ u c (p1 a) ` set2 c" by auto - qed auto - also have "... = setsum (\ b2. count M (u c b1 b2)) (set2 c)" - unfolding comp_def[symmetric] apply(rule setsum_reindex) - using inj unfolding inj_on_def inj2_def using b1 c u(3) by blast - also have "... = count N1 b1" unfolding ss1[OF c b1, symmetric] - apply(rule setsum_cong[OF refl]) apply (transfer fixing: Ms u c b1 set2) - using True h_u[OF c b1] set2_def u(2,3)[OF c b1] u_SET[OF c b1] by fastforce - finally show ?thesis . - qed - thus "count (mmap p1 M) b1 = count N1 b1" by transfer - qed - next -next - show "mmap p2 M = N2" - proof(intro multiset_eqI) - fix b2 - let ?K = "{a. p2 a = b2 \ a \# M}" - have "setsum (count M) ?K = count N2 b2" - proof(cases "b2 \ set_of N2") - case False - hence "?K = {}" using sM(3) by auto - thus ?thesis using False by auto - next - case True - def c \ "f2 b2" - have c: "c \ set_of P" and b2: "b2 \ set2 c" - unfolding set2_def c_def P2 using True by (auto simp: comp_eq_dest[OF set_of_mmap]) - with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p2 a = b2 \ a \ SET}" - by transfer (force intro: setsum_mono_zero_cong_left split: split_if_asm) - also have "... = setsum (count M) ((\ b1. u c b1 b2) ` (set1 c))" - apply(rule setsum_cong) using c b2 proof safe - fix a assume p2a: "p2 a \ set2 c" and "c \ set_of P" and "a \ SET" - hence ac: "a \ sset c" using p2_rev by auto - hence "a = u c (p1 a) (p2 a)" using c by auto - moreover have "p1 a \ set1 c" using ac c by auto - ultimately show "a \ (\x. u c x (p2 a)) ` set1 c" by auto - qed auto - also have "... = setsum (count M o (\ b1. u c b1 b2)) (set1 c)" - apply(rule setsum_reindex) - using inj unfolding inj_on_def inj2_def using b2 c u(2) by blast - also have "... = setsum (\ b1. count M (u c b1 b2)) (set1 c)" by simp - also have "... = count N2 b2" unfolding ss2[OF c b2, symmetric] comp_def - apply(rule setsum_cong[OF refl]) apply (transfer fixing: Ms u c b2 set1) - using True h_u1[OF c _ b2] u(2,3)[OF c _ b2] u_SET[OF c _ b2] set1_def by fastforce - finally show ?thesis . - qed - thus "count (mmap p2 M) b2 = count N2 b2" by transfer - qed - qed -qed - -lemma set_of_bd: "|set_of x| \o natLeq" - by transfer - (auto intro!: ordLess_imp_ordLeq simp: finite_iff_ordLess_natLeq[symmetric] multiset_def) - -lemma wppull_mmap: - assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2" - shows "wppull {M. set_of M \ A} {N1. set_of N1 \ B1} {N2. set_of N2 \ B2} - (mmap f1) (mmap f2) (mmap e1) (mmap e2) (mmap p1) (mmap p2)" -proof - - from assms obtain j where j: "\a'\thePull B1 B2 f1 f2. - j a' \ A \ e1 (p1 (j a')) = e1 (fst a') \ e2 (p2 (j a')) = e2 (snd a')" - by (blast dest: wppull_thePull) - then show ?thesis - by (intro wpull_wppull[OF wpull_mmap[OF wpull_thePull], of _ _ _ _ "mmap j"]) - (auto simp: comp_eq_dest_lhs[OF mmap_comp[symmetric]] comp_eq_dest[OF set_of_mmap] - intro!: mmap_cong simp del: mem_set_of_iff simp: mem_set_of_iff[symmetric]) -qed - -bnf "'a multiset" - map: mmap - sets: set_of - bd: natLeq - wits: "{#}" -by (auto simp add: mmap_id0 mmap_comp set_of_mmap natLeq_card_order natLeq_cinfinite set_of_bd - Grp_def relcompp.simps intro: mmap_cong) - (metis wppull_mmap[OF wppull_fstOp_sndOp, unfolded wppull_def - o_eq_dest_lhs[OF mmap_comp[symmetric]] fstOp_def sndOp_def comp_def, simplified]) - -inductive rel_multiset' where - Zero[intro]: "rel_multiset' R {#} {#}" -| Plus[intro]: "\R a b; rel_multiset' R M N\ \ rel_multiset' R (M + {#a#}) (N + {#b#})" - -lemma map_multiset_Zero_iff[simp]: "mmap f M = {#} \ M = {#}" -by (metis image_is_empty multiset.set_map set_of_eq_empty_iff) - -lemma map_multiset_Zero[simp]: "mmap f {#} = {#}" by simp - -lemma rel_multiset_Zero: "rel_multiset R {#} {#}" -unfolding rel_multiset_def Grp_def by auto - -declare multiset.count[simp] -declare Abs_multiset_inverse[simp] -declare multiset.count_inverse[simp] -declare union_preserves_multiset[simp] - - -lemma map_multiset_Plus[simp]: "mmap f (M1 + M2) = mmap f M1 + mmap f M2" -proof (intro multiset_eqI, transfer fixing: f) - fix x :: 'a and M1 M2 :: "'b \ nat" - assume "M1 \ multiset" "M2 \ multiset" - hence "setsum M1 {a. f a = x \ 0 < M1 a} = setsum M1 {a. f a = x \ 0 < M1 a + M2 a}" - "setsum M2 {a. f a = x \ 0 < M2 a} = setsum M2 {a. f a = x \ 0 < M1 a + M2 a}" - by (auto simp: multiset_def intro!: setsum_mono_zero_cong_left) - then show "(\a | f a = x \ 0 < M1 a + M2 a. M1 a + M2 a) = - setsum M1 {a. f a = x \ 0 < M1 a} + - setsum M2 {a. f a = x \ 0 < M2 a}" - by (auto simp: setsum.distrib[symmetric]) -qed - -lemma map_multiset_singl[simp]: "mmap f {#a#} = {#f a#}" - by transfer auto - -lemma rel_multiset_Plus: -assumes ab: "R a b" and MN: "rel_multiset R M N" -shows "rel_multiset R (M + {#a#}) (N + {#b#})" -proof- - {fix y assume "R a b" and "set_of y \ {(x, y). R x y}" - hence "\ya. mmap fst y + {#a#} = mmap fst ya \ - mmap snd y + {#b#} = mmap snd ya \ - set_of ya \ {(x, y). R x y}" - apply(intro exI[of _ "y + {#(a,b)#}"]) by auto - } - thus ?thesis - using assms - unfolding rel_multiset_def Grp_def by force -qed - -lemma rel_multiset'_imp_rel_multiset: -"rel_multiset' R M N \ rel_multiset R M N" -apply(induct rule: rel_multiset'.induct) -using rel_multiset_Zero rel_multiset_Plus by auto - -lemma mcard_mmap[simp]: "mcard (mmap f M) = mcard M" -proof - - def A \ "\ b. {a. f a = b \ a \# M}" - let ?B = "{b. 0 < setsum (count M) (A b)}" - have "{b. \a. f a = b \ a \# M} \ f ` {a. a \# M}" by auto - moreover have "finite (f ` {a. a \# M})" apply(rule finite_imageI) - using finite_Collect_mem . - ultimately have fin: "finite {b. \a. f a = b \ a \# M}" by(rule finite_subset) - have i: "inj_on A ?B" unfolding inj_on_def A_def apply clarsimp - by (metis (lifting, full_types) mem_Collect_eq neq0_conv setsum.neutral) - have 0: "\ b. 0 < setsum (count M) (A b) \ (\ a \ A b. count M a > 0)" - apply safe - apply (metis less_not_refl setsum_gt_0_iff setsum_infinite) - by (metis A_def finite_Collect_conjI finite_Collect_mem setsum_gt_0_iff) - hence AB: "A ` ?B = {A b | b. \ a \ A b. count M a > 0}" by auto - - have "setsum (\ x. setsum (count M) (A x)) ?B = setsum (setsum (count M) o A) ?B" - unfolding comp_def .. - also have "... = (\x\ A ` ?B. setsum (count M) x)" - unfolding setsum.reindex [OF i, symmetric] .. - also have "... = setsum (count M) (\x\A ` {b. 0 < setsum (count M) (A b)}. x)" - (is "_ = setsum (count M) ?J") - apply(rule setsum.UNION_disjoint[symmetric]) - using 0 fin unfolding A_def by auto - also have "?J = {a. a \# M}" unfolding AB unfolding A_def by auto - finally have "setsum (\ x. setsum (count M) (A x)) ?B = - setsum (count M) {a. a \# M}" . - then show ?thesis unfolding mcard_unfold_setsum A_def by transfer -qed - -lemma rel_multiset_mcard: -assumes "rel_multiset R M N" -shows "mcard M = mcard N" -using assms unfolding rel_multiset_def Grp_def by auto - -lemma multiset_induct2[case_names empty addL addR]: -assumes empty: "P {#} {#}" -and addL: "\M N a. P M N \ P (M + {#a#}) N" -and addR: "\M N a. P M N \ P M (N + {#a#})" -shows "P M N" -apply(induct N rule: multiset_induct) - apply(induct M rule: multiset_induct, rule empty, erule addL) - apply(induct M rule: multiset_induct, erule addR, erule addR) -done - -lemma multiset_induct2_mcard[consumes 1, case_names empty add]: -assumes c: "mcard M = mcard N" -and empty: "P {#} {#}" -and add: "\M N a b. P M N \ P (M + {#a#}) (N + {#b#})" -shows "P M N" -using c proof(induct M arbitrary: N rule: measure_induct_rule[of mcard]) - case (less M) show ?case - proof(cases "M = {#}") - case True hence "N = {#}" using less.prems by auto - thus ?thesis using True empty by auto - next - case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split) - have "N \ {#}" using False less.prems by auto - then obtain N1 b where N: "N = N1 + {#b#}" by (metis multi_nonempty_split) - have "mcard M1 = mcard N1" using less.prems unfolding M N by auto - thus ?thesis using M N less.hyps add by auto - qed -qed - -lemma msed_map_invL: -assumes "mmap f (M + {#a#}) = N" -shows "\ N1. N = N1 + {#f a#} \ mmap f M = N1" -proof- - have "f a \# N" - using assms multiset.set_map[of f "M + {#a#}"] by auto - then obtain N1 where N: "N = N1 + {#f a#}" using multi_member_split by metis - have "mmap f M = N1" using assms unfolding N by simp - thus ?thesis using N by blast -qed - -lemma msed_map_invR: -assumes "mmap f M = N + {#b#}" -shows "\ M1 a. M = M1 + {#a#} \ f a = b \ mmap f M1 = N" -proof- - obtain a where a: "a \# M" and fa: "f a = b" - using multiset.set_map[of f M] unfolding assms - by (metis image_iff mem_set_of_iff union_single_eq_member) - then obtain M1 where M: "M = M1 + {#a#}" using multi_member_split by metis - have "mmap f M1 = N" using assms unfolding M fa[symmetric] by simp - thus ?thesis using M fa by blast -qed - -lemma msed_rel_invL: -assumes "rel_multiset R (M + {#a#}) N" -shows "\ N1 b. N = N1 + {#b#} \ R a b \ rel_multiset R M N1" -proof- - obtain K where KM: "mmap fst K = M + {#a#}" - and KN: "mmap snd K = N" and sK: "set_of K \ {(a, b). R a b}" - using assms - unfolding rel_multiset_def Grp_def by auto - obtain K1 ab where K: "K = K1 + {#ab#}" and a: "fst ab = a" - and K1M: "mmap fst K1 = M" using msed_map_invR[OF KM] by auto - obtain N1 where N: "N = N1 + {#snd ab#}" and K1N1: "mmap snd K1 = N1" - using msed_map_invL[OF KN[unfolded K]] by auto - have Rab: "R a (snd ab)" using sK a unfolding K by auto - have "rel_multiset R M N1" using sK K1M K1N1 - unfolding K rel_multiset_def Grp_def by auto - thus ?thesis using N Rab by auto -qed - -lemma msed_rel_invR: -assumes "rel_multiset R M (N + {#b#})" -shows "\ M1 a. M = M1 + {#a#} \ R a b \ rel_multiset R M1 N" -proof- - obtain K where KN: "mmap snd K = N + {#b#}" - and KM: "mmap fst K = M" and sK: "set_of K \ {(a, b). R a b}" - using assms - unfolding rel_multiset_def Grp_def by auto - obtain K1 ab where K: "K = K1 + {#ab#}" and b: "snd ab = b" - and K1N: "mmap snd K1 = N" using msed_map_invR[OF KN] by auto - obtain M1 where M: "M = M1 + {#fst ab#}" and K1M1: "mmap fst K1 = M1" - using msed_map_invL[OF KM[unfolded K]] by auto - have Rab: "R (fst ab) b" using sK b unfolding K by auto - have "rel_multiset R M1 N" using sK K1N K1M1 - unfolding K rel_multiset_def Grp_def by auto - thus ?thesis using M Rab by auto -qed - -lemma rel_multiset_imp_rel_multiset': -assumes "rel_multiset R M N" -shows "rel_multiset' R M N" -using assms proof(induct M arbitrary: N rule: measure_induct_rule[of mcard]) - case (less M) - have c: "mcard M = mcard N" using rel_multiset_mcard[OF less.prems] . - show ?case - proof(cases "M = {#}") - case True hence "N = {#}" using c by simp - thus ?thesis using True rel_multiset'.Zero by auto - next - case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split) - obtain N1 b where N: "N = N1 + {#b#}" and R: "R a b" and ms: "rel_multiset R M1 N1" - using msed_rel_invL[OF less.prems[unfolded M]] by auto - have "rel_multiset' R M1 N1" using less.hyps[of M1 N1] ms unfolding M by simp - thus ?thesis using rel_multiset'.Plus[of R a b, OF R] unfolding M N by simp - qed -qed - -lemma rel_multiset_rel_multiset': -"rel_multiset R M N = rel_multiset' R M N" -using rel_multiset_imp_rel_multiset' rel_multiset'_imp_rel_multiset by auto - -(* The main end product for rel_multiset: inductive characterization *) -theorems rel_multiset_induct[case_names empty add, induct pred: rel_multiset] = - rel_multiset'.induct[unfolded rel_multiset_rel_multiset'[symmetric]] - - -(* Advanced relator customization *) - -(* Set vs. sum relators: *) - -lemma set_rel_sum_rel[simp]: -"set_rel (sum_rel \ \) A1 A2 \ - set_rel \ (Inl -` A1) (Inl -` A2) \ set_rel \ (Inr -` A1) (Inr -` A2)" -(is "?L \ ?Rl \ ?Rr") -proof safe - assume L: "?L" - show ?Rl unfolding set_rel_def Bex_def vimage_eq proof safe - fix l1 assume "Inl l1 \ A1" - then obtain a2 where a2: "a2 \ A2" and "sum_rel \ \ (Inl l1) a2" - using L unfolding set_rel_def by auto - then obtain l2 where "a2 = Inl l2 \ \ l1 l2" by (cases a2, auto) - thus "\ l2. Inl l2 \ A2 \ \ l1 l2" using a2 by auto - next - fix l2 assume "Inl l2 \ A2" - then obtain a1 where a1: "a1 \ A1" and "sum_rel \ \ a1 (Inl l2)" - using L unfolding set_rel_def by auto - then obtain l1 where "a1 = Inl l1 \ \ l1 l2" by (cases a1, auto) - thus "\ l1. Inl l1 \ A1 \ \ l1 l2" using a1 by auto - qed - show ?Rr unfolding set_rel_def Bex_def vimage_eq proof safe - fix r1 assume "Inr r1 \ A1" - then obtain a2 where a2: "a2 \ A2" and "sum_rel \ \ (Inr r1) a2" - using L unfolding set_rel_def by auto - then obtain r2 where "a2 = Inr r2 \ \ r1 r2" by (cases a2, auto) - thus "\ r2. Inr r2 \ A2 \ \ r1 r2" using a2 by auto - next - fix r2 assume "Inr r2 \ A2" - then obtain a1 where a1: "a1 \ A1" and "sum_rel \ \ a1 (Inr r2)" - using L unfolding set_rel_def by auto - then obtain r1 where "a1 = Inr r1 \ \ r1 r2" by (cases a1, auto) - thus "\ r1. Inr r1 \ A1 \ \ r1 r2" using a1 by auto - qed -next - assume Rl: "?Rl" and Rr: "?Rr" - show ?L unfolding set_rel_def Bex_def vimage_eq proof safe - fix a1 assume a1: "a1 \ A1" - show "\ a2. a2 \ A2 \ sum_rel \ \ a1 a2" - proof(cases a1) - case (Inl l1) then obtain l2 where "Inl l2 \ A2 \ \ l1 l2" - using Rl a1 unfolding set_rel_def by blast - thus ?thesis unfolding Inl by auto - next - case (Inr r1) then obtain r2 where "Inr r2 \ A2 \ \ r1 r2" - using Rr a1 unfolding set_rel_def by blast - thus ?thesis unfolding Inr by auto - qed - next - fix a2 assume a2: "a2 \ A2" - show "\ a1. a1 \ A1 \ sum_rel \ \ a1 a2" - proof(cases a2) - case (Inl l2) then obtain l1 where "Inl l1 \ A1 \ \ l1 l2" - using Rl a2 unfolding set_rel_def by blast - thus ?thesis unfolding Inl by auto - next - case (Inr r2) then obtain r1 where "Inr r1 \ A1 \ \ r1 r2" - using Rr a2 unfolding set_rel_def by blast - thus ?thesis unfolding Inr by auto - qed - qed -qed - -end diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/BNF/Tools/bnf_decl.ML --- a/src/HOL/BNF/Tools/bnf_decl.ML Mon Jan 20 18:24:56 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,117 +0,0 @@ -(* Title: HOL/BNF/Tools/bnf_decl.ML - Author: Dmitriy Traytel, TU Muenchen - Copyright 2013 - -Axiomatic declaration of bounded natural functors. -*) - -signature BNF_DECL = -sig - val bnf_decl: (binding option * (typ * sort)) list -> binding -> mixfix -> binding -> binding -> - typ list -> local_theory -> BNF_Def.bnf * local_theory -end - -structure BNF_Decl : BNF_DECL = -struct - -open BNF_Util -open BNF_Def - -fun prepare_decl prepare_constraint prepare_typ raw_vars b mx user_mapb user_relb user_witTs lthy = - let - fun prepare_type_arg (set_opt, (ty, c)) = - let val s = fst (dest_TFree (prepare_typ lthy ty)) in - (set_opt, (s, prepare_constraint lthy c)) - end; - val ((user_setbs, vars), raw_vars') = - map prepare_type_arg raw_vars - |> `split_list - |>> apfst (map_filter I); - val deads = map_filter (fn (NONE, x) => SOME x | _ => NONE) raw_vars'; - - fun mk_b name user_b = - (if Binding.is_empty user_b then Binding.prefix_name (name ^ "_") b else user_b) - |> Binding.qualify false (Binding.name_of b); - val (Tname, lthy) = Typedecl.basic_typedecl (b, length vars, mx) lthy; - val (bd_type_Tname, lthy) = - Typedecl.basic_typedecl (mk_b "bd_type" Binding.empty, length deads, NoSyn) lthy; - val T = Type (Tname, map TFree vars); - val bd_type_T = Type (bd_type_Tname, map TFree deads); - val lives = map TFree (filter_out (member (op =) deads) vars); - val live = length lives; - val _ = "Trying to declare a BNF with no live variables" |> null lives ? error; - val (lives', _) = BNF_Util.mk_TFrees (length lives) - (fold Variable.declare_typ (map TFree vars) lthy); - val T' = Term.typ_subst_atomic (lives ~~ lives') T; - val mapT = map2 (curry op -->) lives lives' ---> T --> T'; - val setTs = map (fn U => T --> HOLogic.mk_setT U) lives; - val bdT = BNF_Util.mk_relT (bd_type_T, bd_type_T); - val mapb = mk_b BNF_Def.mapN user_mapb; - val bdb = mk_b "bd" Binding.empty; - val setbs = map2 (fn b => fn i => mk_b (BNF_Def.mk_setN i) b) user_setbs - (if live = 1 then [0] else 1 upto live); - - val witTs = map (prepare_typ lthy) user_witTs; - val nwits = length witTs; - val witbs = map (fn i => mk_b (BNF_Def.mk_witN i) Binding.empty) - (if nwits = 1 then [0] else 1 upto nwits); - - val lthy = Local_Theory.background_theory - (Sign.add_consts_i ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) :: - map2 (fn b => fn T => (b, T, NoSyn)) setbs setTs @ - map2 (fn b => fn T => (b, T, NoSyn)) witbs witTs)) - lthy; - val Fmap = Const (Local_Theory.full_name lthy mapb, mapT); - val Fsets = map2 (fn setb => fn setT => - Const (Local_Theory.full_name lthy setb, setT)) setbs setTs; - val Fbd = Const (Local_Theory.full_name lthy bdb, bdT); - val Fwits = map2 (fn witb => fn witT => - Const (Local_Theory.full_name lthy witb, witT)) witbs witTs; - val (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, _) = - prepare_def Do_Inline (user_policy Note_Some) I (K I) (K I) (SOME (map TFree deads)) - user_mapb user_relb user_setbs ((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE) - lthy; - - fun mk_wits_tac set_maps = K (TRYALL Goal.conjunction_tac) THEN' the triv_tac_opt set_maps; - val wit_goals = map Logic.mk_conjunction_balanced wit_goalss; - val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []); - - val (((_, [raw_thms])), (lthy_old, lthy)) = Local_Theory.background_theory_result - (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy - ||> `Local_Theory.restore; - - fun mk_wit_thms set_maps = - Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) (mk_wits_tac set_maps) - |> Conjunction.elim_balanced (length wit_goals) - |> map2 (Conjunction.elim_balanced o length) wit_goalss - |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0)); - val phi = Proof_Context.export_morphism lthy_old lthy; - val thms = unflat all_goalss (Morphism.fact phi raw_thms); - in - BNF_Def.register_bnf key (after_qed mk_wit_thms thms lthy) - end; - -val bnf_decl = prepare_decl (K I) (K I); - -fun read_constraint _ NONE = HOLogic.typeS - | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s; - -val bnf_decl_cmd = prepare_decl read_constraint Syntax.read_typ; - -val parse_witTs = - @{keyword "["} |-- (Parse.short_ident --| @{keyword ":"} -- Scan.repeat Parse.typ - >> (fn ("wits", Ts) => Ts - | (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --| - @{keyword "]"} || Scan.succeed []; - -val parse_bnf_decl = - parse_type_args_named_constrained -- parse_binding -- parse_map_rel_bindings -- - parse_witTs -- Parse.opt_mixfix; - -val _ = - Outer_Syntax.local_theory @{command_spec "bnf_decl"} "bnf declaration" - (parse_bnf_decl >> - (fn ((((bsTs, b), (mapb, relb)), witTs), mx) => - bnf_decl_cmd bsTs b mx mapb relb witTs #> snd)); - -end; diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/BNF_Examples/Derivation_Trees/DTree.thy --- a/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy Mon Jan 20 18:24:56 2014 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/BNF/Examples/Derivation_Trees/DTree.thy +(* Title: HOL/BNF_Examples/Derivation_Trees/DTree.thy Author: Andrei Popescu, TU Muenchen Copyright 2012 diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy --- a/src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy Mon Jan 20 18:24:56 2014 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/BNF/Examples/Derivation_Trees/Gram_Lang.thy +(* Title: HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy Author: Andrei Popescu, TU Muenchen Copyright 2012 diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/BNF_Examples/Derivation_Trees/Parallel.thy --- a/src/HOL/BNF_Examples/Derivation_Trees/Parallel.thy Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/BNF_Examples/Derivation_Trees/Parallel.thy Mon Jan 20 18:24:56 2014 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/BNF/Examples/Derivation_Trees/Parallel.thy +(* Title: HOL/BNF_Examples/Derivation_Trees/Parallel.thy Author: Andrei Popescu, TU Muenchen Copyright 2012 diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy --- a/src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy Mon Jan 20 18:24:56 2014 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/BNF/Examples/Derivation_Trees/Prelim.thy +(* Title: HOL/BNF_Examples/Derivation_Trees/Prelim.thy Author: Andrei Popescu, TU Muenchen Copyright 2012 @@ -8,7 +8,7 @@ header {* Preliminaries *} theory Prelim -imports "../../BNF/More_BNFs" +imports "~~/src/HOL/Library/More_BNFs" begin declare fset_to_fset[simp] diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/BNF_Examples/Koenig.thy --- a/src/HOL/BNF_Examples/Koenig.thy Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/BNF_Examples/Koenig.thy Mon Jan 20 18:24:56 2014 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/BNF/Examples/Koenig.thy +(* Title: HOL/BNF_Examples/Koenig.thy Author: Dmitriy Traytel, TU Muenchen Author: Andrei Popescu, TU Muenchen Copyright 2012 diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/BNF_Examples/Lambda_Term.thy --- a/src/HOL/BNF_Examples/Lambda_Term.thy Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/BNF_Examples/Lambda_Term.thy Mon Jan 20 18:24:56 2014 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/BNF/Examples/Lambda_Term.thy +(* Title: HOL/BNF_Examples/Lambda_Term.thy Author: Dmitriy Traytel, TU Muenchen Author: Andrei Popescu, TU Muenchen Copyright 2012 diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/BNF_Examples/ListF.thy --- a/src/HOL/BNF_Examples/ListF.thy Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/BNF_Examples/ListF.thy Mon Jan 20 18:24:56 2014 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/BNF/Examples/ListF.thy +(* Title: HOL/BNF_Examples/ListF.thy Author: Dmitriy Traytel, TU Muenchen Author: Andrei Popescu, TU Muenchen Copyright 2012 diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/BNF_Examples/Misc_Codatatype.thy --- a/src/HOL/BNF_Examples/Misc_Codatatype.thy Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/BNF_Examples/Misc_Codatatype.thy Mon Jan 20 18:24:56 2014 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/BNF/Examples/Misc_Codatatype.thy +(* Title: HOL/BNF_Examples/Misc_Codatatype.thy Author: Dmitriy Traytel, TU Muenchen Author: Andrei Popescu, TU Muenchen Author: Jasmin Blanchette, TU Muenchen diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/BNF_Examples/Misc_Datatype.thy --- a/src/HOL/BNF_Examples/Misc_Datatype.thy Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/BNF_Examples/Misc_Datatype.thy Mon Jan 20 18:24:56 2014 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/BNF/Examples/Misc_Datatype.thy +(* Title: HOL/BNF_Examples/Misc_Datatype.thy Author: Dmitriy Traytel, TU Muenchen Author: Andrei Popescu, TU Muenchen Author: Jasmin Blanchette, TU Muenchen diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/BNF_Examples/Misc_Primcorec.thy --- a/src/HOL/BNF_Examples/Misc_Primcorec.thy Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/BNF_Examples/Misc_Primcorec.thy Mon Jan 20 18:24:56 2014 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/BNF/Examples/Misc_Primcorec.thy +(* Title: HOL/BNF_Examples/Misc_Primcorec.thy Author: Jasmin Blanchette, TU Muenchen Copyright 2013 diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/BNF_Examples/Misc_Primrec.thy --- a/src/HOL/BNF_Examples/Misc_Primrec.thy Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/BNF_Examples/Misc_Primrec.thy Mon Jan 20 18:24:56 2014 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/BNF/Examples/Misc_Primrec.thy +(* Title: HOL/BNF_Examples/Misc_Primrec.thy Author: Jasmin Blanchette, TU Muenchen Copyright 2013 diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/BNF_Examples/Process.thy --- a/src/HOL/BNF_Examples/Process.thy Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/BNF_Examples/Process.thy Mon Jan 20 18:24:56 2014 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/BNF/Examples/Process.thy +(* Title: HOL/BNF_Examples/Process.thy Author: Andrei Popescu, TU Muenchen Copyright 2012 diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/BNF_Examples/Stream.thy --- a/src/HOL/BNF_Examples/Stream.thy Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/BNF_Examples/Stream.thy Mon Jan 20 18:24:56 2014 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/BNF/Examples/Stream.thy +(* Title: HOL/BNF_Examples/Stream.thy Author: Dmitriy Traytel, TU Muenchen Author: Andrei Popescu, TU Muenchen Copyright 2012, 2013 diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/BNF_Examples/Stream_Processor.thy --- a/src/HOL/BNF_Examples/Stream_Processor.thy Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/BNF_Examples/Stream_Processor.thy Mon Jan 20 18:24:56 2014 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/BNF/Examples/Stream_Processor.thy +(* Title: HOL/BNF_Examples/Stream_Processor.thy Author: Dmitriy Traytel, TU Muenchen Author: Andrei Popescu, TU Muenchen Copyright 2014 diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/BNF_Examples/TreeFI.thy --- a/src/HOL/BNF_Examples/TreeFI.thy Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/BNF_Examples/TreeFI.thy Mon Jan 20 18:24:56 2014 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/BNF/Examples/TreeFI.thy +(* Title: HOL/BNF_Examples/TreeFI.thy Author: Dmitriy Traytel, TU Muenchen Author: Andrei Popescu, TU Muenchen Copyright 2012 diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/BNF_Examples/TreeFsetI.thy --- a/src/HOL/BNF_Examples/TreeFsetI.thy Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/BNF_Examples/TreeFsetI.thy Mon Jan 20 18:24:56 2014 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/BNF/Examples/TreeFsetI.thy +(* Title: HOL/BNF_Examples/TreeFsetI.thy Author: Dmitriy Traytel, TU Muenchen Author: Andrei Popescu, TU Muenchen Copyright 2012 diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/Basic_BNFs.thy --- a/src/HOL/Basic_BNFs.thy Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/Basic_BNFs.thy Mon Jan 20 18:24:56 2014 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/BNF/Basic_BNFs.thy +(* Title: HOL/Basic_BNFs.thy Author: Dmitriy Traytel, TU Muenchen Author: Andrei Popescu, TU Muenchen Author: Jasmin Blanchette, TU Muenchen diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/Cardinals/Cardinal_Notations.thy --- a/src/HOL/Cardinals/Cardinal_Notations.thy Mon Jan 20 18:24:56 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,23 +0,0 @@ -(* Title: HOL/Cardinals/Cardinal_Notations.thy - Author: Jasmin Blanchette, TU Muenchen - Copyright 2013 - -Cardinal notations. -*) - -header {* Cardinal Notations *} - -theory Cardinal_Notations -imports Main -begin - -notation - ordLeq2 (infix "<=o" 50) and - ordLeq3 (infix "\o" 50) and - ordLess2 (infix "o" 50) and + ordLess2 (infix " BNF_Util.Grp" + + +subsection{* Cardinal stuff *} + +lemma countable_card_of_nat: "countable A \ |A| \o |UNIV::nat set|" + unfolding countable_def card_of_ordLeq[symmetric] by auto + +lemma countable_card_le_natLeq: "countable A \ |A| \o natLeq" + unfolding countable_card_of_nat using card_of_nat ordLeq_ordIso_trans ordIso_symmetric by blast + +lemma countable_or_card_of: +assumes "countable A" +shows "(finite A \ |A| + (infinite A \ |A| =o |UNIV::nat set| )" +by (metis assms countable_card_of_nat infinite_iff_card_of_nat ordIso_iff_ordLeq + ordLeq_iff_ordLess_or_ordIso) + +lemma countable_cases_card_of[elim]: + assumes "countable A" + obtains (Fin) "finite A" "|A| (\ f::'a\nat. finite A \ inj_on f A) \ (\ f::'a\nat. infinite A \ bij_betw f A UNIV)" + by (elim countable_enum_cases) fastforce+ + +lemma countable_cases[elim]: + assumes "countable A" + obtains (Fin) f :: "'a\nat" where "finite A" "inj_on f A" + | (Inf) f :: "'a\nat" where "infinite A" "bij_betw f A UNIV" + using assms countable_or by metis + +lemma countable_ordLeq: +assumes "|A| \o |B|" and "countable B" +shows "countable A" +using assms unfolding countable_card_of_nat by(rule ordLeq_transitive) + +lemma countable_ordLess: +assumes AB: "|A| '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 Lifting_Set.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) + +subsection {* Registration as BNF *} + +lemma card_of_countable_sets_range: +fixes A :: "'a set" +shows "|{X. X \ A \ countable X \ X \ {}}| \o |{f::nat \ 'a. range f \ A}|" +apply(rule card_of_ordLeqI[of from_nat_into]) using inj_on_from_nat_into +unfolding inj_on_def by auto + +lemma card_of_countable_sets_Func: +"|{X. X \ A \ countable X \ X \ {}}| \o |A| ^c natLeq" +using card_of_countable_sets_range card_of_Func_UNIV[THEN ordIso_symmetric] +unfolding cexp_def Field_natLeq Field_card_of +by (rule ordLeq_ordIso_trans) + +lemma ordLeq_countable_subsets: +"|A| \o |{X. X \ A \ countable X}|" +apply (rule card_of_ordLeqI[of "\ a. {a}"]) unfolding inj_on_def by auto + +lemma finite_countable_subset: +"finite {X. X \ A \ countable X} \ finite A" +apply default + apply (erule contrapos_pp) + apply (rule card_of_ordLeq_infinite) + apply (rule ordLeq_countable_subsets) + apply assumption +apply (rule finite_Collect_conjI) +apply (rule disjI1) +by (erule finite_Collect_subsets) + +lemma rcset_to_rcset: "countable A \ rcset (the_inv rcset A) = A" + apply (rule f_the_inv_into_f[unfolded inj_on_def image_iff]) + apply transfer' apply simp + apply transfer' apply simp + done + +lemma Collect_Int_Times: +"{(x, y). R x y} \ A \ B = {(x, y). R x y \ x \ A \ y \ B}" +by auto + +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) \ + (\t \ rcset b. \u \ rcset a. R u t)" + +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}} (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 L: "countable ?L'" by auto + hence *: "rcset R' = ?L'" unfolding R'_def by (intro rcset_to_rcset) + thus ?R unfolding Grp_def relcompp.simps conversep.simps + proof (intro CollectI prod_caseI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl) + from * `?L` show "a = cimage fst R'" by transfer (auto simp: image_def Collect_Int_Times) + next + from * `?L` show "b = cimage snd R'" by transfer (auto simp: image_def Collect_Int_Times) + qed simp_all +next + assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps + by transfer force +qed + +bnf "'a cset" + map: cimage + sets: rcset + bd: natLeq + wits: "cempty" + rel: cset_rel +proof - + show "cimage id = id" by transfer' simp +next + fix f g show "cimage (g \ f) = cimage g \ cimage f" by transfer' fastforce +next + fix C f g assume eq: "\a. a \ rcset C \ f a = g a" + thus "cimage f C = cimage g C" by transfer force +next + 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" by transfer (unfold countable_card_le_natLeq) +next + fix R S + show "cset_rel R OO cset_rel S \ cset_rel (R OO S)" + unfolding cset_rel_def[abs_def] by fast +next + fix R + show "cset_rel R = + (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 (transfer, simp) + +end diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/Library/Library.thy Mon Jan 20 18:24:56 2014 +0100 @@ -5,13 +5,14 @@ BigO Binomial Bit + BNF_Decl Boolean_Algebra Char_ord Continuity ContNotDenum Convex Countable - Countable_Set + Countable_Set_Type Debug Diagonal_Subsequence Dlist @@ -37,6 +38,7 @@ Kleene_Algebra Mapping Monad_Syntax + More_BNFs Multiset Numeral_Type OptionalSugar diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/Library/More_BNFs.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/More_BNFs.thy Mon Jan 20 18:24:56 2014 +0100 @@ -0,0 +1,1050 @@ +(* Title: HOL/Library/More_BNFs.thy + Author: Dmitriy Traytel, TU Muenchen + Author: Andrei Popescu, TU Muenchen + Author: Andreas Lochbihler, Karlsruhe Institute of Technology + Author: Jasmin Blanchette, TU Muenchen + Copyright 2012 + +Registration of various types as bounded natural functors. +*) + +header {* Registration of Various Types as Bounded Natural Functors *} + +theory More_BNFs +imports FSet Multiset Cardinal_Notations +begin + +abbreviation "Grp \ BNF_Util.Grp" +abbreviation "fstOp \ BNF_Def.fstOp" +abbreviation "sndOp \ BNF_Def.sndOp" + +lemma option_rec_conv_option_case: "option_rec = option_case" +by (simp add: fun_eq_iff split: option.split) + +bnf "'a option" + map: Option.map + sets: Option.set + bd: natLeq + wits: None + rel: option_rel +proof - + show "Option.map id = id" by (simp add: fun_eq_iff Option.map_def split: option.split) +next + fix f g + show "Option.map (g \ f) = Option.map g \ Option.map f" + by (auto simp add: fun_eq_iff Option.map_def split: option.split) +next + fix f g x + assume "\z. z \ Option.set x \ f z = g z" + thus "Option.map f x = Option.map g x" + by (simp cong: Option.map_cong) +next + fix f + show "Option.set \ Option.map f = op ` f \ Option.set" + by fastforce +next + show "card_order natLeq" by (rule natLeq_card_order) +next + show "cinfinite natLeq" by (rule natLeq_cinfinite) +next + fix x + show "|Option.set x| \o natLeq" + by (cases x) (simp_all add: ordLess_imp_ordLeq finite_iff_ordLess_natLeq[symmetric]) +next + fix R S + show "option_rel R OO option_rel S \ option_rel (R OO S)" + by (auto simp: option_rel_def split: option.splits) +next + fix z + assume "z \ Option.set None" + thus False by simp +next + fix R + show "option_rel R = + (Grp {x. Option.set x \ Collect (split R)} (Option.map fst))\\ OO + Grp {x. Option.set x \ Collect (split R)} (Option.map snd)" + unfolding option_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff prod.cases + by (auto simp: trans[OF eq_commute option_map_is_None] trans[OF eq_commute option_map_eq_Some] + split: option.splits) +qed + +bnf "'a list" + map: map + sets: set + bd: natLeq + wits: Nil + rel: list_all2 +proof - + show "map id = id" by (rule List.map.id) +next + fix f g + show "map (g o f) = map g o map f" by (rule List.map.comp[symmetric]) +next + fix x f g + assume "\z. z \ set x \ f z = g z" + thus "map f x = map g x" by simp +next + fix f + show "set o map f = image f o set" by (rule ext, unfold comp_apply, rule set_map) +next + show "card_order natLeq" by (rule natLeq_card_order) +next + show "cinfinite natLeq" by (rule natLeq_cinfinite) +next + fix x + show "|set x| \o natLeq" + by (metis List.finite_set finite_iff_ordLess_natLeq ordLess_imp_ordLeq) +next + fix R S + show "list_all2 R OO list_all2 S \ list_all2 (R OO S)" + by (metis list_all2_OO order_refl) +next + fix R + show "list_all2 R = + (Grp {x. set x \ {(x, y). R x y}} (map fst))\\ OO + Grp {x. set x \ {(x, y). R x y}} (map snd)" + unfolding list_all2_def[abs_def] Grp_def fun_eq_iff relcompp.simps conversep.simps + by (force simp: zip_map_fst_snd) +qed simp_all + + +(* Finite sets *) + +context +includes fset.lifting +begin + +lemma fset_rel_alt: "fset_rel R a b \ (\t \ fset a. \u \ fset b. R t u) \ + (\t \ fset b. \u \ fset a. R u t)" + by transfer (simp add: set_rel_def) + +lemma fset_to_fset: "finite A \ fset (the_inv fset A) = A" + apply (rule f_the_inv_into_f[unfolded inj_on_def]) + apply (simp add: fset_inject) apply (rule range_eqI Abs_fset_inverse[symmetric] CollectI)+ + . + +lemma fset_rel_aux: +"(\t \ fset a. \u \ fset b. R t u) \ (\u \ fset b. \t \ fset a. R t u) \ + ((Grp {a. fset a \ {(a, b). R a b}} (fimage fst))\\ OO + Grp {a. fset a \ {(a, b). R a b}} (fimage snd)) a b" (is "?L = ?R") +proof + assume ?L + def R' \ "the_inv fset (Collect (split R) \ (fset a \ fset b))" (is "the_inv fset ?L'") + have "finite ?L'" by (intro finite_Int[OF disjI2] finite_cartesian_product) (transfer, simp)+ + hence *: "fset R' = ?L'" unfolding R'_def by (intro fset_to_fset) + show ?R unfolding Grp_def relcompp.simps conversep.simps + proof (intro CollectI prod_caseI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl) + from * show "a = fimage fst R'" using conjunct1[OF `?L`] + by (transfer, auto simp add: image_def Int_def split: prod.splits) + from * show "b = fimage snd R'" using conjunct2[OF `?L`] + by (transfer, auto simp add: image_def Int_def split: prod.splits) + qed (auto simp add: *) +next + assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps + apply (simp add: subset_eq Ball_def) + apply (rule conjI) + apply (transfer, clarsimp, metis snd_conv) + by (transfer, clarsimp, metis fst_conv) +qed + +bnf "'a fset" + map: fimage + sets: fset + bd: natLeq + wits: "{||}" + rel: fset_rel +apply - + apply transfer' apply simp + apply transfer' apply force + apply transfer apply force + apply transfer' apply force + apply (rule natLeq_card_order) + apply (rule natLeq_cinfinite) + apply transfer apply (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq) + apply (fastforce simp: fset_rel_alt) + apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff fset_rel_alt fset_rel_aux) +apply transfer apply simp +done + +lemma fset_rel_fset: "set_rel \ (fset A1) (fset A2) = fset_rel \ A1 A2" + by transfer (rule refl) + +end + +lemmas [simp] = fset.map_comp fset.map_id fset.set_map + + +(* Multisets *) + +lemma setsum_gt_0_iff: +fixes f :: "'a \ nat" assumes "finite A" +shows "setsum f A > 0 \ (\ a \ A. f a > 0)" +(is "?L \ ?R") +proof- + have "?L \ \ setsum f A = 0" by fast + also have "... \ (\ a \ A. f a \ 0)" using assms by simp + also have "... \ ?R" by simp + finally show ?thesis . +qed + +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 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_id0: "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 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 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 comp_apply, blast) +qed + +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) + +context +begin +interpretation lifting_syntax . + +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 + +end + +lemma set_of_mmap: "set_of o mmap h = image h o set_of" +proof (rule ext, unfold comp_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}" +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 + hence "set as \ A" using M by auto + thus "M \ multiset_of ` {as. set as \ A}" using eq by auto +next + show "\x xa xb. \set xa \ A; xb \ set_of (multiset_of xa)\ \ xb \ A" + by (erule set_mp) (unfold set_of_multiset_of) +qed + +lemma card_of_set_of: +"|{M. set_of M \ A}| \o |{as. set as \ A}|" +apply(rule card_of_ordLeqI2[of _ multiset_of]) using multiset_of_surj by auto + +lemma nat_sum_induct: +assumes "\n1 n2. (\ m1 m2. m1 + m2 < n1 + n2 \ phi m1 m2) \ phi n1 n2" +shows "phi (n1::nat) (n2::nat)" +proof- + let ?chi = "\ n1n2 :: nat * nat. phi (fst n1n2) (snd n1n2)" + have "?chi (n1,n2)" + apply(induct rule: measure_induct[of "\ n1n2. fst n1n2 + snd n1n2" ?chi]) + using assms by (metis fstI sndI) + thus ?thesis by simp +qed + +lemma matrix_count: +fixes ct1 ct2 :: "nat \ nat" +assumes "setsum ct1 {.. ct. (\ i1 \ n1. setsum (\ i2. ct i1 i2) {.. + (\ i2 \ n2. setsum (\ i1. ct i1 i2) {.. ct1 ct2 :: nat \ nat. + setsum ct1 {.. ?phi ct1 ct2 n1 n2" + proof(induct rule: nat_sum_induct[of +"\ n1 n2. \ ct1 ct2 :: nat \ nat. + setsum ct1 {.. ?phi ct1 ct2 n1 n2"], + clarify) + fix n1 n2 :: nat and ct1 ct2 :: "nat \ nat" + assume IH: "\ m1 m2. m1 + m2 < n1 + n2 \ + \ dt1 dt2 :: nat \ nat. + setsum dt1 {.. ?phi dt1 dt2 m1 m2" + and ss: "setsum ct1 {.. ct2 n2") + case True + def dt2 \ "\ i2. if i2 = n2 then ct2 i2 - ct1 n1 else ct2 i2" + have "setsum ct1 {.. i1. i1 \ m1 \ setsum (\ i2. dt i1 i2) {.. i2. i2 \ n2 \ setsum (\ i1. dt i1 i2) {.. "\ i1. if i1 = n1 then ct1 i1 - ct2 n2 else ct1 i1" + have "setsum dt1 {.. i1. i1 \ n1 \ setsum (\ i2. dt i1 i2) {.. i2. i2 \ m2 \ setsum (\ i1. dt i1 i2) {.. + \ b1 b1' b2 b2'. {b1,b1'} \ B1 \ {b2,b2'} \ B2 \ u b1 b2 = u b1' b2' + \ b1 = b1' \ b2 = b2'" + +lemma matrix_setsum_finite: +assumes B1: "B1 \ {}" "finite B1" and B2: "B2 \ {}" "finite B2" and u: "inj2 u B1 B2" +and ss: "setsum N1 B1 = setsum N2 B2" +shows "\ M :: 'a \ nat. + (\ b1 \ B1. setsum (\ b2. M (u b1 b2)) B2 = N1 b1) \ + (\ b2 \ B2. setsum (\ b1. M (u b1 b2)) B1 = N2 b2)" +proof- + obtain n1 where "card B1 = Suc n1" using B1 by (metis card_insert finite.simps) + then obtain e1 where e1: "bij_betw e1 {.. "inv_into {.. i1. i1 < Suc n1 \ f1 (e1 i1) = i1" + and e1f1[simp]: "\ b1. b1 \ B1 \ e1 (f1 b1) = b1" unfolding f1_def + apply (metis bij_betw_inv_into e1, metis bij_betw_inv_into_left e1 lessThan_iff) + by (metis e1_surj f_inv_into_f) + (* *) + obtain n2 where "card B2 = Suc n2" using B2 by (metis card_insert finite.simps) + then obtain e2 where e2: "bij_betw e2 {.. "inv_into {.. i2. i2 < Suc n2 \ f2 (e2 i2) = i2" + and e2f2[simp]: "\ b2. b2 \ B2 \ e2 (f2 b2) = b2" unfolding f2_def + apply (metis bij_betw_inv_into e2, metis bij_betw_inv_into_left e2 lessThan_iff) + by (metis e2_surj f_inv_into_f) + (* *) + let ?ct1 = "N1 o e1" let ?ct2 = "N2 o e2" + have ss: "setsum ?ct1 {.. i1. i1 \ n1 \ setsum (\ i2. ct i1 i2) {.. i2. i2 \ n2 \ setsum (\ i1. ct i1 i2) {.. "{u b1 b2 | b1 b2. b1 \ B1 \ b2 \ B2}" + have "\ a \ A. \ b1b2 \ B1 <*> B2. u (fst b1b2) (snd b1b2) = a" + unfolding A_def Ball_def mem_Collect_eq by auto + then obtain h1h2 where h12: + "\a. a \ A \ u (fst (h1h2 a)) (snd (h1h2 a)) = a \ h1h2 a \ B1 <*> B2" by metis + def h1 \ "fst o h1h2" def h2 \ "snd o h1h2" + have h12[simp]: "\a. a \ A \ u (h1 a) (h2 a) = a" + "\ a. a \ A \ h1 a \ B1" "\ a. a \ A \ h2 a \ B2" + using h12 unfolding h1_def h2_def by force+ + {fix b1 b2 assume b1: "b1 \ B1" and b2: "b2 \ B2" + hence inA: "u b1 b2 \ A" unfolding A_def by auto + hence "u b1 b2 = u (h1 (u b1 b2)) (h2 (u b1 b2))" by auto + moreover have "h1 (u b1 b2) \ B1" "h2 (u b1 b2) \ B2" using inA by auto + ultimately have "h1 (u b1 b2) = b1 \ h2 (u b1 b2) = b2" + using u b1 b2 unfolding inj2_def by fastforce + } + hence h1[simp]: "\ b1 b2. \b1 \ B1; b2 \ B2\ \ h1 (u b1 b2) = b1" and + h2[simp]: "\ b1 b2. \b1 \ B1; b2 \ B2\ \ h2 (u b1 b2) = b2" by auto + def M \ "\ a. ct (f1 (h1 a)) (f2 (h2 a))" + show ?thesis + apply(rule exI[of _ M]) proof safe + fix b1 assume b1: "b1 \ B1" + hence f1b1: "f1 b1 \ n1" using f1 unfolding bij_betw_def + by (metis image_eqI lessThan_iff less_Suc_eq_le) + have "(\b2\B2. M (u b1 b2)) = (\i2b2\B2. M (u b1 b2)) = N1 b1" . + next + fix b2 assume b2: "b2 \ B2" + hence f2b2: "f2 b2 \ n2" using f2 unfolding bij_betw_def + by (metis image_eqI lessThan_iff less_Suc_eq_le) + have "(\b1\B1. M (u b1 b2)) = (\i1b1\B1. M (u b1 b2)) = N2 b2" . + qed +qed + +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: "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" +shows "finite {u b1 b2 |b1 b2. b1 \ B1 \ b2 \ B2}" (is "finite ?A") +proof- + have A: "?A = (\ b1b2. u (fst b1b2) (snd b1b2)) ` (B1 <*> B2)" by force + show ?thesis unfolding A using finite_cartesian_product[OF assms] by auto +qed + +(* Weak pullbacks: *) +definition wpull where +"wpull A B1 B2 f1 f2 p1 p2 \ + (\ b1 b2. b1 \ B1 \ b2 \ B2 \ f1 b1 = f2 b2 \ (\ a \ A. p1 a = b1 \ p2 a = b2))" + +(* Weak pseudo-pullbacks *) +definition wppull where +"wppull A B1 B2 f1 f2 e1 e2 p1 p2 \ + (\ b1 b2. b1 \ B1 \ b2 \ B2 \ f1 b1 = f2 b2 \ + (\ a \ A. e1 (p1 a) = e1 b1 \ e2 (p2 a) = e2 b2))" + + +(* The pullback of sets *) +definition thePull where +"thePull B1 B2 f1 f2 = {(b1,b2). b1 \ B1 \ b2 \ B2 \ f1 b1 = f2 b2}" + +lemma wpull_thePull: +"wpull (thePull B1 B2 f1 f2) B1 B2 f1 f2 fst snd" +unfolding wpull_def thePull_def by auto + +lemma wppull_thePull: +assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2" +shows +"\ j. \ a' \ thePull B1 B2 f1 f2. + j a' \ A \ + e1 (p1 (j a')) = e1 (fst a') \ e2 (p2 (j a')) = e2 (snd a')" +(is "\ j. \ a' \ ?A'. ?phi a' (j a')") +proof(rule bchoice[of ?A' ?phi], default) + fix a' assume a': "a' \ ?A'" + hence "fst a' \ B1" unfolding thePull_def by auto + moreover + from a' have "snd a' \ B2" unfolding thePull_def by auto + moreover have "f1 (fst a') = f2 (snd a')" + using a' unfolding csquare_def thePull_def by auto + ultimately show "\ ja'. ?phi a' ja'" + using assms unfolding wppull_def by blast +qed + +lemma wpull_wppull: +assumes wp: "wpull A' B1 B2 f1 f2 p1' p2'" and +1: "\ a' \ A'. j a' \ A \ e1 (p1 (j a')) = e1 (p1' a') \ e2 (p2 (j a')) = e2 (p2' a')" +shows "wppull A B1 B2 f1 f2 e1 e2 p1 p2" +unfolding wppull_def proof safe + fix b1 b2 + assume b1: "b1 \ B1" and b2: "b2 \ B2" and f: "f1 b1 = f2 b2" + then obtain a' where a': "a' \ A'" and b1: "b1 = p1' a'" and b2: "b2 = p2' a'" + using wp unfolding wpull_def by blast + show "\a\A. e1 (p1 a) = e1 b1 \ e2 (p2 a) = e2 b2" + apply (rule bexI[of _ "j a'"]) unfolding b1 b2 using a' 1 by auto +qed + +lemma wppull_fstOp_sndOp: +shows "wppull (Collect (split (P OO Q))) (Collect (split P)) (Collect (split Q)) + snd fst fst snd (fstOp P Q) (sndOp P Q)" +using pick_middlep unfolding wppull_def fstOp_def sndOp_def relcompp.simps by auto + +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. 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 multiset" and N2 :: "'b2 multiset" + assume mmap': "mmap f1 N1 = mmap f2 N2" + 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 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 \ 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 \ 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 (count N1) (set1 c) = count P c" + unfolding P1 set1_def by transfer (auto intro: setsum_cong) + (* *) + 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 \ set_of P \ finite (set2 c)" + using N2(1) unfolding set2_def multiset_def by auto + 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 (count N2) (set2 c) = count P c" + unfolding P2 set2_def by transfer (auto intro: setsum_cong) + (* *) + 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) + then obtain uu where uu: + "\ c \ set_of P. \ b1b2 \ (set1 c) \ (set2 c). + uu c b1b2 \ A \ p1 (uu c b1b2) = fst b1b2 \ p2 (uu c b1b2) = snd b1b2" by metis + def u \ "\ c b1 b2. uu c (b1,b2)" + have u[simp]: + "\ c b1 b2. \c \ set_of P; b1 \ set1 c; b2 \ set2 c\ \ u c b1 b2 \ A" + "\ c b1 b2. \c \ set_of P; b1 \ set1 c; b2 \ set2 c\ \ p1 (u c b1 b2) = b1" + "\ c b1 b2. \c \ set_of P; b1 \ set1 c; b2 \ set2 c\ \ p2 (u c b1 b2) = b2" + using uu unfolding u_def by auto + {fix c assume c: "c \ set_of P" + have "inj2 (u c) (set1 c) (set2 c)" unfolding inj2_def proof clarify + fix b1 b1' b2 b2' + assume "{b1, b1'} \ set1 c" "{b2, b2'} \ set2 c" and 0: "u c b1 b2 = u c b1' b2'" + hence "p1 (u c b1 b2) = b1 \ p2 (u c b1 b2) = b2 \ + p1 (u c b1' b2') = b1' \ p2 (u c b1' b2') = b2'" + using u(2)[OF c] u(3)[OF c] by simp metis + thus "b1 = b1' \ b2 = b2'" using 0 by auto + qed + } note inj = this + def sset \ "\ c. {u c b1 b2 | b1 b2. b1 \ set1 c \ b2 \ set2 c}" + have fin_sset[simp]: "\ c. c \ set_of P \ finite (sset c)" unfolding sset_def + using fin_set1 fin_set2 finite_twosets by blast + have sset_A: "\ c. c \ set_of P \ sset c \ A" unfolding sset_def by auto + {fix c a assume c: "c \ set_of P" and ac: "a \ sset c" + then obtain b1 b2 where b1: "b1 \ set1 c" and b2: "b2 \ set2 c" + and a: "a = u c b1 b2" unfolding sset_def by auto + have "p1 a \ set1 c" and p2a: "p2 a \ set2 c" + using ac a b1 b2 c u(2) u(3) by simp+ + hence "u c (p1 a) (p2 a) = a" unfolding a using b1 b2 inj[OF c] + unfolding inj2_def by (metis c u(2) u(3)) + } note u_p12[simp] = this + {fix c a assume c: "c \ set_of P" and ac: "a \ sset c" + hence "p1 a \ set1 c" unfolding sset_def by auto + }note p1[simp] = this + {fix c a assume c: "c \ set_of P" and ac: "a \ sset c" + hence "p2 a \ set2 c" unfolding sset_def by auto + }note p2[simp] = this + (* *) + {fix c assume c: "c \ set_of P" + hence "\ M. (\ b1 \ set1 c. setsum (\ b2. M (u c b1 b2)) (set2 c) = count N1 b1) \ + (\ b2 \ set2 c. setsum (\ b1. M (u c b1 b2)) (set1 c) = count N2 b2)" + unfolding sset_def + using matrix_setsum_finite[OF set1_NE[OF c] fin_set1[OF c] + set2_NE[OF c] fin_set2[OF c] inj[OF c] ss[OF c]] by auto + } + then obtain Ms where + ss1: "\ c b1. \c \ set_of P; b1 \ set1 c\ \ + setsum (\ b2. Ms c (u c b1 b2)) (set2 c) = count N1 b1" and + ss2: "\ c b2. \c \ set_of P; b2 \ set2 c\ \ + setsum (\ b1. Ms c (u c b1 b2)) (set1 c) = count N2 b2" + by metis + def SET \ "\ c \ set_of P. sset c" + have fin_SET[simp]: "finite SET" unfolding SET_def apply(rule finite_UN_I) by auto + have SET_A: "SET \ A" unfolding SET_def using sset_A by blast + have u_SET[simp]: "\ c b1 b2. \c \ set_of P; b1 \ set1 c; b2 \ set2 c\ \ u c b1 b2 \ SET" + unfolding SET_def sset_def by blast + {fix c a assume c: "c \ set_of P" and a: "a \ SET" and p1a: "p1 a \ set1 c" + then obtain c' where c': "c' \ set_of P" and ac': "a \ sset c'" + unfolding SET_def by auto + hence "p1 a \ set1 c'" unfolding sset_def by auto + hence eq: "c = c'" using p1a c c' set1_disj by auto + hence "a \ sset c" using ac' by simp + } note p1_rev = this + {fix c a assume c: "c \ set_of P" and a: "a \ SET" and p2a: "p2 a \ set2 c" + then obtain c' where c': "c' \ set_of P" and ac': "a \ sset c'" + unfolding SET_def by auto + hence "p2 a \ set2 c'" unfolding sset_def by auto + hence eq: "c = c'" using p2a c c' set2_disj by auto + hence "a \ sset c" using ac' by simp + } note p2_rev = this + (* *) + have "\ a \ SET. \ c \ set_of P. a \ sset c" unfolding SET_def by auto + then obtain h where h: "\ a \ SET. h a \ set_of P \ a \ sset (h a)" by metis + have h_u[simp]: "\ c b1 b2. \c \ set_of P; b1 \ set1 c; b2 \ set2 c\ + \ h (u c b1 b2) = c" + by (metis h p2 set2 u(3) u_SET) + have h_u1: "\ c b1 b2. \c \ set_of P; b1 \ set1 c; b2 \ set2 c\ + \ h (u c b1 b2) = f1 b1" + using h unfolding sset_def by auto + have h_u2: "\ c b1 b2. \c \ set_of P; b1 \ set1 c; b2 \ set2 c\ + \ h (u c b1 b2) = f2 b2" + using h unfolding sset_def by auto + def M \ + "Abs_multiset (\ a. if a \ SET \ p1 a \ set_of N1 \ p2 a \ set_of N2 then Ms (h a) a else 0)" + have "(\ a. if a \ SET \ p1 a \ set_of N1 \ p2 a \ set_of N2 then Ms (h a) a else 0) \ multiset" + unfolding multiset_def by auto + hence [transfer_rule]: "pcr_multiset op = (\ a. if a \ SET \ p1 a \ set_of N1 \ p2 a \ set_of N2 then Ms (h a) a else 0) M" + unfolding M_def pcr_multiset_def cr_multiset_def by (auto simp: Abs_multiset_inverse) + have sM: "set_of M \ SET" "set_of M \ p1 -` (set_of N1)" "set_of M \ p2 -` set_of N2" + by (transfer, auto split: split_if_asm)+ + show "\M. set_of M \ A \ mmap p1 M = N1 \ mmap p2 M = N2" + proof(rule exI[of _ M], safe) + fix a assume *: "a \ set_of M" + from SET_A show "a \ A" + proof (cases "a \ SET") + case False thus ?thesis using * by transfer' auto + qed blast + next + show "mmap p1 M = N1" + proof(intro multiset_eqI) + fix b1 + let ?K = "{a. p1 a = b1 \ a \# M}" + have "setsum (count M) ?K = count N1 b1" + proof(cases "b1 \ set_of N1") + case False + hence "?K = {}" using sM(2) by auto + thus ?thesis using False by auto + next + case True + def c \ "f1 b1" + have c: "c \ set_of P" and b1: "b1 \ set1 c" + unfolding set1_def c_def P1 using True by (auto simp: comp_eq_dest[OF set_of_mmap]) + with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p1 a = b1 \ a \ SET}" + by transfer (force intro: setsum_mono_zero_cong_left split: split_if_asm) + also have "... = setsum (count M) ((\ b2. u c b1 b2) ` (set2 c))" + apply(rule setsum_cong) using c b1 proof safe + fix a assume p1a: "p1 a \ set1 c" and "c \ set_of P" and "a \ SET" + hence ac: "a \ sset c" using p1_rev by auto + hence "a = u c (p1 a) (p2 a)" using c by auto + moreover have "p2 a \ set2 c" using ac c by auto + ultimately show "a \ u c (p1 a) ` set2 c" by auto + qed auto + also have "... = setsum (\ b2. count M (u c b1 b2)) (set2 c)" + unfolding comp_def[symmetric] apply(rule setsum_reindex) + using inj unfolding inj_on_def inj2_def using b1 c u(3) by blast + also have "... = count N1 b1" unfolding ss1[OF c b1, symmetric] + apply(rule setsum_cong[OF refl]) apply (transfer fixing: Ms u c b1 set2) + using True h_u[OF c b1] set2_def u(2,3)[OF c b1] u_SET[OF c b1] by fastforce + finally show ?thesis . + qed + thus "count (mmap p1 M) b1 = count N1 b1" by transfer + qed + next +next + show "mmap p2 M = N2" + proof(intro multiset_eqI) + fix b2 + let ?K = "{a. p2 a = b2 \ a \# M}" + have "setsum (count M) ?K = count N2 b2" + proof(cases "b2 \ set_of N2") + case False + hence "?K = {}" using sM(3) by auto + thus ?thesis using False by auto + next + case True + def c \ "f2 b2" + have c: "c \ set_of P" and b2: "b2 \ set2 c" + unfolding set2_def c_def P2 using True by (auto simp: comp_eq_dest[OF set_of_mmap]) + with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p2 a = b2 \ a \ SET}" + by transfer (force intro: setsum_mono_zero_cong_left split: split_if_asm) + also have "... = setsum (count M) ((\ b1. u c b1 b2) ` (set1 c))" + apply(rule setsum_cong) using c b2 proof safe + fix a assume p2a: "p2 a \ set2 c" and "c \ set_of P" and "a \ SET" + hence ac: "a \ sset c" using p2_rev by auto + hence "a = u c (p1 a) (p2 a)" using c by auto + moreover have "p1 a \ set1 c" using ac c by auto + ultimately show "a \ (\x. u c x (p2 a)) ` set1 c" by auto + qed auto + also have "... = setsum (count M o (\ b1. u c b1 b2)) (set1 c)" + apply(rule setsum_reindex) + using inj unfolding inj_on_def inj2_def using b2 c u(2) by blast + also have "... = setsum (\ b1. count M (u c b1 b2)) (set1 c)" by simp + also have "... = count N2 b2" unfolding ss2[OF c b2, symmetric] comp_def + apply(rule setsum_cong[OF refl]) apply (transfer fixing: Ms u c b2 set1) + using True h_u1[OF c _ b2] u(2,3)[OF c _ b2] u_SET[OF c _ b2] set1_def by fastforce + finally show ?thesis . + qed + thus "count (mmap p2 M) b2 = count N2 b2" by transfer + qed + qed +qed + +lemma set_of_bd: "|set_of x| \o natLeq" + by transfer + (auto intro!: ordLess_imp_ordLeq simp: finite_iff_ordLess_natLeq[symmetric] multiset_def) + +lemma wppull_mmap: + assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2" + shows "wppull {M. set_of M \ A} {N1. set_of N1 \ B1} {N2. set_of N2 \ B2} + (mmap f1) (mmap f2) (mmap e1) (mmap e2) (mmap p1) (mmap p2)" +proof - + from assms obtain j where j: "\a'\thePull B1 B2 f1 f2. + j a' \ A \ e1 (p1 (j a')) = e1 (fst a') \ e2 (p2 (j a')) = e2 (snd a')" + by (blast dest: wppull_thePull) + then show ?thesis + by (intro wpull_wppull[OF wpull_mmap[OF wpull_thePull], of _ _ _ _ "mmap j"]) + (auto simp: comp_eq_dest_lhs[OF mmap_comp[symmetric]] comp_eq_dest[OF set_of_mmap] + intro!: mmap_cong simp del: mem_set_of_iff simp: mem_set_of_iff[symmetric]) +qed + +bnf "'a multiset" + map: mmap + sets: set_of + bd: natLeq + wits: "{#}" +by (auto simp add: mmap_id0 mmap_comp set_of_mmap natLeq_card_order natLeq_cinfinite set_of_bd + Grp_def relcompp.simps intro: mmap_cong) + (metis wppull_mmap[OF wppull_fstOp_sndOp, unfolded wppull_def + o_eq_dest_lhs[OF mmap_comp[symmetric]] fstOp_def sndOp_def comp_def, simplified]) + +inductive rel_multiset' where + Zero[intro]: "rel_multiset' R {#} {#}" +| Plus[intro]: "\R a b; rel_multiset' R M N\ \ rel_multiset' R (M + {#a#}) (N + {#b#})" + +lemma map_multiset_Zero_iff[simp]: "mmap f M = {#} \ M = {#}" +by (metis image_is_empty multiset.set_map set_of_eq_empty_iff) + +lemma map_multiset_Zero[simp]: "mmap f {#} = {#}" by simp + +lemma rel_multiset_Zero: "rel_multiset R {#} {#}" +unfolding rel_multiset_def Grp_def by auto + +declare multiset.count[simp] +declare Abs_multiset_inverse[simp] +declare multiset.count_inverse[simp] +declare union_preserves_multiset[simp] + + +lemma map_multiset_Plus[simp]: "mmap f (M1 + M2) = mmap f M1 + mmap f M2" +proof (intro multiset_eqI, transfer fixing: f) + fix x :: 'a and M1 M2 :: "'b \ nat" + assume "M1 \ multiset" "M2 \ multiset" + hence "setsum M1 {a. f a = x \ 0 < M1 a} = setsum M1 {a. f a = x \ 0 < M1 a + M2 a}" + "setsum M2 {a. f a = x \ 0 < M2 a} = setsum M2 {a. f a = x \ 0 < M1 a + M2 a}" + by (auto simp: multiset_def intro!: setsum_mono_zero_cong_left) + then show "(\a | f a = x \ 0 < M1 a + M2 a. M1 a + M2 a) = + setsum M1 {a. f a = x \ 0 < M1 a} + + setsum M2 {a. f a = x \ 0 < M2 a}" + by (auto simp: setsum.distrib[symmetric]) +qed + +lemma map_multiset_singl[simp]: "mmap f {#a#} = {#f a#}" + by transfer auto + +lemma rel_multiset_Plus: +assumes ab: "R a b" and MN: "rel_multiset R M N" +shows "rel_multiset R (M + {#a#}) (N + {#b#})" +proof- + {fix y assume "R a b" and "set_of y \ {(x, y). R x y}" + hence "\ya. mmap fst y + {#a#} = mmap fst ya \ + mmap snd y + {#b#} = mmap snd ya \ + set_of ya \ {(x, y). R x y}" + apply(intro exI[of _ "y + {#(a,b)#}"]) by auto + } + thus ?thesis + using assms + unfolding rel_multiset_def Grp_def by force +qed + +lemma rel_multiset'_imp_rel_multiset: +"rel_multiset' R M N \ rel_multiset R M N" +apply(induct rule: rel_multiset'.induct) +using rel_multiset_Zero rel_multiset_Plus by auto + +lemma mcard_mmap[simp]: "mcard (mmap f M) = mcard M" +proof - + def A \ "\ b. {a. f a = b \ a \# M}" + let ?B = "{b. 0 < setsum (count M) (A b)}" + have "{b. \a. f a = b \ a \# M} \ f ` {a. a \# M}" by auto + moreover have "finite (f ` {a. a \# M})" apply(rule finite_imageI) + using finite_Collect_mem . + ultimately have fin: "finite {b. \a. f a = b \ a \# M}" by(rule finite_subset) + have i: "inj_on A ?B" unfolding inj_on_def A_def apply clarsimp + by (metis (lifting, full_types) mem_Collect_eq neq0_conv setsum.neutral) + have 0: "\ b. 0 < setsum (count M) (A b) \ (\ a \ A b. count M a > 0)" + apply safe + apply (metis less_not_refl setsum_gt_0_iff setsum_infinite) + by (metis A_def finite_Collect_conjI finite_Collect_mem setsum_gt_0_iff) + hence AB: "A ` ?B = {A b | b. \ a \ A b. count M a > 0}" by auto + + have "setsum (\ x. setsum (count M) (A x)) ?B = setsum (setsum (count M) o A) ?B" + unfolding comp_def .. + also have "... = (\x\ A ` ?B. setsum (count M) x)" + unfolding setsum.reindex [OF i, symmetric] .. + also have "... = setsum (count M) (\x\A ` {b. 0 < setsum (count M) (A b)}. x)" + (is "_ = setsum (count M) ?J") + apply(rule setsum.UNION_disjoint[symmetric]) + using 0 fin unfolding A_def by auto + also have "?J = {a. a \# M}" unfolding AB unfolding A_def by auto + finally have "setsum (\ x. setsum (count M) (A x)) ?B = + setsum (count M) {a. a \# M}" . + then show ?thesis unfolding mcard_unfold_setsum A_def by transfer +qed + +lemma rel_multiset_mcard: +assumes "rel_multiset R M N" +shows "mcard M = mcard N" +using assms unfolding rel_multiset_def Grp_def by auto + +lemma multiset_induct2[case_names empty addL addR]: +assumes empty: "P {#} {#}" +and addL: "\M N a. P M N \ P (M + {#a#}) N" +and addR: "\M N a. P M N \ P M (N + {#a#})" +shows "P M N" +apply(induct N rule: multiset_induct) + apply(induct M rule: multiset_induct, rule empty, erule addL) + apply(induct M rule: multiset_induct, erule addR, erule addR) +done + +lemma multiset_induct2_mcard[consumes 1, case_names empty add]: +assumes c: "mcard M = mcard N" +and empty: "P {#} {#}" +and add: "\M N a b. P M N \ P (M + {#a#}) (N + {#b#})" +shows "P M N" +using c proof(induct M arbitrary: N rule: measure_induct_rule[of mcard]) + case (less M) show ?case + proof(cases "M = {#}") + case True hence "N = {#}" using less.prems by auto + thus ?thesis using True empty by auto + next + case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split) + have "N \ {#}" using False less.prems by auto + then obtain N1 b where N: "N = N1 + {#b#}" by (metis multi_nonempty_split) + have "mcard M1 = mcard N1" using less.prems unfolding M N by auto + thus ?thesis using M N less.hyps add by auto + qed +qed + +lemma msed_map_invL: +assumes "mmap f (M + {#a#}) = N" +shows "\ N1. N = N1 + {#f a#} \ mmap f M = N1" +proof- + have "f a \# N" + using assms multiset.set_map[of f "M + {#a#}"] by auto + then obtain N1 where N: "N = N1 + {#f a#}" using multi_member_split by metis + have "mmap f M = N1" using assms unfolding N by simp + thus ?thesis using N by blast +qed + +lemma msed_map_invR: +assumes "mmap f M = N + {#b#}" +shows "\ M1 a. M = M1 + {#a#} \ f a = b \ mmap f M1 = N" +proof- + obtain a where a: "a \# M" and fa: "f a = b" + using multiset.set_map[of f M] unfolding assms + by (metis image_iff mem_set_of_iff union_single_eq_member) + then obtain M1 where M: "M = M1 + {#a#}" using multi_member_split by metis + have "mmap f M1 = N" using assms unfolding M fa[symmetric] by simp + thus ?thesis using M fa by blast +qed + +lemma msed_rel_invL: +assumes "rel_multiset R (M + {#a#}) N" +shows "\ N1 b. N = N1 + {#b#} \ R a b \ rel_multiset R M N1" +proof- + obtain K where KM: "mmap fst K = M + {#a#}" + and KN: "mmap snd K = N" and sK: "set_of K \ {(a, b). R a b}" + using assms + unfolding rel_multiset_def Grp_def by auto + obtain K1 ab where K: "K = K1 + {#ab#}" and a: "fst ab = a" + and K1M: "mmap fst K1 = M" using msed_map_invR[OF KM] by auto + obtain N1 where N: "N = N1 + {#snd ab#}" and K1N1: "mmap snd K1 = N1" + using msed_map_invL[OF KN[unfolded K]] by auto + have Rab: "R a (snd ab)" using sK a unfolding K by auto + have "rel_multiset R M N1" using sK K1M K1N1 + unfolding K rel_multiset_def Grp_def by auto + thus ?thesis using N Rab by auto +qed + +lemma msed_rel_invR: +assumes "rel_multiset R M (N + {#b#})" +shows "\ M1 a. M = M1 + {#a#} \ R a b \ rel_multiset R M1 N" +proof- + obtain K where KN: "mmap snd K = N + {#b#}" + and KM: "mmap fst K = M" and sK: "set_of K \ {(a, b). R a b}" + using assms + unfolding rel_multiset_def Grp_def by auto + obtain K1 ab where K: "K = K1 + {#ab#}" and b: "snd ab = b" + and K1N: "mmap snd K1 = N" using msed_map_invR[OF KN] by auto + obtain M1 where M: "M = M1 + {#fst ab#}" and K1M1: "mmap fst K1 = M1" + using msed_map_invL[OF KM[unfolded K]] by auto + have Rab: "R (fst ab) b" using sK b unfolding K by auto + have "rel_multiset R M1 N" using sK K1N K1M1 + unfolding K rel_multiset_def Grp_def by auto + thus ?thesis using M Rab by auto +qed + +lemma rel_multiset_imp_rel_multiset': +assumes "rel_multiset R M N" +shows "rel_multiset' R M N" +using assms proof(induct M arbitrary: N rule: measure_induct_rule[of mcard]) + case (less M) + have c: "mcard M = mcard N" using rel_multiset_mcard[OF less.prems] . + show ?case + proof(cases "M = {#}") + case True hence "N = {#}" using c by simp + thus ?thesis using True rel_multiset'.Zero by auto + next + case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split) + obtain N1 b where N: "N = N1 + {#b#}" and R: "R a b" and ms: "rel_multiset R M1 N1" + using msed_rel_invL[OF less.prems[unfolded M]] by auto + have "rel_multiset' R M1 N1" using less.hyps[of M1 N1] ms unfolding M by simp + thus ?thesis using rel_multiset'.Plus[of R a b, OF R] unfolding M N by simp + qed +qed + +lemma rel_multiset_rel_multiset': +"rel_multiset R M N = rel_multiset' R M N" +using rel_multiset_imp_rel_multiset' rel_multiset'_imp_rel_multiset by auto + +(* The main end product for rel_multiset: inductive characterization *) +theorems rel_multiset_induct[case_names empty add, induct pred: rel_multiset] = + rel_multiset'.induct[unfolded rel_multiset_rel_multiset'[symmetric]] + + +(* Advanced relator customization *) + +(* Set vs. sum relators: *) + +lemma set_rel_sum_rel[simp]: +"set_rel (sum_rel \ \) A1 A2 \ + set_rel \ (Inl -` A1) (Inl -` A2) \ set_rel \ (Inr -` A1) (Inr -` A2)" +(is "?L \ ?Rl \ ?Rr") +proof safe + assume L: "?L" + show ?Rl unfolding set_rel_def Bex_def vimage_eq proof safe + fix l1 assume "Inl l1 \ A1" + then obtain a2 where a2: "a2 \ A2" and "sum_rel \ \ (Inl l1) a2" + using L unfolding set_rel_def by auto + then obtain l2 where "a2 = Inl l2 \ \ l1 l2" by (cases a2, auto) + thus "\ l2. Inl l2 \ A2 \ \ l1 l2" using a2 by auto + next + fix l2 assume "Inl l2 \ A2" + then obtain a1 where a1: "a1 \ A1" and "sum_rel \ \ a1 (Inl l2)" + using L unfolding set_rel_def by auto + then obtain l1 where "a1 = Inl l1 \ \ l1 l2" by (cases a1, auto) + thus "\ l1. Inl l1 \ A1 \ \ l1 l2" using a1 by auto + qed + show ?Rr unfolding set_rel_def Bex_def vimage_eq proof safe + fix r1 assume "Inr r1 \ A1" + then obtain a2 where a2: "a2 \ A2" and "sum_rel \ \ (Inr r1) a2" + using L unfolding set_rel_def by auto + then obtain r2 where "a2 = Inr r2 \ \ r1 r2" by (cases a2, auto) + thus "\ r2. Inr r2 \ A2 \ \ r1 r2" using a2 by auto + next + fix r2 assume "Inr r2 \ A2" + then obtain a1 where a1: "a1 \ A1" and "sum_rel \ \ a1 (Inr r2)" + using L unfolding set_rel_def by auto + then obtain r1 where "a1 = Inr r1 \ \ r1 r2" by (cases a1, auto) + thus "\ r1. Inr r1 \ A1 \ \ r1 r2" using a1 by auto + qed +next + assume Rl: "?Rl" and Rr: "?Rr" + show ?L unfolding set_rel_def Bex_def vimage_eq proof safe + fix a1 assume a1: "a1 \ A1" + show "\ a2. a2 \ A2 \ sum_rel \ \ a1 a2" + proof(cases a1) + case (Inl l1) then obtain l2 where "Inl l2 \ A2 \ \ l1 l2" + using Rl a1 unfolding set_rel_def by blast + thus ?thesis unfolding Inl by auto + next + case (Inr r1) then obtain r2 where "Inr r2 \ A2 \ \ r1 r2" + using Rr a1 unfolding set_rel_def by blast + thus ?thesis unfolding Inr by auto + qed + next + fix a2 assume a2: "a2 \ A2" + show "\ a1. a1 \ A1 \ sum_rel \ \ a1 a2" + proof(cases a2) + case (Inl l2) then obtain l1 where "Inl l1 \ A1 \ \ l1 l2" + using Rl a2 unfolding set_rel_def by blast + thus ?thesis unfolding Inl by auto + next + case (Inr r2) then obtain r1 where "Inr r1 \ A1 \ \ r1 r2" + using Rr a2 unfolding set_rel_def by blast + thus ?thesis unfolding Inr by auto + qed + qed +qed + +end diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/Library/bnf_decl.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/bnf_decl.ML Mon Jan 20 18:24:56 2014 +0100 @@ -0,0 +1,117 @@ +(* Title: HOL/BNF/Tools/bnf_decl.ML + Author: Dmitriy Traytel, TU Muenchen + Copyright 2013 + +Axiomatic declaration of bounded natural functors. +*) + +signature BNF_DECL = +sig + val bnf_decl: (binding option * (typ * sort)) list -> binding -> mixfix -> binding -> binding -> + typ list -> local_theory -> BNF_Def.bnf * local_theory +end + +structure BNF_Decl : BNF_DECL = +struct + +open BNF_Util +open BNF_Def + +fun prepare_decl prepare_constraint prepare_typ raw_vars b mx user_mapb user_relb user_witTs lthy = + let + fun prepare_type_arg (set_opt, (ty, c)) = + let val s = fst (dest_TFree (prepare_typ lthy ty)) in + (set_opt, (s, prepare_constraint lthy c)) + end; + val ((user_setbs, vars), raw_vars') = + map prepare_type_arg raw_vars + |> `split_list + |>> apfst (map_filter I); + val deads = map_filter (fn (NONE, x) => SOME x | _ => NONE) raw_vars'; + + fun mk_b name user_b = + (if Binding.is_empty user_b then Binding.prefix_name (name ^ "_") b else user_b) + |> Binding.qualify false (Binding.name_of b); + val (Tname, lthy) = Typedecl.basic_typedecl (b, length vars, mx) lthy; + val (bd_type_Tname, lthy) = + Typedecl.basic_typedecl (mk_b "bd_type" Binding.empty, length deads, NoSyn) lthy; + val T = Type (Tname, map TFree vars); + val bd_type_T = Type (bd_type_Tname, map TFree deads); + val lives = map TFree (filter_out (member (op =) deads) vars); + val live = length lives; + val _ = "Trying to declare a BNF with no live variables" |> null lives ? error; + val (lives', _) = BNF_Util.mk_TFrees (length lives) + (fold Variable.declare_typ (map TFree vars) lthy); + val T' = Term.typ_subst_atomic (lives ~~ lives') T; + val mapT = map2 (curry op -->) lives lives' ---> T --> T'; + val setTs = map (fn U => T --> HOLogic.mk_setT U) lives; + val bdT = BNF_Util.mk_relT (bd_type_T, bd_type_T); + val mapb = mk_b BNF_Def.mapN user_mapb; + val bdb = mk_b "bd" Binding.empty; + val setbs = map2 (fn b => fn i => mk_b (BNF_Def.mk_setN i) b) user_setbs + (if live = 1 then [0] else 1 upto live); + + val witTs = map (prepare_typ lthy) user_witTs; + val nwits = length witTs; + val witbs = map (fn i => mk_b (BNF_Def.mk_witN i) Binding.empty) + (if nwits = 1 then [0] else 1 upto nwits); + + val lthy = Local_Theory.background_theory + (Sign.add_consts_i ((mapb, mapT, NoSyn) :: (bdb, bdT, NoSyn) :: + map2 (fn b => fn T => (b, T, NoSyn)) setbs setTs @ + map2 (fn b => fn T => (b, T, NoSyn)) witbs witTs)) + lthy; + val Fmap = Const (Local_Theory.full_name lthy mapb, mapT); + val Fsets = map2 (fn setb => fn setT => + Const (Local_Theory.full_name lthy setb, setT)) setbs setTs; + val Fbd = Const (Local_Theory.full_name lthy bdb, bdT); + val Fwits = map2 (fn witb => fn witT => + Const (Local_Theory.full_name lthy witb, witT)) witbs witTs; + val (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, _) = + prepare_def Do_Inline (user_policy Note_Some) I (K I) (K I) (SOME (map TFree deads)) + user_mapb user_relb user_setbs ((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE) + lthy; + + fun mk_wits_tac set_maps = K (TRYALL Goal.conjunction_tac) THEN' the triv_tac_opt set_maps; + val wit_goals = map Logic.mk_conjunction_balanced wit_goalss; + val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []); + + val (((_, [raw_thms])), (lthy_old, lthy)) = Local_Theory.background_theory_result + (Specification.axiomatization [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy + ||> `Local_Theory.restore; + + fun mk_wit_thms set_maps = + Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) (mk_wits_tac set_maps) + |> Conjunction.elim_balanced (length wit_goals) + |> map2 (Conjunction.elim_balanced o length) wit_goalss + |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0)); + val phi = Proof_Context.export_morphism lthy_old lthy; + val thms = unflat all_goalss (Morphism.fact phi raw_thms); + in + BNF_Def.register_bnf key (after_qed mk_wit_thms thms lthy) + end; + +val bnf_decl = prepare_decl (K I) (K I); + +fun read_constraint _ NONE = HOLogic.typeS + | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s; + +val bnf_decl_cmd = prepare_decl read_constraint Syntax.read_typ; + +val parse_witTs = + @{keyword "["} |-- (Parse.short_ident --| @{keyword ":"} -- Scan.repeat Parse.typ + >> (fn ("wits", Ts) => Ts + | (s, _) => error ("Unknown label " ^ quote s ^ " (expected \"wits\")"))) --| + @{keyword "]"} || Scan.succeed []; + +val parse_bnf_decl = + parse_type_args_named_constrained -- parse_binding -- parse_map_rel_bindings -- + parse_witTs -- Parse.opt_mixfix; + +val _ = + Outer_Syntax.local_theory @{command_spec "bnf_decl"} "bnf declaration" + (parse_bnf_decl >> + (fn ((((bsTs, b), (mapb, relb)), witTs), mx) => + bnf_decl_cmd bsTs b mx mapb relb witTs #> snd)); + +end; diff -r 2b0b6f69b148 -r b3d0a02a756d src/HOL/ROOT --- a/src/HOL/ROOT Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/ROOT Mon Jan 20 18:24:56 2014 +0100 @@ -699,13 +699,6 @@ "document/root.tex" "document/root.bib" -session "HOL-BNF" in BNF = HOL + - description {* - Bounded Natural Functors for (Co)datatypes, Including More BNFs. - *} - options [document = false] - theories BNF - session "HOL-BNF_Examples" in BNF_Examples = HOL + description {* Examples for Bounded Natural Functors.