# HG changeset patch # User kleing # Date 1199243447 -3600 # Node ID 6326138c1bd7bccd1a3760e9f491f6266581b2ab # Parent 89c7c22e64b443f79712506bb453b9dadc088be7 renamed foldM to fold_mset on general request added Tobias' lemmas on fold_mset (A+B) etc tuned default simp set for fold_mset diff -r 89c7c22e64b4 -r 6326138c1bd7 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Wed Jan 02 01:20:18 2008 +0100 +++ b/src/HOL/Library/Multiset.thy Wed Jan 02 04:10:47 2008 +0100 @@ -1121,70 +1121,70 @@ subsection {* The fold combinator *} text {* The intended behaviour is -@{text "foldM f z {#x\<^isub>1, ..., x\<^isub>n#} = f x\<^isub>1 (\ (f x\<^isub>n z)\)"} +@{text "fold_mset f z {#x\<^isub>1, ..., x\<^isub>n#} = f x\<^isub>1 (\ (f x\<^isub>n z)\)"} if @{text f} is associative-commutative. *} -(* the graph of foldM, z = the start element, f = folding function, +(* the graph of fold_mset, z = the start element, f = folding function, A the multiset, y the result *) inductive - foldMG :: "('a \ 'b \ 'b) \ 'b \ 'a multiset \ 'b \ bool" + fold_msetG :: "('a \ 'b \ 'b) \ 'b \ 'a multiset \ 'b \ bool" for f :: "'a \ 'b \ 'b" and z :: 'b where - emptyI [intro]: "foldMG f z {#} z" -| insertI [intro]: "foldMG f z A y \ foldMG f z (A + {#x#}) (f x y)" + emptyI [intro]: "fold_msetG f z {#} z" +| insertI [intro]: "fold_msetG f z A y \ fold_msetG f z (A + {#x#}) (f x y)" -inductive_cases empty_foldMGE [elim!]: "foldMG f z {#} x" -inductive_cases insert_foldMGE: "foldMG f z (A + {#}) y" +inductive_cases empty_fold_msetGE [elim!]: "fold_msetG f z {#} x" +inductive_cases insert_fold_msetGE: "fold_msetG f z (A + {#}) y" definition - foldM :: "('a \ 'b \ 'b) \ 'b \ 'a multiset \ 'b" + fold_mset :: "('a \ 'b \ 'b) \ 'b \ 'a multiset \ 'b" where - "foldM f z A \ THE x. foldMG f z A x" + "fold_mset f z A \ THE x. fold_msetG f z A x" -lemma Diff1_foldMG: - "\ foldMG f z (A - {#x#}) y; x \# A \ \ foldMG f z A (f x y)" - by (frule_tac x=x in foldMG.insertI, auto) +lemma Diff1_fold_msetG: + "\ fold_msetG f z (A - {#x#}) y; x \# A \ \ fold_msetG f z A (f x y)" + by (frule_tac x=x in fold_msetG.insertI, auto) -lemma foldMG_nonempty: "\x. foldMG f z A x" +lemma fold_msetG_nonempty: "\x. fold_msetG f z A x" apply (induct A) apply blast apply clarsimp - apply (drule_tac x=x in foldMG.insertI) + apply (drule_tac x=x in fold_msetG.insertI) apply auto done -lemma foldM_empty[simp]: "foldM f z {#} = z" - by (unfold foldM_def, blast) +lemma fold_mset_empty[simp]: "fold_mset f z {#} = z" + by (unfold fold_mset_def, blast) locale left_commutative = fixes f :: "'a => 'b => 'b" assumes left_commute: "f x (f y z) = f y (f x z)" -lemma (in left_commutative) foldMG_determ: - "\foldMG f z A x; foldMG f z A y\ \ y = x" +lemma (in left_commutative) fold_msetG_determ: + "\fold_msetG f z A x; fold_msetG f z A y\ \ y = x" proof (induct arbitrary: x y z rule: full_multiset_induct) case (less M x\<^isub>1 x\<^isub>2 Z) have IH: "\A. A \# M \ - (\x x' x''. foldMG f x'' A x \ foldMG f x'' A x' + (\x x' x''. fold_msetG f x'' A x \ fold_msetG f x'' A x' \ x' = x)" by fact - have Mfoldx\<^isub>1: "foldMG f Z M x\<^isub>1" and Mfoldx\<^isub>2: "foldMG f Z M x\<^isub>2" 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 foldMG.cases [OF Mfoldx\<^isub>1]) + proof (rule fold_msetG.cases [OF Mfoldx\<^isub>1]) assume "M = {#}" and "x\<^isub>1 = Z" thus ?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: "foldMG f Z B u" + assume "M = B + {#b#}" and "x\<^isub>1 = f b u" and Bu: "fold_msetG f Z B u" hence MBb: "M = B + {#b#}" and x\<^isub>1: "x\<^isub>1 = f b u" by auto show ?case - proof (rule foldMG.cases [OF Mfoldx\<^isub>2]) + proof (rule fold_msetG.cases [OF Mfoldx\<^isub>2]) assume "M = {#}" "x\<^isub>2 = Z" thus ?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: "foldMG f Z C v" + assume "M = C + {#c#}" and "x\<^isub>2 = f c v" and Cv: "fold_msetG f Z C v" hence MCc: "M = C + {#c#}" and x\<^isub>2: "x\<^isub>2 = f c v" by auto hence CsubM: "C \# M" by simp from MBb have BsubM: "B \# M" by simp @@ -1206,15 +1206,15 @@ 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: "foldMG f Z ?D d" - using foldMG_nonempty by iprover - hence "foldMG f Z B (f c d)" using cinB - by (rule Diff1_foldMG) + then obtain d where Dfoldd: "fold_msetG f Z ?D d" + using fold_msetG_nonempty by iprover + hence "fold_msetG f Z B (f c d)" using cinB + by (rule Diff1_fold_msetG) hence "f c d = u" using IH BsubM Bu by blast moreover - have "foldMG f Z C (f b d)" using binC cinB diff Dfoldd + have "fold_msetG f Z C (f b d)" using binC cinB diff Dfoldd by (auto simp: multiset_add_sub_el_shuffle - dest: foldMG.insertI [where x=b]) + dest: fold_msetG.insertI [where x=b]) hence "f b d = v" using IH CsubM Cv by blast ultimately show ?thesis using x\<^isub>1 x\<^isub>2 by (auto simp: left_commute) @@ -1223,51 +1223,68 @@ qed qed -lemma (in left_commutative) foldM_insert_aux: " - (foldMG f z (A + {#x#}) v) = - (\y. foldMG f z A y \ v = f x y)" +lemma (in left_commutative) fold_mset_insert_aux: " + (fold_msetG f z (A + {#x#}) v) = + (\y. fold_msetG f z A y \ v = f x y)" apply (rule iffI) prefer 2 apply blast - apply (rule_tac A=A and f=f in foldMG_nonempty [THEN exE, standard]) - apply (blast intro: foldMG_determ) + apply (rule_tac A=A and f=f in fold_msetG_nonempty [THEN exE, standard]) + apply (blast intro: fold_msetG_determ) done -lemma (in left_commutative) foldM_equality: "foldMG f z A y \ foldM f z A = y" - by (unfold foldM_def) (blast intro: foldMG_determ) +lemma (in left_commutative) fold_mset_equality: "fold_msetG f z A y \ fold_mset f z A = y" + by (unfold fold_mset_def) (blast intro: fold_msetG_determ) -lemma (in left_commutative) foldM_insert[simp]: - "foldM f z (A + {#x#}) = f x (foldM f z A)" - apply (simp add: foldM_def foldM_insert_aux union_commute) +lemma (in left_commutative) 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 - simp add: foldM_def [symmetric] foldM_equality foldMG_nonempty) + simp add: fold_mset_def [symmetric] fold_mset_equality fold_msetG_nonempty) + done + +lemma (in left_commutative) fold_mset_insert_idem: + shows "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 -lemma (in left_commutative) foldM_insert_idem: - shows "foldM f z (A + {#a#}) = f a (foldM f z A)" - apply (simp add: foldM_def foldM_insert_aux) - apply (rule the_equality) - apply (auto cong add: conj_cong - simp add: foldM_def [symmetric] foldM_equality foldMG_nonempty) - done +lemma (in left_commutative) 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]) + +lemma (in left_commutative) fold_mset_single [simp]: + "fold_mset f z {#x#} = f x z" +using fold_mset_insert[of z "{#}"] by simp -lemma (in left_commutative) foldM_fusion: +lemma (in left_commutative) fold_mset_union [simp]: + "fold_mset f z (A+B) = fold_mset f (fold_mset f z A) B" +proof (induct A) + case empty thus ?case by simp +next + case (add A x) + have "A + {#x#} + B = (A+B) + {#x#}" by(simp add:union_ac) + hence "fold_mset f z (A + {#x#} + B) = f x (fold_mset f z (A + B))" + by (simp add: fold_mset_insert) + also have "\ = fold_mset f (fold_mset f z (A + {#x#})) B" + by (simp add: fold_mset_commute[of x,symmetric] add fold_mset_insert) + finally show ?case . +qed + +lemma (in left_commutative) fold_mset_fusion: includes left_commutative g - shows "\\x y. h (g x y) = f x (h y) \ \ h (foldM g w A) = foldM f (h w) A" + shows "\\x y. h (g x y) = f x (h y) \ \ h (fold_mset g w A) = fold_mset f (h w) A" by (induct A, auto) -lemma (in left_commutative) foldM_commute: - "f x (foldM f z A) = foldM f (f x z) A" - by (induct A, auto simp: left_commute [of x]) - -lemma (in left_commutative) foldM_rec: +lemma (in left_commutative) fold_mset_rec: assumes a: "a \# A" - shows "foldM f z A = f a (foldM f z (A - {#a#}))" + shows "fold_mset f z A = f a (fold_mset f z (A - {#a#}))" proof - from a obtain A' where "A = A' + {#a#}" by (blast dest: multi_member_split) thus ?thesis by simp qed - end