doc-src/TutorialI/Inductive/Advanced.thy
changeset 10426 469f19c4bf97
parent 10370 99bd3e902979
child 10468 87dda999deca
     1.1 --- a/doc-src/TutorialI/Inductive/Advanced.thy	Fri Nov 10 09:17:54 2000 +0100
     1.2 +++ b/doc-src/TutorialI/Inductive/Advanced.thy	Fri Nov 10 15:05:09 2000 +0100
     1.3 @@ -1,5 +1,24 @@
     1.4  (* ID:         $Id$ *)
     1.5 -theory Advanced = Main:
     1.6 +theory Advanced = Even:
     1.7 +
     1.8 +text{* We completely forgot about "rule inversion", or whatever we may want
     1.9 +to call it. Just as a demo I include the two forms that Markus has made available. First the one for binding the result to a name *}
    1.10 +
    1.11 +inductive_cases even_cases [elim!]:
    1.12 +  "Suc(Suc n) \<in> even"
    1.13 +
    1.14 +thm even_cases;
    1.15 +
    1.16 +text{*and now the one for local usage:*}
    1.17 +
    1.18 +lemma "Suc(Suc n) \<in> even \<Longrightarrow> n \<in> even";
    1.19 +by(ind_cases "Suc(Suc n) \<in> even");
    1.20 +
    1.21 +text{*Both forms accept lists of strings.
    1.22 +
    1.23 +Hope you can find some more exciting examples, although these may do
    1.24 +*}
    1.25 +
    1.26  
    1.27  datatype 'f "term" = Apply 'f "'f term list"
    1.28