# HG changeset patch
# User wenzelm
# Date 1023370462 -7200
# Node ID 050cd555d3a2a5392c0264991b5e9fa5d8b7be0e
# Parent  9dbee7f2aff71ec4c1f121ad55d0156a0583e79d
examples;

diff -r 9dbee7f2aff7 -r 050cd555d3a2 doc-src/IsarTut/Tutorial/Tutorial.thy
--- 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 *}