12 vol. 2758, pp. 253-269. *} |
12 vol. 2758, pp. 253-269. *} |
13 |
13 |
14 |
14 |
15 text "S is an inductive invariant of the functional F with respect to the wellfounded relation r." |
15 text "S is an inductive invariant of the functional F with respect to the wellfounded relation r." |
16 |
16 |
17 constdefs indinv :: "('a * 'a) set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool" |
17 definition |
18 "indinv r S F == \<forall>f x. (\<forall>y. (y,x) : r --> S y (f y)) --> S x (F f x)" |
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))" |
19 |
20 |
20 |
21 |
21 text "S is an inductive invariant of the functional F on set D with respect to the wellfounded relation r." |
22 text "S is an inductive invariant of the functional F on set D with respect to the wellfounded relation r." |
22 |
23 |
23 constdefs indinv_on :: "('a * 'a) set => 'a set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool" |
24 definition |
24 "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)" |
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))" |
25 |
27 |
26 |
28 |
27 text "The key theorem, corresponding to theorem 1 of the paper. All other results |
29 text "The key theorem, corresponding to theorem 1 of the paper. All other results |
28 in this theory are proved using instances of this theorem, and theorems |
30 in this theory are proved using instances of this theorem, and theorems |
29 derived from this theorem." |
31 derived from this theorem." |
30 |
32 |
31 theorem indinv_wfrec: |
33 theorem indinv_wfrec: |
32 assumes WF: "wf r" and |
34 assumes wf: "wf r" and |
33 INV: "indinv r S F" |
35 inv: "indinv r S F" |
34 shows "S x (wfrec r F x)" |
36 shows "S x (wfrec r F x)" |
35 proof (induct_tac x rule: wf_induct [OF WF]) |
37 using wf |
|
38 proof (induct x) |
36 fix x |
39 fix x |
37 assume IHYP: "\<forall>y. (y,x) \<in> r --> S y (wfrec r F y)" |
40 assume IHYP: "!!y. (y,x) \<in> r \<Longrightarrow> S y (wfrec r F y)" |
38 then have "\<forall>y. (y,x) \<in> r --> S y (cut (wfrec r F) r x y)" by (simp add: tfl_cut_apply) |
41 then have "!!y. (y,x) \<in> r \<Longrightarrow> S y (cut (wfrec r F) r x y)" by (simp add: tfl_cut_apply) |
39 with INV have "S x (F (cut (wfrec r F) r x) x)" by (unfold indinv_def, blast) |
42 with inv have "S x (F (cut (wfrec r F) r x) x)" by (unfold indinv_def, blast) |
40 thus "S x (wfrec r F x)" using WF by (simp add: wfrec) |
43 thus "S x (wfrec r F x)" using wf by (simp add: wfrec) |
41 qed |
44 qed |
42 |
45 |
43 theorem indinv_on_wfrec: |
46 theorem indinv_on_wfrec: |
44 assumes WF: "wf r" and |
47 assumes WF: "wf r" and |
45 INV: "indinv_on r D S F" and |
48 INV: "indinv_on r D S F" and |