doc-src/IsarOverview/Isar/Calc.thy

added inner syntax mode, includes former type_mode and is_stmt;

theory Calc imports Main begin

subsection{* Chains of equalities *}

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

subsection{* Inequalities and substitution *}

lemmas distrib = zadd_zmult_distrib zadd_zmult_distrib2
                 zdiff_zmult_distrib zdiff_zmult_distrib2
declare numeral_2_eq_2[simp]


lemma fixes a :: int shows "(a+b)\<twosuperior> \<le> 2*(a\<twosuperior> + b\<twosuperior>)"
proof -
       have "(a+b)\<twosuperior> \<le> (a+b)\<twosuperior> + (a-b)\<twosuperior>"  by simp
  also have "(a+b)\<twosuperior> \<le> a\<twosuperior> + b\<twosuperior> + 2*a*b"  by(simp add:distrib)
  also have "(a-b)\<twosuperior> = a\<twosuperior> + b\<twosuperior> - 2*a*b"  by(simp add:distrib)
  finally show ?thesis by simp
qed


subsection{* More transitivity *}

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