*** empty log message ***
Wed, 10 Jul 2002 16:07:52 +0200
changeset 13338 20ca66539bef
parent 13337 f75dfc606ac7
child 13339 0f89104dd377
*** empty log message ***
--- 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
-text{*\noindent This schema works for arbitrary induction rules instead of
+text{* This proof skeletons works for arbitrary induction rules, not just
-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
+  case 2 show ?case by simp
+  case 3 thus ?case by simp
+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)