# HG changeset patch
# User nipkow
# Date 1204203869 -3600
# Node ID 3396ba6d08239820a31aad5a44f272351d3df621
# Parent  6b127c056e833c9eb0e09355720a025d6553b03e
tuned

diff -r 6b127c056e83 -r 3396ba6d0823 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Feb 28 12:56:33 2008 +0100
+++ b/src/HOL/Library/Multiset.thy	Thu Feb 28 14:04:29 2008 +0100
@@ -92,30 +92,30 @@
 *}
 
 lemma const0_in_multiset: "(\<lambda>a. 0) \<in> multiset"
-  by (simp add: multiset_def)
+by (simp add: multiset_def)
 
 lemma only1_in_multiset: "(\<lambda>b. if b = a then 1 else 0) \<in> multiset"
-  by (simp add: multiset_def)
+by (simp add: multiset_def)
 
 lemma union_preserves_multiset:
-    "M \<in> multiset ==> N \<in> multiset ==> (\<lambda>a. M a + N a) \<in> multiset"
-  apply (simp add: multiset_def)
-  apply (drule (1) finite_UnI)
-  apply (simp del: finite_Un add: Un_def)
-  done
+  "M \<in> multiset ==> N \<in> multiset ==> (\<lambda>a. M a + N a) \<in> multiset"
+apply (simp add: multiset_def)
+apply (drule (1) finite_UnI)
+apply (simp del: finite_Un add: Un_def)
+done
 
 lemma diff_preserves_multiset:
-    "M \<in> multiset ==> (\<lambda>a. M a - N a) \<in> multiset"
-  apply (simp add: multiset_def)
-  apply (rule finite_subset)
-   apply auto
-  done
+  "M \<in> multiset ==> (\<lambda>a. M a - N a) \<in> multiset"
+apply (simp add: multiset_def)
+apply (rule finite_subset)
+ apply auto
+done
 
 lemma MCollect_preserves_multiset:
-    "M \<in> multiset ==> (\<lambda>x. if P x then M x else 0) \<in> multiset"
-  apply (simp add: multiset_def)
-  apply (rule finite_subset, auto)
-  done
+  "M \<in> multiset ==> (\<lambda>x. if P x then M x else 0) \<in> multiset"
+apply (simp add: multiset_def)
+apply (rule finite_subset, auto)
+done
 
 lemmas in_multiset = const0_in_multiset only1_in_multiset
   union_preserves_multiset diff_preserves_multiset MCollect_preserves_multiset
@@ -126,22 +126,19 @@
 subsubsection {* Union *}
 
 lemma union_empty [simp]: "M + {#} = M \<and> {#} + M = M"
-  by (simp add: union_def Mempty_def in_multiset)
+by (simp add: union_def Mempty_def in_multiset)
 
 lemma union_commute: "M + N = N + (M::'a multiset)"
-  by (simp add: union_def add_ac in_multiset)
+by (simp add: union_def add_ac in_multiset)
 
 lemma union_assoc: "(M + N) + K = M + (N + (K::'a multiset))"
-  by (simp add: union_def add_ac in_multiset)
+by (simp add: union_def add_ac in_multiset)
 
 lemma union_lcomm: "M + (N + K) = N + (M + (K::'a multiset))"
 proof -
-  have "M + (N + K) = (N + K) + M"
-    by (rule union_commute)
-  also have "\<dots> = N + (K + M)"
-    by (rule union_assoc)
-  also have "K + M = M + K"
-    by (rule union_commute)
+  have "M + (N + K) = (N + K) + M" by (rule union_commute)
+  also have "\<dots> = N + (K + M)" by (rule union_assoc)
+  also have "K + M = M + K" by (rule union_commute)
   finally show ?thesis .
 qed
 
@@ -159,144 +156,143 @@
 subsubsection {* Difference *}
 
 lemma diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
-  by (simp add: Mempty_def diff_def in_multiset)
+by (simp add: Mempty_def diff_def in_multiset)
 
 lemma diff_union_inverse2 [simp]: "M + {#a#} - {#a#} = M"
-  by (simp add: union_def diff_def in_multiset)
+by (simp add: union_def diff_def in_multiset)
 
 lemma diff_cancel: "A - A = {#}"
-  by (simp add: diff_def Mempty_def)
+by (simp add: diff_def Mempty_def)
 
 
 subsubsection {* Count of elements *}
 
 lemma count_empty [simp]: "count {#} a = 0"
-  by (simp add: count_def Mempty_def in_multiset)
+by (simp add: count_def Mempty_def in_multiset)
 
 lemma count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)"
-  by (simp add: count_def single_def in_multiset)
+by (simp add: count_def single_def in_multiset)
 
 lemma count_union [simp]: "count (M + N) a = count M a + count N a"
-  by (simp add: count_def union_def in_multiset)
+by (simp add: count_def union_def in_multiset)
 
 lemma count_diff [simp]: "count (M - N) a = count M a - count N a"
-  by (simp add: count_def diff_def in_multiset)
+by (simp add: count_def diff_def in_multiset)
 
 lemma count_MCollect [simp]:
-    "count {# x:#M. P x #} a = (if P a then count M a else 0)"
-  by (simp add: count_def MCollect_def in_multiset)
+  "count {# x:#M. P x #} a = (if P a then count M a else 0)"
+by (simp add: count_def MCollect_def in_multiset)
 
 
 subsubsection {* Set of elements *}
 
 lemma set_of_empty [simp]: "set_of {#} = {}"
-  by (simp add: set_of_def)
+by (simp add: set_of_def)
 
 lemma set_of_single [simp]: "set_of {#b#} = {b}"
-  by (simp add: set_of_def)
+by (simp add: set_of_def)
 
 lemma set_of_union [simp]: "set_of (M + N) = set_of M \<union> set_of N"
-  by (auto simp add: set_of_def)
+by (auto simp add: set_of_def)
 
 lemma set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})"
-  by (auto simp: set_of_def Mempty_def in_multiset count_def expand_fun_eq)
+by (auto simp: set_of_def Mempty_def in_multiset count_def expand_fun_eq)
 
 lemma mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)"
-  by (auto simp add: set_of_def)
+by (auto simp add: set_of_def)
 
 lemma set_of_MCollect [simp]: "set_of {# x:#M. P x #} = set_of M \<inter> {x. P x}"
-  by (auto simp add: set_of_def)
+by (auto simp add: set_of_def)
 
 
 subsubsection {* Size *}
 
 lemma size_empty [simp,code func]: "size {#} = 0"
-  by (simp add: size_def)
+by (simp add: size_def)
 
 lemma size_single [simp,code func]: "size {#b#} = 1"
-  by (simp add: size_def)
+by (simp add: size_def)
 
 lemma finite_set_of [iff]: "finite (set_of M)"
-  using Rep_multiset [of M]
-  by (simp add: multiset_def set_of_def count_def)
+using Rep_multiset [of M] by (simp add: multiset_def set_of_def count_def)
 
 lemma setsum_count_Int:
-    "finite A ==> setsum (count N) (A \<inter> set_of N) = setsum (count N) A"
-  apply (induct rule: finite_induct)
-   apply simp
-  apply (simp add: Int_insert_left set_of_def)
-  done
+  "finite A ==> setsum (count N) (A \<inter> set_of N) = setsum (count N) A"
+apply (induct rule: finite_induct)
+ apply simp
+apply (simp add: Int_insert_left set_of_def)
+done
 
 lemma size_union[simp,code func]: "size (M + N::'a multiset) = size M + size N"
-  apply (unfold size_def)
-  apply (subgoal_tac "count (M + N) = (\<lambda>a. count M a + count N a)")
-   prefer 2
-   apply (rule ext, simp)
-  apply (simp (no_asm_simp) add: setsum_Un_nat setsum_addf setsum_count_Int)
-  apply (subst Int_commute)
-  apply (simp (no_asm_simp) add: setsum_count_Int)
-  done
+apply (unfold size_def)
+apply (subgoal_tac "count (M + N) = (\<lambda>a. count M a + count N a)")
+ prefer 2
+ apply (rule ext, simp)
+apply (simp (no_asm_simp) add: setsum_Un_nat setsum_addf setsum_count_Int)
+apply (subst Int_commute)
+apply (simp (no_asm_simp) add: setsum_count_Int)
+done
 
 lemma size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})"
-  apply (unfold size_def Mempty_def count_def, auto simp: in_multiset)
-  apply (simp add: set_of_def count_def in_multiset expand_fun_eq)
-  done
+apply (unfold size_def Mempty_def count_def, auto simp: in_multiset)
+apply (simp add: set_of_def count_def in_multiset expand_fun_eq)
+done
 
 lemma nonempty_has_size: "(S \<noteq> {#}) = (0 < size S)"
-  by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty)
+by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty)
 
 lemma size_eq_Suc_imp_elem: "size M = Suc n ==> \<exists>a. a :# M"
-  apply (unfold size_def)
-  apply (drule setsum_SucD)
-  apply auto
-  done
+apply (unfold size_def)
+apply (drule setsum_SucD)
+apply auto
+done
 
 
 subsubsection {* Equality of multisets *}
 
 lemma multiset_eq_conv_count_eq: "(M = N) = (\<forall>a. count M a = count N a)"
-  by (simp add: count_def expand_fun_eq)
+by (simp add: count_def expand_fun_eq)
 
 lemma single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}"
-  by (simp add: single_def Mempty_def in_multiset expand_fun_eq)
+by (simp add: single_def Mempty_def in_multiset expand_fun_eq)
 
 lemma single_eq_single [simp]: "({#a#} = {#b#}) = (a = b)"
-  by (auto simp add: single_def in_multiset expand_fun_eq)
+by (auto simp add: single_def in_multiset expand_fun_eq)
 
 lemma union_eq_empty [iff]: "(M + N = {#}) = (M = {#} \<and> N = {#})"
-  by (auto simp add: union_def Mempty_def in_multiset expand_fun_eq)
+by (auto simp add: union_def Mempty_def in_multiset expand_fun_eq)
 
 lemma empty_eq_union [iff]: "({#} = M + N) = (M = {#} \<and> N = {#})"
-  by (auto simp add: union_def Mempty_def in_multiset expand_fun_eq)
+by (auto simp add: union_def Mempty_def in_multiset expand_fun_eq)
 
 lemma union_right_cancel [simp]: "(M + K = N + K) = (M = (N::'a multiset))"
-  by (simp add: union_def in_multiset expand_fun_eq)
+by (simp add: union_def in_multiset expand_fun_eq)
 
 lemma union_left_cancel [simp]: "(K + M = K + N) = (M = (N::'a multiset))"
-  by (simp add: union_def in_multiset expand_fun_eq)
+by (simp add: union_def in_multiset expand_fun_eq)
 
 lemma union_is_single:
-    "(M + N = {#a#}) = (M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#})"
-  apply (simp add: Mempty_def single_def union_def in_multiset add_is_1 expand_fun_eq)
-  apply blast
-  done
+  "(M + N = {#a#}) = (M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#})"
+apply (simp add: Mempty_def single_def union_def in_multiset add_is_1 expand_fun_eq)
+apply blast
+done
 
 lemma single_is_union:
-    "({#a#} = M + N) \<longleftrightarrow> ({#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = N)"
-  apply (unfold Mempty_def single_def union_def)
-  apply (simp add: add_is_1 one_is_add in_multiset expand_fun_eq)
-  apply (blast dest: sym)
-  done
+  "({#a#} = M + N) \<longleftrightarrow> ({#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = N)"
+apply (unfold Mempty_def single_def union_def)
+apply (simp add: add_is_1 one_is_add in_multiset expand_fun_eq)
+apply (blast dest: sym)
+done
 
 lemma add_eq_conv_diff:
   "(M + {#a#} = N + {#b#}) =
    (M = N \<and> a = b \<or> M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#})"
-  using [[simproc del: neq]]
-  apply (unfold single_def union_def diff_def)
-  apply (simp (no_asm) add: in_multiset expand_fun_eq)
-  apply (rule conjI, force, safe, simp_all)
-  apply (simp add: eq_sym_conv)
-  done
+using [[simproc del: neq]]
+apply (unfold single_def union_def diff_def)
+apply (simp (no_asm) add: in_multiset expand_fun_eq)
+apply (rule conjI, force, safe, simp_all)
+apply (simp add: eq_sym_conv)
+done
 
 declare Rep_multiset_inject [symmetric, simp del]
 
@@ -308,18 +304,18 @@
 
 lemma insert_DiffM:
   "x \<in># M \<Longrightarrow> {#x#} + (M - {#x#}) = M"
-  by (clarsimp simp: multiset_eq_conv_count_eq)
+by (clarsimp simp: multiset_eq_conv_count_eq)
 
 lemma insert_DiffM2[simp]:
   "x \<in># M \<Longrightarrow> M - {#x#} + {#x#} = M"
-  by (clarsimp simp: multiset_eq_conv_count_eq)
+by (clarsimp simp: multiset_eq_conv_count_eq)
 
 lemma multi_union_self_other_eq: 
   "(A::'a multiset) + X = A + Y \<Longrightarrow> X = Y"
-  by (induct A arbitrary: X Y) auto
+by (induct A arbitrary: X Y) auto
 
 lemma multi_self_add_other_not_self[simp]: "(A = A + {#x#}) = False"
-  by (metis single_not_empty union_empty union_left_cancel)
+by (metis single_not_empty union_empty union_left_cancel)
 
 lemma insert_noteq_member: 
   assumes BC: "B + {#b#} = C + {#c#}"
@@ -336,30 +332,30 @@
 lemma add_eq_conv_ex:
   "(M + {#a#} = N + {#b#}) =
     (M = N \<and> a = b \<or> (\<exists>K. M = K + {#b#} \<and> N = K + {#a#}))"
-  by (auto simp add: add_eq_conv_diff)
+by (auto simp add: add_eq_conv_diff)
 
 
 lemma empty_multiset_count:
   "(\<forall>x. count A x = 0) = (A = {#})"
-  by (metis count_empty multiset_eq_conv_count_eq)
+by (metis count_empty multiset_eq_conv_count_eq)
 
 
 subsubsection {* Intersection *}
 
 lemma multiset_inter_count:
-    "count (A #\<inter> B) x = min (count A x) (count B x)"
-  by (simp add: multiset_inter_def min_def)
+  "count (A #\<inter> B) x = min (count A x) (count B x)"
+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.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.inf_assoc)
 
 lemma multiset_inter_left_commute: "A #\<inter> (B #\<inter> C) = B #\<inter> (A #\<inter> C)"
-  by (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def)
+by (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def)
 
 lemmas multiset_inter_ac =
   multiset_inter_commute
@@ -367,31 +363,31 @@
   multiset_inter_left_commute
 
 lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
-  by (simp add: multiset_eq_conv_count_eq multiset_inter_count)
+by (simp add: multiset_eq_conv_count_eq multiset_inter_count)
 
 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)
-  apply auto
-  done
+apply clarsimp
+apply (erule_tac x = a in allE)
+apply auto
+done
 
 
 subsubsection {* Comprehension (filter) *}
 
 lemma MCollect_empty[simp, code func]: "MCollect {#} P = {#}"
-  by (simp add: MCollect_def Mempty_def Abs_multiset_inject
+by (simp add: MCollect_def Mempty_def Abs_multiset_inject
     in_multiset expand_fun_eq)
 
 lemma MCollect_single[simp, code func]:
-    "MCollect {#x#} P = (if P x then {#x#} else {#})"
-  by (simp add: MCollect_def Mempty_def single_def Abs_multiset_inject
+  "MCollect {#x#} P = (if P x then {#x#} else {#})"
+by (simp add: MCollect_def Mempty_def single_def Abs_multiset_inject
     in_multiset expand_fun_eq)
 
 lemma MCollect_union[simp, code func]:
   "MCollect (M+N) f = MCollect M f + MCollect N f"
-  by (simp add: MCollect_def union_def Abs_multiset_inject
+by (simp add: MCollect_def union_def Abs_multiset_inject
     in_multiset expand_fun_eq)
 
 
@@ -400,55 +396,55 @@
 lemma setsum_decr:
   "finite F ==> (0::nat) < f a ==>
     setsum (f (a := f a - 1)) F = (if a\<in>F then setsum f F - 1 else setsum f F)"
-  apply (induct rule: finite_induct)
-   apply auto
-  apply (drule_tac a = a in mk_disjoint_insert, auto)
-  done
+apply (induct rule: finite_induct)
+ apply auto
+apply (drule_tac a = a in mk_disjoint_insert, auto)
+done
 
 lemma rep_multiset_induct_aux:
-  assumes 1: "P (\<lambda>a. (0::nat))"
-    and 2: "!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))"
-  shows "\<forall>f. f \<in> multiset --> setsum f {x. f x \<noteq> 0} = n --> P f"
-  apply (unfold multiset_def)
-  apply (induct_tac n, simp, clarify)
-   apply (subgoal_tac "f = (\<lambda>a.0)")
-    apply simp
-    apply (rule 1)
-   apply (rule ext, force, clarify)
-  apply (frule setsum_SucD, clarify)
-  apply (rename_tac a)
-  apply (subgoal_tac "finite {x. (f (a := f a - 1)) x > 0}")
-   prefer 2
-   apply (rule finite_subset)
-    prefer 2
-    apply assumption
-   apply simp
-   apply blast
-  apply (subgoal_tac "f = (f (a := f a - 1))(a := (f (a := f a - 1)) a + 1)")
-   prefer 2
-   apply (rule ext)
-   apply (simp (no_asm_simp))
-   apply (erule ssubst, rule 2 [unfolded multiset_def], blast)
-  apply (erule allE, erule impE, erule_tac [2] mp, blast)
-  apply (simp (no_asm_simp) add: setsum_decr del: fun_upd_apply One_nat_def)
-  apply (subgoal_tac "{x. x \<noteq> a --> f x \<noteq> 0} = {x. f x \<noteq> 0}")
-   prefer 2
-   apply blast
-  apply (subgoal_tac "{x. x \<noteq> a \<and> f x \<noteq> 0} = {x. f x \<noteq> 0} - {a}")
-   prefer 2
-   apply blast
-  apply (simp add: le_imp_diff_is_add setsum_diff1_nat cong: conj_cong)
-  done
+assumes 1: "P (\<lambda>a. (0::nat))"
+  and 2: "!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))"
+shows "\<forall>f. f \<in> multiset --> setsum f {x. f x \<noteq> 0} = n --> P f"
+apply (unfold multiset_def)
+apply (induct_tac n, simp, clarify)
+ apply (subgoal_tac "f = (\<lambda>a.0)")
+  apply simp
+  apply (rule 1)
+ apply (rule ext, force, clarify)
+apply (frule setsum_SucD, clarify)
+apply (rename_tac a)
+apply (subgoal_tac "finite {x. (f (a := f a - 1)) x > 0}")
+ prefer 2
+ apply (rule finite_subset)
+  prefer 2
+  apply assumption
+ apply simp
+ apply blast
+apply (subgoal_tac "f = (f (a := f a - 1))(a := (f (a := f a - 1)) a + 1)")
+ prefer 2
+ apply (rule ext)
+ apply (simp (no_asm_simp))
+ apply (erule ssubst, rule 2 [unfolded multiset_def], blast)
+apply (erule allE, erule impE, erule_tac [2] mp, blast)
+apply (simp (no_asm_simp) add: setsum_decr del: fun_upd_apply One_nat_def)
+apply (subgoal_tac "{x. x \<noteq> a --> f x \<noteq> 0} = {x. f x \<noteq> 0}")
+ prefer 2
+ apply blast
+apply (subgoal_tac "{x. x \<noteq> a \<and> f x \<noteq> 0} = {x. f x \<noteq> 0} - {a}")
+ prefer 2
+ apply blast
+apply (simp add: le_imp_diff_is_add setsum_diff1_nat cong: conj_cong)
+done
 
 theorem rep_multiset_induct:
   "f \<in> multiset ==> P (\<lambda>a. 0) ==>
     (!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))) ==> P f"
-  using rep_multiset_induct_aux by blast
+using rep_multiset_induct_aux by blast
 
 theorem multiset_induct [case_names empty add, induct type: multiset]:
-  assumes empty: "P {#}"
-    and add: "!!M x. P M ==> P (M + {#x#})"
-  shows "P M"
+assumes empty: "P {#}"
+  and add: "!!M x. P M ==> P (M + {#x#})"
+shows "P M"
 proof -
   note defns = union_def single_def Mempty_def
   show ?thesis
@@ -466,12 +462,12 @@
 qed
 
 lemma multi_nonempty_split: "M \<noteq> {#} \<Longrightarrow> \<exists>A a. M = A + {#a#}"
-  by (induct M) auto
+by (induct M) auto
 
 lemma multiset_cases [cases type, case_names empty add]:
-  assumes em:  "M = {#} \<Longrightarrow> P"
-  assumes add: "\<And>N x. M = N + {#x#} \<Longrightarrow> P"
-  shows "P"
+assumes em:  "M = {#} \<Longrightarrow> P"
+assumes add: "\<And>N x. M = N + {#x#} \<Longrightarrow> P"
+shows "P"
 proof (cases "M = {#}")
   assume "M = {#}" then show ?thesis using em by simp
 next
@@ -482,20 +478,20 @@
 qed
 
 lemma multi_member_split: "x \<in># M \<Longrightarrow> \<exists>A. M = A + {#x#}"
-  apply (cases M)
-   apply simp
-  apply (rule_tac x="M - {#x#}" in exI, simp)
-  done
+apply (cases M)
+ apply simp
+apply (rule_tac x="M - {#x#}" in exI, simp)
+done
 
 lemma multiset_partition: "M = {# x:#M. P x #} + {# x:#M. \<not> P x #}"
-  apply (subst multiset_eq_conv_count_eq)
-  apply auto
-  done
+apply (subst multiset_eq_conv_count_eq)
+apply auto
+done
 
 declare multiset_typedef [simp del]
 
 lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B - {#c#} \<noteq> B"
-  by (cases "B = {#}") (auto dest: multi_member_split)
+by (cases "B = {#}") (auto dest: multi_member_split)
 
 
 subsection {* Orderings *}
@@ -513,7 +509,7 @@
   "mult r = (mult1 r)\<^sup>+"
 
 lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
-  by (simp add: mult1_def)
+by (simp add: mult1_def)
 
 lemma less_add: "(N, M0 + {#a#}) \<in> mult1 r ==>
     (\<exists>M. (M, M0) \<in> mult1 r \<and> N = M + {#a#}) \<or>
@@ -622,10 +618,10 @@
 qed
 
 theorem wf_mult1: "wf r ==> wf (mult1 r)"
-  by (rule acc_wfI) (rule all_accessible)
+by (rule acc_wfI) (rule all_accessible)
 
 theorem wf_mult: "wf r ==> wf (mult r)"
-  unfolding mult_def by (rule wf_trancl) (rule wf_mult1)
+unfolding mult_def by (rule wf_trancl) (rule wf_mult1)
 
 
 subsubsection {* Closure-free presentation *}
@@ -633,7 +629,7 @@
 (*Badly needed: a linear arithmetic procedure for multisets*)
 
 lemma diff_union_single_conv: "a :# J ==> I + J - {#a#} = I + (J - {#a#})"
-  by (simp add: multiset_eq_conv_count_eq)
+by (simp add: multiset_eq_conv_count_eq)
 
 text {* One direction. *}
 
@@ -641,77 +637,77 @@
   "trans r ==> (M, N) \<in> mult r ==>
     \<exists>I J K. N = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and>
     (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r)"
-  apply (unfold mult_def mult1_def set_of_def)
-  apply (erule converse_trancl_induct, clarify)
-   apply (rule_tac x = M0 in exI, simp, clarify)
-  apply (case_tac "a :# K")
-   apply (rule_tac x = I in exI)
-   apply (simp (no_asm))
-   apply (rule_tac x = "(K - {#a#}) + Ka" in exI)
-   apply (simp (no_asm_simp) add: union_assoc [symmetric])
-   apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong)
-   apply (simp add: diff_union_single_conv)
-   apply (simp (no_asm_use) add: trans_def)
-   apply blast
-  apply (subgoal_tac "a :# I")
-   apply (rule_tac x = "I - {#a#}" in exI)
-   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 (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 (no_asm_use) add: trans_def)
-   apply blast
-  apply (subgoal_tac "a :# (M0 + {#a#})")
-   apply simp
-  apply (simp (no_asm))
-  done
+apply (unfold mult_def mult1_def set_of_def)
+apply (erule converse_trancl_induct, clarify)
+ apply (rule_tac x = M0 in exI, simp, clarify)
+apply (case_tac "a :# K")
+ apply (rule_tac x = I in exI)
+ apply (simp (no_asm))
+ apply (rule_tac x = "(K - {#a#}) + Ka" in exI)
+ apply (simp (no_asm_simp) add: union_assoc [symmetric])
+ apply (drule_tac f = "\<lambda>M. M - {#a#}" in arg_cong)
+ apply (simp add: diff_union_single_conv)
+ apply (simp (no_asm_use) add: trans_def)
+ apply blast
+apply (subgoal_tac "a :# I")
+ apply (rule_tac x = "I - {#a#}" in exI)
+ 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 (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 (no_asm_use) add: trans_def)
+ apply blast
+apply (subgoal_tac "a :# (M0 + {#a#})")
+ apply simp
+apply (simp (no_asm))
+done
 
 lemma elem_imp_eq_diff_union: "a :# M ==> M = M - {#a#} + {#a#}"
-  by (simp add: multiset_eq_conv_count_eq)
+by (simp add: multiset_eq_conv_count_eq)
 
 lemma size_eq_Suc_imp_eq_union: "size M = Suc n ==> \<exists>a N. M = N + {#a#}"
-  apply (erule size_eq_Suc_imp_elem [THEN exE])
-  apply (drule elem_imp_eq_diff_union, auto)
-  done
+apply (erule size_eq_Suc_imp_elem [THEN exE])
+apply (drule elem_imp_eq_diff_union, auto)
+done
 
 lemma one_step_implies_mult_aux:
   "trans r ==>
     \<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))
       --> (I + K, I + J) \<in> mult r"
-  apply (induct_tac n, auto)
-  apply (frule size_eq_Suc_imp_eq_union, clarify)
-  apply (rename_tac "J'", simp)
-  apply (erule notE, auto)
-  apply (case_tac "J' = {#}")
-   apply (simp add: mult_def)
-   apply (rule r_into_trancl)
-   apply (simp add: mult1_def set_of_def, blast)
-  txt {* Now we know @{term "J' \<noteq> {#}"}. *}
-  apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition)
-  apply (erule_tac P = "\<forall>k \<in> set_of K. ?P k" in rev_mp)
-  apply (erule ssubst)
-  apply (simp add: Ball_def, auto)
-  apply (subgoal_tac
-    "((I + {# x :# K. (x, a) \<in> r #}) + {# x :# K. (x, a) \<notin> r #},
-      (I + {# x :# K. (x, a) \<in> r #}) + J') \<in> mult r")
-   prefer 2
-   apply force
-  apply (simp (no_asm_use) add: union_assoc [symmetric] mult_def)
-  apply (erule trancl_trans)
-  apply (rule r_into_trancl)
-  apply (simp add: mult1_def set_of_def)
-  apply (rule_tac x = a in exI)
-  apply (rule_tac x = "I + J'" in exI)
-  apply (simp add: union_ac)
-  done
+apply (induct_tac n, auto)
+apply (frule size_eq_Suc_imp_eq_union, clarify)
+apply (rename_tac "J'", simp)
+apply (erule notE, auto)
+apply (case_tac "J' = {#}")
+ apply (simp add: mult_def)
+ apply (rule r_into_trancl)
+ apply (simp add: mult1_def set_of_def, blast)
+txt {* Now we know @{term "J' \<noteq> {#}"}. *}
+apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition)
+apply (erule_tac P = "\<forall>k \<in> set_of K. ?P k" in rev_mp)
+apply (erule ssubst)
+apply (simp add: Ball_def, auto)
+apply (subgoal_tac
+  "((I + {# x :# K. (x, a) \<in> r #}) + {# x :# K. (x, a) \<notin> r #},
+    (I + {# x :# K. (x, a) \<in> r #}) + J') \<in> mult r")
+ prefer 2
+ apply force
+apply (simp (no_asm_use) add: union_assoc [symmetric] mult_def)
+apply (erule trancl_trans)
+apply (rule r_into_trancl)
+apply (simp add: mult1_def set_of_def)
+apply (rule_tac x = a in exI)
+apply (rule_tac x = "I + J'" in exI)
+apply (simp add: union_ac)
+done
 
 lemma one_step_implies_mult:
   "trans r ==> J \<noteq> {#} ==> \<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r
     ==> (I + K, I + J) \<in> mult r"
-  using one_step_implies_mult_aux by blast
+using one_step_implies_mult_aux by blast
 
 
 subsubsection {* Partial-order properties *}
@@ -723,116 +719,116 @@
   le_multiset_def: "M' <= M == M' = M \<or> M' < (M::'a multiset)"
 
 lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}"
-  unfolding trans_def by (blast intro: order_less_trans)
+unfolding trans_def by (blast intro: order_less_trans)
 
 text {*
  \medskip Irreflexivity.
 *}
 
 lemma mult_irrefl_aux:
-    "finite A ==> (\<forall>x \<in> A. \<exists>y \<in> A. x < (y::'a::order)) \<Longrightarrow> A = {}"
-  by (induct rule: finite_induct) (auto intro: order_less_trans)
+  "finite A ==> (\<forall>x \<in> A. \<exists>y \<in> A. x < (y::'a::order)) \<Longrightarrow> A = {}"
+by (induct rule: finite_induct) (auto intro: order_less_trans)
 
 lemma mult_less_not_refl: "\<not> M < (M::'a::order multiset)"
-  apply (unfold less_multiset_def, auto)
-  apply (drule trans_base_order [THEN mult_implies_one_step], auto)
-  apply (drule finite_set_of [THEN mult_irrefl_aux [rule_format (no_asm)]])
-  apply (simp add: set_of_eq_empty_iff)
-  done
+apply (unfold less_multiset_def, auto)
+apply (drule trans_base_order [THEN mult_implies_one_step], auto)
+apply (drule finite_set_of [THEN mult_irrefl_aux [rule_format (no_asm)]])
+apply (simp add: set_of_eq_empty_iff)
+done
 
 lemma mult_less_irrefl [elim!]: "M < (M::'a::order multiset) ==> R"
-  using insert mult_less_not_refl by fast
+using insert mult_less_not_refl by fast
 
 
 text {* Transitivity. *}
 
 theorem mult_less_trans: "K < M ==> M < N ==> K < (N::'a::order multiset)"
-  unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
+unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
 
 text {* Asymmetry. *}
 
 theorem mult_less_not_sym: "M < N ==> \<not> N < (M::'a::order multiset)"
-  apply auto
-  apply (rule mult_less_not_refl [THEN notE])
-  apply (erule mult_less_trans, assumption)
-  done
+apply auto
+apply (rule mult_less_not_refl [THEN notE])
+apply (erule mult_less_trans, assumption)
+done
 
 theorem mult_less_asym:
-    "M < N ==> (\<not> P ==> N < (M::'a::order multiset)) ==> P"
-  using mult_less_not_sym by blast
+  "M < N ==> (\<not> P ==> N < (M::'a::order multiset)) ==> P"
+using mult_less_not_sym by blast
 
 theorem mult_le_refl [iff]: "M <= (M::'a::order multiset)"
-  unfolding le_multiset_def by auto
+unfolding le_multiset_def by auto
 
 text {* Anti-symmetry. *}
 
 theorem mult_le_antisym:
-    "M <= N ==> N <= M ==> M = (N::'a::order multiset)"
-  unfolding le_multiset_def by (blast dest: mult_less_not_sym)
+  "M <= N ==> N <= M ==> M = (N::'a::order multiset)"
+unfolding le_multiset_def by (blast dest: mult_less_not_sym)
 
 text {* Transitivity. *}
 
 theorem mult_le_trans:
-    "K <= M ==> M <= N ==> K <= (N::'a::order multiset)"
-  unfolding le_multiset_def by (blast intro: mult_less_trans)
+  "K <= M ==> M <= N ==> K <= (N::'a::order multiset)"
+unfolding le_multiset_def by (blast intro: mult_less_trans)
 
 theorem mult_less_le: "(M < N) = (M <= N \<and> M \<noteq> (N::'a::order multiset))"
-  unfolding le_multiset_def by auto
+unfolding le_multiset_def by auto
 
 text {* Partial order. *}
 
 instance multiset :: (order) order
-  apply intro_classes
-     apply (rule mult_less_le)
-    apply (rule mult_le_refl)
-   apply (erule mult_le_trans, assumption)
-  apply (erule mult_le_antisym, assumption)
-  done
+apply intro_classes
+   apply (rule mult_less_le)
+  apply (rule mult_le_refl)
+ apply (erule mult_le_trans, assumption)
+apply (erule mult_le_antisym, assumption)
+done
 
 
 subsubsection {* Monotonicity of multiset union *}
 
 lemma mult1_union:
-    "(B, D) \<in> mult1 r ==> trans r ==> (C + B, C + D) \<in> mult1 r"
-  apply (unfold mult1_def)
-  apply auto
-  apply (rule_tac x = a in exI)
-  apply (rule_tac x = "C + M0" in exI)
-  apply (simp add: union_assoc)
-  done
+  "(B, D) \<in> mult1 r ==> trans r ==> (C + B, C + D) \<in> mult1 r"
+apply (unfold mult1_def)
+apply auto
+apply (rule_tac x = a in exI)
+apply (rule_tac x = "C + M0" in exI)
+apply (simp add: union_assoc)
+done
 
 lemma union_less_mono2: "B < D ==> C + B < C + (D::'a::order multiset)"
-  apply (unfold less_multiset_def mult_def)
-  apply (erule trancl_induct)
-   apply (blast intro: mult1_union transI order_less_trans r_into_trancl)
-  apply (blast intro: mult1_union transI order_less_trans r_into_trancl trancl_trans)
-  done
+apply (unfold less_multiset_def mult_def)
+apply (erule trancl_induct)
+ apply (blast intro: mult1_union transI order_less_trans r_into_trancl)
+apply (blast intro: mult1_union transI order_less_trans r_into_trancl trancl_trans)
+done
 
 lemma union_less_mono1: "B < D ==> B + C < D + (C::'a::order multiset)"
-  apply (subst union_commute [of B C])
-  apply (subst union_commute [of D C])
-  apply (erule union_less_mono2)
-  done
+apply (subst union_commute [of B C])
+apply (subst union_commute [of D C])
+apply (erule union_less_mono2)
+done
 
 lemma union_less_mono:
-    "A < C ==> B < D ==> A + B < C + (D::'a::order multiset)"
-  by (blast intro!: union_less_mono1 union_less_mono2 mult_less_trans)
+  "A < C ==> B < D ==> A + B < C + (D::'a::order multiset)"
+by (blast intro!: union_less_mono1 union_less_mono2 mult_less_trans)
 
 lemma union_le_mono:
-    "A <= C ==> B <= D ==> A + B <= C + (D::'a::order multiset)"
-  unfolding le_multiset_def
-  by (blast intro: union_less_mono union_less_mono1 union_less_mono2)
+  "A <= C ==> B <= D ==> A + B <= C + (D::'a::order multiset)"
+unfolding le_multiset_def
+by (blast intro: union_less_mono union_less_mono1 union_less_mono2)
 
 lemma empty_leI [iff]: "{#} <= (M::'a::order multiset)"
-  apply (unfold le_multiset_def less_multiset_def)
-  apply (case_tac "M = {#}")
-   prefer 2
-   apply (subgoal_tac "({#} + {#}, {#} + M) \<in> mult (Collect (split op <))")
-    prefer 2
-    apply (rule one_step_implies_mult)
-      apply (simp only: trans_def)
-      apply auto
-  done
+apply (unfold le_multiset_def less_multiset_def)
+apply (case_tac "M = {#}")
+ prefer 2
+ apply (subgoal_tac "({#} + {#}, {#} + M) \<in> mult (Collect (split op <))")
+  prefer 2
+  apply (rule one_step_implies_mult)
+    apply (simp only: trans_def)
+    apply auto
+done
 
 lemma union_upper1: "A <= A + (B::'a::order multiset)"
 proof -
@@ -841,12 +837,12 @@
 qed
 
 lemma union_upper2: "B <= A + (B::'a::order multiset)"
-  by (subst union_commute) (rule union_upper1)
+by (subst union_commute) (rule union_upper1)
 
 instance multiset :: (order) pordered_ab_semigroup_add
-  apply intro_classes
-  apply (erule union_le_mono[OF mult_le_refl])
-  done
+apply intro_classes
+apply (erule union_le_mono[OF mult_le_refl])
+done
 
 
 subsection {* Link with lists *}
@@ -856,82 +852,82 @@
   "multiset_of (a # x) = multiset_of x + {# a #}"
 
 lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])"
-  by (induct x) auto
+by (induct x) auto
 
 lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])"
-  by (induct x) auto
+by (induct x) auto
 
 lemma set_of_multiset_of[simp]: "set_of(multiset_of x) = set x"
-  by (induct x) auto
+by (induct x) auto
 
 lemma mem_set_multiset_eq: "x \<in> set xs = (x :# multiset_of xs)"
-  by (induct xs) auto
+by (induct xs) auto
 
 lemma multiset_of_append [simp]:
-    "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
-  by (induct xs arbitrary: ys) (auto simp: union_ac)
+  "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
+by (induct xs arbitrary: ys) (auto simp: union_ac)
 
 lemma surj_multiset_of: "surj multiset_of"
-  apply (unfold surj_def)
-  apply (rule allI)
-  apply (rule_tac M = y in multiset_induct)
-   apply auto
-  apply (rule_tac x = "x # xa" in exI)
-  apply auto
-  done
+apply (unfold surj_def)
+apply (rule allI)
+apply (rule_tac M = y in multiset_induct)
+ apply auto
+apply (rule_tac x = "x # xa" in exI)
+apply auto
+done
 
 lemma set_count_greater_0: "set x = {a. count (multiset_of x) a > 0}"
-  by (induct x) auto
+by (induct x) auto
 
 lemma distinct_count_atmost_1:
-   "distinct x = (! a. count (multiset_of x) a = (if a \<in> set x then 1 else 0))"
-   apply (induct 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 (erule_tac x = a in allE, simp, clarify)
-   apply (erule_tac x = aa in allE, simp)
-   done
+  "distinct x = (! a. count (multiset_of x) a = (if a \<in> set x then 1 else 0))"
+apply (induct 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 (erule_tac x = a in allE, simp, clarify)
+apply (erule_tac x = aa in allE, simp)
+done
 
 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_eq_conv_count_eq 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_eq_conv_count_eq distinct_count_atmost_1)
 
 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
+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
+apply simp
+done
 
 lemma multiset_of_compl_union [simp]:
-    "multiset_of [x\<leftarrow>xs. P x] + multiset_of [x\<leftarrow>xs. \<not>P x] = multiset_of xs"
-  by (induct xs) (auto simp: union_ac)
+  "multiset_of [x\<leftarrow>xs. P x] + multiset_of [x\<leftarrow>xs. \<not>P x] = multiset_of xs"
+by (induct xs) (auto simp: union_ac)
 
 lemma count_filter:
-    "count (multiset_of xs) x = length [y \<leftarrow> xs. y = x]"
-  by (induct xs) auto
+  "count (multiset_of xs) x = length [y \<leftarrow> xs. y = x]"
+by (induct xs) auto
 
 lemma nth_mem_multiset_of: "i < length ls \<Longrightarrow> (ls ! i) :# multiset_of ls"
-  apply (induct ls arbitrary: i)
-   apply simp
-  apply (case_tac i)
-   apply auto
-  done
+apply (induct ls arbitrary: i)
+ apply simp
+apply (case_tac i)
+ 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)
+by (induct xs) (auto simp add: multiset_eq_conv_count_eq)
 
 lemma multiset_of_eq_length:
-  assumes "multiset_of xs = multiset_of ys"
-  shows "length xs = length ys"
-  using assms
+assumes "multiset_of xs = multiset_of ys"
+shows "length xs = length ys"
+using assms
 proof (induct arbitrary: ys rule: length_induct)
   case (1 xs ys)
   show ?case
@@ -999,50 +995,50 @@
 notation mset_less  (infix "\<subset>#" 50)
 
 lemma mset_le_refl[simp]: "A \<le># A"
-  unfolding mset_le_def by auto
+unfolding mset_le_def by auto
 
 lemma mset_le_trans: "A \<le># B \<Longrightarrow> B \<le># C \<Longrightarrow> A \<le># C"
-  unfolding mset_le_def by (fast intro: order_trans)
+unfolding mset_le_def by (fast intro: order_trans)
 
 lemma mset_le_antisym: "A \<le># B \<Longrightarrow> B \<le># A \<Longrightarrow> A = B"
-  apply (unfold mset_le_def)
-  apply (rule multiset_eq_conv_count_eq [THEN iffD2])
-  apply (blast intro: order_antisym)
-  done
+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: "(A \<le># B) = (\<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])
-  done
+apply (unfold mset_le_def, rule iffI, rule_tac x = "B - A" in exI)
+apply (auto intro: multiset_eq_conv_count_eq [THEN iffD2])
+done
 
 lemma mset_le_mono_add_right_cancel[simp]: "(A + C \<le># B + C) = (A \<le># B)"
-  unfolding mset_le_def by auto
+unfolding mset_le_def by auto
 
 lemma mset_le_mono_add_left_cancel[simp]: "(C + A \<le># C + B) = (A \<le># B)"
-  unfolding mset_le_def by auto
+unfolding mset_le_def by auto
 
 lemma mset_le_mono_add: "\<lbrakk> A \<le># B; C \<le># D \<rbrakk> \<Longrightarrow> A + C \<le># B + D"
-  apply (unfold mset_le_def)
-  apply auto
-  apply (erule_tac x = a in allE)+
-  apply auto
-  done
+apply (unfold mset_le_def)
+apply auto
+apply (erule_tac x = a in allE)+
+apply auto
+done
 
 lemma mset_le_add_left[simp]: "A \<le># A + B"
-  unfolding mset_le_def by auto
+unfolding mset_le_def by auto
 
 lemma mset_le_add_right[simp]: "B \<le># A + B"
-  unfolding mset_le_def by auto
+unfolding mset_le_def by auto
 
 lemma mset_le_single: "a :# B \<Longrightarrow> {#a#} \<le># B"
-  by (simp add: mset_le_def)
+by (simp add: mset_le_def)
 
 lemma multiset_diff_union_assoc: "C \<le># B \<Longrightarrow> A + B - C = A + (B - C)"
-  by (simp add: multiset_eq_conv_count_eq mset_le_def)
+by (simp add: multiset_eq_conv_count_eq mset_le_def)
 
 lemma mset_le_multiset_union_diff_commute:
-  assumes "B \<le># A"
-  shows "A - B + C = A + C - B"
+assumes "B \<le># A"
+shows "A - B + C = A + C - B"
 proof -
   from mset_le_exists_conv [of "B" "A"] assms have "\<exists>D. A = B + D" ..
   from this obtain D where "A = B + D" ..
@@ -1061,11 +1057,11 @@
 qed
 
 lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le># multiset_of xs"
-  apply (induct xs)
-   apply auto
-  apply (rule mset_le_trans)
-   apply auto
-  done
+apply (induct xs)
+ apply auto
+apply (rule mset_le_trans)
+ apply auto
+done
 
 lemma multiset_of_update:
   "i < length ls \<Longrightarrow> multiset_of (ls[i := v]) = multiset_of ls - {#ls ! i#} + {#v#}"
@@ -1093,69 +1089,69 @@
 lemma multiset_of_swap:
   "i < length ls \<Longrightarrow> j < length ls \<Longrightarrow>
     multiset_of (ls[j := ls ! i, i := ls ! j]) = multiset_of ls"
-  apply (case_tac "i = j")
-   apply simp
-  apply (simp add: multiset_of_update)
-  apply (subst elem_imp_eq_diff_union[symmetric])
-   apply (simp add: nth_mem_multiset_of)
-  apply simp
-  done
+apply (case_tac "i = j")
+ apply simp
+apply (simp add: multiset_of_update)
+apply (subst elem_imp_eq_diff_union[symmetric])
+ apply (simp add: nth_mem_multiset_of)
+apply simp
+done
 
 interpretation mset_order: order ["op \<le>#" "op <#"]
-  by (auto intro: order.intro mset_le_refl mset_le_antisym
+by (auto intro: order.intro mset_le_refl mset_le_antisym
     mset_le_trans simp: mset_less_def)
 
 interpretation mset_order_cancel_semigroup:
     pordered_cancel_ab_semigroup_add ["op +" "op \<le>#" "op <#"]
-  by unfold_locales (erule mset_le_mono_add [OF mset_le_refl])
+by unfold_locales (erule mset_le_mono_add [OF mset_le_refl])
 
 interpretation mset_order_semigroup_cancel:
     pordered_ab_semigroup_add_imp_le ["op +" "op \<le>#" "op <#"]
-  by (unfold_locales) simp
+by (unfold_locales) simp
 
 
 lemma mset_lessD: "A \<subset># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
-  apply (clarsimp simp: mset_le_def mset_less_def)
-  apply (erule_tac x=x in allE)
-  apply auto
-  done
+apply (clarsimp simp: mset_le_def mset_less_def)
+apply (erule_tac x=x in allE)
+apply auto
+done
 
 lemma mset_leD: "A \<subseteq># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
-  apply (clarsimp simp: mset_le_def mset_less_def)
-  apply (erule_tac x = x in allE)
-  apply auto
-  done
+apply (clarsimp simp: mset_le_def mset_less_def)
+apply (erule_tac x = x in allE)
+apply auto
+done
   
 lemma mset_less_insertD: "(A + {#x#} \<subset># B) \<Longrightarrow> (x \<in># B \<and> A \<subset># B)"
-  apply (rule conjI)
-   apply (simp add: mset_lessD)
-  apply (clarsimp simp: mset_le_def mset_less_def)
-  apply safe
-   apply (erule_tac x = a in allE)
-   apply (auto split: split_if_asm)
-  done
+apply (rule conjI)
+ apply (simp add: mset_lessD)
+apply (clarsimp simp: mset_le_def mset_less_def)
+apply safe
+ apply (erule_tac x = a in allE)
+ apply (auto split: split_if_asm)
+done
 
 lemma mset_le_insertD: "(A + {#x#} \<subseteq># B) \<Longrightarrow> (x \<in># B \<and> A \<subseteq># B)"
-  apply (rule conjI)
-   apply (simp add: mset_leD)
-  apply (force simp: mset_le_def mset_less_def split: split_if_asm)
-  done
+apply (rule conjI)
+ apply (simp add: mset_leD)
+apply (force simp: mset_le_def mset_less_def split: split_if_asm)
+done
 
 lemma mset_less_of_empty[simp]: "A \<subset># {#} = False" 
-  by (induct A) (auto simp: mset_le_def mset_less_def)
+by (induct A) (auto simp: mset_le_def mset_less_def)
 
 lemma multi_psub_of_add_self[simp]: "A \<subset># A + {#x#}"
-  by (auto simp: mset_le_def mset_less_def)
+by (auto simp: mset_le_def mset_less_def)
 
 lemma multi_psub_self[simp]: "A \<subset># A = False"
-  by (auto simp: mset_le_def mset_less_def)
+by (auto simp: mset_le_def mset_less_def)
 
 lemma mset_less_add_bothsides:
   "T + {#x#} \<subset># S + {#x#} \<Longrightarrow> T \<subset># S"
-  by (auto simp: mset_le_def mset_less_def)
+by (auto simp: mset_le_def mset_less_def)
 
 lemma mset_less_empty_nonempty: "({#} \<subset># S) = (S \<noteq> {#})"
-  by (auto simp: mset_le_def mset_less_def)
+by (auto simp: mset_le_def mset_less_def)
 
 lemma mset_less_size: "A \<subset># B \<Longrightarrow> size A < size B"
 proof (induct A arbitrary: B)
@@ -1180,7 +1176,7 @@
 lemmas mset_less_trans = mset_order.less_eq_less.less_trans
 
 lemma mset_less_diff_self: "c \<in># B \<Longrightarrow> B - {#c#} \<subset># B"
-  by (auto simp: mset_le_def mset_less_def multi_drop_mem_not_eq)
+by (auto simp: mset_le_def mset_less_def multi_drop_mem_not_eq)
 
 
 subsection {* Strong induction and subset induction for multisets *}
@@ -1205,25 +1201,25 @@
 qed
 
 lemma wf_mset_less_rel: "wf mset_less_rel"
-  apply (unfold mset_less_rel_def)
-  apply (rule wf_measure [THEN wf_subset, where f1=size])
-  apply (clarsimp simp: measure_def inv_image_def mset_less_size)
-  done
+apply (unfold mset_less_rel_def)
+apply (rule wf_measure [THEN wf_subset, where f1=size])
+apply (clarsimp simp: measure_def inv_image_def mset_less_size)
+done
 
 text {* The induction rules: *}
 
 lemma full_multiset_induct [case_names less]:
-  assumes ih: "\<And>B. \<forall>A. A \<subset># B \<longrightarrow> P A \<Longrightarrow> P B"
-  shows "P B"
-  apply (rule wf_mset_less_rel [THEN wf_induct])
-  apply (rule ih, auto simp: mset_less_rel_def)
-  done
+assumes ih: "\<And>B. \<forall>A. A \<subset># B \<longrightarrow> P A \<Longrightarrow> P B"
+shows "P B"
+apply (rule wf_mset_less_rel [THEN wf_induct])
+apply (rule ih, auto simp: mset_less_rel_def)
+done
 
 lemma multi_subset_induct [consumes 2, case_names empty add]:
-  assumes "F \<subseteq># A"
-    and empty: "P {#}"
-    and insert: "\<And>a F. a \<in># A \<Longrightarrow> P F \<Longrightarrow> P (F + {#a#})"
-  shows "P F"
+assumes "F \<subseteq># A"
+  and empty: "P {#}"
+  and insert: "\<And>a F. a \<in># A \<Longrightarrow> P F \<Longrightarrow> P (F + {#a#})"
+shows "P F"
 proof -
   from `F \<subseteq># A`
   show ?thesis
@@ -1244,19 +1240,19 @@
 text{* A consequence: Extensionality. *}
 
 lemma multi_count_eq: "(\<forall>x. count A x = count B x) = (A = B)"
-  apply (rule iffI)
-   prefer 2
-   apply clarsimp 
-  apply (induct A arbitrary: B rule: full_multiset_induct)
-  apply (rename_tac C)
-  apply (case_tac B rule: multiset_cases)
-   apply (simp add: empty_multiset_count)
-  apply simp
-  apply (case_tac "x \<in># C")
-   apply (force dest: multi_member_split)
-  apply (erule_tac x = x in allE)
-  apply simp
-  done
+apply (rule iffI)
+ prefer 2
+ apply clarsimp 
+apply (induct A arbitrary: B rule: full_multiset_induct)
+apply (rename_tac C)
+apply (case_tac B rule: multiset_cases)
+ apply (simp add: empty_multiset_count)
+apply simp
+apply (case_tac "x \<in># C")
+ apply (force dest: multi_member_split)
+apply (erule_tac x = x in allE)
+apply simp
+done
 
 lemmas multi_count_ext = multi_count_eq [THEN iffD1, rule_format]
 
@@ -1291,24 +1287,24 @@
 
 lemma Diff1_fold_msetG:
   "fold_msetG f z (A - {#x#}) y \<Longrightarrow> x \<in># A \<Longrightarrow> fold_msetG f z A (f x y)"
-  apply (frule_tac x = x in fold_msetG.insertI)
-  apply auto
-  done
+apply (frule_tac x = x in fold_msetG.insertI)
+apply auto
+done
 
 lemma fold_msetG_nonempty: "\<exists>x. fold_msetG f z A x"
-  apply (induct A)
-   apply blast
-  apply clarsimp
-  apply (drule_tac x = x in fold_msetG.insertI)
-  apply auto
-  done
+apply (induct A)
+ apply blast
+apply clarsimp
+apply (drule_tac x = x in fold_msetG.insertI)
+apply auto
+done
 
 lemma fold_mset_empty[simp]: "fold_mset f z {#} = z"
-  unfolding fold_mset_def by blast
+unfolding fold_mset_def by blast
 
 locale left_commutative = 
-  fixes f :: "'a => 'b => 'b"
-  assumes left_commute: "f x (f y z) = f y (f x z)"
+fixes f :: "'a => 'b => 'b"
+assumes left_commute: "f x (f y z) = f y (f x z)"
 begin
 
 lemma fold_msetG_determ:
@@ -1375,37 +1371,37 @@
 lemma fold_mset_insert_aux:
   "(fold_msetG f z (A + {#x#}) v) =
     (\<exists>y. fold_msetG f z A y \<and> v = f x y)"
-  apply (rule iffI)
-   prefer 2
-   apply blast
-  apply (rule_tac A=A and f=f in fold_msetG_nonempty [THEN exE, standard])
-  apply (blast intro: fold_msetG_determ)
-  done
+apply (rule iffI)
+ prefer 2
+ apply blast
+apply (rule_tac A=A and f=f in fold_msetG_nonempty [THEN exE, standard])
+apply (blast intro: fold_msetG_determ)
+done
 
 lemma fold_mset_equality: "fold_msetG f z A y \<Longrightarrow> fold_mset f z A = y"
-  unfolding fold_mset_def by (blast intro: fold_msetG_determ)
+unfolding fold_mset_def by (blast intro: fold_msetG_determ)
 
 lemma fold_mset_insert:
-    "fold_mset f z (A + {#x#}) = f x (fold_mset f z A)"
-  apply (simp add: fold_mset_def fold_mset_insert_aux union_commute)  
-  apply (rule the_equality)
-   apply (auto cong add: conj_cong 
+  "fold_mset f z (A + {#x#}) = f x (fold_mset f z A)"
+apply (simp add: fold_mset_def fold_mset_insert_aux union_commute)  
+apply (rule the_equality)
+ apply (auto cong add: conj_cong 
      simp add: fold_mset_def [symmetric] fold_mset_equality fold_msetG_nonempty)
-  done
+done
 
 lemma fold_mset_insert_idem:
-    "fold_mset f z (A + {#a#}) = f a (fold_mset f z A)"
-  apply (simp add: fold_mset_def fold_mset_insert_aux)
-  apply (rule the_equality)
-   apply (auto cong add: conj_cong 
+  "fold_mset f z (A + {#a#}) = f a (fold_mset f z A)"
+apply (simp add: fold_mset_def fold_mset_insert_aux)
+apply (rule the_equality)
+ apply (auto cong add: conj_cong 
      simp add: fold_mset_def [symmetric] fold_mset_equality fold_msetG_nonempty)
-  done
+done
 
 lemma fold_mset_commute: "f x (fold_mset f z A) = fold_mset f (f x z) A"
-  by (induct A) (auto simp: fold_mset_insert left_commute [of x])
-  
+by (induct A) (auto simp: fold_mset_insert left_commute [of x])
+
 lemma fold_mset_single [simp]: "fold_mset f z {#x#} = f x z"
-  using fold_mset_insert [of z "{#}"] by simp
+using fold_mset_insert [of z "{#}"] by simp
 
 lemma fold_mset_union [simp]:
   "fold_mset f z (A+B) = fold_mset f (fold_mset f z A) B"
@@ -1424,7 +1420,7 @@
 lemma fold_mset_fusion:
   includes left_commutative g
   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"
-  by (induct A) auto
+by (induct A) auto
 
 lemma fold_mset_rec:
   assumes "a \<in># A" 
@@ -1454,30 +1450,30 @@
 definition [code func del]: "image_mset f == fold_mset (op + o single o f) {#}"
 
 interpretation image_left_comm: left_commutative ["op + o single o f"]
-  by (unfold_locales) (simp add:union_ac)
+by (unfold_locales) (simp add:union_ac)
 
 lemma image_mset_empty [simp, code func]: "image_mset f {#} = {#}"
-  by (simp add: image_mset_def)
+by (simp add: image_mset_def)
 
 lemma image_mset_single [simp, code func]: "image_mset f {#x#} = {#f x#}"
-  by (simp add: image_mset_def)
+by (simp add: image_mset_def)
 
 lemma image_mset_insert:
   "image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
-  by (simp add: image_mset_def add_ac)
+by (simp add: image_mset_def add_ac)
 
 lemma image_mset_union[simp, code func]:
   "image_mset f (M+N) = image_mset f M + image_mset f N"
-  apply (induct N)
-   apply simp
-  apply (simp add: union_assoc [symmetric] image_mset_insert)
-  done
+apply (induct N)
+ apply simp
+apply (simp add: union_assoc [symmetric] image_mset_insert)
+done
 
 lemma size_image_mset [simp]: "size (image_mset f M) = size M"
-  by (induct M) simp_all
+by (induct M) simp_all
 
 lemma image_mset_is_empty_iff [simp]: "image_mset f M = {#} \<longleftrightarrow> M = {#}"
-  by (cases M) auto
+by (cases M) auto
 
 
 syntax