author wenzelm Thu, 06 Jun 2002 15:34:22 +0200 changeset 13205 050cd555d3a2 parent 13204 9dbee7f2aff7 child 13206 90e5852e55e6
examples;
```--- a/doc-src/IsarTut/Tutorial/Tutorial.thy	Thu Jun 06 14:50:48 2002 +0200
+++ b/doc-src/IsarTut/Tutorial/Tutorial.thy	Thu Jun 06 15:34:22 2002 +0200
@@ -5,6 +5,42 @@

chapter {* Introduction *}

+section {* Step-by-step examples *}
+
+subsection {* Summing natural numbers *}
+
+theorem "2 * (\<Sum>i < n + 1. i) = n * (n + 1)"  (is "?P n")
+proof (induct n)
+  case 0
+  then show "?P 0" by simp
+next
+  case (Suc n)
+  let "?S n = _" = "?P n"
+  have "?S (n + 1) = ?S n + 2 * (n + 1)" by simp
+  also have "?S n = n * (n + 1)" .
+  also have "\<dots> + 2 * (n + 1) = (n + 1) * (n + 2)" by simp
+  finally show "?P (Suc n)" by simp
+qed
+
+theorem "2 * (\<Sum>i < n + 1. i) = n * (n + 1)"
+proof (induct n)
+  case 0
+  then show ?case by simp
+next
+  case Suc
+  then show ?case by simp
+qed
+
+theorem "2 * (\<Sum>i < n + 1. i) = n * (n + 1)"
+  by (induct n) simp_all
+
+theorem "2 * (\<Sum>i < n + 1. i) = n * (n + 1)"
+  apply (induct n)
+   apply simp_all
+  done
+
+
+
chapter {* Interaction and debugging *}

chapter {* Calculational reasoning *}```