author | obua |
Tue, 18 May 2004 10:01:44 +0200 | |
changeset 14754 | a080eeeaec14 |
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 = Main: |
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: Sep 12, 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 formalization of some of the results in |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
7 |
\emph{Inductive Invariants for Nested Recursion}, |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
8 |
by Sava Krsti\'{c} and John Matthews. |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
9 |
Appears in the proceedings of TPHOLs 2003, LNCS vol. 2758, pp. 253-269. *} |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
10 |
|
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 |
text "S is an inductive invariant of the functional F with respect to the wellfounded relation r." |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
13 |
|
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
14 |
constdefs indinv :: "('a * 'a) set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool" |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
15 |
"indinv r S F == \<forall>f x. (\<forall>y. (y,x) : r --> S y (f y)) --> S x (F f x)" |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
16 |
|
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
17 |
|
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
18 |
text "S is an inductive invariant of the functional F on set D with respect to the wellfounded relation r." |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
19 |
|
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
20 |
constdefs indinv_on :: "('a * 'a) set => 'a set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool" |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
21 |
"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)" |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
22 |
|
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
23 |
|
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
24 |
text "The key theorem, corresponding to theorem 1 of the paper. All other results |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
25 |
in this theory are proved using instances of this theorem, and theorems |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
26 |
derived from this theorem." |
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 |
theorem indinv_wfrec: |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
29 |
assumes WF: "wf r" and |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
30 |
INV: "indinv r S F" |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
31 |
shows "S x (wfrec r F x)" |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
32 |
proof (induct_tac x rule: wf_induct [OF WF]) |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
33 |
fix x |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
34 |
assume IHYP: "\<forall>y. (y,x) \<in> r --> S y (wfrec r F y)" |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
35 |
then have "\<forall>y. (y,x) \<in> r --> S y (cut (wfrec r F) r x y)" by (simp add: tfl_cut_apply) |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
36 |
with INV have "S x (F (cut (wfrec r F) r x) x)" by (unfold indinv_def, blast) |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
37 |
thus "S x (wfrec r F x)" using WF by (simp add: wfrec) |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
38 |
qed |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
39 |
|
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
40 |
theorem indinv_on_wfrec: |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
41 |
assumes WF: "wf r" and |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
42 |
INV: "indinv_on r D S F" and |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
43 |
D: "x\<in>D" |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
44 |
shows "S x (wfrec r F x)" |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
45 |
apply (insert INV D indinv_wfrec [OF WF, of "% x y. x\<in>D --> S x y"]) |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
46 |
by (simp add: indinv_on_def indinv_def) |
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 |
theorem ind_fixpoint_on_lemma: |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
49 |
assumes WF: "wf r" and |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
50 |
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) |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
51 |
--> S x (wfrec r F x) & F f x = wfrec r F x" and |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
52 |
D: "x\<in>D" |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
53 |
shows "F (wfrec r F) x = wfrec r F x & S x (wfrec r F x)" |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
54 |
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]) |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
55 |
show "indinv_on r D (%a b. F (wfrec r F) a = b & wfrec r F a = b & S a b) F" |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
56 |
proof (unfold indinv_on_def, clarify) |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
57 |
fix f x |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
58 |
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)" |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
59 |
assume D': "x\<in>D" |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
60 |
from A1 INV [THEN spec, of f, THEN bspec, OF D'] |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
61 |
have "S x (wfrec r F x)" and |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
62 |
"F f x = wfrec r F x" by auto |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
63 |
moreover |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
64 |
from A1 have "\<forall>y\<in>D. (y, x) \<in> r --> S y (wfrec r F y)" by auto |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
65 |
with D' INV [THEN spec, of "wfrec r F", simplified] |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
66 |
have "F (wfrec r F) x = wfrec r F x" by blast |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
67 |
ultimately show "F (wfrec r F) x = F f x & wfrec r F x = F f x & S x (F f x)" by auto |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
68 |
qed |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
69 |
qed |
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 |
theorem ind_fixpoint_lemma: |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
72 |
assumes WF: "wf r" and |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
73 |
INV: "\<forall>f x. (\<forall>y. (y,x) \<in> r --> S y (wfrec r F y) & f y = wfrec r F y) |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
74 |
--> S x (wfrec r F x) & F f x = wfrec r F x" |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
75 |
shows "F (wfrec r F) x = wfrec r F x & S x (wfrec r F x)" |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
76 |
apply (rule ind_fixpoint_on_lemma [OF WF _ UNIV_I, simplified]) |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
77 |
by (rule INV) |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
78 |
|
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
79 |
theorem tfl_indinv_wfrec: |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
80 |
"[| f == wfrec r F; wf r; indinv r S F |] |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
81 |
==> S x (f x)" |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
82 |
by (simp add: indinv_wfrec) |
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 tfl_indinv_on_wfrec: |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
85 |
"[| f == wfrec r F; wf r; indinv_on r D S F; x\<in>D |] |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
86 |
==> S x (f x)" |
f58598341d30
InductiveInvariant_examples illustrates advanced recursive function definitions
paulson
parents:
diff
changeset
|
87 |
by (simp add: indinv_on_wfrec) |
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 |
end |