equal
deleted
inserted
replaced
705 also have "... = y \<cdot> (z \<cdot> x)" by (simp only: assoc) 
705 also have "... = y \<cdot> (z \<cdot> x)" by (simp only: assoc) 
706 also have "z \<cdot> x = x \<cdot> z" by (simp only: commute) 
706 also have "z \<cdot> x = x \<cdot> z" by (simp only: commute) 
707 finally show ?thesis . 
707 finally show ?thesis . 
708 qed 
708 qed 
709 
709 
710 lemma (in ACe) 
710 lemmas (in ACe) AC = assoc commute left_commute 
711 AC: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)" "x \<cdot> y = y \<cdot> x" "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)" 

712 by (rule assoc, rule commute, rule left_commute) (* FIXME localize "lemmas" (!??) *) 

713 
711 
714 lemma (in ACe) left_ident [simp]: "e \<cdot> x = x" 
712 lemma (in ACe) left_ident [simp]: "e \<cdot> x = x" 
715 proof  
713 proof  
716 have "x \<cdot> e = x" by (rule ident) 
714 have "x \<cdot> e = x" by (rule ident) 
717 thus ?thesis by (subst commute) 
715 thus ?thesis by (subst commute) 