1 (* |
|
2 Author: Sava Krsti\'{c} and John Matthews |
|
3 *) |
|
4 |
|
5 header {* Example use if an inductive invariant to solve termination conditions *} |
|
6 |
|
7 theory InductiveInvariant_examples imports InductiveInvariant begin |
|
8 |
|
9 text "A simple example showing how to use an inductive invariant |
|
10 to solve termination conditions generated by recdef on |
|
11 nested recursive function definitions." |
|
12 |
|
13 consts g :: "nat => nat" |
|
14 |
|
15 recdef (permissive) g "less_than" |
|
16 "g 0 = 0" |
|
17 "g (Suc n) = g (g n)" |
|
18 |
|
19 text "We can prove the unsolved termination condition for |
|
20 g by showing it is an inductive invariant." |
|
21 |
|
22 recdef_tc g_tc[simp]: g |
|
23 apply (rule allI) |
|
24 apply (rule_tac x=n in tfl_indinv_wfrec [OF g_def]) |
|
25 apply (auto simp add: indinv_def split: nat.split) |
|
26 apply (frule_tac x=nat in spec) |
|
27 apply (drule_tac x="f nat" in spec) |
|
28 by auto |
|
29 |
|
30 |
|
31 text "This declaration invokes Isabelle's simplifier to |
|
32 remove any termination conditions before adding |
|
33 g's rules to the simpset." |
|
34 declare g.simps [simplified, simp] |
|
35 |
|
36 |
|
37 text "This is an example where the termination condition generated |
|
38 by recdef is not itself an inductive invariant." |
|
39 |
|
40 consts g' :: "nat => nat" |
|
41 recdef (permissive) g' "less_than" |
|
42 "g' 0 = 0" |
|
43 "g' (Suc n) = g' n + g' (g' n)" |
|
44 |
|
45 thm g'.simps |
|
46 |
|
47 |
|
48 text "The strengthened inductive invariant is as follows |
|
49 (this invariant also works for the first example above):" |
|
50 |
|
51 lemma g'_inv: "g' n = 0" |
|
52 thm tfl_indinv_wfrec [OF g'_def] |
|
53 apply (rule_tac x=n in tfl_indinv_wfrec [OF g'_def]) |
|
54 by (auto simp add: indinv_def split: nat.split) |
|
55 |
|
56 recdef_tc g'_tc[simp]: g' |
|
57 by (simp add: g'_inv) |
|
58 |
|
59 text "Now we can remove the termination condition from |
|
60 the rules for g' ." |
|
61 thm g'.simps [simplified] |
|
62 |
|
63 |
|
64 text {* Sometimes a recursive definition is partial, that is, it |
|
65 is only meant to be invoked on "good" inputs. As a contrived |
|
66 example, we will define a new version of g that is only |
|
67 well defined for even inputs greater than zero. *} |
|
68 |
|
69 consts g_even :: "nat => nat" |
|
70 recdef (permissive) g_even "less_than" |
|
71 "g_even (Suc (Suc 0)) = 3" |
|
72 "g_even n = g_even (g_even (n - 2) - 1)" |
|
73 |
|
74 |
|
75 text "We can prove a conditional version of the unsolved termination |
|
76 condition for @{term g_even} by proving a stronger inductive invariant." |
|
77 |
|
78 lemma g_even_indinv: "\<exists>k. n = Suc (Suc (2*k)) ==> g_even n = 3" |
|
79 apply (rule_tac D="{n. \<exists>k. n = Suc (Suc (2*k))}" and x=n in tfl_indinv_on_wfrec [OF g_even_def]) |
|
80 apply (auto simp add: indinv_on_def split: nat.split) |
|
81 by (case_tac ka, auto) |
|
82 |
|
83 |
|
84 text "Now we can prove that the second recursion equation for @{term g_even} |
|
85 holds, provided that n is an even number greater than two." |
|
86 |
|
87 theorem g_even_n: "\<exists>k. n = 2*k + 4 ==> g_even n = g_even (g_even (n - 2) - 1)" |
|
88 apply (subgoal_tac "(\<exists>k. n - 2 = 2*k + 2) & (\<exists>k. n = 2*k + 2)") |
|
89 by (auto simp add: g_even_indinv, arith) |
|
90 |
|
91 |
|
92 text "McCarthy's ninety-one function. This function requires a |
|
93 non-standard measure to prove termination." |
|
94 |
|
95 consts ninety_one :: "nat => nat" |
|
96 recdef (permissive) ninety_one "measure (%n. 101 - n)" |
|
97 "ninety_one x = (if 100 < x |
|
98 then x - 10 |
|
99 else (ninety_one (ninety_one (x+11))))" |
|
100 |
|
101 text "To discharge the termination condition, we will prove |
|
102 a strengthened inductive invariant: |
|
103 S x y == x < y + 11" |
|
104 |
|
105 lemma ninety_one_inv: "n < ninety_one n + 11" |
|
106 apply (rule_tac x=n in tfl_indinv_wfrec [OF ninety_one_def]) |
|
107 apply force |
|
108 apply (auto simp add: indinv_def) |
|
109 apply (frule_tac x="x+11" in spec) |
|
110 apply (frule_tac x="f (x + 11)" in spec) |
|
111 by arith |
|
112 |
|
113 text "Proving the termination condition using the |
|
114 strengthened inductive invariant." |
|
115 |
|
116 recdef_tc ninety_one_tc[rule_format]: ninety_one |
|
117 apply clarify |
|
118 by (cut_tac n="x+11" in ninety_one_inv, arith) |
|
119 |
|
120 text "Now we can remove the termination condition from |
|
121 the simplification rule for @{term ninety_one}." |
|
122 |
|
123 theorem def_ninety_one: |
|
124 "ninety_one x = (if 100 < x |
|
125 then x - 10 |
|
126 else ninety_one (ninety_one (x+11)))" |
|
127 by (subst ninety_one.simps, |
|
128 simp add: ninety_one_tc) |
|
129 |
|
130 end |
|