14052

1 
(* Title: ZF/UNITY/Follows


2 
ID: $Id$


3 
Author: Sidi O Ehmety, Cambridge University Computer Laboratory


4 
Copyright 2002 University of Cambridge


5 


6 
The "Follows" relation of Charpentier and Sivilotte


7 


8 
Theory ported from HOL.


9 
*)


10 


11 
Follows = SubstAx + Increasing +


12 
constdefs


13 
Follows :: "[i, i, i=>i, i=>i] => i"


14 
"Follows(A, r, f, g) ==


15 
Increasing(A, r, g) Int


16 
Increasing(A, r,f) Int


17 
Always({s:state. <f(s), g(s)>:r}) Int


18 
(INT k:A. {s:state. <k, g(s)>:r} LeadsTo {s:state. <k,f(s)>:r})"


19 
consts


20 
Incr :: [i=>i]=>i


21 
n_Incr :: [i=>i]=>i


22 
m_Incr :: [i=>i]=>i


23 
s_Incr :: [i=>i]=>i


24 
n_Fols :: [i=>i, i=>i]=>i (infixl "n'_Fols" 65)


25 


26 
syntax


27 
Follows' :: "[i=>i, i=>i, i, i] => i"


28 
("(_ /Fols _ /Wrt (_ /'/ _))" [60, 0, 0, 60] 60)


29 


30 


31 
translations


32 
"Incr(f)" == "Increasing(list(nat), prefix(nat), f)"


33 
"n_Incr(f)" == "Increasing(nat, Le, f)"


34 
"s_Incr(f)" == "Increasing(Pow(nat), SetLe(nat), f)"


35 
"m_Incr(f)" == "Increasing(Mult(nat), MultLe(nat, Le), f)"


36 


37 
"f n_Fols g" == "Follows(nat, Le, f, g)"


38 


39 
"Follows'(f,g,r,A)" == "Follows(A,r,f,g)"


40 
end
