1.1 --- a/src/HOL/Library/Multiset.thy	Tue May 29 10:08:31 2012 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Tue May 29 10:30:47 2012 +0200
     1.3 @@ -547,67 +547,18 @@
     1.4  apply (drule_tac a = a in mk_disjoint_insert, auto)
     1.5  done
     1.6  
     1.7 -lemma rep_multiset_induct_aux:
     1.8 -assumes 1: "P (\<lambda>a. (0::nat))"
     1.9 -  and 2: "!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))"
    1.10 -shows "\<forall>f. f \<in> multiset --> setsum f {x. f x \<noteq> 0} = n --> P f"
    1.11 -apply (unfold multiset_def)
    1.12 -apply (induct_tac n, simp, clarify)
    1.13 - apply (subgoal_tac "f = (\<lambda>a.0)")
    1.14 -  apply simp
    1.15 -  apply (rule 1)
    1.16 - apply (rule ext, force, clarify)
    1.17 -apply (frule setsum_SucD, clarify)
    1.18 -apply (rename_tac a)
    1.19 -apply (subgoal_tac "finite {x. (f (a := f a - 1)) x > 0}")
    1.20 - prefer 2
    1.21 - apply (rule finite_subset)
    1.22 -  prefer 2
    1.23 -  apply assumption
    1.24 - apply simp
    1.25 - apply blast
    1.26 -apply (subgoal_tac "f = (f (a := f a - 1))(a := (f (a := f a - 1)) a + 1)")
    1.27 - prefer 2
    1.28 - apply (rule ext)
    1.29 - apply (simp (no_asm_simp))
    1.30 - apply (erule ssubst, rule 2 [unfolded multiset_def], blast)
    1.31 -apply (erule allE, erule impE, erule_tac [2] mp, blast)
    1.32 -apply (simp (no_asm_simp) add: setsum_decr del: fun_upd_apply One_nat_def)
    1.33 -apply (subgoal_tac "{x. x \<noteq> a --> f x \<noteq> 0} = {x. f x \<noteq> 0}")
    1.34 - prefer 2
    1.35 - apply blast
    1.36 -apply (subgoal_tac "{x. x \<noteq> a \<and> f x \<noteq> 0} = {x. f x \<noteq> 0} - {a}")
    1.37 - prefer 2
    1.38 - apply blast
    1.39 -apply (simp add: le_imp_diff_is_add setsum_diff1_nat cong: conj_cong)
    1.40 -done
    1.41 -
    1.42 -theorem rep_multiset_induct:
    1.43 -  "f \<in> multiset ==> P (\<lambda>a. 0) ==>
    1.44 -    (!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))) ==> P f"
    1.45 -using rep_multiset_induct_aux by blast
    1.46 -
    1.47  theorem multiset_induct [case_names empty add, induct type: multiset]:
    1.48 -assumes empty: "P {#}"
    1.49 -  and add: "!!M x. P M ==> P (M + {#x#})"
    1.50 -shows "P M"
    1.51 -proof -
    1.52 -  note defns = plus_multiset_def single_def zero_multiset_def
    1.53 -  note add' = add [unfolded defns, simplified]
    1.54 -  have aux: "\<And>a::'a. count (Abs_multiset (\<lambda>b. if b = a then 1 else 0)) =
    1.55 -    (\<lambda>b. if b = a then 1 else 0)" by (simp add: Abs_multiset_inverse in_multiset) 
    1.56 -  show ?thesis
    1.57 -    apply (rule count_inverse [THEN subst])
    1.58 -    apply (rule count [THEN rep_multiset_induct])
    1.59 -     apply (rule empty [unfolded defns])
    1.60 -    apply (subgoal_tac "f(b := f b + 1) = (\<lambda>a. f a + (if a=b then 1 else 0))")
    1.61 -     prefer 2
    1.62 -     apply (simp add: fun_eq_iff)
    1.63 -    apply (erule ssubst)
    1.64 -    apply (erule Abs_multiset_inverse [THEN subst])
    1.65 -    apply (drule add')
    1.66 -    apply (simp add: aux)
    1.67 -    done
    1.68 +  assumes empty: "P {#}"
    1.69 +  assumes add: "\<And>M x. P M \<Longrightarrow> P (M + {#x#})"
    1.70 +  shows "P M"
    1.71 +proof (induct n \<equiv> "size M" arbitrary: M)
    1.72 +  case 0 thus "P M" by (simp add: empty)
    1.73 +next
    1.74 +  case (Suc k)
    1.75 +  obtain N x where "M = N + {#x#}"
    1.76 +    using `Suc k = size M` [symmetric]
    1.77 +    using size_eq_Suc_imp_eq_union by fast
    1.78 +  with Suc add show "P M" by simp
    1.79  qed
    1.80  
    1.81  lemma multi_nonempty_split: "M \<noteq> {#} \<Longrightarrow> \<exists>A a. M = A + {#a#}"
    1.82 @@ -617,20 +568,10 @@
    1.83  assumes em:  "M = {#} \<Longrightarrow> P"
    1.84  assumes add: "\<And>N x. M = N + {#x#} \<Longrightarrow> P"
    1.85  shows "P"
    1.86 -proof (cases "M = {#}")
    1.87 -  assume "M = {#}" then show ?thesis using em by simp
    1.88 -next
    1.89 -  assume "M \<noteq> {#}"
    1.90 -  then obtain M' m where "M = M' + {#m#}" 
    1.91 -    by (blast dest: multi_nonempty_split)
    1.92 -  then show ?thesis using add by simp
    1.93 -qed
    1.94 +using assms by (induct M) simp_all
    1.95  
    1.96  lemma multi_member_split: "x \<in># M \<Longrightarrow> \<exists>A. M = A + {#x#}"
    1.97 -apply (cases M)
    1.98 - apply simp
    1.99 -apply (rule_tac x="M - {#x#}" in exI, simp)
   1.100 -done
   1.101 +by (rule_tac x="M - {#x#}" in exI, simp)
   1.102  
   1.103  lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B - {#c#} \<noteq> B"
   1.104  by (cases "B = {#}") (auto dest: multi_member_split)