14 simplification rules. |
14 simplification rules. |
15 |
15 |
16 Isabelle may fail to prove the termination condition for some |
16 Isabelle may fail to prove the termination condition for some |
17 recursive call. Let us try the following artificial function:*} |
17 recursive call. Let us try the following artificial function:*} |
18 |
18 |
19 consts f :: "nat\<times>nat \<Rightarrow> nat"; |
19 consts f :: "nat\<times>nat \<Rightarrow> nat" |
20 recdef f "measure(\<lambda>(x,y). x-y)" |
20 recdef (*<*)(permissive)(*<*)f "measure(\<lambda>(x,y). x-y)" |
21 "f(x,y) = (if x \<le> y then x else f(x,y+1))"; |
21 "f(x,y) = (if x \<le> y then x else f(x,y+1))" |
22 |
22 |
23 text{*\noindent |
23 text{*\noindent |
24 Isabelle prints a |
24 Isabelle prints a |
25 \REMARK{error or warning? change this part? rename g to f?} |
25 \REMARK{error or warning? change this part? rename g to f?} |
26 message showing you what it was unable to prove. You will then |
26 message showing you what it was unable to prove. You will then |
27 have to prove it as a separate lemma before you attempt the definition |
27 have to prove it as a separate lemma before you attempt the definition |
28 of your function once more. In our case the required lemma is the obvious one: |
28 of your function once more. In our case the required lemma is the obvious one: |
29 *} |
29 *} |
30 |
30 |
31 lemma termi_lem: "\<not> x \<le> y \<Longrightarrow> x - Suc y < x - y"; |
31 lemma termi_lem: "\<not> x \<le> y \<Longrightarrow> x - Suc y < x - y" |
32 |
32 |
33 txt{*\noindent |
33 txt{*\noindent |
34 It was not proved automatically because of the awkward behaviour of subtraction |
34 It was not proved automatically because of the awkward behaviour of subtraction |
35 on type @{typ"nat"}. This requires more arithmetic than is tried by default: |
35 on type @{typ"nat"}. This requires more arithmetic than is tried by default: |
36 *} |
36 *} |
37 |
37 |
38 apply(arith); |
38 apply(arith) |
39 done |
39 done |
40 |
40 |
41 text{*\noindent |
41 text{*\noindent |
42 Because \isacommand{recdef}'s termination prover involves simplification, |
42 Because \isacommand{recdef}'s termination prover involves simplification, |
43 we include in our second attempt a hint: the \attrdx{recdef_simp} attribute |
43 we include in our second attempt a hint: the \attrdx{recdef_simp} attribute |
44 says to use @{thm[source]termi_lem} as |
44 says to use @{thm[source]termi_lem} as |
45 a simplification rule. |
45 a simplification rule. |
46 *} |
46 *} |
47 |
47 |
48 consts g :: "nat\<times>nat \<Rightarrow> nat"; |
48 consts g :: "nat\<times>nat \<Rightarrow> nat" |
49 recdef g "measure(\<lambda>(x,y). x-y)" |
49 recdef g "measure(\<lambda>(x,y). x-y)" |
50 "g(x,y) = (if x \<le> y then x else g(x,y+1))" |
50 "g(x,y) = (if x \<le> y then x else g(x,y+1))" |
51 (hints recdef_simp: termi_lem) |
51 (hints recdef_simp: termi_lem) |
52 |
52 |
53 text{*\noindent |
53 text{*\noindent |
54 This time everything works fine. Now @{thm[source]g.simps} contains precisely |
54 This time everything works fine. Now @{thm[source]g.simps} contains precisely |
55 the stated recursion equation for @{term g}, which has been stored as a |
55 the stated recursion equation for @{term g}, which has been stored as a |
56 simplification rule. Thus we can automatically prove results such as this one: |
56 simplification rule. Thus we can automatically prove results such as this one: |
57 *} |
57 *} |
58 |
58 |
59 theorem "g(1,0) = g(1,1)"; |
59 theorem "g(1,0) = g(1,1)" |
60 apply(simp); |
60 apply(simp) |
61 done |
61 done |
62 |
62 |
63 text{*\noindent |
63 text{*\noindent |
64 More exciting theorems require induction, which is discussed below. |
64 More exciting theorems require induction, which is discussed below. |
65 |
65 |