--- a/src/HOL/ex/InductiveInvariant.thy Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/ex/InductiveInvariant.thy Fri Nov 17 02:20:03 2006 +0100
@@ -15,14 +15,14 @@
text "S is an inductive invariant of the functional F with respect to the wellfounded relation r."
definition
- indinv :: "('a * 'a) set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool"
+ indinv :: "('a * 'a) set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool" where
"indinv r S F = (\<forall>f x. (\<forall>y. (y,x) : r --> S y (f y)) --> S x (F f x))"
text "S is an inductive invariant of the functional F on set D with respect to the wellfounded relation r."
definition
- indinv_on :: "('a * 'a) set => 'a set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool"
+ indinv_on :: "('a * 'a) set => 'a set => ('a => 'b => bool) => (('a => 'b) => ('a => 'b)) => bool" where
"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))"