killed 'More_BNFs' by moving its various bits where they (now) belong
authorblanchet
Fri Jan 24 11:51:45 2014 +0100 (2014-01-24)
changeset 5512926bd1cba3ab5
parent 55128 6e16d2dd4f14
child 55131 9808f186795c
killed 'More_BNFs' by moving its various bits where they (now) belong
src/Doc/Datatypes/Datatypes.thy
src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy
src/HOL/BNF_Examples/Lambda_Term.thy
src/HOL/BNF_Examples/Misc_Codatatype.thy
src/HOL/BNF_Examples/Misc_Datatype.thy
src/HOL/BNF_Examples/TreeFsetI.thy
src/HOL/Library/FSet.thy
src/HOL/Library/Library.thy
src/HOL/Library/More_BNFs.thy
src/HOL/Library/Multiset.thy
src/HOL/Lifting_Option.thy
src/HOL/List.thy
src/HOL/Option.thy
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Thu Jan 23 19:02:22 2014 +0100
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Fri Jan 24 11:51:45 2014 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4  imports
     1.5    Setup
     1.6    "~~/src/HOL/Library/BNF_Decl"
     1.7 -  "~~/src/HOL/Library/More_BNFs"
     1.8 +  "~~/src/HOL/Library/FSet"
     1.9    "~~/src/HOL/Library/Simps_Case_Conv"
    1.10  begin
    1.11  
    1.12 @@ -79,8 +79,8 @@
    1.13  infinite branching.
    1.14  
    1.15  The package is part of @{theory Main}. Additional functionality is provided by
    1.16 -the theories @{theory BNF_Decl} and @{theory More_BNFs}, located in the
    1.17 -directory \verb|~~/src/HOL/Library|.
    1.18 +the theory @{theory BNF_Decl}, located in the directory
    1.19 +\verb|~~/src/HOL/Library|.
    1.20  
    1.21  The package, like its predecessor, fully adheres to the LCF philosophy
    1.22  \cite{mgordon79}: The characteristic theorems associated with the specified
    1.23 @@ -304,13 +304,20 @@
    1.24  
    1.25  text {*
    1.26  \noindent
    1.27 -This is legal:
    1.28 +The following definition of @{typ 'a}-branching trees is legal:
    1.29  *}
    1.30  
    1.31      datatype_new 'a ftree = FTLeaf 'a | FTNode "'a \<Rightarrow> 'a ftree"
    1.32  
    1.33  text {*
    1.34  \noindent
    1.35 +And so is the definition of hereditarily finite sets:
    1.36 +*}
    1.37 +
    1.38 +    datatype_new hfset = HFSet "hfset fset"
    1.39 +
    1.40 +text {*
    1.41 +\noindent
    1.42  In general, type constructors @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
    1.43  allow recursion on a subset of their type arguments @{text 'a\<^sub>1}, \ldots,
    1.44  @{text 'a\<^sub>m}. These type arguments are called \emph{live}; the remaining
    1.45 @@ -2297,8 +2304,9 @@
    1.46    \label{ssec:bnf-introductory-example} *}
    1.47  
    1.48  text {*
    1.49 -More examples in \verb|~~/src/HOL/Basic_BNFs.thy| and
    1.50 -\verb|~~/src/HOL/Library/More_BNFs.thy|.
    1.51 +More examples in \verb|~~/src/HOL/Basic_BNFs.thy|,
    1.52 +\verb|~~/src/HOL/Library/FSet.thy|, and
    1.53 +\verb|~~/src/HOL/Library/Multiset.thy|.
    1.54  
    1.55  %Mention distinction between live and dead type arguments;
    1.56  %  * and existence of map, set for those
    1.57 @@ -2506,12 +2514,12 @@
    1.58  Tobias Nipkow and Makarius Wenzel encouraged us to implement the new
    1.59  (co)datatype package. Andreas Lochbihler provided lots of comments on earlier
    1.60  versions of the package, especially for the coinductive part. Brian Huffman
    1.61 -suggested major simplifications to the internal constructions, many of which has
    1.62 -yet to be implemented. Florian Haftmann and Christian Urban provided general
    1.63 -advice on Isabelle and package writing. Stefan Milius and Lutz Schr\"oder
    1.64 -found an elegant proof to eliminate one of the BNF assumptions. Andreas
    1.65 -Lochbihler and Christian Sternagel suggested many textual improvements to this
    1.66 -tutorial.
    1.67 +suggested major simplifications to the internal constructions, many of which
    1.68 +have yet to be implemented. Florian Haftmann and Christian Urban provided
    1.69 +general advice on Isabelle and package writing. Stefan Milius and Lutz
    1.70 +Schr\"oder found an elegant proof that eliminated one of the BNF proof
    1.71 +obligations. Andreas Lochbihler and Christian Sternagel suggested many textual
    1.72 +improvements to this tutorial.
    1.73  *}
    1.74  
    1.75  end
     2.1 --- a/src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy	Thu Jan 23 19:02:22 2014 +0100
     2.2 +++ b/src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy	Fri Jan 24 11:51:45 2014 +0100
     2.3 @@ -8,7 +8,7 @@
     2.4  header {* Preliminaries *}
     2.5  
     2.6  theory Prelim
     2.7 -imports "~~/src/HOL/Library/More_BNFs"
     2.8 +imports "~~/src/HOL/Library/FSet"
     2.9  begin
    2.10  
    2.11  notation BNF_Def.convol ("<_ , _>")
     3.1 --- a/src/HOL/BNF_Examples/Lambda_Term.thy	Thu Jan 23 19:02:22 2014 +0100
     3.2 +++ b/src/HOL/BNF_Examples/Lambda_Term.thy	Fri Jan 24 11:51:45 2014 +0100
     3.3 @@ -9,7 +9,7 @@
     3.4  header {* Lambda-Terms *}
     3.5  
     3.6  theory Lambda_Term
     3.7 -imports "~~/src/HOL/Library/More_BNFs"
     3.8 +imports "~~/src/HOL/Library/FSet"
     3.9  begin
    3.10  
    3.11  section {* Datatype definition *}
    3.12 @@ -21,7 +21,7 @@
    3.13    Lt "('a \<times> 'a trm) fset" "'a trm"
    3.14  
    3.15  
    3.16 -subsection{* Example: The set of all variables varsOf and free variables fvarsOf of a term: *}
    3.17 +subsection {* Example: The set of all variables varsOf and free variables fvarsOf of a term *}
    3.18  
    3.19  primrec_new varsOf :: "'a trm \<Rightarrow> 'a set" where
    3.20    "varsOf (Var a) = {a}"
    3.21 @@ -38,7 +38,7 @@
    3.22  
    3.23  lemma diff_Un_incl_triv: "\<lbrakk>A \<subseteq> D; C \<subseteq> E\<rbrakk> \<Longrightarrow> A - B \<union> C \<subseteq> D \<union> E" by blast
    3.24  
    3.25 -lemma in_fmap_map_pair_fset_iff[simp]:
    3.26 +lemma in_fimage_map_pair_fset_iff[simp]:
    3.27    "(x, y) |\<in>| fimage (map_pair f g) xts \<longleftrightarrow> (\<exists> t1 t2. (t1, t2) |\<in>| xts \<and> x = f t1 \<and> y = g t2)"
    3.28    by force
    3.29  
     4.1 --- a/src/HOL/BNF_Examples/Misc_Codatatype.thy	Thu Jan 23 19:02:22 2014 +0100
     4.2 +++ b/src/HOL/BNF_Examples/Misc_Codatatype.thy	Fri Jan 24 11:51:45 2014 +0100
     4.3 @@ -10,7 +10,7 @@
     4.4  header {* Miscellaneous Codatatype Definitions *}
     4.5  
     4.6  theory Misc_Codatatype
     4.7 -imports "~~/src/HOL/Library/More_BNFs"
     4.8 +imports "~~/src/HOL/Library/FSet"
     4.9  begin
    4.10  
    4.11  codatatype simple = X1 | X2 | X3 | X4
     5.1 --- a/src/HOL/BNF_Examples/Misc_Datatype.thy	Thu Jan 23 19:02:22 2014 +0100
     5.2 +++ b/src/HOL/BNF_Examples/Misc_Datatype.thy	Fri Jan 24 11:51:45 2014 +0100
     5.3 @@ -10,7 +10,7 @@
     5.4  header {* Miscellaneous Datatype Definitions *}
     5.5  
     5.6  theory Misc_Datatype
     5.7 -imports "~~/src/HOL/Library/More_BNFs"
     5.8 +imports "~~/src/HOL/Library/FSet"
     5.9  begin
    5.10  
    5.11  datatype_new simple = X1 | X2 | X3 | X4
     6.1 --- a/src/HOL/BNF_Examples/TreeFsetI.thy	Thu Jan 23 19:02:22 2014 +0100
     6.2 +++ b/src/HOL/BNF_Examples/TreeFsetI.thy	Fri Jan 24 11:51:45 2014 +0100
     6.3 @@ -9,7 +9,7 @@
     6.4  header {* Finitely Branching Possibly Infinite Trees, with Sets of Children *}
     6.5  
     6.6  theory TreeFsetI
     6.7 -imports "~~/src/HOL/Library/More_BNFs"
     6.8 +imports "~~/src/HOL/Library/FSet"
     6.9  begin
    6.10  
    6.11  codatatype 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset")
     7.1 --- a/src/HOL/Library/FSet.thy	Thu Jan 23 19:02:22 2014 +0100
     7.2 +++ b/src/HOL/Library/FSet.thy	Fri Jan 24 11:51:45 2014 +0100
     7.3 @@ -1,12 +1,13 @@
     7.4  (*  Title:      HOL/Library/FSet.thy
     7.5      Author:     Ondrej Kuncar, TU Muenchen
     7.6      Author:     Cezary Kaliszyk and Christian Urban
     7.7 +    Author:     Andrei Popescu, TU Muenchen
     7.8  *)
     7.9  
    7.10  header {* Type of finite sets defined as a subtype of sets *}
    7.11  
    7.12  theory FSet
    7.13 -imports Main Conditionally_Complete_Lattices
    7.14 +imports Conditionally_Complete_Lattices
    7.15  begin
    7.16  
    7.17  subsection {* Definition of the type *}
    7.18 @@ -16,6 +17,7 @@
    7.19  
    7.20  setup_lifting type_definition_fset
    7.21  
    7.22 +
    7.23  subsection {* Basic operations and type class instantiations *}
    7.24  
    7.25  (* FIXME transfer and right_total vs. bi_total *)
    7.26 @@ -148,6 +150,7 @@
    7.27  abbreviation fUNIV :: "'a::finite fset" where "fUNIV \<equiv> top"
    7.28  abbreviation fuminus :: "'a::finite fset \<Rightarrow> 'a fset" ("|-| _" [81] 80) where "|-| x \<equiv> uminus x"
    7.29  
    7.30 +
    7.31  subsection {* Other operations *}
    7.32  
    7.33  lift_definition finsert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is insert parametric Lifting_Set.insert_transfer
    7.34 @@ -167,6 +170,7 @@
    7.35  
    7.36  context
    7.37  begin
    7.38 +
    7.39  interpretation lifting_syntax .
    7.40  
    7.41  lift_definition ffilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Set.filter 
    7.42 @@ -203,6 +207,7 @@
    7.43  
    7.44  lift_definition ffold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" is Finite_Set.fold ..
    7.45  
    7.46 +
    7.47  subsection {* Transferred lemmas from Set.thy *}
    7.48  
    7.49  lemmas fset_eqI = set_eqI[Transfer.transferred]
    7.50 @@ -442,12 +447,14 @@
    7.51  lemmas ffmember_filter[simp] = member_filter[Transfer.transferred]
    7.52  lemmas fequalityI = equalityI[Transfer.transferred]
    7.53  
    7.54 +
    7.55  subsection {* Additional lemmas*}
    7.56  
    7.57  subsubsection {* @{text fsingleton} *}
    7.58  
    7.59  lemmas fsingletonE = fsingletonD [elim_format]
    7.60  
    7.61 +
    7.62  subsubsection {* @{text femepty} *}
    7.63  
    7.64  lemma fempty_ffilter[simp]: "ffilter (\<lambda>_. False) A = {||}"
    7.65 @@ -457,6 +464,7 @@
    7.66  lemma femptyE [elim!]: "a |\<in>| {||} \<Longrightarrow> P"
    7.67    by simp
    7.68  
    7.69 +
    7.70  subsubsection {* @{text fset} *}
    7.71  
    7.72  lemmas fset_simps[simp] = bot_fset.rep_eq finsert.rep_eq
    7.73 @@ -479,6 +487,7 @@
    7.74  
    7.75  lemmas minus_fset[simp] = minus_fset.rep_eq
    7.76  
    7.77 +
    7.78  subsubsection {* @{text filter_fset} *}
    7.79  
    7.80  lemma subset_ffilter: 
    7.81 @@ -494,6 +503,7 @@
    7.82      ffilter P A |\<subset>| ffilter Q A"
    7.83    unfolding less_fset_def by (auto simp add: subset_ffilter eq_ffilter)
    7.84  
    7.85 +
    7.86  subsubsection {* @{text finsert} *}
    7.87  
    7.88  (* FIXME, transferred doesn't work here *)
    7.89 @@ -505,11 +515,13 @@
    7.90  lemma mk_disjoint_finsert: "a |\<in>| A \<Longrightarrow> \<exists>B. A = finsert a B \<and> a |\<notin>| B"
    7.91    by (rule_tac x = "A |-| {|a|}" in exI, blast)
    7.92  
    7.93 +
    7.94  subsubsection {* @{text fimage} *}
    7.95  
    7.96  lemma subset_fimage_iff: "(B |\<subseteq>| f|`|A) = (\<exists> AA. AA |\<subseteq>| A \<and> B = f|`|AA)"
    7.97  by transfer (metis mem_Collect_eq rev_finite_subset subset_image_iff)
    7.98  
    7.99 +
   7.100  subsubsection {* bounded quantification *}
   7.101  
   7.102  lemma bex_simps [simp, no_atp]:
   7.103 @@ -540,6 +552,7 @@
   7.104  
   7.105  end
   7.106  
   7.107 +
   7.108  subsubsection {* @{text fcard} *}
   7.109  
   7.110  (* FIXME: improve transferred to handle bounded meta quantification *)
   7.111 @@ -622,6 +635,7 @@
   7.112  lemma fcard_pfsubset: "A |\<subseteq>| B \<Longrightarrow> fcard A < fcard B \<Longrightarrow> A < B"
   7.113  by transfer (rule card_psubset)
   7.114  
   7.115 +
   7.116  subsubsection {* @{text ffold} *}
   7.117  
   7.118  (* FIXME: improve transferred to handle bounded meta quantification *)
   7.119 @@ -680,6 +694,7 @@
   7.120  
   7.121  end
   7.122  
   7.123 +
   7.124  subsection {* Choice in fsets *}
   7.125  
   7.126  lemma fset_choice: 
   7.127 @@ -687,6 +702,7 @@
   7.128    shows "\<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"
   7.129    using assms by transfer metis
   7.130  
   7.131 +
   7.132  subsection {* Induction and Cases rules for fsets *}
   7.133  
   7.134  lemma fset_exhaust [case_names empty insert, cases type: fset]:
   7.135 @@ -752,6 +768,7 @@
   7.136    apply simp_all
   7.137    done
   7.138  
   7.139 +
   7.140  subsection {* Setup for Lifting/Transfer *}
   7.141  
   7.142  subsubsection {* Relator and predicator properties *}
   7.143 @@ -851,6 +868,7 @@
   7.144  
   7.145  lemmas fset_invariant_commute [invariant_commute] = set_invariant_commute[Transfer.transferred]
   7.146  
   7.147 +
   7.148  subsubsection {* Quotient theorem for the Lifting package *}
   7.149  
   7.150  lemma Quotient_fset_map[quot_map]:
   7.151 @@ -859,6 +877,7 @@
   7.152    using assms unfolding Quotient_alt_def4
   7.153    by (simp add: fset_rel_OO[symmetric] fset_rel_conversep) (simp add: fset_rel_alt_def, blast)
   7.154  
   7.155 +
   7.156  subsubsection {* Transfer rules for the Transfer package *}
   7.157  
   7.158  text {* Unconditional transfer rules *}
   7.159 @@ -971,4 +990,137 @@
   7.160  lifting_update fset.lifting
   7.161  lifting_forget fset.lifting
   7.162  
   7.163 +
   7.164 +subsection {* BNF setup *}
   7.165 +
   7.166 +context
   7.167 +includes fset.lifting
   7.168 +begin
   7.169 +
   7.170 +lemma fset_rel_alt:
   7.171 +  "fset_rel R a b \<longleftrightarrow> (\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and> (\<forall>t \<in> fset b. \<exists>u \<in> fset a. R u t)"
   7.172 +by transfer (simp add: set_rel_def)
   7.173 +
   7.174 +lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A"
   7.175 +apply (rule f_the_inv_into_f[unfolded inj_on_def])
   7.176 +apply (simp add: fset_inject)
   7.177 +apply (rule range_eqI Abs_fset_inverse[symmetric] CollectI)+
   7.178 +.
   7.179 +
   7.180 +lemma fset_rel_aux:
   7.181 +"(\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and> (\<forall>u \<in> fset b. \<exists>t \<in> fset a. R t u) \<longleftrightarrow>
   7.182 + ((BNF_Util.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage fst))\<inverse>\<inverse> OO
   7.183 +  BNF_Util.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage snd)) a b" (is "?L = ?R")
   7.184 +proof
   7.185 +  assume ?L
   7.186 +  def R' \<equiv> "the_inv fset (Collect (split R) \<inter> (fset a \<times> fset b))" (is "the_inv fset ?L'")
   7.187 +  have "finite ?L'" by (intro finite_Int[OF disjI2] finite_cartesian_product) (transfer, simp)+
   7.188 +  hence *: "fset R' = ?L'" unfolding R'_def by (intro fset_to_fset)
   7.189 +  show ?R unfolding Grp_def relcompp.simps conversep.simps
   7.190 +  proof (intro CollectI prod_caseI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
   7.191 +    from * show "a = fimage fst R'" using conjunct1[OF `?L`]
   7.192 +      by (transfer, auto simp add: image_def Int_def split: prod.splits)
   7.193 +    from * show "b = fimage snd R'" using conjunct2[OF `?L`]
   7.194 +      by (transfer, auto simp add: image_def Int_def split: prod.splits)
   7.195 +  qed (auto simp add: *)
   7.196 +next
   7.197 +  assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps
   7.198 +  apply (simp add: subset_eq Ball_def)
   7.199 +  apply (rule conjI)
   7.200 +  apply (transfer, clarsimp, metis snd_conv)
   7.201 +  by (transfer, clarsimp, metis fst_conv)
   7.202 +qed
   7.203 +
   7.204 +bnf "'a fset"
   7.205 +  map: fimage
   7.206 +  sets: fset 
   7.207 +  bd: natLeq
   7.208 +  wits: "{||}"
   7.209 +  rel: fset_rel
   7.210 +apply -
   7.211 +          apply transfer' apply simp
   7.212 +         apply transfer' apply force
   7.213 +        apply transfer apply force
   7.214 +       apply transfer' apply force
   7.215 +      apply (rule natLeq_card_order)
   7.216 +     apply (rule natLeq_cinfinite)
   7.217 +    apply transfer apply (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq)
   7.218 +   apply (fastforce simp: fset_rel_alt)
   7.219 + apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff fset_rel_alt fset_rel_aux) 
   7.220 +apply transfer apply simp
   7.221 +done
   7.222 +
   7.223 +lemma fset_rel_fset: "set_rel \<chi> (fset A1) (fset A2) = fset_rel \<chi> A1 A2"
   7.224 +  by transfer (rule refl)
   7.225 +
   7.226  end
   7.227 +
   7.228 +lemmas [simp] = fset.map_comp fset.map_id fset.set_map
   7.229 +
   7.230 +
   7.231 +subsection {* Advanced relator customization *}
   7.232 +
   7.233 +(* Set vs. sum relators: *)
   7.234 +
   7.235 +lemma set_rel_sum_rel[simp]: 
   7.236 +"set_rel (sum_rel \<chi> \<phi>) A1 A2 \<longleftrightarrow> 
   7.237 + set_rel \<chi> (Inl -` A1) (Inl -` A2) \<and> set_rel \<phi> (Inr -` A1) (Inr -` A2)"
   7.238 +(is "?L \<longleftrightarrow> ?Rl \<and> ?Rr")
   7.239 +proof safe
   7.240 +  assume L: "?L"
   7.241 +  show ?Rl unfolding set_rel_def Bex_def vimage_eq proof safe
   7.242 +    fix l1 assume "Inl l1 \<in> A1"
   7.243 +    then obtain a2 where a2: "a2 \<in> A2" and "sum_rel \<chi> \<phi> (Inl l1) a2"
   7.244 +    using L unfolding set_rel_def by auto
   7.245 +    then obtain l2 where "a2 = Inl l2 \<and> \<chi> l1 l2" by (cases a2, auto)
   7.246 +    thus "\<exists> l2. Inl l2 \<in> A2 \<and> \<chi> l1 l2" using a2 by auto
   7.247 +  next
   7.248 +    fix l2 assume "Inl l2 \<in> A2"
   7.249 +    then obtain a1 where a1: "a1 \<in> A1" and "sum_rel \<chi> \<phi> a1 (Inl l2)"
   7.250 +    using L unfolding set_rel_def by auto
   7.251 +    then obtain l1 where "a1 = Inl l1 \<and> \<chi> l1 l2" by (cases a1, auto)
   7.252 +    thus "\<exists> l1. Inl l1 \<in> A1 \<and> \<chi> l1 l2" using a1 by auto
   7.253 +  qed
   7.254 +  show ?Rr unfolding set_rel_def Bex_def vimage_eq proof safe
   7.255 +    fix r1 assume "Inr r1 \<in> A1"
   7.256 +    then obtain a2 where a2: "a2 \<in> A2" and "sum_rel \<chi> \<phi> (Inr r1) a2"
   7.257 +    using L unfolding set_rel_def by auto
   7.258 +    then obtain r2 where "a2 = Inr r2 \<and> \<phi> r1 r2" by (cases a2, auto)
   7.259 +    thus "\<exists> r2. Inr r2 \<in> A2 \<and> \<phi> r1 r2" using a2 by auto
   7.260 +  next
   7.261 +    fix r2 assume "Inr r2 \<in> A2"
   7.262 +    then obtain a1 where a1: "a1 \<in> A1" and "sum_rel \<chi> \<phi> a1 (Inr r2)"
   7.263 +    using L unfolding set_rel_def by auto
   7.264 +    then obtain r1 where "a1 = Inr r1 \<and> \<phi> r1 r2" by (cases a1, auto)
   7.265 +    thus "\<exists> r1. Inr r1 \<in> A1 \<and> \<phi> r1 r2" using a1 by auto
   7.266 +  qed
   7.267 +next
   7.268 +  assume Rl: "?Rl" and Rr: "?Rr"
   7.269 +  show ?L unfolding set_rel_def Bex_def vimage_eq proof safe
   7.270 +    fix a1 assume a1: "a1 \<in> A1"
   7.271 +    show "\<exists> a2. a2 \<in> A2 \<and> sum_rel \<chi> \<phi> a1 a2"
   7.272 +    proof(cases a1)
   7.273 +      case (Inl l1) then obtain l2 where "Inl l2 \<in> A2 \<and> \<chi> l1 l2"
   7.274 +      using Rl a1 unfolding set_rel_def by blast
   7.275 +      thus ?thesis unfolding Inl by auto
   7.276 +    next
   7.277 +      case (Inr r1) then obtain r2 where "Inr r2 \<in> A2 \<and> \<phi> r1 r2"
   7.278 +      using Rr a1 unfolding set_rel_def by blast
   7.279 +      thus ?thesis unfolding Inr by auto
   7.280 +    qed
   7.281 +  next
   7.282 +    fix a2 assume a2: "a2 \<in> A2"
   7.283 +    show "\<exists> a1. a1 \<in> A1 \<and> sum_rel \<chi> \<phi> a1 a2"
   7.284 +    proof(cases a2)
   7.285 +      case (Inl l2) then obtain l1 where "Inl l1 \<in> A1 \<and> \<chi> l1 l2"
   7.286 +      using Rl a2 unfolding set_rel_def by blast
   7.287 +      thus ?thesis unfolding Inl by auto
   7.288 +    next
   7.289 +      case (Inr r2) then obtain r1 where "Inr r1 \<in> A1 \<and> \<phi> r1 r2"
   7.290 +      using Rr a2 unfolding set_rel_def by blast
   7.291 +      thus ?thesis unfolding Inr by auto
   7.292 +    qed
   7.293 +  qed
   7.294 +qed
   7.295 +
   7.296 +end
     8.1 --- a/src/HOL/Library/Library.thy	Thu Jan 23 19:02:22 2014 +0100
     8.2 +++ b/src/HOL/Library/Library.thy	Fri Jan 24 11:51:45 2014 +0100
     8.3 @@ -38,7 +38,6 @@
     8.4    Kleene_Algebra
     8.5    Mapping
     8.6    Monad_Syntax
     8.7 -  More_BNFs
     8.8    Multiset
     8.9    Numeral_Type
    8.10    OptionalSugar
     9.1 --- a/src/HOL/Library/More_BNFs.thy	Thu Jan 23 19:02:22 2014 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,1050 +0,0 @@
     9.4 -(*  Title:      HOL/Library/More_BNFs.thy
     9.5 -    Author:     Dmitriy Traytel, TU Muenchen
     9.6 -    Author:     Andrei Popescu, TU Muenchen
     9.7 -    Author:     Andreas Lochbihler, Karlsruhe Institute of Technology
     9.8 -    Author:     Jasmin Blanchette, TU Muenchen
     9.9 -    Copyright   2012
    9.10 -
    9.11 -Registration of various types as bounded natural functors.
    9.12 -*)
    9.13 -
    9.14 -header {* Registration of Various Types as Bounded Natural Functors *}
    9.15 -
    9.16 -theory More_BNFs
    9.17 -imports FSet Multiset Cardinal_Notations
    9.18 -begin
    9.19 -
    9.20 -abbreviation "Grp \<equiv> BNF_Util.Grp"
    9.21 -abbreviation "fstOp \<equiv> BNF_Def.fstOp"
    9.22 -abbreviation "sndOp \<equiv> BNF_Def.sndOp"
    9.23 -
    9.24 -lemma option_rec_conv_option_case: "option_rec = option_case"
    9.25 -by (simp add: fun_eq_iff split: option.split)
    9.26 -
    9.27 -bnf "'a option"
    9.28 -  map: Option.map
    9.29 -  sets: Option.set
    9.30 -  bd: natLeq 
    9.31 -  wits: None
    9.32 -  rel: option_rel
    9.33 -proof -
    9.34 -  show "Option.map id = id" by (simp add: fun_eq_iff Option.map_def split: option.split)
    9.35 -next
    9.36 -  fix f g
    9.37 -  show "Option.map (g \<circ> f) = Option.map g \<circ> Option.map f"
    9.38 -    by (auto simp add: fun_eq_iff Option.map_def split: option.split)
    9.39 -next
    9.40 -  fix f g x
    9.41 -  assume "\<And>z. z \<in> Option.set x \<Longrightarrow> f z = g z"
    9.42 -  thus "Option.map f x = Option.map g x"
    9.43 -    by (simp cong: Option.map_cong)
    9.44 -next
    9.45 -  fix f
    9.46 -  show "Option.set \<circ> Option.map f = op ` f \<circ> Option.set"
    9.47 -    by fastforce
    9.48 -next
    9.49 -  show "card_order natLeq" by (rule natLeq_card_order)
    9.50 -next
    9.51 -  show "cinfinite natLeq" by (rule natLeq_cinfinite)
    9.52 -next
    9.53 -  fix x
    9.54 -  show "|Option.set x| \<le>o natLeq"
    9.55 -    by (cases x) (simp_all add: ordLess_imp_ordLeq finite_iff_ordLess_natLeq[symmetric])
    9.56 -next
    9.57 -  fix R S
    9.58 -  show "option_rel R OO option_rel S \<le> option_rel (R OO S)"
    9.59 -    by (auto simp: option_rel_def split: option.splits)
    9.60 -next
    9.61 -  fix z
    9.62 -  assume "z \<in> Option.set None"
    9.63 -  thus False by simp
    9.64 -next
    9.65 -  fix R
    9.66 -  show "option_rel R =
    9.67 -        (Grp {x. Option.set x \<subseteq> Collect (split R)} (Option.map fst))\<inverse>\<inverse> OO
    9.68 -         Grp {x. Option.set x \<subseteq> Collect (split R)} (Option.map snd)"
    9.69 -  unfolding option_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff prod.cases
    9.70 -  by (auto simp: trans[OF eq_commute option_map_is_None] trans[OF eq_commute option_map_eq_Some]
    9.71 -           split: option.splits)
    9.72 -qed
    9.73 -
    9.74 -bnf "'a list"
    9.75 -  map: map
    9.76 -  sets: set
    9.77 -  bd: natLeq
    9.78 -  wits: Nil
    9.79 -  rel: list_all2
    9.80 -proof -
    9.81 -  show "map id = id" by (rule List.map.id)
    9.82 -next
    9.83 -  fix f g
    9.84 -  show "map (g o f) = map g o map f" by (rule List.map.comp[symmetric])
    9.85 -next
    9.86 -  fix x f g
    9.87 -  assume "\<And>z. z \<in> set x \<Longrightarrow> f z = g z"
    9.88 -  thus "map f x = map g x" by simp
    9.89 -next
    9.90 -  fix f
    9.91 -  show "set o map f = image f o set" by (rule ext, unfold comp_apply, rule set_map)
    9.92 -next
    9.93 -  show "card_order natLeq" by (rule natLeq_card_order)
    9.94 -next
    9.95 -  show "cinfinite natLeq" by (rule natLeq_cinfinite)
    9.96 -next
    9.97 -  fix x
    9.98 -  show "|set x| \<le>o natLeq"
    9.99 -    by (metis List.finite_set finite_iff_ordLess_natLeq ordLess_imp_ordLeq)
   9.100 -next
   9.101 -  fix R S
   9.102 -  show "list_all2 R OO list_all2 S \<le> list_all2 (R OO S)"
   9.103 -    by (metis list_all2_OO order_refl)
   9.104 -next
   9.105 -  fix R
   9.106 -  show "list_all2 R =
   9.107 -         (Grp {x. set x \<subseteq> {(x, y). R x y}} (map fst))\<inverse>\<inverse> OO
   9.108 -         Grp {x. set x \<subseteq> {(x, y). R x y}} (map snd)"
   9.109 -    unfolding list_all2_def[abs_def] Grp_def fun_eq_iff relcompp.simps conversep.simps
   9.110 -    by (force simp: zip_map_fst_snd)
   9.111 -qed simp_all
   9.112 -
   9.113 -
   9.114 -(* Finite sets *)
   9.115 -
   9.116 -context
   9.117 -includes fset.lifting
   9.118 -begin
   9.119 -
   9.120 -lemma fset_rel_alt: "fset_rel R a b \<longleftrightarrow> (\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and>
   9.121 -                                        (\<forall>t \<in> fset b. \<exists>u \<in> fset a. R u t)"
   9.122 -  by transfer (simp add: set_rel_def)
   9.123 -
   9.124 -lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A"
   9.125 -  apply (rule f_the_inv_into_f[unfolded inj_on_def])
   9.126 -  apply (simp add: fset_inject) apply (rule range_eqI Abs_fset_inverse[symmetric] CollectI)+
   9.127 -  .
   9.128 -
   9.129 -lemma fset_rel_aux:
   9.130 -"(\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and> (\<forall>u \<in> fset b. \<exists>t \<in> fset a. R t u) \<longleftrightarrow>
   9.131 - ((Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage fst))\<inverse>\<inverse> OO
   9.132 -  Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage snd)) a b" (is "?L = ?R")
   9.133 -proof
   9.134 -  assume ?L
   9.135 -  def R' \<equiv> "the_inv fset (Collect (split R) \<inter> (fset a \<times> fset b))" (is "the_inv fset ?L'")
   9.136 -  have "finite ?L'" by (intro finite_Int[OF disjI2] finite_cartesian_product) (transfer, simp)+
   9.137 -  hence *: "fset R' = ?L'" unfolding R'_def by (intro fset_to_fset)
   9.138 -  show ?R unfolding Grp_def relcompp.simps conversep.simps
   9.139 -  proof (intro CollectI prod_caseI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
   9.140 -    from * show "a = fimage fst R'" using conjunct1[OF `?L`]
   9.141 -      by (transfer, auto simp add: image_def Int_def split: prod.splits)
   9.142 -    from * show "b = fimage snd R'" using conjunct2[OF `?L`]
   9.143 -      by (transfer, auto simp add: image_def Int_def split: prod.splits)
   9.144 -  qed (auto simp add: *)
   9.145 -next
   9.146 -  assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps
   9.147 -  apply (simp add: subset_eq Ball_def)
   9.148 -  apply (rule conjI)
   9.149 -  apply (transfer, clarsimp, metis snd_conv)
   9.150 -  by (transfer, clarsimp, metis fst_conv)
   9.151 -qed
   9.152 -
   9.153 -bnf "'a fset"
   9.154 -  map: fimage
   9.155 -  sets: fset 
   9.156 -  bd: natLeq
   9.157 -  wits: "{||}"
   9.158 -  rel: fset_rel
   9.159 -apply -
   9.160 -          apply transfer' apply simp
   9.161 -         apply transfer' apply force
   9.162 -        apply transfer apply force
   9.163 -       apply transfer' apply force
   9.164 -      apply (rule natLeq_card_order)
   9.165 -     apply (rule natLeq_cinfinite)
   9.166 -    apply transfer apply (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq)
   9.167 -   apply (fastforce simp: fset_rel_alt)
   9.168 - apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff fset_rel_alt fset_rel_aux) 
   9.169 -apply transfer apply simp
   9.170 -done
   9.171 -
   9.172 -lemma fset_rel_fset: "set_rel \<chi> (fset A1) (fset A2) = fset_rel \<chi> A1 A2"
   9.173 -  by transfer (rule refl)
   9.174 -
   9.175 -end
   9.176 -
   9.177 -lemmas [simp] = fset.map_comp fset.map_id fset.set_map
   9.178 -
   9.179 -
   9.180 -(* Multisets *)
   9.181 -
   9.182 -lemma setsum_gt_0_iff:
   9.183 -fixes f :: "'a \<Rightarrow> nat" assumes "finite A"
   9.184 -shows "setsum f A > 0 \<longleftrightarrow> (\<exists> a \<in> A. f a > 0)"
   9.185 -(is "?L \<longleftrightarrow> ?R")
   9.186 -proof-
   9.187 -  have "?L \<longleftrightarrow> \<not> setsum f A = 0" by fast
   9.188 -  also have "... \<longleftrightarrow> (\<exists> a \<in> A. f a \<noteq> 0)" using assms by simp
   9.189 -  also have "... \<longleftrightarrow> ?R" by simp
   9.190 -  finally show ?thesis .
   9.191 -qed
   9.192 -
   9.193 -lift_definition mmap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" is
   9.194 -  "\<lambda>h f b. setsum f {a. h a = b \<and> f a > 0} :: nat"
   9.195 -unfolding multiset_def proof safe
   9.196 -  fix h :: "'a \<Rightarrow> 'b" and f :: "'a \<Rightarrow> nat"
   9.197 -  assume fin: "finite {a. 0 < f a}"  (is "finite ?A")
   9.198 -  show "finite {b. 0 < setsum f {a. h a = b \<and> 0 < f a}}"
   9.199 -  (is "finite {b. 0 < setsum f (?As b)}")
   9.200 -  proof- let ?B = "{b. 0 < setsum f (?As b)}"
   9.201 -    have "\<And> b. finite (?As b)" using fin by simp
   9.202 -    hence B: "?B = {b. ?As b \<noteq> {}}" by (auto simp add: setsum_gt_0_iff)
   9.203 -    hence "?B \<subseteq> h ` ?A" by auto
   9.204 -    thus ?thesis using finite_surj[OF fin] by auto
   9.205 -  qed
   9.206 -qed
   9.207 -
   9.208 -lemma mmap_id0: "mmap id = id"
   9.209 -proof (intro ext multiset_eqI)
   9.210 -  fix f a show "count (mmap id f) a = count (id f) a"
   9.211 -  proof (cases "count f a = 0")
   9.212 -    case False
   9.213 -    hence 1: "{aa. aa = a \<and> aa \<in># f} = {a}" by auto
   9.214 -    thus ?thesis by transfer auto
   9.215 -  qed (transfer, simp)
   9.216 -qed
   9.217 -
   9.218 -lemma inj_on_setsum_inv:
   9.219 -assumes 1: "(0::nat) < setsum (count f) {a. h a = b' \<and> a \<in># f}" (is "0 < setsum (count f) ?A'")
   9.220 -and     2: "{a. h a = b \<and> a \<in># f} = {a. h a = b' \<and> a \<in># f}" (is "?A = ?A'")
   9.221 -shows "b = b'"
   9.222 -using assms by (auto simp add: setsum_gt_0_iff)
   9.223 -
   9.224 -lemma mmap_comp:
   9.225 -fixes h1 :: "'a \<Rightarrow> 'b" and h2 :: "'b \<Rightarrow> 'c"
   9.226 -shows "mmap (h2 o h1) = mmap h2 o mmap h1"
   9.227 -proof (intro ext multiset_eqI)
   9.228 -  fix f :: "'a multiset" fix c :: 'c
   9.229 -  let ?A = "{a. h2 (h1 a) = c \<and> a \<in># f}"
   9.230 -  let ?As = "\<lambda> b. {a. h1 a = b \<and> a \<in># f}"
   9.231 -  let ?B = "{b. h2 b = c \<and> 0 < setsum (count f) (?As b)}"
   9.232 -  have 0: "{?As b | b.  b \<in> ?B} = ?As ` ?B" by auto
   9.233 -  have "\<And> b. finite (?As b)" by transfer (simp add: multiset_def)
   9.234 -  hence "?B = {b. h2 b = c \<and> ?As b \<noteq> {}}" by (auto simp add: setsum_gt_0_iff)
   9.235 -  hence A: "?A = \<Union> {?As b | b.  b \<in> ?B}" by auto
   9.236 -  have "setsum (count f) ?A = setsum (setsum (count f)) {?As b | b.  b \<in> ?B}"
   9.237 -    unfolding A by transfer (intro setsum_Union_disjoint, auto simp: multiset_def)
   9.238 -  also have "... = setsum (setsum (count f)) (?As ` ?B)" unfolding 0 ..
   9.239 -  also have "... = setsum (setsum (count f) o ?As) ?B"
   9.240 -    by(intro setsum_reindex) (auto simp add: setsum_gt_0_iff inj_on_def)
   9.241 -  also have "... = setsum (\<lambda> b. setsum (count f) (?As b)) ?B" unfolding comp_def ..
   9.242 -  finally have "setsum (count f) ?A = setsum (\<lambda> b. setsum (count f) (?As b)) ?B" .
   9.243 -  thus "count (mmap (h2 \<circ> h1) f) c = count ((mmap h2 \<circ> mmap h1) f) c"
   9.244 -    by transfer (unfold comp_apply, blast)
   9.245 -qed
   9.246 -
   9.247 -lemma mmap_cong:
   9.248 -assumes "\<And>a. a \<in># M \<Longrightarrow> f a = g a"
   9.249 -shows "mmap f M = mmap g M"
   9.250 -using assms by transfer (auto intro!: setsum_cong)
   9.251 -
   9.252 -context
   9.253 -begin
   9.254 -interpretation lifting_syntax .
   9.255 -
   9.256 -lemma set_of_transfer[transfer_rule]: "(pcr_multiset op = ===> op =) (\<lambda>f. {a. 0 < f a}) set_of"
   9.257 -  unfolding set_of_def pcr_multiset_def cr_multiset_def fun_rel_def by auto
   9.258 -
   9.259 -end
   9.260 -
   9.261 -lemma set_of_mmap: "set_of o mmap h = image h o set_of"
   9.262 -proof (rule ext, unfold comp_apply)
   9.263 -  fix M show "set_of (mmap h M) = h ` set_of M"
   9.264 -    by transfer (auto simp add: multiset_def setsum_gt_0_iff)
   9.265 -qed
   9.266 -
   9.267 -lemma multiset_of_surj:
   9.268 -  "multiset_of ` {as. set as \<subseteq> A} = {M. set_of M \<subseteq> A}"
   9.269 -proof safe
   9.270 -  fix M assume M: "set_of M \<subseteq> A"
   9.271 -  obtain as where eq: "M = multiset_of as" using surj_multiset_of unfolding surj_def by auto
   9.272 -  hence "set as \<subseteq> A" using M by auto
   9.273 -  thus "M \<in> multiset_of ` {as. set as \<subseteq> A}" using eq by auto
   9.274 -next
   9.275 -  show "\<And>x xa xb. \<lbrakk>set xa \<subseteq> A; xb \<in> set_of (multiset_of xa)\<rbrakk> \<Longrightarrow> xb \<in> A"
   9.276 -  by (erule set_mp) (unfold set_of_multiset_of)
   9.277 -qed
   9.278 -
   9.279 -lemma card_of_set_of:
   9.280 -"|{M. set_of M \<subseteq> A}| \<le>o |{as. set as \<subseteq> A}|"
   9.281 -apply(rule card_of_ordLeqI2[of _ multiset_of]) using multiset_of_surj by auto
   9.282 -
   9.283 -lemma nat_sum_induct:
   9.284 -assumes "\<And>n1 n2. (\<And> m1 m2. m1 + m2 < n1 + n2 \<Longrightarrow> phi m1 m2) \<Longrightarrow> phi n1 n2"
   9.285 -shows "phi (n1::nat) (n2::nat)"
   9.286 -proof-
   9.287 -  let ?chi = "\<lambda> n1n2 :: nat * nat. phi (fst n1n2) (snd n1n2)"
   9.288 -  have "?chi (n1,n2)"
   9.289 -  apply(induct rule: measure_induct[of "\<lambda> n1n2. fst n1n2 + snd n1n2" ?chi])
   9.290 -  using assms by (metis fstI sndI)
   9.291 -  thus ?thesis by simp
   9.292 -qed
   9.293 -
   9.294 -lemma matrix_count:
   9.295 -fixes ct1 ct2 :: "nat \<Rightarrow> nat"
   9.296 -assumes "setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2}"
   9.297 -shows
   9.298 -"\<exists> ct. (\<forall> i1 \<le> n1. setsum (\<lambda> i2. ct i1 i2) {..<Suc n2} = ct1 i1) \<and>
   9.299 -       (\<forall> i2 \<le> n2. setsum (\<lambda> i1. ct i1 i2) {..<Suc n1} = ct2 i2)"
   9.300 -(is "?phi ct1 ct2 n1 n2")
   9.301 -proof-
   9.302 -  have "\<forall> ct1 ct2 :: nat \<Rightarrow> nat.
   9.303 -        setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2} \<longrightarrow> ?phi ct1 ct2 n1 n2"
   9.304 -  proof(induct rule: nat_sum_induct[of
   9.305 -"\<lambda> n1 n2. \<forall> ct1 ct2 :: nat \<Rightarrow> nat.
   9.306 -     setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2} \<longrightarrow> ?phi ct1 ct2 n1 n2"],
   9.307 -      clarify)
   9.308 -  fix n1 n2 :: nat and ct1 ct2 :: "nat \<Rightarrow> nat"
   9.309 -  assume IH: "\<And> m1 m2. m1 + m2 < n1 + n2 \<Longrightarrow>
   9.310 -                \<forall> dt1 dt2 :: nat \<Rightarrow> nat.
   9.311 -                setsum dt1 {..<Suc m1} = setsum dt2 {..<Suc m2} \<longrightarrow> ?phi dt1 dt2 m1 m2"
   9.312 -  and ss: "setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2}"
   9.313 -  show "?phi ct1 ct2 n1 n2"
   9.314 -  proof(cases n1)
   9.315 -    case 0 note n1 = 0
   9.316 -    show ?thesis
   9.317 -    proof(cases n2)
   9.318 -      case 0 note n2 = 0
   9.319 -      let ?ct = "\<lambda> i1 i2. ct2 0"
   9.320 -      show ?thesis apply(rule exI[of _ ?ct]) using n1 n2 ss by simp
   9.321 -    next
   9.322 -      case (Suc m2) note n2 = Suc
   9.323 -      let ?ct = "\<lambda> i1 i2. ct2 i2"
   9.324 -      show ?thesis apply(rule exI[of _ ?ct]) using n1 n2 ss by auto
   9.325 -    qed
   9.326 -  next
   9.327 -    case (Suc m1) note n1 = Suc
   9.328 -    show ?thesis
   9.329 -    proof(cases n2)
   9.330 -      case 0 note n2 = 0
   9.331 -      let ?ct = "\<lambda> i1 i2. ct1 i1"
   9.332 -      show ?thesis apply(rule exI[of _ ?ct]) using n1 n2 ss by auto
   9.333 -    next
   9.334 -      case (Suc m2) note n2 = Suc
   9.335 -      show ?thesis
   9.336 -      proof(cases "ct1 n1 \<le> ct2 n2")
   9.337 -        case True
   9.338 -        def dt2 \<equiv> "\<lambda> i2. if i2 = n2 then ct2 i2 - ct1 n1 else ct2 i2"
   9.339 -        have "setsum ct1 {..<Suc m1} = setsum dt2 {..<Suc n2}"
   9.340 -        unfolding dt2_def using ss n1 True by auto
   9.341 -        hence "?phi ct1 dt2 m1 n2" using IH[of m1 n2] n1 by simp
   9.342 -        then obtain dt where
   9.343 -        1: "\<And> i1. i1 \<le> m1 \<Longrightarrow> setsum (\<lambda> i2. dt i1 i2) {..<Suc n2} = ct1 i1" and
   9.344 -        2: "\<And> i2. i2 \<le> n2 \<Longrightarrow> setsum (\<lambda> i1. dt i1 i2) {..<Suc m1} = dt2 i2" by auto
   9.345 -        let ?ct = "\<lambda> i1 i2. if i1 = n1 then (if i2 = n2 then ct1 n1 else 0)
   9.346 -                                       else dt i1 i2"
   9.347 -        show ?thesis apply(rule exI[of _ ?ct])
   9.348 -        using n1 n2 1 2 True unfolding dt2_def by simp
   9.349 -      next
   9.350 -        case False
   9.351 -        hence False: "ct2 n2 < ct1 n1" by simp
   9.352 -        def dt1 \<equiv> "\<lambda> i1. if i1 = n1 then ct1 i1 - ct2 n2 else ct1 i1"
   9.353 -        have "setsum dt1 {..<Suc n1} = setsum ct2 {..<Suc m2}"
   9.354 -        unfolding dt1_def using ss n2 False by auto
   9.355 -        hence "?phi dt1 ct2 n1 m2" using IH[of n1 m2] n2 by simp
   9.356 -        then obtain dt where
   9.357 -        1: "\<And> i1. i1 \<le> n1 \<Longrightarrow> setsum (\<lambda> i2. dt i1 i2) {..<Suc m2} = dt1 i1" and
   9.358 -        2: "\<And> i2. i2 \<le> m2 \<Longrightarrow> setsum (\<lambda> i1. dt i1 i2) {..<Suc n1} = ct2 i2" by force
   9.359 -        let ?ct = "\<lambda> i1 i2. if i2 = n2 then (if i1 = n1 then ct2 n2 else 0)
   9.360 -                                       else dt i1 i2"
   9.361 -        show ?thesis apply(rule exI[of _ ?ct])
   9.362 -        using n1 n2 1 2 False unfolding dt1_def by simp
   9.363 -      qed
   9.364 -    qed
   9.365 -  qed
   9.366 -  qed
   9.367 -  thus ?thesis using assms by auto
   9.368 -qed
   9.369 -
   9.370 -definition
   9.371 -"inj2 u B1 B2 \<equiv>
   9.372 - \<forall> b1 b1' b2 b2'. {b1,b1'} \<subseteq> B1 \<and> {b2,b2'} \<subseteq> B2 \<and> u b1 b2 = u b1' b2'
   9.373 -                  \<longrightarrow> b1 = b1' \<and> b2 = b2'"
   9.374 -
   9.375 -lemma matrix_setsum_finite:
   9.376 -assumes B1: "B1 \<noteq> {}" "finite B1" and B2: "B2 \<noteq> {}" "finite B2" and u: "inj2 u B1 B2"
   9.377 -and ss: "setsum N1 B1 = setsum N2 B2"
   9.378 -shows "\<exists> M :: 'a \<Rightarrow> nat.
   9.379 -            (\<forall> b1 \<in> B1. setsum (\<lambda> b2. M (u b1 b2)) B2 = N1 b1) \<and>
   9.380 -            (\<forall> b2 \<in> B2. setsum (\<lambda> b1. M (u b1 b2)) B1 = N2 b2)"
   9.381 -proof-
   9.382 -  obtain n1 where "card B1 = Suc n1" using B1 by (metis card_insert finite.simps)
   9.383 -  then obtain e1 where e1: "bij_betw e1 {..<Suc n1} B1"
   9.384 -  using ex_bij_betw_finite_nat[OF B1(2)] by (metis atLeast0LessThan bij_betw_the_inv_into)
   9.385 -  hence e1_inj: "inj_on e1 {..<Suc n1}" and e1_surj: "e1 ` {..<Suc n1} = B1"
   9.386 -  unfolding bij_betw_def by auto
   9.387 -  def f1 \<equiv> "inv_into {..<Suc n1} e1"
   9.388 -  have f1: "bij_betw f1 B1 {..<Suc n1}"
   9.389 -  and f1e1[simp]: "\<And> i1. i1 < Suc n1 \<Longrightarrow> f1 (e1 i1) = i1"
   9.390 -  and e1f1[simp]: "\<And> b1. b1 \<in> B1 \<Longrightarrow> e1 (f1 b1) = b1" unfolding f1_def
   9.391 -  apply (metis bij_betw_inv_into e1, metis bij_betw_inv_into_left e1 lessThan_iff)
   9.392 -  by (metis e1_surj f_inv_into_f)
   9.393 -  (*  *)
   9.394 -  obtain n2 where "card B2 = Suc n2" using B2 by (metis card_insert finite.simps)
   9.395 -  then obtain e2 where e2: "bij_betw e2 {..<Suc n2} B2"
   9.396 -  using ex_bij_betw_finite_nat[OF B2(2)] by (metis atLeast0LessThan bij_betw_the_inv_into)
   9.397 -  hence e2_inj: "inj_on e2 {..<Suc n2}" and e2_surj: "e2 ` {..<Suc n2} = B2"
   9.398 -  unfolding bij_betw_def by auto
   9.399 -  def f2 \<equiv> "inv_into {..<Suc n2} e2"
   9.400 -  have f2: "bij_betw f2 B2 {..<Suc n2}"
   9.401 -  and f2e2[simp]: "\<And> i2. i2 < Suc n2 \<Longrightarrow> f2 (e2 i2) = i2"
   9.402 -  and e2f2[simp]: "\<And> b2. b2 \<in> B2 \<Longrightarrow> e2 (f2 b2) = b2" unfolding f2_def
   9.403 -  apply (metis bij_betw_inv_into e2, metis bij_betw_inv_into_left e2 lessThan_iff)
   9.404 -  by (metis e2_surj f_inv_into_f)
   9.405 -  (*  *)
   9.406 -  let ?ct1 = "N1 o e1"  let ?ct2 = "N2 o e2"
   9.407 -  have ss: "setsum ?ct1 {..<Suc n1} = setsum ?ct2 {..<Suc n2}"
   9.408 -  unfolding setsum_reindex[OF e1_inj, symmetric] setsum_reindex[OF e2_inj, symmetric]
   9.409 -  e1_surj e2_surj using ss .
   9.410 -  obtain ct where
   9.411 -  ct1: "\<And> i1. i1 \<le> n1 \<Longrightarrow> setsum (\<lambda> i2. ct i1 i2) {..<Suc n2} = ?ct1 i1" and
   9.412 -  ct2: "\<And> i2. i2 \<le> n2 \<Longrightarrow> setsum (\<lambda> i1. ct i1 i2) {..<Suc n1} = ?ct2 i2"
   9.413 -  using matrix_count[OF ss] by blast
   9.414 -  (*  *)
   9.415 -  def A \<equiv> "{u b1 b2 | b1 b2. b1 \<in> B1 \<and> b2 \<in> B2}"
   9.416 -  have "\<forall> a \<in> A. \<exists> b1b2 \<in> B1 <*> B2. u (fst b1b2) (snd b1b2) = a"
   9.417 -  unfolding A_def Ball_def mem_Collect_eq by auto
   9.418 -  then obtain h1h2 where h12:
   9.419 -  "\<And>a. a \<in> A \<Longrightarrow> u (fst (h1h2 a)) (snd (h1h2 a)) = a \<and> h1h2 a \<in> B1 <*> B2" by metis
   9.420 -  def h1 \<equiv> "fst o h1h2"  def h2 \<equiv> "snd o h1h2"
   9.421 -  have h12[simp]: "\<And>a. a \<in> A \<Longrightarrow> u (h1 a) (h2 a) = a"
   9.422 -                  "\<And> a. a \<in> A \<Longrightarrow> h1 a \<in> B1"  "\<And> a. a \<in> A \<Longrightarrow> h2 a \<in> B2"
   9.423 -  using h12 unfolding h1_def h2_def by force+
   9.424 -  {fix b1 b2 assume b1: "b1 \<in> B1" and b2: "b2 \<in> B2"
   9.425 -   hence inA: "u b1 b2 \<in> A" unfolding A_def by auto
   9.426 -   hence "u b1 b2 = u (h1 (u b1 b2)) (h2 (u b1 b2))" by auto
   9.427 -   moreover have "h1 (u b1 b2) \<in> B1" "h2 (u b1 b2) \<in> B2" using inA by auto
   9.428 -   ultimately have "h1 (u b1 b2) = b1 \<and> h2 (u b1 b2) = b2"
   9.429 -   using u b1 b2 unfolding inj2_def by fastforce
   9.430 -  }
   9.431 -  hence h1[simp]: "\<And> b1 b2. \<lbrakk>b1 \<in> B1; b2 \<in> B2\<rbrakk> \<Longrightarrow> h1 (u b1 b2) = b1" and
   9.432 -        h2[simp]: "\<And> b1 b2. \<lbrakk>b1 \<in> B1; b2 \<in> B2\<rbrakk> \<Longrightarrow> h2 (u b1 b2) = b2" by auto
   9.433 -  def M \<equiv> "\<lambda> a. ct (f1 (h1 a)) (f2 (h2 a))"
   9.434 -  show ?thesis
   9.435 -  apply(rule exI[of _ M]) proof safe
   9.436 -    fix b1 assume b1: "b1 \<in> B1"
   9.437 -    hence f1b1: "f1 b1 \<le> n1" using f1 unfolding bij_betw_def
   9.438 -    by (metis image_eqI lessThan_iff less_Suc_eq_le)
   9.439 -    have "(\<Sum>b2\<in>B2. M (u b1 b2)) = (\<Sum>i2<Suc n2. ct (f1 b1) (f2 (e2 i2)))"
   9.440 -    unfolding e2_surj[symmetric] setsum_reindex[OF e2_inj]
   9.441 -    unfolding M_def comp_def apply(intro setsum_cong) apply force
   9.442 -    by (metis e2_surj b1 h1 h2 imageI)
   9.443 -    also have "... = N1 b1" using b1 ct1[OF f1b1] by simp
   9.444 -    finally show "(\<Sum>b2\<in>B2. M (u b1 b2)) = N1 b1" .
   9.445 -  next
   9.446 -    fix b2 assume b2: "b2 \<in> B2"
   9.447 -    hence f2b2: "f2 b2 \<le> n2" using f2 unfolding bij_betw_def
   9.448 -    by (metis image_eqI lessThan_iff less_Suc_eq_le)
   9.449 -    have "(\<Sum>b1\<in>B1. M (u b1 b2)) = (\<Sum>i1<Suc n1. ct (f1 (e1 i1)) (f2 b2))"
   9.450 -    unfolding e1_surj[symmetric] setsum_reindex[OF e1_inj]
   9.451 -    unfolding M_def comp_def apply(intro setsum_cong) apply force
   9.452 -    by (metis e1_surj b2 h1 h2 imageI)
   9.453 -    also have "... = N2 b2" using b2 ct2[OF f2b2] by simp
   9.454 -    finally show "(\<Sum>b1\<in>B1. M (u b1 b2)) = N2 b2" .
   9.455 -  qed
   9.456 -qed
   9.457 -
   9.458 -lemma supp_vimage_mmap: "set_of M \<subseteq> f -` (set_of (mmap f M))"
   9.459 -  by transfer (auto simp: multiset_def setsum_gt_0_iff)
   9.460 -
   9.461 -lemma mmap_ge_0: "b \<in># mmap f M \<longleftrightarrow> (\<exists>a. a \<in># M \<and> f a = b)"
   9.462 -  by transfer (auto simp: multiset_def setsum_gt_0_iff)
   9.463 -
   9.464 -lemma finite_twosets:
   9.465 -assumes "finite B1" and "finite B2"
   9.466 -shows "finite {u b1 b2 |b1 b2. b1 \<in> B1 \<and> b2 \<in> B2}"  (is "finite ?A")
   9.467 -proof-
   9.468 -  have A: "?A = (\<lambda> b1b2. u (fst b1b2) (snd b1b2)) ` (B1 <*> B2)" by force
   9.469 -  show ?thesis unfolding A using finite_cartesian_product[OF assms] by auto
   9.470 -qed
   9.471 -
   9.472 -(* Weak pullbacks: *)
   9.473 -definition wpull where
   9.474 -"wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow>
   9.475 - (\<forall> b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<longrightarrow> (\<exists> a \<in> A. p1 a = b1 \<and> p2 a = b2))"
   9.476 -
   9.477 -(* Weak pseudo-pullbacks *)
   9.478 -definition wppull where
   9.479 -"wppull A B1 B2 f1 f2 e1 e2 p1 p2 \<longleftrightarrow>
   9.480 - (\<forall> b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<longrightarrow>
   9.481 -           (\<exists> a \<in> A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2))"
   9.482 -
   9.483 -
   9.484 -(* The pullback of sets *)
   9.485 -definition thePull where
   9.486 -"thePull B1 B2 f1 f2 = {(b1,b2). b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2}"
   9.487 -
   9.488 -lemma wpull_thePull:
   9.489 -"wpull (thePull B1 B2 f1 f2) B1 B2 f1 f2 fst snd"
   9.490 -unfolding wpull_def thePull_def by auto
   9.491 -
   9.492 -lemma wppull_thePull:
   9.493 -assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
   9.494 -shows
   9.495 -"\<exists> j. \<forall> a' \<in> thePull B1 B2 f1 f2.
   9.496 -   j a' \<in> A \<and>
   9.497 -   e1 (p1 (j a')) = e1 (fst a') \<and> e2 (p2 (j a')) = e2 (snd a')"
   9.498 -(is "\<exists> j. \<forall> a' \<in> ?A'. ?phi a' (j a')")
   9.499 -proof(rule bchoice[of ?A' ?phi], default)
   9.500 -  fix a' assume a': "a' \<in> ?A'"
   9.501 -  hence "fst a' \<in> B1" unfolding thePull_def by auto
   9.502 -  moreover
   9.503 -  from a' have "snd a' \<in> B2" unfolding thePull_def by auto
   9.504 -  moreover have "f1 (fst a') = f2 (snd a')"
   9.505 -  using a' unfolding csquare_def thePull_def by auto
   9.506 -  ultimately show "\<exists> ja'. ?phi a' ja'"
   9.507 -  using assms unfolding wppull_def by blast
   9.508 -qed
   9.509 -
   9.510 -lemma wpull_wppull:
   9.511 -assumes wp: "wpull A' B1 B2 f1 f2 p1' p2'" and
   9.512 -1: "\<forall> a' \<in> A'. j a' \<in> A \<and> e1 (p1 (j a')) = e1 (p1' a') \<and> e2 (p2 (j a')) = e2 (p2' a')"
   9.513 -shows "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
   9.514 -unfolding wppull_def proof safe
   9.515 -  fix b1 b2
   9.516 -  assume b1: "b1 \<in> B1" and b2: "b2 \<in> B2" and f: "f1 b1 = f2 b2"
   9.517 -  then obtain a' where a': "a' \<in> A'" and b1: "b1 = p1' a'" and b2: "b2 = p2' a'"
   9.518 -  using wp unfolding wpull_def by blast
   9.519 -  show "\<exists>a\<in>A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2"
   9.520 -  apply (rule bexI[of _ "j a'"]) unfolding b1 b2 using a' 1 by auto
   9.521 -qed
   9.522 -
   9.523 -lemma wppull_fstOp_sndOp:
   9.524 -shows "wppull (Collect (split (P OO Q))) (Collect (split P)) (Collect (split Q))
   9.525 -  snd fst fst snd (fstOp P Q) (sndOp P Q)"
   9.526 -using pick_middlep unfolding wppull_def fstOp_def sndOp_def relcompp.simps by auto
   9.527 -
   9.528 -lemma wpull_mmap:
   9.529 -fixes A :: "'a set" and B1 :: "'b1 set" and B2 :: "'b2 set"
   9.530 -assumes wp: "wpull A B1 B2 f1 f2 p1 p2"
   9.531 -shows
   9.532 -"wpull {M. set_of M \<subseteq> A}
   9.533 -       {N1. set_of N1 \<subseteq> B1} {N2. set_of N2 \<subseteq> B2}
   9.534 -       (mmap f1) (mmap f2) (mmap p1) (mmap p2)"
   9.535 -unfolding wpull_def proof (safe, unfold Bex_def mem_Collect_eq)
   9.536 -  fix N1 :: "'b1 multiset" and N2 :: "'b2 multiset"
   9.537 -  assume mmap': "mmap f1 N1 = mmap f2 N2"
   9.538 -  and N1[simp]: "set_of N1 \<subseteq> B1"
   9.539 -  and N2[simp]: "set_of N2 \<subseteq> B2"
   9.540 -  def P \<equiv> "mmap f1 N1"
   9.541 -  have P1: "P = mmap f1 N1" and P2: "P = mmap f2 N2" unfolding P_def using mmap' by auto
   9.542 -  note P = P1 P2
   9.543 -  have fin_N1[simp]: "finite (set_of N1)"
   9.544 -   and fin_N2[simp]: "finite (set_of N2)"
   9.545 -   and fin_P[simp]: "finite (set_of P)" by auto
   9.546 -  (*  *)
   9.547 -  def set1 \<equiv> "\<lambda> c. {b1 \<in> set_of N1. f1 b1 = c}"
   9.548 -  have set1[simp]: "\<And> c b1. b1 \<in> set1 c \<Longrightarrow> f1 b1 = c" unfolding set1_def by auto
   9.549 -  have fin_set1: "\<And> c. c \<in> set_of P \<Longrightarrow> finite (set1 c)"
   9.550 -    using N1(1) unfolding set1_def multiset_def by auto
   9.551 -  have set1_NE: "\<And> c. c \<in> set_of P \<Longrightarrow> set1 c \<noteq> {}"
   9.552 -   unfolding set1_def set_of_def P mmap_ge_0 by auto
   9.553 -  have supp_N1_set1: "set_of N1 = (\<Union> c \<in> set_of P. set1 c)"
   9.554 -    using supp_vimage_mmap[of N1 f1] unfolding set1_def P1 by auto
   9.555 -  hence set1_inclN1: "\<And>c. c \<in> set_of P \<Longrightarrow> set1 c \<subseteq> set_of N1" by auto
   9.556 -  hence set1_incl: "\<And> c. c \<in> set_of P \<Longrightarrow> set1 c \<subseteq> B1" using N1 by blast
   9.557 -  have set1_disj: "\<And> c c'. c \<noteq> c' \<Longrightarrow> set1 c \<inter> set1 c' = {}"
   9.558 -    unfolding set1_def by auto
   9.559 -  have setsum_set1: "\<And> c. setsum (count N1) (set1 c) = count P c"
   9.560 -    unfolding P1 set1_def by transfer (auto intro: setsum_cong)
   9.561 -  (*  *)
   9.562 -  def set2 \<equiv> "\<lambda> c. {b2 \<in> set_of N2. f2 b2 = c}"
   9.563 -  have set2[simp]: "\<And> c b2. b2 \<in> set2 c \<Longrightarrow> f2 b2 = c" unfolding set2_def by auto
   9.564 -  have fin_set2: "\<And> c. c \<in> set_of P \<Longrightarrow> finite (set2 c)"
   9.565 -  using N2(1) unfolding set2_def multiset_def by auto
   9.566 -  have set2_NE: "\<And> c. c \<in> set_of P \<Longrightarrow> set2 c \<noteq> {}"
   9.567 -    unfolding set2_def P2 mmap_ge_0 set_of_def by auto
   9.568 -  have supp_N2_set2: "set_of N2 = (\<Union> c \<in> set_of P. set2 c)"
   9.569 -    using supp_vimage_mmap[of N2 f2] unfolding set2_def P2 by auto
   9.570 -  hence set2_inclN2: "\<And>c. c \<in> set_of P \<Longrightarrow> set2 c \<subseteq> set_of N2" by auto
   9.571 -  hence set2_incl: "\<And> c. c \<in> set_of P \<Longrightarrow> set2 c \<subseteq> B2" using N2 by blast
   9.572 -  have set2_disj: "\<And> c c'. c \<noteq> c' \<Longrightarrow> set2 c \<inter> set2 c' = {}"
   9.573 -    unfolding set2_def by auto
   9.574 -  have setsum_set2: "\<And> c. setsum (count N2) (set2 c) = count P c"
   9.575 -    unfolding P2 set2_def by transfer (auto intro: setsum_cong)
   9.576 -  (*  *)
   9.577 -  have ss: "\<And> c. c \<in> set_of P \<Longrightarrow> setsum (count N1) (set1 c) = setsum (count N2) (set2 c)"
   9.578 -    unfolding setsum_set1 setsum_set2 ..
   9.579 -  have "\<forall> c \<in> set_of P. \<forall> b1b2 \<in> (set1 c) \<times> (set2 c).
   9.580 -          \<exists> a \<in> A. p1 a = fst b1b2 \<and> p2 a = snd b1b2"
   9.581 -    using wp set1_incl set2_incl unfolding wpull_def Ball_def mem_Collect_eq
   9.582 -    by simp (metis set1 set2 set_rev_mp)
   9.583 -  then obtain uu where uu:
   9.584 -  "\<forall> c \<in> set_of P. \<forall> b1b2 \<in> (set1 c) \<times> (set2 c).
   9.585 -     uu c b1b2 \<in> A \<and> p1 (uu c b1b2) = fst b1b2 \<and> p2 (uu c b1b2) = snd b1b2" by metis
   9.586 -  def u \<equiv> "\<lambda> c b1 b2. uu c (b1,b2)"
   9.587 -  have u[simp]:
   9.588 -  "\<And> c b1 b2. \<lbrakk>c \<in> set_of P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk> \<Longrightarrow> u c b1 b2 \<in> A"
   9.589 -  "\<And> c b1 b2. \<lbrakk>c \<in> set_of P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk> \<Longrightarrow> p1 (u c b1 b2) = b1"
   9.590 -  "\<And> c b1 b2. \<lbrakk>c \<in> set_of P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk> \<Longrightarrow> p2 (u c b1 b2) = b2"
   9.591 -    using uu unfolding u_def by auto
   9.592 -  {fix c assume c: "c \<in> set_of P"
   9.593 -   have "inj2 (u c) (set1 c) (set2 c)" unfolding inj2_def proof clarify
   9.594 -     fix b1 b1' b2 b2'
   9.595 -     assume "{b1, b1'} \<subseteq> set1 c" "{b2, b2'} \<subseteq> set2 c" and 0: "u c b1 b2 = u c b1' b2'"
   9.596 -     hence "p1 (u c b1 b2) = b1 \<and> p2 (u c b1 b2) = b2 \<and>
   9.597 -            p1 (u c b1' b2') = b1' \<and> p2 (u c b1' b2') = b2'"
   9.598 -     using u(2)[OF c] u(3)[OF c] by simp metis
   9.599 -     thus "b1 = b1' \<and> b2 = b2'" using 0 by auto
   9.600 -   qed
   9.601 -  } note inj = this
   9.602 -  def sset \<equiv> "\<lambda> c. {u c b1 b2 | b1 b2. b1 \<in> set1 c \<and> b2 \<in> set2 c}"
   9.603 -  have fin_sset[simp]: "\<And> c. c \<in> set_of P \<Longrightarrow> finite (sset c)" unfolding sset_def
   9.604 -    using fin_set1 fin_set2 finite_twosets by blast
   9.605 -  have sset_A: "\<And> c. c \<in> set_of P \<Longrightarrow> sset c \<subseteq> A" unfolding sset_def by auto
   9.606 -  {fix c a assume c: "c \<in> set_of P" and ac: "a \<in> sset c"
   9.607 -   then obtain b1 b2 where b1: "b1 \<in> set1 c" and b2: "b2 \<in> set2 c"
   9.608 -   and a: "a = u c b1 b2" unfolding sset_def by auto
   9.609 -   have "p1 a \<in> set1 c" and p2a: "p2 a \<in> set2 c"
   9.610 -   using ac a b1 b2 c u(2) u(3) by simp+
   9.611 -   hence "u c (p1 a) (p2 a) = a" unfolding a using b1 b2 inj[OF c]
   9.612 -   unfolding inj2_def by (metis c u(2) u(3))
   9.613 -  } note u_p12[simp] = this
   9.614 -  {fix c a assume c: "c \<in> set_of P" and ac: "a \<in> sset c"
   9.615 -   hence "p1 a \<in> set1 c" unfolding sset_def by auto
   9.616 -  }note p1[simp] = this
   9.617 -  {fix c a assume c: "c \<in> set_of P" and ac: "a \<in> sset c"
   9.618 -   hence "p2 a \<in> set2 c" unfolding sset_def by auto
   9.619 -  }note p2[simp] = this
   9.620 -  (*  *)
   9.621 -  {fix c assume c: "c \<in> set_of P"
   9.622 -   hence "\<exists> M. (\<forall> b1 \<in> set1 c. setsum (\<lambda> b2. M (u c b1 b2)) (set2 c) = count N1 b1) \<and>
   9.623 -               (\<forall> b2 \<in> set2 c. setsum (\<lambda> b1. M (u c b1 b2)) (set1 c) = count N2 b2)"
   9.624 -   unfolding sset_def
   9.625 -   using matrix_setsum_finite[OF set1_NE[OF c] fin_set1[OF c]
   9.626 -                                 set2_NE[OF c] fin_set2[OF c] inj[OF c] ss[OF c]] by auto
   9.627 -  }
   9.628 -  then obtain Ms where
   9.629 -  ss1: "\<And> c b1. \<lbrakk>c \<in> set_of P; b1 \<in> set1 c\<rbrakk> \<Longrightarrow>
   9.630 -                   setsum (\<lambda> b2. Ms c (u c b1 b2)) (set2 c) = count N1 b1" and
   9.631 -  ss2: "\<And> c b2. \<lbrakk>c \<in> set_of P; b2 \<in> set2 c\<rbrakk> \<Longrightarrow>
   9.632 -                   setsum (\<lambda> b1. Ms c (u c b1 b2)) (set1 c) = count N2 b2"
   9.633 -  by metis
   9.634 -  def SET \<equiv> "\<Union> c \<in> set_of P. sset c"
   9.635 -  have fin_SET[simp]: "finite SET" unfolding SET_def apply(rule finite_UN_I) by auto
   9.636 -  have SET_A: "SET \<subseteq> A" unfolding SET_def using sset_A by blast
   9.637 -  have u_SET[simp]: "\<And> c b1 b2. \<lbrakk>c \<in> set_of P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk> \<Longrightarrow> u c b1 b2 \<in> SET"
   9.638 -    unfolding SET_def sset_def by blast
   9.639 -  {fix c a assume c: "c \<in> set_of P" and a: "a \<in> SET" and p1a: "p1 a \<in> set1 c"
   9.640 -   then obtain c' where c': "c' \<in> set_of P" and ac': "a \<in> sset c'"
   9.641 -    unfolding SET_def by auto
   9.642 -   hence "p1 a \<in> set1 c'" unfolding sset_def by auto
   9.643 -   hence eq: "c = c'" using p1a c c' set1_disj by auto
   9.644 -   hence "a \<in> sset c" using ac' by simp
   9.645 -  } note p1_rev = this
   9.646 -  {fix c a assume c: "c \<in> set_of P" and a: "a \<in> SET" and p2a: "p2 a \<in> set2 c"
   9.647 -   then obtain c' where c': "c' \<in> set_of P" and ac': "a \<in> sset c'"
   9.648 -   unfolding SET_def by auto
   9.649 -   hence "p2 a \<in> set2 c'" unfolding sset_def by auto
   9.650 -   hence eq: "c = c'" using p2a c c' set2_disj by auto
   9.651 -   hence "a \<in> sset c" using ac' by simp
   9.652 -  } note p2_rev = this
   9.653 -  (*  *)
   9.654 -  have "\<forall> a \<in> SET. \<exists> c \<in> set_of P. a \<in> sset c" unfolding SET_def by auto
   9.655 -  then obtain h where h: "\<forall> a \<in> SET. h a \<in> set_of P \<and> a \<in> sset (h a)" by metis
   9.656 -  have h_u[simp]: "\<And> c b1 b2. \<lbrakk>c \<in> set_of P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk>
   9.657 -                      \<Longrightarrow> h (u c b1 b2) = c"
   9.658 -  by (metis h p2 set2 u(3) u_SET)
   9.659 -  have h_u1: "\<And> c b1 b2. \<lbrakk>c \<in> set_of P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk>
   9.660 -                      \<Longrightarrow> h (u c b1 b2) = f1 b1"
   9.661 -  using h unfolding sset_def by auto
   9.662 -  have h_u2: "\<And> c b1 b2. \<lbrakk>c \<in> set_of P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk>
   9.663 -                      \<Longrightarrow> h (u c b1 b2) = f2 b2"
   9.664 -  using h unfolding sset_def by auto
   9.665 -  def M \<equiv>
   9.666 -    "Abs_multiset (\<lambda> a. if a \<in> SET \<and> p1 a \<in> set_of N1 \<and> p2 a \<in> set_of N2 then Ms (h a) a else 0)"
   9.667 -  have "(\<lambda> a. if a \<in> SET \<and> p1 a \<in> set_of N1 \<and> p2 a \<in> set_of N2 then Ms (h a) a else 0) \<in> multiset"
   9.668 -    unfolding multiset_def by auto
   9.669 -  hence [transfer_rule]: "pcr_multiset op = (\<lambda> a. if a \<in> SET \<and> p1 a \<in> set_of N1 \<and> p2 a \<in> set_of N2 then Ms (h a) a else 0) M"
   9.670 -    unfolding M_def pcr_multiset_def cr_multiset_def by (auto simp: Abs_multiset_inverse)
   9.671 -  have sM: "set_of M \<subseteq> SET" "set_of M \<subseteq> p1 -` (set_of N1)" "set_of M \<subseteq> p2 -` set_of N2"
   9.672 -    by (transfer, auto split: split_if_asm)+
   9.673 -  show "\<exists>M. set_of M \<subseteq> A \<and> mmap p1 M = N1 \<and> mmap p2 M = N2"
   9.674 -  proof(rule exI[of _ M], safe)
   9.675 -    fix a assume *: "a \<in> set_of M"
   9.676 -    from SET_A show "a \<in> A"
   9.677 -    proof (cases "a \<in> SET")
   9.678 -      case False thus ?thesis using * by transfer' auto
   9.679 -    qed blast
   9.680 -  next
   9.681 -    show "mmap p1 M = N1"
   9.682 -    proof(intro multiset_eqI)
   9.683 -      fix b1
   9.684 -      let ?K = "{a. p1 a = b1 \<and> a \<in># M}"
   9.685 -      have "setsum (count M) ?K = count N1 b1"
   9.686 -      proof(cases "b1 \<in> set_of N1")
   9.687 -        case False
   9.688 -        hence "?K = {}" using sM(2) by auto
   9.689 -        thus ?thesis using False by auto
   9.690 -      next
   9.691 -        case True
   9.692 -        def c \<equiv> "f1 b1"
   9.693 -        have c: "c \<in> set_of P" and b1: "b1 \<in> set1 c"
   9.694 -          unfolding set1_def c_def P1 using True by (auto simp: comp_eq_dest[OF set_of_mmap])
   9.695 -        with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p1 a = b1 \<and> a \<in> SET}"
   9.696 -          by transfer (force intro: setsum_mono_zero_cong_left split: split_if_asm)
   9.697 -        also have "... = setsum (count M) ((\<lambda> b2. u c b1 b2) ` (set2 c))"
   9.698 -          apply(rule setsum_cong) using c b1 proof safe
   9.699 -          fix a assume p1a: "p1 a \<in> set1 c" and "c \<in> set_of P" and "a \<in> SET"
   9.700 -          hence ac: "a \<in> sset c" using p1_rev by auto
   9.701 -          hence "a = u c (p1 a) (p2 a)" using c by auto
   9.702 -          moreover have "p2 a \<in> set2 c" using ac c by auto
   9.703 -          ultimately show "a \<in> u c (p1 a) ` set2 c" by auto
   9.704 -        qed auto
   9.705 -        also have "... = setsum (\<lambda> b2. count M (u c b1 b2)) (set2 c)"
   9.706 -          unfolding comp_def[symmetric] apply(rule setsum_reindex)
   9.707 -          using inj unfolding inj_on_def inj2_def using b1 c u(3) by blast
   9.708 -        also have "... = count N1 b1" unfolding ss1[OF c b1, symmetric]
   9.709 -          apply(rule setsum_cong[OF refl]) apply (transfer fixing: Ms u c b1 set2)
   9.710 -          using True h_u[OF c b1] set2_def u(2,3)[OF c b1] u_SET[OF c b1] by fastforce
   9.711 -        finally show ?thesis .
   9.712 -      qed
   9.713 -      thus "count (mmap p1 M) b1 = count N1 b1" by transfer
   9.714 -    qed
   9.715 -  next
   9.716 -next
   9.717 -    show "mmap p2 M = N2"
   9.718 -    proof(intro multiset_eqI)
   9.719 -      fix b2
   9.720 -      let ?K = "{a. p2 a = b2 \<and> a \<in># M}"
   9.721 -      have "setsum (count M) ?K = count N2 b2"
   9.722 -      proof(cases "b2 \<in> set_of N2")
   9.723 -        case False
   9.724 -        hence "?K = {}" using sM(3) by auto
   9.725 -        thus ?thesis using False by auto
   9.726 -      next
   9.727 -        case True
   9.728 -        def c \<equiv> "f2 b2"
   9.729 -        have c: "c \<in> set_of P" and b2: "b2 \<in> set2 c"
   9.730 -          unfolding set2_def c_def P2 using True by (auto simp: comp_eq_dest[OF set_of_mmap])
   9.731 -        with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p2 a = b2 \<and> a \<in> SET}"
   9.732 -          by transfer (force intro: setsum_mono_zero_cong_left split: split_if_asm)
   9.733 -        also have "... = setsum (count M) ((\<lambda> b1. u c b1 b2) ` (set1 c))"
   9.734 -          apply(rule setsum_cong) using c b2 proof safe
   9.735 -          fix a assume p2a: "p2 a \<in> set2 c" and "c \<in> set_of P" and "a \<in> SET"
   9.736 -          hence ac: "a \<in> sset c" using p2_rev by auto
   9.737 -          hence "a = u c (p1 a) (p2 a)" using c by auto
   9.738 -          moreover have "p1 a \<in> set1 c" using ac c by auto
   9.739 -          ultimately show "a \<in> (\<lambda>x. u c x (p2 a)) ` set1 c" by auto
   9.740 -        qed auto
   9.741 -        also have "... = setsum (count M o (\<lambda> b1. u c b1 b2)) (set1 c)"
   9.742 -          apply(rule setsum_reindex)
   9.743 -          using inj unfolding inj_on_def inj2_def using b2 c u(2) by blast
   9.744 -        also have "... = setsum (\<lambda> b1. count M (u c b1 b2)) (set1 c)" by simp
   9.745 -        also have "... = count N2 b2" unfolding ss2[OF c b2, symmetric] comp_def
   9.746 -          apply(rule setsum_cong[OF refl]) apply (transfer fixing: Ms u c b2 set1)
   9.747 -          using True h_u1[OF c _ b2] u(2,3)[OF c _ b2] u_SET[OF c _ b2] set1_def by fastforce
   9.748 -        finally show ?thesis .
   9.749 -      qed
   9.750 -      thus "count (mmap p2 M) b2 = count N2 b2" by transfer
   9.751 -    qed
   9.752 -  qed
   9.753 -qed
   9.754 -
   9.755 -lemma set_of_bd: "|set_of x| \<le>o natLeq"
   9.756 -  by transfer
   9.757 -    (auto intro!: ordLess_imp_ordLeq simp: finite_iff_ordLess_natLeq[symmetric] multiset_def)
   9.758 -
   9.759 -lemma wppull_mmap:
   9.760 -  assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
   9.761 -  shows "wppull {M. set_of M \<subseteq> A} {N1. set_of N1 \<subseteq> B1} {N2. set_of N2 \<subseteq> B2}
   9.762 -    (mmap f1) (mmap f2) (mmap e1) (mmap e2) (mmap p1) (mmap p2)"
   9.763 -proof -
   9.764 -  from assms obtain j where j: "\<forall>a'\<in>thePull B1 B2 f1 f2.
   9.765 -    j a' \<in> A \<and> e1 (p1 (j a')) = e1 (fst a') \<and> e2 (p2 (j a')) = e2 (snd a')" 
   9.766 -    by (blast dest: wppull_thePull)
   9.767 -  then show ?thesis
   9.768 -    by (intro wpull_wppull[OF wpull_mmap[OF wpull_thePull], of _ _ _ _ "mmap j"])
   9.769 -      (auto simp: comp_eq_dest_lhs[OF mmap_comp[symmetric]] comp_eq_dest[OF set_of_mmap]
   9.770 -        intro!: mmap_cong simp del: mem_set_of_iff simp: mem_set_of_iff[symmetric])
   9.771 -qed
   9.772 -
   9.773 -bnf "'a multiset"
   9.774 -  map: mmap
   9.775 -  sets: set_of 
   9.776 -  bd: natLeq
   9.777 -  wits: "{#}"
   9.778 -by (auto simp add: mmap_id0 mmap_comp set_of_mmap natLeq_card_order natLeq_cinfinite set_of_bd
   9.779 -  Grp_def relcompp.simps intro: mmap_cong)
   9.780 -  (metis wppull_mmap[OF wppull_fstOp_sndOp, unfolded wppull_def
   9.781 -    o_eq_dest_lhs[OF mmap_comp[symmetric]] fstOp_def sndOp_def comp_def, simplified])
   9.782 -
   9.783 -inductive rel_multiset' where
   9.784 -  Zero[intro]: "rel_multiset' R {#} {#}"
   9.785 -| Plus[intro]: "\<lbrakk>R a b; rel_multiset' R M N\<rbrakk> \<Longrightarrow> rel_multiset' R (M + {#a#}) (N + {#b#})"
   9.786 -
   9.787 -lemma map_multiset_Zero_iff[simp]: "mmap f M = {#} \<longleftrightarrow> M = {#}"
   9.788 -by (metis image_is_empty multiset.set_map set_of_eq_empty_iff)
   9.789 -
   9.790 -lemma map_multiset_Zero[simp]: "mmap f {#} = {#}" by simp
   9.791 -
   9.792 -lemma rel_multiset_Zero: "rel_multiset R {#} {#}"
   9.793 -unfolding rel_multiset_def Grp_def by auto
   9.794 -
   9.795 -declare multiset.count[simp]
   9.796 -declare Abs_multiset_inverse[simp]
   9.797 -declare multiset.count_inverse[simp]
   9.798 -declare union_preserves_multiset[simp]
   9.799 -
   9.800 -
   9.801 -lemma map_multiset_Plus[simp]: "mmap f (M1 + M2) = mmap f M1 + mmap f M2"
   9.802 -proof (intro multiset_eqI, transfer fixing: f)
   9.803 -  fix x :: 'a and M1 M2 :: "'b \<Rightarrow> nat"
   9.804 -  assume "M1 \<in> multiset" "M2 \<in> multiset"
   9.805 -  hence "setsum M1 {a. f a = x \<and> 0 < M1 a} = setsum M1 {a. f a = x \<and> 0 < M1 a + M2 a}"
   9.806 -        "setsum M2 {a. f a = x \<and> 0 < M2 a} = setsum M2 {a. f a = x \<and> 0 < M1 a + M2 a}"
   9.807 -    by (auto simp: multiset_def intro!: setsum_mono_zero_cong_left)
   9.808 -  then show "(\<Sum>a | f a = x \<and> 0 < M1 a + M2 a. M1 a + M2 a) =
   9.809 -       setsum M1 {a. f a = x \<and> 0 < M1 a} +
   9.810 -       setsum M2 {a. f a = x \<and> 0 < M2 a}"
   9.811 -    by (auto simp: setsum.distrib[symmetric])
   9.812 -qed
   9.813 -
   9.814 -lemma map_multiset_singl[simp]: "mmap f {#a#} = {#f a#}"
   9.815 -  by transfer auto
   9.816 -
   9.817 -lemma rel_multiset_Plus:
   9.818 -assumes ab: "R a b" and MN: "rel_multiset R M N"
   9.819 -shows "rel_multiset R (M + {#a#}) (N + {#b#})"
   9.820 -proof-
   9.821 -  {fix y assume "R a b" and "set_of y \<subseteq> {(x, y). R x y}"
   9.822 -   hence "\<exists>ya. mmap fst y + {#a#} = mmap fst ya \<and>
   9.823 -               mmap snd y + {#b#} = mmap snd ya \<and>
   9.824 -               set_of ya \<subseteq> {(x, y). R x y}"
   9.825 -   apply(intro exI[of _ "y + {#(a,b)#}"]) by auto
   9.826 -  }
   9.827 -  thus ?thesis
   9.828 -  using assms
   9.829 -  unfolding rel_multiset_def Grp_def by force
   9.830 -qed
   9.831 -
   9.832 -lemma rel_multiset'_imp_rel_multiset:
   9.833 -"rel_multiset' R M N \<Longrightarrow> rel_multiset R M N"
   9.834 -apply(induct rule: rel_multiset'.induct)
   9.835 -using rel_multiset_Zero rel_multiset_Plus by auto
   9.836 -
   9.837 -lemma mcard_mmap[simp]: "mcard (mmap f M) = mcard M"
   9.838 -proof -
   9.839 -  def A \<equiv> "\<lambda> b. {a. f a = b \<and> a \<in># M}"
   9.840 -  let ?B = "{b. 0 < setsum (count M) (A b)}"
   9.841 -  have "{b. \<exists>a. f a = b \<and> a \<in># M} \<subseteq> f ` {a. a \<in># M}" by auto
   9.842 -  moreover have "finite (f ` {a. a \<in># M})" apply(rule finite_imageI)
   9.843 -  using finite_Collect_mem .
   9.844 -  ultimately have fin: "finite {b. \<exists>a. f a = b \<and> a \<in># M}" by(rule finite_subset)
   9.845 -  have i: "inj_on A ?B" unfolding inj_on_def A_def apply clarsimp
   9.846 -    by (metis (lifting, full_types) mem_Collect_eq neq0_conv setsum.neutral)
   9.847 -  have 0: "\<And> b. 0 < setsum (count M) (A b) \<longleftrightarrow> (\<exists> a \<in> A b. count M a > 0)"
   9.848 -  apply safe
   9.849 -    apply (metis less_not_refl setsum_gt_0_iff setsum_infinite)
   9.850 -    by (metis A_def finite_Collect_conjI finite_Collect_mem setsum_gt_0_iff)
   9.851 -  hence AB: "A ` ?B = {A b | b. \<exists> a \<in> A b. count M a > 0}" by auto
   9.852 -
   9.853 -  have "setsum (\<lambda> x. setsum (count M) (A x)) ?B = setsum (setsum (count M) o A) ?B"
   9.854 -  unfolding comp_def ..
   9.855 -  also have "... = (\<Sum>x\<in> A ` ?B. setsum (count M) x)"
   9.856 -  unfolding setsum.reindex [OF i, symmetric] ..
   9.857 -  also have "... = setsum (count M) (\<Union>x\<in>A ` {b. 0 < setsum (count M) (A b)}. x)"
   9.858 -  (is "_ = setsum (count M) ?J")
   9.859 -  apply(rule setsum.UNION_disjoint[symmetric])
   9.860 -  using 0 fin unfolding A_def by auto
   9.861 -  also have "?J = {a. a \<in># M}" unfolding AB unfolding A_def by auto
   9.862 -  finally have "setsum (\<lambda> x. setsum (count M) (A x)) ?B =
   9.863 -                setsum (count M) {a. a \<in># M}" .
   9.864 -  then show ?thesis unfolding mcard_unfold_setsum A_def by transfer
   9.865 -qed
   9.866 -
   9.867 -lemma rel_multiset_mcard:
   9.868 -assumes "rel_multiset R M N"
   9.869 -shows "mcard M = mcard N"
   9.870 -using assms unfolding rel_multiset_def Grp_def by auto
   9.871 -
   9.872 -lemma multiset_induct2[case_names empty addL addR]:
   9.873 -assumes empty: "P {#} {#}"
   9.874 -and addL: "\<And>M N a. P M N \<Longrightarrow> P (M + {#a#}) N"
   9.875 -and addR: "\<And>M N a. P M N \<Longrightarrow> P M (N + {#a#})"
   9.876 -shows "P M N"
   9.877 -apply(induct N rule: multiset_induct)
   9.878 -  apply(induct M rule: multiset_induct, rule empty, erule addL)
   9.879 -  apply(induct M rule: multiset_induct, erule addR, erule addR)
   9.880 -done
   9.881 -
   9.882 -lemma multiset_induct2_mcard[consumes 1, case_names empty add]:
   9.883 -assumes c: "mcard M = mcard N"
   9.884 -and empty: "P {#} {#}"
   9.885 -and add: "\<And>M N a b. P M N \<Longrightarrow> P (M + {#a#}) (N + {#b#})"
   9.886 -shows "P M N"
   9.887 -using c proof(induct M arbitrary: N rule: measure_induct_rule[of mcard])
   9.888 -  case (less M)  show ?case
   9.889 -  proof(cases "M = {#}")
   9.890 -    case True hence "N = {#}" using less.prems by auto
   9.891 -    thus ?thesis using True empty by auto
   9.892 -  next
   9.893 -    case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split)
   9.894 -    have "N \<noteq> {#}" using False less.prems by auto
   9.895 -    then obtain N1 b where N: "N = N1 + {#b#}" by (metis multi_nonempty_split)
   9.896 -    have "mcard M1 = mcard N1" using less.prems unfolding M N by auto
   9.897 -    thus ?thesis using M N less.hyps add by auto
   9.898 -  qed
   9.899 -qed
   9.900 -
   9.901 -lemma msed_map_invL:
   9.902 -assumes "mmap f (M + {#a#}) = N"
   9.903 -shows "\<exists> N1. N = N1 + {#f a#} \<and> mmap f M = N1"
   9.904 -proof-
   9.905 -  have "f a \<in># N"
   9.906 -  using assms multiset.set_map[of f "M + {#a#}"] by auto
   9.907 -  then obtain N1 where N: "N = N1 + {#f a#}" using multi_member_split by metis
   9.908 -  have "mmap f M = N1" using assms unfolding N by simp
   9.909 -  thus ?thesis using N by blast
   9.910 -qed
   9.911 -
   9.912 -lemma msed_map_invR:
   9.913 -assumes "mmap f M = N + {#b#}"
   9.914 -shows "\<exists> M1 a. M = M1 + {#a#} \<and> f a = b \<and> mmap f M1 = N"
   9.915 -proof-
   9.916 -  obtain a where a: "a \<in># M" and fa: "f a = b"
   9.917 -  using multiset.set_map[of f M] unfolding assms
   9.918 -  by (metis image_iff mem_set_of_iff union_single_eq_member)
   9.919 -  then obtain M1 where M: "M = M1 + {#a#}" using multi_member_split by metis
   9.920 -  have "mmap f M1 = N" using assms unfolding M fa[symmetric] by simp
   9.921 -  thus ?thesis using M fa by blast
   9.922 -qed
   9.923 -
   9.924 -lemma msed_rel_invL:
   9.925 -assumes "rel_multiset R (M + {#a#}) N"
   9.926 -shows "\<exists> N1 b. N = N1 + {#b#} \<and> R a b \<and> rel_multiset R M N1"
   9.927 -proof-
   9.928 -  obtain K where KM: "mmap fst K = M + {#a#}"
   9.929 -  and KN: "mmap snd K = N" and sK: "set_of K \<subseteq> {(a, b). R a b}"
   9.930 -  using assms
   9.931 -  unfolding rel_multiset_def Grp_def by auto
   9.932 -  obtain K1 ab where K: "K = K1 + {#ab#}" and a: "fst ab = a"
   9.933 -  and K1M: "mmap fst K1 = M" using msed_map_invR[OF KM] by auto
   9.934 -  obtain N1 where N: "N = N1 + {#snd ab#}" and K1N1: "mmap snd K1 = N1"
   9.935 -  using msed_map_invL[OF KN[unfolded K]] by auto
   9.936 -  have Rab: "R a (snd ab)" using sK a unfolding K by auto
   9.937 -  have "rel_multiset R M N1" using sK K1M K1N1
   9.938 -  unfolding K rel_multiset_def Grp_def by auto
   9.939 -  thus ?thesis using N Rab by auto
   9.940 -qed
   9.941 -
   9.942 -lemma msed_rel_invR:
   9.943 -assumes "rel_multiset R M (N + {#b#})"
   9.944 -shows "\<exists> M1 a. M = M1 + {#a#} \<and> R a b \<and> rel_multiset R M1 N"
   9.945 -proof-
   9.946 -  obtain K where KN: "mmap snd K = N + {#b#}"
   9.947 -  and KM: "mmap fst K = M" and sK: "set_of K \<subseteq> {(a, b). R a b}"
   9.948 -  using assms
   9.949 -  unfolding rel_multiset_def Grp_def by auto
   9.950 -  obtain K1 ab where K: "K = K1 + {#ab#}" and b: "snd ab = b"
   9.951 -  and K1N: "mmap snd K1 = N" using msed_map_invR[OF KN] by auto
   9.952 -  obtain M1 where M: "M = M1 + {#fst ab#}" and K1M1: "mmap fst K1 = M1"
   9.953 -  using msed_map_invL[OF KM[unfolded K]] by auto
   9.954 -  have Rab: "R (fst ab) b" using sK b unfolding K by auto
   9.955 -  have "rel_multiset R M1 N" using sK K1N K1M1
   9.956 -  unfolding K rel_multiset_def Grp_def by auto
   9.957 -  thus ?thesis using M Rab by auto
   9.958 -qed
   9.959 -
   9.960 -lemma rel_multiset_imp_rel_multiset':
   9.961 -assumes "rel_multiset R M N"
   9.962 -shows "rel_multiset' R M N"
   9.963 -using assms proof(induct M arbitrary: N rule: measure_induct_rule[of mcard])
   9.964 -  case (less M)
   9.965 -  have c: "mcard M = mcard N" using rel_multiset_mcard[OF less.prems] .
   9.966 -  show ?case
   9.967 -  proof(cases "M = {#}")
   9.968 -    case True hence "N = {#}" using c by simp
   9.969 -    thus ?thesis using True rel_multiset'.Zero by auto
   9.970 -  next
   9.971 -    case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split)
   9.972 -    obtain N1 b where N: "N = N1 + {#b#}" and R: "R a b" and ms: "rel_multiset R M1 N1"
   9.973 -    using msed_rel_invL[OF less.prems[unfolded M]] by auto
   9.974 -    have "rel_multiset' R M1 N1" using less.hyps[of M1 N1] ms unfolding M by simp
   9.975 -    thus ?thesis using rel_multiset'.Plus[of R a b, OF R] unfolding M N by simp
   9.976 -  qed
   9.977 -qed
   9.978 -
   9.979 -lemma rel_multiset_rel_multiset':
   9.980 -"rel_multiset R M N = rel_multiset' R M N"
   9.981 -using  rel_multiset_imp_rel_multiset' rel_multiset'_imp_rel_multiset by auto
   9.982 -
   9.983 -(* The main end product for rel_multiset: inductive characterization *)
   9.984 -theorems rel_multiset_induct[case_names empty add, induct pred: rel_multiset] =
   9.985 -         rel_multiset'.induct[unfolded rel_multiset_rel_multiset'[symmetric]]
   9.986 -
   9.987 -
   9.988 -(* Advanced relator customization *)
   9.989 -
   9.990 -(* Set vs. sum relators: *)
   9.991 -
   9.992 -lemma set_rel_sum_rel[simp]: 
   9.993 -"set_rel (sum_rel \<chi> \<phi>) A1 A2 \<longleftrightarrow> 
   9.994 - set_rel \<chi> (Inl -` A1) (Inl -` A2) \<and> set_rel \<phi> (Inr -` A1) (Inr -` A2)"
   9.995 -(is "?L \<longleftrightarrow> ?Rl \<and> ?Rr")
   9.996 -proof safe
   9.997 -  assume L: "?L"
   9.998 -  show ?Rl unfolding set_rel_def Bex_def vimage_eq proof safe
   9.999 -    fix l1 assume "Inl l1 \<in> A1"
  9.1000 -    then obtain a2 where a2: "a2 \<in> A2" and "sum_rel \<chi> \<phi> (Inl l1) a2"
  9.1001 -    using L unfolding set_rel_def by auto
  9.1002 -    then obtain l2 where "a2 = Inl l2 \<and> \<chi> l1 l2" by (cases a2, auto)
  9.1003 -    thus "\<exists> l2. Inl l2 \<in> A2 \<and> \<chi> l1 l2" using a2 by auto
  9.1004 -  next
  9.1005 -    fix l2 assume "Inl l2 \<in> A2"
  9.1006 -    then obtain a1 where a1: "a1 \<in> A1" and "sum_rel \<chi> \<phi> a1 (Inl l2)"
  9.1007 -    using L unfolding set_rel_def by auto
  9.1008 -    then obtain l1 where "a1 = Inl l1 \<and> \<chi> l1 l2" by (cases a1, auto)
  9.1009 -    thus "\<exists> l1. Inl l1 \<in> A1 \<and> \<chi> l1 l2" using a1 by auto
  9.1010 -  qed
  9.1011 -  show ?Rr unfolding set_rel_def Bex_def vimage_eq proof safe
  9.1012 -    fix r1 assume "Inr r1 \<in> A1"
  9.1013 -    then obtain a2 where a2: "a2 \<in> A2" and "sum_rel \<chi> \<phi> (Inr r1) a2"
  9.1014 -    using L unfolding set_rel_def by auto
  9.1015 -    then obtain r2 where "a2 = Inr r2 \<and> \<phi> r1 r2" by (cases a2, auto)
  9.1016 -    thus "\<exists> r2. Inr r2 \<in> A2 \<and> \<phi> r1 r2" using a2 by auto
  9.1017 -  next
  9.1018 -    fix r2 assume "Inr r2 \<in> A2"
  9.1019 -    then obtain a1 where a1: "a1 \<in> A1" and "sum_rel \<chi> \<phi> a1 (Inr r2)"
  9.1020 -    using L unfolding set_rel_def by auto
  9.1021 -    then obtain r1 where "a1 = Inr r1 \<and> \<phi> r1 r2" by (cases a1, auto)
  9.1022 -    thus "\<exists> r1. Inr r1 \<in> A1 \<and> \<phi> r1 r2" using a1 by auto
  9.1023 -  qed
  9.1024 -next
  9.1025 -  assume Rl: "?Rl" and Rr: "?Rr"
  9.1026 -  show ?L unfolding set_rel_def Bex_def vimage_eq proof safe
  9.1027 -    fix a1 assume a1: "a1 \<in> A1"
  9.1028 -    show "\<exists> a2. a2 \<in> A2 \<and> sum_rel \<chi> \<phi> a1 a2"
  9.1029 -    proof(cases a1)
  9.1030 -      case (Inl l1) then obtain l2 where "Inl l2 \<in> A2 \<and> \<chi> l1 l2"
  9.1031 -      using Rl a1 unfolding set_rel_def by blast
  9.1032 -      thus ?thesis unfolding Inl by auto
  9.1033 -    next
  9.1034 -      case (Inr r1) then obtain r2 where "Inr r2 \<in> A2 \<and> \<phi> r1 r2"
  9.1035 -      using Rr a1 unfolding set_rel_def by blast
  9.1036 -      thus ?thesis unfolding Inr by auto
  9.1037 -    qed
  9.1038 -  next
  9.1039 -    fix a2 assume a2: "a2 \<in> A2"
  9.1040 -    show "\<exists> a1. a1 \<in> A1 \<and> sum_rel \<chi> \<phi> a1 a2"
  9.1041 -    proof(cases a2)
  9.1042 -      case (Inl l2) then obtain l1 where "Inl l1 \<in> A1 \<and> \<chi> l1 l2"
  9.1043 -      using Rl a2 unfolding set_rel_def by blast
  9.1044 -      thus ?thesis unfolding Inl by auto
  9.1045 -    next
  9.1046 -      case (Inr r2) then obtain r1 where "Inr r1 \<in> A1 \<and> \<phi> r1 r2"
  9.1047 -      using Rr a2 unfolding set_rel_def by blast
  9.1048 -      thus ?thesis unfolding Inr by auto
  9.1049 -    qed
  9.1050 -  qed
  9.1051 -qed
  9.1052 -
  9.1053 -end
    10.1 --- a/src/HOL/Library/Multiset.thy	Thu Jan 23 19:02:22 2014 +0100
    10.2 +++ b/src/HOL/Library/Multiset.thy	Fri Jan 24 11:51:45 2014 +0100
    10.3 @@ -1,5 +1,6 @@
    10.4  (*  Title:      HOL/Library/Multiset.thy
    10.5      Author:     Tobias Nipkow, Markus Wenzel, Lawrence C Paulson, Norbert Voelker
    10.6 +    Author:     Andrei Popescu, TU Muenchen
    10.7  *)
    10.8  
    10.9  header {* (Finite) multisets *}
   10.10 @@ -2157,5 +2158,810 @@
   10.11  
   10.12  hide_const (open) msetify
   10.13  
   10.14 +
   10.15 +subsection {* BNF setup *}
   10.16 +
   10.17 +lemma setsum_gt_0_iff:
   10.18 +fixes f :: "'a \<Rightarrow> nat" assumes "finite A"
   10.19 +shows "setsum f A > 0 \<longleftrightarrow> (\<exists> a \<in> A. f a > 0)"
   10.20 +(is "?L \<longleftrightarrow> ?R")
   10.21 +proof-
   10.22 +  have "?L \<longleftrightarrow> \<not> setsum f A = 0" by fast
   10.23 +  also have "... \<longleftrightarrow> (\<exists> a \<in> A. f a \<noteq> 0)" using assms by simp
   10.24 +  also have "... \<longleftrightarrow> ?R" by simp
   10.25 +  finally show ?thesis .
   10.26 +qed
   10.27 +
   10.28 +lift_definition mmap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" is
   10.29 +  "\<lambda>h f b. setsum f {a. h a = b \<and> f a > 0} :: nat"
   10.30 +unfolding multiset_def proof safe
   10.31 +  fix h :: "'a \<Rightarrow> 'b" and f :: "'a \<Rightarrow> nat"
   10.32 +  assume fin: "finite {a. 0 < f a}"  (is "finite ?A")
   10.33 +  show "finite {b. 0 < setsum f {a. h a = b \<and> 0 < f a}}"
   10.34 +  (is "finite {b. 0 < setsum f (?As b)}")
   10.35 +  proof- let ?B = "{b. 0 < setsum f (?As b)}"
   10.36 +    have "\<And> b. finite (?As b)" using fin by simp
   10.37 +    hence B: "?B = {b. ?As b \<noteq> {}}" by (auto simp add: setsum_gt_0_iff)
   10.38 +    hence "?B \<subseteq> h ` ?A" by auto
   10.39 +    thus ?thesis using finite_surj[OF fin] by auto
   10.40 +  qed
   10.41 +qed
   10.42 +
   10.43 +lemma mmap_id0: "mmap id = id"
   10.44 +proof (intro ext multiset_eqI)
   10.45 +  fix f a show "count (mmap id f) a = count (id f) a"
   10.46 +  proof (cases "count f a = 0")
   10.47 +    case False
   10.48 +    hence 1: "{aa. aa = a \<and> aa \<in># f} = {a}" by auto
   10.49 +    thus ?thesis by transfer auto
   10.50 +  qed (transfer, simp)
   10.51 +qed
   10.52 +
   10.53 +lemma inj_on_setsum_inv:
   10.54 +assumes 1: "(0::nat) < setsum (count f) {a. h a = b' \<and> a \<in># f}" (is "0 < setsum (count f) ?A'")
   10.55 +and     2: "{a. h a = b \<and> a \<in># f} = {a. h a = b' \<and> a \<in># f}" (is "?A = ?A'")
   10.56 +shows "b = b'"
   10.57 +using assms by (auto simp add: setsum_gt_0_iff)
   10.58 +
   10.59 +lemma mmap_comp:
   10.60 +fixes h1 :: "'a \<Rightarrow> 'b" and h2 :: "'b \<Rightarrow> 'c"
   10.61 +shows "mmap (h2 o h1) = mmap h2 o mmap h1"
   10.62 +proof (intro ext multiset_eqI)
   10.63 +  fix f :: "'a multiset" fix c :: 'c
   10.64 +  let ?A = "{a. h2 (h1 a) = c \<and> a \<in># f}"
   10.65 +  let ?As = "\<lambda> b. {a. h1 a = b \<and> a \<in># f}"
   10.66 +  let ?B = "{b. h2 b = c \<and> 0 < setsum (count f) (?As b)}"
   10.67 +  have 0: "{?As b | b.  b \<in> ?B} = ?As ` ?B" by auto
   10.68 +  have "\<And> b. finite (?As b)" by transfer (simp add: multiset_def)
   10.69 +  hence "?B = {b. h2 b = c \<and> ?As b \<noteq> {}}" by (auto simp add: setsum_gt_0_iff)
   10.70 +  hence A: "?A = \<Union> {?As b | b.  b \<in> ?B}" by auto
   10.71 +  have "setsum (count f) ?A = setsum (setsum (count f)) {?As b | b.  b \<in> ?B}"
   10.72 +    unfolding A by transfer (intro setsum_Union_disjoint, auto simp: multiset_def)
   10.73 +  also have "... = setsum (setsum (count f)) (?As ` ?B)" unfolding 0 ..
   10.74 +  also have "... = setsum (setsum (count f) o ?As) ?B"
   10.75 +    by(intro setsum_reindex) (auto simp add: setsum_gt_0_iff inj_on_def)
   10.76 +  also have "... = setsum (\<lambda> b. setsum (count f) (?As b)) ?B" unfolding comp_def ..
   10.77 +  finally have "setsum (count f) ?A = setsum (\<lambda> b. setsum (count f) (?As b)) ?B" .
   10.78 +  thus "count (mmap (h2 \<circ> h1) f) c = count ((mmap h2 \<circ> mmap h1) f) c"
   10.79 +    by transfer (unfold comp_apply, blast)
   10.80 +qed
   10.81 +
   10.82 +lemma mmap_cong:
   10.83 +assumes "\<And>a. a \<in># M \<Longrightarrow> f a = g a"
   10.84 +shows "mmap f M = mmap g M"
   10.85 +using assms by transfer (auto intro!: setsum_cong)
   10.86 +
   10.87 +context
   10.88 +begin
   10.89 +interpretation lifting_syntax .
   10.90 +
   10.91 +lemma set_of_transfer[transfer_rule]: "(pcr_multiset op = ===> op =) (\<lambda>f. {a. 0 < f a}) set_of"
   10.92 +  unfolding set_of_def pcr_multiset_def cr_multiset_def fun_rel_def by auto
   10.93 +
   10.94  end
   10.95  
   10.96 +lemma set_of_mmap: "set_of o mmap h = image h o set_of"
   10.97 +proof (rule ext, unfold comp_apply)
   10.98 +  fix M show "set_of (mmap h M) = h ` set_of M"
   10.99 +    by transfer (auto simp add: multiset_def setsum_gt_0_iff)
  10.100 +qed
  10.101 +
  10.102 +lemma multiset_of_surj:
  10.103 +  "multiset_of ` {as. set as \<subseteq> A} = {M. set_of M \<subseteq> A}"
  10.104 +proof safe
  10.105 +  fix M assume M: "set_of M \<subseteq> A"
  10.106 +  obtain as where eq: "M = multiset_of as" using surj_multiset_of unfolding surj_def by auto
  10.107 +  hence "set as \<subseteq> A" using M by auto
  10.108 +  thus "M \<in> multiset_of ` {as. set as \<subseteq> A}" using eq by auto
  10.109 +next
  10.110 +  show "\<And>x xa xb. \<lbrakk>set xa \<subseteq> A; xb \<in> set_of (multiset_of xa)\<rbrakk> \<Longrightarrow> xb \<in> A"
  10.111 +  by (erule set_mp) (unfold set_of_multiset_of)
  10.112 +qed
  10.113 +
  10.114 +lemma card_of_set_of:
  10.115 +"(card_of {M. set_of M \<subseteq> A}, card_of {as. set as \<subseteq> A}) \<in> ordLeq"
  10.116 +apply(rule card_of_ordLeqI2[of _ multiset_of]) using multiset_of_surj by auto
  10.117 +
  10.118 +lemma nat_sum_induct:
  10.119 +assumes "\<And>n1 n2. (\<And> m1 m2. m1 + m2 < n1 + n2 \<Longrightarrow> phi m1 m2) \<Longrightarrow> phi n1 n2"
  10.120 +shows "phi (n1::nat) (n2::nat)"
  10.121 +proof-
  10.122 +  let ?chi = "\<lambda> n1n2 :: nat * nat. phi (fst n1n2) (snd n1n2)"
  10.123 +  have "?chi (n1,n2)"
  10.124 +  apply(induct rule: measure_induct[of "\<lambda> n1n2. fst n1n2 + snd n1n2" ?chi])
  10.125 +  using assms by (metis fstI sndI)
  10.126 +  thus ?thesis by simp
  10.127 +qed
  10.128 +
  10.129 +lemma matrix_count:
  10.130 +fixes ct1 ct2 :: "nat \<Rightarrow> nat"
  10.131 +assumes "setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2}"
  10.132 +shows
  10.133 +"\<exists> ct. (\<forall> i1 \<le> n1. setsum (\<lambda> i2. ct i1 i2) {..<Suc n2} = ct1 i1) \<and>
  10.134 +       (\<forall> i2 \<le> n2. setsum (\<lambda> i1. ct i1 i2) {..<Suc n1} = ct2 i2)"
  10.135 +(is "?phi ct1 ct2 n1 n2")
  10.136 +proof-
  10.137 +  have "\<forall> ct1 ct2 :: nat \<Rightarrow> nat.
  10.138 +        setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2} \<longrightarrow> ?phi ct1 ct2 n1 n2"
  10.139 +  proof(induct rule: nat_sum_induct[of
  10.140 +"\<lambda> n1 n2. \<forall> ct1 ct2 :: nat \<Rightarrow> nat.
  10.141 +     setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2} \<longrightarrow> ?phi ct1 ct2 n1 n2"],
  10.142 +      clarify)
  10.143 +  fix n1 n2 :: nat and ct1 ct2 :: "nat \<Rightarrow> nat"
  10.144 +  assume IH: "\<And> m1 m2. m1 + m2 < n1 + n2 \<Longrightarrow>
  10.145 +                \<forall> dt1 dt2 :: nat \<Rightarrow> nat.
  10.146 +                setsum dt1 {..<Suc m1} = setsum dt2 {..<Suc m2} \<longrightarrow> ?phi dt1 dt2 m1 m2"
  10.147 +  and ss: "setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2}"
  10.148 +  show "?phi ct1 ct2 n1 n2"
  10.149 +  proof(cases n1)
  10.150 +    case 0 note n1 = 0
  10.151 +    show ?thesis
  10.152 +    proof(cases n2)
  10.153 +      case 0 note n2 = 0
  10.154 +      let ?ct = "\<lambda> i1 i2. ct2 0"
  10.155 +      show ?thesis apply(rule exI[of _ ?ct]) using n1 n2 ss by simp
  10.156 +    next
  10.157 +      case (Suc m2) note n2 = Suc
  10.158 +      let ?ct = "\<lambda> i1 i2. ct2 i2"
  10.159 +      show ?thesis apply(rule exI[of _ ?ct]) using n1 n2 ss by auto
  10.160 +    qed
  10.161 +  next
  10.162 +    case (Suc m1) note n1 = Suc
  10.163 +    show ?thesis
  10.164 +    proof(cases n2)
  10.165 +      case 0 note n2 = 0
  10.166 +      let ?ct = "\<lambda> i1 i2. ct1 i1"
  10.167 +      show ?thesis apply(rule exI[of _ ?ct]) using n1 n2 ss by auto
  10.168 +    next
  10.169 +      case (Suc m2) note n2 = Suc
  10.170 +      show ?thesis
  10.171 +      proof(cases "ct1 n1 \<le> ct2 n2")
  10.172 +        case True
  10.173 +        def dt2 \<equiv> "\<lambda> i2. if i2 = n2 then ct2 i2 - ct1 n1 else ct2 i2"
  10.174 +        have "setsum ct1 {..<Suc m1} = setsum dt2 {..<Suc n2}"
  10.175 +        unfolding dt2_def using ss n1 True by auto
  10.176 +        hence "?phi ct1 dt2 m1 n2" using IH[of m1 n2] n1 by simp
  10.177 +        then obtain dt where
  10.178 +        1: "\<And> i1. i1 \<le> m1 \<Longrightarrow> setsum (\<lambda> i2. dt i1 i2) {..<Suc n2} = ct1 i1" and
  10.179 +        2: "\<And> i2. i2 \<le> n2 \<Longrightarrow> setsum (\<lambda> i1. dt i1 i2) {..<Suc m1} = dt2 i2" by auto
  10.180 +        let ?ct = "\<lambda> i1 i2. if i1 = n1 then (if i2 = n2 then ct1 n1 else 0)
  10.181 +                                       else dt i1 i2"
  10.182 +        show ?thesis apply(rule exI[of _ ?ct])
  10.183 +        using n1 n2 1 2 True unfolding dt2_def by simp
  10.184 +      next
  10.185 +        case False
  10.186 +        hence False: "ct2 n2 < ct1 n1" by simp
  10.187 +        def dt1 \<equiv> "\<lambda> i1. if i1 = n1 then ct1 i1 - ct2 n2 else ct1 i1"
  10.188 +        have "setsum dt1 {..<Suc n1} = setsum ct2 {..<Suc m2}"
  10.189 +        unfolding dt1_def using ss n2 False by auto
  10.190 +        hence "?phi dt1 ct2 n1 m2" using IH[of n1 m2] n2 by simp
  10.191 +        then obtain dt where
  10.192 +        1: "\<And> i1. i1 \<le> n1 \<Longrightarrow> setsum (\<lambda> i2. dt i1 i2) {..<Suc m2} = dt1 i1" and
  10.193 +        2: "\<And> i2. i2 \<le> m2 \<Longrightarrow> setsum (\<lambda> i1. dt i1 i2) {..<Suc n1} = ct2 i2" by force
  10.194 +        let ?ct = "\<lambda> i1 i2. if i2 = n2 then (if i1 = n1 then ct2 n2 else 0)
  10.195 +                                       else dt i1 i2"
  10.196 +        show ?thesis apply(rule exI[of _ ?ct])
  10.197 +        using n1 n2 1 2 False unfolding dt1_def by simp
  10.198 +      qed
  10.199 +    qed
  10.200 +  qed
  10.201 +  qed
  10.202 +  thus ?thesis using assms by auto
  10.203 +qed
  10.204 +
  10.205 +definition
  10.206 +"inj2 u B1 B2 \<equiv>
  10.207 + \<forall> b1 b1' b2 b2'. {b1,b1'} \<subseteq> B1 \<and> {b2,b2'} \<subseteq> B2 \<and> u b1 b2 = u b1' b2'
  10.208 +                  \<longrightarrow> b1 = b1' \<and> b2 = b2'"
  10.209 +
  10.210 +lemma matrix_setsum_finite:
  10.211 +assumes B1: "B1 \<noteq> {}" "finite B1" and B2: "B2 \<noteq> {}" "finite B2" and u: "inj2 u B1 B2"
  10.212 +and ss: "setsum N1 B1 = setsum N2 B2"
  10.213 +shows "\<exists> M :: 'a \<Rightarrow> nat.
  10.214 +            (\<forall> b1 \<in> B1. setsum (\<lambda> b2. M (u b1 b2)) B2 = N1 b1) \<and>
  10.215 +            (\<forall> b2 \<in> B2. setsum (\<lambda> b1. M (u b1 b2)) B1 = N2 b2)"
  10.216 +proof-
  10.217 +  obtain n1 where "card B1 = Suc n1" using B1 by (metis card_insert finite.simps)
  10.218 +  then obtain e1 where e1: "bij_betw e1 {..<Suc n1} B1"
  10.219 +  using ex_bij_betw_finite_nat[OF B1(2)] by (metis atLeast0LessThan bij_betw_the_inv_into)
  10.220 +  hence e1_inj: "inj_on e1 {..<Suc n1}" and e1_surj: "e1 ` {..<Suc n1} = B1"
  10.221 +  unfolding bij_betw_def by auto
  10.222 +  def f1 \<equiv> "inv_into {..<Suc n1} e1"
  10.223 +  have f1: "bij_betw f1 B1 {..<Suc n1}"
  10.224 +  and f1e1[simp]: "\<And> i1. i1 < Suc n1 \<Longrightarrow> f1 (e1 i1) = i1"
  10.225 +  and e1f1[simp]: "\<And> b1. b1 \<in> B1 \<Longrightarrow> e1 (f1 b1) = b1" unfolding f1_def
  10.226 +  apply (metis bij_betw_inv_into e1, metis bij_betw_inv_into_left e1 lessThan_iff)
  10.227 +  by (metis e1_surj f_inv_into_f)
  10.228 +  (*  *)
  10.229 +  obtain n2 where "card B2 = Suc n2" using B2 by (metis card_insert finite.simps)
  10.230 +  then obtain e2 where e2: "bij_betw e2 {..<Suc n2} B2"
  10.231 +  using ex_bij_betw_finite_nat[OF B2(2)] by (metis atLeast0LessThan bij_betw_the_inv_into)
  10.232 +  hence e2_inj: "inj_on e2 {..<Suc n2}" and e2_surj: "e2 ` {..<Suc n2} = B2"
  10.233 +  unfolding bij_betw_def by auto
  10.234 +  def f2 \<equiv> "inv_into {..<Suc n2} e2"
  10.235 +  have f2: "bij_betw f2 B2 {..<Suc n2}"
  10.236 +  and f2e2[simp]: "\<And> i2. i2 < Suc n2 \<Longrightarrow> f2 (e2 i2) = i2"
  10.237 +  and e2f2[simp]: "\<And> b2. b2 \<in> B2 \<Longrightarrow> e2 (f2 b2) = b2" unfolding f2_def
  10.238 +  apply (metis bij_betw_inv_into e2, metis bij_betw_inv_into_left e2 lessThan_iff)
  10.239 +  by (metis e2_surj f_inv_into_f)
  10.240 +  (*  *)
  10.241 +  let ?ct1 = "N1 o e1"  let ?ct2 = "N2 o e2"
  10.242 +  have ss: "setsum ?ct1 {..<Suc n1} = setsum ?ct2 {..<Suc n2}"
  10.243 +  unfolding setsum_reindex[OF e1_inj, symmetric] setsum_reindex[OF e2_inj, symmetric]
  10.244 +  e1_surj e2_surj using ss .
  10.245 +  obtain ct where
  10.246 +  ct1: "\<And> i1. i1 \<le> n1 \<Longrightarrow> setsum (\<lambda> i2. ct i1 i2) {..<Suc n2} = ?ct1 i1" and
  10.247 +  ct2: "\<And> i2. i2 \<le> n2 \<Longrightarrow> setsum (\<lambda> i1. ct i1 i2) {..<Suc n1} = ?ct2 i2"
  10.248 +  using matrix_count[OF ss] by blast
  10.249 +  (*  *)
  10.250 +  def A \<equiv> "{u b1 b2 | b1 b2. b1 \<in> B1 \<and> b2 \<in> B2}"
  10.251 +  have "\<forall> a \<in> A. \<exists> b1b2 \<in> B1 <*> B2. u (fst b1b2) (snd b1b2) = a"
  10.252 +  unfolding A_def Ball_def mem_Collect_eq by auto
  10.253 +  then obtain h1h2 where h12:
  10.254 +  "\<And>a. a \<in> A \<Longrightarrow> u (fst (h1h2 a)) (snd (h1h2 a)) = a \<and> h1h2 a \<in> B1 <*> B2" by metis
  10.255 +  def h1 \<equiv> "fst o h1h2"  def h2 \<equiv> "snd o h1h2"
  10.256 +  have h12[simp]: "\<And>a. a \<in> A \<Longrightarrow> u (h1 a) (h2 a) = a"
  10.257 +                  "\<And> a. a \<in> A \<Longrightarrow> h1 a \<in> B1"  "\<And> a. a \<in> A \<Longrightarrow> h2 a \<in> B2"
  10.258 +  using h12 unfolding h1_def h2_def by force+
  10.259 +  {fix b1 b2 assume b1: "b1 \<in> B1" and b2: "b2 \<in> B2"
  10.260 +   hence inA: "u b1 b2 \<in> A" unfolding A_def by auto
  10.261 +   hence "u b1 b2 = u (h1 (u b1 b2)) (h2 (u b1 b2))" by auto
  10.262 +   moreover have "h1 (u b1 b2) \<in> B1" "h2 (u b1 b2) \<in> B2" using inA by auto
  10.263 +   ultimately have "h1 (u b1 b2) = b1 \<and> h2 (u b1 b2) = b2"
  10.264 +   using u b1 b2 unfolding inj2_def by fastforce
  10.265 +  }
  10.266 +  hence h1[simp]: "\<And> b1 b2. \<lbrakk>b1 \<in> B1; b2 \<in> B2\<rbrakk> \<Longrightarrow> h1 (u b1 b2) = b1" and
  10.267 +        h2[simp]: "\<And> b1 b2. \<lbrakk>b1 \<in> B1; b2 \<in> B2\<rbrakk> \<Longrightarrow> h2 (u b1 b2) = b2" by auto
  10.268 +  def M \<equiv> "\<lambda> a. ct (f1 (h1 a)) (f2 (h2 a))"
  10.269 +  show ?thesis
  10.270 +  apply(rule exI[of _ M]) proof safe
  10.271 +    fix b1 assume b1: "b1 \<in> B1"
  10.272 +    hence f1b1: "f1 b1 \<le> n1" using f1 unfolding bij_betw_def
  10.273 +    by (metis image_eqI lessThan_iff less_Suc_eq_le)
  10.274 +    have "(\<Sum>b2\<in>B2. M (u b1 b2)) = (\<Sum>i2<Suc n2. ct (f1 b1) (f2 (e2 i2)))"
  10.275 +    unfolding e2_surj[symmetric] setsum_reindex[OF e2_inj]
  10.276 +    unfolding M_def comp_def apply(intro setsum_cong) apply force
  10.277 +    by (metis e2_surj b1 h1 h2 imageI)
  10.278 +    also have "... = N1 b1" using b1 ct1[OF f1b1] by simp
  10.279 +    finally show "(\<Sum>b2\<in>B2. M (u b1 b2)) = N1 b1" .
  10.280 +  next
  10.281 +    fix b2 assume b2: "b2 \<in> B2"
  10.282 +    hence f2b2: "f2 b2 \<le> n2" using f2 unfolding bij_betw_def
  10.283 +    by (metis image_eqI lessThan_iff less_Suc_eq_le)
  10.284 +    have "(\<Sum>b1\<in>B1. M (u b1 b2)) = (\<Sum>i1<Suc n1. ct (f1 (e1 i1)) (f2 b2))"
  10.285 +    unfolding e1_surj[symmetric] setsum_reindex[OF e1_inj]
  10.286 +    unfolding M_def comp_def apply(intro setsum_cong) apply force
  10.287 +    by (metis e1_surj b2 h1 h2 imageI)
  10.288 +    also have "... = N2 b2" using b2 ct2[OF f2b2] by simp
  10.289 +    finally show "(\<Sum>b1\<in>B1. M (u b1 b2)) = N2 b2" .
  10.290 +  qed
  10.291 +qed
  10.292 +
  10.293 +lemma supp_vimage_mmap: "set_of M \<subseteq> f -` (set_of (mmap f M))"
  10.294 +  by transfer (auto simp: multiset_def setsum_gt_0_iff)
  10.295 +
  10.296 +lemma mmap_ge_0: "b \<in># mmap f M \<longleftrightarrow> (\<exists>a. a \<in># M \<and> f a = b)"
  10.297 +  by transfer (auto simp: multiset_def setsum_gt_0_iff)
  10.298 +
  10.299 +lemma finite_twosets:
  10.300 +assumes "finite B1" and "finite B2"
  10.301 +shows "finite {u b1 b2 |b1 b2. b1 \<in> B1 \<and> b2 \<in> B2}"  (is "finite ?A")
  10.302 +proof-
  10.303 +  have A: "?A = (\<lambda> b1b2. u (fst b1b2) (snd b1b2)) ` (B1 <*> B2)" by force
  10.304 +  show ?thesis unfolding A using finite_cartesian_product[OF assms] by auto
  10.305 +qed
  10.306 +
  10.307 +(* Weak pullbacks: *)
  10.308 +definition wpull where
  10.309 +"wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow>
  10.310 + (\<forall> b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<longrightarrow> (\<exists> a \<in> A. p1 a = b1 \<and> p2 a = b2))"
  10.311 +
  10.312 +(* Weak pseudo-pullbacks *)
  10.313 +definition wppull where
  10.314 +"wppull A B1 B2 f1 f2 e1 e2 p1 p2 \<longleftrightarrow>
  10.315 + (\<forall> b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<longrightarrow>
  10.316 +           (\<exists> a \<in> A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2))"
  10.317 +
  10.318 +
  10.319 +(* The pullback of sets *)
  10.320 +definition thePull where
  10.321 +"thePull B1 B2 f1 f2 = {(b1,b2). b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2}"
  10.322 +
  10.323 +lemma wpull_thePull:
  10.324 +"wpull (thePull B1 B2 f1 f2) B1 B2 f1 f2 fst snd"
  10.325 +unfolding wpull_def thePull_def by auto
  10.326 +
  10.327 +lemma wppull_thePull:
  10.328 +assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
  10.329 +shows
  10.330 +"\<exists> j. \<forall> a' \<in> thePull B1 B2 f1 f2.
  10.331 +   j a' \<in> A \<and>
  10.332 +   e1 (p1 (j a')) = e1 (fst a') \<and> e2 (p2 (j a')) = e2 (snd a')"
  10.333 +(is "\<exists> j. \<forall> a' \<in> ?A'. ?phi a' (j a')")
  10.334 +proof(rule bchoice[of ?A' ?phi], default)
  10.335 +  fix a' assume a': "a' \<in> ?A'"
  10.336 +  hence "fst a' \<in> B1" unfolding thePull_def by auto
  10.337 +  moreover
  10.338 +  from a' have "snd a' \<in> B2" unfolding thePull_def by auto
  10.339 +  moreover have "f1 (fst a') = f2 (snd a')"
  10.340 +  using a' unfolding csquare_def thePull_def by auto
  10.341 +  ultimately show "\<exists> ja'. ?phi a' ja'"
  10.342 +  using assms unfolding wppull_def by blast
  10.343 +qed
  10.344 +
  10.345 +lemma wpull_wppull:
  10.346 +assumes wp: "wpull A' B1 B2 f1 f2 p1' p2'" and
  10.347 +1: "\<forall> a' \<in> A'. j a' \<in> A \<and> e1 (p1 (j a')) = e1 (p1' a') \<and> e2 (p2 (j a')) = e2 (p2' a')"
  10.348 +shows "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
  10.349 +unfolding wppull_def proof safe
  10.350 +  fix b1 b2
  10.351 +  assume b1: "b1 \<in> B1" and b2: "b2 \<in> B2" and f: "f1 b1 = f2 b2"
  10.352 +  then obtain a' where a': "a' \<in> A'" and b1: "b1 = p1' a'" and b2: "b2 = p2' a'"
  10.353 +  using wp unfolding wpull_def by blast
  10.354 +  show "\<exists>a\<in>A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2"
  10.355 +  apply (rule bexI[of _ "j a'"]) unfolding b1 b2 using a' 1 by auto
  10.356 +qed
  10.357 +
  10.358 +lemma wppull_fstOp_sndOp:
  10.359 +shows "wppull (Collect (split (P OO Q))) (Collect (split P)) (Collect (split Q))
  10.360 +  snd fst fst snd (BNF_Def.fstOp P Q) (BNF_Def.sndOp P Q)"
  10.361 +using pick_middlep unfolding wppull_def fstOp_def sndOp_def relcompp.simps by auto
  10.362 +
  10.363 +lemma wpull_mmap:
  10.364 +fixes A :: "'a set" and B1 :: "'b1 set" and B2 :: "'b2 set"
  10.365 +assumes wp: "wpull A B1 B2 f1 f2 p1 p2"
  10.366 +shows
  10.367 +"wpull {M. set_of M \<subseteq> A}
  10.368 +       {N1. set_of N1 \<subseteq> B1} {N2. set_of N2 \<subseteq> B2}
  10.369 +       (mmap f1) (mmap f2) (mmap p1) (mmap p2)"
  10.370 +unfolding wpull_def proof (safe, unfold Bex_def mem_Collect_eq)
  10.371 +  fix N1 :: "'b1 multiset" and N2 :: "'b2 multiset"
  10.372 +  assume mmap': "mmap f1 N1 = mmap f2 N2"
  10.373 +  and N1[simp]: "set_of N1 \<subseteq> B1"
  10.374 +  and N2[simp]: "set_of N2 \<subseteq> B2"
  10.375 +  def P \<equiv> "mmap f1 N1"
  10.376 +  have P1: "P = mmap f1 N1" and P2: "P = mmap f2 N2" unfolding P_def using mmap' by auto
  10.377 +  note P = P1 P2
  10.378 +  have fin_N1[simp]: "finite (set_of N1)"
  10.379 +   and fin_N2[simp]: "finite (set_of N2)"
  10.380 +   and fin_P[simp]: "finite (set_of P)" by auto
  10.381 +
  10.382 +  def set1 \<equiv> "\<lambda> c. {b1 \<in> set_of N1. f1 b1 = c}"
  10.383 +  have set1[simp]: "\<And> c b1. b1 \<in> set1 c \<Longrightarrow> f1 b1 = c" unfolding set1_def by auto
  10.384 +  have fin_set1: "\<And> c. c \<in> set_of P \<Longrightarrow> finite (set1 c)"
  10.385 +    using N1(1) unfolding set1_def multiset_def by auto
  10.386 +  have set1_NE: "\<And> c. c \<in> set_of P \<Longrightarrow> set1 c \<noteq> {}"
  10.387 +   unfolding set1_def set_of_def P mmap_ge_0 by auto
  10.388 +  have supp_N1_set1: "set_of N1 = (\<Union> c \<in> set_of P. set1 c)"
  10.389 +    using supp_vimage_mmap[of N1 f1] unfolding set1_def P1 by auto
  10.390 +  hence set1_inclN1: "\<And>c. c \<in> set_of P \<Longrightarrow> set1 c \<subseteq> set_of N1" by auto
  10.391 +  hence set1_incl: "\<And> c. c \<in> set_of P \<Longrightarrow> set1 c \<subseteq> B1" using N1 by blast
  10.392 +  have set1_disj: "\<And> c c'. c \<noteq> c' \<Longrightarrow> set1 c \<inter> set1 c' = {}"
  10.393 +    unfolding set1_def by auto
  10.394 +  have setsum_set1: "\<And> c. setsum (count N1) (set1 c) = count P c"
  10.395 +    unfolding P1 set1_def by transfer (auto intro: setsum_cong)
  10.396 +
  10.397 +  def set2 \<equiv> "\<lambda> c. {b2 \<in> set_of N2. f2 b2 = c}"
  10.398 +  have set2[simp]: "\<And> c b2. b2 \<in> set2 c \<Longrightarrow> f2 b2 = c" unfolding set2_def by auto
  10.399 +  have fin_set2: "\<And> c. c \<in> set_of P \<Longrightarrow> finite (set2 c)"
  10.400 +  using N2(1) unfolding set2_def multiset_def by auto
  10.401 +  have set2_NE: "\<And> c. c \<in> set_of P \<Longrightarrow> set2 c \<noteq> {}"
  10.402 +    unfolding set2_def P2 mmap_ge_0 set_of_def by auto
  10.403 +  have supp_N2_set2: "set_of N2 = (\<Union> c \<in> set_of P. set2 c)"
  10.404 +    using supp_vimage_mmap[of N2 f2] unfolding set2_def P2 by auto
  10.405 +  hence set2_inclN2: "\<And>c. c \<in> set_of P \<Longrightarrow> set2 c \<subseteq> set_of N2" by auto
  10.406 +  hence set2_incl: "\<And> c. c \<in> set_of P \<Longrightarrow> set2 c \<subseteq> B2" using N2 by blast
  10.407 +  have set2_disj: "\<And> c c'. c \<noteq> c' \<Longrightarrow> set2 c \<inter> set2 c' = {}"
  10.408 +    unfolding set2_def by auto
  10.409 +  have setsum_set2: "\<And> c. setsum (count N2) (set2 c) = count P c"
  10.410 +    unfolding P2 set2_def by transfer (auto intro: setsum_cong)
  10.411 +
  10.412 +  have ss: "\<And> c. c \<in> set_of P \<Longrightarrow> setsum (count N1) (set1 c) = setsum (count N2) (set2 c)"
  10.413 +    unfolding setsum_set1 setsum_set2 ..
  10.414 +  have "\<forall> c \<in> set_of P. \<forall> b1b2 \<in> (set1 c) \<times> (set2 c).
  10.415 +          \<exists> a \<in> A. p1 a = fst b1b2 \<and> p2 a = snd b1b2"
  10.416 +    using wp set1_incl set2_incl unfolding wpull_def Ball_def mem_Collect_eq
  10.417 +    by simp (metis set1 set2 set_rev_mp)
  10.418 +  then obtain uu where uu:
  10.419 +  "\<forall> c \<in> set_of P. \<forall> b1b2 \<in> (set1 c) \<times> (set2 c).
  10.420 +     uu c b1b2 \<in> A \<and> p1 (uu c b1b2) = fst b1b2 \<and> p2 (uu c b1b2) = snd b1b2" by metis
  10.421 +  def u \<equiv> "\<lambda> c b1 b2. uu c (b1,b2)"
  10.422 +  have u[simp]:
  10.423 +  "\<And> c b1 b2. \<lbrakk>c \<in> set_of P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk> \<Longrightarrow> u c b1 b2 \<in> A"
  10.424 +  "\<And> c b1 b2. \<lbrakk>c \<in> set_of P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk> \<Longrightarrow> p1 (u c b1 b2) = b1"
  10.425 +  "\<And> c b1 b2. \<lbrakk>c \<in> set_of P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk> \<Longrightarrow> p2 (u c b1 b2) = b2"
  10.426 +    using uu unfolding u_def by auto
  10.427 +  {fix c assume c: "c \<in> set_of P"
  10.428 +   have "inj2 (u c) (set1 c) (set2 c)" unfolding inj2_def proof clarify
  10.429 +     fix b1 b1' b2 b2'
  10.430 +     assume "{b1, b1'} \<subseteq> set1 c" "{b2, b2'} \<subseteq> set2 c" and 0: "u c b1 b2 = u c b1' b2'"
  10.431 +     hence "p1 (u c b1 b2) = b1 \<and> p2 (u c b1 b2) = b2 \<and>
  10.432 +            p1 (u c b1' b2') = b1' \<and> p2 (u c b1' b2') = b2'"
  10.433 +     using u(2)[OF c] u(3)[OF c] by simp metis
  10.434 +     thus "b1 = b1' \<and> b2 = b2'" using 0 by auto
  10.435 +   qed
  10.436 +  } note inj = this
  10.437 +  def sset \<equiv> "\<lambda> c. {u c b1 b2 | b1 b2. b1 \<in> set1 c \<and> b2 \<in> set2 c}"
  10.438 +  have fin_sset[simp]: "\<And> c. c \<in> set_of P \<Longrightarrow> finite (sset c)" unfolding sset_def
  10.439 +    using fin_set1 fin_set2 finite_twosets by blast
  10.440 +  have sset_A: "\<And> c. c \<in> set_of P \<Longrightarrow> sset c \<subseteq> A" unfolding sset_def by auto
  10.441 +  {fix c a assume c: "c \<in> set_of P" and ac: "a \<in> sset c"
  10.442 +   then obtain b1 b2 where b1: "b1 \<in> set1 c" and b2: "b2 \<in> set2 c"
  10.443 +   and a: "a = u c b1 b2" unfolding sset_def by auto
  10.444 +   have "p1 a \<in> set1 c" and p2a: "p2 a \<in> set2 c"
  10.445 +   using ac a b1 b2 c u(2) u(3) by simp+
  10.446 +   hence "u c (p1 a) (p2 a) = a" unfolding a using b1 b2 inj[OF c]
  10.447 +   unfolding inj2_def by (metis c u(2) u(3))
  10.448 +  } note u_p12[simp] = this
  10.449 +  {fix c a assume c: "c \<in> set_of P" and ac: "a \<in> sset c"
  10.450 +   hence "p1 a \<in> set1 c" unfolding sset_def by auto
  10.451 +  }note p1[simp] = this
  10.452 +  {fix c a assume c: "c \<in> set_of P" and ac: "a \<in> sset c"
  10.453 +   hence "p2 a \<in> set2 c" unfolding sset_def by auto
  10.454 +  }note p2[simp] = this
  10.455 +
  10.456 +  {fix c assume c: "c \<in> set_of P"
  10.457 +   hence "\<exists> M. (\<forall> b1 \<in> set1 c. setsum (\<lambda> b2. M (u c b1 b2)) (set2 c) = count N1 b1) \<and>
  10.458 +               (\<forall> b2 \<in> set2 c. setsum (\<lambda> b1. M (u c b1 b2)) (set1 c) = count N2 b2)"
  10.459 +   unfolding sset_def
  10.460 +   using matrix_setsum_finite[OF set1_NE[OF c] fin_set1[OF c]
  10.461 +                                 set2_NE[OF c] fin_set2[OF c] inj[OF c] ss[OF c]] by auto
  10.462 +  }
  10.463 +  then obtain Ms where
  10.464 +  ss1: "\<And> c b1. \<lbrakk>c \<in> set_of P; b1 \<in> set1 c\<rbrakk> \<Longrightarrow>
  10.465 +                   setsum (\<lambda> b2. Ms c (u c b1 b2)) (set2 c) = count N1 b1" and
  10.466 +  ss2: "\<And> c b2. \<lbrakk>c \<in> set_of P; b2 \<in> set2 c\<rbrakk> \<Longrightarrow>
  10.467 +                   setsum (\<lambda> b1. Ms c (u c b1 b2)) (set1 c) = count N2 b2"
  10.468 +  by metis
  10.469 +  def SET \<equiv> "\<Union> c \<in> set_of P. sset c"
  10.470 +  have fin_SET[simp]: "finite SET" unfolding SET_def apply(rule finite_UN_I) by auto
  10.471 +  have SET_A: "SET \<subseteq> A" unfolding SET_def using sset_A by blast
  10.472 +  have u_SET[simp]: "\<And> c b1 b2. \<lbrakk>c \<in> set_of P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk> \<Longrightarrow> u c b1 b2 \<in> SET"
  10.473 +    unfolding SET_def sset_def by blast
  10.474 +  {fix c a assume c: "c \<in> set_of P" and a: "a \<in> SET" and p1a: "p1 a \<in> set1 c"
  10.475 +   then obtain c' where c': "c' \<in> set_of P" and ac': "a \<in> sset c'"
  10.476 +    unfolding SET_def by auto
  10.477 +   hence "p1 a \<in> set1 c'" unfolding sset_def by auto
  10.478 +   hence eq: "c = c'" using p1a c c' set1_disj by auto
  10.479 +   hence "a \<in> sset c" using ac' by simp
  10.480 +  } note p1_rev = this
  10.481 +  {fix c a assume c: "c \<in> set_of P" and a: "a \<in> SET" and p2a: "p2 a \<in> set2 c"
  10.482 +   then obtain c' where c': "c' \<in> set_of P" and ac': "a \<in> sset c'"
  10.483 +   unfolding SET_def by auto
  10.484 +   hence "p2 a \<in> set2 c'" unfolding sset_def by auto
  10.485 +   hence eq: "c = c'" using p2a c c' set2_disj by auto
  10.486 +   hence "a \<in> sset c" using ac' by simp
  10.487 +  } note p2_rev = this
  10.488 +
  10.489 +  have "\<forall> a \<in> SET. \<exists> c \<in> set_of P. a \<in> sset c" unfolding SET_def by auto
  10.490 +  then obtain h where h: "\<forall> a \<in> SET. h a \<in> set_of P \<and> a \<in> sset (h a)" by metis
  10.491 +  have h_u[simp]: "\<And> c b1 b2. \<lbrakk>c \<in> set_of P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk>
  10.492 +                      \<Longrightarrow> h (u c b1 b2) = c"
  10.493 +  by (metis h p2 set2 u(3) u_SET)
  10.494 +  have h_u1: "\<And> c b1 b2. \<lbrakk>c \<in> set_of P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk>
  10.495 +                      \<Longrightarrow> h (u c b1 b2) = f1 b1"
  10.496 +  using h unfolding sset_def by auto
  10.497 +  have h_u2: "\<And> c b1 b2. \<lbrakk>c \<in> set_of P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk>
  10.498 +                      \<Longrightarrow> h (u c b1 b2) = f2 b2"
  10.499 +  using h unfolding sset_def by auto
  10.500 +  def M \<equiv>
  10.501 +    "Abs_multiset (\<lambda> a. if a \<in> SET \<and> p1 a \<in> set_of N1 \<and> p2 a \<in> set_of N2 then Ms (h a) a else 0)"
  10.502 +  have "(\<lambda> a. if a \<in> SET \<and> p1 a \<in> set_of N1 \<and> p2 a \<in> set_of N2 then Ms (h a) a else 0) \<in> multiset"
  10.503 +    unfolding multiset_def by auto
  10.504 +  hence [transfer_rule]: "pcr_multiset op = (\<lambda> a. if a \<in> SET \<and> p1 a \<in> set_of N1 \<and> p2 a \<in> set_of N2 then Ms (h a) a else 0) M"
  10.505 +    unfolding M_def pcr_multiset_def cr_multiset_def by (auto simp: Abs_multiset_inverse)
  10.506 +  have sM: "set_of M \<subseteq> SET" "set_of M \<subseteq> p1 -` (set_of N1)" "set_of M \<subseteq> p2 -` set_of N2"
  10.507 +    by (transfer, auto split: split_if_asm)+
  10.508 +  show "\<exists>M. set_of M \<subseteq> A \<and> mmap p1 M = N1 \<and> mmap p2 M = N2"
  10.509 +  proof(rule exI[of _ M], safe)
  10.510 +    fix a assume *: "a \<in> set_of M"
  10.511 +    from SET_A show "a \<in> A"
  10.512 +    proof (cases "a \<in> SET")
  10.513 +      case False thus ?thesis using * by transfer' auto
  10.514 +    qed blast
  10.515 +  next
  10.516 +    show "mmap p1 M = N1"
  10.517 +    proof(intro multiset_eqI)
  10.518 +      fix b1
  10.519 +      let ?K = "{a. p1 a = b1 \<and> a \<in># M}"
  10.520 +      have "setsum (count M) ?K = count N1 b1"
  10.521 +      proof(cases "b1 \<in> set_of N1")
  10.522 +        case False
  10.523 +        hence "?K = {}" using sM(2) by auto
  10.524 +        thus ?thesis using False by auto
  10.525 +      next
  10.526 +        case True
  10.527 +        def c \<equiv> "f1 b1"
  10.528 +        have c: "c \<in> set_of P" and b1: "b1 \<in> set1 c"
  10.529 +          unfolding set1_def c_def P1 using True by (auto simp: comp_eq_dest[OF set_of_mmap])
  10.530 +        with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p1 a = b1 \<and> a \<in> SET}"
  10.531 +          by transfer (force intro: setsum_mono_zero_cong_left split: split_if_asm)
  10.532 +        also have "... = setsum (count M) ((\<lambda> b2. u c b1 b2) ` (set2 c))"
  10.533 +          apply(rule setsum_cong) using c b1 proof safe
  10.534 +          fix a assume p1a: "p1 a \<in> set1 c" and "c \<in> set_of P" and "a \<in> SET"
  10.535 +          hence ac: "a \<in> sset c" using p1_rev by auto
  10.536 +          hence "a = u c (p1 a) (p2 a)" using c by auto
  10.537 +          moreover have "p2 a \<in> set2 c" using ac c by auto
  10.538 +          ultimately show "a \<in> u c (p1 a) ` set2 c" by auto
  10.539 +        qed auto
  10.540 +        also have "... = setsum (\<lambda> b2. count M (u c b1 b2)) (set2 c)"
  10.541 +          unfolding comp_def[symmetric] apply(rule setsum_reindex)
  10.542 +          using inj unfolding inj_on_def inj2_def using b1 c u(3) by blast
  10.543 +        also have "... = count N1 b1" unfolding ss1[OF c b1, symmetric]
  10.544 +          apply(rule setsum_cong[OF refl]) apply (transfer fixing: Ms u c b1 set2)
  10.545 +          using True h_u[OF c b1] set2_def u(2,3)[OF c b1] u_SET[OF c b1] by fastforce
  10.546 +        finally show ?thesis .
  10.547 +      qed
  10.548 +      thus "count (mmap p1 M) b1 = count N1 b1" by transfer
  10.549 +    qed
  10.550 +  next
  10.551 +    show "mmap p2 M = N2"
  10.552 +    proof(intro multiset_eqI)
  10.553 +      fix b2
  10.554 +      let ?K = "{a. p2 a = b2 \<and> a \<in># M}"
  10.555 +      have "setsum (count M) ?K = count N2 b2"
  10.556 +      proof(cases "b2 \<in> set_of N2")
  10.557 +        case False
  10.558 +        hence "?K = {}" using sM(3) by auto
  10.559 +        thus ?thesis using False by auto
  10.560 +      next
  10.561 +        case True
  10.562 +        def c \<equiv> "f2 b2"
  10.563 +        have c: "c \<in> set_of P" and b2: "b2 \<in> set2 c"
  10.564 +          unfolding set2_def c_def P2 using True by (auto simp: comp_eq_dest[OF set_of_mmap])
  10.565 +        with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p2 a = b2 \<and> a \<in> SET}"
  10.566 +          by transfer (force intro: setsum_mono_zero_cong_left split: split_if_asm)
  10.567 +        also have "... = setsum (count M) ((\<lambda> b1. u c b1 b2) ` (set1 c))"
  10.568 +          apply(rule setsum_cong) using c b2 proof safe
  10.569 +          fix a assume p2a: "p2 a \<in> set2 c" and "c \<in> set_of P" and "a \<in> SET"
  10.570 +          hence ac: "a \<in> sset c" using p2_rev by auto
  10.571 +          hence "a = u c (p1 a) (p2 a)" using c by auto
  10.572 +          moreover have "p1 a \<in> set1 c" using ac c by auto
  10.573 +          ultimately show "a \<in> (\<lambda>x. u c x (p2 a)) ` set1 c" by auto
  10.574 +        qed auto
  10.575 +        also have "... = setsum (count M o (\<lambda> b1. u c b1 b2)) (set1 c)"
  10.576 +          apply(rule setsum_reindex)
  10.577 +          using inj unfolding inj_on_def inj2_def using b2 c u(2) by blast
  10.578 +        also have "... = setsum (\<lambda> b1. count M (u c b1 b2)) (set1 c)" by simp
  10.579 +        also have "... = count N2 b2" unfolding ss2[OF c b2, symmetric] comp_def
  10.580 +          apply(rule setsum_cong[OF refl]) apply (transfer fixing: Ms u c b2 set1)
  10.581 +          using True h_u1[OF c _ b2] u(2,3)[OF c _ b2] u_SET[OF c _ b2] set1_def by fastforce
  10.582 +        finally show ?thesis .
  10.583 +      qed
  10.584 +      thus "count (mmap p2 M) b2 = count N2 b2" by transfer
  10.585 +    qed
  10.586 +  qed
  10.587 +qed
  10.588 +
  10.589 +lemma set_of_bd: "(card_of (set_of x), natLeq) \<in> ordLeq"
  10.590 +  by transfer
  10.591 +    (auto intro!: ordLess_imp_ordLeq simp: finite_iff_ordLess_natLeq[symmetric] multiset_def)
  10.592 +
  10.593 +lemma wppull_mmap:
  10.594 +  assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
  10.595 +  shows "wppull {M. set_of M \<subseteq> A} {N1. set_of N1 \<subseteq> B1} {N2. set_of N2 \<subseteq> B2}
  10.596 +    (mmap f1) (mmap f2) (mmap e1) (mmap e2) (mmap p1) (mmap p2)"
  10.597 +proof -
  10.598 +  from assms obtain j where j: "\<forall>a'\<in>thePull B1 B2 f1 f2.
  10.599 +    j a' \<in> A \<and> e1 (p1 (j a')) = e1 (fst a') \<and> e2 (p2 (j a')) = e2 (snd a')" 
  10.600 +    by (blast dest: wppull_thePull)
  10.601 +  then show ?thesis
  10.602 +    by (intro wpull_wppull[OF wpull_mmap[OF wpull_thePull], of _ _ _ _ "mmap j"])
  10.603 +      (auto simp: comp_eq_dest_lhs[OF mmap_comp[symmetric]] comp_eq_dest[OF set_of_mmap]
  10.604 +        intro!: mmap_cong simp del: mem_set_of_iff simp: mem_set_of_iff[symmetric])
  10.605 +qed
  10.606 +
  10.607 +bnf "'a multiset"
  10.608 +  map: mmap
  10.609 +  sets: set_of 
  10.610 +  bd: natLeq
  10.611 +  wits: "{#}"
  10.612 +by (auto simp add: mmap_id0 mmap_comp set_of_mmap natLeq_card_order natLeq_cinfinite set_of_bd
  10.613 +  Grp_def relcompp.simps intro: mmap_cong)
  10.614 +  (metis wppull_mmap[OF wppull_fstOp_sndOp, unfolded wppull_def
  10.615 +    o_eq_dest_lhs[OF mmap_comp[symmetric]] fstOp_def sndOp_def comp_def, simplified])
  10.616 +
  10.617 +inductive rel_multiset' where
  10.618 +  Zero[intro]: "rel_multiset' R {#} {#}"
  10.619 +| Plus[intro]: "\<lbrakk>R a b; rel_multiset' R M N\<rbrakk> \<Longrightarrow> rel_multiset' R (M + {#a#}) (N + {#b#})"
  10.620 +
  10.621 +lemma map_multiset_Zero_iff[simp]: "mmap f M = {#} \<longleftrightarrow> M = {#}"
  10.622 +by (metis image_is_empty multiset.set_map set_of_eq_empty_iff)
  10.623 +
  10.624 +lemma map_multiset_Zero[simp]: "mmap f {#} = {#}" by simp
  10.625 +
  10.626 +lemma rel_multiset_Zero: "rel_multiset R {#} {#}"
  10.627 +unfolding rel_multiset_def Grp_def by auto
  10.628 +
  10.629 +declare multiset.count[simp]
  10.630 +declare Abs_multiset_inverse[simp]
  10.631 +declare multiset.count_inverse[simp]
  10.632 +declare union_preserves_multiset[simp]
  10.633 +
  10.634 +lemma map_multiset_Plus[simp]: "mmap f (M1 + M2) = mmap f M1 + mmap f M2"
  10.635 +proof (intro multiset_eqI, transfer fixing: f)
  10.636 +  fix x :: 'a and M1 M2 :: "'b \<Rightarrow> nat"
  10.637 +  assume "M1 \<in> multiset" "M2 \<in> multiset"
  10.638 +  hence "setsum M1 {a. f a = x \<and> 0 < M1 a} = setsum M1 {a. f a = x \<and> 0 < M1 a + M2 a}"
  10.639 +        "setsum M2 {a. f a = x \<and> 0 < M2 a} = setsum M2 {a. f a = x \<and> 0 < M1 a + M2 a}"
  10.640 +    by (auto simp: multiset_def intro!: setsum_mono_zero_cong_left)
  10.641 +  then show "(\<Sum>a | f a = x \<and> 0 < M1 a + M2 a. M1 a + M2 a) =
  10.642 +       setsum M1 {a. f a = x \<and> 0 < M1 a} +
  10.643 +       setsum M2 {a. f a = x \<and> 0 < M2 a}"
  10.644 +    by (auto simp: setsum.distrib[symmetric])
  10.645 +qed
  10.646 +
  10.647 +lemma map_multiset_single[simp]: "mmap f {#a#} = {#f a#}"
  10.648 +  by transfer auto
  10.649 +
  10.650 +lemma rel_multiset_Plus:
  10.651 +assumes ab: "R a b" and MN: "rel_multiset R M N"
  10.652 +shows "rel_multiset R (M + {#a#}) (N + {#b#})"
  10.653 +proof-
  10.654 +  {fix y assume "R a b" and "set_of y \<subseteq> {(x, y). R x y}"
  10.655 +   hence "\<exists>ya. mmap fst y + {#a#} = mmap fst ya \<and>
  10.656 +               mmap snd y + {#b#} = mmap snd ya \<and>
  10.657 +               set_of ya \<subseteq> {(x, y). R x y}"
  10.658 +   apply(intro exI[of _ "y + {#(a,b)#}"]) by auto
  10.659 +  }
  10.660 +  thus ?thesis
  10.661 +  using assms
  10.662 +  unfolding rel_multiset_def Grp_def by force
  10.663 +qed
  10.664 +
  10.665 +lemma rel_multiset'_imp_rel_multiset:
  10.666 +"rel_multiset' R M N \<Longrightarrow> rel_multiset R M N"
  10.667 +apply(induct rule: rel_multiset'.induct)
  10.668 +using rel_multiset_Zero rel_multiset_Plus by auto
  10.669 +
  10.670 +lemma mcard_mmap[simp]: "mcard (mmap f M) = mcard M"
  10.671 +proof -
  10.672 +  def A \<equiv> "\<lambda> b. {a. f a = b \<and> a \<in># M}"
  10.673 +  let ?B = "{b. 0 < setsum (count M) (A b)}"
  10.674 +  have "{b. \<exists>a. f a = b \<and> a \<in># M} \<subseteq> f ` {a. a \<in># M}" by auto
  10.675 +  moreover have "finite (f ` {a. a \<in># M})" apply(rule finite_imageI)
  10.676 +  using finite_Collect_mem .
  10.677 +  ultimately have fin: "finite {b. \<exists>a. f a = b \<and> a \<in># M}" by(rule finite_subset)
  10.678 +  have i: "inj_on A ?B" unfolding inj_on_def A_def apply clarsimp
  10.679 +    by (metis (lifting, full_types) mem_Collect_eq neq0_conv setsum.neutral)
  10.680 +  have 0: "\<And> b. 0 < setsum (count M) (A b) \<longleftrightarrow> (\<exists> a \<in> A b. count M a > 0)"
  10.681 +  apply safe
  10.682 +    apply (metis less_not_refl setsum_gt_0_iff setsum_infinite)
  10.683 +    by (metis A_def finite_Collect_conjI finite_Collect_mem setsum_gt_0_iff)
  10.684 +  hence AB: "A ` ?B = {A b | b. \<exists> a \<in> A b. count M a > 0}" by auto
  10.685 +
  10.686 +  have "setsum (\<lambda> x. setsum (count M) (A x)) ?B = setsum (setsum (count M) o A) ?B"
  10.687 +  unfolding comp_def ..
  10.688 +  also have "... = (\<Sum>x\<in> A ` ?B. setsum (count M) x)"
  10.689 +  unfolding setsum.reindex [OF i, symmetric] ..
  10.690 +  also have "... = setsum (count M) (\<Union>x\<in>A ` {b. 0 < setsum (count M) (A b)}. x)"
  10.691 +  (is "_ = setsum (count M) ?J")
  10.692 +  apply(rule setsum.UNION_disjoint[symmetric])
  10.693 +  using 0 fin unfolding A_def by auto
  10.694 +  also have "?J = {a. a \<in># M}" unfolding AB unfolding A_def by auto
  10.695 +  finally have "setsum (\<lambda> x. setsum (count M) (A x)) ?B =
  10.696 +                setsum (count M) {a. a \<in># M}" .
  10.697 +  then show ?thesis unfolding mcard_unfold_setsum A_def by transfer
  10.698 +qed
  10.699 +
  10.700 +lemma rel_multiset_mcard:
  10.701 +assumes "rel_multiset R M N"
  10.702 +shows "mcard M = mcard N"
  10.703 +using assms unfolding rel_multiset_def Grp_def by auto
  10.704 +
  10.705 +lemma multiset_induct2[case_names empty addL addR]:
  10.706 +assumes empty: "P {#} {#}"
  10.707 +and addL: "\<And>M N a. P M N \<Longrightarrow> P (M + {#a#}) N"
  10.708 +and addR: "\<And>M N a. P M N \<Longrightarrow> P M (N + {#a#})"
  10.709 +shows "P M N"
  10.710 +apply(induct N rule: multiset_induct)
  10.711 +  apply(induct M rule: multiset_induct, rule empty, erule addL)
  10.712 +  apply(induct M rule: multiset_induct, erule addR, erule addR)
  10.713 +done
  10.714 +
  10.715 +lemma multiset_induct2_mcard[consumes 1, case_names empty add]:
  10.716 +assumes c: "mcard M = mcard N"
  10.717 +and empty: "P {#} {#}"
  10.718 +and add: "\<And>M N a b. P M N \<Longrightarrow> P (M + {#a#}) (N + {#b#})"
  10.719 +shows "P M N"
  10.720 +using c proof(induct M arbitrary: N rule: measure_induct_rule[of mcard])
  10.721 +  case (less M)  show ?case
  10.722 +  proof(cases "M = {#}")
  10.723 +    case True hence "N = {#}" using less.prems by auto
  10.724 +    thus ?thesis using True empty by auto
  10.725 +  next
  10.726 +    case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split)
  10.727 +    have "N \<noteq> {#}" using False less.prems by auto
  10.728 +    then obtain N1 b where N: "N = N1 + {#b#}" by (metis multi_nonempty_split)
  10.729 +    have "mcard M1 = mcard N1" using less.prems unfolding M N by auto
  10.730 +    thus ?thesis using M N less.hyps add by auto
  10.731 +  qed
  10.732 +qed
  10.733 +
  10.734 +lemma msed_map_invL:
  10.735 +assumes "mmap f (M + {#a#}) = N"
  10.736 +shows "\<exists> N1. N = N1 + {#f a#} \<and> mmap f M = N1"
  10.737 +proof-
  10.738 +  have "f a \<in># N"
  10.739 +  using assms multiset.set_map[of f "M + {#a#}"] by auto
  10.740 +  then obtain N1 where N: "N = N1 + {#f a#}" using multi_member_split by metis
  10.741 +  have "mmap f M = N1" using assms unfolding N by simp
  10.742 +  thus ?thesis using N by blast
  10.743 +qed
  10.744 +
  10.745 +lemma msed_map_invR:
  10.746 +assumes "mmap f M = N + {#b#}"
  10.747 +shows "\<exists> M1 a. M = M1 + {#a#} \<and> f a = b \<and> mmap f M1 = N"
  10.748 +proof-
  10.749 +  obtain a where a: "a \<in># M" and fa: "f a = b"
  10.750 +  using multiset.set_map[of f M] unfolding assms
  10.751 +  by (metis image_iff mem_set_of_iff union_single_eq_member)
  10.752 +  then obtain M1 where M: "M = M1 + {#a#}" using multi_member_split by metis
  10.753 +  have "mmap f M1 = N" using assms unfolding M fa[symmetric] by simp
  10.754 +  thus ?thesis using M fa by blast
  10.755 +qed
  10.756 +
  10.757 +lemma msed_rel_invL:
  10.758 +assumes "rel_multiset R (M + {#a#}) N"
  10.759 +shows "\<exists> N1 b. N = N1 + {#b#} \<and> R a b \<and> rel_multiset R M N1"
  10.760 +proof-
  10.761 +  obtain K where KM: "mmap fst K = M + {#a#}"
  10.762 +  and KN: "mmap snd K = N" and sK: "set_of K \<subseteq> {(a, b). R a b}"
  10.763 +  using assms
  10.764 +  unfolding rel_multiset_def Grp_def by auto
  10.765 +  obtain K1 ab where K: "K = K1 + {#ab#}" and a: "fst ab = a"
  10.766 +  and K1M: "mmap fst K1 = M" using msed_map_invR[OF KM] by auto
  10.767 +  obtain N1 where N: "N = N1 + {#snd ab#}" and K1N1: "mmap snd K1 = N1"
  10.768 +  using msed_map_invL[OF KN[unfolded K]] by auto
  10.769 +  have Rab: "R a (snd ab)" using sK a unfolding K by auto
  10.770 +  have "rel_multiset R M N1" using sK K1M K1N1
  10.771 +  unfolding K rel_multiset_def Grp_def by auto
  10.772 +  thus ?thesis using N Rab by auto
  10.773 +qed
  10.774 +
  10.775 +lemma msed_rel_invR:
  10.776 +assumes "rel_multiset R M (N + {#b#})"
  10.777 +shows "\<exists> M1 a. M = M1 + {#a#} \<and> R a b \<and> rel_multiset R M1 N"
  10.778 +proof-
  10.779 +  obtain K where KN: "mmap snd K = N + {#b#}"
  10.780 +  and KM: "mmap fst K = M" and sK: "set_of K \<subseteq> {(a, b). R a b}"
  10.781 +  using assms
  10.782 +  unfolding rel_multiset_def Grp_def by auto
  10.783 +  obtain K1 ab where K: "K = K1 + {#ab#}" and b: "snd ab = b"
  10.784 +  and K1N: "mmap snd K1 = N" using msed_map_invR[OF KN] by auto
  10.785 +  obtain M1 where M: "M = M1 + {#fst ab#}" and K1M1: "mmap fst K1 = M1"
  10.786 +  using msed_map_invL[OF KM[unfolded K]] by auto
  10.787 +  have Rab: "R (fst ab) b" using sK b unfolding K by auto
  10.788 +  have "rel_multiset R M1 N" using sK K1N K1M1
  10.789 +  unfolding K rel_multiset_def Grp_def by auto
  10.790 +  thus ?thesis using M Rab by auto
  10.791 +qed
  10.792 +
  10.793 +lemma rel_multiset_imp_rel_multiset':
  10.794 +assumes "rel_multiset R M N"
  10.795 +shows "rel_multiset' R M N"
  10.796 +using assms proof(induct M arbitrary: N rule: measure_induct_rule[of mcard])
  10.797 +  case (less M)
  10.798 +  have c: "mcard M = mcard N" using rel_multiset_mcard[OF less.prems] .
  10.799 +  show ?case
  10.800 +  proof(cases "M = {#}")
  10.801 +    case True hence "N = {#}" using c by simp
  10.802 +    thus ?thesis using True rel_multiset'.Zero by auto
  10.803 +  next
  10.804 +    case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split)
  10.805 +    obtain N1 b where N: "N = N1 + {#b#}" and R: "R a b" and ms: "rel_multiset R M1 N1"
  10.806 +    using msed_rel_invL[OF less.prems[unfolded M]] by auto
  10.807 +    have "rel_multiset' R M1 N1" using less.hyps[of M1 N1] ms unfolding M by simp
  10.808 +    thus ?thesis using rel_multiset'.Plus[of R a b, OF R] unfolding M N by simp
  10.809 +  qed
  10.810 +qed
  10.811 +
  10.812 +lemma rel_multiset_rel_multiset':
  10.813 +"rel_multiset R M N = rel_multiset' R M N"
  10.814 +using  rel_multiset_imp_rel_multiset' rel_multiset'_imp_rel_multiset by auto
  10.815 +
  10.816 +(* The main end product for rel_multiset: inductive characterization *)
  10.817 +theorems rel_multiset_induct[case_names empty add, induct pred: rel_multiset] =
  10.818 +         rel_multiset'.induct[unfolded rel_multiset_rel_multiset'[symmetric]]
  10.819 +
  10.820 +end
    11.1 --- a/src/HOL/Lifting_Option.thy	Thu Jan 23 19:02:22 2014 +0100
    11.2 +++ b/src/HOL/Lifting_Option.thy	Fri Jan 24 11:51:45 2014 +0100
    11.3 @@ -1,5 +1,6 @@
    11.4  (*  Title:      HOL/Lifting_Option.thy
    11.5      Author:     Brian Huffman and Ondrej Kuncar
    11.6 +    Author:     Andreas Lochbihler, Karlsruhe Institute of Technology
    11.7  *)
    11.8  
    11.9  header {* Setup for Lifting/Transfer for the option type *}
   11.10 @@ -114,4 +115,57 @@
   11.11  
   11.12  end
   11.13  
   11.14 +
   11.15 +subsubsection {* BNF setup *}
   11.16 +
   11.17 +lemma option_rec_conv_option_case: "option_rec = option_case"
   11.18 +by (simp add: fun_eq_iff split: option.split)
   11.19 +
   11.20 +bnf "'a option"
   11.21 +  map: Option.map
   11.22 +  sets: Option.set
   11.23 +  bd: natLeq
   11.24 +  wits: None
   11.25 +  rel: option_rel
   11.26 +proof -
   11.27 +  show "Option.map id = id" by (rule Option.map.id)
   11.28 +next
   11.29 +  fix f g
   11.30 +  show "Option.map (g \<circ> f) = Option.map g \<circ> Option.map f"
   11.31 +    by (auto simp add: fun_eq_iff Option.map_def split: option.split)
   11.32 +next
   11.33 +  fix f g x
   11.34 +  assume "\<And>z. z \<in> Option.set x \<Longrightarrow> f z = g z"
   11.35 +  thus "Option.map f x = Option.map g x"
   11.36 +    by (simp cong: Option.map_cong)
   11.37 +next
   11.38 +  fix f
   11.39 +  show "Option.set \<circ> Option.map f = op ` f \<circ> Option.set"
   11.40 +    by fastforce
   11.41 +next
   11.42 +  show "card_order natLeq" by (rule natLeq_card_order)
   11.43 +next
   11.44 +  show "cinfinite natLeq" by (rule natLeq_cinfinite)
   11.45 +next
   11.46 +  fix x
   11.47 +  show "|Option.set x| \<le>o natLeq"
   11.48 +    by (cases x) (simp_all add: ordLess_imp_ordLeq finite_iff_ordLess_natLeq[symmetric])
   11.49 +next
   11.50 +  fix R S
   11.51 +  show "option_rel R OO option_rel S \<le> option_rel (R OO S)"
   11.52 +    by (auto simp: option_rel_def split: option.splits)
   11.53 +next
   11.54 +  fix z
   11.55 +  assume "z \<in> Option.set None"
   11.56 +  thus False by simp
   11.57 +next
   11.58 +  fix R
   11.59 +  show "option_rel R =
   11.60 +        (Grp {x. Option.set x \<subseteq> Collect (split R)} (Option.map fst))\<inverse>\<inverse> OO
   11.61 +         Grp {x. Option.set x \<subseteq> Collect (split R)} (Option.map snd)"
   11.62 +  unfolding option_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff prod.cases
   11.63 +  by (auto simp: trans[OF eq_commute option_map_is_None] trans[OF eq_commute option_map_eq_Some]
   11.64 +           split: option.splits)
   11.65 +qed
   11.66 +
   11.67  end
    12.1 --- a/src/HOL/List.thy	Thu Jan 23 19:02:22 2014 +0100
    12.2 +++ b/src/HOL/List.thy	Fri Jan 24 11:51:45 2014 +0100
    12.3 @@ -5936,7 +5936,6 @@
    12.4  
    12.5  subsection {* Code generation *}
    12.6  
    12.7 -
    12.8  text{* Optional tail recursive version of @{const map}. Can avoid
    12.9  stack overflow in some target languages. *}
   12.10  
   12.11 @@ -6531,6 +6530,7 @@
   12.12    "wf (set xs) = acyclic (set xs)"
   12.13    by (simp add: wf_iff_acyclic_if_finite)
   12.14  
   12.15 +
   12.16  subsection {* Setup for Lifting/Transfer *}
   12.17  
   12.18  subsubsection {* Relator and predicator properties *}
   12.19 @@ -6879,4 +6879,46 @@
   12.20  
   12.21  end
   12.22  
   12.23 +
   12.24 +subsection {* BNF setup *}
   12.25 +
   12.26 +bnf "'a list"
   12.27 +  map: map
   12.28 +  sets: set
   12.29 +  bd: natLeq
   12.30 +  wits: Nil
   12.31 +  rel: list_all2
   12.32 +proof -
   12.33 +  show "map id = id" by (rule List.map.id)
   12.34 +next
   12.35 +  fix f g
   12.36 +  show "map (g o f) = map g o map f" by (rule List.map.comp[symmetric])
   12.37 +next
   12.38 +  fix x f g
   12.39 +  assume "\<And>z. z \<in> set x \<Longrightarrow> f z = g z"
   12.40 +  thus "map f x = map g x" by simp
   12.41 +next
   12.42 +  fix f
   12.43 +  show "set o map f = image f o set" by (rule ext, unfold comp_apply, rule set_map)
   12.44 +next
   12.45 +  show "card_order natLeq" by (rule natLeq_card_order)
   12.46 +next
   12.47 +  show "cinfinite natLeq" by (rule natLeq_cinfinite)
   12.48 +next
   12.49 +  fix x
   12.50 +  show "|set x| \<le>o natLeq"
   12.51 +    by (metis List.finite_set finite_iff_ordLess_natLeq ordLess_imp_ordLeq)
   12.52 +next
   12.53 +  fix R S
   12.54 +  show "list_all2 R OO list_all2 S \<le> list_all2 (R OO S)"
   12.55 +    by (metis list_all2_OO order_refl)
   12.56 +next
   12.57 +  fix R
   12.58 +  show "list_all2 R =
   12.59 +         (Grp {x. set x \<subseteq> {(x, y). R x y}} (map fst))\<inverse>\<inverse> OO
   12.60 +         Grp {x. set x \<subseteq> {(x, y). R x y}} (map snd)"
   12.61 +    unfolding list_all2_def[abs_def] Grp_def fun_eq_iff relcompp.simps conversep.simps
   12.62 +    by (force simp: zip_map_fst_snd)
   12.63 +qed simp
   12.64 +
   12.65  end
    13.1 --- a/src/HOL/Option.thy	Thu Jan 23 19:02:22 2014 +0100
    13.2 +++ b/src/HOL/Option.thy	Fri Jan 24 11:51:45 2014 +0100
    13.3 @@ -233,4 +233,3 @@
    13.4    Option None Some
    13.5  
    13.6  end
    13.7 -