Merge
authorpaulson <lp15@cam.ac.uk>
Fri Jan 24 16:54:25 2014 +0000 (2014-01-24)
changeset 551319808f186795c
parent 55130 70db8d380d62
parent 55129 26bd1cba3ab5
child 55132 ee5a0ca00b6f
child 55133 687656233ad8
child 55157 06897ea77f78
Merge
src/HOL/Library/More_BNFs.thy
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Fri Jan 24 15:21:00 2014 +0000
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Fri Jan 24 16:54:25 2014 +0000
     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	Fri Jan 24 15:21:00 2014 +0000
     2.2 +++ b/src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy	Fri Jan 24 16:54:25 2014 +0000
     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	Fri Jan 24 15:21:00 2014 +0000
     3.2 +++ b/src/HOL/BNF_Examples/Lambda_Term.thy	Fri Jan 24 16:54:25 2014 +0000
     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	Fri Jan 24 15:21:00 2014 +0000
     4.2 +++ b/src/HOL/BNF_Examples/Misc_Codatatype.thy	Fri Jan 24 16:54:25 2014 +0000
     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	Fri Jan 24 15:21:00 2014 +0000
     5.2 +++ b/src/HOL/BNF_Examples/Misc_Datatype.thy	Fri Jan 24 16:54:25 2014 +0000
     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	Fri Jan 24 15:21:00 2014 +0000
     6.2 +++ b/src/HOL/BNF_Examples/TreeFsetI.thy	Fri Jan 24 16:54:25 2014 +0000
     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/Cardinal_Notations.thy	Fri Jan 24 15:21:00 2014 +0000
     7.2 +++ b/src/HOL/Library/Cardinal_Notations.thy	Fri Jan 24 16:54:25 2014 +0000
     7.3 @@ -17,8 +17,13 @@
     7.4    ordLess2 (infix "<o" 50) and
     7.5    ordIso2 (infix "=o" 50) and
     7.6    card_of ("|_|") and
     7.7 -  csum (infixr "+c" 65) and
     7.8 -  cprod (infixr "*c" 80) and
     7.9 -  cexp (infixr "^c" 90)
    7.10 +  BNF_Cardinal_Arithmetic.csum (infixr "+c" 65) and
    7.11 +  BNF_Cardinal_Arithmetic.cprod (infixr "*c" 80) and
    7.12 +  BNF_Cardinal_Arithmetic.cexp (infixr "^c" 90)
    7.13 +
    7.14 +abbreviation "cinfinite \<equiv> BNF_Cardinal_Arithmetic.cinfinite"
    7.15 +abbreviation "czero \<equiv> BNF_Cardinal_Arithmetic.czero"
    7.16 +abbreviation "cone \<equiv> BNF_Cardinal_Arithmetic.cone"
    7.17 +abbreviation "ctwo \<equiv> BNF_Cardinal_Arithmetic.ctwo"
    7.18  
    7.19  end
     8.1 --- a/src/HOL/Library/FSet.thy	Fri Jan 24 15:21:00 2014 +0000
     8.2 +++ b/src/HOL/Library/FSet.thy	Fri Jan 24 16:54:25 2014 +0000
     8.3 @@ -1,12 +1,13 @@
     8.4  (*  Title:      HOL/Library/FSet.thy
     8.5      Author:     Ondrej Kuncar, TU Muenchen
     8.6      Author:     Cezary Kaliszyk and Christian Urban
     8.7 +    Author:     Andrei Popescu, TU Muenchen
     8.8  *)
     8.9  
    8.10  header {* Type of finite sets defined as a subtype of sets *}
    8.11  
    8.12  theory FSet
    8.13 -imports Main Conditionally_Complete_Lattices
    8.14 +imports Conditionally_Complete_Lattices
    8.15  begin
    8.16  
    8.17  subsection {* Definition of the type *}
    8.18 @@ -16,6 +17,7 @@
    8.19  
    8.20  setup_lifting type_definition_fset
    8.21  
    8.22 +
    8.23  subsection {* Basic operations and type class instantiations *}
    8.24  
    8.25  (* FIXME transfer and right_total vs. bi_total *)
    8.26 @@ -148,6 +150,7 @@
    8.27  abbreviation fUNIV :: "'a::finite fset" where "fUNIV \<equiv> top"
    8.28  abbreviation fuminus :: "'a::finite fset \<Rightarrow> 'a fset" ("|-| _" [81] 80) where "|-| x \<equiv> uminus x"
    8.29  
    8.30 +
    8.31  subsection {* Other operations *}
    8.32  
    8.33  lift_definition finsert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is insert parametric Lifting_Set.insert_transfer
    8.34 @@ -167,6 +170,7 @@
    8.35  
    8.36  context
    8.37  begin
    8.38 +
    8.39  interpretation lifting_syntax .
    8.40  
    8.41  lift_definition ffilter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Set.filter 
    8.42 @@ -203,6 +207,7 @@
    8.43  
    8.44  lift_definition ffold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" is Finite_Set.fold ..
    8.45  
    8.46 +
    8.47  subsection {* Transferred lemmas from Set.thy *}
    8.48  
    8.49  lemmas fset_eqI = set_eqI[Transfer.transferred]
    8.50 @@ -442,12 +447,14 @@
    8.51  lemmas ffmember_filter[simp] = member_filter[Transfer.transferred]
    8.52  lemmas fequalityI = equalityI[Transfer.transferred]
    8.53  
    8.54 +
    8.55  subsection {* Additional lemmas*}
    8.56  
    8.57  subsubsection {* @{text fsingleton} *}
    8.58  
    8.59  lemmas fsingletonE = fsingletonD [elim_format]
    8.60  
    8.61 +
    8.62  subsubsection {* @{text femepty} *}
    8.63  
    8.64  lemma fempty_ffilter[simp]: "ffilter (\<lambda>_. False) A = {||}"
    8.65 @@ -457,6 +464,7 @@
    8.66  lemma femptyE [elim!]: "a |\<in>| {||} \<Longrightarrow> P"
    8.67    by simp
    8.68  
    8.69 +
    8.70  subsubsection {* @{text fset} *}
    8.71  
    8.72  lemmas fset_simps[simp] = bot_fset.rep_eq finsert.rep_eq
    8.73 @@ -479,6 +487,7 @@
    8.74  
    8.75  lemmas minus_fset[simp] = minus_fset.rep_eq
    8.76  
    8.77 +
    8.78  subsubsection {* @{text filter_fset} *}
    8.79  
    8.80  lemma subset_ffilter: 
    8.81 @@ -494,6 +503,7 @@
    8.82      ffilter P A |\<subset>| ffilter Q A"
    8.83    unfolding less_fset_def by (auto simp add: subset_ffilter eq_ffilter)
    8.84  
    8.85 +
    8.86  subsubsection {* @{text finsert} *}
    8.87  
    8.88  (* FIXME, transferred doesn't work here *)
    8.89 @@ -505,11 +515,13 @@
    8.90  lemma mk_disjoint_finsert: "a |\<in>| A \<Longrightarrow> \<exists>B. A = finsert a B \<and> a |\<notin>| B"
    8.91    by (rule_tac x = "A |-| {|a|}" in exI, blast)
    8.92  
    8.93 +
    8.94  subsubsection {* @{text fimage} *}
    8.95  
    8.96  lemma subset_fimage_iff: "(B |\<subseteq>| f|`|A) = (\<exists> AA. AA |\<subseteq>| A \<and> B = f|`|AA)"
    8.97  by transfer (metis mem_Collect_eq rev_finite_subset subset_image_iff)
    8.98  
    8.99 +
   8.100  subsubsection {* bounded quantification *}
   8.101  
   8.102  lemma bex_simps [simp, no_atp]:
   8.103 @@ -540,6 +552,7 @@
   8.104  
   8.105  end
   8.106  
   8.107 +
   8.108  subsubsection {* @{text fcard} *}
   8.109  
   8.110  (* FIXME: improve transferred to handle bounded meta quantification *)
   8.111 @@ -622,6 +635,7 @@
   8.112  lemma fcard_pfsubset: "A |\<subseteq>| B \<Longrightarrow> fcard A < fcard B \<Longrightarrow> A < B"
   8.113  by transfer (rule card_psubset)
   8.114  
   8.115 +
   8.116  subsubsection {* @{text ffold} *}
   8.117  
   8.118  (* FIXME: improve transferred to handle bounded meta quantification *)
   8.119 @@ -680,6 +694,7 @@
   8.120  
   8.121  end
   8.122  
   8.123 +
   8.124  subsection {* Choice in fsets *}
   8.125  
   8.126  lemma fset_choice: 
   8.127 @@ -687,6 +702,7 @@
   8.128    shows "\<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"
   8.129    using assms by transfer metis
   8.130  
   8.131 +
   8.132  subsection {* Induction and Cases rules for fsets *}
   8.133  
   8.134  lemma fset_exhaust [case_names empty insert, cases type: fset]:
   8.135 @@ -752,6 +768,7 @@
   8.136    apply simp_all
   8.137    done
   8.138  
   8.139 +
   8.140  subsection {* Setup for Lifting/Transfer *}
   8.141  
   8.142  subsubsection {* Relator and predicator properties *}
   8.143 @@ -851,6 +868,7 @@
   8.144  
   8.145  lemmas fset_invariant_commute [invariant_commute] = set_invariant_commute[Transfer.transferred]
   8.146  
   8.147 +
   8.148  subsubsection {* Quotient theorem for the Lifting package *}
   8.149  
   8.150  lemma Quotient_fset_map[quot_map]:
   8.151 @@ -859,6 +877,7 @@
   8.152    using assms unfolding Quotient_alt_def4
   8.153    by (simp add: fset_rel_OO[symmetric] fset_rel_conversep) (simp add: fset_rel_alt_def, blast)
   8.154  
   8.155 +
   8.156  subsubsection {* Transfer rules for the Transfer package *}
   8.157  
   8.158  text {* Unconditional transfer rules *}
   8.159 @@ -971,4 +990,137 @@
   8.160  lifting_update fset.lifting
   8.161  lifting_forget fset.lifting
   8.162  
   8.163 +
   8.164 +subsection {* BNF setup *}
   8.165 +
   8.166 +context
   8.167 +includes fset.lifting
   8.168 +begin
   8.169 +
   8.170 +lemma fset_rel_alt:
   8.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)"
   8.172 +by transfer (simp add: set_rel_def)
   8.173 +
   8.174 +lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A"
   8.175 +apply (rule f_the_inv_into_f[unfolded inj_on_def])
   8.176 +apply (simp add: fset_inject)
   8.177 +apply (rule range_eqI Abs_fset_inverse[symmetric] CollectI)+
   8.178 +.
   8.179 +
   8.180 +lemma fset_rel_aux:
   8.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>
   8.182 + ((BNF_Util.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage fst))\<inverse>\<inverse> OO
   8.183 +  BNF_Util.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage snd)) a b" (is "?L = ?R")
   8.184 +proof
   8.185 +  assume ?L
   8.186 +  def R' \<equiv> "the_inv fset (Collect (split R) \<inter> (fset a \<times> fset b))" (is "the_inv fset ?L'")
   8.187 +  have "finite ?L'" by (intro finite_Int[OF disjI2] finite_cartesian_product) (transfer, simp)+
   8.188 +  hence *: "fset R' = ?L'" unfolding R'_def by (intro fset_to_fset)
   8.189 +  show ?R unfolding Grp_def relcompp.simps conversep.simps
   8.190 +  proof (intro CollectI prod_caseI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
   8.191 +    from * show "a = fimage fst R'" using conjunct1[OF `?L`]
   8.192 +      by (transfer, auto simp add: image_def Int_def split: prod.splits)
   8.193 +    from * show "b = fimage snd R'" using conjunct2[OF `?L`]
   8.194 +      by (transfer, auto simp add: image_def Int_def split: prod.splits)
   8.195 +  qed (auto simp add: *)
   8.196 +next
   8.197 +  assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps
   8.198 +  apply (simp add: subset_eq Ball_def)
   8.199 +  apply (rule conjI)
   8.200 +  apply (transfer, clarsimp, metis snd_conv)
   8.201 +  by (transfer, clarsimp, metis fst_conv)
   8.202 +qed
   8.203 +
   8.204 +bnf "'a fset"
   8.205 +  map: fimage
   8.206 +  sets: fset 
   8.207 +  bd: natLeq
   8.208 +  wits: "{||}"
   8.209 +  rel: fset_rel
   8.210 +apply -
   8.211 +          apply transfer' apply simp
   8.212 +         apply transfer' apply force
   8.213 +        apply transfer apply force
   8.214 +       apply transfer' apply force
   8.215 +      apply (rule natLeq_card_order)
   8.216 +     apply (rule natLeq_cinfinite)
   8.217 +    apply transfer apply (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq)
   8.218 +   apply (fastforce simp: fset_rel_alt)
   8.219 + apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff fset_rel_alt fset_rel_aux) 
   8.220 +apply transfer apply simp
   8.221 +done
   8.222 +
   8.223 +lemma fset_rel_fset: "set_rel \<chi> (fset A1) (fset A2) = fset_rel \<chi> A1 A2"
   8.224 +  by transfer (rule refl)
   8.225 +
   8.226  end
   8.227 +
   8.228 +lemmas [simp] = fset.map_comp fset.map_id fset.set_map
   8.229 +
   8.230 +
   8.231 +subsection {* Advanced relator customization *}
   8.232 +
   8.233 +(* Set vs. sum relators: *)
   8.234 +
   8.235 +lemma set_rel_sum_rel[simp]: 
   8.236 +"set_rel (sum_rel \<chi> \<phi>) A1 A2 \<longleftrightarrow> 
   8.237 + set_rel \<chi> (Inl -` A1) (Inl -` A2) \<and> set_rel \<phi> (Inr -` A1) (Inr -` A2)"
   8.238 +(is "?L \<longleftrightarrow> ?Rl \<and> ?Rr")
   8.239 +proof safe
   8.240 +  assume L: "?L"
   8.241 +  show ?Rl unfolding set_rel_def Bex_def vimage_eq proof safe
   8.242 +    fix l1 assume "Inl l1 \<in> A1"
   8.243 +    then obtain a2 where a2: "a2 \<in> A2" and "sum_rel \<chi> \<phi> (Inl l1) a2"
   8.244 +    using L unfolding set_rel_def by auto
   8.245 +    then obtain l2 where "a2 = Inl l2 \<and> \<chi> l1 l2" by (cases a2, auto)
   8.246 +    thus "\<exists> l2. Inl l2 \<in> A2 \<and> \<chi> l1 l2" using a2 by auto
   8.247 +  next
   8.248 +    fix l2 assume "Inl l2 \<in> A2"
   8.249 +    then obtain a1 where a1: "a1 \<in> A1" and "sum_rel \<chi> \<phi> a1 (Inl l2)"
   8.250 +    using L unfolding set_rel_def by auto
   8.251 +    then obtain l1 where "a1 = Inl l1 \<and> \<chi> l1 l2" by (cases a1, auto)
   8.252 +    thus "\<exists> l1. Inl l1 \<in> A1 \<and> \<chi> l1 l2" using a1 by auto
   8.253 +  qed
   8.254 +  show ?Rr unfolding set_rel_def Bex_def vimage_eq proof safe
   8.255 +    fix r1 assume "Inr r1 \<in> A1"
   8.256 +    then obtain a2 where a2: "a2 \<in> A2" and "sum_rel \<chi> \<phi> (Inr r1) a2"
   8.257 +    using L unfolding set_rel_def by auto
   8.258 +    then obtain r2 where "a2 = Inr r2 \<and> \<phi> r1 r2" by (cases a2, auto)
   8.259 +    thus "\<exists> r2. Inr r2 \<in> A2 \<and> \<phi> r1 r2" using a2 by auto
   8.260 +  next
   8.261 +    fix r2 assume "Inr r2 \<in> A2"
   8.262 +    then obtain a1 where a1: "a1 \<in> A1" and "sum_rel \<chi> \<phi> a1 (Inr r2)"
   8.263 +    using L unfolding set_rel_def by auto
   8.264 +    then obtain r1 where "a1 = Inr r1 \<and> \<phi> r1 r2" by (cases a1, auto)
   8.265 +    thus "\<exists> r1. Inr r1 \<in> A1 \<and> \<phi> r1 r2" using a1 by auto
   8.266 +  qed
   8.267 +next
   8.268 +  assume Rl: "?Rl" and Rr: "?Rr"
   8.269 +  show ?L unfolding set_rel_def Bex_def vimage_eq proof safe
   8.270 +    fix a1 assume a1: "a1 \<in> A1"
   8.271 +    show "\<exists> a2. a2 \<in> A2 \<and> sum_rel \<chi> \<phi> a1 a2"
   8.272 +    proof(cases a1)
   8.273 +      case (Inl l1) then obtain l2 where "Inl l2 \<in> A2 \<and> \<chi> l1 l2"
   8.274 +      using Rl a1 unfolding set_rel_def by blast
   8.275 +      thus ?thesis unfolding Inl by auto
   8.276 +    next
   8.277 +      case (Inr r1) then obtain r2 where "Inr r2 \<in> A2 \<and> \<phi> r1 r2"
   8.278 +      using Rr a1 unfolding set_rel_def by blast
   8.279 +      thus ?thesis unfolding Inr by auto
   8.280 +    qed
   8.281 +  next
   8.282 +    fix a2 assume a2: "a2 \<in> A2"
   8.283 +    show "\<exists> a1. a1 \<in> A1 \<and> sum_rel \<chi> \<phi> a1 a2"
   8.284 +    proof(cases a2)
   8.285 +      case (Inl l2) then obtain l1 where "Inl l1 \<in> A1 \<and> \<chi> l1 l2"
   8.286 +      using Rl a2 unfolding set_rel_def by blast
   8.287 +      thus ?thesis unfolding Inl by auto
   8.288 +    next
   8.289 +      case (Inr r2) then obtain r1 where "Inr r1 \<in> A1 \<and> \<phi> r1 r2"
   8.290 +      using Rr a2 unfolding set_rel_def by blast
   8.291 +      thus ?thesis unfolding Inr by auto
   8.292 +    qed
   8.293 +  qed
   8.294 +qed
   8.295 +
   8.296 +end
     9.1 --- a/src/HOL/Library/Library.thy	Fri Jan 24 15:21:00 2014 +0000
     9.2 +++ b/src/HOL/Library/Library.thy	Fri Jan 24 16:54:25 2014 +0000
     9.3 @@ -38,7 +38,6 @@
     9.4    Kleene_Algebra
     9.5    Mapping
     9.6    Monad_Syntax
     9.7 -  More_BNFs
     9.8    Multiset
     9.9    Numeral_Type
    9.10    OptionalSugar
    10.1 --- a/src/HOL/Library/More_BNFs.thy	Fri Jan 24 15:21:00 2014 +0000
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,1050 +0,0 @@
    10.4 -(*  Title:      HOL/Library/More_BNFs.thy
    10.5 -    Author:     Dmitriy Traytel, TU Muenchen
    10.6 -    Author:     Andrei Popescu, TU Muenchen
    10.7 -    Author:     Andreas Lochbihler, Karlsruhe Institute of Technology
    10.8 -    Author:     Jasmin Blanchette, TU Muenchen
    10.9 -    Copyright   2012
   10.10 -
   10.11 -Registration of various types as bounded natural functors.
   10.12 -*)
   10.13 -
   10.14 -header {* Registration of Various Types as Bounded Natural Functors *}
   10.15 -
   10.16 -theory More_BNFs
   10.17 -imports FSet Multiset Cardinal_Notations
   10.18 -begin
   10.19 -
   10.20 -abbreviation "Grp \<equiv> BNF_Util.Grp"
   10.21 -abbreviation "fstOp \<equiv> BNF_Def.fstOp"
   10.22 -abbreviation "sndOp \<equiv> BNF_Def.sndOp"
   10.23 -
   10.24 -lemma option_rec_conv_option_case: "option_rec = option_case"
   10.25 -by (simp add: fun_eq_iff split: option.split)
   10.26 -
   10.27 -bnf "'a option"
   10.28 -  map: Option.map
   10.29 -  sets: Option.set
   10.30 -  bd: natLeq 
   10.31 -  wits: None
   10.32 -  rel: option_rel
   10.33 -proof -
   10.34 -  show "Option.map id = id" by (simp add: fun_eq_iff Option.map_def split: option.split)
   10.35 -next
   10.36 -  fix f g
   10.37 -  show "Option.map (g \<circ> f) = Option.map g \<circ> Option.map f"
   10.38 -    by (auto simp add: fun_eq_iff Option.map_def split: option.split)
   10.39 -next
   10.40 -  fix f g x
   10.41 -  assume "\<And>z. z \<in> Option.set x \<Longrightarrow> f z = g z"
   10.42 -  thus "Option.map f x = Option.map g x"
   10.43 -    by (simp cong: Option.map_cong)
   10.44 -next
   10.45 -  fix f
   10.46 -  show "Option.set \<circ> Option.map f = op ` f \<circ> Option.set"
   10.47 -    by fastforce
   10.48 -next
   10.49 -  show "card_order natLeq" by (rule natLeq_card_order)
   10.50 -next
   10.51 -  show "cinfinite natLeq" by (rule natLeq_cinfinite)
   10.52 -next
   10.53 -  fix x
   10.54 -  show "|Option.set x| \<le>o natLeq"
   10.55 -    by (cases x) (simp_all add: ordLess_imp_ordLeq finite_iff_ordLess_natLeq[symmetric])
   10.56 -next
   10.57 -  fix R S
   10.58 -  show "option_rel R OO option_rel S \<le> option_rel (R OO S)"
   10.59 -    by (auto simp: option_rel_def split: option.splits)
   10.60 -next
   10.61 -  fix z
   10.62 -  assume "z \<in> Option.set None"
   10.63 -  thus False by simp
   10.64 -next
   10.65 -  fix R
   10.66 -  show "option_rel R =
   10.67 -        (Grp {x. Option.set x \<subseteq> Collect (split R)} (Option.map fst))\<inverse>\<inverse> OO
   10.68 -         Grp {x. Option.set x \<subseteq> Collect (split R)} (Option.map snd)"
   10.69 -  unfolding option_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff prod.cases
   10.70 -  by (auto simp: trans[OF eq_commute option_map_is_None] trans[OF eq_commute option_map_eq_Some]
   10.71 -           split: option.splits)
   10.72 -qed
   10.73 -
   10.74 -bnf "'a list"
   10.75 -  map: map
   10.76 -  sets: set
   10.77 -  bd: natLeq
   10.78 -  wits: Nil
   10.79 -  rel: list_all2
   10.80 -proof -
   10.81 -  show "map id = id" by (rule List.map.id)
   10.82 -next
   10.83 -  fix f g
   10.84 -  show "map (g o f) = map g o map f" by (rule List.map.comp[symmetric])
   10.85 -next
   10.86 -  fix x f g
   10.87 -  assume "\<And>z. z \<in> set x \<Longrightarrow> f z = g z"
   10.88 -  thus "map f x = map g x" by simp
   10.89 -next
   10.90 -  fix f
   10.91 -  show "set o map f = image f o set" by (rule ext, unfold comp_apply, rule set_map)
   10.92 -next
   10.93 -  show "card_order natLeq" by (rule natLeq_card_order)
   10.94 -next
   10.95 -  show "cinfinite natLeq" by (rule natLeq_cinfinite)
   10.96 -next
   10.97 -  fix x
   10.98 -  show "|set x| \<le>o natLeq"
   10.99 -    by (metis List.finite_set finite_iff_ordLess_natLeq ordLess_imp_ordLeq)
  10.100 -next
  10.101 -  fix R S
  10.102 -  show "list_all2 R OO list_all2 S \<le> list_all2 (R OO S)"
  10.103 -    by (metis list_all2_OO order_refl)
  10.104 -next
  10.105 -  fix R
  10.106 -  show "list_all2 R =
  10.107 -         (Grp {x. set x \<subseteq> {(x, y). R x y}} (map fst))\<inverse>\<inverse> OO
  10.108 -         Grp {x. set x \<subseteq> {(x, y). R x y}} (map snd)"
  10.109 -    unfolding list_all2_def[abs_def] Grp_def fun_eq_iff relcompp.simps conversep.simps
  10.110 -    by (force simp: zip_map_fst_snd)
  10.111 -qed simp_all
  10.112 -
  10.113 -
  10.114 -(* Finite sets *)
  10.115 -
  10.116 -context
  10.117 -includes fset.lifting
  10.118 -begin
  10.119 -
  10.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>
  10.121 -                                        (\<forall>t \<in> fset b. \<exists>u \<in> fset a. R u t)"
  10.122 -  by transfer (simp add: set_rel_def)
  10.123 -
  10.124 -lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A"
  10.125 -  apply (rule f_the_inv_into_f[unfolded inj_on_def])
  10.126 -  apply (simp add: fset_inject) apply (rule range_eqI Abs_fset_inverse[symmetric] CollectI)+
  10.127 -  .
  10.128 -
  10.129 -lemma fset_rel_aux:
  10.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>
  10.131 - ((Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage fst))\<inverse>\<inverse> OO
  10.132 -  Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage snd)) a b" (is "?L = ?R")
  10.133 -proof
  10.134 -  assume ?L
  10.135 -  def R' \<equiv> "the_inv fset (Collect (split R) \<inter> (fset a \<times> fset b))" (is "the_inv fset ?L'")
  10.136 -  have "finite ?L'" by (intro finite_Int[OF disjI2] finite_cartesian_product) (transfer, simp)+
  10.137 -  hence *: "fset R' = ?L'" unfolding R'_def by (intro fset_to_fset)
  10.138 -  show ?R unfolding Grp_def relcompp.simps conversep.simps
  10.139 -  proof (intro CollectI prod_caseI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
  10.140 -    from * show "a = fimage fst R'" using conjunct1[OF `?L`]
  10.141 -      by (transfer, auto simp add: image_def Int_def split: prod.splits)
  10.142 -    from * show "b = fimage snd R'" using conjunct2[OF `?L`]
  10.143 -      by (transfer, auto simp add: image_def Int_def split: prod.splits)
  10.144 -  qed (auto simp add: *)
  10.145 -next
  10.146 -  assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps
  10.147 -  apply (simp add: subset_eq Ball_def)
  10.148 -  apply (rule conjI)
  10.149 -  apply (transfer, clarsimp, metis snd_conv)
  10.150 -  by (transfer, clarsimp, metis fst_conv)
  10.151 -qed
  10.152 -
  10.153 -bnf "'a fset"
  10.154 -  map: fimage
  10.155 -  sets: fset 
  10.156 -  bd: natLeq
  10.157 -  wits: "{||}"
  10.158 -  rel: fset_rel
  10.159 -apply -
  10.160 -          apply transfer' apply simp
  10.161 -         apply transfer' apply force
  10.162 -        apply transfer apply force
  10.163 -       apply transfer' apply force
  10.164 -      apply (rule natLeq_card_order)
  10.165 -     apply (rule natLeq_cinfinite)
  10.166 -    apply transfer apply (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq)
  10.167 -   apply (fastforce simp: fset_rel_alt)
  10.168 - apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff fset_rel_alt fset_rel_aux) 
  10.169 -apply transfer apply simp
  10.170 -done
  10.171 -
  10.172 -lemma fset_rel_fset: "set_rel \<chi> (fset A1) (fset A2) = fset_rel \<chi> A1 A2"
  10.173 -  by transfer (rule refl)
  10.174 -
  10.175 -end
  10.176 -
  10.177 -lemmas [simp] = fset.map_comp fset.map_id fset.set_map
  10.178 -
  10.179 -
  10.180 -(* Multisets *)
  10.181 -
  10.182 -lemma setsum_gt_0_iff:
  10.183 -fixes f :: "'a \<Rightarrow> nat" assumes "finite A"
  10.184 -shows "setsum f A > 0 \<longleftrightarrow> (\<exists> a \<in> A. f a > 0)"
  10.185 -(is "?L \<longleftrightarrow> ?R")
  10.186 -proof-
  10.187 -  have "?L \<longleftrightarrow> \<not> setsum f A = 0" by fast
  10.188 -  also have "... \<longleftrightarrow> (\<exists> a \<in> A. f a \<noteq> 0)" using assms by simp
  10.189 -  also have "... \<longleftrightarrow> ?R" by simp
  10.190 -  finally show ?thesis .
  10.191 -qed
  10.192 -
  10.193 -lift_definition mmap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" is
  10.194 -  "\<lambda>h f b. setsum f {a. h a = b \<and> f a > 0} :: nat"
  10.195 -unfolding multiset_def proof safe
  10.196 -  fix h :: "'a \<Rightarrow> 'b" and f :: "'a \<Rightarrow> nat"
  10.197 -  assume fin: "finite {a. 0 < f a}"  (is "finite ?A")
  10.198 -  show "finite {b. 0 < setsum f {a. h a = b \<and> 0 < f a}}"
  10.199 -  (is "finite {b. 0 < setsum f (?As b)}")
  10.200 -  proof- let ?B = "{b. 0 < setsum f (?As b)}"
  10.201 -    have "\<And> b. finite (?As b)" using fin by simp
  10.202 -    hence B: "?B = {b. ?As b \<noteq> {}}" by (auto simp add: setsum_gt_0_iff)
  10.203 -    hence "?B \<subseteq> h ` ?A" by auto
  10.204 -    thus ?thesis using finite_surj[OF fin] by auto
  10.205 -  qed
  10.206 -qed
  10.207 -
  10.208 -lemma mmap_id0: "mmap id = id"
  10.209 -proof (intro ext multiset_eqI)
  10.210 -  fix f a show "count (mmap id f) a = count (id f) a"
  10.211 -  proof (cases "count f a = 0")
  10.212 -    case False
  10.213 -    hence 1: "{aa. aa = a \<and> aa \<in># f} = {a}" by auto
  10.214 -    thus ?thesis by transfer auto
  10.215 -  qed (transfer, simp)
  10.216 -qed
  10.217 -
  10.218 -lemma inj_on_setsum_inv:
  10.219 -assumes 1: "(0::nat) < setsum (count f) {a. h a = b' \<and> a \<in># f}" (is "0 < setsum (count f) ?A'")
  10.220 -and     2: "{a. h a = b \<and> a \<in># f} = {a. h a = b' \<and> a \<in># f}" (is "?A = ?A'")
  10.221 -shows "b = b'"
  10.222 -using assms by (auto simp add: setsum_gt_0_iff)
  10.223 -
  10.224 -lemma mmap_comp:
  10.225 -fixes h1 :: "'a \<Rightarrow> 'b" and h2 :: "'b \<Rightarrow> 'c"
  10.226 -shows "mmap (h2 o h1) = mmap h2 o mmap h1"
  10.227 -proof (intro ext multiset_eqI)
  10.228 -  fix f :: "'a multiset" fix c :: 'c
  10.229 -  let ?A = "{a. h2 (h1 a) = c \<and> a \<in># f}"
  10.230 -  let ?As = "\<lambda> b. {a. h1 a = b \<and> a \<in># f}"
  10.231 -  let ?B = "{b. h2 b = c \<and> 0 < setsum (count f) (?As b)}"
  10.232 -  have 0: "{?As b | b.  b \<in> ?B} = ?As ` ?B" by auto
  10.233 -  have "\<And> b. finite (?As b)" by transfer (simp add: multiset_def)
  10.234 -  hence "?B = {b. h2 b = c \<and> ?As b \<noteq> {}}" by (auto simp add: setsum_gt_0_iff)
  10.235 -  hence A: "?A = \<Union> {?As b | b.  b \<in> ?B}" by auto
  10.236 -  have "setsum (count f) ?A = setsum (setsum (count f)) {?As b | b.  b \<in> ?B}"
  10.237 -    unfolding A by transfer (intro setsum_Union_disjoint, auto simp: multiset_def)
  10.238 -  also have "... = setsum (setsum (count f)) (?As ` ?B)" unfolding 0 ..
  10.239 -  also have "... = setsum (setsum (count f) o ?As) ?B"
  10.240 -    by(intro setsum_reindex) (auto simp add: setsum_gt_0_iff inj_on_def)
  10.241 -  also have "... = setsum (\<lambda> b. setsum (count f) (?As b)) ?B" unfolding comp_def ..
  10.242 -  finally have "setsum (count f) ?A = setsum (\<lambda> b. setsum (count f) (?As b)) ?B" .
  10.243 -  thus "count (mmap (h2 \<circ> h1) f) c = count ((mmap h2 \<circ> mmap h1) f) c"
  10.244 -    by transfer (unfold comp_apply, blast)
  10.245 -qed
  10.246 -
  10.247 -lemma mmap_cong:
  10.248 -assumes "\<And>a. a \<in># M \<Longrightarrow> f a = g a"
  10.249 -shows "mmap f M = mmap g M"
  10.250 -using assms by transfer (auto intro!: setsum_cong)
  10.251 -
  10.252 -context
  10.253 -begin
  10.254 -interpretation lifting_syntax .
  10.255 -
  10.256 -lemma set_of_transfer[transfer_rule]: "(pcr_multiset op = ===> op =) (\<lambda>f. {a. 0 < f a}) set_of"
  10.257 -  unfolding set_of_def pcr_multiset_def cr_multiset_def fun_rel_def by auto
  10.258 -
  10.259 -end
  10.260 -
  10.261 -lemma set_of_mmap: "set_of o mmap h = image h o set_of"
  10.262 -proof (rule ext, unfold comp_apply)
  10.263 -  fix M show "set_of (mmap h M) = h ` set_of M"
  10.264 -    by transfer (auto simp add: multiset_def setsum_gt_0_iff)
  10.265 -qed
  10.266 -
  10.267 -lemma multiset_of_surj:
  10.268 -  "multiset_of ` {as. set as \<subseteq> A} = {M. set_of M \<subseteq> A}"
  10.269 -proof safe
  10.270 -  fix M assume M: "set_of M \<subseteq> A"
  10.271 -  obtain as where eq: "M = multiset_of as" using surj_multiset_of unfolding surj_def by auto
  10.272 -  hence "set as \<subseteq> A" using M by auto
  10.273 -  thus "M \<in> multiset_of ` {as. set as \<subseteq> A}" using eq by auto
  10.274 -next
  10.275 -  show "\<And>x xa xb. \<lbrakk>set xa \<subseteq> A; xb \<in> set_of (multiset_of xa)\<rbrakk> \<Longrightarrow> xb \<in> A"
  10.276 -  by (erule set_mp) (unfold set_of_multiset_of)
  10.277 -qed
  10.278 -
  10.279 -lemma card_of_set_of:
  10.280 -"|{M. set_of M \<subseteq> A}| \<le>o |{as. set as \<subseteq> A}|"
  10.281 -apply(rule card_of_ordLeqI2[of _ multiset_of]) using multiset_of_surj by auto
  10.282 -
  10.283 -lemma nat_sum_induct:
  10.284 -assumes "\<And>n1 n2. (\<And> m1 m2. m1 + m2 < n1 + n2 \<Longrightarrow> phi m1 m2) \<Longrightarrow> phi n1 n2"
  10.285 -shows "phi (n1::nat) (n2::nat)"
  10.286 -proof-
  10.287 -  let ?chi = "\<lambda> n1n2 :: nat * nat. phi (fst n1n2) (snd n1n2)"
  10.288 -  have "?chi (n1,n2)"
  10.289 -  apply(induct rule: measure_induct[of "\<lambda> n1n2. fst n1n2 + snd n1n2" ?chi])
  10.290 -  using assms by (metis fstI sndI)
  10.291 -  thus ?thesis by simp
  10.292 -qed
  10.293 -
  10.294 -lemma matrix_count:
  10.295 -fixes ct1 ct2 :: "nat \<Rightarrow> nat"
  10.296 -assumes "setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2}"
  10.297 -shows
  10.298 -"\<exists> ct. (\<forall> i1 \<le> n1. setsum (\<lambda> i2. ct i1 i2) {..<Suc n2} = ct1 i1) \<and>
  10.299 -       (\<forall> i2 \<le> n2. setsum (\<lambda> i1. ct i1 i2) {..<Suc n1} = ct2 i2)"
  10.300 -(is "?phi ct1 ct2 n1 n2")
  10.301 -proof-
  10.302 -  have "\<forall> ct1 ct2 :: nat \<Rightarrow> nat.
  10.303 -        setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2} \<longrightarrow> ?phi ct1 ct2 n1 n2"
  10.304 -  proof(induct rule: nat_sum_induct[of
  10.305 -"\<lambda> n1 n2. \<forall> ct1 ct2 :: nat \<Rightarrow> nat.
  10.306 -     setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2} \<longrightarrow> ?phi ct1 ct2 n1 n2"],
  10.307 -      clarify)
  10.308 -  fix n1 n2 :: nat and ct1 ct2 :: "nat \<Rightarrow> nat"
  10.309 -  assume IH: "\<And> m1 m2. m1 + m2 < n1 + n2 \<Longrightarrow>
  10.310 -                \<forall> dt1 dt2 :: nat \<Rightarrow> nat.
  10.311 -                setsum dt1 {..<Suc m1} = setsum dt2 {..<Suc m2} \<longrightarrow> ?phi dt1 dt2 m1 m2"
  10.312 -  and ss: "setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2}"
  10.313 -  show "?phi ct1 ct2 n1 n2"
  10.314 -  proof(cases n1)
  10.315 -    case 0 note n1 = 0
  10.316 -    show ?thesis
  10.317 -    proof(cases n2)
  10.318 -      case 0 note n2 = 0
  10.319 -      let ?ct = "\<lambda> i1 i2. ct2 0"
  10.320 -      show ?thesis apply(rule exI[of _ ?ct]) using n1 n2 ss by simp
  10.321 -    next
  10.322 -      case (Suc m2) note n2 = Suc
  10.323 -      let ?ct = "\<lambda> i1 i2. ct2 i2"
  10.324 -      show ?thesis apply(rule exI[of _ ?ct]) using n1 n2 ss by auto
  10.325 -    qed
  10.326 -  next
  10.327 -    case (Suc m1) note n1 = Suc
  10.328 -    show ?thesis
  10.329 -    proof(cases n2)
  10.330 -      case 0 note n2 = 0
  10.331 -      let ?ct = "\<lambda> i1 i2. ct1 i1"
  10.332 -      show ?thesis apply(rule exI[of _ ?ct]) using n1 n2 ss by auto
  10.333 -    next
  10.334 -      case (Suc m2) note n2 = Suc
  10.335 -      show ?thesis
  10.336 -      proof(cases "ct1 n1 \<le> ct2 n2")
  10.337 -        case True
  10.338 -        def dt2 \<equiv> "\<lambda> i2. if i2 = n2 then ct2 i2 - ct1 n1 else ct2 i2"
  10.339 -        have "setsum ct1 {..<Suc m1} = setsum dt2 {..<Suc n2}"
  10.340 -        unfolding dt2_def using ss n1 True by auto
  10.341 -        hence "?phi ct1 dt2 m1 n2" using IH[of m1 n2] n1 by simp
  10.342 -        then obtain dt where
  10.343 -        1: "\<And> i1. i1 \<le> m1 \<Longrightarrow> setsum (\<lambda> i2. dt i1 i2) {..<Suc n2} = ct1 i1" and
  10.344 -        2: "\<And> i2. i2 \<le> n2 \<Longrightarrow> setsum (\<lambda> i1. dt i1 i2) {..<Suc m1} = dt2 i2" by auto
  10.345 -        let ?ct = "\<lambda> i1 i2. if i1 = n1 then (if i2 = n2 then ct1 n1 else 0)
  10.346 -                                       else dt i1 i2"
  10.347 -        show ?thesis apply(rule exI[of _ ?ct])
  10.348 -        using n1 n2 1 2 True unfolding dt2_def by simp
  10.349 -      next
  10.350 -        case False
  10.351 -        hence False: "ct2 n2 < ct1 n1" by simp
  10.352 -        def dt1 \<equiv> "\<lambda> i1. if i1 = n1 then ct1 i1 - ct2 n2 else ct1 i1"
  10.353 -        have "setsum dt1 {..<Suc n1} = setsum ct2 {..<Suc m2}"
  10.354 -        unfolding dt1_def using ss n2 False by auto
  10.355 -        hence "?phi dt1 ct2 n1 m2" using IH[of n1 m2] n2 by simp
  10.356 -        then obtain dt where
  10.357 -        1: "\<And> i1. i1 \<le> n1 \<Longrightarrow> setsum (\<lambda> i2. dt i1 i2) {..<Suc m2} = dt1 i1" and
  10.358 -        2: "\<And> i2. i2 \<le> m2 \<Longrightarrow> setsum (\<lambda> i1. dt i1 i2) {..<Suc n1} = ct2 i2" by force
  10.359 -        let ?ct = "\<lambda> i1 i2. if i2 = n2 then (if i1 = n1 then ct2 n2 else 0)
  10.360 -                                       else dt i1 i2"
  10.361 -        show ?thesis apply(rule exI[of _ ?ct])
  10.362 -        using n1 n2 1 2 False unfolding dt1_def by simp
  10.363 -      qed
  10.364 -    qed
  10.365 -  qed
  10.366 -  qed
  10.367 -  thus ?thesis using assms by auto
  10.368 -qed
  10.369 -
  10.370 -definition
  10.371 -"inj2 u B1 B2 \<equiv>
  10.372 - \<forall> b1 b1' b2 b2'. {b1,b1'} \<subseteq> B1 \<and> {b2,b2'} \<subseteq> B2 \<and> u b1 b2 = u b1' b2'
  10.373 -                  \<longrightarrow> b1 = b1' \<and> b2 = b2'"
  10.374 -
  10.375 -lemma matrix_setsum_finite:
  10.376 -assumes B1: "B1 \<noteq> {}" "finite B1" and B2: "B2 \<noteq> {}" "finite B2" and u: "inj2 u B1 B2"
  10.377 -and ss: "setsum N1 B1 = setsum N2 B2"
  10.378 -shows "\<exists> M :: 'a \<Rightarrow> nat.
  10.379 -            (\<forall> b1 \<in> B1. setsum (\<lambda> b2. M (u b1 b2)) B2 = N1 b1) \<and>
  10.380 -            (\<forall> b2 \<in> B2. setsum (\<lambda> b1. M (u b1 b2)) B1 = N2 b2)"
  10.381 -proof-
  10.382 -  obtain n1 where "card B1 = Suc n1" using B1 by (metis card_insert finite.simps)
  10.383 -  then obtain e1 where e1: "bij_betw e1 {..<Suc n1} B1"
  10.384 -  using ex_bij_betw_finite_nat[OF B1(2)] by (metis atLeast0LessThan bij_betw_the_inv_into)
  10.385 -  hence e1_inj: "inj_on e1 {..<Suc n1}" and e1_surj: "e1 ` {..<Suc n1} = B1"
  10.386 -  unfolding bij_betw_def by auto
  10.387 -  def f1 \<equiv> "inv_into {..<Suc n1} e1"
  10.388 -  have f1: "bij_betw f1 B1 {..<Suc n1}"
  10.389 -  and f1e1[simp]: "\<And> i1. i1 < Suc n1 \<Longrightarrow> f1 (e1 i1) = i1"
  10.390 -  and e1f1[simp]: "\<And> b1. b1 \<in> B1 \<Longrightarrow> e1 (f1 b1) = b1" unfolding f1_def
  10.391 -  apply (metis bij_betw_inv_into e1, metis bij_betw_inv_into_left e1 lessThan_iff)
  10.392 -  by (metis e1_surj f_inv_into_f)
  10.393 -  (*  *)
  10.394 -  obtain n2 where "card B2 = Suc n2" using B2 by (metis card_insert finite.simps)
  10.395 -  then obtain e2 where e2: "bij_betw e2 {..<Suc n2} B2"
  10.396 -  using ex_bij_betw_finite_nat[OF B2(2)] by (metis atLeast0LessThan bij_betw_the_inv_into)
  10.397 -  hence e2_inj: "inj_on e2 {..<Suc n2}" and e2_surj: "e2 ` {..<Suc n2} = B2"
  10.398 -  unfolding bij_betw_def by auto
  10.399 -  def f2 \<equiv> "inv_into {..<Suc n2} e2"
  10.400 -  have f2: "bij_betw f2 B2 {..<Suc n2}"
  10.401 -  and f2e2[simp]: "\<And> i2. i2 < Suc n2 \<Longrightarrow> f2 (e2 i2) = i2"
  10.402 -  and e2f2[simp]: "\<And> b2. b2 \<in> B2 \<Longrightarrow> e2 (f2 b2) = b2" unfolding f2_def
  10.403 -  apply (metis bij_betw_inv_into e2, metis bij_betw_inv_into_left e2 lessThan_iff)
  10.404 -  by (metis e2_surj f_inv_into_f)
  10.405 -  (*  *)
  10.406 -  let ?ct1 = "N1 o e1"  let ?ct2 = "N2 o e2"
  10.407 -  have ss: "setsum ?ct1 {..<Suc n1} = setsum ?ct2 {..<Suc n2}"
  10.408 -  unfolding setsum_reindex[OF e1_inj, symmetric] setsum_reindex[OF e2_inj, symmetric]
  10.409 -  e1_surj e2_surj using ss .
  10.410 -  obtain ct where
  10.411 -  ct1: "\<And> i1. i1 \<le> n1 \<Longrightarrow> setsum (\<lambda> i2. ct i1 i2) {..<Suc n2} = ?ct1 i1" and
  10.412 -  ct2: "\<And> i2. i2 \<le> n2 \<Longrightarrow> setsum (\<lambda> i1. ct i1 i2) {..<Suc n1} = ?ct2 i2"
  10.413 -  using matrix_count[OF ss] by blast
  10.414 -  (*  *)
  10.415 -  def A \<equiv> "{u b1 b2 | b1 b2. b1 \<in> B1 \<and> b2 \<in> B2}"
  10.416 -  have "\<forall> a \<in> A. \<exists> b1b2 \<in> B1 <*> B2. u (fst b1b2) (snd b1b2) = a"
  10.417 -  unfolding A_def Ball_def mem_Collect_eq by auto
  10.418 -  then obtain h1h2 where h12:
  10.419 -  "\<And>a. a \<in> A \<Longrightarrow> u (fst (h1h2 a)) (snd (h1h2 a)) = a \<and> h1h2 a \<in> B1 <*> B2" by metis
  10.420 -  def h1 \<equiv> "fst o h1h2"  def h2 \<equiv> "snd o h1h2"
  10.421 -  have h12[simp]: "\<And>a. a \<in> A \<Longrightarrow> u (h1 a) (h2 a) = a"
  10.422 -                  "\<And> a. a \<in> A \<Longrightarrow> h1 a \<in> B1"  "\<And> a. a \<in> A \<Longrightarrow> h2 a \<in> B2"
  10.423 -  using h12 unfolding h1_def h2_def by force+
  10.424 -  {fix b1 b2 assume b1: "b1 \<in> B1" and b2: "b2 \<in> B2"
  10.425 -   hence inA: "u b1 b2 \<in> A" unfolding A_def by auto
  10.426 -   hence "u b1 b2 = u (h1 (u b1 b2)) (h2 (u b1 b2))" by auto
  10.427 -   moreover have "h1 (u b1 b2) \<in> B1" "h2 (u b1 b2) \<in> B2" using inA by auto
  10.428 -   ultimately have "h1 (u b1 b2) = b1 \<and> h2 (u b1 b2) = b2"
  10.429 -   using u b1 b2 unfolding inj2_def by fastforce
  10.430 -  }
  10.431 -  hence h1[simp]: "\<And> b1 b2. \<lbrakk>b1 \<in> B1; b2 \<in> B2\<rbrakk> \<Longrightarrow> h1 (u b1 b2) = b1" and
  10.432 -        h2[simp]: "\<And> b1 b2. \<lbrakk>b1 \<in> B1; b2 \<in> B2\<rbrakk> \<Longrightarrow> h2 (u b1 b2) = b2" by auto
  10.433 -  def M \<equiv> "\<lambda> a. ct (f1 (h1 a)) (f2 (h2 a))"
  10.434 -  show ?thesis
  10.435 -  apply(rule exI[of _ M]) proof safe
  10.436 -    fix b1 assume b1: "b1 \<in> B1"
  10.437 -    hence f1b1: "f1 b1 \<le> n1" using f1 unfolding bij_betw_def
  10.438 -    by (metis image_eqI lessThan_iff less_Suc_eq_le)
  10.439 -    have "(\<Sum>b2\<in>B2. M (u b1 b2)) = (\<Sum>i2<Suc n2. ct (f1 b1) (f2 (e2 i2)))"
  10.440 -    unfolding e2_surj[symmetric] setsum_reindex[OF e2_inj]
  10.441 -    unfolding M_def comp_def apply(intro setsum_cong) apply force
  10.442 -    by (metis e2_surj b1 h1 h2 imageI)
  10.443 -    also have "... = N1 b1" using b1 ct1[OF f1b1] by simp
  10.444 -    finally show "(\<Sum>b2\<in>B2. M (u b1 b2)) = N1 b1" .
  10.445 -  next
  10.446 -    fix b2 assume b2: "b2 \<in> B2"
  10.447 -    hence f2b2: "f2 b2 \<le> n2" using f2 unfolding bij_betw_def
  10.448 -    by (metis image_eqI lessThan_iff less_Suc_eq_le)
  10.449 -    have "(\<Sum>b1\<in>B1. M (u b1 b2)) = (\<Sum>i1<Suc n1. ct (f1 (e1 i1)) (f2 b2))"
  10.450 -    unfolding e1_surj[symmetric] setsum_reindex[OF e1_inj]
  10.451 -    unfolding M_def comp_def apply(intro setsum_cong) apply force
  10.452 -    by (metis e1_surj b2 h1 h2 imageI)
  10.453 -    also have "... = N2 b2" using b2 ct2[OF f2b2] by simp
  10.454 -    finally show "(\<Sum>b1\<in>B1. M (u b1 b2)) = N2 b2" .
  10.455 -  qed
  10.456 -qed
  10.457 -
  10.458 -lemma supp_vimage_mmap: "set_of M \<subseteq> f -` (set_of (mmap f M))"
  10.459 -  by transfer (auto simp: multiset_def setsum_gt_0_iff)
  10.460 -
  10.461 -lemma mmap_ge_0: "b \<in># mmap f M \<longleftrightarrow> (\<exists>a. a \<in># M \<and> f a = b)"
  10.462 -  by transfer (auto simp: multiset_def setsum_gt_0_iff)
  10.463 -
  10.464 -lemma finite_twosets:
  10.465 -assumes "finite B1" and "finite B2"
  10.466 -shows "finite {u b1 b2 |b1 b2. b1 \<in> B1 \<and> b2 \<in> B2}"  (is "finite ?A")
  10.467 -proof-
  10.468 -  have A: "?A = (\<lambda> b1b2. u (fst b1b2) (snd b1b2)) ` (B1 <*> B2)" by force
  10.469 -  show ?thesis unfolding A using finite_cartesian_product[OF assms] by auto
  10.470 -qed
  10.471 -
  10.472 -(* Weak pullbacks: *)
  10.473 -definition wpull where
  10.474 -"wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow>
  10.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))"
  10.476 -
  10.477 -(* Weak pseudo-pullbacks *)
  10.478 -definition wppull where
  10.479 -"wppull A B1 B2 f1 f2 e1 e2 p1 p2 \<longleftrightarrow>
  10.480 - (\<forall> b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<longrightarrow>
  10.481 -           (\<exists> a \<in> A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2))"
  10.482 -
  10.483 -
  10.484 -(* The pullback of sets *)
  10.485 -definition thePull where
  10.486 -"thePull B1 B2 f1 f2 = {(b1,b2). b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2}"
  10.487 -
  10.488 -lemma wpull_thePull:
  10.489 -"wpull (thePull B1 B2 f1 f2) B1 B2 f1 f2 fst snd"
  10.490 -unfolding wpull_def thePull_def by auto
  10.491 -
  10.492 -lemma wppull_thePull:
  10.493 -assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
  10.494 -shows
  10.495 -"\<exists> j. \<forall> a' \<in> thePull B1 B2 f1 f2.
  10.496 -   j a' \<in> A \<and>
  10.497 -   e1 (p1 (j a')) = e1 (fst a') \<and> e2 (p2 (j a')) = e2 (snd a')"
  10.498 -(is "\<exists> j. \<forall> a' \<in> ?A'. ?phi a' (j a')")
  10.499 -proof(rule bchoice[of ?A' ?phi], default)
  10.500 -  fix a' assume a': "a' \<in> ?A'"
  10.501 -  hence "fst a' \<in> B1" unfolding thePull_def by auto
  10.502 -  moreover
  10.503 -  from a' have "snd a' \<in> B2" unfolding thePull_def by auto
  10.504 -  moreover have "f1 (fst a') = f2 (snd a')"
  10.505 -  using a' unfolding csquare_def thePull_def by auto
  10.506 -  ultimately show "\<exists> ja'. ?phi a' ja'"
  10.507 -  using assms unfolding wppull_def by blast
  10.508 -qed
  10.509 -
  10.510 -lemma wpull_wppull:
  10.511 -assumes wp: "wpull A' B1 B2 f1 f2 p1' p2'" and
  10.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')"
  10.513 -shows "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
  10.514 -unfolding wppull_def proof safe
  10.515 -  fix b1 b2
  10.516 -  assume b1: "b1 \<in> B1" and b2: "b2 \<in> B2" and f: "f1 b1 = f2 b2"
  10.517 -  then obtain a' where a': "a' \<in> A'" and b1: "b1 = p1' a'" and b2: "b2 = p2' a'"
  10.518 -  using wp unfolding wpull_def by blast
  10.519 -  show "\<exists>a\<in>A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2"
  10.520 -  apply (rule bexI[of _ "j a'"]) unfolding b1 b2 using a' 1 by auto
  10.521 -qed
  10.522 -
  10.523 -lemma wppull_fstOp_sndOp:
  10.524 -shows "wppull (Collect (split (P OO Q))) (Collect (split P)) (Collect (split Q))
  10.525 -  snd fst fst snd (fstOp P Q) (sndOp P Q)"
  10.526 -using pick_middlep unfolding wppull_def fstOp_def sndOp_def relcompp.simps by auto
  10.527 -
  10.528 -lemma wpull_mmap:
  10.529 -fixes A :: "'a set" and B1 :: "'b1 set" and B2 :: "'b2 set"
  10.530 -assumes wp: "wpull A B1 B2 f1 f2 p1 p2"
  10.531 -shows
  10.532 -"wpull {M. set_of M \<subseteq> A}
  10.533 -       {N1. set_of N1 \<subseteq> B1} {N2. set_of N2 \<subseteq> B2}
  10.534 -       (mmap f1) (mmap f2) (mmap p1) (mmap p2)"
  10.535 -unfolding wpull_def proof (safe, unfold Bex_def mem_Collect_eq)
  10.536 -  fix N1 :: "'b1 multiset" and N2 :: "'b2 multiset"
  10.537 -  assume mmap': "mmap f1 N1 = mmap f2 N2"
  10.538 -  and N1[simp]: "set_of N1 \<subseteq> B1"
  10.539 -  and N2[simp]: "set_of N2 \<subseteq> B2"
  10.540 -  def P \<equiv> "mmap f1 N1"
  10.541 -  have P1: "P = mmap f1 N1" and P2: "P = mmap f2 N2" unfolding P_def using mmap' by auto
  10.542 -  note P = P1 P2
  10.543 -  have fin_N1[simp]: "finite (set_of N1)"
  10.544 -   and fin_N2[simp]: "finite (set_of N2)"
  10.545 -   and fin_P[simp]: "finite (set_of P)" by auto
  10.546 -  (*  *)
  10.547 -  def set1 \<equiv> "\<lambda> c. {b1 \<in> set_of N1. f1 b1 = c}"
  10.548 -  have set1[simp]: "\<And> c b1. b1 \<in> set1 c \<Longrightarrow> f1 b1 = c" unfolding set1_def by auto
  10.549 -  have fin_set1: "\<And> c. c \<in> set_of P \<Longrightarrow> finite (set1 c)"
  10.550 -    using N1(1) unfolding set1_def multiset_def by auto
  10.551 -  have set1_NE: "\<And> c. c \<in> set_of P \<Longrightarrow> set1 c \<noteq> {}"
  10.552 -   unfolding set1_def set_of_def P mmap_ge_0 by auto
  10.553 -  have supp_N1_set1: "set_of N1 = (\<Union> c \<in> set_of P. set1 c)"
  10.554 -    using supp_vimage_mmap[of N1 f1] unfolding set1_def P1 by auto
  10.555 -  hence set1_inclN1: "\<And>c. c \<in> set_of P \<Longrightarrow> set1 c \<subseteq> set_of N1" by auto
  10.556 -  hence set1_incl: "\<And> c. c \<in> set_of P \<Longrightarrow> set1 c \<subseteq> B1" using N1 by blast
  10.557 -  have set1_disj: "\<And> c c'. c \<noteq> c' \<Longrightarrow> set1 c \<inter> set1 c' = {}"
  10.558 -    unfolding set1_def by auto
  10.559 -  have setsum_set1: "\<And> c. setsum (count N1) (set1 c) = count P c"
  10.560 -    unfolding P1 set1_def by transfer (auto intro: setsum_cong)
  10.561 -  (*  *)
  10.562 -  def set2 \<equiv> "\<lambda> c. {b2 \<in> set_of N2. f2 b2 = c}"
  10.563 -  have set2[simp]: "\<And> c b2. b2 \<in> set2 c \<Longrightarrow> f2 b2 = c" unfolding set2_def by auto
  10.564 -  have fin_set2: "\<And> c. c \<in> set_of P \<Longrightarrow> finite (set2 c)"
  10.565 -  using N2(1) unfolding set2_def multiset_def by auto
  10.566 -  have set2_NE: "\<And> c. c \<in> set_of P \<Longrightarrow> set2 c \<noteq> {}"
  10.567 -    unfolding set2_def P2 mmap_ge_0 set_of_def by auto
  10.568 -  have supp_N2_set2: "set_of N2 = (\<Union> c \<in> set_of P. set2 c)"
  10.569 -    using supp_vimage_mmap[of N2 f2] unfolding set2_def P2 by auto
  10.570 -  hence set2_inclN2: "\<And>c. c \<in> set_of P \<Longrightarrow> set2 c \<subseteq> set_of N2" by auto
  10.571 -  hence set2_incl: "\<And> c. c \<in> set_of P \<Longrightarrow> set2 c \<subseteq> B2" using N2 by blast
  10.572 -  have set2_disj: "\<And> c c'. c \<noteq> c' \<Longrightarrow> set2 c \<inter> set2 c' = {}"
  10.573 -    unfolding set2_def by auto
  10.574 -  have setsum_set2: "\<And> c. setsum (count N2) (set2 c) = count P c"
  10.575 -    unfolding P2 set2_def by transfer (auto intro: setsum_cong)
  10.576 -  (*  *)
  10.577 -  have ss: "\<And> c. c \<in> set_of P \<Longrightarrow> setsum (count N1) (set1 c) = setsum (count N2) (set2 c)"
  10.578 -    unfolding setsum_set1 setsum_set2 ..
  10.579 -  have "\<forall> c \<in> set_of P. \<forall> b1b2 \<in> (set1 c) \<times> (set2 c).
  10.580 -          \<exists> a \<in> A. p1 a = fst b1b2 \<and> p2 a = snd b1b2"
  10.581 -    using wp set1_incl set2_incl unfolding wpull_def Ball_def mem_Collect_eq
  10.582 -    by simp (metis set1 set2 set_rev_mp)
  10.583 -  then obtain uu where uu:
  10.584 -  "\<forall> c \<in> set_of P. \<forall> b1b2 \<in> (set1 c) \<times> (set2 c).
  10.585 -     uu c b1b2 \<in> A \<and> p1 (uu c b1b2) = fst b1b2 \<and> p2 (uu c b1b2) = snd b1b2" by metis
  10.586 -  def u \<equiv> "\<lambda> c b1 b2. uu c (b1,b2)"
  10.587 -  have u[simp]:
  10.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"
  10.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"
  10.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"
  10.591 -    using uu unfolding u_def by auto
  10.592 -  {fix c assume c: "c \<in> set_of P"
  10.593 -   have "inj2 (u c) (set1 c) (set2 c)" unfolding inj2_def proof clarify
  10.594 -     fix b1 b1' b2 b2'
  10.595 -     assume "{b1, b1'} \<subseteq> set1 c" "{b2, b2'} \<subseteq> set2 c" and 0: "u c b1 b2 = u c b1' b2'"
  10.596 -     hence "p1 (u c b1 b2) = b1 \<and> p2 (u c b1 b2) = b2 \<and>
  10.597 -            p1 (u c b1' b2') = b1' \<and> p2 (u c b1' b2') = b2'"
  10.598 -     using u(2)[OF c] u(3)[OF c] by simp metis
  10.599 -     thus "b1 = b1' \<and> b2 = b2'" using 0 by auto
  10.600 -   qed
  10.601 -  } note inj = this
  10.602 -  def sset \<equiv> "\<lambda> c. {u c b1 b2 | b1 b2. b1 \<in> set1 c \<and> b2 \<in> set2 c}"
  10.603 -  have fin_sset[simp]: "\<And> c. c \<in> set_of P \<Longrightarrow> finite (sset c)" unfolding sset_def
  10.604 -    using fin_set1 fin_set2 finite_twosets by blast
  10.605 -  have sset_A: "\<And> c. c \<in> set_of P \<Longrightarrow> sset c \<subseteq> A" unfolding sset_def by auto
  10.606 -  {fix c a assume c: "c \<in> set_of P" and ac: "a \<in> sset c"
  10.607 -   then obtain b1 b2 where b1: "b1 \<in> set1 c" and b2: "b2 \<in> set2 c"
  10.608 -   and a: "a = u c b1 b2" unfolding sset_def by auto
  10.609 -   have "p1 a \<in> set1 c" and p2a: "p2 a \<in> set2 c"
  10.610 -   using ac a b1 b2 c u(2) u(3) by simp+
  10.611 -   hence "u c (p1 a) (p2 a) = a" unfolding a using b1 b2 inj[OF c]
  10.612 -   unfolding inj2_def by (metis c u(2) u(3))
  10.613 -  } note u_p12[simp] = this
  10.614 -  {fix c a assume c: "c \<in> set_of P" and ac: "a \<in> sset c"
  10.615 -   hence "p1 a \<in> set1 c" unfolding sset_def by auto
  10.616 -  }note p1[simp] = this
  10.617 -  {fix c a assume c: "c \<in> set_of P" and ac: "a \<in> sset c"
  10.618 -   hence "p2 a \<in> set2 c" unfolding sset_def by auto
  10.619 -  }note p2[simp] = this
  10.620 -  (*  *)
  10.621 -  {fix c assume c: "c \<in> set_of P"
  10.622 -   hence "\<exists> M. (\<forall> b1 \<in> set1 c. setsum (\<lambda> b2. M (u c b1 b2)) (set2 c) = count N1 b1) \<and>
  10.623 -               (\<forall> b2 \<in> set2 c. setsum (\<lambda> b1. M (u c b1 b2)) (set1 c) = count N2 b2)"
  10.624 -   unfolding sset_def
  10.625 -   using matrix_setsum_finite[OF set1_NE[OF c] fin_set1[OF c]
  10.626 -                                 set2_NE[OF c] fin_set2[OF c] inj[OF c] ss[OF c]] by auto
  10.627 -  }
  10.628 -  then obtain Ms where
  10.629 -  ss1: "\<And> c b1. \<lbrakk>c \<in> set_of P; b1 \<in> set1 c\<rbrakk> \<Longrightarrow>
  10.630 -                   setsum (\<lambda> b2. Ms c (u c b1 b2)) (set2 c) = count N1 b1" and
  10.631 -  ss2: "\<And> c b2. \<lbrakk>c \<in> set_of P; b2 \<in> set2 c\<rbrakk> \<Longrightarrow>
  10.632 -                   setsum (\<lambda> b1. Ms c (u c b1 b2)) (set1 c) = count N2 b2"
  10.633 -  by metis
  10.634 -  def SET \<equiv> "\<Union> c \<in> set_of P. sset c"
  10.635 -  have fin_SET[simp]: "finite SET" unfolding SET_def apply(rule finite_UN_I) by auto
  10.636 -  have SET_A: "SET \<subseteq> A" unfolding SET_def using sset_A by blast
  10.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"
  10.638 -    unfolding SET_def sset_def by blast
  10.639 -  {fix c a assume c: "c \<in> set_of P" and a: "a \<in> SET" and p1a: "p1 a \<in> set1 c"
  10.640 -   then obtain c' where c': "c' \<in> set_of P" and ac': "a \<in> sset c'"
  10.641 -    unfolding SET_def by auto
  10.642 -   hence "p1 a \<in> set1 c'" unfolding sset_def by auto
  10.643 -   hence eq: "c = c'" using p1a c c' set1_disj by auto
  10.644 -   hence "a \<in> sset c" using ac' by simp
  10.645 -  } note p1_rev = this
  10.646 -  {fix c a assume c: "c \<in> set_of P" and a: "a \<in> SET" and p2a: "p2 a \<in> set2 c"
  10.647 -   then obtain c' where c': "c' \<in> set_of P" and ac': "a \<in> sset c'"
  10.648 -   unfolding SET_def by auto
  10.649 -   hence "p2 a \<in> set2 c'" unfolding sset_def by auto
  10.650 -   hence eq: "c = c'" using p2a c c' set2_disj by auto
  10.651 -   hence "a \<in> sset c" using ac' by simp
  10.652 -  } note p2_rev = this
  10.653 -  (*  *)
  10.654 -  have "\<forall> a \<in> SET. \<exists> c \<in> set_of P. a \<in> sset c" unfolding SET_def by auto
  10.655 -  then obtain h where h: "\<forall> a \<in> SET. h a \<in> set_of P \<and> a \<in> sset (h a)" by metis
  10.656 -  have h_u[simp]: "\<And> c b1 b2. \<lbrakk>c \<in> set_of P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk>
  10.657 -                      \<Longrightarrow> h (u c b1 b2) = c"
  10.658 -  by (metis h p2 set2 u(3) u_SET)
  10.659 -  have h_u1: "\<And> c b1 b2. \<lbrakk>c \<in> set_of P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk>
  10.660 -                      \<Longrightarrow> h (u c b1 b2) = f1 b1"
  10.661 -  using h unfolding sset_def by auto
  10.662 -  have h_u2: "\<And> c b1 b2. \<lbrakk>c \<in> set_of P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk>
  10.663 -                      \<Longrightarrow> h (u c b1 b2) = f2 b2"
  10.664 -  using h unfolding sset_def by auto
  10.665 -  def M \<equiv>
  10.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)"
  10.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"
  10.668 -    unfolding multiset_def by auto
  10.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"
  10.670 -    unfolding M_def pcr_multiset_def cr_multiset_def by (auto simp: Abs_multiset_inverse)
  10.671 -  have sM: "set_of M \<subseteq> SET" "set_of M \<subseteq> p1 -` (set_of N1)" "set_of M \<subseteq> p2 -` set_of N2"
  10.672 -    by (transfer, auto split: split_if_asm)+
  10.673 -  show "\<exists>M. set_of M \<subseteq> A \<and> mmap p1 M = N1 \<and> mmap p2 M = N2"
  10.674 -  proof(rule exI[of _ M], safe)
  10.675 -    fix a assume *: "a \<in> set_of M"
  10.676 -    from SET_A show "a \<in> A"
  10.677 -    proof (cases "a \<in> SET")
  10.678 -      case False thus ?thesis using * by transfer' auto
  10.679 -    qed blast
  10.680 -  next
  10.681 -    show "mmap p1 M = N1"
  10.682 -    proof(intro multiset_eqI)
  10.683 -      fix b1
  10.684 -      let ?K = "{a. p1 a = b1 \<and> a \<in># M}"
  10.685 -      have "setsum (count M) ?K = count N1 b1"
  10.686 -      proof(cases "b1 \<in> set_of N1")
  10.687 -        case False
  10.688 -        hence "?K = {}" using sM(2) by auto
  10.689 -        thus ?thesis using False by auto
  10.690 -      next
  10.691 -        case True
  10.692 -        def c \<equiv> "f1 b1"
  10.693 -        have c: "c \<in> set_of P" and b1: "b1 \<in> set1 c"
  10.694 -          unfolding set1_def c_def P1 using True by (auto simp: comp_eq_dest[OF set_of_mmap])
  10.695 -        with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p1 a = b1 \<and> a \<in> SET}"
  10.696 -          by transfer (force intro: setsum_mono_zero_cong_left split: split_if_asm)
  10.697 -        also have "... = setsum (count M) ((\<lambda> b2. u c b1 b2) ` (set2 c))"
  10.698 -          apply(rule setsum_cong) using c b1 proof safe
  10.699 -          fix a assume p1a: "p1 a \<in> set1 c" and "c \<in> set_of P" and "a \<in> SET"
  10.700 -          hence ac: "a \<in> sset c" using p1_rev by auto
  10.701 -          hence "a = u c (p1 a) (p2 a)" using c by auto
  10.702 -          moreover have "p2 a \<in> set2 c" using ac c by auto
  10.703 -          ultimately show "a \<in> u c (p1 a) ` set2 c" by auto
  10.704 -        qed auto
  10.705 -        also have "... = setsum (\<lambda> b2. count M (u c b1 b2)) (set2 c)"
  10.706 -          unfolding comp_def[symmetric] apply(rule setsum_reindex)
  10.707 -          using inj unfolding inj_on_def inj2_def using b1 c u(3) by blast
  10.708 -        also have "... = count N1 b1" unfolding ss1[OF c b1, symmetric]
  10.709 -          apply(rule setsum_cong[OF refl]) apply (transfer fixing: Ms u c b1 set2)
  10.710 -          using True h_u[OF c b1] set2_def u(2,3)[OF c b1] u_SET[OF c b1] by fastforce
  10.711 -        finally show ?thesis .
  10.712 -      qed
  10.713 -      thus "count (mmap p1 M) b1 = count N1 b1" by transfer
  10.714 -    qed
  10.715 -  next
  10.716 -next
  10.717 -    show "mmap p2 M = N2"
  10.718 -    proof(intro multiset_eqI)
  10.719 -      fix b2
  10.720 -      let ?K = "{a. p2 a = b2 \<and> a \<in># M}"
  10.721 -      have "setsum (count M) ?K = count N2 b2"
  10.722 -      proof(cases "b2 \<in> set_of N2")
  10.723 -        case False
  10.724 -        hence "?K = {}" using sM(3) by auto
  10.725 -        thus ?thesis using False by auto
  10.726 -      next
  10.727 -        case True
  10.728 -        def c \<equiv> "f2 b2"
  10.729 -        have c: "c \<in> set_of P" and b2: "b2 \<in> set2 c"
  10.730 -          unfolding set2_def c_def P2 using True by (auto simp: comp_eq_dest[OF set_of_mmap])
  10.731 -        with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p2 a = b2 \<and> a \<in> SET}"
  10.732 -          by transfer (force intro: setsum_mono_zero_cong_left split: split_if_asm)
  10.733 -        also have "... = setsum (count M) ((\<lambda> b1. u c b1 b2) ` (set1 c))"
  10.734 -          apply(rule setsum_cong) using c b2 proof safe
  10.735 -          fix a assume p2a: "p2 a \<in> set2 c" and "c \<in> set_of P" and "a \<in> SET"
  10.736 -          hence ac: "a \<in> sset c" using p2_rev by auto
  10.737 -          hence "a = u c (p1 a) (p2 a)" using c by auto
  10.738 -          moreover have "p1 a \<in> set1 c" using ac c by auto
  10.739 -          ultimately show "a \<in> (\<lambda>x. u c x (p2 a)) ` set1 c" by auto
  10.740 -        qed auto
  10.741 -        also have "... = setsum (count M o (\<lambda> b1. u c b1 b2)) (set1 c)"
  10.742 -          apply(rule setsum_reindex)
  10.743 -          using inj unfolding inj_on_def inj2_def using b2 c u(2) by blast
  10.744 -        also have "... = setsum (\<lambda> b1. count M (u c b1 b2)) (set1 c)" by simp
  10.745 -        also have "... = count N2 b2" unfolding ss2[OF c b2, symmetric] comp_def
  10.746 -          apply(rule setsum_cong[OF refl]) apply (transfer fixing: Ms u c b2 set1)
  10.747 -          using True h_u1[OF c _ b2] u(2,3)[OF c _ b2] u_SET[OF c _ b2] set1_def by fastforce
  10.748 -        finally show ?thesis .
  10.749 -      qed
  10.750 -      thus "count (mmap p2 M) b2 = count N2 b2" by transfer
  10.751 -    qed
  10.752 -  qed
  10.753 -qed
  10.754 -
  10.755 -lemma set_of_bd: "|set_of x| \<le>o natLeq"
  10.756 -  by transfer
  10.757 -    (auto intro!: ordLess_imp_ordLeq simp: finite_iff_ordLess_natLeq[symmetric] multiset_def)
  10.758 -
  10.759 -lemma wppull_mmap:
  10.760 -  assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
  10.761 -  shows "wppull {M. set_of M \<subseteq> A} {N1. set_of N1 \<subseteq> B1} {N2. set_of N2 \<subseteq> B2}
  10.762 -    (mmap f1) (mmap f2) (mmap e1) (mmap e2) (mmap p1) (mmap p2)"
  10.763 -proof -
  10.764 -  from assms obtain j where j: "\<forall>a'\<in>thePull B1 B2 f1 f2.
  10.765 -    j a' \<in> A \<and> e1 (p1 (j a')) = e1 (fst a') \<and> e2 (p2 (j a')) = e2 (snd a')" 
  10.766 -    by (blast dest: wppull_thePull)
  10.767 -  then show ?thesis
  10.768 -    by (intro wpull_wppull[OF wpull_mmap[OF wpull_thePull], of _ _ _ _ "mmap j"])
  10.769 -      (auto simp: comp_eq_dest_lhs[OF mmap_comp[symmetric]] comp_eq_dest[OF set_of_mmap]
  10.770 -        intro!: mmap_cong simp del: mem_set_of_iff simp: mem_set_of_iff[symmetric])
  10.771 -qed
  10.772 -
  10.773 -bnf "'a multiset"
  10.774 -  map: mmap
  10.775 -  sets: set_of 
  10.776 -  bd: natLeq
  10.777 -  wits: "{#}"
  10.778 -by (auto simp add: mmap_id0 mmap_comp set_of_mmap natLeq_card_order natLeq_cinfinite set_of_bd
  10.779 -  Grp_def relcompp.simps intro: mmap_cong)
  10.780 -  (metis wppull_mmap[OF wppull_fstOp_sndOp, unfolded wppull_def
  10.781 -    o_eq_dest_lhs[OF mmap_comp[symmetric]] fstOp_def sndOp_def comp_def, simplified])
  10.782 -
  10.783 -inductive rel_multiset' where
  10.784 -  Zero[intro]: "rel_multiset' R {#} {#}"
  10.785 -| Plus[intro]: "\<lbrakk>R a b; rel_multiset' R M N\<rbrakk> \<Longrightarrow> rel_multiset' R (M + {#a#}) (N + {#b#})"
  10.786 -
  10.787 -lemma map_multiset_Zero_iff[simp]: "mmap f M = {#} \<longleftrightarrow> M = {#}"
  10.788 -by (metis image_is_empty multiset.set_map set_of_eq_empty_iff)
  10.789 -
  10.790 -lemma map_multiset_Zero[simp]: "mmap f {#} = {#}" by simp
  10.791 -
  10.792 -lemma rel_multiset_Zero: "rel_multiset R {#} {#}"
  10.793 -unfolding rel_multiset_def Grp_def by auto
  10.794 -
  10.795 -declare multiset.count[simp]
  10.796 -declare Abs_multiset_inverse[simp]
  10.797 -declare multiset.count_inverse[simp]
  10.798 -declare union_preserves_multiset[simp]
  10.799 -
  10.800 -
  10.801 -lemma map_multiset_Plus[simp]: "mmap f (M1 + M2) = mmap f M1 + mmap f M2"
  10.802 -proof (intro multiset_eqI, transfer fixing: f)
  10.803 -  fix x :: 'a and M1 M2 :: "'b \<Rightarrow> nat"
  10.804 -  assume "M1 \<in> multiset" "M2 \<in> multiset"
  10.805 -  hence "setsum M1 {a. f a = x \<and> 0 < M1 a} = setsum M1 {a. f a = x \<and> 0 < M1 a + M2 a}"
  10.806 -        "setsum M2 {a. f a = x \<and> 0 < M2 a} = setsum M2 {a. f a = x \<and> 0 < M1 a + M2 a}"
  10.807 -    by (auto simp: multiset_def intro!: setsum_mono_zero_cong_left)
  10.808 -  then show "(\<Sum>a | f a = x \<and> 0 < M1 a + M2 a. M1 a + M2 a) =
  10.809 -       setsum M1 {a. f a = x \<and> 0 < M1 a} +
  10.810 -       setsum M2 {a. f a = x \<and> 0 < M2 a}"
  10.811 -    by (auto simp: setsum.distrib[symmetric])
  10.812 -qed
  10.813 -
  10.814 -lemma map_multiset_singl[simp]: "mmap f {#a#} = {#f a#}"
  10.815 -  by transfer auto
  10.816 -
  10.817 -lemma rel_multiset_Plus:
  10.818 -assumes ab: "R a b" and MN: "rel_multiset R M N"
  10.819 -shows "rel_multiset R (M + {#a#}) (N + {#b#})"
  10.820 -proof-
  10.821 -  {fix y assume "R a b" and "set_of y \<subseteq> {(x, y). R x y}"
  10.822 -   hence "\<exists>ya. mmap fst y + {#a#} = mmap fst ya \<and>
  10.823 -               mmap snd y + {#b#} = mmap snd ya \<and>
  10.824 -               set_of ya \<subseteq> {(x, y). R x y}"
  10.825 -   apply(intro exI[of _ "y + {#(a,b)#}"]) by auto
  10.826 -  }
  10.827 -  thus ?thesis
  10.828 -  using assms
  10.829 -  unfolding rel_multiset_def Grp_def by force
  10.830 -qed
  10.831 -
  10.832 -lemma rel_multiset'_imp_rel_multiset:
  10.833 -"rel_multiset' R M N \<Longrightarrow> rel_multiset R M N"
  10.834 -apply(induct rule: rel_multiset'.induct)
  10.835 -using rel_multiset_Zero rel_multiset_Plus by auto
  10.836 -
  10.837 -lemma mcard_mmap[simp]: "mcard (mmap f M) = mcard M"
  10.838 -proof -
  10.839 -  def A \<equiv> "\<lambda> b. {a. f a = b \<and> a \<in># M}"
  10.840 -  let ?B = "{b. 0 < setsum (count M) (A b)}"
  10.841 -  have "{b. \<exists>a. f a = b \<and> a \<in># M} \<subseteq> f ` {a. a \<in># M}" by auto
  10.842 -  moreover have "finite (f ` {a. a \<in># M})" apply(rule finite_imageI)
  10.843 -  using finite_Collect_mem .
  10.844 -  ultimately have fin: "finite {b. \<exists>a. f a = b \<and> a \<in># M}" by(rule finite_subset)
  10.845 -  have i: "inj_on A ?B" unfolding inj_on_def A_def apply clarsimp
  10.846 -    by (metis (lifting, full_types) mem_Collect_eq neq0_conv setsum.neutral)
  10.847 -  have 0: "\<And> b. 0 < setsum (count M) (A b) \<longleftrightarrow> (\<exists> a \<in> A b. count M a > 0)"
  10.848 -  apply safe
  10.849 -    apply (metis less_not_refl setsum_gt_0_iff setsum_infinite)
  10.850 -    by (metis A_def finite_Collect_conjI finite_Collect_mem setsum_gt_0_iff)
  10.851 -  hence AB: "A ` ?B = {A b | b. \<exists> a \<in> A b. count M a > 0}" by auto
  10.852 -
  10.853 -  have "setsum (\<lambda> x. setsum (count M) (A x)) ?B = setsum (setsum (count M) o A) ?B"
  10.854 -  unfolding comp_def ..
  10.855 -  also have "... = (\<Sum>x\<in> A ` ?B. setsum (count M) x)"
  10.856 -  unfolding setsum.reindex [OF i, symmetric] ..
  10.857 -  also have "... = setsum (count M) (\<Union>x\<in>A ` {b. 0 < setsum (count M) (A b)}. x)"
  10.858 -  (is "_ = setsum (count M) ?J")
  10.859 -  apply(rule setsum.UNION_disjoint[symmetric])
  10.860 -  using 0 fin unfolding A_def by auto
  10.861 -  also have "?J = {a. a \<in># M}" unfolding AB unfolding A_def by auto
  10.862 -  finally have "setsum (\<lambda> x. setsum (count M) (A x)) ?B =
  10.863 -                setsum (count M) {a. a \<in># M}" .
  10.864 -  then show ?thesis unfolding mcard_unfold_setsum A_def by transfer
  10.865 -qed
  10.866 -
  10.867 -lemma rel_multiset_mcard:
  10.868 -assumes "rel_multiset R M N"
  10.869 -shows "mcard M = mcard N"
  10.870 -using assms unfolding rel_multiset_def Grp_def by auto
  10.871 -
  10.872 -lemma multiset_induct2[case_names empty addL addR]:
  10.873 -assumes empty: "P {#} {#}"
  10.874 -and addL: "\<And>M N a. P M N \<Longrightarrow> P (M + {#a#}) N"
  10.875 -and addR: "\<And>M N a. P M N \<Longrightarrow> P M (N + {#a#})"
  10.876 -shows "P M N"
  10.877 -apply(induct N rule: multiset_induct)
  10.878 -  apply(induct M rule: multiset_induct, rule empty, erule addL)
  10.879 -  apply(induct M rule: multiset_induct, erule addR, erule addR)
  10.880 -done
  10.881 -
  10.882 -lemma multiset_induct2_mcard[consumes 1, case_names empty add]:
  10.883 -assumes c: "mcard M = mcard N"
  10.884 -and empty: "P {#} {#}"
  10.885 -and add: "\<And>M N a b. P M N \<Longrightarrow> P (M + {#a#}) (N + {#b#})"
  10.886 -shows "P M N"
  10.887 -using c proof(induct M arbitrary: N rule: measure_induct_rule[of mcard])
  10.888 -  case (less M)  show ?case
  10.889 -  proof(cases "M = {#}")
  10.890 -    case True hence "N = {#}" using less.prems by auto
  10.891 -    thus ?thesis using True empty by auto
  10.892 -  next
  10.893 -    case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split)
  10.894 -    have "N \<noteq> {#}" using False less.prems by auto
  10.895 -    then obtain N1 b where N: "N = N1 + {#b#}" by (metis multi_nonempty_split)
  10.896 -    have "mcard M1 = mcard N1" using less.prems unfolding M N by auto
  10.897 -    thus ?thesis using M N less.hyps add by auto
  10.898 -  qed
  10.899 -qed
  10.900 -
  10.901 -lemma msed_map_invL:
  10.902 -assumes "mmap f (M + {#a#}) = N"
  10.903 -shows "\<exists> N1. N = N1 + {#f a#} \<and> mmap f M = N1"
  10.904 -proof-
  10.905 -  have "f a \<in># N"
  10.906 -  using assms multiset.set_map[of f "M + {#a#}"] by auto
  10.907 -  then obtain N1 where N: "N = N1 + {#f a#}" using multi_member_split by metis
  10.908 -  have "mmap f M = N1" using assms unfolding N by simp
  10.909 -  thus ?thesis using N by blast
  10.910 -qed
  10.911 -
  10.912 -lemma msed_map_invR:
  10.913 -assumes "mmap f M = N + {#b#}"
  10.914 -shows "\<exists> M1 a. M = M1 + {#a#} \<and> f a = b \<and> mmap f M1 = N"
  10.915 -proof-
  10.916 -  obtain a where a: "a \<in># M" and fa: "f a = b"
  10.917 -  using multiset.set_map[of f M] unfolding assms
  10.918 -  by (metis image_iff mem_set_of_iff union_single_eq_member)
  10.919 -  then obtain M1 where M: "M = M1 + {#a#}" using multi_member_split by metis
  10.920 -  have "mmap f M1 = N" using assms unfolding M fa[symmetric] by simp
  10.921 -  thus ?thesis using M fa by blast
  10.922 -qed
  10.923 -
  10.924 -lemma msed_rel_invL:
  10.925 -assumes "rel_multiset R (M + {#a#}) N"
  10.926 -shows "\<exists> N1 b. N = N1 + {#b#} \<and> R a b \<and> rel_multiset R M N1"
  10.927 -proof-
  10.928 -  obtain K where KM: "mmap fst K = M + {#a#}"
  10.929 -  and KN: "mmap snd K = N" and sK: "set_of K \<subseteq> {(a, b). R a b}"
  10.930 -  using assms
  10.931 -  unfolding rel_multiset_def Grp_def by auto
  10.932 -  obtain K1 ab where K: "K = K1 + {#ab#}" and a: "fst ab = a"
  10.933 -  and K1M: "mmap fst K1 = M" using msed_map_invR[OF KM] by auto
  10.934 -  obtain N1 where N: "N = N1 + {#snd ab#}" and K1N1: "mmap snd K1 = N1"
  10.935 -  using msed_map_invL[OF KN[unfolded K]] by auto
  10.936 -  have Rab: "R a (snd ab)" using sK a unfolding K by auto
  10.937 -  have "rel_multiset R M N1" using sK K1M K1N1
  10.938 -  unfolding K rel_multiset_def Grp_def by auto
  10.939 -  thus ?thesis using N Rab by auto
  10.940 -qed
  10.941 -
  10.942 -lemma msed_rel_invR:
  10.943 -assumes "rel_multiset R M (N + {#b#})"
  10.944 -shows "\<exists> M1 a. M = M1 + {#a#} \<and> R a b \<and> rel_multiset R M1 N"
  10.945 -proof-
  10.946 -  obtain K where KN: "mmap snd K = N + {#b#}"
  10.947 -  and KM: "mmap fst K = M" and sK: "set_of K \<subseteq> {(a, b). R a b}"
  10.948 -  using assms
  10.949 -  unfolding rel_multiset_def Grp_def by auto
  10.950 -  obtain K1 ab where K: "K = K1 + {#ab#}" and b: "snd ab = b"
  10.951 -  and K1N: "mmap snd K1 = N" using msed_map_invR[OF KN] by auto
  10.952 -  obtain M1 where M: "M = M1 + {#fst ab#}" and K1M1: "mmap fst K1 = M1"
  10.953 -  using msed_map_invL[OF KM[unfolded K]] by auto
  10.954 -  have Rab: "R (fst ab) b" using sK b unfolding K by auto
  10.955 -  have "rel_multiset R M1 N" using sK K1N K1M1
  10.956 -  unfolding K rel_multiset_def Grp_def by auto
  10.957 -  thus ?thesis using M Rab by auto
  10.958 -qed
  10.959 -
  10.960 -lemma rel_multiset_imp_rel_multiset':
  10.961 -assumes "rel_multiset R M N"
  10.962 -shows "rel_multiset' R M N"
  10.963 -using assms proof(induct M arbitrary: N rule: measure_induct_rule[of mcard])
  10.964 -  case (less M)
  10.965 -  have c: "mcard M = mcard N" using rel_multiset_mcard[OF less.prems] .
  10.966 -  show ?case
  10.967 -  proof(cases "M = {#}")
  10.968 -    case True hence "N = {#}" using c by simp
  10.969 -    thus ?thesis using True rel_multiset'.Zero by auto
  10.970 -  next
  10.971 -    case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split)
  10.972 -    obtain N1 b where N: "N = N1 + {#b#}" and R: "R a b" and ms: "rel_multiset R M1 N1"
  10.973 -    using msed_rel_invL[OF less.prems[unfolded M]] by auto
  10.974 -    have "rel_multiset' R M1 N1" using less.hyps[of M1 N1] ms unfolding M by simp
  10.975 -    thus ?thesis using rel_multiset'.Plus[of R a b, OF R] unfolding M N by simp
  10.976 -  qed
  10.977 -qed
  10.978 -
  10.979 -lemma rel_multiset_rel_multiset':
  10.980 -"rel_multiset R M N = rel_multiset' R M N"
  10.981 -using  rel_multiset_imp_rel_multiset' rel_multiset'_imp_rel_multiset by auto
  10.982 -
  10.983 -(* The main end product for rel_multiset: inductive characterization *)
  10.984 -theorems rel_multiset_induct[case_names empty add, induct pred: rel_multiset] =
  10.985 -         rel_multiset'.induct[unfolded rel_multiset_rel_multiset'[symmetric]]
  10.986 -
  10.987 -
  10.988 -(* Advanced relator customization *)
  10.989 -
  10.990 -(* Set vs. sum relators: *)
  10.991 -
  10.992 -lemma set_rel_sum_rel[simp]: 
  10.993 -"set_rel (sum_rel \<chi> \<phi>) A1 A2 \<longleftrightarrow> 
  10.994 - set_rel \<chi> (Inl -` A1) (Inl -` A2) \<and> set_rel \<phi> (Inr -` A1) (Inr -` A2)"
  10.995 -(is "?L \<longleftrightarrow> ?Rl \<and> ?Rr")
  10.996 -proof safe
  10.997 -  assume L: "?L"
  10.998 -  show ?Rl unfolding set_rel_def Bex_def vimage_eq proof safe
  10.999 -    fix l1 assume "Inl l1 \<in> A1"
 10.1000 -    then obtain a2 where a2: "a2 \<in> A2" and "sum_rel \<chi> \<phi> (Inl l1) a2"
 10.1001 -    using L unfolding set_rel_def by auto
 10.1002 -    then obtain l2 where "a2 = Inl l2 \<and> \<chi> l1 l2" by (cases a2, auto)
 10.1003 -    thus "\<exists> l2. Inl l2 \<in> A2 \<and> \<chi> l1 l2" using a2 by auto
 10.1004 -  next
 10.1005 -    fix l2 assume "Inl l2 \<in> A2"
 10.1006 -    then obtain a1 where a1: "a1 \<in> A1" and "sum_rel \<chi> \<phi> a1 (Inl l2)"
 10.1007 -    using L unfolding set_rel_def by auto
 10.1008 -    then obtain l1 where "a1 = Inl l1 \<and> \<chi> l1 l2" by (cases a1, auto)
 10.1009 -    thus "\<exists> l1. Inl l1 \<in> A1 \<and> \<chi> l1 l2" using a1 by auto
 10.1010 -  qed
 10.1011 -  show ?Rr unfolding set_rel_def Bex_def vimage_eq proof safe
 10.1012 -    fix r1 assume "Inr r1 \<in> A1"
 10.1013 -    then obtain a2 where a2: "a2 \<in> A2" and "sum_rel \<chi> \<phi> (Inr r1) a2"
 10.1014 -    using L unfolding set_rel_def by auto
 10.1015 -    then obtain r2 where "a2 = Inr r2 \<and> \<phi> r1 r2" by (cases a2, auto)
 10.1016 -    thus "\<exists> r2. Inr r2 \<in> A2 \<and> \<phi> r1 r2" using a2 by auto
 10.1017 -  next
 10.1018 -    fix r2 assume "Inr r2 \<in> A2"
 10.1019 -    then obtain a1 where a1: "a1 \<in> A1" and "sum_rel \<chi> \<phi> a1 (Inr r2)"
 10.1020 -    using L unfolding set_rel_def by auto
 10.1021 -    then obtain r1 where "a1 = Inr r1 \<and> \<phi> r1 r2" by (cases a1, auto)
 10.1022 -    thus "\<exists> r1. Inr r1 \<in> A1 \<and> \<phi> r1 r2" using a1 by auto
 10.1023 -  qed
 10.1024 -next
 10.1025 -  assume Rl: "?Rl" and Rr: "?Rr"
 10.1026 -  show ?L unfolding set_rel_def Bex_def vimage_eq proof safe
 10.1027 -    fix a1 assume a1: "a1 \<in> A1"
 10.1028 -    show "\<exists> a2. a2 \<in> A2 \<and> sum_rel \<chi> \<phi> a1 a2"
 10.1029 -    proof(cases a1)
 10.1030 -      case (Inl l1) then obtain l2 where "Inl l2 \<in> A2 \<and> \<chi> l1 l2"
 10.1031 -      using Rl a1 unfolding set_rel_def by blast
 10.1032 -      thus ?thesis unfolding Inl by auto
 10.1033 -    next
 10.1034 -      case (Inr r1) then obtain r2 where "Inr r2 \<in> A2 \<and> \<phi> r1 r2"
 10.1035 -      using Rr a1 unfolding set_rel_def by blast
 10.1036 -      thus ?thesis unfolding Inr by auto
 10.1037 -    qed
 10.1038 -  next
 10.1039 -    fix a2 assume a2: "a2 \<in> A2"
 10.1040 -    show "\<exists> a1. a1 \<in> A1 \<and> sum_rel \<chi> \<phi> a1 a2"
 10.1041 -    proof(cases a2)
 10.1042 -      case (Inl l2) then obtain l1 where "Inl l1 \<in> A1 \<and> \<chi> l1 l2"
 10.1043 -      using Rl a2 unfolding set_rel_def by blast
 10.1044 -      thus ?thesis unfolding Inl by auto
 10.1045 -    next
 10.1046 -      case (Inr r2) then obtain r1 where "Inr r1 \<in> A1 \<and> \<phi> r1 r2"
 10.1047 -      using Rr a2 unfolding set_rel_def by blast
 10.1048 -      thus ?thesis unfolding Inr by auto
 10.1049 -    qed
 10.1050 -  qed
 10.1051 -qed
 10.1052 -
 10.1053 -end
    11.1 --- a/src/HOL/Library/Multiset.thy	Fri Jan 24 15:21:00 2014 +0000
    11.2 +++ b/src/HOL/Library/Multiset.thy	Fri Jan 24 16:54:25 2014 +0000
    11.3 @@ -1,5 +1,6 @@
    11.4  (*  Title:      HOL/Library/Multiset.thy
    11.5      Author:     Tobias Nipkow, Markus Wenzel, Lawrence C Paulson, Norbert Voelker
    11.6 +    Author:     Andrei Popescu, TU Muenchen
    11.7  *)
    11.8  
    11.9  header {* (Finite) multisets *}
   11.10 @@ -2157,5 +2158,810 @@
   11.11  
   11.12  hide_const (open) msetify
   11.13  
   11.14 +
   11.15 +subsection {* BNF setup *}
   11.16 +
   11.17 +lemma setsum_gt_0_iff:
   11.18 +fixes f :: "'a \<Rightarrow> nat" assumes "finite A"
   11.19 +shows "setsum f A > 0 \<longleftrightarrow> (\<exists> a \<in> A. f a > 0)"
   11.20 +(is "?L \<longleftrightarrow> ?R")
   11.21 +proof-
   11.22 +  have "?L \<longleftrightarrow> \<not> setsum f A = 0" by fast
   11.23 +  also have "... \<longleftrightarrow> (\<exists> a \<in> A. f a \<noteq> 0)" using assms by simp
   11.24 +  also have "... \<longleftrightarrow> ?R" by simp
   11.25 +  finally show ?thesis .
   11.26 +qed
   11.27 +
   11.28 +lift_definition mmap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" is
   11.29 +  "\<lambda>h f b. setsum f {a. h a = b \<and> f a > 0} :: nat"
   11.30 +unfolding multiset_def proof safe
   11.31 +  fix h :: "'a \<Rightarrow> 'b" and f :: "'a \<Rightarrow> nat"
   11.32 +  assume fin: "finite {a. 0 < f a}"  (is "finite ?A")
   11.33 +  show "finite {b. 0 < setsum f {a. h a = b \<and> 0 < f a}}"
   11.34 +  (is "finite {b. 0 < setsum f (?As b)}")
   11.35 +  proof- let ?B = "{b. 0 < setsum f (?As b)}"
   11.36 +    have "\<And> b. finite (?As b)" using fin by simp
   11.37 +    hence B: "?B = {b. ?As b \<noteq> {}}" by (auto simp add: setsum_gt_0_iff)
   11.38 +    hence "?B \<subseteq> h ` ?A" by auto
   11.39 +    thus ?thesis using finite_surj[OF fin] by auto
   11.40 +  qed
   11.41 +qed
   11.42 +
   11.43 +lemma mmap_id0: "mmap id = id"
   11.44 +proof (intro ext multiset_eqI)
   11.45 +  fix f a show "count (mmap id f) a = count (id f) a"
   11.46 +  proof (cases "count f a = 0")
   11.47 +    case False
   11.48 +    hence 1: "{aa. aa = a \<and> aa \<in># f} = {a}" by auto
   11.49 +    thus ?thesis by transfer auto
   11.50 +  qed (transfer, simp)
   11.51 +qed
   11.52 +
   11.53 +lemma inj_on_setsum_inv:
   11.54 +assumes 1: "(0::nat) < setsum (count f) {a. h a = b' \<and> a \<in># f}" (is "0 < setsum (count f) ?A'")
   11.55 +and     2: "{a. h a = b \<and> a \<in># f} = {a. h a = b' \<and> a \<in># f}" (is "?A = ?A'")
   11.56 +shows "b = b'"
   11.57 +using assms by (auto simp add: setsum_gt_0_iff)
   11.58 +
   11.59 +lemma mmap_comp:
   11.60 +fixes h1 :: "'a \<Rightarrow> 'b" and h2 :: "'b \<Rightarrow> 'c"
   11.61 +shows "mmap (h2 o h1) = mmap h2 o mmap h1"
   11.62 +proof (intro ext multiset_eqI)
   11.63 +  fix f :: "'a multiset" fix c :: 'c
   11.64 +  let ?A = "{a. h2 (h1 a) = c \<and> a \<in># f}"
   11.65 +  let ?As = "\<lambda> b. {a. h1 a = b \<and> a \<in># f}"
   11.66 +  let ?B = "{b. h2 b = c \<and> 0 < setsum (count f) (?As b)}"
   11.67 +  have 0: "{?As b | b.  b \<in> ?B} = ?As ` ?B" by auto
   11.68 +  have "\<And> b. finite (?As b)" by transfer (simp add: multiset_def)
   11.69 +  hence "?B = {b. h2 b = c \<and> ?As b \<noteq> {}}" by (auto simp add: setsum_gt_0_iff)
   11.70 +  hence A: "?A = \<Union> {?As b | b.  b \<in> ?B}" by auto
   11.71 +  have "setsum (count f) ?A = setsum (setsum (count f)) {?As b | b.  b \<in> ?B}"
   11.72 +    unfolding A by transfer (intro setsum_Union_disjoint, auto simp: multiset_def)
   11.73 +  also have "... = setsum (setsum (count f)) (?As ` ?B)" unfolding 0 ..
   11.74 +  also have "... = setsum (setsum (count f) o ?As) ?B"
   11.75 +    by(intro setsum_reindex) (auto simp add: setsum_gt_0_iff inj_on_def)
   11.76 +  also have "... = setsum (\<lambda> b. setsum (count f) (?As b)) ?B" unfolding comp_def ..
   11.77 +  finally have "setsum (count f) ?A = setsum (\<lambda> b. setsum (count f) (?As b)) ?B" .
   11.78 +  thus "count (mmap (h2 \<circ> h1) f) c = count ((mmap h2 \<circ> mmap h1) f) c"
   11.79 +    by transfer (unfold comp_apply, blast)
   11.80 +qed
   11.81 +
   11.82 +lemma mmap_cong:
   11.83 +assumes "\<And>a. a \<in># M \<Longrightarrow> f a = g a"
   11.84 +shows "mmap f M = mmap g M"
   11.85 +using assms by transfer (auto intro!: setsum_cong)
   11.86 +
   11.87 +context
   11.88 +begin
   11.89 +interpretation lifting_syntax .
   11.90 +
   11.91 +lemma set_of_transfer[transfer_rule]: "(pcr_multiset op = ===> op =) (\<lambda>f. {a. 0 < f a}) set_of"
   11.92 +  unfolding set_of_def pcr_multiset_def cr_multiset_def fun_rel_def by auto
   11.93 +
   11.94  end
   11.95  
   11.96 +lemma set_of_mmap: "set_of o mmap h = image h o set_of"
   11.97 +proof (rule ext, unfold comp_apply)
   11.98 +  fix M show "set_of (mmap h M) = h ` set_of M"
   11.99 +    by transfer (auto simp add: multiset_def setsum_gt_0_iff)
  11.100 +qed
  11.101 +
  11.102 +lemma multiset_of_surj:
  11.103 +  "multiset_of ` {as. set as \<subseteq> A} = {M. set_of M \<subseteq> A}"
  11.104 +proof safe
  11.105 +  fix M assume M: "set_of M \<subseteq> A"
  11.106 +  obtain as where eq: "M = multiset_of as" using surj_multiset_of unfolding surj_def by auto
  11.107 +  hence "set as \<subseteq> A" using M by auto
  11.108 +  thus "M \<in> multiset_of ` {as. set as \<subseteq> A}" using eq by auto
  11.109 +next
  11.110 +  show "\<And>x xa xb. \<lbrakk>set xa \<subseteq> A; xb \<in> set_of (multiset_of xa)\<rbrakk> \<Longrightarrow> xb \<in> A"
  11.111 +  by (erule set_mp) (unfold set_of_multiset_of)
  11.112 +qed
  11.113 +
  11.114 +lemma card_of_set_of:
  11.115 +"(card_of {M. set_of M \<subseteq> A}, card_of {as. set as \<subseteq> A}) \<in> ordLeq"
  11.116 +apply(rule card_of_ordLeqI2[of _ multiset_of]) using multiset_of_surj by auto
  11.117 +
  11.118 +lemma nat_sum_induct:
  11.119 +assumes "\<And>n1 n2. (\<And> m1 m2. m1 + m2 < n1 + n2 \<Longrightarrow> phi m1 m2) \<Longrightarrow> phi n1 n2"
  11.120 +shows "phi (n1::nat) (n2::nat)"
  11.121 +proof-
  11.122 +  let ?chi = "\<lambda> n1n2 :: nat * nat. phi (fst n1n2) (snd n1n2)"
  11.123 +  have "?chi (n1,n2)"
  11.124 +  apply(induct rule: measure_induct[of "\<lambda> n1n2. fst n1n2 + snd n1n2" ?chi])
  11.125 +  using assms by (metis fstI sndI)
  11.126 +  thus ?thesis by simp
  11.127 +qed
  11.128 +
  11.129 +lemma matrix_count:
  11.130 +fixes ct1 ct2 :: "nat \<Rightarrow> nat"
  11.131 +assumes "setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2}"
  11.132 +shows
  11.133 +"\<exists> ct. (\<forall> i1 \<le> n1. setsum (\<lambda> i2. ct i1 i2) {..<Suc n2} = ct1 i1) \<and>
  11.134 +       (\<forall> i2 \<le> n2. setsum (\<lambda> i1. ct i1 i2) {..<Suc n1} = ct2 i2)"
  11.135 +(is "?phi ct1 ct2 n1 n2")
  11.136 +proof-
  11.137 +  have "\<forall> ct1 ct2 :: nat \<Rightarrow> nat.
  11.138 +        setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2} \<longrightarrow> ?phi ct1 ct2 n1 n2"
  11.139 +  proof(induct rule: nat_sum_induct[of
  11.140 +"\<lambda> n1 n2. \<forall> ct1 ct2 :: nat \<Rightarrow> nat.
  11.141 +     setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2} \<longrightarrow> ?phi ct1 ct2 n1 n2"],
  11.142 +      clarify)
  11.143 +  fix n1 n2 :: nat and ct1 ct2 :: "nat \<Rightarrow> nat"
  11.144 +  assume IH: "\<And> m1 m2. m1 + m2 < n1 + n2 \<Longrightarrow>
  11.145 +                \<forall> dt1 dt2 :: nat \<Rightarrow> nat.
  11.146 +                setsum dt1 {..<Suc m1} = setsum dt2 {..<Suc m2} \<longrightarrow> ?phi dt1 dt2 m1 m2"
  11.147 +  and ss: "setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2}"
  11.148 +  show "?phi ct1 ct2 n1 n2"
  11.149 +  proof(cases n1)
  11.150 +    case 0 note n1 = 0
  11.151 +    show ?thesis
  11.152 +    proof(cases n2)
  11.153 +      case 0 note n2 = 0
  11.154 +      let ?ct = "\<lambda> i1 i2. ct2 0"
  11.155 +      show ?thesis apply(rule exI[of _ ?ct]) using n1 n2 ss by simp
  11.156 +    next
  11.157 +      case (Suc m2) note n2 = Suc
  11.158 +      let ?ct = "\<lambda> i1 i2. ct2 i2"
  11.159 +      show ?thesis apply(rule exI[of _ ?ct]) using n1 n2 ss by auto
  11.160 +    qed
  11.161 +  next
  11.162 +    case (Suc m1) note n1 = Suc
  11.163 +    show ?thesis
  11.164 +    proof(cases n2)
  11.165 +      case 0 note n2 = 0
  11.166 +      let ?ct = "\<lambda> i1 i2. ct1 i1"
  11.167 +      show ?thesis apply(rule exI[of _ ?ct]) using n1 n2 ss by auto
  11.168 +    next
  11.169 +      case (Suc m2) note n2 = Suc
  11.170 +      show ?thesis
  11.171 +      proof(cases "ct1 n1 \<le> ct2 n2")
  11.172 +        case True
  11.173 +        def dt2 \<equiv> "\<lambda> i2. if i2 = n2 then ct2 i2 - ct1 n1 else ct2 i2"
  11.174 +        have "setsum ct1 {..<Suc m1} = setsum dt2 {..<Suc n2}"
  11.175 +        unfolding dt2_def using ss n1 True by auto
  11.176 +        hence "?phi ct1 dt2 m1 n2" using IH[of m1 n2] n1 by simp
  11.177 +        then obtain dt where
  11.178 +        1: "\<And> i1. i1 \<le> m1 \<Longrightarrow> setsum (\<lambda> i2. dt i1 i2) {..<Suc n2} = ct1 i1" and
  11.179 +        2: "\<And> i2. i2 \<le> n2 \<Longrightarrow> setsum (\<lambda> i1. dt i1 i2) {..<Suc m1} = dt2 i2" by auto
  11.180 +        let ?ct = "\<lambda> i1 i2. if i1 = n1 then (if i2 = n2 then ct1 n1 else 0)
  11.181 +                                       else dt i1 i2"
  11.182 +        show ?thesis apply(rule exI[of _ ?ct])
  11.183 +        using n1 n2 1 2 True unfolding dt2_def by simp
  11.184 +      next
  11.185 +        case False
  11.186 +        hence False: "ct2 n2 < ct1 n1" by simp
  11.187 +        def dt1 \<equiv> "\<lambda> i1. if i1 = n1 then ct1 i1 - ct2 n2 else ct1 i1"
  11.188 +        have "setsum dt1 {..<Suc n1} = setsum ct2 {..<Suc m2}"
  11.189 +        unfolding dt1_def using ss n2 False by auto
  11.190 +        hence "?phi dt1 ct2 n1 m2" using IH[of n1 m2] n2 by simp
  11.191 +        then obtain dt where
  11.192 +        1: "\<And> i1. i1 \<le> n1 \<Longrightarrow> setsum (\<lambda> i2. dt i1 i2) {..<Suc m2} = dt1 i1" and
  11.193 +        2: "\<And> i2. i2 \<le> m2 \<Longrightarrow> setsum (\<lambda> i1. dt i1 i2) {..<Suc n1} = ct2 i2" by force
  11.194 +        let ?ct = "\<lambda> i1 i2. if i2 = n2 then (if i1 = n1 then ct2 n2 else 0)
  11.195 +                                       else dt i1 i2"
  11.196 +        show ?thesis apply(rule exI[of _ ?ct])
  11.197 +        using n1 n2 1 2 False unfolding dt1_def by simp
  11.198 +      qed
  11.199 +    qed
  11.200 +  qed
  11.201 +  qed
  11.202 +  thus ?thesis using assms by auto
  11.203 +qed
  11.204 +
  11.205 +definition
  11.206 +"inj2 u B1 B2 \<equiv>
  11.207 + \<forall> b1 b1' b2 b2'. {b1,b1'} \<subseteq> B1 \<and> {b2,b2'} \<subseteq> B2 \<and> u b1 b2 = u b1' b2'
  11.208 +                  \<longrightarrow> b1 = b1' \<and> b2 = b2'"
  11.209 +
  11.210 +lemma matrix_setsum_finite:
  11.211 +assumes B1: "B1 \<noteq> {}" "finite B1" and B2: "B2 \<noteq> {}" "finite B2" and u: "inj2 u B1 B2"
  11.212 +and ss: "setsum N1 B1 = setsum N2 B2"
  11.213 +shows "\<exists> M :: 'a \<Rightarrow> nat.
  11.214 +            (\<forall> b1 \<in> B1. setsum (\<lambda> b2. M (u b1 b2)) B2 = N1 b1) \<and>
  11.215 +            (\<forall> b2 \<in> B2. setsum (\<lambda> b1. M (u b1 b2)) B1 = N2 b2)"
  11.216 +proof-
  11.217 +  obtain n1 where "card B1 = Suc n1" using B1 by (metis card_insert finite.simps)
  11.218 +  then obtain e1 where e1: "bij_betw e1 {..<Suc n1} B1"
  11.219 +  using ex_bij_betw_finite_nat[OF B1(2)] by (metis atLeast0LessThan bij_betw_the_inv_into)
  11.220 +  hence e1_inj: "inj_on e1 {..<Suc n1}" and e1_surj: "e1 ` {..<Suc n1} = B1"
  11.221 +  unfolding bij_betw_def by auto
  11.222 +  def f1 \<equiv> "inv_into {..<Suc n1} e1"
  11.223 +  have f1: "bij_betw f1 B1 {..<Suc n1}"
  11.224 +  and f1e1[simp]: "\<And> i1. i1 < Suc n1 \<Longrightarrow> f1 (e1 i1) = i1"
  11.225 +  and e1f1[simp]: "\<And> b1. b1 \<in> B1 \<Longrightarrow> e1 (f1 b1) = b1" unfolding f1_def
  11.226 +  apply (metis bij_betw_inv_into e1, metis bij_betw_inv_into_left e1 lessThan_iff)
  11.227 +  by (metis e1_surj f_inv_into_f)
  11.228 +  (*  *)
  11.229 +  obtain n2 where "card B2 = Suc n2" using B2 by (metis card_insert finite.simps)
  11.230 +  then obtain e2 where e2: "bij_betw e2 {..<Suc n2} B2"
  11.231 +  using ex_bij_betw_finite_nat[OF B2(2)] by (metis atLeast0LessThan bij_betw_the_inv_into)
  11.232 +  hence e2_inj: "inj_on e2 {..<Suc n2}" and e2_surj: "e2 ` {..<Suc n2} = B2"
  11.233 +  unfolding bij_betw_def by auto
  11.234 +  def f2 \<equiv> "inv_into {..<Suc n2} e2"
  11.235 +  have f2: "bij_betw f2 B2 {..<Suc n2}"
  11.236 +  and f2e2[simp]: "\<And> i2. i2 < Suc n2 \<Longrightarrow> f2 (e2 i2) = i2"
  11.237 +  and e2f2[simp]: "\<And> b2. b2 \<in> B2 \<Longrightarrow> e2 (f2 b2) = b2" unfolding f2_def
  11.238 +  apply (metis bij_betw_inv_into e2, metis bij_betw_inv_into_left e2 lessThan_iff)
  11.239 +  by (metis e2_surj f_inv_into_f)
  11.240 +  (*  *)
  11.241 +  let ?ct1 = "N1 o e1"  let ?ct2 = "N2 o e2"
  11.242 +  have ss: "setsum ?ct1 {..<Suc n1} = setsum ?ct2 {..<Suc n2}"
  11.243 +  unfolding setsum_reindex[OF e1_inj, symmetric] setsum_reindex[OF e2_inj, symmetric]
  11.244 +  e1_surj e2_surj using ss .
  11.245 +  obtain ct where
  11.246 +  ct1: "\<And> i1. i1 \<le> n1 \<Longrightarrow> setsum (\<lambda> i2. ct i1 i2) {..<Suc n2} = ?ct1 i1" and
  11.247 +  ct2: "\<And> i2. i2 \<le> n2 \<Longrightarrow> setsum (\<lambda> i1. ct i1 i2) {..<Suc n1} = ?ct2 i2"
  11.248 +  using matrix_count[OF ss] by blast
  11.249 +  (*  *)
  11.250 +  def A \<equiv> "{u b1 b2 | b1 b2. b1 \<in> B1 \<and> b2 \<in> B2}"
  11.251 +  have "\<forall> a \<in> A. \<exists> b1b2 \<in> B1 <*> B2. u (fst b1b2) (snd b1b2) = a"
  11.252 +  unfolding A_def Ball_def mem_Collect_eq by auto
  11.253 +  then obtain h1h2 where h12:
  11.254 +  "\<And>a. a \<in> A \<Longrightarrow> u (fst (h1h2 a)) (snd (h1h2 a)) = a \<and> h1h2 a \<in> B1 <*> B2" by metis
  11.255 +  def h1 \<equiv> "fst o h1h2"  def h2 \<equiv> "snd o h1h2"
  11.256 +  have h12[simp]: "\<And>a. a \<in> A \<Longrightarrow> u (h1 a) (h2 a) = a"
  11.257 +                  "\<And> a. a \<in> A \<Longrightarrow> h1 a \<in> B1"  "\<And> a. a \<in> A \<Longrightarrow> h2 a \<in> B2"
  11.258 +  using h12 unfolding h1_def h2_def by force+
  11.259 +  {fix b1 b2 assume b1: "b1 \<in> B1" and b2: "b2 \<in> B2"
  11.260 +   hence inA: "u b1 b2 \<in> A" unfolding A_def by auto
  11.261 +   hence "u b1 b2 = u (h1 (u b1 b2)) (h2 (u b1 b2))" by auto
  11.262 +   moreover have "h1 (u b1 b2) \<in> B1" "h2 (u b1 b2) \<in> B2" using inA by auto
  11.263 +   ultimately have "h1 (u b1 b2) = b1 \<and> h2 (u b1 b2) = b2"
  11.264 +   using u b1 b2 unfolding inj2_def by fastforce
  11.265 +  }
  11.266 +  hence h1[simp]: "\<And> b1 b2. \<lbrakk>b1 \<in> B1; b2 \<in> B2\<rbrakk> \<Longrightarrow> h1 (u b1 b2) = b1" and
  11.267 +        h2[simp]: "\<And> b1 b2. \<lbrakk>b1 \<in> B1; b2 \<in> B2\<rbrakk> \<Longrightarrow> h2 (u b1 b2) = b2" by auto
  11.268 +  def M \<equiv> "\<lambda> a. ct (f1 (h1 a)) (f2 (h2 a))"
  11.269 +  show ?thesis
  11.270 +  apply(rule exI[of _ M]) proof safe
  11.271 +    fix b1 assume b1: "b1 \<in> B1"
  11.272 +    hence f1b1: "f1 b1 \<le> n1" using f1 unfolding bij_betw_def
  11.273 +    by (metis image_eqI lessThan_iff less_Suc_eq_le)
  11.274 +    have "(\<Sum>b2\<in>B2. M (u b1 b2)) = (\<Sum>i2<Suc n2. ct (f1 b1) (f2 (e2 i2)))"
  11.275 +    unfolding e2_surj[symmetric] setsum_reindex[OF e2_inj]
  11.276 +    unfolding M_def comp_def apply(intro setsum_cong) apply force
  11.277 +    by (metis e2_surj b1 h1 h2 imageI)
  11.278 +    also have "... = N1 b1" using b1 ct1[OF f1b1] by simp
  11.279 +    finally show "(\<Sum>b2\<in>B2. M (u b1 b2)) = N1 b1" .
  11.280 +  next
  11.281 +    fix b2 assume b2: "b2 \<in> B2"
  11.282 +    hence f2b2: "f2 b2 \<le> n2" using f2 unfolding bij_betw_def
  11.283 +    by (metis image_eqI lessThan_iff less_Suc_eq_le)
  11.284 +    have "(\<Sum>b1\<in>B1. M (u b1 b2)) = (\<Sum>i1<Suc n1. ct (f1 (e1 i1)) (f2 b2))"
  11.285 +    unfolding e1_surj[symmetric] setsum_reindex[OF e1_inj]
  11.286 +    unfolding M_def comp_def apply(intro setsum_cong) apply force
  11.287 +    by (metis e1_surj b2 h1 h2 imageI)
  11.288 +    also have "... = N2 b2" using b2 ct2[OF f2b2] by simp
  11.289 +    finally show "(\<Sum>b1\<in>B1. M (u b1 b2)) = N2 b2" .
  11.290 +  qed
  11.291 +qed
  11.292 +
  11.293 +lemma supp_vimage_mmap: "set_of M \<subseteq> f -` (set_of (mmap f M))"
  11.294 +  by transfer (auto simp: multiset_def setsum_gt_0_iff)
  11.295 +
  11.296 +lemma mmap_ge_0: "b \<in># mmap f M \<longleftrightarrow> (\<exists>a. a \<in># M \<and> f a = b)"
  11.297 +  by transfer (auto simp: multiset_def setsum_gt_0_iff)
  11.298 +
  11.299 +lemma finite_twosets:
  11.300 +assumes "finite B1" and "finite B2"
  11.301 +shows "finite {u b1 b2 |b1 b2. b1 \<in> B1 \<and> b2 \<in> B2}"  (is "finite ?A")
  11.302 +proof-
  11.303 +  have A: "?A = (\<lambda> b1b2. u (fst b1b2) (snd b1b2)) ` (B1 <*> B2)" by force
  11.304 +  show ?thesis unfolding A using finite_cartesian_product[OF assms] by auto
  11.305 +qed
  11.306 +
  11.307 +(* Weak pullbacks: *)
  11.308 +definition wpull where
  11.309 +"wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow>
  11.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))"
  11.311 +
  11.312 +(* Weak pseudo-pullbacks *)
  11.313 +definition wppull where
  11.314 +"wppull A B1 B2 f1 f2 e1 e2 p1 p2 \<longleftrightarrow>
  11.315 + (\<forall> b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<longrightarrow>
  11.316 +           (\<exists> a \<in> A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2))"
  11.317 +
  11.318 +
  11.319 +(* The pullback of sets *)
  11.320 +definition thePull where
  11.321 +"thePull B1 B2 f1 f2 = {(b1,b2). b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2}"
  11.322 +
  11.323 +lemma wpull_thePull:
  11.324 +"wpull (thePull B1 B2 f1 f2) B1 B2 f1 f2 fst snd"
  11.325 +unfolding wpull_def thePull_def by auto
  11.326 +
  11.327 +lemma wppull_thePull:
  11.328 +assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
  11.329 +shows
  11.330 +"\<exists> j. \<forall> a' \<in> thePull B1 B2 f1 f2.
  11.331 +   j a' \<in> A \<and>
  11.332 +   e1 (p1 (j a')) = e1 (fst a') \<and> e2 (p2 (j a')) = e2 (snd a')"
  11.333 +(is "\<exists> j. \<forall> a' \<in> ?A'. ?phi a' (j a')")
  11.334 +proof(rule bchoice[of ?A' ?phi], default)
  11.335 +  fix a' assume a': "a' \<in> ?A'"
  11.336 +  hence "fst a' \<in> B1" unfolding thePull_def by auto
  11.337 +  moreover
  11.338 +  from a' have "snd a' \<in> B2" unfolding thePull_def by auto
  11.339 +  moreover have "f1 (fst a') = f2 (snd a')"
  11.340 +  using a' unfolding csquare_def thePull_def by auto
  11.341 +  ultimately show "\<exists> ja'. ?phi a' ja'"
  11.342 +  using assms unfolding wppull_def by blast
  11.343 +qed
  11.344 +
  11.345 +lemma wpull_wppull:
  11.346 +assumes wp: "wpull A' B1 B2 f1 f2 p1' p2'" and
  11.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')"
  11.348 +shows "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
  11.349 +unfolding wppull_def proof safe
  11.350 +  fix b1 b2
  11.351 +  assume b1: "b1 \<in> B1" and b2: "b2 \<in> B2" and f: "f1 b1 = f2 b2"
  11.352 +  then obtain a' where a': "a' \<in> A'" and b1: "b1 = p1' a'" and b2: "b2 = p2' a'"
  11.353 +  using wp unfolding wpull_def by blast
  11.354 +  show "\<exists>a\<in>A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2"
  11.355 +  apply (rule bexI[of _ "j a'"]) unfolding b1 b2 using a' 1 by auto
  11.356 +qed
  11.357 +
  11.358 +lemma wppull_fstOp_sndOp:
  11.359 +shows "wppull (Collect (split (P OO Q))) (Collect (split P)) (Collect (split Q))
  11.360 +  snd fst fst snd (BNF_Def.fstOp P Q) (BNF_Def.sndOp P Q)"
  11.361 +using pick_middlep unfolding wppull_def fstOp_def sndOp_def relcompp.simps by auto
  11.362 +
  11.363 +lemma wpull_mmap:
  11.364 +fixes A :: "'a set" and B1 :: "'b1 set" and B2 :: "'b2 set"
  11.365 +assumes wp: "wpull A B1 B2 f1 f2 p1 p2"
  11.366 +shows
  11.367 +"wpull {M. set_of M \<subseteq> A}
  11.368 +       {N1. set_of N1 \<subseteq> B1} {N2. set_of N2 \<subseteq> B2}
  11.369 +       (mmap f1) (mmap f2) (mmap p1) (mmap p2)"
  11.370 +unfolding wpull_def proof (safe, unfold Bex_def mem_Collect_eq)
  11.371 +  fix N1 :: "'b1 multiset" and N2 :: "'b2 multiset"
  11.372 +  assume mmap': "mmap f1 N1 = mmap f2 N2"
  11.373 +  and N1[simp]: "set_of N1 \<subseteq> B1"
  11.374 +  and N2[simp]: "set_of N2 \<subseteq> B2"
  11.375 +  def P \<equiv> "mmap f1 N1"
  11.376 +  have P1: "P = mmap f1 N1" and P2: "P = mmap f2 N2" unfolding P_def using mmap' by auto
  11.377 +  note P = P1 P2
  11.378 +  have fin_N1[simp]: "finite (set_of N1)"
  11.379 +   and fin_N2[simp]: "finite (set_of N2)"
  11.380 +   and fin_P[simp]: "finite (set_of P)" by auto
  11.381 +
  11.382 +  def set1 \<equiv> "\<lambda> c. {b1 \<in> set_of N1. f1 b1 = c}"
  11.383 +  have set1[simp]: "\<And> c b1. b1 \<in> set1 c \<Longrightarrow> f1 b1 = c" unfolding set1_def by auto
  11.384 +  have fin_set1: "\<And> c. c \<in> set_of P \<Longrightarrow> finite (set1 c)"
  11.385 +    using N1(1) unfolding set1_def multiset_def by auto
  11.386 +  have set1_NE: "\<And> c. c \<in> set_of P \<Longrightarrow> set1 c \<noteq> {}"
  11.387 +   unfolding set1_def set_of_def P mmap_ge_0 by auto
  11.388 +  have supp_N1_set1: "set_of N1 = (\<Union> c \<in> set_of P. set1 c)"
  11.389 +    using supp_vimage_mmap[of N1 f1] unfolding set1_def P1 by auto
  11.390 +  hence set1_inclN1: "\<And>c. c \<in> set_of P \<Longrightarrow> set1 c \<subseteq> set_of N1" by auto
  11.391 +  hence set1_incl: "\<And> c. c \<in> set_of P \<Longrightarrow> set1 c \<subseteq> B1" using N1 by blast
  11.392 +  have set1_disj: "\<And> c c'. c \<noteq> c' \<Longrightarrow> set1 c \<inter> set1 c' = {}"
  11.393 +    unfolding set1_def by auto
  11.394 +  have setsum_set1: "\<And> c. setsum (count N1) (set1 c) = count P c"
  11.395 +    unfolding P1 set1_def by transfer (auto intro: setsum_cong)
  11.396 +
  11.397 +  def set2 \<equiv> "\<lambda> c. {b2 \<in> set_of N2. f2 b2 = c}"
  11.398 +  have set2[simp]: "\<And> c b2. b2 \<in> set2 c \<Longrightarrow> f2 b2 = c" unfolding set2_def by auto
  11.399 +  have fin_set2: "\<And> c. c \<in> set_of P \<Longrightarrow> finite (set2 c)"
  11.400 +  using N2(1) unfolding set2_def multiset_def by auto
  11.401 +  have set2_NE: "\<And> c. c \<in> set_of P \<Longrightarrow> set2 c \<noteq> {}"
  11.402 +    unfolding set2_def P2 mmap_ge_0 set_of_def by auto
  11.403 +  have supp_N2_set2: "set_of N2 = (\<Union> c \<in> set_of P. set2 c)"
  11.404 +    using supp_vimage_mmap[of N2 f2] unfolding set2_def P2 by auto
  11.405 +  hence set2_inclN2: "\<And>c. c \<in> set_of P \<Longrightarrow> set2 c \<subseteq> set_of N2" by auto
  11.406 +  hence set2_incl: "\<And> c. c \<in> set_of P \<Longrightarrow> set2 c \<subseteq> B2" using N2 by blast
  11.407 +  have set2_disj: "\<And> c c'. c \<noteq> c' \<Longrightarrow> set2 c \<inter> set2 c' = {}"
  11.408 +    unfolding set2_def by auto
  11.409 +  have setsum_set2: "\<And> c. setsum (count N2) (set2 c) = count P c"
  11.410 +    unfolding P2 set2_def by transfer (auto intro: setsum_cong)
  11.411 +
  11.412 +  have ss: "\<And> c. c \<in> set_of P \<Longrightarrow> setsum (count N1) (set1 c) = setsum (count N2) (set2 c)"
  11.413 +    unfolding setsum_set1 setsum_set2 ..
  11.414 +  have "\<forall> c \<in> set_of P. \<forall> b1b2 \<in> (set1 c) \<times> (set2 c).
  11.415 +          \<exists> a \<in> A. p1 a = fst b1b2 \<and> p2 a = snd b1b2"
  11.416 +    using wp set1_incl set2_incl unfolding wpull_def Ball_def mem_Collect_eq
  11.417 +    by simp (metis set1 set2 set_rev_mp)
  11.418 +  then obtain uu where uu:
  11.419 +  "\<forall> c \<in> set_of P. \<forall> b1b2 \<in> (set1 c) \<times> (set2 c).
  11.420 +     uu c b1b2 \<in> A \<and> p1 (uu c b1b2) = fst b1b2 \<and> p2 (uu c b1b2) = snd b1b2" by metis
  11.421 +  def u \<equiv> "\<lambda> c b1 b2. uu c (b1,b2)"
  11.422 +  have u[simp]:
  11.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"
  11.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"
  11.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"
  11.426 +    using uu unfolding u_def by auto
  11.427 +  {fix c assume c: "c \<in> set_of P"
  11.428 +   have "inj2 (u c) (set1 c) (set2 c)" unfolding inj2_def proof clarify
  11.429 +     fix b1 b1' b2 b2'
  11.430 +     assume "{b1, b1'} \<subseteq> set1 c" "{b2, b2'} \<subseteq> set2 c" and 0: "u c b1 b2 = u c b1' b2'"
  11.431 +     hence "p1 (u c b1 b2) = b1 \<and> p2 (u c b1 b2) = b2 \<and>
  11.432 +            p1 (u c b1' b2') = b1' \<and> p2 (u c b1' b2') = b2'"
  11.433 +     using u(2)[OF c] u(3)[OF c] by simp metis
  11.434 +     thus "b1 = b1' \<and> b2 = b2'" using 0 by auto
  11.435 +   qed
  11.436 +  } note inj = this
  11.437 +  def sset \<equiv> "\<lambda> c. {u c b1 b2 | b1 b2. b1 \<in> set1 c \<and> b2 \<in> set2 c}"
  11.438 +  have fin_sset[simp]: "\<And> c. c \<in> set_of P \<Longrightarrow> finite (sset c)" unfolding sset_def
  11.439 +    using fin_set1 fin_set2 finite_twosets by blast
  11.440 +  have sset_A: "\<And> c. c \<in> set_of P \<Longrightarrow> sset c \<subseteq> A" unfolding sset_def by auto
  11.441 +  {fix c a assume c: "c \<in> set_of P" and ac: "a \<in> sset c"
  11.442 +   then obtain b1 b2 where b1: "b1 \<in> set1 c" and b2: "b2 \<in> set2 c"
  11.443 +   and a: "a = u c b1 b2" unfolding sset_def by auto
  11.444 +   have "p1 a \<in> set1 c" and p2a: "p2 a \<in> set2 c"
  11.445 +   using ac a b1 b2 c u(2) u(3) by simp+
  11.446 +   hence "u c (p1 a) (p2 a) = a" unfolding a using b1 b2 inj[OF c]
  11.447 +   unfolding inj2_def by (metis c u(2) u(3))
  11.448 +  } note u_p12[simp] = this
  11.449 +  {fix c a assume c: "c \<in> set_of P" and ac: "a \<in> sset c"
  11.450 +   hence "p1 a \<in> set1 c" unfolding sset_def by auto
  11.451 +  }note p1[simp] = this
  11.452 +  {fix c a assume c: "c \<in> set_of P" and ac: "a \<in> sset c"
  11.453 +   hence "p2 a \<in> set2 c" unfolding sset_def by auto
  11.454 +  }note p2[simp] = this
  11.455 +
  11.456 +  {fix c assume c: "c \<in> set_of P"
  11.457 +   hence "\<exists> M. (\<forall> b1 \<in> set1 c. setsum (\<lambda> b2. M (u c b1 b2)) (set2 c) = count N1 b1) \<and>
  11.458 +               (\<forall> b2 \<in> set2 c. setsum (\<lambda> b1. M (u c b1 b2)) (set1 c) = count N2 b2)"
  11.459 +   unfolding sset_def
  11.460 +   using matrix_setsum_finite[OF set1_NE[OF c] fin_set1[OF c]
  11.461 +                                 set2_NE[OF c] fin_set2[OF c] inj[OF c] ss[OF c]] by auto
  11.462 +  }
  11.463 +  then obtain Ms where
  11.464 +  ss1: "\<And> c b1. \<lbrakk>c \<in> set_of P; b1 \<in> set1 c\<rbrakk> \<Longrightarrow>
  11.465 +                   setsum (\<lambda> b2. Ms c (u c b1 b2)) (set2 c) = count N1 b1" and
  11.466 +  ss2: "\<And> c b2. \<lbrakk>c \<in> set_of P; b2 \<in> set2 c\<rbrakk> \<Longrightarrow>
  11.467 +                   setsum (\<lambda> b1. Ms c (u c b1 b2)) (set1 c) = count N2 b2"
  11.468 +  by metis
  11.469 +  def SET \<equiv> "\<Union> c \<in> set_of P. sset c"
  11.470 +  have fin_SET[simp]: "finite SET" unfolding SET_def apply(rule finite_UN_I) by auto
  11.471 +  have SET_A: "SET \<subseteq> A" unfolding SET_def using sset_A by blast
  11.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"
  11.473 +    unfolding SET_def sset_def by blast
  11.474 +  {fix c a assume c: "c \<in> set_of P" and a: "a \<in> SET" and p1a: "p1 a \<in> set1 c"
  11.475 +   then obtain c' where c': "c' \<in> set_of P" and ac': "a \<in> sset c'"
  11.476 +    unfolding SET_def by auto
  11.477 +   hence "p1 a \<in> set1 c'" unfolding sset_def by auto
  11.478 +   hence eq: "c = c'" using p1a c c' set1_disj by auto
  11.479 +   hence "a \<in> sset c" using ac' by simp
  11.480 +  } note p1_rev = this
  11.481 +  {fix c a assume c: "c \<in> set_of P" and a: "a \<in> SET" and p2a: "p2 a \<in> set2 c"
  11.482 +   then obtain c' where c': "c' \<in> set_of P" and ac': "a \<in> sset c'"
  11.483 +   unfolding SET_def by auto
  11.484 +   hence "p2 a \<in> set2 c'" unfolding sset_def by auto
  11.485 +   hence eq: "c = c'" using p2a c c' set2_disj by auto
  11.486 +   hence "a \<in> sset c" using ac' by simp
  11.487 +  } note p2_rev = this
  11.488 +
  11.489 +  have "\<forall> a \<in> SET. \<exists> c \<in> set_of P. a \<in> sset c" unfolding SET_def by auto
  11.490 +  then obtain h where h: "\<forall> a \<in> SET. h a \<in> set_of P \<and> a \<in> sset (h a)" by metis
  11.491 +  have h_u[simp]: "\<And> c b1 b2. \<lbrakk>c \<in> set_of P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk>
  11.492 +                      \<Longrightarrow> h (u c b1 b2) = c"
  11.493 +  by (metis h p2 set2 u(3) u_SET)
  11.494 +  have h_u1: "\<And> c b1 b2. \<lbrakk>c \<in> set_of P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk>
  11.495 +                      \<Longrightarrow> h (u c b1 b2) = f1 b1"
  11.496 +  using h unfolding sset_def by auto
  11.497 +  have h_u2: "\<And> c b1 b2. \<lbrakk>c \<in> set_of P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk>
  11.498 +                      \<Longrightarrow> h (u c b1 b2) = f2 b2"
  11.499 +  using h unfolding sset_def by auto
  11.500 +  def M \<equiv>
  11.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)"
  11.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"
  11.503 +    unfolding multiset_def by auto
  11.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"
  11.505 +    unfolding M_def pcr_multiset_def cr_multiset_def by (auto simp: Abs_multiset_inverse)
  11.506 +  have sM: "set_of M \<subseteq> SET" "set_of M \<subseteq> p1 -` (set_of N1)" "set_of M \<subseteq> p2 -` set_of N2"
  11.507 +    by (transfer, auto split: split_if_asm)+
  11.508 +  show "\<exists>M. set_of M \<subseteq> A \<and> mmap p1 M = N1 \<and> mmap p2 M = N2"
  11.509 +  proof(rule exI[of _ M], safe)
  11.510 +    fix a assume *: "a \<in> set_of M"
  11.511 +    from SET_A show "a \<in> A"
  11.512 +    proof (cases "a \<in> SET")
  11.513 +      case False thus ?thesis using * by transfer' auto
  11.514 +    qed blast
  11.515 +  next
  11.516 +    show "mmap p1 M = N1"
  11.517 +    proof(intro multiset_eqI)
  11.518 +      fix b1
  11.519 +      let ?K = "{a. p1 a = b1 \<and> a \<in># M}"
  11.520 +      have "setsum (count M) ?K = count N1 b1"
  11.521 +      proof(cases "b1 \<in> set_of N1")
  11.522 +        case False
  11.523 +        hence "?K = {}" using sM(2) by auto
  11.524 +        thus ?thesis using False by auto
  11.525 +      next
  11.526 +        case True
  11.527 +        def c \<equiv> "f1 b1"
  11.528 +        have c: "c \<in> set_of P" and b1: "b1 \<in> set1 c"
  11.529 +          unfolding set1_def c_def P1 using True by (auto simp: comp_eq_dest[OF set_of_mmap])
  11.530 +        with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p1 a = b1 \<and> a \<in> SET}"
  11.531 +          by transfer (force intro: setsum_mono_zero_cong_left split: split_if_asm)
  11.532 +        also have "... = setsum (count M) ((\<lambda> b2. u c b1 b2) ` (set2 c))"
  11.533 +          apply(rule setsum_cong) using c b1 proof safe
  11.534 +          fix a assume p1a: "p1 a \<in> set1 c" and "c \<in> set_of P" and "a \<in> SET"
  11.535 +          hence ac: "a \<in> sset c" using p1_rev by auto
  11.536 +          hence "a = u c (p1 a) (p2 a)" using c by auto
  11.537 +          moreover have "p2 a \<in> set2 c" using ac c by auto
  11.538 +          ultimately show "a \<in> u c (p1 a) ` set2 c" by auto
  11.539 +        qed auto
  11.540 +        also have "... = setsum (\<lambda> b2. count M (u c b1 b2)) (set2 c)"
  11.541 +          unfolding comp_def[symmetric] apply(rule setsum_reindex)
  11.542 +          using inj unfolding inj_on_def inj2_def using b1 c u(3) by blast
  11.543 +        also have "... = count N1 b1" unfolding ss1[OF c b1, symmetric]
  11.544 +          apply(rule setsum_cong[OF refl]) apply (transfer fixing: Ms u c b1 set2)
  11.545 +          using True h_u[OF c b1] set2_def u(2,3)[OF c b1] u_SET[OF c b1] by fastforce
  11.546 +        finally show ?thesis .
  11.547 +      qed
  11.548 +      thus "count (mmap p1 M) b1 = count N1 b1" by transfer
  11.549 +    qed
  11.550 +  next
  11.551 +    show "mmap p2 M = N2"
  11.552 +    proof(intro multiset_eqI)
  11.553 +      fix b2
  11.554 +      let ?K = "{a. p2 a = b2 \<and> a \<in># M}"
  11.555 +      have "setsum (count M) ?K = count N2 b2"
  11.556 +      proof(cases "b2 \<in> set_of N2")
  11.557 +        case False
  11.558 +        hence "?K = {}" using sM(3) by auto
  11.559 +        thus ?thesis using False by auto
  11.560 +      next
  11.561 +        case True
  11.562 +        def c \<equiv> "f2 b2"
  11.563 +        have c: "c \<in> set_of P" and b2: "b2 \<in> set2 c"
  11.564 +          unfolding set2_def c_def P2 using True by (auto simp: comp_eq_dest[OF set_of_mmap])
  11.565 +        with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p2 a = b2 \<and> a \<in> SET}"
  11.566 +          by transfer (force intro: setsum_mono_zero_cong_left split: split_if_asm)
  11.567 +        also have "... = setsum (count M) ((\<lambda> b1. u c b1 b2) ` (set1 c))"
  11.568 +          apply(rule setsum_cong) using c b2 proof safe
  11.569 +          fix a assume p2a: "p2 a \<in> set2 c" and "c \<in> set_of P" and "a \<in> SET"
  11.570 +          hence ac: "a \<in> sset c" using p2_rev by auto
  11.571 +          hence "a = u c (p1 a) (p2 a)" using c by auto
  11.572 +          moreover have "p1 a \<in> set1 c" using ac c by auto
  11.573 +          ultimately show "a \<in> (\<lambda>x. u c x (p2 a)) ` set1 c" by auto
  11.574 +        qed auto
  11.575 +        also have "... = setsum (count M o (\<lambda> b1. u c b1 b2)) (set1 c)"
  11.576 +          apply(rule setsum_reindex)
  11.577 +          using inj unfolding inj_on_def inj2_def using b2 c u(2) by blast
  11.578 +        also have "... = setsum (\<lambda> b1. count M (u c b1 b2)) (set1 c)" by simp
  11.579 +        also have "... = count N2 b2" unfolding ss2[OF c b2, symmetric] comp_def
  11.580 +          apply(rule setsum_cong[OF refl]) apply (transfer fixing: Ms u c b2 set1)
  11.581 +          using True h_u1[OF c _ b2] u(2,3)[OF c _ b2] u_SET[OF c _ b2] set1_def by fastforce
  11.582 +        finally show ?thesis .
  11.583 +      qed
  11.584 +      thus "count (mmap p2 M) b2 = count N2 b2" by transfer
  11.585 +    qed
  11.586 +  qed
  11.587 +qed
  11.588 +
  11.589 +lemma set_of_bd: "(card_of (set_of x), natLeq) \<in> ordLeq"
  11.590 +  by transfer
  11.591 +    (auto intro!: ordLess_imp_ordLeq simp: finite_iff_ordLess_natLeq[symmetric] multiset_def)
  11.592 +
  11.593 +lemma wppull_mmap:
  11.594 +  assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
  11.595 +  shows "wppull {M. set_of M \<subseteq> A} {N1. set_of N1 \<subseteq> B1} {N2. set_of N2 \<subseteq> B2}
  11.596 +    (mmap f1) (mmap f2) (mmap e1) (mmap e2) (mmap p1) (mmap p2)"
  11.597 +proof -
  11.598 +  from assms obtain j where j: "\<forall>a'\<in>thePull B1 B2 f1 f2.
  11.599 +    j a' \<in> A \<and> e1 (p1 (j a')) = e1 (fst a') \<and> e2 (p2 (j a')) = e2 (snd a')" 
  11.600 +    by (blast dest: wppull_thePull)
  11.601 +  then show ?thesis
  11.602 +    by (intro wpull_wppull[OF wpull_mmap[OF wpull_thePull], of _ _ _ _ "mmap j"])
  11.603 +      (auto simp: comp_eq_dest_lhs[OF mmap_comp[symmetric]] comp_eq_dest[OF set_of_mmap]
  11.604 +        intro!: mmap_cong simp del: mem_set_of_iff simp: mem_set_of_iff[symmetric])
  11.605 +qed
  11.606 +
  11.607 +bnf "'a multiset"
  11.608 +  map: mmap
  11.609 +  sets: set_of 
  11.610 +  bd: natLeq
  11.611 +  wits: "{#}"
  11.612 +by (auto simp add: mmap_id0 mmap_comp set_of_mmap natLeq_card_order natLeq_cinfinite set_of_bd
  11.613 +  Grp_def relcompp.simps intro: mmap_cong)
  11.614 +  (metis wppull_mmap[OF wppull_fstOp_sndOp, unfolded wppull_def
  11.615 +    o_eq_dest_lhs[OF mmap_comp[symmetric]] fstOp_def sndOp_def comp_def, simplified])
  11.616 +
  11.617 +inductive rel_multiset' where
  11.618 +  Zero[intro]: "rel_multiset' R {#} {#}"
  11.619 +| Plus[intro]: "\<lbrakk>R a b; rel_multiset' R M N\<rbrakk> \<Longrightarrow> rel_multiset' R (M + {#a#}) (N + {#b#})"
  11.620 +
  11.621 +lemma map_multiset_Zero_iff[simp]: "mmap f M = {#} \<longleftrightarrow> M = {#}"
  11.622 +by (metis image_is_empty multiset.set_map set_of_eq_empty_iff)
  11.623 +
  11.624 +lemma map_multiset_Zero[simp]: "mmap f {#} = {#}" by simp
  11.625 +
  11.626 +lemma rel_multiset_Zero: "rel_multiset R {#} {#}"
  11.627 +unfolding rel_multiset_def Grp_def by auto
  11.628 +
  11.629 +declare multiset.count[simp]
  11.630 +declare Abs_multiset_inverse[simp]
  11.631 +declare multiset.count_inverse[simp]
  11.632 +declare union_preserves_multiset[simp]
  11.633 +
  11.634 +lemma map_multiset_Plus[simp]: "mmap f (M1 + M2) = mmap f M1 + mmap f M2"
  11.635 +proof (intro multiset_eqI, transfer fixing: f)
  11.636 +  fix x :: 'a and M1 M2 :: "'b \<Rightarrow> nat"
  11.637 +  assume "M1 \<in> multiset" "M2 \<in> multiset"
  11.638 +  hence "setsum M1 {a. f a = x \<and> 0 < M1 a} = setsum M1 {a. f a = x \<and> 0 < M1 a + M2 a}"
  11.639 +        "setsum M2 {a. f a = x \<and> 0 < M2 a} = setsum M2 {a. f a = x \<and> 0 < M1 a + M2 a}"
  11.640 +    by (auto simp: multiset_def intro!: setsum_mono_zero_cong_left)
  11.641 +  then show "(\<Sum>a | f a = x \<and> 0 < M1 a + M2 a. M1 a + M2 a) =
  11.642 +       setsum M1 {a. f a = x \<and> 0 < M1 a} +
  11.643 +       setsum M2 {a. f a = x \<and> 0 < M2 a}"
  11.644 +    by (auto simp: setsum.distrib[symmetric])
  11.645 +qed
  11.646 +
  11.647 +lemma map_multiset_single[simp]: "mmap f {#a#} = {#f a#}"
  11.648 +  by transfer auto
  11.649 +
  11.650 +lemma rel_multiset_Plus:
  11.651 +assumes ab: "R a b" and MN: "rel_multiset R M N"
  11.652 +shows "rel_multiset R (M + {#a#}) (N + {#b#})"
  11.653 +proof-
  11.654 +  {fix y assume "R a b" and "set_of y \<subseteq> {(x, y). R x y}"
  11.655 +   hence "\<exists>ya. mmap fst y + {#a#} = mmap fst ya \<and>
  11.656 +               mmap snd y + {#b#} = mmap snd ya \<and>
  11.657 +               set_of ya \<subseteq> {(x, y). R x y}"
  11.658 +   apply(intro exI[of _ "y + {#(a,b)#}"]) by auto
  11.659 +  }
  11.660 +  thus ?thesis
  11.661 +  using assms
  11.662 +  unfolding rel_multiset_def Grp_def by force
  11.663 +qed
  11.664 +
  11.665 +lemma rel_multiset'_imp_rel_multiset:
  11.666 +"rel_multiset' R M N \<Longrightarrow> rel_multiset R M N"
  11.667 +apply(induct rule: rel_multiset'.induct)
  11.668 +using rel_multiset_Zero rel_multiset_Plus by auto
  11.669 +
  11.670 +lemma mcard_mmap[simp]: "mcard (mmap f M) = mcard M"
  11.671 +proof -
  11.672 +  def A \<equiv> "\<lambda> b. {a. f a = b \<and> a \<in># M}"
  11.673 +  let ?B = "{b. 0 < setsum (count M) (A b)}"
  11.674 +  have "{b. \<exists>a. f a = b \<and> a \<in># M} \<subseteq> f ` {a. a \<in># M}" by auto
  11.675 +  moreover have "finite (f ` {a. a \<in># M})" apply(rule finite_imageI)
  11.676 +  using finite_Collect_mem .
  11.677 +  ultimately have fin: "finite {b. \<exists>a. f a = b \<and> a \<in># M}" by(rule finite_subset)
  11.678 +  have i: "inj_on A ?B" unfolding inj_on_def A_def apply clarsimp
  11.679 +    by (metis (lifting, full_types) mem_Collect_eq neq0_conv setsum.neutral)
  11.680 +  have 0: "\<And> b. 0 < setsum (count M) (A b) \<longleftrightarrow> (\<exists> a \<in> A b. count M a > 0)"
  11.681 +  apply safe
  11.682 +    apply (metis less_not_refl setsum_gt_0_iff setsum_infinite)
  11.683 +    by (metis A_def finite_Collect_conjI finite_Collect_mem setsum_gt_0_iff)
  11.684 +  hence AB: "A ` ?B = {A b | b. \<exists> a \<in> A b. count M a > 0}" by auto
  11.685 +
  11.686 +  have "setsum (\<lambda> x. setsum (count M) (A x)) ?B = setsum (setsum (count M) o A) ?B"
  11.687 +  unfolding comp_def ..
  11.688 +  also have "... = (\<Sum>x\<in> A ` ?B. setsum (count M) x)"
  11.689 +  unfolding setsum.reindex [OF i, symmetric] ..
  11.690 +  also have "... = setsum (count M) (\<Union>x\<in>A ` {b. 0 < setsum (count M) (A b)}. x)"
  11.691 +  (is "_ = setsum (count M) ?J")
  11.692 +  apply(rule setsum.UNION_disjoint[symmetric])
  11.693 +  using 0 fin unfolding A_def by auto
  11.694 +  also have "?J = {a. a \<in># M}" unfolding AB unfolding A_def by auto
  11.695 +  finally have "setsum (\<lambda> x. setsum (count M) (A x)) ?B =
  11.696 +                setsum (count M) {a. a \<in># M}" .
  11.697 +  then show ?thesis unfolding mcard_unfold_setsum A_def by transfer
  11.698 +qed
  11.699 +
  11.700 +lemma rel_multiset_mcard:
  11.701 +assumes "rel_multiset R M N"
  11.702 +shows "mcard M = mcard N"
  11.703 +using assms unfolding rel_multiset_def Grp_def by auto
  11.704 +
  11.705 +lemma multiset_induct2[case_names empty addL addR]:
  11.706 +assumes empty: "P {#} {#}"
  11.707 +and addL: "\<And>M N a. P M N \<Longrightarrow> P (M + {#a#}) N"
  11.708 +and addR: "\<And>M N a. P M N \<Longrightarrow> P M (N + {#a#})"
  11.709 +shows "P M N"
  11.710 +apply(induct N rule: multiset_induct)
  11.711 +  apply(induct M rule: multiset_induct, rule empty, erule addL)
  11.712 +  apply(induct M rule: multiset_induct, erule addR, erule addR)
  11.713 +done
  11.714 +
  11.715 +lemma multiset_induct2_mcard[consumes 1, case_names empty add]:
  11.716 +assumes c: "mcard M = mcard N"
  11.717 +and empty: "P {#} {#}"
  11.718 +and add: "\<And>M N a b. P M N \<Longrightarrow> P (M + {#a#}) (N + {#b#})"
  11.719 +shows "P M N"
  11.720 +using c proof(induct M arbitrary: N rule: measure_induct_rule[of mcard])
  11.721 +  case (less M)  show ?case
  11.722 +  proof(cases "M = {#}")
  11.723 +    case True hence "N = {#}" using less.prems by auto
  11.724 +    thus ?thesis using True empty by auto
  11.725 +  next
  11.726 +    case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split)
  11.727 +    have "N \<noteq> {#}" using False less.prems by auto
  11.728 +    then obtain N1 b where N: "N = N1 + {#b#}" by (metis multi_nonempty_split)
  11.729 +    have "mcard M1 = mcard N1" using less.prems unfolding M N by auto
  11.730 +    thus ?thesis using M N less.hyps add by auto
  11.731 +  qed
  11.732 +qed
  11.733 +
  11.734 +lemma msed_map_invL:
  11.735 +assumes "mmap f (M + {#a#}) = N"
  11.736 +shows "\<exists> N1. N = N1 + {#f a#} \<and> mmap f M = N1"
  11.737 +proof-
  11.738 +  have "f a \<in># N"
  11.739 +  using assms multiset.set_map[of f "M + {#a#}"] by auto
  11.740 +  then obtain N1 where N: "N = N1 + {#f a#}" using multi_member_split by metis
  11.741 +  have "mmap f M = N1" using assms unfolding N by simp
  11.742 +  thus ?thesis using N by blast
  11.743 +qed
  11.744 +
  11.745 +lemma msed_map_invR:
  11.746 +assumes "mmap f M = N + {#b#}"
  11.747 +shows "\<exists> M1 a. M = M1 + {#a#} \<and> f a = b \<and> mmap f M1 = N"
  11.748 +proof-
  11.749 +  obtain a where a: "a \<in># M" and fa: "f a = b"
  11.750 +  using multiset.set_map[of f M] unfolding assms
  11.751 +  by (metis image_iff mem_set_of_iff union_single_eq_member)
  11.752 +  then obtain M1 where M: "M = M1 + {#a#}" using multi_member_split by metis
  11.753 +  have "mmap f M1 = N" using assms unfolding M fa[symmetric] by simp
  11.754 +  thus ?thesis using M fa by blast
  11.755 +qed
  11.756 +
  11.757 +lemma msed_rel_invL:
  11.758 +assumes "rel_multiset R (M + {#a#}) N"
  11.759 +shows "\<exists> N1 b. N = N1 + {#b#} \<and> R a b \<and> rel_multiset R M N1"
  11.760 +proof-
  11.761 +  obtain K where KM: "mmap fst K = M + {#a#}"
  11.762 +  and KN: "mmap snd K = N" and sK: "set_of K \<subseteq> {(a, b). R a b}"
  11.763 +  using assms
  11.764 +  unfolding rel_multiset_def Grp_def by auto
  11.765 +  obtain K1 ab where K: "K = K1 + {#ab#}" and a: "fst ab = a"
  11.766 +  and K1M: "mmap fst K1 = M" using msed_map_invR[OF KM] by auto
  11.767 +  obtain N1 where N: "N = N1 + {#snd ab#}" and K1N1: "mmap snd K1 = N1"
  11.768 +  using msed_map_invL[OF KN[unfolded K]] by auto
  11.769 +  have Rab: "R a (snd ab)" using sK a unfolding K by auto
  11.770 +  have "rel_multiset R M N1" using sK K1M K1N1
  11.771 +  unfolding K rel_multiset_def Grp_def by auto
  11.772 +  thus ?thesis using N Rab by auto
  11.773 +qed
  11.774 +
  11.775 +lemma msed_rel_invR:
  11.776 +assumes "rel_multiset R M (N + {#b#})"
  11.777 +shows "\<exists> M1 a. M = M1 + {#a#} \<and> R a b \<and> rel_multiset R M1 N"
  11.778 +proof-
  11.779 +  obtain K where KN: "mmap snd K = N + {#b#}"
  11.780 +  and KM: "mmap fst K = M" and sK: "set_of K \<subseteq> {(a, b). R a b}"
  11.781 +  using assms
  11.782 +  unfolding rel_multiset_def Grp_def by auto
  11.783 +  obtain K1 ab where K: "K = K1 + {#ab#}" and b: "snd ab = b"
  11.784 +  and K1N: "mmap snd K1 = N" using msed_map_invR[OF KN] by auto
  11.785 +  obtain M1 where M: "M = M1 + {#fst ab#}" and K1M1: "mmap fst K1 = M1"
  11.786 +  using msed_map_invL[OF KM[unfolded K]] by auto
  11.787 +  have Rab: "R (fst ab) b" using sK b unfolding K by auto
  11.788 +  have "rel_multiset R M1 N" using sK K1N K1M1
  11.789 +  unfolding K rel_multiset_def Grp_def by auto
  11.790 +  thus ?thesis using M Rab by auto
  11.791 +qed
  11.792 +
  11.793 +lemma rel_multiset_imp_rel_multiset':
  11.794 +assumes "rel_multiset R M N"
  11.795 +shows "rel_multiset' R M N"
  11.796 +using assms proof(induct M arbitrary: N rule: measure_induct_rule[of mcard])
  11.797 +  case (less M)
  11.798 +  have c: "mcard M = mcard N" using rel_multiset_mcard[OF less.prems] .
  11.799 +  show ?case
  11.800 +  proof(cases "M = {#}")
  11.801 +    case True hence "N = {#}" using c by simp
  11.802 +    thus ?thesis using True rel_multiset'.Zero by auto
  11.803 +  next
  11.804 +    case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split)
  11.805 +    obtain N1 b where N: "N = N1 + {#b#}" and R: "R a b" and ms: "rel_multiset R M1 N1"
  11.806 +    using msed_rel_invL[OF less.prems[unfolded M]] by auto
  11.807 +    have "rel_multiset' R M1 N1" using less.hyps[of M1 N1] ms unfolding M by simp
  11.808 +    thus ?thesis using rel_multiset'.Plus[of R a b, OF R] unfolding M N by simp
  11.809 +  qed
  11.810 +qed
  11.811 +
  11.812 +lemma rel_multiset_rel_multiset':
  11.813 +"rel_multiset R M N = rel_multiset' R M N"
  11.814 +using  rel_multiset_imp_rel_multiset' rel_multiset'_imp_rel_multiset by auto
  11.815 +
  11.816 +(* The main end product for rel_multiset: inductive characterization *)
  11.817 +theorems rel_multiset_induct[case_names empty add, induct pred: rel_multiset] =
  11.818 +         rel_multiset'.induct[unfolded rel_multiset_rel_multiset'[symmetric]]
  11.819 +
  11.820 +end
    12.1 --- a/src/HOL/Lifting_Option.thy	Fri Jan 24 15:21:00 2014 +0000
    12.2 +++ b/src/HOL/Lifting_Option.thy	Fri Jan 24 16:54:25 2014 +0000
    12.3 @@ -1,5 +1,6 @@
    12.4  (*  Title:      HOL/Lifting_Option.thy
    12.5      Author:     Brian Huffman and Ondrej Kuncar
    12.6 +    Author:     Andreas Lochbihler, Karlsruhe Institute of Technology
    12.7  *)
    12.8  
    12.9  header {* Setup for Lifting/Transfer for the option type *}
   12.10 @@ -114,4 +115,57 @@
   12.11  
   12.12  end
   12.13  
   12.14 +
   12.15 +subsubsection {* BNF setup *}
   12.16 +
   12.17 +lemma option_rec_conv_option_case: "option_rec = option_case"
   12.18 +by (simp add: fun_eq_iff split: option.split)
   12.19 +
   12.20 +bnf "'a option"
   12.21 +  map: Option.map
   12.22 +  sets: Option.set
   12.23 +  bd: natLeq
   12.24 +  wits: None
   12.25 +  rel: option_rel
   12.26 +proof -
   12.27 +  show "Option.map id = id" by (rule Option.map.id)
   12.28 +next
   12.29 +  fix f g
   12.30 +  show "Option.map (g \<circ> f) = Option.map g \<circ> Option.map f"
   12.31 +    by (auto simp add: fun_eq_iff Option.map_def split: option.split)
   12.32 +next
   12.33 +  fix f g x
   12.34 +  assume "\<And>z. z \<in> Option.set x \<Longrightarrow> f z = g z"
   12.35 +  thus "Option.map f x = Option.map g x"
   12.36 +    by (simp cong: Option.map_cong)
   12.37 +next
   12.38 +  fix f
   12.39 +  show "Option.set \<circ> Option.map f = op ` f \<circ> Option.set"
   12.40 +    by fastforce
   12.41 +next
   12.42 +  show "card_order natLeq" by (rule natLeq_card_order)
   12.43 +next
   12.44 +  show "cinfinite natLeq" by (rule natLeq_cinfinite)
   12.45 +next
   12.46 +  fix x
   12.47 +  show "|Option.set x| \<le>o natLeq"
   12.48 +    by (cases x) (simp_all add: ordLess_imp_ordLeq finite_iff_ordLess_natLeq[symmetric])
   12.49 +next
   12.50 +  fix R S
   12.51 +  show "option_rel R OO option_rel S \<le> option_rel (R OO S)"
   12.52 +    by (auto simp: option_rel_def split: option.splits)
   12.53 +next
   12.54 +  fix z
   12.55 +  assume "z \<in> Option.set None"
   12.56 +  thus False by simp
   12.57 +next
   12.58 +  fix R
   12.59 +  show "option_rel R =
   12.60 +        (Grp {x. Option.set x \<subseteq> Collect (split R)} (Option.map fst))\<inverse>\<inverse> OO
   12.61 +         Grp {x. Option.set x \<subseteq> Collect (split R)} (Option.map snd)"
   12.62 +  unfolding option_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff prod.cases
   12.63 +  by (auto simp: trans[OF eq_commute option_map_is_None] trans[OF eq_commute option_map_eq_Some]
   12.64 +           split: option.splits)
   12.65 +qed
   12.66 +
   12.67  end
    13.1 --- a/src/HOL/List.thy	Fri Jan 24 15:21:00 2014 +0000
    13.2 +++ b/src/HOL/List.thy	Fri Jan 24 16:54:25 2014 +0000
    13.3 @@ -5936,7 +5936,6 @@
    13.4  
    13.5  subsection {* Code generation *}
    13.6  
    13.7 -
    13.8  text{* Optional tail recursive version of @{const map}. Can avoid
    13.9  stack overflow in some target languages. *}
   13.10  
   13.11 @@ -6531,6 +6530,7 @@
   13.12    "wf (set xs) = acyclic (set xs)"
   13.13    by (simp add: wf_iff_acyclic_if_finite)
   13.14  
   13.15 +
   13.16  subsection {* Setup for Lifting/Transfer *}
   13.17  
   13.18  subsubsection {* Relator and predicator properties *}
   13.19 @@ -6879,4 +6879,46 @@
   13.20  
   13.21  end
   13.22  
   13.23 +
   13.24 +subsection {* BNF setup *}
   13.25 +
   13.26 +bnf "'a list"
   13.27 +  map: map
   13.28 +  sets: set
   13.29 +  bd: natLeq
   13.30 +  wits: Nil
   13.31 +  rel: list_all2
   13.32 +proof -
   13.33 +  show "map id = id" by (rule List.map.id)
   13.34 +next
   13.35 +  fix f g
   13.36 +  show "map (g o f) = map g o map f" by (rule List.map.comp[symmetric])
   13.37 +next
   13.38 +  fix x f g
   13.39 +  assume "\<And>z. z \<in> set x \<Longrightarrow> f z = g z"
   13.40 +  thus "map f x = map g x" by simp
   13.41 +next
   13.42 +  fix f
   13.43 +  show "set o map f = image f o set" by (rule ext, unfold comp_apply, rule set_map)
   13.44 +next
   13.45 +  show "card_order natLeq" by (rule natLeq_card_order)
   13.46 +next
   13.47 +  show "cinfinite natLeq" by (rule natLeq_cinfinite)
   13.48 +next
   13.49 +  fix x
   13.50 +  show "|set x| \<le>o natLeq"
   13.51 +    by (metis List.finite_set finite_iff_ordLess_natLeq ordLess_imp_ordLeq)
   13.52 +next
   13.53 +  fix R S
   13.54 +  show "list_all2 R OO list_all2 S \<le> list_all2 (R OO S)"
   13.55 +    by (metis list_all2_OO order_refl)
   13.56 +next
   13.57 +  fix R
   13.58 +  show "list_all2 R =
   13.59 +         (Grp {x. set x \<subseteq> {(x, y). R x y}} (map fst))\<inverse>\<inverse> OO
   13.60 +         Grp {x. set x \<subseteq> {(x, y). R x y}} (map snd)"
   13.61 +    unfolding list_all2_def[abs_def] Grp_def fun_eq_iff relcompp.simps conversep.simps
   13.62 +    by (force simp: zip_map_fst_snd)
   13.63 +qed simp
   13.64 +
   13.65  end
    14.1 --- a/src/HOL/Main.thy	Fri Jan 24 15:21:00 2014 +0000
    14.2 +++ b/src/HOL/Main.thy	Fri Jan 24 16:54:25 2014 +0000
    14.3 @@ -29,6 +29,7 @@
    14.4    convol ("<_ , _>")
    14.5  
    14.6  hide_const (open)
    14.7 +  czero cinfinite cfinite csum cone ctwo Csum cprod cexp
    14.8    image2 image2p vimage2p Gr Grp collect fsts snds setl setr
    14.9    convol pick_middlep fstOp sndOp csquare inver relImage relInvImage
   14.10    prefCl PrefCl Succ Shift shift proj
    15.1 --- a/src/HOL/Option.thy	Fri Jan 24 15:21:00 2014 +0000
    15.2 +++ b/src/HOL/Option.thy	Fri Jan 24 16:54:25 2014 +0000
    15.3 @@ -233,4 +233,3 @@
    15.4    Option None Some
    15.5  
    15.6  end
    15.7 -