# 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 "\<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