5 text\<open> |
5 text\<open> |
6 When a function~$f$ is defined via \isacommand{recdef}, Isabelle tries to prove |
6 When a function~$f$ is defined via \isacommand{recdef}, Isabelle tries to prove |
7 its termination with the help of the user-supplied measure. Each of the examples |
7 its termination with the help of the user-supplied measure. Each of the examples |
8 above is simple enough that Isabelle can automatically prove that the |
8 above is simple enough that Isabelle can automatically prove that the |
9 argument's measure decreases in each recursive call. As a result, |
9 argument's measure decreases in each recursive call. As a result, |
10 $f$@{text".simps"} will contain the defining equations (or variants derived |
10 $f$\<open>.simps\<close> will contain the defining equations (or variants derived |
11 from them) as theorems. For example, look (via \isacommand{thm}) at |
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 |
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 |
13 the same function. What is more, those equations are automatically declared as |
14 simplification rules. |
14 simplification rules. |
15 |
15 |
27 showing you what it was unable to prove: |
27 showing you what it was unable to prove: |
28 @{text[display]"length (filter ... xs) < Suc (length xs)"} |
28 @{text[display]"length (filter ... xs) < Suc (length xs)"} |
29 We can either prove this as a separate lemma, or try to figure out which |
29 We can either prove this as a separate lemma, or try to figure out which |
30 existing lemmas may help. We opt for the second alternative. The theory of |
30 existing lemmas may help. We opt for the second alternative. The theory of |
31 lists contains the simplification rule @{thm length_filter_le[no_vars]}, |
31 lists contains the simplification rule @{thm length_filter_le[no_vars]}, |
32 which is what we need, provided we turn \mbox{@{text"< Suc"}} |
32 which is what we need, provided we turn \mbox{\<open>< Suc\<close>} |
33 into |
33 into |
34 @{text"\<le>"} so that the rule applies. Lemma |
34 \<open>\<le>\<close> so that the rule applies. Lemma |
35 @{thm[source]less_Suc_eq_le} does just that: @{thm less_Suc_eq_le[no_vars]}. |
35 @{thm[source]less_Suc_eq_le} does just that: @{thm less_Suc_eq_le[no_vars]}. |
36 |
36 |
37 Now we retry the above definition but supply the lemma(s) just found (or |
37 Now we retry the above definition but supply the lemma(s) just found (or |
38 proved). Because \isacommand{recdef}'s termination prover involves |
38 proved). Because \isacommand{recdef}'s termination prover involves |
39 simplification, we include in our second attempt a hint: the |
39 simplification, we include in our second attempt a hint: the |
46 "qs(x#xs) = qs(filter (\<lambda>y. y\<le>x) xs) @ [x] @ qs(filter (\<lambda>y. x<y) xs)" |
46 "qs(x#xs) = qs(filter (\<lambda>y. y\<le>x) xs) @ [x] @ qs(filter (\<lambda>y. x<y) xs)" |
47 (hints recdef_simp: less_Suc_eq_le) |
47 (hints recdef_simp: less_Suc_eq_le) |
48 (*<*)local(*>*) |
48 (*<*)local(*>*) |
49 text\<open>\noindent |
49 text\<open>\noindent |
50 This time everything works fine. Now @{thm[source]qs.simps} contains precisely |
50 This time everything works fine. Now @{thm[source]qs.simps} contains precisely |
51 the stated recursion equations for @{text qs} and they have become |
51 the stated recursion equations for \<open>qs\<close> and they have become |
52 simplification rules. |
52 simplification rules. |
53 Thus we can automatically prove results such as this one: |
53 Thus we can automatically prove results such as this one: |
54 \<close> |
54 \<close> |
55 |
55 |
56 theorem "qs[2,3,0] = qs[3,0,2]" |
56 theorem "qs[2,3,0] = qs[3,0,2]" |