src/HOL/Library/Multiset.thy
changeset 48010 0da831254551
parent 48009 9b9150033b5a
child 48011 391439b10100
     1.1 --- a/src/HOL/Library/Multiset.thy	Tue May 29 10:30:47 2012 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Tue May 29 11:13:00 2012 +0200
     1.3 @@ -1542,87 +1542,54 @@
     1.4  context comp_fun_commute
     1.5  begin
     1.6  
     1.7 +lemma fold_msetG_insertE_aux:
     1.8 +  "fold_msetG f z A y \<Longrightarrow> a \<in># A \<Longrightarrow> \<exists>y'. y = f a y' \<and> fold_msetG f z (A - {#a#}) y'"
     1.9 +proof (induct set: fold_msetG)
    1.10 +  case (insertI A y x) show ?case
    1.11 +  proof (cases "x = a")
    1.12 +    assume "x = a" with insertI show ?case by auto
    1.13 +  next
    1.14 +    assume "x \<noteq> a"
    1.15 +    then obtain y' where y: "y = f a y'" and y': "fold_msetG f z (A - {#a#}) y'"
    1.16 +      using insertI by auto
    1.17 +    have "f x y = f a (f x y')"
    1.18 +      unfolding y by (rule fun_left_comm)
    1.19 +    moreover have "fold_msetG f z (A + {#x#} - {#a#}) (f x y')"
    1.20 +      using y' and `x \<noteq> a`
    1.21 +      by (simp add: diff_union_swap [symmetric] fold_msetG.insertI)
    1.22 +    ultimately show ?case by fast
    1.23 +  qed
    1.24 +qed simp
    1.25 +
    1.26 +lemma fold_msetG_insertE:
    1.27 +  assumes "fold_msetG f z (A + {#x#}) v"
    1.28 +  obtains y where "v = f x y" and "fold_msetG f z A y"
    1.29 +using assms by (auto dest: fold_msetG_insertE_aux [where a=x])
    1.30 +
    1.31  lemma fold_msetG_determ:
    1.32    "fold_msetG f z A x \<Longrightarrow> fold_msetG f z A y \<Longrightarrow> y = x"
    1.33 -proof (induct arbitrary: x y z rule: full_multiset_induct)
    1.34 -  case (less M x\<^isub>1 x\<^isub>2 Z)
    1.35 -  have IH: "\<forall>A. A < M \<longrightarrow> 
    1.36 -    (\<forall>x x' x''. fold_msetG f x'' A x \<longrightarrow> fold_msetG f x'' A x'
    1.37 -               \<longrightarrow> x' = x)" by fact
    1.38 -  have Mfoldx\<^isub>1: "fold_msetG f Z M x\<^isub>1" and Mfoldx\<^isub>2: "fold_msetG f Z M x\<^isub>2" by fact+
    1.39 -  show ?case
    1.40 -  proof (rule fold_msetG.cases [OF Mfoldx\<^isub>1])
    1.41 -    assume "M = {#}" and "x\<^isub>1 = Z"
    1.42 -    then show ?case using Mfoldx\<^isub>2 by auto 
    1.43 -  next
    1.44 -    fix B b u
    1.45 -    assume "M = B + {#b#}" and "x\<^isub>1 = f b u" and Bu: "fold_msetG f Z B u"
    1.46 -    then have MBb: "M = B + {#b#}" and x\<^isub>1: "x\<^isub>1 = f b u" by auto
    1.47 -    show ?case
    1.48 -    proof (rule fold_msetG.cases [OF Mfoldx\<^isub>2])
    1.49 -      assume "M = {#}" "x\<^isub>2 = Z"
    1.50 -      then show ?case using Mfoldx\<^isub>1 by auto
    1.51 -    next
    1.52 -      fix C c v
    1.53 -      assume "M = C + {#c#}" and "x\<^isub>2 = f c v" and Cv: "fold_msetG f Z C v"
    1.54 -      then have MCc: "M = C + {#c#}" and x\<^isub>2: "x\<^isub>2 = f c v" by auto
    1.55 -      then have CsubM: "C < M" by simp
    1.56 -      from MBb have BsubM: "B < M" by simp
    1.57 -      show ?case
    1.58 -      proof cases
    1.59 -        assume *: "b = c"
    1.60 -        then have "B = C" using MBb MCc by auto
    1.61 -        with * show ?thesis using Bu Cv x\<^isub>1 x\<^isub>2 CsubM IH by auto
    1.62 -      next
    1.63 -        assume diff: "b \<noteq> c"
    1.64 -        let ?D = "B - {#c#}"
    1.65 -        have cinB: "c \<in># B" and binC: "b \<in># C" using MBb MCc diff
    1.66 -          by (auto intro: insert_noteq_member dest: sym)
    1.67 -        have "B - {#c#} < B" using cinB by (rule mset_less_diff_self)
    1.68 -        then have DsubM: "?D < M" using BsubM by (blast intro: order_less_trans)
    1.69 -        from MBb MCc have "B + {#b#} = C + {#c#}" by blast
    1.70 -        then have [simp]: "B + {#b#} - {#c#} = C"
    1.71 -          using MBb MCc binC cinB by auto
    1.72 -        have B: "B = ?D + {#c#}" and C: "C = ?D + {#b#}"
    1.73 -          using MBb MCc diff binC cinB
    1.74 -          by (auto simp: multiset_add_sub_el_shuffle)
    1.75 -        then obtain d where Dfoldd: "fold_msetG f Z ?D d"
    1.76 -          using fold_msetG_nonempty by iprover
    1.77 -        then have "fold_msetG f Z B (f c d)" using cinB
    1.78 -          by (rule Diff1_fold_msetG)
    1.79 -        then have "f c d = u" using IH BsubM Bu by blast
    1.80 -        moreover 
    1.81 -        have "fold_msetG f Z C (f b d)" using binC cinB diff Dfoldd
    1.82 -          by (auto simp: multiset_add_sub_el_shuffle 
    1.83 -            dest: fold_msetG.insertI [where x=b])
    1.84 -        then have "f b d = v" using IH CsubM Cv by blast
    1.85 -        ultimately show ?thesis using x\<^isub>1 x\<^isub>2
    1.86 -          by (auto simp: fun_left_comm)
    1.87 -      qed
    1.88 -    qed
    1.89 -  qed
    1.90 -qed
    1.91 -        
    1.92 -lemma fold_mset_insert_aux:
    1.93 -  "(fold_msetG f z (A + {#x#}) v) =
    1.94 -    (\<exists>y. fold_msetG f z A y \<and> v = f x y)"
    1.95 -apply (rule iffI)
    1.96 - prefer 2
    1.97 - apply blast
    1.98 -apply (rule_tac A1=A and f1=f in fold_msetG_nonempty [THEN exE])
    1.99 -apply (blast intro: fold_msetG_determ)
   1.100 -done
   1.101 +proof (induct arbitrary: y set: fold_msetG)
   1.102 +  case (insertI A y x v)
   1.103 +  from `fold_msetG f z (A + {#x#}) v`
   1.104 +  obtain y' where "v = f x y'" and "fold_msetG f z A y'"
   1.105 +    by (rule fold_msetG_insertE)
   1.106 +  from `fold_msetG f z A y'` have "y' = y" by (rule insertI)
   1.107 +  with `v = f x y'` show "v = f x y" by simp
   1.108 +qed fast
   1.109  
   1.110  lemma fold_mset_equality: "fold_msetG f z A y \<Longrightarrow> fold_mset f z A = y"
   1.111  unfolding fold_mset_def by (blast intro: fold_msetG_determ)
   1.112  
   1.113 +lemma fold_msetG_fold_mset: "fold_msetG f z A (fold_mset f z A)"
   1.114 +proof -
   1.115 +  from fold_msetG_nonempty fold_msetG_determ
   1.116 +  have "\<exists>!x. fold_msetG f z A x" by (rule ex_ex1I)
   1.117 +  then show ?thesis unfolding fold_mset_def by (rule theI')
   1.118 +qed
   1.119 +
   1.120  lemma fold_mset_insert:
   1.121    "fold_mset f z (A + {#x#}) = f x (fold_mset f z A)"
   1.122 -apply (simp add: fold_mset_def fold_mset_insert_aux)
   1.123 -apply (rule the_equality)
   1.124 - apply (auto cong add: conj_cong 
   1.125 -     simp add: fold_mset_def [symmetric] fold_mset_equality fold_msetG_nonempty)
   1.126 -done
   1.127 +by (intro fold_mset_equality fold_msetG.insertI fold_msetG_fold_mset)
   1.128  
   1.129  lemma fold_mset_commute: "f x (fold_mset f z A) = fold_mset f (f x z) A"
   1.130  by (induct A) (auto simp: fold_mset_insert fun_left_comm [of x])