|
11479
|
1 |
(* Title: ZF/UNITY/SubstAx.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Sidi O Ehmety, Computer Laboratory
|
|
|
4 |
Copyright 2001 University of Cambridge
|
|
|
5 |
|
|
|
6 |
Weak LeadsTo relation (restricted to the set of reachable states)
|
|
|
7 |
|
|
|
8 |
Theory ported from HOL.
|
|
|
9 |
*)
|
|
|
10 |
|
|
|
11 |
SubstAx = WFair + Constrains +
|
|
|
12 |
|
|
|
13 |
constdefs
|
|
12195
|
14 |
(* The definitions below are not `conventional', but yields simpler rules *)
|
|
11479
|
15 |
Ensures :: "[i,i] => i" (infixl 60)
|
|
12195
|
16 |
"A Ensures B == {F:program. F : (reachable(F) Int A) ensures (reachable(F) Int B) }"
|
|
11479
|
17 |
|
|
12195
|
18 |
LeadsTo :: "[i, i] => i" (infixl 60)
|
|
|
19 |
"A LeadsTo B == {F:program. F:(reachable(F) Int A) leadsTo (reachable(F) Int B)}"
|
|
11479
|
20 |
|
|
|
21 |
syntax (xsymbols)
|
|
|
22 |
"op LeadsTo" :: "[i, i] => i" (infixl " \\<longmapsto>w " 60)
|
|
|
23 |
|
|
|
24 |
end
|