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) |