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