equal
deleted
inserted
replaced
|
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 |
1 theory InductiveInvariant imports Main begin |
7 theory InductiveInvariant imports Main begin |
2 |
8 |
3 (** Authors: Sava Krsti\'{c} and John Matthews **) |
9 text {* A formalization of some of the results in \emph{Inductive |
4 (** Date: Sep 12, 2003 **) |
10 Invariants for Nested Recursion}, by Sava Krsti\'{c} and John |
5 |
11 Matthews. Appears in the proceedings of TPHOLs 2003, LNCS |
6 text {* A formalization of some of the results in |
12 vol. 2758, pp. 253-269. *} |
7 \emph{Inductive Invariants for Nested Recursion}, |
|
8 by Sava Krsti\'{c} and John Matthews. |
|
9 Appears in the proceedings of TPHOLs 2003, LNCS vol. 2758, pp. 253-269. *} |
|
10 |
13 |
11 |
14 |
12 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." |
13 |
16 |
14 constdefs indinv :: "('a * 'a) set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool" |
17 constdefs indinv :: "('a * 'a) set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool" |