# HG changeset patch
# User nipkow
# Date 1273754045 -7200
# Node ID 489c1fbbb02811251e8dd957a53b93f8752ca6f3
# Parent  c6bae4456741758122c0bf2e2c85fb57167324da
Multiset: renamed, added and tuned lemmas;
Permutation: replaced local "remove" by List.remove1

diff -r c6bae4456741 -r 489c1fbbb028 NEWS
--- a/NEWS	Wed May 12 22:33:10 2010 -0700
+++ b/NEWS	Thu May 13 14:34:05 2010 +0200
@@ -298,8 +298,14 @@
     generation;
   - use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union,
     if needed.
+Renamed:
+  multiset_eq_conv_count_eq -> multiset_ext_iff
+  multi_count_ext -> multiset_ext
+  diff_union_inverse2 -> diff_union_cancelR
 INCOMPATIBILITY.
 
+* Theory Permutation: replaced local "remove" by List.remove1.
+
 * Code generation: ML and OCaml code is decorated with signatures.
 
 * Theory List: added transpose.
diff -r c6bae4456741 -r 489c1fbbb028 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Wed May 12 22:33:10 2010 -0700
+++ b/src/HOL/Algebra/Divisibility.thy	Thu May 13 14:34:05 2010 +0200
@@ -2193,7 +2193,7 @@
 
   from csmset msubset
       have "fmset G bs = fmset G as + fmset G cs"
-      by (simp add: multiset_eq_conv_count_eq mset_le_def)
+      by (simp add: multiset_ext_iff mset_le_def)
   hence basc: "b \<sim> a \<otimes> c"
       by (rule fmset_wfactors_mult) fact+
 
diff -r c6bae4456741 -r 489c1fbbb028 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed May 12 22:33:10 2010 -0700
+++ b/src/HOL/Library/Multiset.thy	Thu May 13 14:34:05 2010 +0200
@@ -24,13 +24,13 @@
 notation (xsymbols)
   Melem (infix "\<in>#" 50)
 
-lemma multiset_eq_conv_count_eq:
+lemma multiset_ext_iff:
   "M = N \<longleftrightarrow> (\<forall>a. count M a = count N a)"
   by (simp only: count_inject [symmetric] expand_fun_eq)
 
-lemma multi_count_ext:
+lemma multiset_ext:
   "(\<And>x. count A x = count B x) \<Longrightarrow> A = B"
-  using multiset_eq_conv_count_eq by auto
+  using multiset_ext_iff by auto
 
 text {*
  \medskip Preservation of the representing set @{term multiset}.
@@ -127,7 +127,7 @@
   by (simp add: union_def in_multiset multiset_typedef)
 
 instance multiset :: (type) cancel_comm_monoid_add proof
-qed (simp_all add: multiset_eq_conv_count_eq)
+qed (simp_all add: multiset_ext_iff)
 
 
 subsubsection {* Difference *}
@@ -146,56 +146,62 @@
   by (simp add: diff_def in_multiset multiset_typedef)
 
 lemma diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
-  by (simp add: Mempty_def diff_def in_multiset multiset_typedef)
+by(simp add: multiset_ext_iff)
+
+lemma diff_cancel[simp]: "A - A = {#}"
+by (rule multiset_ext) simp
 
-lemma diff_union_inverse2 [simp]: "M + {#a#} - {#a#} = M"
-  by (rule multi_count_ext)
-    (auto simp del: count_single simp add: union_def diff_def in_multiset multiset_typedef)
+lemma diff_union_cancelR [simp]: "M + N - N = (M::'a multiset)"
+by(simp add: multiset_ext_iff)
 
-lemma diff_cancel: "A - A = {#}"
-  by (rule multi_count_ext) simp
+lemma diff_union_cancelL [simp]: "N + M - N = (M::'a multiset)"
+by(simp add: multiset_ext_iff)
 
 lemma insert_DiffM:
   "x \<in># M \<Longrightarrow> {#x#} + (M - {#x#}) = M"
-  by (clarsimp simp: multiset_eq_conv_count_eq)
+  by (clarsimp simp: multiset_ext_iff)
 
 lemma insert_DiffM2 [simp]:
   "x \<in># M \<Longrightarrow> M - {#x#} + {#x#} = M"
-  by (clarsimp simp: multiset_eq_conv_count_eq)
+  by (clarsimp simp: multiset_ext_iff)
 
 lemma diff_right_commute:
   "(M::'a multiset) - N - Q = M - Q - N"
-  by (auto simp add: multiset_eq_conv_count_eq)
+  by (auto simp add: multiset_ext_iff)
+
+lemma diff_add:
+  "(M::'a multiset) - (N + Q) = M - N - Q"
+by (simp add: multiset_ext_iff)
 
 lemma diff_union_swap:
   "a \<noteq> b \<Longrightarrow> M - {#a#} + {#b#} = M + {#b#} - {#a#}"
-  by (auto simp add: multiset_eq_conv_count_eq)
+  by (auto simp add: multiset_ext_iff)
 
 lemma diff_union_single_conv:
   "a \<in># J \<Longrightarrow> I + J - {#a#} = I + (J - {#a#})"
-  by (simp add: multiset_eq_conv_count_eq)
+  by (simp add: multiset_ext_iff)
 
 
 subsubsection {* Equality of multisets *}
 
 lemma single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}"
-  by (simp add: multiset_eq_conv_count_eq)
+  by (simp add: multiset_ext_iff)
 
 lemma single_eq_single [simp]: "{#a#} = {#b#} \<longleftrightarrow> a = b"
-  by (auto simp add: multiset_eq_conv_count_eq)
+  by (auto simp add: multiset_ext_iff)
 
 lemma union_eq_empty [iff]: "M + N = {#} \<longleftrightarrow> M = {#} \<and> N = {#}"
-  by (auto simp add: multiset_eq_conv_count_eq)
+  by (auto simp add: multiset_ext_iff)
 
 lemma empty_eq_union [iff]: "{#} = M + N \<longleftrightarrow> M = {#} \<and> N = {#}"
-  by (auto simp add: multiset_eq_conv_count_eq)
+  by (auto simp add: multiset_ext_iff)
 
 lemma multi_self_add_other_not_self [simp]: "M = M + {#x#} \<longleftrightarrow> False"
-  by (auto simp add: multiset_eq_conv_count_eq)
+  by (auto simp add: multiset_ext_iff)
 
 lemma diff_single_trivial:
   "\<not> x \<in># M \<Longrightarrow> M - {#x#} = M"
-  by (auto simp add: multiset_eq_conv_count_eq)
+  by (auto simp add: multiset_ext_iff)
 
 lemma diff_single_eq_union:
   "x \<in># M \<Longrightarrow> M - {#x#} = N \<longleftrightarrow> M = N + {#x#}"
@@ -210,27 +216,11 @@
   by auto
 
 lemma union_is_single:
-  "M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#}" (is "?lhs = ?rhs")
-proof
+  "M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#}" (is "?lhs = ?rhs")proof
   assume ?rhs then show ?lhs by auto
 next
-  assume ?lhs
-  then have "\<And>b. count (M + N) b = (if b = a then 1 else 0)" by auto
-  then have *: "\<And>b. count M b + count N b = (if b = a then 1 else 0)" by auto
-  then have "count M a + count N a = 1" by auto
-  then have **: "count M a = 1 \<and> count N a = 0 \<or> count M a = 0 \<and> count N a = 1"
-    by auto
-  from * have "\<And>b. b \<noteq> a \<Longrightarrow> count M b + count N b = 0" by auto
-  then have ***: "\<And>b. b \<noteq> a \<Longrightarrow> count M b = 0 \<and> count N b = 0" by auto
-  from ** and *** have
-    "(\<forall>b. count M b = (if b = a then 1 else 0) \<and> count N b = 0) \<or>
-      (\<forall>b. count M b = 0 \<and> count N b = (if b = a then 1 else 0))"
-    by auto
-  then have
-    "(\<forall>b. count M b = (if b = a then 1 else 0)) \<and> (\<forall>b. count N b = 0) \<or>
-      (\<forall>b. count M b = 0) \<and> (\<forall>b. count N b = (if b = a then 1 else 0))"
-    by auto
-  then show ?rhs by (auto simp add: multiset_eq_conv_count_eq)
+  assume ?lhs thus ?rhs
+    by(simp add: multiset_ext_iff split:if_splits) (metis add_is_1)
 qed
 
 lemma single_is_union:
@@ -239,6 +229,7 @@
 
 lemma add_eq_conv_diff:
   "M + {#a#} = N + {#b#} \<longleftrightarrow> M = N \<and> a = b \<or> M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#}"  (is "?lhs = ?rhs")
+(* shorter: by (simp add: multiset_ext_iff) fastsimp *)
 proof
   assume ?rhs then show ?lhs
   by (auto simp add: add_assoc add_commute [of "{#b#}"])
@@ -287,7 +278,7 @@
   mset_less_def: "(A::'a multiset) < B \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
 
 instance proof
-qed (auto simp add: mset_le_def mset_less_def multiset_eq_conv_count_eq intro: order_trans antisym)
+qed (auto simp add: mset_le_def mset_less_def multiset_ext_iff intro: order_trans antisym)
 
 end
 
@@ -298,7 +289,7 @@
 lemma mset_le_exists_conv:
   "(A::'a multiset) \<le> B \<longleftrightarrow> (\<exists>C. B = A + C)"
 apply (unfold mset_le_def, rule iffI, rule_tac x = "B - A" in exI)
-apply (auto intro: multiset_eq_conv_count_eq [THEN iffD2])
+apply (auto intro: multiset_ext_iff [THEN iffD2])
 done
 
 lemma mset_le_mono_add_right_cancel [simp]:
@@ -327,11 +318,11 @@
 
 lemma multiset_diff_union_assoc:
   "C \<le> B \<Longrightarrow> (A::'a multiset) + B - C = A + (B - C)"
-  by (simp add: multiset_eq_conv_count_eq mset_le_def)
+  by (simp add: multiset_ext_iff mset_le_def)
 
 lemma mset_le_multiset_union_diff_commute:
   "B \<le> A \<Longrightarrow> (A::'a multiset) - B + C = A + C - B"
-by (simp add: multiset_eq_conv_count_eq mset_le_def)
+by (simp add: multiset_ext_iff mset_le_def)
 
 lemma mset_lessD: "A < B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
 apply (clarsimp simp: mset_le_def mset_less_def)
@@ -361,7 +352,7 @@
 done
 
 lemma mset_less_of_empty[simp]: "A < {#} \<longleftrightarrow> False"
-  by (auto simp add: mset_less_def mset_le_def multiset_eq_conv_count_eq)
+  by (auto simp add: mset_less_def mset_le_def multiset_ext_iff)
 
 lemma multi_psub_of_add_self[simp]: "A < A + {#x#}"
   by (auto simp: mset_le_def mset_less_def)
@@ -379,7 +370,7 @@
 
 lemma mset_less_diff_self:
   "c \<in># B \<Longrightarrow> B - {#c#} < B"
-  by (auto simp: mset_le_def mset_less_def multiset_eq_conv_count_eq)
+  by (auto simp: mset_le_def mset_less_def multiset_ext_iff)
 
 
 subsubsection {* Intersection *}
@@ -406,15 +397,15 @@
   by (simp add: multiset_inter_def multiset_typedef)
 
 lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
-  by (rule multi_count_ext) (auto simp add: multiset_inter_count)
+  by (rule multiset_ext) (auto simp add: multiset_inter_count)
 
 lemma multiset_union_diff_commute:
   assumes "B #\<inter> C = {#}"
   shows "A + B - C = A - C + B"
-proof (rule multi_count_ext)
+proof (rule multiset_ext)
   fix x
   from assms have "min (count B x) (count C x) = 0"
-    by (auto simp add: multiset_inter_count multiset_eq_conv_count_eq)
+    by (auto simp add: multiset_inter_count multiset_ext_iff)
   then have "count B x = 0 \<or> count C x = 0"
     by auto
   then show "count (A + B - C) x = count (A - C + B) x"
@@ -429,15 +420,15 @@
   by (simp add: MCollect_def in_multiset multiset_typedef)
 
 lemma MCollect_empty [simp]: "MCollect {#} P = {#}"
-  by (rule multi_count_ext) simp
+  by (rule multiset_ext) simp
 
 lemma MCollect_single [simp]:
   "MCollect {#x#} P = (if P x then {#x#} else {#})"
-  by (rule multi_count_ext) simp
+  by (rule multiset_ext) simp
 
 lemma MCollect_union [simp]:
   "MCollect (M + N) f = MCollect M f + MCollect N f"
-  by (rule multi_count_ext) simp
+  by (rule multiset_ext) simp
 
 
 subsubsection {* Set of elements *}
@@ -455,7 +446,7 @@
 by (auto simp add: set_of_def)
 
 lemma set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})"
-by (auto simp add: set_of_def multiset_eq_conv_count_eq)
+by (auto simp add: set_of_def multiset_ext_iff)
 
 lemma mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)"
 by (auto simp add: set_of_def)
@@ -503,7 +494,7 @@
 done
 
 lemma size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})"
-by (auto simp add: size_def multiset_eq_conv_count_eq)
+by (auto simp add: size_def multiset_ext_iff)
 
 lemma nonempty_has_size: "(S \<noteq> {#}) = (0 < size S)"
 by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty)
@@ -624,7 +615,7 @@
 by (cases "B = {#}") (auto dest: multi_member_split)
 
 lemma multiset_partition: "M = {# x:#M. P x #} + {# x:#M. \<not> P x #}"
-apply (subst multiset_eq_conv_count_eq)
+apply (subst multiset_ext_iff)
 apply auto
 done
 
@@ -756,12 +747,12 @@
 
 lemma multiset_of_eq_setD:
   "multiset_of xs = multiset_of ys \<Longrightarrow> set xs = set ys"
-by (rule) (auto simp add:multiset_eq_conv_count_eq set_count_greater_0)
+by (rule) (auto simp add:multiset_ext_iff set_count_greater_0)
 
 lemma set_eq_iff_multiset_of_eq_distinct:
   "distinct x \<Longrightarrow> distinct y \<Longrightarrow>
     (set x = set y) = (multiset_of x = multiset_of y)"
-by (auto simp: multiset_eq_conv_count_eq distinct_count_atmost_1)
+by (auto simp: multiset_ext_iff distinct_count_atmost_1)
 
 lemma set_eq_iff_multiset_of_remdups_eq:
    "(set x = set y) = (multiset_of (remdups x) = multiset_of (remdups y))"
@@ -787,8 +778,9 @@
  apply auto
 done
 
-lemma multiset_of_remove1: "multiset_of (remove1 a xs) = multiset_of xs - {#a#}"
-by (induct xs) (auto simp add: multiset_eq_conv_count_eq)
+lemma multiset_of_remove1[simp]:
+  "multiset_of (remove1 a xs) = multiset_of xs - {#a#}"
+by (induct xs) (auto simp add: multiset_ext_iff)
 
 lemma multiset_of_eq_length:
 assumes "multiset_of xs = multiset_of ys"
@@ -925,15 +917,15 @@
 
 lemma Mempty_Bag [code]:
   "{#} = Bag []"
-  by (simp add: multiset_eq_conv_count_eq)
+  by (simp add: multiset_ext_iff)
   
 lemma single_Bag [code]:
   "{#x#} = Bag [(x, 1)]"
-  by (simp add: multiset_eq_conv_count_eq)
+  by (simp add: multiset_ext_iff)
 
 lemma MCollect_Bag [code]:
   "MCollect (Bag xs) P = Bag (filter (P \<circ> fst) xs)"
-  by (simp add: multiset_eq_conv_count_eq count_of_filter)
+  by (simp add: multiset_ext_iff count_of_filter)
 
 lemma mset_less_eq_Bag [code]:
   "Bag xs \<le> A \<longleftrightarrow> (\<forall>(x, n) \<in> set xs. count_of xs x \<le> count A x)"
@@ -1140,10 +1132,10 @@
  apply (rule_tac x = "J + {#a#}" in exI)
  apply (rule_tac x = "K + Ka" in exI)
  apply (rule conjI)
-  apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split)
+  apply (simp add: multiset_ext_iff split: nat_diff_split)
  apply (rule conjI)
   apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong, simp)
-  apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split)
+  apply (simp add: multiset_ext_iff split: nat_diff_split)
  apply (simp (no_asm_use) add: trans_def)
  apply blast
 apply (subgoal_tac "a :# (M0 + {#a#})")
@@ -1658,7 +1650,7 @@
 
 subsection {* Legacy theorem bindings *}
 
-lemmas multi_count_eq = multiset_eq_conv_count_eq [symmetric]
+lemmas multi_count_eq = multiset_ext_iff [symmetric]
 
 lemma union_commute: "M + N = N + (M::'a multiset)"
   by (fact add_commute)
diff -r c6bae4456741 -r 489c1fbbb028 src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Wed May 12 22:33:10 2010 -0700
+++ b/src/HOL/Library/Permutation.thy	Thu May 13 14:34:05 2010 +0200
@@ -93,29 +93,16 @@
 
 subsection {* Removing elements *}
 
-primrec remove :: "'a => 'a list => 'a list" where
-    "remove x [] = []"
-  | "remove x (y # ys) = (if x = y then ys else y # remove x ys)"
-
-lemma perm_remove: "x \<in> set ys ==> ys <~~> x # remove x ys"
+lemma perm_remove: "x \<in> set ys ==> ys <~~> x # remove1 x ys"
   by (induct ys) auto
 
-lemma remove_commute: "remove x (remove y l) = remove y (remove x l)"
-  by (induct l) auto
-
-lemma multiset_of_remove [simp]:
-    "multiset_of (remove a x) = multiset_of x - {#a#}"
-  apply (induct x)
-   apply (auto simp: multiset_eq_conv_count_eq)
-  done
-
 
 text {* \medskip Congruence rule *}
 
-lemma perm_remove_perm: "xs <~~> ys ==> remove z xs <~~> remove z ys"
+lemma perm_remove_perm: "xs <~~> ys ==> remove1 z xs <~~> remove1 z ys"
   by (induct pred: perm) auto
 
-lemma remove_hd [simp]: "remove z (z # xs) = xs"
+lemma remove_hd [simp]: "remove1 z (z # xs) = xs"
   by auto
 
 lemma cons_perm_imp_perm: "z # xs <~~> z # ys ==> xs <~~> ys"
@@ -146,7 +133,7 @@
   apply (erule_tac [2] perm.induct, simp_all add: union_ac)
   apply (erule rev_mp, rule_tac x=ys in spec)
   apply (induct_tac xs, auto)
-  apply (erule_tac x = "remove a x" in allE, drule sym, simp)
+  apply (erule_tac x = "remove1 a x" in allE, drule sym, simp)
   apply (subgoal_tac "a \<in> set x")
   apply (drule_tac z=a in perm.Cons)
   apply (erule perm.trans, rule perm_sym, erule perm_remove)
diff -r c6bae4456741 -r 489c1fbbb028 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed May 12 22:33:10 2010 -0700
+++ b/src/HOL/List.thy	Thu May 13 14:34:05 2010 +0200
@@ -2961,6 +2961,9 @@
   (if x \<in> set xs then remove1 x xs @ ys else xs @ remove1 x ys)"
 by (induct xs) auto
 
+lemma remove1_commute: "remove1 x (remove1 y zs) = remove1 y (remove1 x zs)"
+by (induct zs) auto
+
 lemma in_set_remove1[simp]:
   "a \<noteq> b \<Longrightarrow> a : set(remove1 b xs) = (a : set xs)"
 apply (induct xs)
diff -r c6bae4456741 -r 489c1fbbb028 src/HOL/Number_Theory/UniqueFactorization.thy
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Wed May 12 22:33:10 2010 -0700
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Thu May 13 14:34:05 2010 +0200
@@ -56,11 +56,6 @@
   apply auto
 done
  
-(* Should this go in Multiset.thy? *)
-(* TN: No longer an intro-rule; needed only once and might get in the way *)
-lemma multiset_eqI: "[| !!x. count M x = count N x |] ==> M = N"
-  by (subst multiset_eq_conv_count_eq, blast)
-
 (* Here is a version of set product for multisets. Is it worth moving
    to multiset.thy? If so, one should similarly define msetsum for abelian 
    semirings, using of_nat. Also, is it worth developing bounded quantifiers 
@@ -210,7 +205,7 @@
     ultimately have "count M a = count N a"
       by auto
   }
-  thus ?thesis by (simp add:multiset_eq_conv_count_eq)
+  thus ?thesis by (simp add:multiset_ext_iff)
 qed
 
 definition multiset_prime_factorization :: "nat => nat multiset" where