1.1 --- a/src/HOL/Library/Multiset.thy Thu Feb 28 12:56:33 2008 +0100
1.2 +++ b/src/HOL/Library/Multiset.thy Thu Feb 28 14:04:29 2008 +0100
1.3 @@ -92,30 +92,30 @@
1.4 *}
1.5
1.6 lemma const0_in_multiset: "(\<lambda>a. 0) \<in> multiset"
1.7 - by (simp add: multiset_def)
1.8 +by (simp add: multiset_def)
1.9
1.10 lemma only1_in_multiset: "(\<lambda>b. if b = a then 1 else 0) \<in> multiset"
1.11 - by (simp add: multiset_def)
1.12 +by (simp add: multiset_def)
1.13
1.14 lemma union_preserves_multiset:
1.15 - "M \<in> multiset ==> N \<in> multiset ==> (\<lambda>a. M a + N a) \<in> multiset"
1.16 - apply (simp add: multiset_def)
1.17 - apply (drule (1) finite_UnI)
1.18 - apply (simp del: finite_Un add: Un_def)
1.19 - done
1.20 + "M \<in> multiset ==> N \<in> multiset ==> (\<lambda>a. M a + N a) \<in> multiset"
1.21 +apply (simp add: multiset_def)
1.22 +apply (drule (1) finite_UnI)
1.23 +apply (simp del: finite_Un add: Un_def)
1.24 +done
1.25
1.26 lemma diff_preserves_multiset:
1.27 - "M \<in> multiset ==> (\<lambda>a. M a - N a) \<in> multiset"
1.28 - apply (simp add: multiset_def)
1.29 - apply (rule finite_subset)
1.30 - apply auto
1.31 - done
1.32 + "M \<in> multiset ==> (\<lambda>a. M a - N a) \<in> multiset"
1.33 +apply (simp add: multiset_def)
1.34 +apply (rule finite_subset)
1.35 + apply auto
1.36 +done
1.37
1.38 lemma MCollect_preserves_multiset:
1.39 - "M \<in> multiset ==> (\<lambda>x. if P x then M x else 0) \<in> multiset"
1.40 - apply (simp add: multiset_def)
1.41 - apply (rule finite_subset, auto)
1.42 - done
1.43 + "M \<in> multiset ==> (\<lambda>x. if P x then M x else 0) \<in> multiset"
1.44 +apply (simp add: multiset_def)
1.45 +apply (rule finite_subset, auto)
1.46 +done
1.47
1.48 lemmas in_multiset = const0_in_multiset only1_in_multiset
1.49 union_preserves_multiset diff_preserves_multiset MCollect_preserves_multiset
1.50 @@ -126,22 +126,19 @@
1.51 subsubsection {* Union *}
1.52
1.53 lemma union_empty [simp]: "M + {#} = M \<and> {#} + M = M"
1.54 - by (simp add: union_def Mempty_def in_multiset)
1.55 +by (simp add: union_def Mempty_def in_multiset)
1.56
1.57 lemma union_commute: "M + N = N + (M::'a multiset)"
1.58 - by (simp add: union_def add_ac in_multiset)
1.59 +by (simp add: union_def add_ac in_multiset)
1.60
1.61 lemma union_assoc: "(M + N) + K = M + (N + (K::'a multiset))"
1.62 - by (simp add: union_def add_ac in_multiset)
1.63 +by (simp add: union_def add_ac in_multiset)
1.64
1.65 lemma union_lcomm: "M + (N + K) = N + (M + (K::'a multiset))"
1.66 proof -
1.67 - have "M + (N + K) = (N + K) + M"
1.68 - by (rule union_commute)
1.69 - also have "\<dots> = N + (K + M)"
1.70 - by (rule union_assoc)
1.71 - also have "K + M = M + K"
1.72 - by (rule union_commute)
1.73 + have "M + (N + K) = (N + K) + M" by (rule union_commute)
1.74 + also have "\<dots> = N + (K + M)" by (rule union_assoc)
1.75 + also have "K + M = M + K" by (rule union_commute)
1.76 finally show ?thesis .
1.77 qed
1.78
1.79 @@ -159,144 +156,143 @@
1.80 subsubsection {* Difference *}
1.81
1.82 lemma diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
1.83 - by (simp add: Mempty_def diff_def in_multiset)
1.84 +by (simp add: Mempty_def diff_def in_multiset)
1.85
1.86 lemma diff_union_inverse2 [simp]: "M + {#a#} - {#a#} = M"
1.87 - by (simp add: union_def diff_def in_multiset)
1.88 +by (simp add: union_def diff_def in_multiset)
1.89
1.90 lemma diff_cancel: "A - A = {#}"
1.91 - by (simp add: diff_def Mempty_def)
1.92 +by (simp add: diff_def Mempty_def)
1.93
1.94
1.95 subsubsection {* Count of elements *}
1.96
1.97 lemma count_empty [simp]: "count {#} a = 0"
1.98 - by (simp add: count_def Mempty_def in_multiset)
1.99 +by (simp add: count_def Mempty_def in_multiset)
1.100
1.101 lemma count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)"
1.102 - by (simp add: count_def single_def in_multiset)
1.103 +by (simp add: count_def single_def in_multiset)
1.104
1.105 lemma count_union [simp]: "count (M + N) a = count M a + count N a"
1.106 - by (simp add: count_def union_def in_multiset)
1.107 +by (simp add: count_def union_def in_multiset)
1.108
1.109 lemma count_diff [simp]: "count (M - N) a = count M a - count N a"
1.110 - by (simp add: count_def diff_def in_multiset)
1.111 +by (simp add: count_def diff_def in_multiset)
1.112
1.113 lemma count_MCollect [simp]:
1.114 - "count {# x:#M. P x #} a = (if P a then count M a else 0)"
1.115 - by (simp add: count_def MCollect_def in_multiset)
1.116 + "count {# x:#M. P x #} a = (if P a then count M a else 0)"
1.117 +by (simp add: count_def MCollect_def in_multiset)
1.118
1.119
1.120 subsubsection {* Set of elements *}
1.121
1.122 lemma set_of_empty [simp]: "set_of {#} = {}"
1.123 - by (simp add: set_of_def)
1.124 +by (simp add: set_of_def)
1.125
1.126 lemma set_of_single [simp]: "set_of {#b#} = {b}"
1.127 - by (simp add: set_of_def)
1.128 +by (simp add: set_of_def)
1.129
1.130 lemma set_of_union [simp]: "set_of (M + N) = set_of M \<union> set_of N"
1.131 - by (auto simp add: set_of_def)
1.132 +by (auto simp add: set_of_def)
1.133
1.134 lemma set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})"
1.135 - by (auto simp: set_of_def Mempty_def in_multiset count_def expand_fun_eq)
1.136 +by (auto simp: set_of_def Mempty_def in_multiset count_def expand_fun_eq)
1.137
1.138 lemma mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)"
1.139 - by (auto simp add: set_of_def)
1.140 +by (auto simp add: set_of_def)
1.141
1.142 lemma set_of_MCollect [simp]: "set_of {# x:#M. P x #} = set_of M \<inter> {x. P x}"
1.143 - by (auto simp add: set_of_def)
1.144 +by (auto simp add: set_of_def)
1.145
1.146
1.147 subsubsection {* Size *}
1.148
1.149 lemma size_empty [simp,code func]: "size {#} = 0"
1.150 - by (simp add: size_def)
1.151 +by (simp add: size_def)
1.152
1.153 lemma size_single [simp,code func]: "size {#b#} = 1"
1.154 - by (simp add: size_def)
1.155 +by (simp add: size_def)
1.156
1.157 lemma finite_set_of [iff]: "finite (set_of M)"
1.158 - using Rep_multiset [of M]
1.159 - by (simp add: multiset_def set_of_def count_def)
1.160 +using Rep_multiset [of M] by (simp add: multiset_def set_of_def count_def)
1.161
1.162 lemma setsum_count_Int:
1.163 - "finite A ==> setsum (count N) (A \<inter> set_of N) = setsum (count N) A"
1.164 - apply (induct rule: finite_induct)
1.165 - apply simp
1.166 - apply (simp add: Int_insert_left set_of_def)
1.167 - done
1.168 + "finite A ==> setsum (count N) (A \<inter> set_of N) = setsum (count N) A"
1.169 +apply (induct rule: finite_induct)
1.170 + apply simp
1.171 +apply (simp add: Int_insert_left set_of_def)
1.172 +done
1.173
1.174 lemma size_union[simp,code func]: "size (M + N::'a multiset) = size M + size N"
1.175 - apply (unfold size_def)
1.176 - apply (subgoal_tac "count (M + N) = (\<lambda>a. count M a + count N a)")
1.177 - prefer 2
1.178 - apply (rule ext, simp)
1.179 - apply (simp (no_asm_simp) add: setsum_Un_nat setsum_addf setsum_count_Int)
1.180 - apply (subst Int_commute)
1.181 - apply (simp (no_asm_simp) add: setsum_count_Int)
1.182 - done
1.183 +apply (unfold size_def)
1.184 +apply (subgoal_tac "count (M + N) = (\<lambda>a. count M a + count N a)")
1.185 + prefer 2
1.186 + apply (rule ext, simp)
1.187 +apply (simp (no_asm_simp) add: setsum_Un_nat setsum_addf setsum_count_Int)
1.188 +apply (subst Int_commute)
1.189 +apply (simp (no_asm_simp) add: setsum_count_Int)
1.190 +done
1.191
1.192 lemma size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})"
1.193 - apply (unfold size_def Mempty_def count_def, auto simp: in_multiset)
1.194 - apply (simp add: set_of_def count_def in_multiset expand_fun_eq)
1.195 - done
1.196 +apply (unfold size_def Mempty_def count_def, auto simp: in_multiset)
1.197 +apply (simp add: set_of_def count_def in_multiset expand_fun_eq)
1.198 +done
1.199
1.200 lemma nonempty_has_size: "(S \<noteq> {#}) = (0 < size S)"
1.201 - by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty)
1.202 +by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty)
1.203
1.204 lemma size_eq_Suc_imp_elem: "size M = Suc n ==> \<exists>a. a :# M"
1.205 - apply (unfold size_def)
1.206 - apply (drule setsum_SucD)
1.207 - apply auto
1.208 - done
1.209 +apply (unfold size_def)
1.210 +apply (drule setsum_SucD)
1.211 +apply auto
1.212 +done
1.213
1.214
1.215 subsubsection {* Equality of multisets *}
1.216
1.217 lemma multiset_eq_conv_count_eq: "(M = N) = (\<forall>a. count M a = count N a)"
1.218 - by (simp add: count_def expand_fun_eq)
1.219 +by (simp add: count_def expand_fun_eq)
1.220
1.221 lemma single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}"
1.222 - by (simp add: single_def Mempty_def in_multiset expand_fun_eq)
1.223 +by (simp add: single_def Mempty_def in_multiset expand_fun_eq)
1.224
1.225 lemma single_eq_single [simp]: "({#a#} = {#b#}) = (a = b)"
1.226 - by (auto simp add: single_def in_multiset expand_fun_eq)
1.227 +by (auto simp add: single_def in_multiset expand_fun_eq)
1.228
1.229 lemma union_eq_empty [iff]: "(M + N = {#}) = (M = {#} \<and> N = {#})"
1.230 - by (auto simp add: union_def Mempty_def in_multiset expand_fun_eq)
1.231 +by (auto simp add: union_def Mempty_def in_multiset expand_fun_eq)
1.232
1.233 lemma empty_eq_union [iff]: "({#} = M + N) = (M = {#} \<and> N = {#})"
1.234 - by (auto simp add: union_def Mempty_def in_multiset expand_fun_eq)
1.235 +by (auto simp add: union_def Mempty_def in_multiset expand_fun_eq)
1.236
1.237 lemma union_right_cancel [simp]: "(M + K = N + K) = (M = (N::'a multiset))"
1.238 - by (simp add: union_def in_multiset expand_fun_eq)
1.239 +by (simp add: union_def in_multiset expand_fun_eq)
1.240
1.241 lemma union_left_cancel [simp]: "(K + M = K + N) = (M = (N::'a multiset))"
1.242 - by (simp add: union_def in_multiset expand_fun_eq)
1.243 +by (simp add: union_def in_multiset expand_fun_eq)
1.244
1.245 lemma union_is_single:
1.246 - "(M + N = {#a#}) = (M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#})"
1.247 - apply (simp add: Mempty_def single_def union_def in_multiset add_is_1 expand_fun_eq)
1.248 - apply blast
1.249 - done
1.250 + "(M + N = {#a#}) = (M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#})"
1.251 +apply (simp add: Mempty_def single_def union_def in_multiset add_is_1 expand_fun_eq)
1.252 +apply blast
1.253 +done
1.254
1.255 lemma single_is_union:
1.256 - "({#a#} = M + N) \<longleftrightarrow> ({#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = N)"
1.257 - apply (unfold Mempty_def single_def union_def)
1.258 - apply (simp add: add_is_1 one_is_add in_multiset expand_fun_eq)
1.259 - apply (blast dest: sym)
1.260 - done
1.261 + "({#a#} = M + N) \<longleftrightarrow> ({#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = N)"
1.262 +apply (unfold Mempty_def single_def union_def)
1.263 +apply (simp add: add_is_1 one_is_add in_multiset expand_fun_eq)
1.264 +apply (blast dest: sym)
1.265 +done
1.266
1.267 lemma add_eq_conv_diff:
1.268 "(M + {#a#} = N + {#b#}) =
1.269 (M = N \<and> a = b \<or> M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#})"
1.270 - using [[simproc del: neq]]
1.271 - apply (unfold single_def union_def diff_def)
1.272 - apply (simp (no_asm) add: in_multiset expand_fun_eq)
1.273 - apply (rule conjI, force, safe, simp_all)
1.274 - apply (simp add: eq_sym_conv)
1.275 - done
1.276 +using [[simproc del: neq]]
1.277 +apply (unfold single_def union_def diff_def)
1.278 +apply (simp (no_asm) add: in_multiset expand_fun_eq)
1.279 +apply (rule conjI, force, safe, simp_all)
1.280 +apply (simp add: eq_sym_conv)
1.281 +done
1.282
1.283 declare Rep_multiset_inject [symmetric, simp del]
1.284
1.285 @@ -308,18 +304,18 @@
1.286
1.287 lemma insert_DiffM:
1.288 "x \<in># M \<Longrightarrow> {#x#} + (M - {#x#}) = M"
1.289 - by (clarsimp simp: multiset_eq_conv_count_eq)
1.290 +by (clarsimp simp: multiset_eq_conv_count_eq)
1.291
1.292 lemma insert_DiffM2[simp]:
1.293 "x \<in># M \<Longrightarrow> M - {#x#} + {#x#} = M"
1.294 - by (clarsimp simp: multiset_eq_conv_count_eq)
1.295 +by (clarsimp simp: multiset_eq_conv_count_eq)
1.296
1.297 lemma multi_union_self_other_eq:
1.298 "(A::'a multiset) + X = A + Y \<Longrightarrow> X = Y"
1.299 - by (induct A arbitrary: X Y) auto
1.300 +by (induct A arbitrary: X Y) auto
1.301
1.302 lemma multi_self_add_other_not_self[simp]: "(A = A + {#x#}) = False"
1.303 - by (metis single_not_empty union_empty union_left_cancel)
1.304 +by (metis single_not_empty union_empty union_left_cancel)
1.305
1.306 lemma insert_noteq_member:
1.307 assumes BC: "B + {#b#} = C + {#c#}"
1.308 @@ -336,30 +332,30 @@
1.309 lemma add_eq_conv_ex:
1.310 "(M + {#a#} = N + {#b#}) =
1.311 (M = N \<and> a = b \<or> (\<exists>K. M = K + {#b#} \<and> N = K + {#a#}))"
1.312 - by (auto simp add: add_eq_conv_diff)
1.313 +by (auto simp add: add_eq_conv_diff)
1.314
1.315
1.316 lemma empty_multiset_count:
1.317 "(\<forall>x. count A x = 0) = (A = {#})"
1.318 - by (metis count_empty multiset_eq_conv_count_eq)
1.319 +by (metis count_empty multiset_eq_conv_count_eq)
1.320
1.321
1.322 subsubsection {* Intersection *}
1.323
1.324 lemma multiset_inter_count:
1.325 - "count (A #\<inter> B) x = min (count A x) (count B x)"
1.326 - by (simp add: multiset_inter_def min_def)
1.327 + "count (A #\<inter> B) x = min (count A x) (count B x)"
1.328 +by (simp add: multiset_inter_def min_def)
1.329
1.330 lemma multiset_inter_commute: "A #\<inter> B = B #\<inter> A"
1.331 - by (simp add: multiset_eq_conv_count_eq multiset_inter_count
1.332 +by (simp add: multiset_eq_conv_count_eq multiset_inter_count
1.333 min_max.inf_commute)
1.334
1.335 lemma multiset_inter_assoc: "A #\<inter> (B #\<inter> C) = A #\<inter> B #\<inter> C"
1.336 - by (simp add: multiset_eq_conv_count_eq multiset_inter_count
1.337 +by (simp add: multiset_eq_conv_count_eq multiset_inter_count
1.338 min_max.inf_assoc)
1.339
1.340 lemma multiset_inter_left_commute: "A #\<inter> (B #\<inter> C) = B #\<inter> (A #\<inter> C)"
1.341 - by (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def)
1.342 +by (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def)
1.343
1.344 lemmas multiset_inter_ac =
1.345 multiset_inter_commute
1.346 @@ -367,31 +363,31 @@
1.347 multiset_inter_left_commute
1.348
1.349 lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
1.350 - by (simp add: multiset_eq_conv_count_eq multiset_inter_count)
1.351 +by (simp add: multiset_eq_conv_count_eq multiset_inter_count)
1.352
1.353 lemma multiset_union_diff_commute: "B #\<inter> C = {#} \<Longrightarrow> A + B - C = A - C + B"
1.354 - apply (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def
1.355 +apply (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def
1.356 split: split_if_asm)
1.357 - apply clarsimp
1.358 - apply (erule_tac x = a in allE)
1.359 - apply auto
1.360 - done
1.361 +apply clarsimp
1.362 +apply (erule_tac x = a in allE)
1.363 +apply auto
1.364 +done
1.365
1.366
1.367 subsubsection {* Comprehension (filter) *}
1.368
1.369 lemma MCollect_empty[simp, code func]: "MCollect {#} P = {#}"
1.370 - by (simp add: MCollect_def Mempty_def Abs_multiset_inject
1.371 +by (simp add: MCollect_def Mempty_def Abs_multiset_inject
1.372 in_multiset expand_fun_eq)
1.373
1.374 lemma MCollect_single[simp, code func]:
1.375 - "MCollect {#x#} P = (if P x then {#x#} else {#})"
1.376 - by (simp add: MCollect_def Mempty_def single_def Abs_multiset_inject
1.377 + "MCollect {#x#} P = (if P x then {#x#} else {#})"
1.378 +by (simp add: MCollect_def Mempty_def single_def Abs_multiset_inject
1.379 in_multiset expand_fun_eq)
1.380
1.381 lemma MCollect_union[simp, code func]:
1.382 "MCollect (M+N) f = MCollect M f + MCollect N f"
1.383 - by (simp add: MCollect_def union_def Abs_multiset_inject
1.384 +by (simp add: MCollect_def union_def Abs_multiset_inject
1.385 in_multiset expand_fun_eq)
1.386
1.387
1.388 @@ -400,55 +396,55 @@
1.389 lemma setsum_decr:
1.390 "finite F ==> (0::nat) < f a ==>
1.391 setsum (f (a := f a - 1)) F = (if a\<in>F then setsum f F - 1 else setsum f F)"
1.392 - apply (induct rule: finite_induct)
1.393 - apply auto
1.394 - apply (drule_tac a = a in mk_disjoint_insert, auto)
1.395 - done
1.396 +apply (induct rule: finite_induct)
1.397 + apply auto
1.398 +apply (drule_tac a = a in mk_disjoint_insert, auto)
1.399 +done
1.400
1.401 lemma rep_multiset_induct_aux:
1.402 - assumes 1: "P (\<lambda>a. (0::nat))"
1.403 - and 2: "!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))"
1.404 - shows "\<forall>f. f \<in> multiset --> setsum f {x. f x \<noteq> 0} = n --> P f"
1.405 - apply (unfold multiset_def)
1.406 - apply (induct_tac n, simp, clarify)
1.407 - apply (subgoal_tac "f = (\<lambda>a.0)")
1.408 - apply simp
1.409 - apply (rule 1)
1.410 - apply (rule ext, force, clarify)
1.411 - apply (frule setsum_SucD, clarify)
1.412 - apply (rename_tac a)
1.413 - apply (subgoal_tac "finite {x. (f (a := f a - 1)) x > 0}")
1.414 - prefer 2
1.415 - apply (rule finite_subset)
1.416 - prefer 2
1.417 - apply assumption
1.418 - apply simp
1.419 - apply blast
1.420 - apply (subgoal_tac "f = (f (a := f a - 1))(a := (f (a := f a - 1)) a + 1)")
1.421 - prefer 2
1.422 - apply (rule ext)
1.423 - apply (simp (no_asm_simp))
1.424 - apply (erule ssubst, rule 2 [unfolded multiset_def], blast)
1.425 - apply (erule allE, erule impE, erule_tac [2] mp, blast)
1.426 - apply (simp (no_asm_simp) add: setsum_decr del: fun_upd_apply One_nat_def)
1.427 - apply (subgoal_tac "{x. x \<noteq> a --> f x \<noteq> 0} = {x. f x \<noteq> 0}")
1.428 - prefer 2
1.429 - apply blast
1.430 - apply (subgoal_tac "{x. x \<noteq> a \<and> f x \<noteq> 0} = {x. f x \<noteq> 0} - {a}")
1.431 - prefer 2
1.432 - apply blast
1.433 - apply (simp add: le_imp_diff_is_add setsum_diff1_nat cong: conj_cong)
1.434 - done
1.435 +assumes 1: "P (\<lambda>a. (0::nat))"
1.436 + and 2: "!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))"
1.437 +shows "\<forall>f. f \<in> multiset --> setsum f {x. f x \<noteq> 0} = n --> P f"
1.438 +apply (unfold multiset_def)
1.439 +apply (induct_tac n, simp, clarify)
1.440 + apply (subgoal_tac "f = (\<lambda>a.0)")
1.441 + apply simp
1.442 + apply (rule 1)
1.443 + apply (rule ext, force, clarify)
1.444 +apply (frule setsum_SucD, clarify)
1.445 +apply (rename_tac a)
1.446 +apply (subgoal_tac "finite {x. (f (a := f a - 1)) x > 0}")
1.447 + prefer 2
1.448 + apply (rule finite_subset)
1.449 + prefer 2
1.450 + apply assumption
1.451 + apply simp
1.452 + apply blast
1.453 +apply (subgoal_tac "f = (f (a := f a - 1))(a := (f (a := f a - 1)) a + 1)")
1.454 + prefer 2
1.455 + apply (rule ext)
1.456 + apply (simp (no_asm_simp))
1.457 + apply (erule ssubst, rule 2 [unfolded multiset_def], blast)
1.458 +apply (erule allE, erule impE, erule_tac [2] mp, blast)
1.459 +apply (simp (no_asm_simp) add: setsum_decr del: fun_upd_apply One_nat_def)
1.460 +apply (subgoal_tac "{x. x \<noteq> a --> f x \<noteq> 0} = {x. f x \<noteq> 0}")
1.461 + prefer 2
1.462 + apply blast
1.463 +apply (subgoal_tac "{x. x \<noteq> a \<and> f x \<noteq> 0} = {x. f x \<noteq> 0} - {a}")
1.464 + prefer 2
1.465 + apply blast
1.466 +apply (simp add: le_imp_diff_is_add setsum_diff1_nat cong: conj_cong)
1.467 +done
1.468
1.469 theorem rep_multiset_induct:
1.470 "f \<in> multiset ==> P (\<lambda>a. 0) ==>
1.471 (!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))) ==> P f"
1.472 - using rep_multiset_induct_aux by blast
1.473 +using rep_multiset_induct_aux by blast
1.474
1.475 theorem multiset_induct [case_names empty add, induct type: multiset]:
1.476 - assumes empty: "P {#}"
1.477 - and add: "!!M x. P M ==> P (M + {#x#})"
1.478 - shows "P M"
1.479 +assumes empty: "P {#}"
1.480 + and add: "!!M x. P M ==> P (M + {#x#})"
1.481 +shows "P M"
1.482 proof -
1.483 note defns = union_def single_def Mempty_def
1.484 show ?thesis
1.485 @@ -466,12 +462,12 @@
1.486 qed
1.487
1.488 lemma multi_nonempty_split: "M \<noteq> {#} \<Longrightarrow> \<exists>A a. M = A + {#a#}"
1.489 - by (induct M) auto
1.490 +by (induct M) auto
1.491
1.492 lemma multiset_cases [cases type, case_names empty add]:
1.493 - assumes em: "M = {#} \<Longrightarrow> P"
1.494 - assumes add: "\<And>N x. M = N + {#x#} \<Longrightarrow> P"
1.495 - shows "P"
1.496 +assumes em: "M = {#} \<Longrightarrow> P"
1.497 +assumes add: "\<And>N x. M = N + {#x#} \<Longrightarrow> P"
1.498 +shows "P"
1.499 proof (cases "M = {#}")
1.500 assume "M = {#}" then show ?thesis using em by simp
1.501 next
1.502 @@ -482,20 +478,20 @@
1.503 qed
1.504
1.505 lemma multi_member_split: "x \<in># M \<Longrightarrow> \<exists>A. M = A + {#x#}"
1.506 - apply (cases M)
1.507 - apply simp
1.508 - apply (rule_tac x="M - {#x#}" in exI, simp)
1.509 - done
1.510 +apply (cases M)
1.511 + apply simp
1.512 +apply (rule_tac x="M - {#x#}" in exI, simp)
1.513 +done
1.514
1.515 lemma multiset_partition: "M = {# x:#M. P x #} + {# x:#M. \<not> P x #}"
1.516 - apply (subst multiset_eq_conv_count_eq)
1.517 - apply auto
1.518 - done
1.519 +apply (subst multiset_eq_conv_count_eq)
1.520 +apply auto
1.521 +done
1.522
1.523 declare multiset_typedef [simp del]
1.524
1.525 lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B - {#c#} \<noteq> B"
1.526 - by (cases "B = {#}") (auto dest: multi_member_split)
1.527 +by (cases "B = {#}") (auto dest: multi_member_split)
1.528
1.529
1.530 subsection {* Orderings *}
1.531 @@ -513,7 +509,7 @@
1.532 "mult r = (mult1 r)\<^sup>+"
1.533
1.534 lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
1.535 - by (simp add: mult1_def)
1.536 +by (simp add: mult1_def)
1.537
1.538 lemma less_add: "(N, M0 + {#a#}) \<in> mult1 r ==>
1.539 (\<exists>M. (M, M0) \<in> mult1 r \<and> N = M + {#a#}) \<or>
1.540 @@ -622,10 +618,10 @@
1.541 qed
1.542
1.543 theorem wf_mult1: "wf r ==> wf (mult1 r)"
1.544 - by (rule acc_wfI) (rule all_accessible)
1.545 +by (rule acc_wfI) (rule all_accessible)
1.546
1.547 theorem wf_mult: "wf r ==> wf (mult r)"
1.548 - unfolding mult_def by (rule wf_trancl) (rule wf_mult1)
1.549 +unfolding mult_def by (rule wf_trancl) (rule wf_mult1)
1.550
1.551
1.552 subsubsection {* Closure-free presentation *}
1.553 @@ -633,7 +629,7 @@
1.554 (*Badly needed: a linear arithmetic procedure for multisets*)
1.555
1.556 lemma diff_union_single_conv: "a :# J ==> I + J - {#a#} = I + (J - {#a#})"
1.557 - by (simp add: multiset_eq_conv_count_eq)
1.558 +by (simp add: multiset_eq_conv_count_eq)
1.559
1.560 text {* One direction. *}
1.561
1.562 @@ -641,77 +637,77 @@
1.563 "trans r ==> (M, N) \<in> mult r ==>
1.564 \<exists>I J K. N = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and>
1.565 (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r)"
1.566 - apply (unfold mult_def mult1_def set_of_def)
1.567 - apply (erule converse_trancl_induct, clarify)
1.568 - apply (rule_tac x = M0 in exI, simp, clarify)
1.569 - apply (case_tac "a :# K")
1.570 - apply (rule_tac x = I in exI)
1.571 - apply (simp (no_asm))
1.572 - apply (rule_tac x = "(K - {#a#}) + Ka" in exI)
1.573 - apply (simp (no_asm_simp) add: union_assoc [symmetric])
1.574 - apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong)
1.575 - apply (simp add: diff_union_single_conv)
1.576 - apply (simp (no_asm_use) add: trans_def)
1.577 - apply blast
1.578 - apply (subgoal_tac "a :# I")
1.579 - apply (rule_tac x = "I - {#a#}" in exI)
1.580 - apply (rule_tac x = "J + {#a#}" in exI)
1.581 - apply (rule_tac x = "K + Ka" in exI)
1.582 - apply (rule conjI)
1.583 - apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split)
1.584 - apply (rule conjI)
1.585 - apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong, simp)
1.586 - apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split)
1.587 - apply (simp (no_asm_use) add: trans_def)
1.588 - apply blast
1.589 - apply (subgoal_tac "a :# (M0 + {#a#})")
1.590 - apply simp
1.591 - apply (simp (no_asm))
1.592 - done
1.593 +apply (unfold mult_def mult1_def set_of_def)
1.594 +apply (erule converse_trancl_induct, clarify)
1.595 + apply (rule_tac x = M0 in exI, simp, clarify)
1.596 +apply (case_tac "a :# K")
1.597 + apply (rule_tac x = I in exI)
1.598 + apply (simp (no_asm))
1.599 + apply (rule_tac x = "(K - {#a#}) + Ka" in exI)
1.600 + apply (simp (no_asm_simp) add: union_assoc [symmetric])
1.601 + apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong)
1.602 + apply (simp add: diff_union_single_conv)
1.603 + apply (simp (no_asm_use) add: trans_def)
1.604 + apply blast
1.605 +apply (subgoal_tac "a :# I")
1.606 + apply (rule_tac x = "I - {#a#}" in exI)
1.607 + apply (rule_tac x = "J + {#a#}" in exI)
1.608 + apply (rule_tac x = "K + Ka" in exI)
1.609 + apply (rule conjI)
1.610 + apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split)
1.611 + apply (rule conjI)
1.612 + apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong, simp)
1.613 + apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split)
1.614 + apply (simp (no_asm_use) add: trans_def)
1.615 + apply blast
1.616 +apply (subgoal_tac "a :# (M0 + {#a#})")
1.617 + apply simp
1.618 +apply (simp (no_asm))
1.619 +done
1.620
1.621 lemma elem_imp_eq_diff_union: "a :# M ==> M = M - {#a#} + {#a#}"
1.622 - by (simp add: multiset_eq_conv_count_eq)
1.623 +by (simp add: multiset_eq_conv_count_eq)
1.624
1.625 lemma size_eq_Suc_imp_eq_union: "size M = Suc n ==> \<exists>a N. M = N + {#a#}"
1.626 - apply (erule size_eq_Suc_imp_elem [THEN exE])
1.627 - apply (drule elem_imp_eq_diff_union, auto)
1.628 - done
1.629 +apply (erule size_eq_Suc_imp_elem [THEN exE])
1.630 +apply (drule elem_imp_eq_diff_union, auto)
1.631 +done
1.632
1.633 lemma one_step_implies_mult_aux:
1.634 "trans r ==>
1.635 \<forall>I J K. (size J = n \<and> J \<noteq> {#} \<and> (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r))
1.636 --> (I + K, I + J) \<in> mult r"
1.637 - apply (induct_tac n, auto)
1.638 - apply (frule size_eq_Suc_imp_eq_union, clarify)
1.639 - apply (rename_tac "J'", simp)
1.640 - apply (erule notE, auto)
1.641 - apply (case_tac "J' = {#}")
1.642 - apply (simp add: mult_def)
1.643 - apply (rule r_into_trancl)
1.644 - apply (simp add: mult1_def set_of_def, blast)
1.645 - txt {* Now we know @{term "J' \<noteq> {#}"}. *}
1.646 - apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition)
1.647 - apply (erule_tac P = "\<forall>k \<in> set_of K. ?P k" in rev_mp)
1.648 - apply (erule ssubst)
1.649 - apply (simp add: Ball_def, auto)
1.650 - apply (subgoal_tac
1.651 - "((I + {# x :# K. (x, a) \<in> r #}) + {# x :# K. (x, a) \<notin> r #},
1.652 - (I + {# x :# K. (x, a) \<in> r #}) + J') \<in> mult r")
1.653 - prefer 2
1.654 - apply force
1.655 - apply (simp (no_asm_use) add: union_assoc [symmetric] mult_def)
1.656 - apply (erule trancl_trans)
1.657 - apply (rule r_into_trancl)
1.658 - apply (simp add: mult1_def set_of_def)
1.659 - apply (rule_tac x = a in exI)
1.660 - apply (rule_tac x = "I + J'" in exI)
1.661 - apply (simp add: union_ac)
1.662 - done
1.663 +apply (induct_tac n, auto)
1.664 +apply (frule size_eq_Suc_imp_eq_union, clarify)
1.665 +apply (rename_tac "J'", simp)
1.666 +apply (erule notE, auto)
1.667 +apply (case_tac "J' = {#}")
1.668 + apply (simp add: mult_def)
1.669 + apply (rule r_into_trancl)
1.670 + apply (simp add: mult1_def set_of_def, blast)
1.671 +txt {* Now we know @{term "J' \<noteq> {#}"}. *}
1.672 +apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition)
1.673 +apply (erule_tac P = "\<forall>k \<in> set_of K. ?P k" in rev_mp)
1.674 +apply (erule ssubst)
1.675 +apply (simp add: Ball_def, auto)
1.676 +apply (subgoal_tac
1.677 + "((I + {# x :# K. (x, a) \<in> r #}) + {# x :# K. (x, a) \<notin> r #},
1.678 + (I + {# x :# K. (x, a) \<in> r #}) + J') \<in> mult r")
1.679 + prefer 2
1.680 + apply force
1.681 +apply (simp (no_asm_use) add: union_assoc [symmetric] mult_def)
1.682 +apply (erule trancl_trans)
1.683 +apply (rule r_into_trancl)
1.684 +apply (simp add: mult1_def set_of_def)
1.685 +apply (rule_tac x = a in exI)
1.686 +apply (rule_tac x = "I + J'" in exI)
1.687 +apply (simp add: union_ac)
1.688 +done
1.689
1.690 lemma one_step_implies_mult:
1.691 "trans r ==> J \<noteq> {#} ==> \<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r
1.692 ==> (I + K, I + J) \<in> mult r"
1.693 - using one_step_implies_mult_aux by blast
1.694 +using one_step_implies_mult_aux by blast
1.695
1.696
1.697 subsubsection {* Partial-order properties *}
1.698 @@ -723,116 +719,116 @@
1.699 le_multiset_def: "M' <= M == M' = M \<or> M' < (M::'a multiset)"
1.700
1.701 lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}"
1.702 - unfolding trans_def by (blast intro: order_less_trans)
1.703 +unfolding trans_def by (blast intro: order_less_trans)
1.704
1.705 text {*
1.706 \medskip Irreflexivity.
1.707 *}
1.708
1.709 lemma mult_irrefl_aux:
1.710 - "finite A ==> (\<forall>x \<in> A. \<exists>y \<in> A. x < (y::'a::order)) \<Longrightarrow> A = {}"
1.711 - by (induct rule: finite_induct) (auto intro: order_less_trans)
1.712 + "finite A ==> (\<forall>x \<in> A. \<exists>y \<in> A. x < (y::'a::order)) \<Longrightarrow> A = {}"
1.713 +by (induct rule: finite_induct) (auto intro: order_less_trans)
1.714
1.715 lemma mult_less_not_refl: "\<not> M < (M::'a::order multiset)"
1.716 - apply (unfold less_multiset_def, auto)
1.717 - apply (drule trans_base_order [THEN mult_implies_one_step], auto)
1.718 - apply (drule finite_set_of [THEN mult_irrefl_aux [rule_format (no_asm)]])
1.719 - apply (simp add: set_of_eq_empty_iff)
1.720 - done
1.721 +apply (unfold less_multiset_def, auto)
1.722 +apply (drule trans_base_order [THEN mult_implies_one_step], auto)
1.723 +apply (drule finite_set_of [THEN mult_irrefl_aux [rule_format (no_asm)]])
1.724 +apply (simp add: set_of_eq_empty_iff)
1.725 +done
1.726
1.727 lemma mult_less_irrefl [elim!]: "M < (M::'a::order multiset) ==> R"
1.728 - using insert mult_less_not_refl by fast
1.729 +using insert mult_less_not_refl by fast
1.730
1.731
1.732 text {* Transitivity. *}
1.733
1.734 theorem mult_less_trans: "K < M ==> M < N ==> K < (N::'a::order multiset)"
1.735 - unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
1.736 +unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
1.737
1.738 text {* Asymmetry. *}
1.739
1.740 theorem mult_less_not_sym: "M < N ==> \<not> N < (M::'a::order multiset)"
1.741 - apply auto
1.742 - apply (rule mult_less_not_refl [THEN notE])
1.743 - apply (erule mult_less_trans, assumption)
1.744 - done
1.745 +apply auto
1.746 +apply (rule mult_less_not_refl [THEN notE])
1.747 +apply (erule mult_less_trans, assumption)
1.748 +done
1.749
1.750 theorem mult_less_asym:
1.751 - "M < N ==> (\<not> P ==> N < (M::'a::order multiset)) ==> P"
1.752 - using mult_less_not_sym by blast
1.753 + "M < N ==> (\<not> P ==> N < (M::'a::order multiset)) ==> P"
1.754 +using mult_less_not_sym by blast
1.755
1.756 theorem mult_le_refl [iff]: "M <= (M::'a::order multiset)"
1.757 - unfolding le_multiset_def by auto
1.758 +unfolding le_multiset_def by auto
1.759
1.760 text {* Anti-symmetry. *}
1.761
1.762 theorem mult_le_antisym:
1.763 - "M <= N ==> N <= M ==> M = (N::'a::order multiset)"
1.764 - unfolding le_multiset_def by (blast dest: mult_less_not_sym)
1.765 + "M <= N ==> N <= M ==> M = (N::'a::order multiset)"
1.766 +unfolding le_multiset_def by (blast dest: mult_less_not_sym)
1.767
1.768 text {* Transitivity. *}
1.769
1.770 theorem mult_le_trans:
1.771 - "K <= M ==> M <= N ==> K <= (N::'a::order multiset)"
1.772 - unfolding le_multiset_def by (blast intro: mult_less_trans)
1.773 + "K <= M ==> M <= N ==> K <= (N::'a::order multiset)"
1.774 +unfolding le_multiset_def by (blast intro: mult_less_trans)
1.775
1.776 theorem mult_less_le: "(M < N) = (M <= N \<and> M \<noteq> (N::'a::order multiset))"
1.777 - unfolding le_multiset_def by auto
1.778 +unfolding le_multiset_def by auto
1.779
1.780 text {* Partial order. *}
1.781
1.782 instance multiset :: (order) order
1.783 - apply intro_classes
1.784 - apply (rule mult_less_le)
1.785 - apply (rule mult_le_refl)
1.786 - apply (erule mult_le_trans, assumption)
1.787 - apply (erule mult_le_antisym, assumption)
1.788 - done
1.789 +apply intro_classes
1.790 + apply (rule mult_less_le)
1.791 + apply (rule mult_le_refl)
1.792 + apply (erule mult_le_trans, assumption)
1.793 +apply (erule mult_le_antisym, assumption)
1.794 +done
1.795
1.796
1.797 subsubsection {* Monotonicity of multiset union *}
1.798
1.799 lemma mult1_union:
1.800 - "(B, D) \<in> mult1 r ==> trans r ==> (C + B, C + D) \<in> mult1 r"
1.801 - apply (unfold mult1_def)
1.802 - apply auto
1.803 - apply (rule_tac x = a in exI)
1.804 - apply (rule_tac x = "C + M0" in exI)
1.805 - apply (simp add: union_assoc)
1.806 - done
1.807 + "(B, D) \<in> mult1 r ==> trans r ==> (C + B, C + D) \<in> mult1 r"
1.808 +apply (unfold mult1_def)
1.809 +apply auto
1.810 +apply (rule_tac x = a in exI)
1.811 +apply (rule_tac x = "C + M0" in exI)
1.812 +apply (simp add: union_assoc)
1.813 +done
1.814
1.815 lemma union_less_mono2: "B < D ==> C + B < C + (D::'a::order multiset)"
1.816 - apply (unfold less_multiset_def mult_def)
1.817 - apply (erule trancl_induct)
1.818 - apply (blast intro: mult1_union transI order_less_trans r_into_trancl)
1.819 - apply (blast intro: mult1_union transI order_less_trans r_into_trancl trancl_trans)
1.820 - done
1.821 +apply (unfold less_multiset_def mult_def)
1.822 +apply (erule trancl_induct)
1.823 + apply (blast intro: mult1_union transI order_less_trans r_into_trancl)
1.824 +apply (blast intro: mult1_union transI order_less_trans r_into_trancl trancl_trans)
1.825 +done
1.826
1.827 lemma union_less_mono1: "B < D ==> B + C < D + (C::'a::order multiset)"
1.828 - apply (subst union_commute [of B C])
1.829 - apply (subst union_commute [of D C])
1.830 - apply (erule union_less_mono2)
1.831 - done
1.832 +apply (subst union_commute [of B C])
1.833 +apply (subst union_commute [of D C])
1.834 +apply (erule union_less_mono2)
1.835 +done
1.836
1.837 lemma union_less_mono:
1.838 - "A < C ==> B < D ==> A + B < C + (D::'a::order multiset)"
1.839 - by (blast intro!: union_less_mono1 union_less_mono2 mult_less_trans)
1.840 + "A < C ==> B < D ==> A + B < C + (D::'a::order multiset)"
1.841 +by (blast intro!: union_less_mono1 union_less_mono2 mult_less_trans)
1.842
1.843 lemma union_le_mono:
1.844 - "A <= C ==> B <= D ==> A + B <= C + (D::'a::order multiset)"
1.845 - unfolding le_multiset_def
1.846 - by (blast intro: union_less_mono union_less_mono1 union_less_mono2)
1.847 + "A <= C ==> B <= D ==> A + B <= C + (D::'a::order multiset)"
1.848 +unfolding le_multiset_def
1.849 +by (blast intro: union_less_mono union_less_mono1 union_less_mono2)
1.850
1.851 lemma empty_leI [iff]: "{#} <= (M::'a::order multiset)"
1.852 - apply (unfold le_multiset_def less_multiset_def)
1.853 - apply (case_tac "M = {#}")
1.854 - prefer 2
1.855 - apply (subgoal_tac "({#} + {#}, {#} + M) \<in> mult (Collect (split op <))")
1.856 - prefer 2
1.857 - apply (rule one_step_implies_mult)
1.858 - apply (simp only: trans_def)
1.859 - apply auto
1.860 - done
1.861 +apply (unfold le_multiset_def less_multiset_def)
1.862 +apply (case_tac "M = {#}")
1.863 + prefer 2
1.864 + apply (subgoal_tac "({#} + {#}, {#} + M) \<in> mult (Collect (split op <))")
1.865 + prefer 2
1.866 + apply (rule one_step_implies_mult)
1.867 + apply (simp only: trans_def)
1.868 + apply auto
1.869 +done
1.870
1.871 lemma union_upper1: "A <= A + (B::'a::order multiset)"
1.872 proof -
1.873 @@ -841,12 +837,12 @@
1.874 qed
1.875
1.876 lemma union_upper2: "B <= A + (B::'a::order multiset)"
1.877 - by (subst union_commute) (rule union_upper1)
1.878 +by (subst union_commute) (rule union_upper1)
1.879
1.880 instance multiset :: (order) pordered_ab_semigroup_add
1.881 - apply intro_classes
1.882 - apply (erule union_le_mono[OF mult_le_refl])
1.883 - done
1.884 +apply intro_classes
1.885 +apply (erule union_le_mono[OF mult_le_refl])
1.886 +done
1.887
1.888
1.889 subsection {* Link with lists *}
1.890 @@ -856,82 +852,82 @@
1.891 "multiset_of (a # x) = multiset_of x + {# a #}"
1.892
1.893 lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])"
1.894 - by (induct x) auto
1.895 +by (induct x) auto
1.896
1.897 lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])"
1.898 - by (induct x) auto
1.899 +by (induct x) auto
1.900
1.901 lemma set_of_multiset_of[simp]: "set_of(multiset_of x) = set x"
1.902 - by (induct x) auto
1.903 +by (induct x) auto
1.904
1.905 lemma mem_set_multiset_eq: "x \<in> set xs = (x :# multiset_of xs)"
1.906 - by (induct xs) auto
1.907 +by (induct xs) auto
1.908
1.909 lemma multiset_of_append [simp]:
1.910 - "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
1.911 - by (induct xs arbitrary: ys) (auto simp: union_ac)
1.912 + "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
1.913 +by (induct xs arbitrary: ys) (auto simp: union_ac)
1.914
1.915 lemma surj_multiset_of: "surj multiset_of"
1.916 - apply (unfold surj_def)
1.917 - apply (rule allI)
1.918 - apply (rule_tac M = y in multiset_induct)
1.919 - apply auto
1.920 - apply (rule_tac x = "x # xa" in exI)
1.921 - apply auto
1.922 - done
1.923 +apply (unfold surj_def)
1.924 +apply (rule allI)
1.925 +apply (rule_tac M = y in multiset_induct)
1.926 + apply auto
1.927 +apply (rule_tac x = "x # xa" in exI)
1.928 +apply auto
1.929 +done
1.930
1.931 lemma set_count_greater_0: "set x = {a. count (multiset_of x) a > 0}"
1.932 - by (induct x) auto
1.933 +by (induct x) auto
1.934
1.935 lemma distinct_count_atmost_1:
1.936 - "distinct x = (! a. count (multiset_of x) a = (if a \<in> set x then 1 else 0))"
1.937 - apply (induct x, simp, rule iffI, simp_all)
1.938 - apply (rule conjI)
1.939 - apply (simp_all add: set_of_multiset_of [THEN sym] del: set_of_multiset_of)
1.940 - apply (erule_tac x = a in allE, simp, clarify)
1.941 - apply (erule_tac x = aa in allE, simp)
1.942 - done
1.943 + "distinct x = (! a. count (multiset_of x) a = (if a \<in> set x then 1 else 0))"
1.944 +apply (induct x, simp, rule iffI, simp_all)
1.945 +apply (rule conjI)
1.946 +apply (simp_all add: set_of_multiset_of [THEN sym] del: set_of_multiset_of)
1.947 +apply (erule_tac x = a in allE, simp, clarify)
1.948 +apply (erule_tac x = aa in allE, simp)
1.949 +done
1.950
1.951 lemma multiset_of_eq_setD:
1.952 "multiset_of xs = multiset_of ys \<Longrightarrow> set xs = set ys"
1.953 - by (rule) (auto simp add:multiset_eq_conv_count_eq set_count_greater_0)
1.954 +by (rule) (auto simp add:multiset_eq_conv_count_eq set_count_greater_0)
1.955
1.956 lemma set_eq_iff_multiset_of_eq_distinct:
1.957 "distinct x \<Longrightarrow> distinct y \<Longrightarrow>
1.958 (set x = set y) = (multiset_of x = multiset_of y)"
1.959 - by (auto simp: multiset_eq_conv_count_eq distinct_count_atmost_1)
1.960 +by (auto simp: multiset_eq_conv_count_eq distinct_count_atmost_1)
1.961
1.962 lemma set_eq_iff_multiset_of_remdups_eq:
1.963 "(set x = set y) = (multiset_of (remdups x) = multiset_of (remdups y))"
1.964 - apply (rule iffI)
1.965 - apply (simp add: set_eq_iff_multiset_of_eq_distinct[THEN iffD1])
1.966 - apply (drule distinct_remdups [THEN distinct_remdups
1.967 +apply (rule iffI)
1.968 +apply (simp add: set_eq_iff_multiset_of_eq_distinct[THEN iffD1])
1.969 +apply (drule distinct_remdups [THEN distinct_remdups
1.970 [THEN set_eq_iff_multiset_of_eq_distinct [THEN iffD2]]])
1.971 - apply simp
1.972 - done
1.973 +apply simp
1.974 +done
1.975
1.976 lemma multiset_of_compl_union [simp]:
1.977 - "multiset_of [x\<leftarrow>xs. P x] + multiset_of [x\<leftarrow>xs. \<not>P x] = multiset_of xs"
1.978 - by (induct xs) (auto simp: union_ac)
1.979 + "multiset_of [x\<leftarrow>xs. P x] + multiset_of [x\<leftarrow>xs. \<not>P x] = multiset_of xs"
1.980 +by (induct xs) (auto simp: union_ac)
1.981
1.982 lemma count_filter:
1.983 - "count (multiset_of xs) x = length [y \<leftarrow> xs. y = x]"
1.984 - by (induct xs) auto
1.985 + "count (multiset_of xs) x = length [y \<leftarrow> xs. y = x]"
1.986 +by (induct xs) auto
1.987
1.988 lemma nth_mem_multiset_of: "i < length ls \<Longrightarrow> (ls ! i) :# multiset_of ls"
1.989 - apply (induct ls arbitrary: i)
1.990 - apply simp
1.991 - apply (case_tac i)
1.992 - apply auto
1.993 - done
1.994 +apply (induct ls arbitrary: i)
1.995 + apply simp
1.996 +apply (case_tac i)
1.997 + apply auto
1.998 +done
1.999
1.1000 lemma multiset_of_remove1: "multiset_of (remove1 a xs) = multiset_of xs - {#a#}"
1.1001 - by (induct xs) (auto simp add: multiset_eq_conv_count_eq)
1.1002 +by (induct xs) (auto simp add: multiset_eq_conv_count_eq)
1.1003
1.1004 lemma multiset_of_eq_length:
1.1005 - assumes "multiset_of xs = multiset_of ys"
1.1006 - shows "length xs = length ys"
1.1007 - using assms
1.1008 +assumes "multiset_of xs = multiset_of ys"
1.1009 +shows "length xs = length ys"
1.1010 +using assms
1.1011 proof (induct arbitrary: ys rule: length_induct)
1.1012 case (1 xs ys)
1.1013 show ?case
1.1014 @@ -999,50 +995,50 @@
1.1015 notation mset_less (infix "\<subset>#" 50)
1.1016
1.1017 lemma mset_le_refl[simp]: "A \<le># A"
1.1018 - unfolding mset_le_def by auto
1.1019 +unfolding mset_le_def by auto
1.1020
1.1021 lemma mset_le_trans: "A \<le># B \<Longrightarrow> B \<le># C \<Longrightarrow> A \<le># C"
1.1022 - unfolding mset_le_def by (fast intro: order_trans)
1.1023 +unfolding mset_le_def by (fast intro: order_trans)
1.1024
1.1025 lemma mset_le_antisym: "A \<le># B \<Longrightarrow> B \<le># A \<Longrightarrow> A = B"
1.1026 - apply (unfold mset_le_def)
1.1027 - apply (rule multiset_eq_conv_count_eq [THEN iffD2])
1.1028 - apply (blast intro: order_antisym)
1.1029 - done
1.1030 +apply (unfold mset_le_def)
1.1031 +apply (rule multiset_eq_conv_count_eq [THEN iffD2])
1.1032 +apply (blast intro: order_antisym)
1.1033 +done
1.1034
1.1035 lemma mset_le_exists_conv: "(A \<le># B) = (\<exists>C. B = A + C)"
1.1036 - apply (unfold mset_le_def, rule iffI, rule_tac x = "B - A" in exI)
1.1037 - apply (auto intro: multiset_eq_conv_count_eq [THEN iffD2])
1.1038 - done
1.1039 +apply (unfold mset_le_def, rule iffI, rule_tac x = "B - A" in exI)
1.1040 +apply (auto intro: multiset_eq_conv_count_eq [THEN iffD2])
1.1041 +done
1.1042
1.1043 lemma mset_le_mono_add_right_cancel[simp]: "(A + C \<le># B + C) = (A \<le># B)"
1.1044 - unfolding mset_le_def by auto
1.1045 +unfolding mset_le_def by auto
1.1046
1.1047 lemma mset_le_mono_add_left_cancel[simp]: "(C + A \<le># C + B) = (A \<le># B)"
1.1048 - unfolding mset_le_def by auto
1.1049 +unfolding mset_le_def by auto
1.1050
1.1051 lemma mset_le_mono_add: "\<lbrakk> A \<le># B; C \<le># D \<rbrakk> \<Longrightarrow> A + C \<le># B + D"
1.1052 - apply (unfold mset_le_def)
1.1053 - apply auto
1.1054 - apply (erule_tac x = a in allE)+
1.1055 - apply auto
1.1056 - done
1.1057 +apply (unfold mset_le_def)
1.1058 +apply auto
1.1059 +apply (erule_tac x = a in allE)+
1.1060 +apply auto
1.1061 +done
1.1062
1.1063 lemma mset_le_add_left[simp]: "A \<le># A + B"
1.1064 - unfolding mset_le_def by auto
1.1065 +unfolding mset_le_def by auto
1.1066
1.1067 lemma mset_le_add_right[simp]: "B \<le># A + B"
1.1068 - unfolding mset_le_def by auto
1.1069 +unfolding mset_le_def by auto
1.1070
1.1071 lemma mset_le_single: "a :# B \<Longrightarrow> {#a#} \<le># B"
1.1072 - by (simp add: mset_le_def)
1.1073 +by (simp add: mset_le_def)
1.1074
1.1075 lemma multiset_diff_union_assoc: "C \<le># B \<Longrightarrow> A + B - C = A + (B - C)"
1.1076 - by (simp add: multiset_eq_conv_count_eq mset_le_def)
1.1077 +by (simp add: multiset_eq_conv_count_eq mset_le_def)
1.1078
1.1079 lemma mset_le_multiset_union_diff_commute:
1.1080 - assumes "B \<le># A"
1.1081 - shows "A - B + C = A + C - B"
1.1082 +assumes "B \<le># A"
1.1083 +shows "A - B + C = A + C - B"
1.1084 proof -
1.1085 from mset_le_exists_conv [of "B" "A"] assms have "\<exists>D. A = B + D" ..
1.1086 from this obtain D where "A = B + D" ..
1.1087 @@ -1061,11 +1057,11 @@
1.1088 qed
1.1089
1.1090 lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le># multiset_of xs"
1.1091 - apply (induct xs)
1.1092 - apply auto
1.1093 - apply (rule mset_le_trans)
1.1094 - apply auto
1.1095 - done
1.1096 +apply (induct xs)
1.1097 + apply auto
1.1098 +apply (rule mset_le_trans)
1.1099 + apply auto
1.1100 +done
1.1101
1.1102 lemma multiset_of_update:
1.1103 "i < length ls \<Longrightarrow> multiset_of (ls[i := v]) = multiset_of ls - {#ls ! i#} + {#v#}"
1.1104 @@ -1093,69 +1089,69 @@
1.1105 lemma multiset_of_swap:
1.1106 "i < length ls \<Longrightarrow> j < length ls \<Longrightarrow>
1.1107 multiset_of (ls[j := ls ! i, i := ls ! j]) = multiset_of ls"
1.1108 - apply (case_tac "i = j")
1.1109 - apply simp
1.1110 - apply (simp add: multiset_of_update)
1.1111 - apply (subst elem_imp_eq_diff_union[symmetric])
1.1112 - apply (simp add: nth_mem_multiset_of)
1.1113 - apply simp
1.1114 - done
1.1115 +apply (case_tac "i = j")
1.1116 + apply simp
1.1117 +apply (simp add: multiset_of_update)
1.1118 +apply (subst elem_imp_eq_diff_union[symmetric])
1.1119 + apply (simp add: nth_mem_multiset_of)
1.1120 +apply simp
1.1121 +done
1.1122
1.1123 interpretation mset_order: order ["op \<le>#" "op <#"]
1.1124 - by (auto intro: order.intro mset_le_refl mset_le_antisym
1.1125 +by (auto intro: order.intro mset_le_refl mset_le_antisym
1.1126 mset_le_trans simp: mset_less_def)
1.1127
1.1128 interpretation mset_order_cancel_semigroup:
1.1129 pordered_cancel_ab_semigroup_add ["op +" "op \<le>#" "op <#"]
1.1130 - by unfold_locales (erule mset_le_mono_add [OF mset_le_refl])
1.1131 +by unfold_locales (erule mset_le_mono_add [OF mset_le_refl])
1.1132
1.1133 interpretation mset_order_semigroup_cancel:
1.1134 pordered_ab_semigroup_add_imp_le ["op +" "op \<le>#" "op <#"]
1.1135 - by (unfold_locales) simp
1.1136 +by (unfold_locales) simp
1.1137
1.1138
1.1139 lemma mset_lessD: "A \<subset># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
1.1140 - apply (clarsimp simp: mset_le_def mset_less_def)
1.1141 - apply (erule_tac x=x in allE)
1.1142 - apply auto
1.1143 - done
1.1144 +apply (clarsimp simp: mset_le_def mset_less_def)
1.1145 +apply (erule_tac x=x in allE)
1.1146 +apply auto
1.1147 +done
1.1148
1.1149 lemma mset_leD: "A \<subseteq># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
1.1150 - apply (clarsimp simp: mset_le_def mset_less_def)
1.1151 - apply (erule_tac x = x in allE)
1.1152 - apply auto
1.1153 - done
1.1154 +apply (clarsimp simp: mset_le_def mset_less_def)
1.1155 +apply (erule_tac x = x in allE)
1.1156 +apply auto
1.1157 +done
1.1158
1.1159 lemma mset_less_insertD: "(A + {#x#} \<subset># B) \<Longrightarrow> (x \<in># B \<and> A \<subset># B)"
1.1160 - apply (rule conjI)
1.1161 - apply (simp add: mset_lessD)
1.1162 - apply (clarsimp simp: mset_le_def mset_less_def)
1.1163 - apply safe
1.1164 - apply (erule_tac x = a in allE)
1.1165 - apply (auto split: split_if_asm)
1.1166 - done
1.1167 +apply (rule conjI)
1.1168 + apply (simp add: mset_lessD)
1.1169 +apply (clarsimp simp: mset_le_def mset_less_def)
1.1170 +apply safe
1.1171 + apply (erule_tac x = a in allE)
1.1172 + apply (auto split: split_if_asm)
1.1173 +done
1.1174
1.1175 lemma mset_le_insertD: "(A + {#x#} \<subseteq># B) \<Longrightarrow> (x \<in># B \<and> A \<subseteq># B)"
1.1176 - apply (rule conjI)
1.1177 - apply (simp add: mset_leD)
1.1178 - apply (force simp: mset_le_def mset_less_def split: split_if_asm)
1.1179 - done
1.1180 +apply (rule conjI)
1.1181 + apply (simp add: mset_leD)
1.1182 +apply (force simp: mset_le_def mset_less_def split: split_if_asm)
1.1183 +done
1.1184
1.1185 lemma mset_less_of_empty[simp]: "A \<subset># {#} = False"
1.1186 - by (induct A) (auto simp: mset_le_def mset_less_def)
1.1187 +by (induct A) (auto simp: mset_le_def mset_less_def)
1.1188
1.1189 lemma multi_psub_of_add_self[simp]: "A \<subset># A + {#x#}"
1.1190 - by (auto simp: mset_le_def mset_less_def)
1.1191 +by (auto simp: mset_le_def mset_less_def)
1.1192
1.1193 lemma multi_psub_self[simp]: "A \<subset># A = False"
1.1194 - by (auto simp: mset_le_def mset_less_def)
1.1195 +by (auto simp: mset_le_def mset_less_def)
1.1196
1.1197 lemma mset_less_add_bothsides:
1.1198 "T + {#x#} \<subset># S + {#x#} \<Longrightarrow> T \<subset># S"
1.1199 - by (auto simp: mset_le_def mset_less_def)
1.1200 +by (auto simp: mset_le_def mset_less_def)
1.1201
1.1202 lemma mset_less_empty_nonempty: "({#} \<subset># S) = (S \<noteq> {#})"
1.1203 - by (auto simp: mset_le_def mset_less_def)
1.1204 +by (auto simp: mset_le_def mset_less_def)
1.1205
1.1206 lemma mset_less_size: "A \<subset># B \<Longrightarrow> size A < size B"
1.1207 proof (induct A arbitrary: B)
1.1208 @@ -1180,7 +1176,7 @@
1.1209 lemmas mset_less_trans = mset_order.less_eq_less.less_trans
1.1210
1.1211 lemma mset_less_diff_self: "c \<in># B \<Longrightarrow> B - {#c#} \<subset># B"
1.1212 - by (auto simp: mset_le_def mset_less_def multi_drop_mem_not_eq)
1.1213 +by (auto simp: mset_le_def mset_less_def multi_drop_mem_not_eq)
1.1214
1.1215
1.1216 subsection {* Strong induction and subset induction for multisets *}
1.1217 @@ -1205,25 +1201,25 @@
1.1218 qed
1.1219
1.1220 lemma wf_mset_less_rel: "wf mset_less_rel"
1.1221 - apply (unfold mset_less_rel_def)
1.1222 - apply (rule wf_measure [THEN wf_subset, where f1=size])
1.1223 - apply (clarsimp simp: measure_def inv_image_def mset_less_size)
1.1224 - done
1.1225 +apply (unfold mset_less_rel_def)
1.1226 +apply (rule wf_measure [THEN wf_subset, where f1=size])
1.1227 +apply (clarsimp simp: measure_def inv_image_def mset_less_size)
1.1228 +done
1.1229
1.1230 text {* The induction rules: *}
1.1231
1.1232 lemma full_multiset_induct [case_names less]:
1.1233 - assumes ih: "\<And>B. \<forall>A. A \<subset># B \<longrightarrow> P A \<Longrightarrow> P B"
1.1234 - shows "P B"
1.1235 - apply (rule wf_mset_less_rel [THEN wf_induct])
1.1236 - apply (rule ih, auto simp: mset_less_rel_def)
1.1237 - done
1.1238 +assumes ih: "\<And>B. \<forall>A. A \<subset># B \<longrightarrow> P A \<Longrightarrow> P B"
1.1239 +shows "P B"
1.1240 +apply (rule wf_mset_less_rel [THEN wf_induct])
1.1241 +apply (rule ih, auto simp: mset_less_rel_def)
1.1242 +done
1.1243
1.1244 lemma multi_subset_induct [consumes 2, case_names empty add]:
1.1245 - assumes "F \<subseteq># A"
1.1246 - and empty: "P {#}"
1.1247 - and insert: "\<And>a F. a \<in># A \<Longrightarrow> P F \<Longrightarrow> P (F + {#a#})"
1.1248 - shows "P F"
1.1249 +assumes "F \<subseteq># A"
1.1250 + and empty: "P {#}"
1.1251 + and insert: "\<And>a F. a \<in># A \<Longrightarrow> P F \<Longrightarrow> P (F + {#a#})"
1.1252 +shows "P F"
1.1253 proof -
1.1254 from `F \<subseteq># A`
1.1255 show ?thesis
1.1256 @@ -1244,19 +1240,19 @@
1.1257 text{* A consequence: Extensionality. *}
1.1258
1.1259 lemma multi_count_eq: "(\<forall>x. count A x = count B x) = (A = B)"
1.1260 - apply (rule iffI)
1.1261 - prefer 2
1.1262 - apply clarsimp
1.1263 - apply (induct A arbitrary: B rule: full_multiset_induct)
1.1264 - apply (rename_tac C)
1.1265 - apply (case_tac B rule: multiset_cases)
1.1266 - apply (simp add: empty_multiset_count)
1.1267 - apply simp
1.1268 - apply (case_tac "x \<in># C")
1.1269 - apply (force dest: multi_member_split)
1.1270 - apply (erule_tac x = x in allE)
1.1271 - apply simp
1.1272 - done
1.1273 +apply (rule iffI)
1.1274 + prefer 2
1.1275 + apply clarsimp
1.1276 +apply (induct A arbitrary: B rule: full_multiset_induct)
1.1277 +apply (rename_tac C)
1.1278 +apply (case_tac B rule: multiset_cases)
1.1279 + apply (simp add: empty_multiset_count)
1.1280 +apply simp
1.1281 +apply (case_tac "x \<in># C")
1.1282 + apply (force dest: multi_member_split)
1.1283 +apply (erule_tac x = x in allE)
1.1284 +apply simp
1.1285 +done
1.1286
1.1287 lemmas multi_count_ext = multi_count_eq [THEN iffD1, rule_format]
1.1288
1.1289 @@ -1291,24 +1287,24 @@
1.1290
1.1291 lemma Diff1_fold_msetG:
1.1292 "fold_msetG f z (A - {#x#}) y \<Longrightarrow> x \<in># A \<Longrightarrow> fold_msetG f z A (f x y)"
1.1293 - apply (frule_tac x = x in fold_msetG.insertI)
1.1294 - apply auto
1.1295 - done
1.1296 +apply (frule_tac x = x in fold_msetG.insertI)
1.1297 +apply auto
1.1298 +done
1.1299
1.1300 lemma fold_msetG_nonempty: "\<exists>x. fold_msetG f z A x"
1.1301 - apply (induct A)
1.1302 - apply blast
1.1303 - apply clarsimp
1.1304 - apply (drule_tac x = x in fold_msetG.insertI)
1.1305 - apply auto
1.1306 - done
1.1307 +apply (induct A)
1.1308 + apply blast
1.1309 +apply clarsimp
1.1310 +apply (drule_tac x = x in fold_msetG.insertI)
1.1311 +apply auto
1.1312 +done
1.1313
1.1314 lemma fold_mset_empty[simp]: "fold_mset f z {#} = z"
1.1315 - unfolding fold_mset_def by blast
1.1316 +unfolding fold_mset_def by blast
1.1317
1.1318 locale left_commutative =
1.1319 - fixes f :: "'a => 'b => 'b"
1.1320 - assumes left_commute: "f x (f y z) = f y (f x z)"
1.1321 +fixes f :: "'a => 'b => 'b"
1.1322 +assumes left_commute: "f x (f y z) = f y (f x z)"
1.1323 begin
1.1324
1.1325 lemma fold_msetG_determ:
1.1326 @@ -1375,37 +1371,37 @@
1.1327 lemma fold_mset_insert_aux:
1.1328 "(fold_msetG f z (A + {#x#}) v) =
1.1329 (\<exists>y. fold_msetG f z A y \<and> v = f x y)"
1.1330 - apply (rule iffI)
1.1331 - prefer 2
1.1332 - apply blast
1.1333 - apply (rule_tac A=A and f=f in fold_msetG_nonempty [THEN exE, standard])
1.1334 - apply (blast intro: fold_msetG_determ)
1.1335 - done
1.1336 +apply (rule iffI)
1.1337 + prefer 2
1.1338 + apply blast
1.1339 +apply (rule_tac A=A and f=f in fold_msetG_nonempty [THEN exE, standard])
1.1340 +apply (blast intro: fold_msetG_determ)
1.1341 +done
1.1342
1.1343 lemma fold_mset_equality: "fold_msetG f z A y \<Longrightarrow> fold_mset f z A = y"
1.1344 - unfolding fold_mset_def by (blast intro: fold_msetG_determ)
1.1345 +unfolding fold_mset_def by (blast intro: fold_msetG_determ)
1.1346
1.1347 lemma fold_mset_insert:
1.1348 - "fold_mset f z (A + {#x#}) = f x (fold_mset f z A)"
1.1349 - apply (simp add: fold_mset_def fold_mset_insert_aux union_commute)
1.1350 - apply (rule the_equality)
1.1351 - apply (auto cong add: conj_cong
1.1352 + "fold_mset f z (A + {#x#}) = f x (fold_mset f z A)"
1.1353 +apply (simp add: fold_mset_def fold_mset_insert_aux union_commute)
1.1354 +apply (rule the_equality)
1.1355 + apply (auto cong add: conj_cong
1.1356 simp add: fold_mset_def [symmetric] fold_mset_equality fold_msetG_nonempty)
1.1357 - done
1.1358 +done
1.1359
1.1360 lemma fold_mset_insert_idem:
1.1361 - "fold_mset f z (A + {#a#}) = f a (fold_mset f z A)"
1.1362 - apply (simp add: fold_mset_def fold_mset_insert_aux)
1.1363 - apply (rule the_equality)
1.1364 - apply (auto cong add: conj_cong
1.1365 + "fold_mset f z (A + {#a#}) = f a (fold_mset f z A)"
1.1366 +apply (simp add: fold_mset_def fold_mset_insert_aux)
1.1367 +apply (rule the_equality)
1.1368 + apply (auto cong add: conj_cong
1.1369 simp add: fold_mset_def [symmetric] fold_mset_equality fold_msetG_nonempty)
1.1370 - done
1.1371 +done
1.1372
1.1373 lemma fold_mset_commute: "f x (fold_mset f z A) = fold_mset f (f x z) A"
1.1374 - by (induct A) (auto simp: fold_mset_insert left_commute [of x])
1.1375 -
1.1376 +by (induct A) (auto simp: fold_mset_insert left_commute [of x])
1.1377 +
1.1378 lemma fold_mset_single [simp]: "fold_mset f z {#x#} = f x z"
1.1379 - using fold_mset_insert [of z "{#}"] by simp
1.1380 +using fold_mset_insert [of z "{#}"] by simp
1.1381
1.1382 lemma fold_mset_union [simp]:
1.1383 "fold_mset f z (A+B) = fold_mset f (fold_mset f z A) B"
1.1384 @@ -1424,7 +1420,7 @@
1.1385 lemma fold_mset_fusion:
1.1386 includes left_commutative g
1.1387 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.1388 - by (induct A) auto
1.1389 +by (induct A) auto
1.1390
1.1391 lemma fold_mset_rec:
1.1392 assumes "a \<in># A"
1.1393 @@ -1454,30 +1450,30 @@
1.1394 definition [code func del]: "image_mset f == fold_mset (op + o single o f) {#}"
1.1395
1.1396 interpretation image_left_comm: left_commutative ["op + o single o f"]
1.1397 - by (unfold_locales) (simp add:union_ac)
1.1398 +by (unfold_locales) (simp add:union_ac)
1.1399
1.1400 lemma image_mset_empty [simp, code func]: "image_mset f {#} = {#}"
1.1401 - by (simp add: image_mset_def)
1.1402 +by (simp add: image_mset_def)
1.1403
1.1404 lemma image_mset_single [simp, code func]: "image_mset f {#x#} = {#f x#}"
1.1405 - by (simp add: image_mset_def)
1.1406 +by (simp add: image_mset_def)
1.1407
1.1408 lemma image_mset_insert:
1.1409 "image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
1.1410 - by (simp add: image_mset_def add_ac)
1.1411 +by (simp add: image_mset_def add_ac)
1.1412
1.1413 lemma image_mset_union[simp, code func]:
1.1414 "image_mset f (M+N) = image_mset f M + image_mset f N"
1.1415 - apply (induct N)
1.1416 - apply simp
1.1417 - apply (simp add: union_assoc [symmetric] image_mset_insert)
1.1418 - done
1.1419 +apply (induct N)
1.1420 + apply simp
1.1421 +apply (simp add: union_assoc [symmetric] image_mset_insert)
1.1422 +done
1.1423
1.1424 lemma size_image_mset [simp]: "size (image_mset f M) = size M"
1.1425 - by (induct M) simp_all
1.1426 +by (induct M) simp_all
1.1427
1.1428 lemma image_mset_is_empty_iff [simp]: "image_mset f M = {#} \<longleftrightarrow> M = {#}"
1.1429 - by (cases M) auto
1.1430 +by (cases M) auto
1.1431
1.1432
1.1433 syntax