tuned document;
authorwenzelm
Tue Feb 26 16:10:54 2008 +0100 (2008-02-26)
changeset 2614595670b6e1fa3
parent 26144 98d23fc02585
child 26146 61cb176d0385
tuned document;
tuned proofs;
src/HOL/Library/Multiset.thy
     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.214 -apply (simp add: add_is_1 one_is_add in_multiset expand_fun_eq)
   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.219 +  apply (simp add: add_is_1 one_is_add in_multiset expand_fun_eq)
   1.220 +  apply (blast dest: sym)
   1.221 +  done
   1.222  
   1.223  lemma add_eq_conv_diff:
   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.249  lemma add_eq_conv_ex:
   1.250    "(M + {#a#} = N + {#b#}) =
   1.251      (M = N \<and> a = b \<or> (\<exists>K. M = K + {#b#} \<and> N = K + {#a#}))"
   1.252 -by (auto simp add: add_eq_conv_diff)
   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.795  lemma mset_less_add_bothsides:
   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.848  lemma multiset_add_sub_el_shuffle: 
   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.1143 -by(unfold_locales)(simp add:union_ac)
  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.1148 -by(simp add:image_mset_def)
  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.1153 -by(simp add:image_mset_def)
  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.1159 -by(simp add:image_mset_def add_ac)
  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