17388
|
1 |
(* ID: $Id$
|
|
2 |
Author: Sava Krsti\'{c} and John Matthews
|
|
3 |
*)
|
|
4 |
|
|
5 |
header {* Some of the results in Inductive Invariants for Nested Recursion *}
|
|
6 |
|
16417
|
7 |
theory InductiveInvariant imports Main begin
|
15636
|
8 |
|
17388
|
9 |
text {* A formalization of some of the results in \emph{Inductive
|
|
10 |
Invariants for Nested Recursion}, by Sava Krsti\'{c} and John
|
|
11 |
Matthews. Appears in the proceedings of TPHOLs 2003, LNCS
|
|
12 |
vol. 2758, pp. 253-269. *}
|
15636
|
13 |
|
|
14 |
|
|
15 |
text "S is an inductive invariant of the functional F with respect to the wellfounded relation r."
|
|
16 |
|
19736
|
17 |
definition
|
|
18 |
indinv :: "('a * 'a) set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool"
|
|
19 |
"indinv r S F = (\<forall>f x. (\<forall>y. (y,x) : r --> S y (f y)) --> S x (F f x))"
|
15636
|
20 |
|
|
21 |
|
|
22 |
text "S is an inductive invariant of the functional F on set D with respect to the wellfounded relation r."
|
|
23 |
|
19736
|
24 |
definition
|
|
25 |
indinv_on :: "('a * 'a) set => 'a set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool"
|
|
26 |
"indinv_on r D S F = (\<forall>f. \<forall>x\<in>D. (\<forall>y\<in>D. (y,x) \<in> r --> S y (f y)) --> S x (F f x))"
|
15636
|
27 |
|
|
28 |
|
|
29 |
text "The key theorem, corresponding to theorem 1 of the paper. All other results
|
|
30 |
in this theory are proved using instances of this theorem, and theorems
|
|
31 |
derived from this theorem."
|
|
32 |
|
|
33 |
theorem indinv_wfrec:
|
19736
|
34 |
assumes wf: "wf r" and
|
|
35 |
inv: "indinv r S F"
|
15636
|
36 |
shows "S x (wfrec r F x)"
|
19736
|
37 |
using wf
|
|
38 |
proof (induct x)
|
15636
|
39 |
fix x
|
19736
|
40 |
assume IHYP: "!!y. (y,x) \<in> r \<Longrightarrow> S y (wfrec r F y)"
|
|
41 |
then have "!!y. (y,x) \<in> r \<Longrightarrow> S y (cut (wfrec r F) r x y)" by (simp add: tfl_cut_apply)
|
|
42 |
with inv have "S x (F (cut (wfrec r F) r x) x)" by (unfold indinv_def, blast)
|
|
43 |
thus "S x (wfrec r F x)" using wf by (simp add: wfrec)
|
15636
|
44 |
qed
|
|
45 |
|
|
46 |
theorem indinv_on_wfrec:
|
|
47 |
assumes WF: "wf r" and
|
|
48 |
INV: "indinv_on r D S F" and
|
|
49 |
D: "x\<in>D"
|
|
50 |
shows "S x (wfrec r F x)"
|
|
51 |
apply (insert INV D indinv_wfrec [OF WF, of "% x y. x\<in>D --> S x y"])
|
|
52 |
by (simp add: indinv_on_def indinv_def)
|
|
53 |
|
|
54 |
theorem ind_fixpoint_on_lemma:
|
|
55 |
assumes WF: "wf r" and
|
|
56 |
INV: "\<forall>f. \<forall>x\<in>D. (\<forall>y\<in>D. (y,x) \<in> r --> S y (wfrec r F y) & f y = wfrec r F y)
|
|
57 |
--> S x (wfrec r F x) & F f x = wfrec r F x" and
|
|
58 |
D: "x\<in>D"
|
|
59 |
shows "F (wfrec r F) x = wfrec r F x & S x (wfrec r F x)"
|
|
60 |
proof (rule indinv_on_wfrec [OF WF _ D, of "% a b. F (wfrec r F) a = b & wfrec r F a = b & S a b" F, simplified])
|
|
61 |
show "indinv_on r D (%a b. F (wfrec r F) a = b & wfrec r F a = b & S a b) F"
|
|
62 |
proof (unfold indinv_on_def, clarify)
|
|
63 |
fix f x
|
|
64 |
assume A1: "\<forall>y\<in>D. (y, x) \<in> r --> F (wfrec r F) y = f y & wfrec r F y = f y & S y (f y)"
|
|
65 |
assume D': "x\<in>D"
|
|
66 |
from A1 INV [THEN spec, of f, THEN bspec, OF D']
|
|
67 |
have "S x (wfrec r F x)" and
|
|
68 |
"F f x = wfrec r F x" by auto
|
|
69 |
moreover
|
|
70 |
from A1 have "\<forall>y\<in>D. (y, x) \<in> r --> S y (wfrec r F y)" by auto
|
|
71 |
with D' INV [THEN spec, of "wfrec r F", simplified]
|
|
72 |
have "F (wfrec r F) x = wfrec r F x" by blast
|
|
73 |
ultimately show "F (wfrec r F) x = F f x & wfrec r F x = F f x & S x (F f x)" by auto
|
|
74 |
qed
|
|
75 |
qed
|
|
76 |
|
|
77 |
theorem ind_fixpoint_lemma:
|
|
78 |
assumes WF: "wf r" and
|
|
79 |
INV: "\<forall>f x. (\<forall>y. (y,x) \<in> r --> S y (wfrec r F y) & f y = wfrec r F y)
|
|
80 |
--> S x (wfrec r F x) & F f x = wfrec r F x"
|
|
81 |
shows "F (wfrec r F) x = wfrec r F x & S x (wfrec r F x)"
|
|
82 |
apply (rule ind_fixpoint_on_lemma [OF WF _ UNIV_I, simplified])
|
|
83 |
by (rule INV)
|
|
84 |
|
|
85 |
theorem tfl_indinv_wfrec:
|
|
86 |
"[| f == wfrec r F; wf r; indinv r S F |]
|
|
87 |
==> S x (f x)"
|
|
88 |
by (simp add: indinv_wfrec)
|
|
89 |
|
|
90 |
theorem tfl_indinv_on_wfrec:
|
|
91 |
"[| f == wfrec r F; wf r; indinv_on r D S F; x\<in>D |]
|
|
92 |
==> S x (f x)"
|
|
93 |
by (simp add: indinv_on_wfrec)
|
|
94 |
|
17388
|
95 |
end
|