# HG changeset patch
# User nipkow
# Date 1026310072 -7200
# Node ID 20ca66539bef00bfb7e08d472c7a321acf320123
# Parent  f75dfc606ac76766d04d6c73d306cf0e1dc7e95a
*** empty log message ***

diff -r f75dfc606ac7 -r 20ca66539bef doc-src/TutorialI/IsarOverview/Isar/Logic.thy
--- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Wed Jul 10 15:07:02 2002 +0200
+++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Wed Jul 10 16:07:52 2002 +0200
@@ -714,7 +714,9 @@
 "rot [x] = [x]"
 "rot (x#y#zs) = y # rot(x#zs)"
 
-text{* The proof is trivial: all three cases go through by simplification.*}
+text{* In the first proof we set up each case explicitly, merely using
+pattern matching to abbreviate the statement: *}
+
 lemma "length(rot xs) = length xs" (is "?P xs")
 proof (induct xs rule: rot.induct)
   show "?P []" by simp
@@ -724,12 +726,25 @@
   fix x y zs assume "?P (x#zs)"
   thus "?P (x#y#zs)" by simp
 qed
-
-text{*\noindent This schema works for arbitrary induction rules instead of
+text{* This proof skeletons works for arbitrary induction rules, not just
 @{thm[source]rot.induct}.
 
-Of course the above proof is simple enough that it could be condensed to*}
-(*<*)lemma "length(rot xs) = length xs"(*>*)
+In the following proof we rely on a default naming scheme for cases: they are
+called 1, 2, etc, unless they have been named explicitly. The latter happens
+only with datatypes and inductively defined sets, but not with recursive
+functions. *}
+
+lemma "xs \<noteq> [] \<Longrightarrow> rot xs = tl xs @ [hd xs]"
+proof (induct xs rule: rot.induct)
+  case 1 thus ?case by simp
+next
+  case 2 show ?case by simp
+next
+  case 3 thus ?case by simp
+qed
+
+text{*Of course both proofs are so simple that they can be condensed to*}
+(*<*)lemma "xs \<noteq> [] \<Longrightarrow> rot xs = tl xs @ [hd xs]"(*>*)
 by (induct xs rule: rot.induct, simp_all)
 
 (*<*)end(*>*)