1.1 --- a/doc-src/IsarOverview/Isar/Calc.thy	Tue May 26 13:40:49 2009 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,49 +0,0 @@
     1.4 -theory Calc imports Main begin
     1.5 -
     1.6 -subsection{* Chains of equalities *}
     1.7 -
     1.8 -axclass
     1.9 -  group < zero, plus, minus
    1.10 -  assoc:       "(x + y) + z = x + (y + z)"
    1.11 -  left_0:      "0 + x = x"
    1.12 -  left_minus:  "-x + x = 0"
    1.13 -
    1.14 -theorem right_minus: "x + -x = (0::'a::group)"
    1.15 -proof -
    1.16 -  have   "x + -x = (-(-x) + -x) + (x + -x)"
    1.17 -    by (simp only: left_0 left_minus)
    1.18 -  also have "... = -(-x) + ((-x + x) + -x)"
    1.19 -    by (simp only: group.assoc)
    1.20 -  also have "... = 0"
    1.21 -    by (simp only: left_0 left_minus)
    1.22 -  finally show ?thesis .
    1.23 -qed
    1.24 -
    1.25 -subsection{* Inequalities and substitution *}
    1.26 -
    1.27 -lemmas distrib = zadd_zmult_distrib zadd_zmult_distrib2
    1.28 -                 zdiff_zmult_distrib zdiff_zmult_distrib2
    1.29 -declare numeral_2_eq_2[simp]
    1.30 -
    1.31 -
    1.32 -lemma fixes a :: int shows "(a+b)\<twosuperior> \<le> 2*(a\<twosuperior> + b\<twosuperior>)"
    1.33 -proof -
    1.34 -       have "(a+b)\<twosuperior> \<le> (a+b)\<twosuperior> + (a-b)\<twosuperior>"  by simp
    1.35 -  also have "(a+b)\<twosuperior> \<le> a\<twosuperior> + b\<twosuperior> + 2*a*b"  by(simp add:distrib)
    1.36 -  also have "(a-b)\<twosuperior> = a\<twosuperior> + b\<twosuperior> - 2*a*b"  by(simp add:distrib)
    1.37 -  finally show ?thesis by simp
    1.38 -qed
    1.39 -
    1.40 -
    1.41 -subsection{* More transitivity *}
    1.42 -
    1.43 -lemma assumes R: "(a,b) \<in> R" "(b,c) \<in> R" "(c,d) \<in> R"
    1.44 -      shows "(a,d) \<in> R\<^sup>*"
    1.45 -proof -
    1.46 -       have "(a,b) \<in> R\<^sup>*" ..
    1.47 -  also have "(b,c) \<in> R\<^sup>*" ..
    1.48 -  also have "(c,d) \<in> R\<^sup>*" ..
    1.49 -  finally show ?thesis .
    1.50 -qed
    1.51 -
    1.52 -end
    1.53 \ No newline at end of file