summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | kleing |

Thu, 13 Dec 2007 22:35:45 +0100 | |

changeset 25623 | baa627b6f962 |

parent 25622 | 6067d838041a |

child 25624 | 04b67ee73327 |

removed syntax in locale left_commutative

--- 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 "\<cdot>" 70) - assumes left_commute: "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> 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: "\<lbrakk>foldMG f z A x; foldMG f z A y\<rbrakk> \<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 \<subset># M \<longrightarrow> - (\<forall>x x' x''. foldMG op \<cdot> x'' A x \<longrightarrow> foldMG op \<cdot> x'' A x' + (\<forall>x x' x''. foldMG f x'' A x \<longrightarrow> foldMG f x'' A x' \<longrightarrow> 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 \<cdot> u" and Bu: "foldMG op \<cdot> Z B u" - hence MBb: "M = B + {#b#}" and x\<^isub>1: "x\<^isub>1 = b \<cdot> 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 \<cdot> v" and Cv: "foldMG op \<cdot> Z C v" - hence MCc: "M = C + {#c#}" and x\<^isub>2: "x\<^isub>2 = c \<cdot> 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 \<subset># M" by simp from MBb have BsubM: "B \<subset># 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 \<cdot> d)" using cinB + hence "foldMG f Z B (f c d)" using cinB by (rule Diff1_foldMG) - hence "c \<cdot> 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 \<cdot> 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 \<cdot> 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 \<cdot> 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