# HG changeset patch
# User huffman
# Date 1338282780 -7200
# Node ID 0da831254551aabd743d2be824317e48973850d7
# Parent  9b9150033b5a0e12100412fcfff379bddecb5765
shortened more multiset proofs

diff -r 9b9150033b5a -r 0da831254551 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue May 29 10:30:47 2012 +0200
+++ b/src/HOL/Library/Multiset.thy	Tue May 29 11:13:00 2012 +0200
@@ -1542,87 +1542,54 @@
 context comp_fun_commute
 begin
 
+lemma fold_msetG_insertE_aux:
+  "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'"
+proof (induct set: fold_msetG)
+  case (insertI A y x) show ?case
+  proof (cases "x = a")
+    assume "x = a" with insertI show ?case by auto
+  next
+    assume "x \<noteq> a"
+    then obtain y' where y: "y = f a y'" and y': "fold_msetG f z (A - {#a#}) y'"
+      using insertI by auto
+    have "f x y = f a (f x y')"
+      unfolding y by (rule fun_left_comm)
+    moreover have "fold_msetG f z (A + {#x#} - {#a#}) (f x y')"
+      using y' and `x \<noteq> a`
+      by (simp add: diff_union_swap [symmetric] fold_msetG.insertI)
+    ultimately show ?case by fast
+  qed
+qed simp
+
+lemma fold_msetG_insertE:
+  assumes "fold_msetG f z (A + {#x#}) v"
+  obtains y where "v = f x y" and "fold_msetG f z A y"
+using assms by (auto dest: fold_msetG_insertE_aux [where a=x])
+
 lemma fold_msetG_determ:
   "fold_msetG f z A x \<Longrightarrow> fold_msetG f z A y \<Longrightarrow> y = x"
-proof (induct arbitrary: x y z rule: full_multiset_induct)
-  case (less M x\<^isub>1 x\<^isub>2 Z)
-  have IH: "\<forall>A. A < M \<longrightarrow> 
-    (\<forall>x x' x''. fold_msetG f x'' A x \<longrightarrow> fold_msetG f x'' A x'
-               \<longrightarrow> x' = x)" by fact
-  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+
-  show ?case
-  proof (rule fold_msetG.cases [OF Mfoldx\<^isub>1])
-    assume "M = {#}" and "x\<^isub>1 = Z"
-    then show ?case using Mfoldx\<^isub>2 by auto 
-  next
-    fix B b u
-    assume "M = B + {#b#}" and "x\<^isub>1 = f b u" and Bu: "fold_msetG f Z B u"
-    then have MBb: "M = B + {#b#}" and x\<^isub>1: "x\<^isub>1 = f b u" by auto
-    show ?case
-    proof (rule fold_msetG.cases [OF Mfoldx\<^isub>2])
-      assume "M = {#}" "x\<^isub>2 = Z"
-      then show ?case using Mfoldx\<^isub>1 by auto
-    next
-      fix C c v
-      assume "M = C + {#c#}" and "x\<^isub>2 = f c v" and Cv: "fold_msetG f Z C v"
-      then have MCc: "M = C + {#c#}" and x\<^isub>2: "x\<^isub>2 = f c v" by auto
-      then have CsubM: "C < M" by simp
-      from MBb have BsubM: "B < M" by simp
-      show ?case
-      proof cases
-        assume *: "b = c"
-        then have "B = C" using MBb MCc by auto
-        with * show ?thesis using Bu Cv x\<^isub>1 x\<^isub>2 CsubM IH by auto
-      next
-        assume diff: "b \<noteq> c"
-        let ?D = "B - {#c#}"
-        have cinB: "c \<in># B" and binC: "b \<in># C" using MBb MCc diff
-          by (auto intro: insert_noteq_member dest: sym)
-        have "B - {#c#} < B" using cinB by (rule mset_less_diff_self)
-        then have DsubM: "?D < M" using BsubM by (blast intro: order_less_trans)
-        from MBb MCc have "B + {#b#} = C + {#c#}" by blast
-        then have [simp]: "B + {#b#} - {#c#} = C"
-          using MBb MCc binC cinB by auto
-        have B: "B = ?D + {#c#}" and C: "C = ?D + {#b#}"
-          using MBb MCc diff binC cinB
-          by (auto simp: multiset_add_sub_el_shuffle)
-        then obtain d where Dfoldd: "fold_msetG f Z ?D d"
-          using fold_msetG_nonempty by iprover
-        then have "fold_msetG f Z B (f c d)" using cinB
-          by (rule Diff1_fold_msetG)
-        then have "f c d = u" using IH BsubM Bu by blast
-        moreover 
-        have "fold_msetG f Z C (f b d)" using binC cinB diff Dfoldd
-          by (auto simp: multiset_add_sub_el_shuffle 
-            dest: fold_msetG.insertI [where x=b])
-        then have "f b d = v" using IH CsubM Cv by blast
-        ultimately show ?thesis using x\<^isub>1 x\<^isub>2
-          by (auto simp: fun_left_comm)
-      qed
-    qed
-  qed
-qed
-        
-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 A1=A and f1=f in fold_msetG_nonempty [THEN exE])
-apply (blast intro: fold_msetG_determ)
-done
+proof (induct arbitrary: y set: fold_msetG)
+  case (insertI A y x v)
+  from `fold_msetG f z (A + {#x#}) v`
+  obtain y' where "v = f x y'" and "fold_msetG f z A y'"
+    by (rule fold_msetG_insertE)
+  from `fold_msetG f z A y'` have "y' = y" by (rule insertI)
+  with `v = f x y'` show "v = f x y" by simp
+qed fast
 
 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)
 
+lemma fold_msetG_fold_mset: "fold_msetG f z A (fold_mset f z A)"
+proof -
+  from fold_msetG_nonempty fold_msetG_determ
+  have "\<exists>!x. fold_msetG f z A x" by (rule ex_ex1I)
+  then show ?thesis unfolding fold_mset_def by (rule theI')
+qed
+
 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)
-apply (rule the_equality)
- apply (auto cong add: conj_cong 
-     simp add: fold_mset_def [symmetric] fold_mset_equality fold_msetG_nonempty)
-done
+by (intro fold_mset_equality fold_msetG.insertI fold_msetG_fold_mset)
 
 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 fun_left_comm [of x])