author  paulson 
Thu, 24 Aug 2000 12:39:24 +0200  
changeset 9685  6d123a7e30bd 
parent 8122  b43ad07660b9 
child 13796  19f50fa807ae 
permissions  rwrr 
4776  1 
(* Title: HOL/UNITY/SubstAx 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1998 University of Cambridge 

5 

6536  6 
Weak LeadsTo relation (restricted to the set of reachable states) 
4776  7 
*) 
8 

5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset

9 
SubstAx = WFair + Constrains + 
4776  10 

8041  11 
constdefs 
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8041
diff
changeset

12 
Ensures :: "['a set, 'a set] => 'a program set" (infixl 60) 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8041
diff
changeset

13 
"A Ensures B == {F. F : (reachable F Int A) ensures B}" 
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8041
diff
changeset

14 

8041  15 
LeadsTo :: "['a set, 'a set] => 'a program set" (infixl 60) 
16 
"A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}" 

4776  17 

9685  18 
syntax (xsymbols) 
19 
"op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \\<longmapsto>w " 60) 

20 

4776  21 
end 