diff -r 59c1bfc81d91 -r 3a4d03d1a31b src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Aug 31 15:46:36 2005 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed Aug 31 15:46:37 2005 +0200
@@ -52,7 +52,7 @@
   Zero_multiset_def [simp]: "0 == {#}"
   size_def: "size M == setsum (count M) (set_of M)"
 
-constdefs 
+constdefs
  multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70)
  "multiset_inter A B \<equiv> A - (A - B)"
 
@@ -109,7 +109,7 @@
 lemmas union_ac = union_assoc union_commute union_lcomm
 
 instance multiset :: (type) comm_monoid_add
-proof 
+proof
   fix a b c :: "'a multiset"
   show "(a + b) + c = a + (b + c)" by (rule union_assoc)
   show "a + b = b + a" by (rule union_commute)
@@ -254,11 +254,11 @@
   by (simp add: multiset_inter_def min_def)
 
 lemma multiset_inter_commute: "A #\<inter> B = B #\<inter> A"
-  by (simp add: multiset_eq_conv_count_eq multiset_inter_count 
+  by (simp add: multiset_eq_conv_count_eq multiset_inter_count
     min_max.below_inf.inf_commute)
 
 lemma multiset_inter_assoc: "A #\<inter> (B #\<inter> C) = A #\<inter> B #\<inter> C"
-  by (simp add: multiset_eq_conv_count_eq multiset_inter_count 
+  by (simp add: multiset_eq_conv_count_eq multiset_inter_count
     min_max.below_inf.inf_assoc)
 
 lemma multiset_inter_left_commute: "A #\<inter> (B #\<inter> C) = B #\<inter> (A #\<inter> C)"
@@ -270,7 +270,7 @@
   multiset_inter_left_commute
 
 lemma multiset_union_diff_commute: "B #\<inter> C = {#} \<Longrightarrow> A + B - C = A - C + B"
-  apply (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def 
+  apply (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def
     split: split_if_asm)
   apply clarsimp
   apply (erule_tac x = a in allE)
@@ -345,7 +345,7 @@
      prefer 2
      apply (simp add: expand_fun_eq)
     apply (erule ssubst)
-    apply (erule Abs_multiset_inverse [THEN subst]) 
+    apply (erule Abs_multiset_inverse [THEN subst])
     apply (erule prem2 [unfolded defns, simplified])
     done
 qed
@@ -728,7 +728,7 @@
 
 lemma union_upper1: "A <= A + (B::'a::order multiset)"
 proof -
-  have "A + {#} <= A + B" by (blast intro: union_le_mono) 
+  have "A + {#} <= A + B" by (blast intro: union_le_mono)
   thus ?thesis by simp
 qed
 
@@ -736,63 +736,63 @@
 by (subst union_commute, rule union_upper1)
 
 
-subsection {* Link with lists *} 
+subsection {* Link with lists *}
 
-consts 
+consts
   multiset_of :: "'a list \<Rightarrow> 'a multiset"
 primrec
   "multiset_of [] = {#}"
   "multiset_of (a # x) = multiset_of x + {# a #}"
 
 lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])"
-  by (induct_tac x, auto) 
+  by (induct_tac x, auto)
 
 lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])"
   by (induct_tac x, auto)
 
 lemma set_of_multiset_of[simp]: "set_of(multiset_of x) = set x"
-  by (induct_tac x, auto) 
+  by (induct_tac x, auto)
 
 lemma mem_set_multiset_eq: "x \<in> set xs = (x :# multiset_of xs)"
   by (induct xs) auto
 
-lemma multiset_of_append[simp]: 
+lemma multiset_of_append[simp]:
   "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
-  by (rule_tac x=ys in spec, induct_tac xs, auto simp: union_ac) 
+  by (rule_tac x=ys in spec, induct_tac xs, auto simp: union_ac)
 
 lemma surj_multiset_of: "surj multiset_of"
-  apply (unfold surj_def, rule allI) 
-  apply (rule_tac M=y in multiset_induct, auto) 
-  apply (rule_tac x = "x # xa" in exI, auto) 
+  apply (unfold surj_def, rule allI)
+  apply (rule_tac M=y in multiset_induct, auto)
+  apply (rule_tac x = "x # xa" in exI, auto)
   done
 
 lemma set_count_greater_0: "set x = {a. 0 < count (multiset_of x) a}"
-  by (induct_tac x, auto)  
+  by (induct_tac x, auto)
 
-lemma distinct_count_atmost_1: 
+lemma distinct_count_atmost_1:
    "distinct x = (! a. count (multiset_of x) a = (if a \<in> set x then 1 else 0))"
    apply ( induct_tac x, simp, rule iffI, simp_all)
-   apply (rule conjI)  
-   apply (simp_all add: set_of_multiset_of [THEN sym] del: set_of_multiset_of) 
+   apply (rule conjI)
+   apply (simp_all add: set_of_multiset_of [THEN sym] del: set_of_multiset_of)
    apply (erule_tac x=a in allE, simp, clarify)
-   apply (erule_tac x=aa in allE, simp) 
+   apply (erule_tac x=aa in allE, simp)
    done
 
-lemma multiset_of_eq_setD: 
+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)
 
-lemma set_eq_iff_multiset_of_eq_distinct: 
-  "\<lbrakk>distinct x; distinct y\<rbrakk> 
+lemma set_eq_iff_multiset_of_eq_distinct:
+  "\<lbrakk>distinct x; distinct y\<rbrakk>
    \<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_eq_conv_count_eq distinct_count_atmost_1)
 
-lemma set_eq_iff_multiset_of_remdups_eq: 
+lemma set_eq_iff_multiset_of_remdups_eq:
    "(set x = set y) = (multiset_of (remdups x) = multiset_of (remdups y))"
-  apply (rule iffI) 
-  apply (simp add: set_eq_iff_multiset_of_eq_distinct[THEN iffD1]) 
-  apply (drule distinct_remdups[THEN distinct_remdups 
-                      [THEN set_eq_iff_multiset_of_eq_distinct[THEN iffD2]]]) 
+  apply (rule iffI)
+  apply (simp add: set_eq_iff_multiset_of_eq_distinct[THEN iffD1])
+  apply (drule distinct_remdups[THEN distinct_remdups
+                      [THEN set_eq_iff_multiset_of_eq_distinct[THEN iffD2]]])
   apply simp
   done
 
@@ -800,61 +800,66 @@
  "multiset_of [x\<in>xs. P x] + multiset_of [x\<in>xs. \<not>P x] = multiset_of xs"
   by (induct xs) (auto simp: union_ac)
 
-lemma count_filter: 
+lemma count_filter:
   "count (multiset_of xs) x = length [y \<in> xs. y = x]"
   by (induct xs, auto)
 
 
 subsection {* Pointwise ordering induced by count *}
 
-consts 
+consts
   mset_le :: "['a multiset, 'a multiset] \<Rightarrow> bool"
 
-syntax 
-  "_mset_le" :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"   ("_ \<le># _"  [50,51] 50) 
-translations 
+syntax
+  "_mset_le" :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"   ("_ \<le># _"  [50,51] 50)
+translations
   "x \<le># y" == "mset_le x y"
 
-defs 
-  mset_le_def:   "xs \<le># ys  == (! a. count xs a \<le> count ys a)"
+defs
+  mset_le_def: "xs \<le># ys == (\<forall>a. count xs a \<le> count ys a)"
 
 lemma mset_le_refl[simp]: "xs \<le># xs"
-  by (unfold mset_le_def, auto) 
+  by (unfold mset_le_def) auto
 
 lemma mset_le_trans: "\<lbrakk> xs \<le># ys; ys \<le># zs \<rbrakk> \<Longrightarrow> xs \<le># zs"
-  by (unfold mset_le_def, fast intro: order_trans) 
+  by (unfold mset_le_def) (fast intro: order_trans)
 
 lemma mset_le_antisym: "\<lbrakk> xs\<le># ys; ys \<le># xs\<rbrakk> \<Longrightarrow> xs = ys"
-  apply (unfold mset_le_def) 
-  apply (rule multiset_eq_conv_count_eq[THEN iffD2]) 
+  apply (unfold mset_le_def)
+  apply (rule multiset_eq_conv_count_eq[THEN iffD2])
   apply (blast intro: order_antisym)
   done
 
-lemma mset_le_exists_conv: 
-  "(xs \<le># ys) = (? zs. ys = xs + zs)"
-  apply (unfold mset_le_def, rule iffI, rule_tac x = "ys - xs" in exI) 
+lemma mset_le_exists_conv:
+  "(xs \<le># ys) = (\<exists>zs. ys = xs + zs)"
+  apply (unfold mset_le_def, rule iffI, rule_tac x = "ys - xs" in exI)
   apply (auto intro: multiset_eq_conv_count_eq [THEN iffD2])
   done
 
 lemma mset_le_mono_add_right_cancel[simp]: "(xs + zs \<le># ys + zs) = (xs \<le># ys)"
-  by (unfold mset_le_def, auto) 
+  by (unfold mset_le_def) auto
 
 lemma mset_le_mono_add_left_cancel[simp]: "(zs + xs \<le># zs + ys) = (xs \<le># ys)"
-  by (unfold mset_le_def, auto) 
+  by (unfold mset_le_def) auto
 
-lemma mset_le_mono_add: "\<lbrakk> xs \<le># ys; vs \<le># ws \<rbrakk> \<Longrightarrow> xs + vs \<le># ys + ws" 
-  apply (unfold mset_le_def, auto) 
+lemma mset_le_mono_add: "\<lbrakk> xs \<le># ys; vs \<le># ws \<rbrakk> \<Longrightarrow> xs + vs \<le># ys + ws"
+  apply (unfold mset_le_def)
+  apply auto
   apply (erule_tac x=a in allE)+
   apply auto
   done
 
 lemma mset_le_add_left[simp]: "xs \<le># xs + ys"
-  by (unfold mset_le_def, auto) 
+  by (unfold mset_le_def) auto
 
 lemma mset_le_add_right[simp]: "ys \<le># xs + ys"
-  by (unfold mset_le_def, auto)
+  by (unfold mset_le_def) auto
 
 lemma multiset_of_remdups_le: "multiset_of (remdups x) \<le># multiset_of x"
-  by (induct_tac x, auto, rule mset_le_trans, auto)
+  apply (induct x)
+   apply auto
+  apply (rule mset_le_trans)
+   apply auto
+  done
 
 end