doc-src/TutorialI/IsarOverview/Isar/Calc.thy
author nipkow
Mon, 09 Sep 2002 17:28:29 +0200
changeset 13562 5b71e1408ac4
child 13613 531f1f524848
permissions -rw-r--r--
*** empty log message ***

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