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.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.162 +
1.163 +lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
1.165 +
1.166 +lemma image_mset_single [simp]: "image_mset f {#x#} = {#f x#}"
1.168 +
1.169 +lemma image_mset_insert:
1.170 +  "image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
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.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.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.384 -
1.385 -lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
1.387 -
1.388 -lemma image_mset_single [simp]: "image_mset f {#x#} = {#f x#}"
1.390 -
1.391 -lemma image_mset_insert:
1.392 -  "image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
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.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"
```