*** empty log message ***
authornipkow
Wed Jul 10 16:07:52 2002 +0200 (2002-07-10 ago)
changeset 1333820ca66539bef
parent 13337 f75dfc606ac7
child 13339 0f89104dd377
*** empty log message ***
doc-src/TutorialI/IsarOverview/Isar/Logic.thy
     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(*>*)