equal
deleted
inserted
replaced
4 |
4 |
5 text{* |
5 text{* |
6 When a function is defined via \isacommand{recdef}, Isabelle tries to prove |
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 |
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 |
8 examples are simple enough that Isabelle can prove automatically that the |
9 measure of the argument goes down in each recursive call. In that case |
9 measure of the argument goes down in each recursive call. As a result, |
10 $f$.\isa{simps} contains the defining equations (or variants derived from |
10 \isa{$f$.simps} will contain the defining equations (or variants derived from |
11 them) as theorems. For example, look (via \isacommand{thm}) at |
11 them) as theorems. For example, look (via \isacommand{thm}) at |
12 \isa{sep.simps} and \isa{sep1.simps} to see that they define the same |
12 \isa{sep.simps} and \isa{sep1.simps} to see that they define the same |
13 function. What is more, those equations are automatically declared as |
13 function. What is more, those equations are automatically declared as |
14 simplification rules. |
14 simplification rules. |
15 |
15 |
37 *} |
37 *} |
38 |
38 |
39 apply(arith).; |
39 apply(arith).; |
40 |
40 |
41 text{*\noindent |
41 text{*\noindent |
42 Because \isacommand{recdef}'s the termination prover involves simplification, |
42 Because \isacommand{recdef}'s termination prover involves simplification, |
43 we have declared our lemma a simplification rule. Therefore our second |
43 we have turned our lemma into a simplification rule. Therefore our second |
44 attempt to define our function will automatically take it into account: |
44 attempt to define our function will automatically take it into account: |
45 *} |
45 *} |
46 |
46 |
47 consts g :: "nat*nat \\<Rightarrow> nat"; |
47 consts g :: "nat*nat \\<Rightarrow> nat"; |
48 recdef g "measure(\\<lambda>(x,y). x-y)" |
48 recdef g "measure(\\<lambda>(x,y). x-y)" |