src/HOL/Library/Multiset.thy
changeset 48023 6dfe5e774012
parent 48012 b6e5e86a7303
child 48040 4caf6cd063be
     1.1 --- a/src/HOL/Library/Multiset.thy	Tue May 29 13:46:50 2012 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Tue May 29 17:06:04 2012 +0200
     1.3 @@ -654,6 +654,221 @@
     1.4  qed
     1.5  
     1.6  
     1.7 +subsection {* The fold combinator *}
     1.8 +
     1.9 +text {*
    1.10 +  The intended behaviour is
    1.11 +  @{text "fold_mset f z {#x\<^isub>1, ..., x\<^isub>n#} = f x\<^isub>1 (\<dots> (f x\<^isub>n z)\<dots>)"}
    1.12 +  if @{text f} is associative-commutative. 
    1.13 +*}
    1.14 +
    1.15 +text {*
    1.16 +  The graph of @{text "fold_mset"}, @{text "z"}: the start element,
    1.17 +  @{text "f"}: folding function, @{text "A"}: the multiset, @{text
    1.18 +  "y"}: the result.
    1.19 +*}
    1.20 +inductive 
    1.21 +  fold_msetG :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b \<Rightarrow> bool" 
    1.22 +  for f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" 
    1.23 +  and z :: 'b
    1.24 +where
    1.25 +  emptyI [intro]:  "fold_msetG f z {#} z"
    1.26 +| insertI [intro]: "fold_msetG f z A y \<Longrightarrow> fold_msetG f z (A + {#x#}) (f x y)"
    1.27 +
    1.28 +inductive_cases empty_fold_msetGE [elim!]: "fold_msetG f z {#} x"
    1.29 +inductive_cases insert_fold_msetGE: "fold_msetG f z (A + {#}) y" 
    1.30 +
    1.31 +definition
    1.32 +  fold_mset :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b" where
    1.33 +  "fold_mset f z A = (THE x. fold_msetG f z A x)"
    1.34 +
    1.35 +lemma Diff1_fold_msetG:
    1.36 +  "fold_msetG f z (A - {#x#}) y \<Longrightarrow> x \<in># A \<Longrightarrow> fold_msetG f z A (f x y)"
    1.37 +apply (frule_tac x = x in fold_msetG.insertI)
    1.38 +apply auto
    1.39 +done
    1.40 +
    1.41 +lemma fold_msetG_nonempty: "\<exists>x. fold_msetG f z A x"
    1.42 +apply (induct A)
    1.43 + apply blast
    1.44 +apply clarsimp
    1.45 +apply (drule_tac x = x in fold_msetG.insertI)
    1.46 +apply auto
    1.47 +done
    1.48 +
    1.49 +lemma fold_mset_empty[simp]: "fold_mset f z {#} = z"
    1.50 +unfolding fold_mset_def by blast
    1.51 +
    1.52 +context comp_fun_commute
    1.53 +begin
    1.54 +
    1.55 +lemma fold_msetG_insertE_aux:
    1.56 +  "fold_msetG f z A y \<Longrightarrow> a \<in># A \<Longrightarrow> \<exists>y'. y = f a y' \<and> fold_msetG f z (A - {#a#}) y'"
    1.57 +proof (induct set: fold_msetG)
    1.58 +  case (insertI A y x) show ?case
    1.59 +  proof (cases "x = a")
    1.60 +    assume "x = a" with insertI show ?case by auto
    1.61 +  next
    1.62 +    assume "x \<noteq> a"
    1.63 +    then obtain y' where y: "y = f a y'" and y': "fold_msetG f z (A - {#a#}) y'"
    1.64 +      using insertI by auto
    1.65 +    have "f x y = f a (f x y')"
    1.66 +      unfolding y by (rule fun_left_comm)
    1.67 +    moreover have "fold_msetG f z (A + {#x#} - {#a#}) (f x y')"
    1.68 +      using y' and `x \<noteq> a`
    1.69 +      by (simp add: diff_union_swap [symmetric] fold_msetG.insertI)
    1.70 +    ultimately show ?case by fast
    1.71 +  qed
    1.72 +qed simp
    1.73 +
    1.74 +lemma fold_msetG_insertE:
    1.75 +  assumes "fold_msetG f z (A + {#x#}) v"
    1.76 +  obtains y where "v = f x y" and "fold_msetG f z A y"
    1.77 +using assms by (auto dest: fold_msetG_insertE_aux [where a=x])
    1.78 +
    1.79 +lemma fold_msetG_determ:
    1.80 +  "fold_msetG f z A x \<Longrightarrow> fold_msetG f z A y \<Longrightarrow> y = x"
    1.81 +proof (induct arbitrary: y set: fold_msetG)
    1.82 +  case (insertI A y x v)
    1.83 +  from `fold_msetG f z (A + {#x#}) v`
    1.84 +  obtain y' where "v = f x y'" and "fold_msetG f z A y'"
    1.85 +    by (rule fold_msetG_insertE)
    1.86 +  from `fold_msetG f z A y'` have "y' = y" by (rule insertI)
    1.87 +  with `v = f x y'` show "v = f x y" by simp
    1.88 +qed fast
    1.89 +
    1.90 +lemma fold_mset_equality: "fold_msetG f z A y \<Longrightarrow> fold_mset f z A = y"
    1.91 +unfolding fold_mset_def by (blast intro: fold_msetG_determ)
    1.92 +
    1.93 +lemma fold_msetG_fold_mset: "fold_msetG f z A (fold_mset f z A)"
    1.94 +proof -
    1.95 +  from fold_msetG_nonempty fold_msetG_determ
    1.96 +  have "\<exists>!x. fold_msetG f z A x" by (rule ex_ex1I)
    1.97 +  then show ?thesis unfolding fold_mset_def by (rule theI')
    1.98 +qed
    1.99 +
   1.100 +lemma fold_mset_insert:
   1.101 +  "fold_mset f z (A + {#x#}) = f x (fold_mset f z A)"
   1.102 +by (intro fold_mset_equality fold_msetG.insertI fold_msetG_fold_mset)
   1.103 +
   1.104 +lemma fold_mset_commute: "f x (fold_mset f z A) = fold_mset f (f x z) A"
   1.105 +by (induct A) (auto simp: fold_mset_insert fun_left_comm [of x])
   1.106 +
   1.107 +lemma fold_mset_single [simp]: "fold_mset f z {#x#} = f x z"
   1.108 +using fold_mset_insert [of z "{#}"] by simp
   1.109 +
   1.110 +lemma fold_mset_union [simp]:
   1.111 +  "fold_mset f z (A+B) = fold_mset f (fold_mset f z A) B"
   1.112 +proof (induct A)
   1.113 +  case empty then show ?case by simp
   1.114 +next
   1.115 +  case (add A x)
   1.116 +  have "A + {#x#} + B = (A+B) + {#x#}" by (simp add: add_ac)
   1.117 +  then have "fold_mset f z (A + {#x#} + B) = f x (fold_mset f z (A + B))" 
   1.118 +    by (simp add: fold_mset_insert)
   1.119 +  also have "\<dots> = fold_mset f (fold_mset f z (A + {#x#})) B"
   1.120 +    by (simp add: fold_mset_commute[of x,symmetric] add fold_mset_insert)
   1.121 +  finally show ?case .
   1.122 +qed
   1.123 +
   1.124 +lemma fold_mset_fusion:
   1.125 +  assumes "comp_fun_commute g"
   1.126 +  shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold_mset g w A) = fold_mset f (h w) A" (is "PROP ?P")
   1.127 +proof -
   1.128 +  interpret comp_fun_commute g by (fact assms)
   1.129 +  show "PROP ?P" by (induct A) auto
   1.130 +qed
   1.131 +
   1.132 +lemma fold_mset_rec:
   1.133 +  assumes "a \<in># A" 
   1.134 +  shows "fold_mset f z A = f a (fold_mset f z (A - {#a#}))"
   1.135 +proof -
   1.136 +  from assms obtain A' where "A = A' + {#a#}"
   1.137 +    by (blast dest: multi_member_split)
   1.138 +  then show ?thesis by simp
   1.139 +qed
   1.140 +
   1.141 +end
   1.142 +
   1.143 +text {*
   1.144 +  A note on code generation: When defining some function containing a
   1.145 +  subterm @{term"fold_mset F"}, code generation is not automatic. When
   1.146 +  interpreting locale @{text left_commutative} with @{text F}, the
   1.147 +  would be code thms for @{const fold_mset} become thms like
   1.148 +  @{term"fold_mset F z {#} = z"} where @{text F} is not a pattern but
   1.149 +  contains defined symbols, i.e.\ is not a code thm. Hence a separate
   1.150 +  constant with its own code thms needs to be introduced for @{text
   1.151 +  F}. See the image operator below.
   1.152 +*}
   1.153 +
   1.154 +
   1.155 +subsection {* Image *}
   1.156 +
   1.157 +definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
   1.158 +  "image_mset f = fold_mset (op + o single o f) {#}"
   1.159 +
   1.160 +interpretation image_fun_commute: comp_fun_commute "op + o single o f" for f
   1.161 +proof qed (simp add: add_ac fun_eq_iff)
   1.162 +
   1.163 +lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
   1.164 +by (simp add: image_mset_def)
   1.165 +
   1.166 +lemma image_mset_single [simp]: "image_mset f {#x#} = {#f x#}"
   1.167 +by (simp add: image_mset_def)
   1.168 +
   1.169 +lemma image_mset_insert:
   1.170 +  "image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
   1.171 +by (simp add: image_mset_def add_ac)
   1.172 +
   1.173 +lemma image_mset_union [simp]:
   1.174 +  "image_mset f (M+N) = image_mset f M + image_mset f N"
   1.175 +apply (induct N)
   1.176 + apply simp
   1.177 +apply (simp add: add_assoc [symmetric] image_mset_insert)
   1.178 +done
   1.179 +
   1.180 +lemma size_image_mset [simp]: "size (image_mset f M) = size M"
   1.181 +by (induct M) simp_all
   1.182 +
   1.183 +lemma image_mset_is_empty_iff [simp]: "image_mset f M = {#} \<longleftrightarrow> M = {#}"
   1.184 +by (cases M) auto
   1.185 +
   1.186 +syntax
   1.187 +  "_comprehension1_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
   1.188 +      ("({#_/. _ :# _#})")
   1.189 +translations
   1.190 +  "{#e. x:#M#}" == "CONST image_mset (%x. e) M"
   1.191 +
   1.192 +syntax
   1.193 +  "_comprehension2_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
   1.194 +      ("({#_/ | _ :# _./ _#})")
   1.195 +translations
   1.196 +  "{#e | x:#M. P#}" => "{#e. x :# {# x:#M. P#}#}"
   1.197 +
   1.198 +text {*
   1.199 +  This allows to write not just filters like @{term "{#x:#M. x<c#}"}
   1.200 +  but also images like @{term "{#x+x. x:#M #}"} and @{term [source]
   1.201 +  "{#x+x|x:#M. x<c#}"}, where the latter is currently displayed as
   1.202 +  @{term "{#x+x|x:#M. x<c#}"}.
   1.203 +*}
   1.204 +
   1.205 +enriched_type image_mset: image_mset
   1.206 +proof -
   1.207 +  fix f g show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)"
   1.208 +  proof
   1.209 +    fix A
   1.210 +    show "(image_mset f \<circ> image_mset g) A = image_mset (f \<circ> g) A"
   1.211 +      by (induct A) simp_all
   1.212 +  qed
   1.213 +  show "image_mset id = id"
   1.214 +  proof
   1.215 +    fix A
   1.216 +    show "image_mset id A = id A"
   1.217 +      by (induct A) simp_all
   1.218 +  qed
   1.219 +qed
   1.220 +
   1.221 +
   1.222  subsection {* Alternative representations *}
   1.223  
   1.224  subsubsection {* Lists *}
   1.225 @@ -1456,221 +1671,6 @@
   1.226  qed (auto simp add: le_multiset_def intro: union_less_mono2)
   1.227  
   1.228  
   1.229 -subsection {* The fold combinator *}
   1.230 -
   1.231 -text {*
   1.232 -  The intended behaviour is
   1.233 -  @{text "fold_mset f z {#x\<^isub>1, ..., x\<^isub>n#} = f x\<^isub>1 (\<dots> (f x\<^isub>n z)\<dots>)"}
   1.234 -  if @{text f} is associative-commutative. 
   1.235 -*}
   1.236 -
   1.237 -text {*
   1.238 -  The graph of @{text "fold_mset"}, @{text "z"}: the start element,
   1.239 -  @{text "f"}: folding function, @{text "A"}: the multiset, @{text
   1.240 -  "y"}: the result.
   1.241 -*}
   1.242 -inductive 
   1.243 -  fold_msetG :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b \<Rightarrow> bool" 
   1.244 -  for f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" 
   1.245 -  and z :: 'b
   1.246 -where
   1.247 -  emptyI [intro]:  "fold_msetG f z {#} z"
   1.248 -| insertI [intro]: "fold_msetG f z A y \<Longrightarrow> fold_msetG f z (A + {#x#}) (f x y)"
   1.249 -
   1.250 -inductive_cases empty_fold_msetGE [elim!]: "fold_msetG f z {#} x"
   1.251 -inductive_cases insert_fold_msetGE: "fold_msetG f z (A + {#}) y" 
   1.252 -
   1.253 -definition
   1.254 -  fold_mset :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b" where
   1.255 -  "fold_mset f z A = (THE x. fold_msetG f z A x)"
   1.256 -
   1.257 -lemma Diff1_fold_msetG:
   1.258 -  "fold_msetG f z (A - {#x#}) y \<Longrightarrow> x \<in># A \<Longrightarrow> fold_msetG f z A (f x y)"
   1.259 -apply (frule_tac x = x in fold_msetG.insertI)
   1.260 -apply auto
   1.261 -done
   1.262 -
   1.263 -lemma fold_msetG_nonempty: "\<exists>x. fold_msetG f z A x"
   1.264 -apply (induct A)
   1.265 - apply blast
   1.266 -apply clarsimp
   1.267 -apply (drule_tac x = x in fold_msetG.insertI)
   1.268 -apply auto
   1.269 -done
   1.270 -
   1.271 -lemma fold_mset_empty[simp]: "fold_mset f z {#} = z"
   1.272 -unfolding fold_mset_def by blast
   1.273 -
   1.274 -context comp_fun_commute
   1.275 -begin
   1.276 -
   1.277 -lemma fold_msetG_insertE_aux:
   1.278 -  "fold_msetG f z A y \<Longrightarrow> a \<in># A \<Longrightarrow> \<exists>y'. y = f a y' \<and> fold_msetG f z (A - {#a#}) y'"
   1.279 -proof (induct set: fold_msetG)
   1.280 -  case (insertI A y x) show ?case
   1.281 -  proof (cases "x = a")
   1.282 -    assume "x = a" with insertI show ?case by auto
   1.283 -  next
   1.284 -    assume "x \<noteq> a"
   1.285 -    then obtain y' where y: "y = f a y'" and y': "fold_msetG f z (A - {#a#}) y'"
   1.286 -      using insertI by auto
   1.287 -    have "f x y = f a (f x y')"
   1.288 -      unfolding y by (rule fun_left_comm)
   1.289 -    moreover have "fold_msetG f z (A + {#x#} - {#a#}) (f x y')"
   1.290 -      using y' and `x \<noteq> a`
   1.291 -      by (simp add: diff_union_swap [symmetric] fold_msetG.insertI)
   1.292 -    ultimately show ?case by fast
   1.293 -  qed
   1.294 -qed simp
   1.295 -
   1.296 -lemma fold_msetG_insertE:
   1.297 -  assumes "fold_msetG f z (A + {#x#}) v"
   1.298 -  obtains y where "v = f x y" and "fold_msetG f z A y"
   1.299 -using assms by (auto dest: fold_msetG_insertE_aux [where a=x])
   1.300 -
   1.301 -lemma fold_msetG_determ:
   1.302 -  "fold_msetG f z A x \<Longrightarrow> fold_msetG f z A y \<Longrightarrow> y = x"
   1.303 -proof (induct arbitrary: y set: fold_msetG)
   1.304 -  case (insertI A y x v)
   1.305 -  from `fold_msetG f z (A + {#x#}) v`
   1.306 -  obtain y' where "v = f x y'" and "fold_msetG f z A y'"
   1.307 -    by (rule fold_msetG_insertE)
   1.308 -  from `fold_msetG f z A y'` have "y' = y" by (rule insertI)
   1.309 -  with `v = f x y'` show "v = f x y" by simp
   1.310 -qed fast
   1.311 -
   1.312 -lemma fold_mset_equality: "fold_msetG f z A y \<Longrightarrow> fold_mset f z A = y"
   1.313 -unfolding fold_mset_def by (blast intro: fold_msetG_determ)
   1.314 -
   1.315 -lemma fold_msetG_fold_mset: "fold_msetG f z A (fold_mset f z A)"
   1.316 -proof -
   1.317 -  from fold_msetG_nonempty fold_msetG_determ
   1.318 -  have "\<exists>!x. fold_msetG f z A x" by (rule ex_ex1I)
   1.319 -  then show ?thesis unfolding fold_mset_def by (rule theI')
   1.320 -qed
   1.321 -
   1.322 -lemma fold_mset_insert:
   1.323 -  "fold_mset f z (A + {#x#}) = f x (fold_mset f z A)"
   1.324 -by (intro fold_mset_equality fold_msetG.insertI fold_msetG_fold_mset)
   1.325 -
   1.326 -lemma fold_mset_commute: "f x (fold_mset f z A) = fold_mset f (f x z) A"
   1.327 -by (induct A) (auto simp: fold_mset_insert fun_left_comm [of x])
   1.328 -
   1.329 -lemma fold_mset_single [simp]: "fold_mset f z {#x#} = f x z"
   1.330 -using fold_mset_insert [of z "{#}"] by simp
   1.331 -
   1.332 -lemma fold_mset_union [simp]:
   1.333 -  "fold_mset f z (A+B) = fold_mset f (fold_mset f z A) B"
   1.334 -proof (induct A)
   1.335 -  case empty then show ?case by simp
   1.336 -next
   1.337 -  case (add A x)
   1.338 -  have "A + {#x#} + B = (A+B) + {#x#}" by (simp add: add_ac)
   1.339 -  then have "fold_mset f z (A + {#x#} + B) = f x (fold_mset f z (A + B))" 
   1.340 -    by (simp add: fold_mset_insert)
   1.341 -  also have "\<dots> = fold_mset f (fold_mset f z (A + {#x#})) B"
   1.342 -    by (simp add: fold_mset_commute[of x,symmetric] add fold_mset_insert)
   1.343 -  finally show ?case .
   1.344 -qed
   1.345 -
   1.346 -lemma fold_mset_fusion:
   1.347 -  assumes "comp_fun_commute g"
   1.348 -  shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold_mset g w A) = fold_mset f (h w) A" (is "PROP ?P")
   1.349 -proof -
   1.350 -  interpret comp_fun_commute g by (fact assms)
   1.351 -  show "PROP ?P" by (induct A) auto
   1.352 -qed
   1.353 -
   1.354 -lemma fold_mset_rec:
   1.355 -  assumes "a \<in># A" 
   1.356 -  shows "fold_mset f z A = f a (fold_mset f z (A - {#a#}))"
   1.357 -proof -
   1.358 -  from assms obtain A' where "A = A' + {#a#}"
   1.359 -    by (blast dest: multi_member_split)
   1.360 -  then show ?thesis by simp
   1.361 -qed
   1.362 -
   1.363 -end
   1.364 -
   1.365 -text {*
   1.366 -  A note on code generation: When defining some function containing a
   1.367 -  subterm @{term"fold_mset F"}, code generation is not automatic. When
   1.368 -  interpreting locale @{text left_commutative} with @{text F}, the
   1.369 -  would be code thms for @{const fold_mset} become thms like
   1.370 -  @{term"fold_mset F z {#} = z"} where @{text F} is not a pattern but
   1.371 -  contains defined symbols, i.e.\ is not a code thm. Hence a separate
   1.372 -  constant with its own code thms needs to be introduced for @{text
   1.373 -  F}. See the image operator below.
   1.374 -*}
   1.375 -
   1.376 -
   1.377 -subsection {* Image *}
   1.378 -
   1.379 -definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
   1.380 -  "image_mset f = fold_mset (op + o single o f) {#}"
   1.381 -
   1.382 -interpretation image_fun_commute: comp_fun_commute "op + o single o f" for f
   1.383 -proof qed (simp add: add_ac fun_eq_iff)
   1.384 -
   1.385 -lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
   1.386 -by (simp add: image_mset_def)
   1.387 -
   1.388 -lemma image_mset_single [simp]: "image_mset f {#x#} = {#f x#}"
   1.389 -by (simp add: image_mset_def)
   1.390 -
   1.391 -lemma image_mset_insert:
   1.392 -  "image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
   1.393 -by (simp add: image_mset_def add_ac)
   1.394 -
   1.395 -lemma image_mset_union [simp]:
   1.396 -  "image_mset f (M+N) = image_mset f M + image_mset f N"
   1.397 -apply (induct N)
   1.398 - apply simp
   1.399 -apply (simp add: add_assoc [symmetric] image_mset_insert)
   1.400 -done
   1.401 -
   1.402 -lemma size_image_mset [simp]: "size (image_mset f M) = size M"
   1.403 -by (induct M) simp_all
   1.404 -
   1.405 -lemma image_mset_is_empty_iff [simp]: "image_mset f M = {#} \<longleftrightarrow> M = {#}"
   1.406 -by (cases M) auto
   1.407 -
   1.408 -syntax
   1.409 -  "_comprehension1_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
   1.410 -      ("({#_/. _ :# _#})")
   1.411 -translations
   1.412 -  "{#e. x:#M#}" == "CONST image_mset (%x. e) M"
   1.413 -
   1.414 -syntax
   1.415 -  "_comprehension2_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
   1.416 -      ("({#_/ | _ :# _./ _#})")
   1.417 -translations
   1.418 -  "{#e | x:#M. P#}" => "{#e. x :# {# x:#M. P#}#}"
   1.419 -
   1.420 -text {*
   1.421 -  This allows to write not just filters like @{term "{#x:#M. x<c#}"}
   1.422 -  but also images like @{term "{#x+x. x:#M #}"} and @{term [source]
   1.423 -  "{#x+x|x:#M. x<c#}"}, where the latter is currently displayed as
   1.424 -  @{term "{#x+x|x:#M. x<c#}"}.
   1.425 -*}
   1.426 -
   1.427 -enriched_type image_mset: image_mset
   1.428 -proof -
   1.429 -  fix f g show "image_mset f \<circ> image_mset g = image_mset (f \<circ> g)"
   1.430 -  proof
   1.431 -    fix A
   1.432 -    show "(image_mset f \<circ> image_mset g) A = image_mset (f \<circ> g) A"
   1.433 -      by (induct A) simp_all
   1.434 -  qed
   1.435 -  show "image_mset id = id"
   1.436 -  proof
   1.437 -    fix A
   1.438 -    show "image_mset id A = id A"
   1.439 -      by (induct A) simp_all
   1.440 -  qed
   1.441 -qed
   1.442 -
   1.443 -
   1.444  subsection {* Termination proofs with multiset orders *}
   1.445  
   1.446  lemma multi_member_skip: "x \<in># XS \<Longrightarrow> x \<in># {# y #} + XS"