--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/IsarOverview/Isar/Calc.thy Mon Sep 09 17:28:29 2002 +0200
@@ -0,0 +1,30 @@
+theory Calc = Main:
+
+axclass
+ group < zero, plus, minus
+ assoc: "(x + y) + z = x + (y + z)"
+ left_0: "0 + x = x"
+ left_minus: "-x + x = 0"
+
+theorem right_minus: "x + -x = (0::'a::group)"
+proof -
+ have "x + -x = (-(-x) + -x) + (x + -x)"
+ by (simp only: left_0 left_minus)
+ also have "... = -(-x) + ((-x + x) + -x)"
+ by (simp only: group.assoc)
+ also have "... = 0"
+ by (simp only: left_0 left_minus)
+ finally show ?thesis .
+qed
+
+
+lemma assumes R: "(a,b) \<in> R" "(b,c) \<in> R" "(c,d) \<in> R"
+ shows "(a,d) \<in> R\<^sup>*"
+proof -
+ have "(a,b) \<in> R\<^sup>*" ..
+ also have "(b,c) \<in> R\<^sup>*" ..
+ also have "(c,d) \<in> R\<^sup>*" ..
+ finally show ?thesis .
+qed
+
+end
\ No newline at end of file