Multiset: renamed, added and tuned lemmas;
authornipkow
Thu May 13 14:34:05 2010 +0200 (2010-05-13)
changeset 36903489c1fbbb028
parent 36902 c6bae4456741
child 36906 9eff24f4e5db
Multiset: renamed, added and tuned lemmas;
Permutation: replaced local "remove" by List.remove1
NEWS
src/HOL/Algebra/Divisibility.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Permutation.thy
src/HOL/List.thy
src/HOL/Number_Theory/UniqueFactorization.thy
     1.1 --- a/NEWS	Wed May 12 22:33:10 2010 -0700
     1.2 +++ b/NEWS	Thu May 13 14:34:05 2010 +0200
     1.3 @@ -298,8 +298,14 @@
     1.4      generation;
     1.5    - use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union,
     1.6      if needed.
     1.7 +Renamed:
     1.8 +  multiset_eq_conv_count_eq -> multiset_ext_iff
     1.9 +  multi_count_ext -> multiset_ext
    1.10 +  diff_union_inverse2 -> diff_union_cancelR
    1.11  INCOMPATIBILITY.
    1.12  
    1.13 +* Theory Permutation: replaced local "remove" by List.remove1.
    1.14 +
    1.15  * Code generation: ML and OCaml code is decorated with signatures.
    1.16  
    1.17  * Theory List: added transpose.
     2.1 --- a/src/HOL/Algebra/Divisibility.thy	Wed May 12 22:33:10 2010 -0700
     2.2 +++ b/src/HOL/Algebra/Divisibility.thy	Thu May 13 14:34:05 2010 +0200
     2.3 @@ -2193,7 +2193,7 @@
     2.4  
     2.5    from csmset msubset
     2.6        have "fmset G bs = fmset G as + fmset G cs"
     2.7 -      by (simp add: multiset_eq_conv_count_eq mset_le_def)
     2.8 +      by (simp add: multiset_ext_iff mset_le_def)
     2.9    hence basc: "b \<sim> a \<otimes> c"
    2.10        by (rule fmset_wfactors_mult) fact+
    2.11  
     3.1 --- a/src/HOL/Library/Multiset.thy	Wed May 12 22:33:10 2010 -0700
     3.2 +++ b/src/HOL/Library/Multiset.thy	Thu May 13 14:34:05 2010 +0200
     3.3 @@ -24,13 +24,13 @@
     3.4  notation (xsymbols)
     3.5    Melem (infix "\<in>#" 50)
     3.6  
     3.7 -lemma multiset_eq_conv_count_eq:
     3.8 +lemma multiset_ext_iff:
     3.9    "M = N \<longleftrightarrow> (\<forall>a. count M a = count N a)"
    3.10    by (simp only: count_inject [symmetric] expand_fun_eq)
    3.11  
    3.12 -lemma multi_count_ext:
    3.13 +lemma multiset_ext:
    3.14    "(\<And>x. count A x = count B x) \<Longrightarrow> A = B"
    3.15 -  using multiset_eq_conv_count_eq by auto
    3.16 +  using multiset_ext_iff by auto
    3.17  
    3.18  text {*
    3.19   \medskip Preservation of the representing set @{term multiset}.
    3.20 @@ -127,7 +127,7 @@
    3.21    by (simp add: union_def in_multiset multiset_typedef)
    3.22  
    3.23  instance multiset :: (type) cancel_comm_monoid_add proof
    3.24 -qed (simp_all add: multiset_eq_conv_count_eq)
    3.25 +qed (simp_all add: multiset_ext_iff)
    3.26  
    3.27  
    3.28  subsubsection {* Difference *}
    3.29 @@ -146,56 +146,62 @@
    3.30    by (simp add: diff_def in_multiset multiset_typedef)
    3.31  
    3.32  lemma diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
    3.33 -  by (simp add: Mempty_def diff_def in_multiset multiset_typedef)
    3.34 +by(simp add: multiset_ext_iff)
    3.35 +
    3.36 +lemma diff_cancel[simp]: "A - A = {#}"
    3.37 +by (rule multiset_ext) simp
    3.38  
    3.39 -lemma diff_union_inverse2 [simp]: "M + {#a#} - {#a#} = M"
    3.40 -  by (rule multi_count_ext)
    3.41 -    (auto simp del: count_single simp add: union_def diff_def in_multiset multiset_typedef)
    3.42 +lemma diff_union_cancelR [simp]: "M + N - N = (M::'a multiset)"
    3.43 +by(simp add: multiset_ext_iff)
    3.44  
    3.45 -lemma diff_cancel: "A - A = {#}"
    3.46 -  by (rule multi_count_ext) simp
    3.47 +lemma diff_union_cancelL [simp]: "N + M - N = (M::'a multiset)"
    3.48 +by(simp add: multiset_ext_iff)
    3.49  
    3.50  lemma insert_DiffM:
    3.51    "x \<in># M \<Longrightarrow> {#x#} + (M - {#x#}) = M"
    3.52 -  by (clarsimp simp: multiset_eq_conv_count_eq)
    3.53 +  by (clarsimp simp: multiset_ext_iff)
    3.54  
    3.55  lemma insert_DiffM2 [simp]:
    3.56    "x \<in># M \<Longrightarrow> M - {#x#} + {#x#} = M"
    3.57 -  by (clarsimp simp: multiset_eq_conv_count_eq)
    3.58 +  by (clarsimp simp: multiset_ext_iff)
    3.59  
    3.60  lemma diff_right_commute:
    3.61    "(M::'a multiset) - N - Q = M - Q - N"
    3.62 -  by (auto simp add: multiset_eq_conv_count_eq)
    3.63 +  by (auto simp add: multiset_ext_iff)
    3.64 +
    3.65 +lemma diff_add:
    3.66 +  "(M::'a multiset) - (N + Q) = M - N - Q"
    3.67 +by (simp add: multiset_ext_iff)
    3.68  
    3.69  lemma diff_union_swap:
    3.70    "a \<noteq> b \<Longrightarrow> M - {#a#} + {#b#} = M + {#b#} - {#a#}"
    3.71 -  by (auto simp add: multiset_eq_conv_count_eq)
    3.72 +  by (auto simp add: multiset_ext_iff)
    3.73  
    3.74  lemma diff_union_single_conv:
    3.75    "a \<in># J \<Longrightarrow> I + J - {#a#} = I + (J - {#a#})"
    3.76 -  by (simp add: multiset_eq_conv_count_eq)
    3.77 +  by (simp add: multiset_ext_iff)
    3.78  
    3.79  
    3.80  subsubsection {* Equality of multisets *}
    3.81  
    3.82  lemma single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}"
    3.83 -  by (simp add: multiset_eq_conv_count_eq)
    3.84 +  by (simp add: multiset_ext_iff)
    3.85  
    3.86  lemma single_eq_single [simp]: "{#a#} = {#b#} \<longleftrightarrow> a = b"
    3.87 -  by (auto simp add: multiset_eq_conv_count_eq)
    3.88 +  by (auto simp add: multiset_ext_iff)
    3.89  
    3.90  lemma union_eq_empty [iff]: "M + N = {#} \<longleftrightarrow> M = {#} \<and> N = {#}"
    3.91 -  by (auto simp add: multiset_eq_conv_count_eq)
    3.92 +  by (auto simp add: multiset_ext_iff)
    3.93  
    3.94  lemma empty_eq_union [iff]: "{#} = M + N \<longleftrightarrow> M = {#} \<and> N = {#}"
    3.95 -  by (auto simp add: multiset_eq_conv_count_eq)
    3.96 +  by (auto simp add: multiset_ext_iff)
    3.97  
    3.98  lemma multi_self_add_other_not_self [simp]: "M = M + {#x#} \<longleftrightarrow> False"
    3.99 -  by (auto simp add: multiset_eq_conv_count_eq)
   3.100 +  by (auto simp add: multiset_ext_iff)
   3.101  
   3.102  lemma diff_single_trivial:
   3.103    "\<not> x \<in># M \<Longrightarrow> M - {#x#} = M"
   3.104 -  by (auto simp add: multiset_eq_conv_count_eq)
   3.105 +  by (auto simp add: multiset_ext_iff)
   3.106  
   3.107  lemma diff_single_eq_union:
   3.108    "x \<in># M \<Longrightarrow> M - {#x#} = N \<longleftrightarrow> M = N + {#x#}"
   3.109 @@ -210,27 +216,11 @@
   3.110    by auto
   3.111  
   3.112  lemma union_is_single:
   3.113 -  "M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#}" (is "?lhs = ?rhs")
   3.114 -proof
   3.115 +  "M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#}" (is "?lhs = ?rhs")proof
   3.116    assume ?rhs then show ?lhs by auto
   3.117  next
   3.118 -  assume ?lhs
   3.119 -  then have "\<And>b. count (M + N) b = (if b = a then 1 else 0)" by auto
   3.120 -  then have *: "\<And>b. count M b + count N b = (if b = a then 1 else 0)" by auto
   3.121 -  then have "count M a + count N a = 1" by auto
   3.122 -  then have **: "count M a = 1 \<and> count N a = 0 \<or> count M a = 0 \<and> count N a = 1"
   3.123 -    by auto
   3.124 -  from * have "\<And>b. b \<noteq> a \<Longrightarrow> count M b + count N b = 0" by auto
   3.125 -  then have ***: "\<And>b. b \<noteq> a \<Longrightarrow> count M b = 0 \<and> count N b = 0" by auto
   3.126 -  from ** and *** have
   3.127 -    "(\<forall>b. count M b = (if b = a then 1 else 0) \<and> count N b = 0) \<or>
   3.128 -      (\<forall>b. count M b = 0 \<and> count N b = (if b = a then 1 else 0))"
   3.129 -    by auto
   3.130 -  then have
   3.131 -    "(\<forall>b. count M b = (if b = a then 1 else 0)) \<and> (\<forall>b. count N b = 0) \<or>
   3.132 -      (\<forall>b. count M b = 0) \<and> (\<forall>b. count N b = (if b = a then 1 else 0))"
   3.133 -    by auto
   3.134 -  then show ?rhs by (auto simp add: multiset_eq_conv_count_eq)
   3.135 +  assume ?lhs thus ?rhs
   3.136 +    by(simp add: multiset_ext_iff split:if_splits) (metis add_is_1)
   3.137  qed
   3.138  
   3.139  lemma single_is_union:
   3.140 @@ -239,6 +229,7 @@
   3.141  
   3.142  lemma add_eq_conv_diff:
   3.143    "M + {#a#} = N + {#b#} \<longleftrightarrow> M = N \<and> a = b \<or> M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#}"  (is "?lhs = ?rhs")
   3.144 +(* shorter: by (simp add: multiset_ext_iff) fastsimp *)
   3.145  proof
   3.146    assume ?rhs then show ?lhs
   3.147    by (auto simp add: add_assoc add_commute [of "{#b#}"])
   3.148 @@ -287,7 +278,7 @@
   3.149    mset_less_def: "(A::'a multiset) < B \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
   3.150  
   3.151  instance proof
   3.152 -qed (auto simp add: mset_le_def mset_less_def multiset_eq_conv_count_eq intro: order_trans antisym)
   3.153 +qed (auto simp add: mset_le_def mset_less_def multiset_ext_iff intro: order_trans antisym)
   3.154  
   3.155  end
   3.156  
   3.157 @@ -298,7 +289,7 @@
   3.158  lemma mset_le_exists_conv:
   3.159    "(A::'a multiset) \<le> B \<longleftrightarrow> (\<exists>C. B = A + C)"
   3.160  apply (unfold mset_le_def, rule iffI, rule_tac x = "B - A" in exI)
   3.161 -apply (auto intro: multiset_eq_conv_count_eq [THEN iffD2])
   3.162 +apply (auto intro: multiset_ext_iff [THEN iffD2])
   3.163  done
   3.164  
   3.165  lemma mset_le_mono_add_right_cancel [simp]:
   3.166 @@ -327,11 +318,11 @@
   3.167  
   3.168  lemma multiset_diff_union_assoc:
   3.169    "C \<le> B \<Longrightarrow> (A::'a multiset) + B - C = A + (B - C)"
   3.170 -  by (simp add: multiset_eq_conv_count_eq mset_le_def)
   3.171 +  by (simp add: multiset_ext_iff mset_le_def)
   3.172  
   3.173  lemma mset_le_multiset_union_diff_commute:
   3.174    "B \<le> A \<Longrightarrow> (A::'a multiset) - B + C = A + C - B"
   3.175 -by (simp add: multiset_eq_conv_count_eq mset_le_def)
   3.176 +by (simp add: multiset_ext_iff mset_le_def)
   3.177  
   3.178  lemma mset_lessD: "A < B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
   3.179  apply (clarsimp simp: mset_le_def mset_less_def)
   3.180 @@ -361,7 +352,7 @@
   3.181  done
   3.182  
   3.183  lemma mset_less_of_empty[simp]: "A < {#} \<longleftrightarrow> False"
   3.184 -  by (auto simp add: mset_less_def mset_le_def multiset_eq_conv_count_eq)
   3.185 +  by (auto simp add: mset_less_def mset_le_def multiset_ext_iff)
   3.186  
   3.187  lemma multi_psub_of_add_self[simp]: "A < A + {#x#}"
   3.188    by (auto simp: mset_le_def mset_less_def)
   3.189 @@ -379,7 +370,7 @@
   3.190  
   3.191  lemma mset_less_diff_self:
   3.192    "c \<in># B \<Longrightarrow> B - {#c#} < B"
   3.193 -  by (auto simp: mset_le_def mset_less_def multiset_eq_conv_count_eq)
   3.194 +  by (auto simp: mset_le_def mset_less_def multiset_ext_iff)
   3.195  
   3.196  
   3.197  subsubsection {* Intersection *}
   3.198 @@ -406,15 +397,15 @@
   3.199    by (simp add: multiset_inter_def multiset_typedef)
   3.200  
   3.201  lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
   3.202 -  by (rule multi_count_ext) (auto simp add: multiset_inter_count)
   3.203 +  by (rule multiset_ext) (auto simp add: multiset_inter_count)
   3.204  
   3.205  lemma multiset_union_diff_commute:
   3.206    assumes "B #\<inter> C = {#}"
   3.207    shows "A + B - C = A - C + B"
   3.208 -proof (rule multi_count_ext)
   3.209 +proof (rule multiset_ext)
   3.210    fix x
   3.211    from assms have "min (count B x) (count C x) = 0"
   3.212 -    by (auto simp add: multiset_inter_count multiset_eq_conv_count_eq)
   3.213 +    by (auto simp add: multiset_inter_count multiset_ext_iff)
   3.214    then have "count B x = 0 \<or> count C x = 0"
   3.215      by auto
   3.216    then show "count (A + B - C) x = count (A - C + B) x"
   3.217 @@ -429,15 +420,15 @@
   3.218    by (simp add: MCollect_def in_multiset multiset_typedef)
   3.219  
   3.220  lemma MCollect_empty [simp]: "MCollect {#} P = {#}"
   3.221 -  by (rule multi_count_ext) simp
   3.222 +  by (rule multiset_ext) simp
   3.223  
   3.224  lemma MCollect_single [simp]:
   3.225    "MCollect {#x#} P = (if P x then {#x#} else {#})"
   3.226 -  by (rule multi_count_ext) simp
   3.227 +  by (rule multiset_ext) simp
   3.228  
   3.229  lemma MCollect_union [simp]:
   3.230    "MCollect (M + N) f = MCollect M f + MCollect N f"
   3.231 -  by (rule multi_count_ext) simp
   3.232 +  by (rule multiset_ext) simp
   3.233  
   3.234  
   3.235  subsubsection {* Set of elements *}
   3.236 @@ -455,7 +446,7 @@
   3.237  by (auto simp add: set_of_def)
   3.238  
   3.239  lemma set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})"
   3.240 -by (auto simp add: set_of_def multiset_eq_conv_count_eq)
   3.241 +by (auto simp add: set_of_def multiset_ext_iff)
   3.242  
   3.243  lemma mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)"
   3.244  by (auto simp add: set_of_def)
   3.245 @@ -503,7 +494,7 @@
   3.246  done
   3.247  
   3.248  lemma size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})"
   3.249 -by (auto simp add: size_def multiset_eq_conv_count_eq)
   3.250 +by (auto simp add: size_def multiset_ext_iff)
   3.251  
   3.252  lemma nonempty_has_size: "(S \<noteq> {#}) = (0 < size S)"
   3.253  by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty)
   3.254 @@ -624,7 +615,7 @@
   3.255  by (cases "B = {#}") (auto dest: multi_member_split)
   3.256  
   3.257  lemma multiset_partition: "M = {# x:#M. P x #} + {# x:#M. \<not> P x #}"
   3.258 -apply (subst multiset_eq_conv_count_eq)
   3.259 +apply (subst multiset_ext_iff)
   3.260  apply auto
   3.261  done
   3.262  
   3.263 @@ -756,12 +747,12 @@
   3.264  
   3.265  lemma multiset_of_eq_setD:
   3.266    "multiset_of xs = multiset_of ys \<Longrightarrow> set xs = set ys"
   3.267 -by (rule) (auto simp add:multiset_eq_conv_count_eq set_count_greater_0)
   3.268 +by (rule) (auto simp add:multiset_ext_iff set_count_greater_0)
   3.269  
   3.270  lemma set_eq_iff_multiset_of_eq_distinct:
   3.271    "distinct x \<Longrightarrow> distinct y \<Longrightarrow>
   3.272      (set x = set y) = (multiset_of x = multiset_of y)"
   3.273 -by (auto simp: multiset_eq_conv_count_eq distinct_count_atmost_1)
   3.274 +by (auto simp: multiset_ext_iff distinct_count_atmost_1)
   3.275  
   3.276  lemma set_eq_iff_multiset_of_remdups_eq:
   3.277     "(set x = set y) = (multiset_of (remdups x) = multiset_of (remdups y))"
   3.278 @@ -787,8 +778,9 @@
   3.279   apply auto
   3.280  done
   3.281  
   3.282 -lemma multiset_of_remove1: "multiset_of (remove1 a xs) = multiset_of xs - {#a#}"
   3.283 -by (induct xs) (auto simp add: multiset_eq_conv_count_eq)
   3.284 +lemma multiset_of_remove1[simp]:
   3.285 +  "multiset_of (remove1 a xs) = multiset_of xs - {#a#}"
   3.286 +by (induct xs) (auto simp add: multiset_ext_iff)
   3.287  
   3.288  lemma multiset_of_eq_length:
   3.289  assumes "multiset_of xs = multiset_of ys"
   3.290 @@ -925,15 +917,15 @@
   3.291  
   3.292  lemma Mempty_Bag [code]:
   3.293    "{#} = Bag []"
   3.294 -  by (simp add: multiset_eq_conv_count_eq)
   3.295 +  by (simp add: multiset_ext_iff)
   3.296    
   3.297  lemma single_Bag [code]:
   3.298    "{#x#} = Bag [(x, 1)]"
   3.299 -  by (simp add: multiset_eq_conv_count_eq)
   3.300 +  by (simp add: multiset_ext_iff)
   3.301  
   3.302  lemma MCollect_Bag [code]:
   3.303    "MCollect (Bag xs) P = Bag (filter (P \<circ> fst) xs)"
   3.304 -  by (simp add: multiset_eq_conv_count_eq count_of_filter)
   3.305 +  by (simp add: multiset_ext_iff count_of_filter)
   3.306  
   3.307  lemma mset_less_eq_Bag [code]:
   3.308    "Bag xs \<le> A \<longleftrightarrow> (\<forall>(x, n) \<in> set xs. count_of xs x \<le> count A x)"
   3.309 @@ -1140,10 +1132,10 @@
   3.310   apply (rule_tac x = "J + {#a#}" in exI)
   3.311   apply (rule_tac x = "K + Ka" in exI)
   3.312   apply (rule conjI)
   3.313 -  apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split)
   3.314 +  apply (simp add: multiset_ext_iff split: nat_diff_split)
   3.315   apply (rule conjI)
   3.316    apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong, simp)
   3.317 -  apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split)
   3.318 +  apply (simp add: multiset_ext_iff split: nat_diff_split)
   3.319   apply (simp (no_asm_use) add: trans_def)
   3.320   apply blast
   3.321  apply (subgoal_tac "a :# (M0 + {#a#})")
   3.322 @@ -1658,7 +1650,7 @@
   3.323  
   3.324  subsection {* Legacy theorem bindings *}
   3.325  
   3.326 -lemmas multi_count_eq = multiset_eq_conv_count_eq [symmetric]
   3.327 +lemmas multi_count_eq = multiset_ext_iff [symmetric]
   3.328  
   3.329  lemma union_commute: "M + N = N + (M::'a multiset)"
   3.330    by (fact add_commute)
     4.1 --- a/src/HOL/Library/Permutation.thy	Wed May 12 22:33:10 2010 -0700
     4.2 +++ b/src/HOL/Library/Permutation.thy	Thu May 13 14:34:05 2010 +0200
     4.3 @@ -93,29 +93,16 @@
     4.4  
     4.5  subsection {* Removing elements *}
     4.6  
     4.7 -primrec remove :: "'a => 'a list => 'a list" where
     4.8 -    "remove x [] = []"
     4.9 -  | "remove x (y # ys) = (if x = y then ys else y # remove x ys)"
    4.10 -
    4.11 -lemma perm_remove: "x \<in> set ys ==> ys <~~> x # remove x ys"
    4.12 +lemma perm_remove: "x \<in> set ys ==> ys <~~> x # remove1 x ys"
    4.13    by (induct ys) auto
    4.14  
    4.15 -lemma remove_commute: "remove x (remove y l) = remove y (remove x l)"
    4.16 -  by (induct l) auto
    4.17 -
    4.18 -lemma multiset_of_remove [simp]:
    4.19 -    "multiset_of (remove a x) = multiset_of x - {#a#}"
    4.20 -  apply (induct x)
    4.21 -   apply (auto simp: multiset_eq_conv_count_eq)
    4.22 -  done
    4.23 -
    4.24  
    4.25  text {* \medskip Congruence rule *}
    4.26  
    4.27 -lemma perm_remove_perm: "xs <~~> ys ==> remove z xs <~~> remove z ys"
    4.28 +lemma perm_remove_perm: "xs <~~> ys ==> remove1 z xs <~~> remove1 z ys"
    4.29    by (induct pred: perm) auto
    4.30  
    4.31 -lemma remove_hd [simp]: "remove z (z # xs) = xs"
    4.32 +lemma remove_hd [simp]: "remove1 z (z # xs) = xs"
    4.33    by auto
    4.34  
    4.35  lemma cons_perm_imp_perm: "z # xs <~~> z # ys ==> xs <~~> ys"
    4.36 @@ -146,7 +133,7 @@
    4.37    apply (erule_tac [2] perm.induct, simp_all add: union_ac)
    4.38    apply (erule rev_mp, rule_tac x=ys in spec)
    4.39    apply (induct_tac xs, auto)
    4.40 -  apply (erule_tac x = "remove a x" in allE, drule sym, simp)
    4.41 +  apply (erule_tac x = "remove1 a x" in allE, drule sym, simp)
    4.42    apply (subgoal_tac "a \<in> set x")
    4.43    apply (drule_tac z=a in perm.Cons)
    4.44    apply (erule perm.trans, rule perm_sym, erule perm_remove)
     5.1 --- a/src/HOL/List.thy	Wed May 12 22:33:10 2010 -0700
     5.2 +++ b/src/HOL/List.thy	Thu May 13 14:34:05 2010 +0200
     5.3 @@ -2961,6 +2961,9 @@
     5.4    (if x \<in> set xs then remove1 x xs @ ys else xs @ remove1 x ys)"
     5.5  by (induct xs) auto
     5.6  
     5.7 +lemma remove1_commute: "remove1 x (remove1 y zs) = remove1 y (remove1 x zs)"
     5.8 +by (induct zs) auto
     5.9 +
    5.10  lemma in_set_remove1[simp]:
    5.11    "a \<noteq> b \<Longrightarrow> a : set(remove1 b xs) = (a : set xs)"
    5.12  apply (induct xs)
     6.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Wed May 12 22:33:10 2010 -0700
     6.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Thu May 13 14:34:05 2010 +0200
     6.3 @@ -56,11 +56,6 @@
     6.4    apply auto
     6.5  done
     6.6   
     6.7 -(* Should this go in Multiset.thy? *)
     6.8 -(* TN: No longer an intro-rule; needed only once and might get in the way *)
     6.9 -lemma multiset_eqI: "[| !!x. count M x = count N x |] ==> M = N"
    6.10 -  by (subst multiset_eq_conv_count_eq, blast)
    6.11 -
    6.12  (* Here is a version of set product for multisets. Is it worth moving
    6.13     to multiset.thy? If so, one should similarly define msetsum for abelian 
    6.14     semirings, using of_nat. Also, is it worth developing bounded quantifiers 
    6.15 @@ -210,7 +205,7 @@
    6.16      ultimately have "count M a = count N a"
    6.17        by auto
    6.18    }
    6.19 -  thus ?thesis by (simp add:multiset_eq_conv_count_eq)
    6.20 +  thus ?thesis by (simp add:multiset_ext_iff)
    6.21  qed
    6.22  
    6.23  definition multiset_prime_factorization :: "nat => nat multiset" where