# HG changeset patch # User kleing # Date 1197581745 -3600 # Node ID baa627b6f96242a1c7d17ea7c9826c5301afa810 # Parent 6067d838041a9ced5aba54e6d8a08f1f80053aa7 removed syntax in locale left_commutative diff -r 6067d838041a -r baa627b6f962 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Thu Dec 13 07:09:23 2007 +0100 +++ b/src/HOL/Library/Multiset.thy Thu Dec 13 22:35:45 2007 +0100 @@ -1159,15 +1159,15 @@ by (unfold foldM_def, blast) locale left_commutative = - fixes f :: "'a => 'b => 'b" (infixl "\" 70) - assumes left_commute: "x \ (y \ z) = y \ (x \ z)" + 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" 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 op \ x'' A x \ foldMG op \ x'' A x' + (\x x' x''. foldMG f x'' A x \ foldMG 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+ show ?case @@ -1176,16 +1176,16 @@ thus ?case using Mfoldx\<^isub>2 by auto next fix B b u - assume "M = B + {#b#}" and "x\<^isub>1 = b \ u" and Bu: "foldMG op \ Z B u" - hence MBb: "M = B + {#b#}" and x\<^isub>1: "x\<^isub>1 = b \ u" by auto + assume "M = B + {#b#}" and "x\<^isub>1 = f b u" and Bu: "foldMG 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]) 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 = c \ v" and Cv: "foldMG op \ Z C v" - hence MCc: "M = C + {#c#}" and x\<^isub>2: "x\<^isub>2 = c \ v" by auto + assume "M = C + {#c#}" and "x\<^isub>2 = f c v" and Cv: "foldMG 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 show ?case @@ -1208,14 +1208,14 @@ 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 (c \ d)" using cinB + hence "foldMG f Z B (f c d)" using cinB by (rule Diff1_foldMG) - hence "c \ d = u" using IH BsubM Bu by blast + hence "f c d = u" using IH BsubM Bu by blast moreover - have "foldMG f Z C (b \ d)" using binC cinB diff Dfoldd + have "foldMG 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]) - hence "b \ d = v" using IH CsubM Cv by blast + 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) qed @@ -1245,7 +1245,7 @@ done lemma (in left_commutative) foldM_insert_idem: - shows "foldM f z (A + {#a#}) = a \ foldM f z A" + 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