doc-src/TutorialI/Recdef/termination.thy
 author nipkow Wed Dec 13 09:39:53 2000 +0100 (2000-12-13) changeset 10654 458068404143 parent 10522 ed3964d1f1a4 child 10795 9e888d60d3e5 permissions -rw-r--r--
*** empty log message ***
     1 (*<*)

     2 theory termination = examples:

     3 (*>*)

     4

     5 text{*

     6 When a function is defined via \isacommand{recdef}, Isabelle tries to prove

     7 its termination with the help of the user-supplied measure.  All of the above

     8 examples are simple enough that Isabelle can prove automatically that the

     9 measure of the argument goes down in each recursive call. As a result,

    10 $f$@{text".simps"} will contain the defining equations (or variants derived

    11 from them) as theorems. For example, look (via \isacommand{thm}) at

    12 @{thm[source]sep.simps} and @{thm[source]sep1.simps} to see that they define

    13 the same function. What is more, those equations are automatically declared as

    14 simplification rules.

    15

    16 In general, Isabelle may not be able to prove all termination conditions

    17 (there is one for each recursive call) automatically. For example,

    18 termination of the following artificial function

    19 *}

    20

    21 consts f :: "nat\<times>nat \<Rightarrow> nat";

    22 recdef f "measure(\<lambda>(x,y). x-y)"

    23   "f(x,y) = (if x \<le> y then x else f(x,y+1))";

    24

    25 text{*\noindent

    26 is not proved automatically (although maybe it should be). Isabelle prints a

    27 kind of error message showing you what it was unable to prove. You will then

    28 have to prove it as a separate lemma before you attempt the definition

    29 of your function once more. In our case the required lemma is the obvious one:

    30 *}

    31

    32 lemma termi_lem: "\<not> x \<le> y \<Longrightarrow> x - Suc y < x - y";

    33

    34 txt{*\noindent

    35 It was not proved automatically because of the special nature of @{text"-"}

    36 on @{typ"nat"}. This requires more arithmetic than is tried by default:

    37 *}

    38

    39 apply(arith);

    40 done

    41

    42 text{*\noindent

    43 Because \isacommand{recdef}'s termination prover involves simplification,

    44 we include with our second attempt the hint to use @{thm[source]termi_lem} as

    45 a simplification rule:\indexbold{*recdef_simp}

    46 *}

    47

    48 consts g :: "nat\<times>nat \<Rightarrow> nat";

    49 recdef g "measure(\<lambda>(x,y). x-y)"

    50   "g(x,y) = (if x \<le> y then x else g(x,y+1))"

    51 (hints recdef_simp: termi_lem)

    52

    53 text{*\noindent

    54 This time everything works fine. Now @{thm[source]g.simps} contains precisely

    55 the stated recursion equation for @{term g} and they are simplification

    56 rules. Thus we can automatically prove

    57 *}

    58

    59 theorem "g(1,0) = g(1,1)";

    60 apply(simp);

    61 done

    62

    63 text{*\noindent

    64 More exciting theorems require induction, which is discussed below.

    65

    66 If the termination proof requires a new lemma that is of general use, you can

    67 turn it permanently into a simplification rule, in which case the above

    68 \isacommand{hint} is not necessary. But our @{thm[source]termi_lem} is not

    69 sufficiently general to warrant this distinction.

    70

    71 The attentive reader may wonder why we chose to call our function @{term g}

    72 rather than @{term f} the second time around. The reason is that, despite

    73 the failed termination proof, the definition of @{term f} did not

    74 fail, and thus we could not define it a second time. However, all theorems

    75 about @{term f}, for example @{thm[source]f.simps}, carry as a precondition

    76 the unproved termination condition. Moreover, the theorems

    77 @{thm[source]f.simps} are not simplification rules. However, this mechanism

    78 allows a delayed proof of termination: instead of proving

    79 @{thm[source]termi_lem} up front, we could prove

    80 it later on and then use it to remove the preconditions from the theorems

    81 about @{term f}. In most cases this is more cumbersome than proving things

    82 up front.

    83 %FIXME, with one exception: nested recursion.

    84 *}

    85

    86 (*<*)

    87 end

    88 (*>*)