author wenzelm Tue Feb 26 16:10:54 2008 +0100 (2008-02-26) changeset 26145 95670b6e1fa3 parent 26144 98d23fc02585 child 26146 61cb176d0385
tuned document;
tuned proofs;
```     1.1 --- a/src/HOL/Library/Multiset.thy	Tue Feb 26 16:10:54 2008 +0100
1.2 +++ b/src/HOL/Library/Multiset.thy	Tue Feb 26 16:10:54 2008 +0100
1.3 @@ -43,7 +43,8 @@
1.4    Melem :: "'a => 'a multiset => bool"  ("(_/ :# _)" [50, 51] 50) where
1.5    "a :# M == 0 < count M a"
1.6
1.7 -notation (xsymbols) Melem (infix "\<in>#" 50)
1.8 +notation (xsymbols)
1.9 +  Melem (infix "\<in>#" 50)
1.10
1.11  syntax
1.12    "_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset"    ("(1{# _ :# _./ _#})")
1.13 @@ -59,16 +60,16 @@
1.14
1.15  definition
1.16    union_def[code func del]:
1.17 -  "M + N == Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
1.18 +  "M + N = Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
1.19
1.20  definition
1.21 -  diff_def: "M - N == Abs_multiset (\<lambda>a. Rep_multiset M a - Rep_multiset N a)"
1.22 +  diff_def: "M - N = Abs_multiset (\<lambda>a. Rep_multiset M a - Rep_multiset N a)"
1.23
1.24  definition
1.25 -  Zero_multiset_def [simp]: "0 == {#}"
1.26 +  Zero_multiset_def [simp]: "0 = {#}"
1.27
1.28  definition
1.29 -  size_def[code func del]: "size M == setsum (count M) (set_of M)"
1.30 +  size_def[code func del]: "size M = setsum (count M) (set_of M)"
1.31
1.32  instance ..
1.33
1.34 @@ -78,9 +79,9 @@
1.35    multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"  (infixl "#\<inter>" 70) where
1.36    "multiset_inter A B = A - (A - B)"
1.37
1.38 -syntax -- "Multiset Enumeration"
1.39 +text {* Multiset Enumeration *}
1.40 +syntax
1.41    "@multiset" :: "args => 'a multiset"    ("{#(_)#}")
1.42 -
1.43  translations
1.44    "{#x, xs#}" == "{#x#} + {#xs#}"
1.45    "{#x#}" == "CONST single x"
1.46 @@ -119,18 +120,19 @@
1.47  lemmas in_multiset = const0_in_multiset only1_in_multiset
1.48    union_preserves_multiset diff_preserves_multiset MCollect_preserves_multiset
1.49
1.50 +
1.51  subsection {* Algebraic properties *}
1.52
1.53  subsubsection {* Union *}
1.54
1.55  lemma union_empty [simp]: "M + {#} = M \<and> {#} + M = M"
1.56 -by (simp add: union_def Mempty_def in_multiset)
1.57 +  by (simp add: union_def Mempty_def in_multiset)
1.58
1.59  lemma union_commute: "M + N = N + (M::'a multiset)"
1.60 -by (simp add: union_def add_ac in_multiset)
1.61 +  by (simp add: union_def add_ac in_multiset)
1.62
1.63  lemma union_assoc: "(M + N) + K = M + (N + (K::'a multiset))"
1.64 -by (simp add: union_def add_ac in_multiset)
1.65 +  by (simp add: union_def add_ac in_multiset)
1.66
1.67  lemma union_lcomm: "M + (N + K) = N + (M + (K::'a multiset))"
1.68  proof -
1.69 @@ -157,62 +159,62 @@
1.70  subsubsection {* Difference *}
1.71
1.72  lemma diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
1.73 -by (simp add: Mempty_def diff_def in_multiset)
1.74 +  by (simp add: Mempty_def diff_def in_multiset)
1.75
1.76  lemma diff_union_inverse2 [simp]: "M + {#a#} - {#a#} = M"
1.77 -by (simp add: union_def diff_def in_multiset)
1.78 +  by (simp add: union_def diff_def in_multiset)
1.79
1.80  lemma diff_cancel: "A - A = {#}"
1.81 -by (simp add: diff_def Mempty_def)
1.82 +  by (simp add: diff_def Mempty_def)
1.83
1.84
1.85  subsubsection {* Count of elements *}
1.86
1.87  lemma count_empty [simp]: "count {#} a = 0"
1.88 -by (simp add: count_def Mempty_def in_multiset)
1.89 +  by (simp add: count_def Mempty_def in_multiset)
1.90
1.91  lemma count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)"
1.92 -by (simp add: count_def single_def in_multiset)
1.93 +  by (simp add: count_def single_def in_multiset)
1.94
1.95  lemma count_union [simp]: "count (M + N) a = count M a + count N a"
1.96 -by (simp add: count_def union_def in_multiset)
1.97 +  by (simp add: count_def union_def in_multiset)
1.98
1.99  lemma count_diff [simp]: "count (M - N) a = count M a - count N a"
1.100 -by (simp add: count_def diff_def in_multiset)
1.101 +  by (simp add: count_def diff_def in_multiset)
1.102
1.103  lemma count_MCollect [simp]:
1.104 -  "count {# x:#M. P x #} a = (if P a then count M a else 0)"
1.105 -by (simp add: count_def MCollect_def in_multiset)
1.106 +    "count {# x:#M. P x #} a = (if P a then count M a else 0)"
1.107 +  by (simp add: count_def MCollect_def in_multiset)
1.108
1.109
1.110  subsubsection {* Set of elements *}
1.111
1.112  lemma set_of_empty [simp]: "set_of {#} = {}"
1.113 -by (simp add: set_of_def)
1.114 +  by (simp add: set_of_def)
1.115
1.116  lemma set_of_single [simp]: "set_of {#b#} = {b}"
1.117 -by (simp add: set_of_def)
1.118 +  by (simp add: set_of_def)
1.119
1.120  lemma set_of_union [simp]: "set_of (M + N) = set_of M \<union> set_of N"
1.121 -by (auto simp add: set_of_def)
1.122 +  by (auto simp add: set_of_def)
1.123
1.124  lemma set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})"
1.125 -by(auto simp: set_of_def Mempty_def in_multiset count_def expand_fun_eq)
1.126 +  by (auto simp: set_of_def Mempty_def in_multiset count_def expand_fun_eq)
1.127
1.128  lemma mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)"
1.129 -by (auto simp add: set_of_def)
1.130 +  by (auto simp add: set_of_def)
1.131
1.132  lemma set_of_MCollect [simp]: "set_of {# x:#M. P x #} = set_of M \<inter> {x. P x}"
1.133 -by (auto simp add: set_of_def)
1.134 +  by (auto simp add: set_of_def)
1.135
1.136
1.137  subsubsection {* Size *}
1.138
1.139  lemma size_empty [simp,code func]: "size {#} = 0"
1.140 -by (simp add: size_def)
1.141 +  by (simp add: size_def)
1.142
1.143  lemma size_single [simp,code func]: "size {#b#} = 1"
1.144 -by (simp add: size_def)
1.145 +  by (simp add: size_def)
1.146
1.147  lemma finite_set_of [iff]: "finite (set_of M)"
1.148    using Rep_multiset [of M]
1.149 @@ -236,53 +238,55 @@
1.150    done
1.151
1.152  lemma size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})"
1.153 -apply (unfold size_def Mempty_def count_def, auto simp: in_multiset)
1.154 -apply (simp add: set_of_def count_def in_multiset expand_fun_eq)
1.155 -done
1.156 +  apply (unfold size_def Mempty_def count_def, auto simp: in_multiset)
1.157 +  apply (simp add: set_of_def count_def in_multiset expand_fun_eq)
1.158 +  done
1.159
1.160  lemma nonempty_has_size: "(S \<noteq> {#}) = (0 < size S)"
1.161 -by(metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty)
1.162 +  by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty)
1.163
1.164  lemma size_eq_Suc_imp_elem: "size M = Suc n ==> \<exists>a. a :# M"
1.165    apply (unfold size_def)
1.166 -  apply (drule setsum_SucD, auto)
1.167 +  apply (drule setsum_SucD)
1.168 +  apply auto
1.169    done
1.170
1.171 +
1.172  subsubsection {* Equality of multisets *}
1.173
1.174  lemma multiset_eq_conv_count_eq: "(M = N) = (\<forall>a. count M a = count N a)"
1.175    by (simp add: count_def expand_fun_eq)
1.176
1.177  lemma single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}"
1.178 -by (simp add: single_def Mempty_def in_multiset expand_fun_eq)
1.179 +  by (simp add: single_def Mempty_def in_multiset expand_fun_eq)
1.180
1.181  lemma single_eq_single [simp]: "({#a#} = {#b#}) = (a = b)"
1.182 -by (auto simp add: single_def in_multiset expand_fun_eq)
1.183 +  by (auto simp add: single_def in_multiset expand_fun_eq)
1.184
1.185  lemma union_eq_empty [iff]: "(M + N = {#}) = (M = {#} \<and> N = {#})"
1.186 -by (auto simp add: union_def Mempty_def in_multiset expand_fun_eq)
1.187 +  by (auto simp add: union_def Mempty_def in_multiset expand_fun_eq)
1.188
1.189  lemma empty_eq_union [iff]: "({#} = M + N) = (M = {#} \<and> N = {#})"
1.190 -by (auto simp add: union_def Mempty_def in_multiset expand_fun_eq)
1.191 +  by (auto simp add: union_def Mempty_def in_multiset expand_fun_eq)
1.192
1.193  lemma union_right_cancel [simp]: "(M + K = N + K) = (M = (N::'a multiset))"
1.194 -by (simp add: union_def in_multiset expand_fun_eq)
1.195 +  by (simp add: union_def in_multiset expand_fun_eq)
1.196
1.197  lemma union_left_cancel [simp]: "(K + M = K + N) = (M = (N::'a multiset))"
1.198 -by (simp add: union_def in_multiset expand_fun_eq)
1.199 +  by (simp add: union_def in_multiset expand_fun_eq)
1.200
1.201  lemma union_is_single:
1.202 -  "(M + N = {#a#}) = (M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#})"
1.203 -apply (simp add: Mempty_def single_def union_def in_multiset add_is_1 expand_fun_eq)
1.204 -apply blast
1.205 -done
1.206 +    "(M + N = {#a#}) = (M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#})"
1.207 +  apply (simp add: Mempty_def single_def union_def in_multiset add_is_1 expand_fun_eq)
1.208 +  apply blast
1.209 +  done
1.210
1.211  lemma single_is_union:
1.212 -     "({#a#} = M + N) = ({#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = N)"
1.213 -apply (unfold Mempty_def single_def union_def)
1.215 -apply (blast dest: sym)
1.216 -done
1.217 +    "({#a#} = M + N) \<longleftrightarrow> ({#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = N)"
1.218 +  apply (unfold Mempty_def single_def union_def)
1.220 +  apply (blast dest: sym)
1.221 +  done
1.222
1.224    "(M + {#a#} = N + {#b#}) =
1.225 @@ -312,10 +316,10 @@
1.226
1.227  lemma multi_union_self_other_eq:
1.228    "(A::'a multiset) + X = A + Y \<Longrightarrow> X = Y"
1.229 -  by (induct A arbitrary: X Y, auto)
1.230 +  by (induct A arbitrary: X Y) auto
1.231
1.232  lemma multi_self_add_other_not_self[simp]: "(A = A + {#x#}) = False"
1.233 -by (metis single_not_empty union_empty union_left_cancel)
1.234 +  by (metis single_not_empty union_empty union_left_cancel)
1.235
1.236  lemma insert_noteq_member:
1.237    assumes BC: "B + {#b#} = C + {#c#}"
1.238 @@ -324,38 +328,38 @@
1.239  proof -
1.240    have "c \<in># C + {#c#}" by simp
1.241    have nc: "\<not> c \<in># {#b#}" using bnotc by simp
1.242 -  hence "c \<in># B + {#b#}" using BC by simp
1.243 -  thus "c \<in># B" using nc by simp
1.244 +  then have "c \<in># B + {#b#}" using BC by simp
1.245 +  then show "c \<in># B" using nc by simp
1.246  qed
1.247
1.248
1.250    "(M + {#a#} = N + {#b#}) =
1.251      (M = N \<and> a = b \<or> (\<exists>K. M = K + {#b#} \<and> N = K + {#a#}))"
1.253 +  by (auto simp add: add_eq_conv_diff)
1.254
1.255
1.256  lemma empty_multiset_count:
1.257    "(\<forall>x. count A x = 0) = (A = {#})"
1.258 -by(metis count_empty multiset_eq_conv_count_eq)
1.259 +  by (metis count_empty multiset_eq_conv_count_eq)
1.260
1.261
1.262  subsubsection {* Intersection *}
1.263
1.264  lemma multiset_inter_count:
1.265 -  "count (A #\<inter> B) x = min (count A x) (count B x)"
1.266 -by (simp add: multiset_inter_def min_def)
1.267 +    "count (A #\<inter> B) x = min (count A x) (count B x)"
1.268 +  by (simp add: multiset_inter_def min_def)
1.269
1.270  lemma multiset_inter_commute: "A #\<inter> B = B #\<inter> A"
1.271 -by (simp add: multiset_eq_conv_count_eq multiset_inter_count
1.272 +  by (simp add: multiset_eq_conv_count_eq multiset_inter_count
1.273      min_max.inf_commute)
1.274
1.275  lemma multiset_inter_assoc: "A #\<inter> (B #\<inter> C) = A #\<inter> B #\<inter> C"
1.276 -by (simp add: multiset_eq_conv_count_eq multiset_inter_count
1.277 +  by (simp add: multiset_eq_conv_count_eq multiset_inter_count
1.278      min_max.inf_assoc)
1.279
1.280  lemma multiset_inter_left_commute: "A #\<inter> (B #\<inter> C) = B #\<inter> (A #\<inter> C)"
1.281 -by (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def)
1.282 +  by (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def)
1.283
1.284  lemmas multiset_inter_ac =
1.285    multiset_inter_commute
1.286 @@ -363,7 +367,7 @@
1.287    multiset_inter_left_commute
1.288
1.289  lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
1.290 -by (simp add: multiset_eq_conv_count_eq multiset_inter_count)
1.291 +  by (simp add: multiset_eq_conv_count_eq multiset_inter_count)
1.292
1.293  lemma multiset_union_diff_commute: "B #\<inter> C = {#} \<Longrightarrow> A + B - C = A - C + B"
1.294    apply (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def
1.295 @@ -377,15 +381,18 @@
1.296  subsubsection {* Comprehension (filter) *}
1.297
1.298  lemma MCollect_empty[simp, code func]: "MCollect {#} P = {#}"
1.299 -by(simp add:MCollect_def Mempty_def Abs_multiset_inject in_multiset expand_fun_eq)
1.300 +  by (simp add: MCollect_def Mempty_def Abs_multiset_inject
1.301 +    in_multiset expand_fun_eq)
1.302
1.303  lemma MCollect_single[simp, code func]:
1.304 -  "MCollect {#x#} P = (if P x then {#x#} else {#})"
1.305 -by(simp add:MCollect_def Mempty_def single_def Abs_multiset_inject in_multiset expand_fun_eq)
1.306 +    "MCollect {#x#} P = (if P x then {#x#} else {#})"
1.307 +  by (simp add: MCollect_def Mempty_def single_def Abs_multiset_inject
1.308 +    in_multiset expand_fun_eq)
1.309
1.310  lemma MCollect_union[simp, code func]:
1.311    "MCollect (M+N) f = MCollect M f + MCollect N f"
1.312 -by(simp add:MCollect_def union_def Abs_multiset_inject in_multiset expand_fun_eq)
1.313 +  by (simp add: MCollect_def union_def Abs_multiset_inject
1.314 +    in_multiset expand_fun_eq)
1.315
1.316
1.317  subsection {* Induction and case splits *}
1.318 @@ -459,33 +466,37 @@
1.319  qed
1.320
1.321  lemma multi_nonempty_split: "M \<noteq> {#} \<Longrightarrow> \<exists>A a. M = A + {#a#}"
1.322 -  by (induct M, auto)
1.323 +  by (induct M) auto
1.324
1.325  lemma multiset_cases [cases type, case_names empty add]:
1.326    assumes em:  "M = {#} \<Longrightarrow> P"
1.327    assumes add: "\<And>N x. M = N + {#x#} \<Longrightarrow> P"
1.328    shows "P"
1.329  proof (cases "M = {#}")
1.330 -  assume "M = {#}" thus ?thesis using em by simp
1.331 +  assume "M = {#}" then show ?thesis using em by simp
1.332  next
1.333    assume "M \<noteq> {#}"
1.334    then obtain M' m where "M = M' + {#m#}"
1.335      by (blast dest: multi_nonempty_split)
1.336 -  thus ?thesis using add by simp
1.337 +  then show ?thesis using add by simp
1.338  qed
1.339
1.340  lemma multi_member_split: "x \<in># M \<Longrightarrow> \<exists>A. M = A + {#x#}"
1.341 -  apply (cases M, simp)
1.342 +  apply (cases M)
1.343 +   apply simp
1.344    apply (rule_tac x="M - {#x#}" in exI, simp)
1.345    done
1.346
1.347  lemma multiset_partition: "M = {# x:#M. P x #} + {# x:#M. \<not> P x #}"
1.348 -  by (subst multiset_eq_conv_count_eq, auto)
1.349 +  apply (subst multiset_eq_conv_count_eq)
1.350 +  apply auto
1.351 +  done
1.352
1.353  declare multiset_typedef [simp del]
1.354
1.355  lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B - {#c#} \<noteq> B"
1.356 -  by (cases "B={#}", auto dest: multi_member_split)
1.357 +  by (cases "B = {#}") (auto dest: multi_member_split)
1.358 +
1.359
1.360  subsection {* Orderings *}
1.361
1.362 @@ -748,7 +759,7 @@
1.363
1.364  theorem mult_less_asym:
1.365      "M < N ==> (\<not> P ==> N < (M::'a::order multiset)) ==> P"
1.366 -  by (insert mult_less_not_sym, blast)
1.367 +  using mult_less_not_sym by blast
1.368
1.369  theorem mult_le_refl [iff]: "M <= (M::'a::order multiset)"
1.370    unfolding le_multiset_def by auto
1.371 @@ -772,9 +783,9 @@
1.372
1.373  instance multiset :: (order) order
1.374    apply intro_classes
1.375 -  apply (rule mult_less_le)
1.376 -  apply (rule mult_le_refl)
1.377 -  apply (erule mult_le_trans, assumption)
1.378 +     apply (rule mult_less_le)
1.379 +    apply (rule mult_le_refl)
1.380 +   apply (erule mult_le_trans, assumption)
1.381    apply (erule mult_le_antisym, assumption)
1.382    done
1.383
1.384 @@ -783,7 +794,8 @@
1.385
1.386  lemma mult1_union:
1.387      "(B, D) \<in> mult1 r ==> trans r ==> (C + B, C + D) \<in> mult1 r"
1.388 -  apply (unfold mult1_def, auto)
1.389 +  apply (unfold mult1_def)
1.390 +  apply auto
1.391    apply (rule_tac x = a in exI)
1.392    apply (rule_tac x = "C + M0" in exI)
1.393    apply (simp add: union_assoc)
1.394 @@ -804,8 +816,7 @@
1.395
1.396  lemma union_less_mono:
1.397      "A < C ==> B < D ==> A + B < C + (D::'a::order multiset)"
1.398 -  apply (blast intro!: union_less_mono1 union_less_mono2 mult_less_trans)
1.399 -  done
1.400 +  by (blast intro!: union_less_mono1 union_less_mono2 mult_less_trans)
1.401
1.402  lemma union_le_mono:
1.403      "A <= C ==> B <= D ==> A + B <= C + (D::'a::order multiset)"
1.404 @@ -819,7 +830,8 @@
1.405     apply (subgoal_tac "({#} + {#}, {#} + M) \<in> mult (Collect (split op <))")
1.406      prefer 2
1.407      apply (rule one_step_implies_mult)
1.408 -      apply (simp only: trans_def, auto)
1.409 +      apply (simp only: trans_def)
1.410 +      apply auto
1.411    done
1.412
1.413  lemma union_upper1: "A <= A + (B::'a::order multiset)"
1.414 @@ -832,15 +844,16 @@
1.415    by (subst union_commute) (rule union_upper1)
1.416
1.417  instance multiset :: (order) pordered_ab_semigroup_add
1.418 -apply intro_classes
1.419 -apply(erule union_le_mono[OF mult_le_refl])
1.420 -done
1.421 +  apply intro_classes
1.422 +  apply (erule union_le_mono[OF mult_le_refl])
1.423 +  done
1.424 +
1.425
1.426  subsection {* Link with lists *}
1.427
1.428  primrec multiset_of :: "'a list \<Rightarrow> 'a multiset" where
1.429 -"multiset_of [] = {#}" |
1.430 -"multiset_of (a # x) = multiset_of x + {# a #}"
1.431 +  "multiset_of [] = {#}" |
1.432 +  "multiset_of (a # x) = multiset_of x + {# a #}"
1.433
1.434  lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])"
1.435    by (induct x) auto
1.436 @@ -859,9 +872,12 @@
1.437    by (induct xs arbitrary: ys) (auto simp: union_ac)
1.438
1.439  lemma surj_multiset_of: "surj multiset_of"
1.440 -  apply (unfold surj_def, rule allI)
1.441 -  apply (rule_tac M=y in multiset_induct, auto)
1.442 -  apply (rule_tac x = "x # xa" in exI, auto)
1.443 +  apply (unfold surj_def)
1.444 +  apply (rule allI)
1.445 +  apply (rule_tac M = y in multiset_induct)
1.446 +   apply auto
1.447 +  apply (rule_tac x = "x # xa" in exI)
1.448 +  apply auto
1.449    done
1.450
1.451  lemma set_count_greater_0: "set x = {a. count (multiset_of x) a > 0}"
1.452 @@ -872,8 +888,8 @@
1.453     apply (induct x, simp, rule iffI, simp_all)
1.454     apply (rule conjI)
1.455     apply (simp_all add: set_of_multiset_of [THEN sym] del: set_of_multiset_of)
1.456 -   apply (erule_tac x=a in allE, simp, clarify)
1.457 -   apply (erule_tac x=aa in allE, simp)
1.458 +   apply (erule_tac x = a in allE, simp, clarify)
1.459 +   apply (erule_tac x = aa in allE, simp)
1.460     done
1.461
1.462  lemma multiset_of_eq_setD:
1.463 @@ -881,16 +897,16 @@
1.464    by (rule) (auto simp add:multiset_eq_conv_count_eq set_count_greater_0)
1.465
1.466  lemma set_eq_iff_multiset_of_eq_distinct:
1.467 -  "\<lbrakk>distinct x; distinct y\<rbrakk>
1.468 -   \<Longrightarrow> (set x = set y) = (multiset_of x = multiset_of y)"
1.469 +  "distinct x \<Longrightarrow> distinct y \<Longrightarrow>
1.470 +    (set x = set y) = (multiset_of x = multiset_of y)"
1.471    by (auto simp: multiset_eq_conv_count_eq distinct_count_atmost_1)
1.472
1.473  lemma set_eq_iff_multiset_of_remdups_eq:
1.474     "(set x = set y) = (multiset_of (remdups x) = multiset_of (remdups y))"
1.475    apply (rule iffI)
1.476    apply (simp add: set_eq_iff_multiset_of_eq_distinct[THEN iffD1])
1.477 -  apply (drule distinct_remdups[THEN distinct_remdups
1.478 -                      [THEN set_eq_iff_multiset_of_eq_distinct[THEN iffD2]]])
1.479 +  apply (drule distinct_remdups [THEN distinct_remdups
1.480 +      [THEN set_eq_iff_multiset_of_eq_distinct [THEN iffD2]]])
1.481    apply simp
1.482    done
1.483
1.484 @@ -903,59 +919,67 @@
1.485    by (induct xs) auto
1.486
1.487  lemma nth_mem_multiset_of: "i < length ls \<Longrightarrow> (ls ! i) :# multiset_of ls"
1.488 -by (induct ls arbitrary: i, simp, case_tac i, auto)
1.489 +  apply (induct ls arbitrary: i)
1.490 +   apply simp
1.491 +  apply (case_tac i)
1.492 +   apply auto
1.493 +  done
1.494
1.495  lemma multiset_of_remove1: "multiset_of (remove1 a xs) = multiset_of xs - {#a#}"
1.496 -by (induct xs, auto simp add: multiset_eq_conv_count_eq)
1.497 +  by (induct xs) (auto simp add: multiset_eq_conv_count_eq)
1.498
1.499  lemma multiset_of_eq_length:
1.500    assumes "multiset_of xs = multiset_of ys"
1.501 -  shows "List.length xs = List.length ys"
1.502 +  shows "length xs = length ys"
1.503    using assms
1.504  proof (induct arbitrary: ys rule: length_induct)
1.505    case (1 xs ys)
1.506    show ?case
1.507    proof (cases xs)
1.508 -    case Nil with 1(2) show ?thesis by simp
1.509 +    case Nil with "1.prems" show ?thesis by simp
1.510    next
1.511      case (Cons x xs')
1.512      note xCons = Cons
1.513      show ?thesis
1.514      proof (cases ys)
1.515        case Nil
1.516 -      with 1(2) Cons show ?thesis by simp
1.517 +      with "1.prems" Cons show ?thesis by simp
1.518      next
1.519        case (Cons y ys')
1.520        have x_in_ys: "x = y \<or> x \<in> set ys'"
1.521        proof (cases "x = y")
1.522 -	case True thus ?thesis ..
1.523 +	case True then show ?thesis ..
1.524        next
1.525  	case False
1.526 -	from 1(2)[symmetric] xCons Cons have "x :# multiset_of ys' + {#y#}" by simp
1.527 +	from "1.prems" [symmetric] xCons Cons have "x :# multiset_of ys' + {#y#}" by simp
1.528  	with False show ?thesis by (simp add: mem_set_multiset_eq)
1.529        qed
1.530 -      from 1(1) have IH: "List.length xs' < List.length xs \<longrightarrow>
1.531 -	(\<forall>x. multiset_of xs' = multiset_of x \<longrightarrow> List.length xs' = List.length x)" by blast
1.532 -      from 1(2) x_in_ys Cons xCons have "multiset_of xs' = multiset_of (remove1 x (y#ys'))"
1.533 +      from "1.hyps" have IH: "length xs' < length xs \<longrightarrow>
1.534 +	(\<forall>x. multiset_of xs' = multiset_of x \<longrightarrow> length xs' = length x)" by blast
1.535 +      from "1.prems" x_in_ys Cons xCons have "multiset_of xs' = multiset_of (remove1 x (y#ys'))"
1.536  	apply -
1.537  	apply (simp add: multiset_of_remove1, simp only: add_eq_conv_diff)
1.538  	apply fastsimp
1.539  	done
1.540 -      with IH xCons have IH': "List.length xs' = List.length (remove1 x (y#ys'))" by fastsimp
1.541 -      from x_in_ys have "x \<noteq> y \<Longrightarrow> List.length ys' > 0" by auto
1.542 +      with IH xCons have IH': "length xs' = length (remove1 x (y#ys'))" by fastsimp
1.543 +      from x_in_ys have "x \<noteq> y \<Longrightarrow> length ys' > 0" by auto
1.544        with Cons xCons x_in_ys IH' show ?thesis by (auto simp add: length_remove1)
1.545      qed
1.546    qed
1.547  qed
1.548
1.549 -text {* This lemma shows which properties suffice to show that
1.550 -  a function f with f xs = ys behaves like sort. *}
1.551 -lemma properties_for_sort: "\<lbrakk> multiset_of ys = multiset_of xs; sorted ys\<rbrakk> \<Longrightarrow> sort xs = ys"
1.552 +text {*
1.553 +  This lemma shows which properties suffice to show that a function
1.554 +  @{text "f"} with @{text "f xs = ys"} behaves like sort.
1.555 +*}
1.556 +lemma properties_for_sort:
1.557 +  "multiset_of ys = multiset_of xs \<Longrightarrow> sorted ys \<Longrightarrow> sort xs = ys"
1.558  proof (induct xs arbitrary: ys)
1.559 -  case Nil thus ?case by simp
1.560 +  case Nil then show ?case by simp
1.561  next
1.562    case (Cons x xs)
1.563 -  hence "x \<in> set ys" by (auto simp add:  mem_set_multiset_eq intro!: ccontr)
1.564 +  then have "x \<in> set ys"
1.565 +    by (auto simp add:  mem_set_multiset_eq intro!: ccontr)
1.566    with Cons.prems Cons.hyps [of "remove1 x ys"] show ?case
1.567      by (simp add: sorted_remove1 multiset_of_remove1 insort_remove1)
1.568  qed
1.569 @@ -966,27 +990,27 @@
1.570  definition
1.571    mset_le :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<le>#" 50) where
1.572    "(A \<le># B) = (\<forall>a. count A a \<le> count B a)"
1.573 +
1.574  definition
1.575    mset_less :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "<#" 50) where
1.576    "(A <# B) = (A \<le># B \<and> A \<noteq> B)"
1.577
1.578 -notation mset_le (infix "\<subseteq>#" 50)
1.579 -notation mset_less (infix "\<subset>#" 50)
1.580 +notation mset_le  (infix "\<subseteq>#" 50)
1.581 +notation mset_less  (infix "\<subset>#" 50)
1.582
1.583  lemma mset_le_refl[simp]: "A \<le># A"
1.584    unfolding mset_le_def by auto
1.585
1.586 -lemma mset_le_trans: "\<lbrakk> A \<le># B; B \<le># C \<rbrakk> \<Longrightarrow> A \<le># C"
1.587 +lemma mset_le_trans: "A \<le># B \<Longrightarrow> B \<le># C \<Longrightarrow> A \<le># C"
1.588    unfolding mset_le_def by (fast intro: order_trans)
1.589
1.590 -lemma mset_le_antisym: "\<lbrakk> A \<le># B; B \<le># A \<rbrakk> \<Longrightarrow> A = B"
1.591 +lemma mset_le_antisym: "A \<le># B \<Longrightarrow> B \<le># A \<Longrightarrow> A = B"
1.592    apply (unfold mset_le_def)
1.593 -  apply (rule multiset_eq_conv_count_eq[THEN iffD2])
1.594 +  apply (rule multiset_eq_conv_count_eq [THEN iffD2])
1.595    apply (blast intro: order_antisym)
1.596    done
1.597
1.598 -lemma mset_le_exists_conv:
1.599 -  "(A \<le># B) = (\<exists>C. B = A + C)"
1.600 +lemma mset_le_exists_conv: "(A \<le># B) = (\<exists>C. B = A + C)"
1.601    apply (unfold mset_le_def, rule iffI, rule_tac x = "B - A" in exI)
1.602    apply (auto intro: multiset_eq_conv_count_eq [THEN iffD2])
1.603    done
1.604 @@ -1000,7 +1024,7 @@
1.605  lemma mset_le_mono_add: "\<lbrakk> A \<le># B; C \<le># D \<rbrakk> \<Longrightarrow> A + C \<le># B + D"
1.606    apply (unfold mset_le_def)
1.607    apply auto
1.608 -  apply (erule_tac x=a in allE)+
1.609 +  apply (erule_tac x = a in allE)+
1.610    apply auto
1.611    done
1.612
1.613 @@ -1011,128 +1035,124 @@
1.614    unfolding mset_le_def by auto
1.615
1.616  lemma mset_le_single: "a :# B \<Longrightarrow> {#a#} \<le># B"
1.617 -by (simp add: mset_le_def)
1.618 +  by (simp add: mset_le_def)
1.619
1.620  lemma multiset_diff_union_assoc: "C \<le># B \<Longrightarrow> A + B - C = A + (B - C)"
1.621 -by (simp add: multiset_eq_conv_count_eq mset_le_def)
1.622 +  by (simp add: multiset_eq_conv_count_eq mset_le_def)
1.623
1.624  lemma mset_le_multiset_union_diff_commute:
1.625    assumes "B \<le># A"
1.626    shows "A - B + C = A + C - B"
1.627  proof -
1.628 - from mset_le_exists_conv [of "B" "A"] assms have "\<exists>D. A = B + D" ..
1.629 - from this obtain D where "A = B + D" ..
1.630 - thus ?thesis
1.631 -   apply -
1.632 -   apply simp
1.633 -   apply (subst union_commute)
1.634 -   apply (subst multiset_diff_union_assoc)
1.635 -   apply simp
1.636 -   apply (simp add: diff_cancel)
1.637 -   apply (subst union_assoc)
1.638 -   apply (subst union_commute[of "B" _])
1.639 -   apply (subst multiset_diff_union_assoc)
1.640 -   apply simp
1.641 -   apply (simp add: diff_cancel)
1.642 -   done
1.643 +  from mset_le_exists_conv [of "B" "A"] assms have "\<exists>D. A = B + D" ..
1.644 +  from this obtain D where "A = B + D" ..
1.645 +  then show ?thesis
1.646 +    apply simp
1.647 +    apply (subst union_commute)
1.648 +    apply (subst multiset_diff_union_assoc)
1.649 +    apply simp
1.650 +    apply (simp add: diff_cancel)
1.651 +    apply (subst union_assoc)
1.652 +    apply (subst union_commute[of "B" _])
1.653 +    apply (subst multiset_diff_union_assoc)
1.654 +    apply simp
1.655 +    apply (simp add: diff_cancel)
1.656 +    done
1.657  qed
1.658
1.659  lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le># multiset_of xs"
1.660 -apply (induct xs)
1.661 - apply auto
1.662 -apply (rule mset_le_trans)
1.663 - apply auto
1.664 -done
1.665 +  apply (induct xs)
1.666 +   apply auto
1.667 +  apply (rule mset_le_trans)
1.668 +   apply auto
1.669 +  done
1.670
1.671 -lemma multiset_of_update: "i < length ls \<Longrightarrow> multiset_of (ls[i := v]) = multiset_of ls - {#ls ! i#} + {#v#}"
1.672 +lemma multiset_of_update:
1.673 +  "i < length ls \<Longrightarrow> multiset_of (ls[i := v]) = multiset_of ls - {#ls ! i#} + {#v#}"
1.674  proof (induct ls arbitrary: i)
1.675 -  case Nil thus ?case by simp
1.676 +  case Nil then show ?case by simp
1.677  next
1.678    case (Cons x xs)
1.679    show ?case
1.680 -    proof (cases i)
1.681 -      case 0 thus ?thesis by simp
1.682 -    next
1.683 -      case (Suc i')
1.684 -      with Cons show ?thesis
1.685 -	apply -
1.686 -	apply simp
1.687 -	apply (subst union_assoc)
1.688 -	apply (subst union_commute[where M="{#v#}" and N="{#x#}"])
1.689 -	apply (subst union_assoc[symmetric])
1.690 -	apply simp
1.691 -	apply (rule mset_le_multiset_union_diff_commute)
1.692 -	apply (simp add: mset_le_single nth_mem_multiset_of)
1.693 -	done
1.694 +  proof (cases i)
1.695 +    case 0 then show ?thesis by simp
1.696 +  next
1.697 +    case (Suc i')
1.698 +    with Cons show ?thesis
1.699 +      apply simp
1.700 +      apply (subst union_assoc)
1.701 +      apply (subst union_commute [where M = "{#v#}" and N = "{#x#}"])
1.702 +      apply (subst union_assoc [symmetric])
1.703 +      apply simp
1.704 +      apply (rule mset_le_multiset_union_diff_commute)
1.705 +      apply (simp add: mset_le_single nth_mem_multiset_of)
1.706 +      done
1.707    qed
1.708  qed
1.709
1.710 -lemma multiset_of_swap: "\<lbrakk> i < length ls; j < length ls \<rbrakk> \<Longrightarrow> multiset_of (ls[j := ls ! i, i := ls ! j]) = multiset_of ls"
1.711 -apply (case_tac "i=j")
1.712 -apply simp
1.713 -apply (simp add: multiset_of_update)
1.714 -apply (subst elem_imp_eq_diff_union[symmetric])
1.715 -apply (simp add: nth_mem_multiset_of)
1.716 -apply simp
1.717 -done
1.718 +lemma multiset_of_swap:
1.719 +  "i < length ls \<Longrightarrow> j < length ls \<Longrightarrow>
1.720 +    multiset_of (ls[j := ls ! i, i := ls ! j]) = multiset_of ls"
1.721 +  apply (case_tac "i = j")
1.722 +   apply simp
1.723 +  apply (simp add: multiset_of_update)
1.724 +  apply (subst elem_imp_eq_diff_union[symmetric])
1.725 +   apply (simp add: nth_mem_multiset_of)
1.726 +  apply simp
1.727 +  done
1.728
1.729 -interpretation mset_order:
1.730 -  order ["op \<le>#" "op <#"]
1.731 +interpretation mset_order: order ["op \<le>#" "op <#"]
1.732    by (auto intro: order.intro mset_le_refl mset_le_antisym
1.733      mset_le_trans simp: mset_less_def)
1.734
1.735  interpretation mset_order_cancel_semigroup:
1.736 -  pordered_cancel_ab_semigroup_add ["op +" "op \<le>#" "op <#"]
1.737 +    pordered_cancel_ab_semigroup_add ["op +" "op \<le>#" "op <#"]
1.738    by unfold_locales (erule mset_le_mono_add [OF mset_le_refl])
1.739
1.740  interpretation mset_order_semigroup_cancel:
1.741 -  pordered_ab_semigroup_add_imp_le ["op +" "op \<le>#" "op <#"]
1.742 +    pordered_ab_semigroup_add_imp_le ["op +" "op \<le>#" "op <#"]
1.743    by (unfold_locales) simp
1.744
1.745
1.746 -lemma mset_lessD:
1.747 -  "\<lbrakk> A \<subset># B ; x \<in># A \<rbrakk> \<Longrightarrow> x \<in># B"
1.748 +lemma mset_lessD: "A \<subset># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
1.749    apply (clarsimp simp: mset_le_def mset_less_def)
1.750    apply (erule_tac x=x in allE)
1.751    apply auto
1.752    done
1.753
1.754 -lemma mset_leD:
1.755 -  "\<lbrakk> A \<subseteq># B ; x \<in># A \<rbrakk> \<Longrightarrow> x \<in># B"
1.756 +lemma mset_leD: "A \<subseteq># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
1.757    apply (clarsimp simp: mset_le_def mset_less_def)
1.758 -  apply (erule_tac x=x in allE)
1.759 +  apply (erule_tac x = x in allE)
1.760    apply auto
1.761    done
1.762
1.763 -lemma mset_less_insertD:
1.764 -  "(A + {#x#} \<subset># B) \<Longrightarrow> (x \<in># B \<and> A \<subset># B)"
1.765 +lemma mset_less_insertD: "(A + {#x#} \<subset># B) \<Longrightarrow> (x \<in># B \<and> A \<subset># B)"
1.766    apply (rule conjI)
1.767     apply (simp add: mset_lessD)
1.768    apply (clarsimp simp: mset_le_def mset_less_def)
1.769    apply safe
1.770 -   apply (erule_tac x=a in allE)
1.771 +   apply (erule_tac x = a in allE)
1.772     apply (auto split: split_if_asm)
1.773    done
1.774
1.775 -lemma mset_le_insertD:
1.776 -  "(A + {#x#} \<subseteq># B) \<Longrightarrow> (x \<in># B \<and> A \<subseteq># B)"
1.777 +lemma mset_le_insertD: "(A + {#x#} \<subseteq># B) \<Longrightarrow> (x \<in># B \<and> A \<subseteq># B)"
1.778    apply (rule conjI)
1.779     apply (simp add: mset_leD)
1.780    apply (force simp: mset_le_def mset_less_def split: split_if_asm)
1.781    done
1.782
1.783  lemma mset_less_of_empty[simp]: "A \<subset># {#} = False"
1.784 -  by (induct A, auto simp: mset_le_def mset_less_def)
1.785 +  by (induct A) (auto simp: mset_le_def mset_less_def)
1.786
1.787  lemma multi_psub_of_add_self[simp]: "A \<subset># A + {#x#}"
1.788 -  by (clarsimp simp: mset_le_def mset_less_def)
1.789 +  by (auto simp: mset_le_def mset_less_def)
1.790
1.791  lemma multi_psub_self[simp]: "A \<subset># A = False"
1.792 -  by (clarsimp simp: mset_le_def mset_less_def)
1.793 +  by (auto simp: mset_le_def mset_less_def)
1.794
1.796    "T + {#x#} \<subset># S + {#x#} \<Longrightarrow> T \<subset># S"
1.797 -  by (clarsimp simp: mset_le_def mset_less_def)
1.798 +  by (auto simp: mset_le_def mset_less_def)
1.799
1.800  lemma mset_less_empty_nonempty: "({#} \<subset># S) = (S \<noteq> {#})"
1.801    by (auto simp: mset_le_def mset_less_def)
1.802 @@ -1140,21 +1160,21 @@
1.803  lemma mset_less_size: "A \<subset># B \<Longrightarrow> size A < size B"
1.804  proof (induct A arbitrary: B)
1.805    case (empty M)
1.806 -  hence "M \<noteq> {#}" by (simp add: mset_less_empty_nonempty)
1.807 +  then have "M \<noteq> {#}" by (simp add: mset_less_empty_nonempty)
1.808    then obtain M' x where "M = M' + {#x#}"
1.809      by (blast dest: multi_nonempty_split)
1.810 -  thus ?case by simp
1.811 +  then show ?case by simp
1.812  next
1.813    case (add S x T)
1.814    have IH: "\<And>B. S \<subset># B \<Longrightarrow> size S < size B" by fact
1.815    have SxsubT: "S + {#x#} \<subset># T" by fact
1.816 -  hence "x \<in># T" and "S \<subset># T" by (auto dest: mset_less_insertD)
1.817 +  then have "x \<in># T" and "S \<subset># T" by (auto dest: mset_less_insertD)
1.818    then obtain T' where T: "T = T' + {#x#}"
1.819      by (blast dest: multi_member_split)
1.820 -  hence "S \<subset># T'" using SxsubT
1.821 +  then have "S \<subset># T'" using SxsubT
1.822      by (blast intro: mset_less_add_bothsides)
1.823 -  hence "size S < size T'" using IH by simp
1.824 -  thus ?case using T by simp
1.825 +  then have "size S < size T'" using IH by simp
1.826 +  then show ?case using T by simp
1.827  qed
1.828
1.829  lemmas mset_less_trans = mset_order.less_eq_less.less_trans
1.830 @@ -1162,26 +1182,26 @@
1.831  lemma mset_less_diff_self: "c \<in># B \<Longrightarrow> B - {#c#} \<subset># B"
1.832    by (auto simp: mset_le_def mset_less_def multi_drop_mem_not_eq)
1.833
1.834 +
1.835  subsection {* Strong induction and subset induction for multisets *}
1.836
1.837  text {* Well-foundedness of proper subset operator: *}
1.838
1.839 +text {* proper multiset subset *}
1.840  definition
1.841 -  mset_less_rel  :: "('a multiset * 'a multiset) set"
1.842 -  where
1.843 -  --{* proper multiset subset *}
1.844 -  "mset_less_rel \<equiv> {(A,B). A \<subset># B}"
1.845 +  mset_less_rel :: "('a multiset * 'a multiset) set" where
1.846 +  "mset_less_rel = {(A,B). A \<subset># B}"
1.847
1.849 -  assumes cinB: "c \<in># B" and bnotc: "b \<noteq> c"
1.850 +  assumes "c \<in># B" and "b \<noteq> c"
1.851    shows "B - {#c#} + {#b#} = B + {#b#} - {#c#}"
1.852  proof -
1.853 -  from cinB obtain A where B: "B = A + {#c#}"
1.854 +  from `c \<in># B` obtain A where B: "B = A + {#c#}"
1.855      by (blast dest: multi_member_split)
1.856    have "A + {#b#} = A + {#b#} + {#c#} - {#c#}" by simp
1.857 -  hence "A + {#b#} = A + {#c#} + {#b#} - {#c#}"
1.858 +  then have "A + {#b#} = A + {#c#} + {#b#} - {#c#}"
1.859      by (simp add: union_ac)
1.860 -  thus ?thesis using B by simp
1.861 +  then show ?thesis using B by simp
1.862  qed
1.863
1.864  lemma wf_mset_less_rel: "wf mset_less_rel"
1.865 @@ -1215,7 +1235,7 @@
1.866      show "P (F + {#x#})"
1.867      proof (rule insert)
1.868        from i show "x \<in># A" by (auto dest: mset_le_insertD)
1.869 -      from i have "F \<subseteq># A" by (auto simp: mset_le_insertD)
1.870 +      from i have "F \<subseteq># A" by (auto dest: mset_le_insertD)
1.871        with P show "P F" .
1.872      qed
1.873    qed
1.874 @@ -1223,8 +1243,7 @@
1.875
1.876  text{* A consequence: Extensionality. *}
1.877
1.878 -lemma multi_count_eq:
1.879 -  "(\<forall>x. count A x = count B x) = (A = B)"
1.880 +lemma multi_count_eq: "(\<forall>x. count A x = count B x) = (A = B)"
1.881    apply (rule iffI)
1.882     prefer 2
1.883     apply clarsimp
1.884 @@ -1235,21 +1254,26 @@
1.885    apply simp
1.886    apply (case_tac "x \<in># C")
1.887     apply (force dest: multi_member_split)
1.888 -  apply (erule_tac x=x in allE)
1.889 +  apply (erule_tac x = x in allE)
1.890    apply simp
1.891    done
1.892
1.893  lemmas multi_count_ext = multi_count_eq [THEN iffD1, rule_format]
1.894
1.895 +
1.896  subsection {* The fold combinator *}
1.897
1.898 -text {* The intended behaviour is
1.899 -@{text "fold_mset f z {#x\<^isub>1, ..., x\<^isub>n#} = f x\<^isub>1 (\<dots> (f x\<^isub>n z)\<dots>)"}
1.900 -if @{text f} is associative-commutative.
1.901 +text {*
1.902 +  The intended behaviour is
1.903 +  @{text "fold_mset f z {#x\<^isub>1, ..., x\<^isub>n#} = f x\<^isub>1 (\<dots> (f x\<^isub>n z)\<dots>)"}
1.904 +  if @{text f} is associative-commutative.
1.905  *}
1.906
1.907 -(* the graph of fold_mset, z = the start element, f = folding function,
1.908 -   A the multiset, y the result *)
1.909 +text {*
1.910 +  The graph of @{text "fold_mset"}, @{text "z"}: the start element,
1.911 +  @{text "f"}: folding function, @{text "A"}: the multiset, @{text
1.912 +  "y"}: the result.
1.913 +*}
1.914  inductive
1.915    fold_msetG :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b \<Rightarrow> bool"
1.916    for f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b"
1.917 @@ -1262,31 +1286,33 @@
1.918  inductive_cases insert_fold_msetGE: "fold_msetG f z (A + {#}) y"
1.919
1.920  definition
1.921 -  fold_mset :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b"
1.922 -where
1.923 -  "fold_mset f z A \<equiv> THE x. fold_msetG f z A x"
1.924 +  fold_mset :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b" where
1.925 +  "fold_mset f z A = (THE x. fold_msetG f z A x)"
1.926
1.927  lemma Diff1_fold_msetG:
1.928 -  "\<lbrakk> fold_msetG f z (A - {#x#}) y; x \<in># A \<rbrakk> \<Longrightarrow> fold_msetG f z A (f x y)"
1.929 -  by (frule_tac x=x in fold_msetG.insertI, auto)
1.930 +  "fold_msetG f z (A - {#x#}) y \<Longrightarrow> x \<in># A \<Longrightarrow> fold_msetG f z A (f x y)"
1.931 +  apply (frule_tac x = x in fold_msetG.insertI)
1.932 +  apply auto
1.933 +  done
1.934
1.935  lemma fold_msetG_nonempty: "\<exists>x. fold_msetG f z A x"
1.936    apply (induct A)
1.937     apply blast
1.938    apply clarsimp
1.939 -  apply (drule_tac x=x in fold_msetG.insertI)
1.940 +  apply (drule_tac x = x in fold_msetG.insertI)
1.941    apply auto
1.942    done
1.943
1.944  lemma fold_mset_empty[simp]: "fold_mset f z {#} = z"
1.945 -  by (unfold fold_mset_def, blast)
1.946 +  unfolding fold_mset_def by blast
1.947
1.948  locale left_commutative =
1.949    fixes f :: "'a => 'b => 'b"
1.950    assumes left_commute: "f x (f y z) = f y (f x z)"
1.951 +begin
1.952
1.953 -lemma (in left_commutative) fold_msetG_determ:
1.954 -  "\<lbrakk>fold_msetG f z A x; fold_msetG f z A y\<rbrakk> \<Longrightarrow> y = x"
1.955 +lemma fold_msetG_determ:
1.956 +  "fold_msetG f z A x \<Longrightarrow> fold_msetG f z A y \<Longrightarrow> y = x"
1.957  proof (induct arbitrary: x y z rule: full_multiset_induct)
1.958    case (less M x\<^isub>1 x\<^isub>2 Z)
1.959    have IH: "\<forall>A. A \<subset># M \<longrightarrow>
1.960 @@ -1296,20 +1322,20 @@
1.961    show ?case
1.962    proof (rule fold_msetG.cases [OF Mfoldx\<^isub>1])
1.963      assume "M = {#}" and "x\<^isub>1 = Z"
1.964 -    thus ?case using Mfoldx\<^isub>2 by auto
1.965 +    then show ?case using Mfoldx\<^isub>2 by auto
1.966    next
1.967      fix B b u
1.968      assume "M = B + {#b#}" and "x\<^isub>1 = f b u" and Bu: "fold_msetG f Z B u"
1.969 -    hence MBb: "M = B + {#b#}" and x\<^isub>1: "x\<^isub>1 = f b u" by auto
1.970 +    then have MBb: "M = B + {#b#}" and x\<^isub>1: "x\<^isub>1 = f b u" by auto
1.971      show ?case
1.972      proof (rule fold_msetG.cases [OF Mfoldx\<^isub>2])
1.973        assume "M = {#}" "x\<^isub>2 = Z"
1.974 -      thus ?case using Mfoldx\<^isub>1 by auto
1.975 +      then show ?case using Mfoldx\<^isub>1 by auto
1.976      next
1.977        fix C c v
1.978        assume "M = C + {#c#}" and "x\<^isub>2 = f c v" and Cv: "fold_msetG f Z C v"
1.979 -      hence MCc: "M = C + {#c#}" and x\<^isub>2: "x\<^isub>2 = f c v" by auto
1.980 -      hence CsubM: "C \<subset># M" by simp
1.981 +      then have MCc: "M = C + {#c#}" and x\<^isub>2: "x\<^isub>2 = f c v" by auto
1.982 +      then have CsubM: "C \<subset># M" by simp
1.983        from MBb have BsubM: "B \<subset># M" by simp
1.984        show ?case
1.985        proof cases
1.986 @@ -1322,23 +1348,23 @@
1.987          have cinB: "c \<in># B" and binC: "b \<in># C" using MBb MCc diff
1.988            by (auto intro: insert_noteq_member dest: sym)
1.989          have "B - {#c#} \<subset># B" using cinB by (rule mset_less_diff_self)
1.990 -        hence DsubM: "?D \<subset># M" using BsubM by (blast intro: mset_less_trans)
1.991 +        then have DsubM: "?D \<subset># M" using BsubM by (blast intro: mset_less_trans)
1.992          from MBb MCc have "B + {#b#} = C + {#c#}" by blast
1.993 -        hence [simp]: "B + {#b#} - {#c#} = C"
1.994 +        then have [simp]: "B + {#b#} - {#c#} = C"
1.995            using MBb MCc binC cinB by auto
1.996          have B: "B = ?D + {#c#}" and C: "C = ?D + {#b#}"
1.997            using MBb MCc diff binC cinB
1.998            by (auto simp: multiset_add_sub_el_shuffle)
1.999          then obtain d where Dfoldd: "fold_msetG f Z ?D d"
1.1000            using fold_msetG_nonempty by iprover
1.1001 -        hence "fold_msetG f Z B (f c d)" using cinB
1.1002 +        then have "fold_msetG f Z B (f c d)" using cinB
1.1003            by (rule Diff1_fold_msetG)
1.1004 -        hence "f c d = u" using IH BsubM Bu by blast
1.1005 +        then have "f c d = u" using IH BsubM Bu by blast
1.1006          moreover
1.1007          have "fold_msetG f Z C (f b d)" using binC cinB diff Dfoldd
1.1008            by (auto simp: multiset_add_sub_el_shuffle
1.1009              dest: fold_msetG.insertI [where x=b])
1.1010 -        hence "f b d = v" using IH CsubM Cv by blast
1.1011 +        then have "f b d = v" using IH CsubM Cv by blast
1.1012          ultimately show ?thesis using x\<^isub>1 x\<^isub>2
1.1013            by (auto simp: left_commute)
1.1014        qed
1.1015 @@ -1346,8 +1372,8 @@
1.1016    qed
1.1017  qed
1.1018
1.1019 -lemma (in left_commutative) fold_mset_insert_aux: "
1.1020 -    (fold_msetG f z (A + {#x#}) v) =
1.1021 +lemma fold_mset_insert_aux:
1.1022 +  "(fold_msetG f z (A + {#x#}) v) =
1.1023      (\<exists>y. fold_msetG f z A y \<and> v = f x y)"
1.1024    apply (rule iffI)
1.1025     prefer 2
1.1026 @@ -1356,112 +1382,121 @@
1.1027    apply (blast intro: fold_msetG_determ)
1.1028    done
1.1029
1.1030 -lemma (in left_commutative) fold_mset_equality: "fold_msetG f z A y \<Longrightarrow> fold_mset f z A = y"
1.1031 -  by (unfold fold_mset_def) (blast intro: fold_msetG_determ)
1.1032 +lemma fold_mset_equality: "fold_msetG f z A y \<Longrightarrow> fold_mset f z A = y"
1.1033 +  unfolding fold_mset_def by (blast intro: fold_msetG_determ)
1.1034
1.1035 -lemma (in left_commutative) fold_mset_insert:
1.1036 -  "fold_mset f z (A + {#x#}) = f x (fold_mset f z A)"
1.1037 +lemma fold_mset_insert:
1.1038 +    "fold_mset f z (A + {#x#}) = f x (fold_mset f z A)"
1.1039    apply (simp add: fold_mset_def fold_mset_insert_aux union_commute)
1.1040    apply (rule the_equality)
1.1041 -  apply (auto cong add: conj_cong
1.1042 -              simp add: fold_mset_def [symmetric] fold_mset_equality fold_msetG_nonempty)
1.1043 +   apply (auto cong add: conj_cong
1.1044 +     simp add: fold_mset_def [symmetric] fold_mset_equality fold_msetG_nonempty)
1.1045    done
1.1046
1.1047 -lemma (in left_commutative) fold_mset_insert_idem:
1.1048 -  shows "fold_mset f z (A + {#a#}) = f a (fold_mset f z A)"
1.1049 +lemma fold_mset_insert_idem:
1.1050 +    "fold_mset f z (A + {#a#}) = f a (fold_mset f z A)"
1.1051    apply (simp add: fold_mset_def fold_mset_insert_aux)
1.1052    apply (rule the_equality)
1.1053 -  apply (auto cong add: conj_cong
1.1054 -              simp add: fold_mset_def [symmetric] fold_mset_equality fold_msetG_nonempty)
1.1055 +   apply (auto cong add: conj_cong
1.1056 +     simp add: fold_mset_def [symmetric] fold_mset_equality fold_msetG_nonempty)
1.1057    done
1.1058
1.1059 -lemma (in left_commutative) fold_mset_commute:
1.1060 -  "f x (fold_mset f z A) = fold_mset f (f x z) A"
1.1061 -  by (induct A, auto simp: fold_mset_insert left_commute [of x])
1.1062 +lemma fold_mset_commute: "f x (fold_mset f z A) = fold_mset f (f x z) A"
1.1063 +  by (induct A) (auto simp: fold_mset_insert left_commute [of x])
1.1064
1.1065 -lemma (in left_commutative) fold_mset_single [simp]:
1.1066 -   "fold_mset f z {#x#} = f x z"
1.1067 -using fold_mset_insert[of z "{#}"] by simp
1.1068 +lemma fold_mset_single [simp]: "fold_mset f z {#x#} = f x z"
1.1069 +  using fold_mset_insert [of z "{#}"] by simp
1.1070
1.1071 -lemma (in left_commutative) fold_mset_union [simp]:
1.1072 -   "fold_mset f z (A+B) = fold_mset f (fold_mset f z A) B"
1.1073 +lemma fold_mset_union [simp]:
1.1074 +  "fold_mset f z (A+B) = fold_mset f (fold_mset f z A) B"
1.1075  proof (induct A)
1.1076 -   case empty thus ?case by simp
1.1077 +  case empty then show ?case by simp
1.1078  next
1.1079 -   case (add A x)
1.1080 -   have "A + {#x#} + B = (A+B) + {#x#}" by(simp add:union_ac)
1.1081 -   hence "fold_mset f z (A + {#x#} + B) = f x (fold_mset f z (A + B))"
1.1082 -     by (simp add: fold_mset_insert)
1.1083 -   also have "\<dots> = fold_mset f (fold_mset f z (A + {#x#})) B"
1.1084 -     by (simp add: fold_mset_commute[of x,symmetric] add fold_mset_insert)
1.1085 -   finally show ?case .
1.1086 +  case (add A x)
1.1087 +  have "A + {#x#} + B = (A+B) + {#x#}" by(simp add:union_ac)
1.1088 +  then have "fold_mset f z (A + {#x#} + B) = f x (fold_mset f z (A + B))"
1.1089 +    by (simp add: fold_mset_insert)
1.1090 +  also have "\<dots> = fold_mset f (fold_mset f z (A + {#x#})) B"
1.1091 +    by (simp add: fold_mset_commute[of x,symmetric] add fold_mset_insert)
1.1092 +  finally show ?case .
1.1093  qed
1.1094
1.1095 -lemma (in left_commutative) fold_mset_fusion:
1.1096 +lemma fold_mset_fusion:
1.1097    includes left_commutative g
1.1098 -  shows "\<lbrakk>\<And>x y. h (g x y) = f x (h y) \<rbrakk> \<Longrightarrow> h (fold_mset g w A) = fold_mset f (h w) A"
1.1099 -  by (induct A, auto)
1.1100 +  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"
1.1101 +  by (induct A) auto
1.1102
1.1103 -lemma (in left_commutative) fold_mset_rec:
1.1104 -  assumes a: "a \<in># A"
1.1105 +lemma fold_mset_rec:
1.1106 +  assumes "a \<in># A"
1.1107    shows "fold_mset f z A = f a (fold_mset f z (A - {#a#}))"
1.1108  proof -
1.1109 -  from a obtain A' where "A = A' + {#a#}" by (blast dest: multi_member_split)
1.1110 -  thus ?thesis by simp
1.1111 +  from assms obtain A' where "A = A' + {#a#}"
1.1112 +    by (blast dest: multi_member_split)
1.1113 +  then show ?thesis by simp
1.1114  qed
1.1115
1.1116 -text{* A note on code generation: When defining some
1.1117 -function containing a subterm @{term"fold_mset F"}, code generation is
1.1118 -not automatic. When interpreting locale @{text left_commutative} with
1.1119 -@{text F}, the would be code thms for @{const fold_mset} become thms like
1.1120 -@{term"fold_mset F z {#} = z"} where @{text F} is not a pattern but contains
1.1121 -defined symbols, i.e.\ is not a code thm. Hence a separate constant with its
1.1122 -own code thms needs to be introduced for @{text F}. See the image operator
1.1123 -below. *}
1.1124 +end
1.1125 +
1.1126 +text {*
1.1127 +  A note on code generation: When defining some function containing a
1.1128 +  subterm @{term"fold_mset F"}, code generation is not automatic. When
1.1129 +  interpreting locale @{text left_commutative} with @{text F}, the
1.1130 +  would be code thms for @{const fold_mset} become thms like
1.1131 +  @{term"fold_mset F z {#} = z"} where @{text F} is not a pattern but
1.1132 +  contains defined symbols, i.e.\ is not a code thm. Hence a separate
1.1133 +  constant with its own code thms needs to be introduced for @{text
1.1134 +  F}. See the image operator below.
1.1135 +*}
1.1136 +
1.1137
1.1138  subsection {* Image *}
1.1139
1.1140  definition [code func del]: "image_mset f == fold_mset (op + o single o f) {#}"
1.1141
1.1142 -interpretation image_left_comm: left_commutative["op + o single o f"]
1.1144 +interpretation image_left_comm: left_commutative ["op + o single o f"]
1.1145 +  by (unfold_locales) (simp add:union_ac)
1.1146
1.1147 -lemma image_mset_empty[simp,code func]: "image_mset f {#} = {#}"
1.1149 +lemma image_mset_empty [simp, code func]: "image_mset f {#} = {#}"
1.1150 +  by (simp add: image_mset_def)
1.1151
1.1152 -lemma image_mset_single[simp,code func]: "image_mset f {#x#} = {#f x#}"
1.1154 +lemma image_mset_single [simp, code func]: "image_mset f {#x#} = {#f x#}"
1.1155 +  by (simp add: image_mset_def)
1.1156
1.1157  lemma image_mset_insert:
1.1158    "image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
1.1160 +  by (simp add: image_mset_def add_ac)
1.1161
1.1162  lemma image_mset_union[simp, code func]:
1.1163    "image_mset f (M+N) = image_mset f M + image_mset f N"
1.1164 -apply(induct N)
1.1165 - apply simp
1.1166 -apply(simp add:union_assoc[symmetric] image_mset_insert)
1.1167 -done
1.1168 +  apply (induct N)
1.1169 +   apply simp
1.1170 +  apply (simp add: union_assoc [symmetric] image_mset_insert)
1.1171 +  done
1.1172
1.1173 -lemma size_image_mset[simp]: "size(image_mset f M) = size M"
1.1174 -by(induct M) simp_all
1.1175 +lemma size_image_mset [simp]: "size (image_mset f M) = size M"
1.1176 +  by (induct M) simp_all
1.1177
1.1178 -lemma image_mset_is_empty_iff[simp]: "image_mset f M = {#} \<longleftrightarrow> M={#}"
1.1179 -by (cases M) auto
1.1180 +lemma image_mset_is_empty_iff [simp]: "image_mset f M = {#} \<longleftrightarrow> M = {#}"
1.1181 +  by (cases M) auto
1.1182
1.1183
1.1184 -syntax comprehension1_mset :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
1.1185 -       ("({#_/. _ :# _#})")
1.1186 -translations "{#e. x:#M#}" == "CONST image_mset (%x. e) M"
1.1187 +syntax
1.1188 +  comprehension1_mset :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
1.1189 +      ("({#_/. _ :# _#})")
1.1190 +translations
1.1191 +  "{#e. x:#M#}" == "CONST image_mset (%x. e) M"
1.1192
1.1193 -syntax comprehension2_mset :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
1.1194 -       ("({#_/ | _ :# _./ _#})")
1.1195 +syntax
1.1196 +  comprehension2_mset :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
1.1197 +      ("({#_/ | _ :# _./ _#})")
1.1198  translations
1.1199    "{#e | x:#M. P#}" => "{#e. x :# {# x:#M. P#}#}"
1.1200
1.1201 -text{* This allows to write not just filters like @{term"{#x:#M. x<c#}"}
1.1202 -but also images like @{term"{#x+x. x:#M #}"}
1.1203 -and @{term[source]"{#x+x|x:#M. x<c#}"}, where the latter is currently
1.1204 -displayed as @{term"{#x+x|x:#M. x<c#}"}. *}
1.1205 +text {*
1.1206 +  This allows to write not just filters like @{term "{#x:#M. x<c#}"}
1.1207 +  but also images like @{term "{#x+x. x:#M #}"} and @{term [source]
1.1208 +  "{#x+x|x:#M. x<c#}"}, where the latter is currently displayed as
1.1209 +  @{term "{#x+x|x:#M. x<c#}"}.
1.1210 +*}
1.1211
1.1212  end
```