diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Sep 13 11:13:15 2010 +0200
@@ -24,13 +24,13 @@
 notation (xsymbols)
   Melem (infix "\<in>#" 50)
 
-lemma multiset_ext_iff:
+lemma multiset_eq_iff:
   "M = N \<longleftrightarrow> (\<forall>a. count M a = count N a)"
-  by (simp only: count_inject [symmetric] ext_iff)
+  by (simp only: count_inject [symmetric] fun_eq_iff)
 
-lemma multiset_ext:
+lemma multiset_eqI:
   "(\<And>x. count A x = count B x) \<Longrightarrow> A = B"
-  using multiset_ext_iff by auto
+  using multiset_eq_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_ext_iff)
+qed (simp_all add: multiset_eq_iff)
 
 
 subsubsection {* Difference *}
@@ -146,62 +146,62 @@
   by (simp add: diff_def in_multiset multiset_typedef)
 
 lemma diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
-by(simp add: multiset_ext_iff)
+by(simp add: multiset_eq_iff)
 
 lemma diff_cancel[simp]: "A - A = {#}"
-by (rule multiset_ext) simp
+by (rule multiset_eqI) simp
 
 lemma diff_union_cancelR [simp]: "M + N - N = (M::'a multiset)"
-by(simp add: multiset_ext_iff)
+by(simp add: multiset_eq_iff)
 
 lemma diff_union_cancelL [simp]: "N + M - N = (M::'a multiset)"
-by(simp add: multiset_ext_iff)
+by(simp add: multiset_eq_iff)
 
 lemma insert_DiffM:
   "x \<in># M \<Longrightarrow> {#x#} + (M - {#x#}) = M"
-  by (clarsimp simp: multiset_ext_iff)
+  by (clarsimp simp: multiset_eq_iff)
 
 lemma insert_DiffM2 [simp]:
   "x \<in># M \<Longrightarrow> M - {#x#} + {#x#} = M"
-  by (clarsimp simp: multiset_ext_iff)
+  by (clarsimp simp: multiset_eq_iff)
 
 lemma diff_right_commute:
   "(M::'a multiset) - N - Q = M - Q - N"
-  by (auto simp add: multiset_ext_iff)
+  by (auto simp add: multiset_eq_iff)
 
 lemma diff_add:
   "(M::'a multiset) - (N + Q) = M - N - Q"
-by (simp add: multiset_ext_iff)
+by (simp add: multiset_eq_iff)
 
 lemma diff_union_swap:
   "a \<noteq> b \<Longrightarrow> M - {#a#} + {#b#} = M + {#b#} - {#a#}"
-  by (auto simp add: multiset_ext_iff)
+  by (auto simp add: multiset_eq_iff)
 
 lemma diff_union_single_conv:
   "a \<in># J \<Longrightarrow> I + J - {#a#} = I + (J - {#a#})"
-  by (simp add: multiset_ext_iff)
+  by (simp add: multiset_eq_iff)
 
 
 subsubsection {* Equality of multisets *}
 
 lemma single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}"
-  by (simp add: multiset_ext_iff)
+  by (simp add: multiset_eq_iff)
 
 lemma single_eq_single [simp]: "{#a#} = {#b#} \<longleftrightarrow> a = b"
-  by (auto simp add: multiset_ext_iff)
+  by (auto simp add: multiset_eq_iff)
 
 lemma union_eq_empty [iff]: "M + N = {#} \<longleftrightarrow> M = {#} \<and> N = {#}"
-  by (auto simp add: multiset_ext_iff)
+  by (auto simp add: multiset_eq_iff)
 
 lemma empty_eq_union [iff]: "{#} = M + N \<longleftrightarrow> M = {#} \<and> N = {#}"
-  by (auto simp add: multiset_ext_iff)
+  by (auto simp add: multiset_eq_iff)
 
 lemma multi_self_add_other_not_self [simp]: "M = M + {#x#} \<longleftrightarrow> False"
-  by (auto simp add: multiset_ext_iff)
+  by (auto simp add: multiset_eq_iff)
 
 lemma diff_single_trivial:
   "\<not> x \<in># M \<Longrightarrow> M - {#x#} = M"
-  by (auto simp add: multiset_ext_iff)
+  by (auto simp add: multiset_eq_iff)
 
 lemma diff_single_eq_union:
   "x \<in># M \<Longrightarrow> M - {#x#} = N \<longleftrightarrow> M = N + {#x#}"
@@ -220,7 +220,7 @@
   assume ?rhs then show ?lhs by auto
 next
   assume ?lhs thus ?rhs
-    by(simp add: multiset_ext_iff split:if_splits) (metis add_is_1)
+    by(simp add: multiset_eq_iff split:if_splits) (metis add_is_1)
 qed
 
 lemma single_is_union:
@@ -229,7 +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 *)
+(* shorter: by (simp add: multiset_eq_iff) fastsimp *)
 proof
   assume ?rhs then show ?lhs
   by (auto simp add: add_assoc add_commute [of "{#b#}"])
@@ -278,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_ext_iff intro: order_trans antisym)
+qed (auto simp add: mset_le_def mset_less_def multiset_eq_iff intro: order_trans antisym)
 
 end
 
@@ -289,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_ext_iff [THEN iffD2])
+apply (auto intro: multiset_eq_iff [THEN iffD2])
 done
 
 lemma mset_le_mono_add_right_cancel [simp]:
@@ -318,11 +318,11 @@
 
 lemma multiset_diff_union_assoc:
   "C \<le> B \<Longrightarrow> (A::'a multiset) + B - C = A + (B - C)"
-  by (simp add: multiset_ext_iff mset_le_def)
+  by (simp add: multiset_eq_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_ext_iff mset_le_def)
+by (simp add: multiset_eq_iff mset_le_def)
 
 lemma diff_le_self[simp]: "(M::'a multiset) - N \<le> M"
 by(simp add: mset_le_def)
@@ -355,7 +355,7 @@
 done
 
 lemma mset_less_of_empty[simp]: "A < {#} \<longleftrightarrow> False"
-  by (auto simp add: mset_less_def mset_le_def multiset_ext_iff)
+  by (auto simp add: mset_less_def mset_le_def multiset_eq_iff)
 
 lemma multi_psub_of_add_self[simp]: "A < A + {#x#}"
   by (auto simp: mset_le_def mset_less_def)
@@ -373,7 +373,7 @@
 
 lemma mset_less_diff_self:
   "c \<in># B \<Longrightarrow> B - {#c#} < B"
-  by (auto simp: mset_le_def mset_less_def multiset_ext_iff)
+  by (auto simp: mset_le_def mset_less_def multiset_eq_iff)
 
 
 subsubsection {* Intersection *}
@@ -400,15 +400,15 @@
   by (simp add: multiset_inter_def multiset_typedef)
 
 lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
-  by (rule multiset_ext) (auto simp add: multiset_inter_count)
+  by (rule multiset_eqI) (auto simp add: multiset_inter_count)
 
 lemma multiset_union_diff_commute:
   assumes "B #\<inter> C = {#}"
   shows "A + B - C = A - C + B"
-proof (rule multiset_ext)
+proof (rule multiset_eqI)
   fix x
   from assms have "min (count B x) (count C x) = 0"
-    by (auto simp add: multiset_inter_count multiset_ext_iff)
+    by (auto simp add: multiset_inter_count multiset_eq_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"
@@ -423,15 +423,15 @@
   by (simp add: MCollect_def in_multiset multiset_typedef)
 
 lemma MCollect_empty [simp]: "MCollect {#} P = {#}"
-  by (rule multiset_ext) simp
+  by (rule multiset_eqI) simp
 
 lemma MCollect_single [simp]:
   "MCollect {#x#} P = (if P x then {#x#} else {#})"
-  by (rule multiset_ext) simp
+  by (rule multiset_eqI) simp
 
 lemma MCollect_union [simp]:
   "MCollect (M + N) f = MCollect M f + MCollect N f"
-  by (rule multiset_ext) simp
+  by (rule multiset_eqI) simp
 
 
 subsubsection {* Set of elements *}
@@ -449,7 +449,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_ext_iff)
+by (auto simp add: set_of_def multiset_eq_iff)
 
 lemma mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)"
 by (auto simp add: set_of_def)
@@ -497,7 +497,7 @@
 done
 
 lemma size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})"
-by (auto simp add: size_def multiset_ext_iff)
+by (auto simp add: size_def multiset_eq_iff)
 
 lemma nonempty_has_size: "(S \<noteq> {#}) = (0 < size S)"
 by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty)
@@ -584,7 +584,7 @@
      apply (rule empty [unfolded defns])
     apply (subgoal_tac "f(b := f b + 1) = (\<lambda>a. f a + (if a=b then 1 else 0))")
      prefer 2
-     apply (simp add: ext_iff)
+     apply (simp add: fun_eq_iff)
     apply (erule ssubst)
     apply (erule Abs_multiset_inverse [THEN subst])
     apply (drule add')
@@ -618,7 +618,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_ext_iff)
+apply (subst multiset_eq_iff)
 apply auto
 done
 
@@ -758,12 +758,12 @@
 
 lemma multiset_of_eq_setD:
   "multiset_of xs = multiset_of ys \<Longrightarrow> set xs = set ys"
-by (rule) (auto simp add:multiset_ext_iff set_count_greater_0)
+by (rule) (auto simp add:multiset_eq_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_ext_iff distinct_count_atmost_1)
+by (auto simp: multiset_eq_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))"
@@ -791,7 +791,7 @@
 
 lemma multiset_of_remove1[simp]:
   "multiset_of (remove1 a xs) = multiset_of xs - {#a#}"
-by (induct xs) (auto simp add: multiset_ext_iff)
+by (induct xs) (auto simp add: multiset_eq_iff)
 
 lemma multiset_of_eq_length:
   assumes "multiset_of xs = multiset_of ys"
@@ -886,13 +886,13 @@
   with finite_dom_map_of [of xs] have "finite ?A"
     by (auto intro: finite_subset)
   then show ?thesis
-    by (simp add: count_of_def ext_iff multiset_def)
+    by (simp add: count_of_def fun_eq_iff multiset_def)
 qed
 
 lemma count_simps [simp]:
   "count_of [] = (\<lambda>_. 0)"
   "count_of ((x, n) # xs) = (\<lambda>y. if x = y then n else count_of xs y)"
-  by (simp_all add: count_of_def ext_iff)
+  by (simp_all add: count_of_def fun_eq_iff)
 
 lemma count_of_empty:
   "x \<notin> fst ` set xs \<Longrightarrow> count_of xs x = 0"
@@ -913,15 +913,15 @@
 
 lemma Mempty_Bag [code]:
   "{#} = Bag []"
-  by (simp add: multiset_ext_iff)
+  by (simp add: multiset_eq_iff)
   
 lemma single_Bag [code]:
   "{#x#} = Bag [(x, 1)]"
-  by (simp add: multiset_ext_iff)
+  by (simp add: multiset_eq_iff)
 
 lemma MCollect_Bag [code]:
   "MCollect (Bag xs) P = Bag (filter (P \<circ> fst) xs)"
-  by (simp add: multiset_ext_iff count_of_filter)
+  by (simp add: multiset_eq_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)"
@@ -1132,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_ext_iff split: nat_diff_split)
+  apply (simp add: multiset_eq_iff split: nat_diff_split)
  apply (rule conjI)
   apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong, simp)
-  apply (simp add: multiset_ext_iff split: nat_diff_split)
+  apply (simp add: multiset_eq_iff split: nat_diff_split)
  apply (simp (no_asm_use) add: trans_def)
  apply blast
 apply (subgoal_tac "a :# (M0 + {#a#})")
@@ -1650,7 +1650,7 @@
 
 subsection {* Legacy theorem bindings *}
 
-lemmas multi_count_eq = multiset_ext_iff [symmetric]
+lemmas multi_count_eq = multiset_eq_iff [symmetric]
 
 lemma union_commute: "M + N = N + (M::'a multiset)"
   by (fact add_commute)