author nipkow Wed Jul 10 16:07:52 2002 +0200 (2002-07-10 ago) changeset 13338 20ca66539bef parent 13337 f75dfc606ac7 child 13339 0f89104dd377
*** empty log message ***
     1.1 --- a/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Wed Jul 10 15:07:02 2002 +0200
1.2 +++ b/doc-src/TutorialI/IsarOverview/Isar/Logic.thy	Wed Jul 10 16:07:52 2002 +0200
1.3 @@ -714,7 +714,9 @@
1.4  "rot [x] = [x]"
1.5  "rot (x#y#zs) = y # rot(x#zs)"
1.6
1.7 -text{* The proof is trivial: all three cases go through by simplification.*}
1.8 +text{* In the first proof we set up each case explicitly, merely using
1.9 +pattern matching to abbreviate the statement: *}
1.10 +
1.11  lemma "length(rot xs) = length xs" (is "?P xs")
1.12  proof (induct xs rule: rot.induct)
1.13    show "?P []" by simp
1.14 @@ -724,12 +726,25 @@
1.15    fix x y zs assume "?P (x#zs)"
1.16    thus "?P (x#y#zs)" by simp
1.17  qed
1.18 -
1.19 -text{*\noindent This schema works for arbitrary induction rules instead of
1.20 +text{* This proof skeletons works for arbitrary induction rules, not just
1.21  @{thm[source]rot.induct}.
1.22
1.23 -Of course the above proof is simple enough that it could be condensed to*}
1.24 -(*<*)lemma "length(rot xs) = length xs"(*>*)
1.25 +In the following proof we rely on a default naming scheme for cases: they are
1.26 +called 1, 2, etc, unless they have been named explicitly. The latter happens
1.27 +only with datatypes and inductively defined sets, but not with recursive
1.28 +functions. *}
1.29 +
1.30 +lemma "xs \<noteq> [] \<Longrightarrow> rot xs = tl xs @ [hd xs]"
1.31 +proof (induct xs rule: rot.induct)
1.32 +  case 1 thus ?case by simp
1.33 +next
1.34 +  case 2 show ?case by simp
1.35 +next
1.36 +  case 3 thus ?case by simp
1.37 +qed
1.38 +
1.39 +text{*Of course both proofs are so simple that they can be condensed to*}
1.40 +(*<*)lemma "xs \<noteq> [] \<Longrightarrow> rot xs = tl xs @ [hd xs]"(*>*)
1.41  by (induct xs rule: rot.induct, simp_all)
1.42
1.43  (*<*)end(*>*)