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(*>*)