equal
deleted
inserted
replaced
31 \begin{isamarkuptxt}% |
31 \begin{isamarkuptxt}% |
32 \noindent |
32 \noindent |
33 It was not proved automatically because of the special nature of \isa{{\isacharminus}} |
33 It was not proved automatically because of the special nature of \isa{{\isacharminus}} |
34 on \isa{nat}. This requires more arithmetic than is tried by default:% |
34 on \isa{nat}. This requires more arithmetic than is tried by default:% |
35 \end{isamarkuptxt}% |
35 \end{isamarkuptxt}% |
36 \isacommand{by}{\isacharparenleft}arith{\isacharparenright}% |
36 \isacommand{apply}{\isacharparenleft}arith{\isacharparenright}\isanewline |
|
37 \isacommand{done}% |
37 \begin{isamarkuptext}% |
38 \begin{isamarkuptext}% |
38 \noindent |
39 \noindent |
39 Because \isacommand{recdef}'s termination prover involves simplification, |
40 Because \isacommand{recdef}'s termination prover involves simplification, |
40 we include with our second attempt the hint to use \isa{termi{\isacharunderscore}lem} as |
41 we include with our second attempt the hint to use \isa{termi{\isacharunderscore}lem} as |
41 a simplification rule:% |
42 a simplification rule:% |
49 This time everything works fine. Now \isa{g{\isachardot}simps} contains precisely |
50 This time everything works fine. Now \isa{g{\isachardot}simps} contains precisely |
50 the stated recursion equation for \isa{g} and they are simplification |
51 the stated recursion equation for \isa{g} and they are simplification |
51 rules. Thus we can automatically prove% |
52 rules. Thus we can automatically prove% |
52 \end{isamarkuptext}% |
53 \end{isamarkuptext}% |
53 \isacommand{theorem}\ {\isachardoublequote}g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{0}{\isacharparenright}\ {\isacharequal}\ g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{1}{\isacharparenright}{\isachardoublequote}\isanewline |
54 \isacommand{theorem}\ {\isachardoublequote}g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{0}{\isacharparenright}\ {\isacharequal}\ g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{1}{\isacharparenright}{\isachardoublequote}\isanewline |
54 \isacommand{by}{\isacharparenleft}simp{\isacharparenright}% |
55 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline |
|
56 \isacommand{done}% |
55 \begin{isamarkuptext}% |
57 \begin{isamarkuptext}% |
56 \noindent |
58 \noindent |
57 More exciting theorems require induction, which is discussed below. |
59 More exciting theorems require induction, which is discussed below. |
58 |
60 |
59 If the termination proof requires a new lemma that is of general use, you can |
61 If the termination proof requires a new lemma that is of general use, you can |