|
6706
|
1 |
(* Title: HOL/UNITY/Follows
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
|
4 |
Copyright 1998 University of Cambridge
|
|
|
5 |
|
|
|
6 |
The Follows relation of Charpentier and Sivilotte
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
Follows = Union +
|
|
|
10 |
|
|
|
11 |
constdefs
|
|
|
12 |
|
|
|
13 |
Follows :: "['a => 'b::{order}, 'a => 'b::{order}] => 'a program set"
|
|
6809
|
14 |
(infixl "Fols" 65)
|
|
|
15 |
"f Fols g == Increasing g Int Increasing f Int
|
|
|
16 |
Always {s. f s <= g s} Int
|
|
|
17 |
(INT k. {s. k <= g s} LeadsTo {s. k <= f s})"
|
|
6706
|
18 |
|
|
|
19 |
|
|
|
20 |
end
|