equal
deleted
inserted
replaced
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 definition |
17 definition |
18 indinv :: "('a * 'a) set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool" |
18 indinv :: "('a * 'a) set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool" where |
19 "indinv r S F = (\<forall>f x. (\<forall>y. (y,x) : r --> S y (f y)) --> S x (F f x))" |
19 "indinv r S F = (\<forall>f x. (\<forall>y. (y,x) : r --> S y (f y)) --> S x (F f x))" |
20 |
20 |
21 |
21 |
22 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." |
23 |
23 |
24 definition |
24 definition |
25 indinv_on :: "('a * 'a) set => 'a set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool" |
25 indinv_on :: "('a * 'a) set => 'a set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool" where |
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))" |
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))" |
27 |
27 |
28 |
28 |
29 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 |
30 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 |