1 (* Title: HOL/UNITY/SubstAx |
1 (* Title: HOL/UNITY/SubstAx |
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1998 University of Cambridge |
3 Copyright 1998 University of Cambridge |
5 |
4 |
6 Weak LeadsTo relation (restricted to the set of reachable states) |
5 Weak LeadsTo relation (restricted to the set of reachable states) |
7 *) |
6 *) |
8 |
7 |
9 header{*Weak Progress*} |
8 header{*Weak Progress*} |
10 |
9 |
11 theory SubstAx imports WFair Constrains begin |
10 theory SubstAx imports WFair Constrains begin |
12 |
11 |
13 constdefs |
12 definition Ensures :: "['a set, 'a set] => 'a program set" (infixl "Ensures" 60) where |
14 Ensures :: "['a set, 'a set] => 'a program set" (infixl "Ensures" 60) |
|
15 "A Ensures B == {F. F \<in> (reachable F \<inter> A) ensures B}" |
13 "A Ensures B == {F. F \<in> (reachable F \<inter> A) ensures B}" |
16 |
14 |
17 LeadsTo :: "['a set, 'a set] => 'a program set" (infixl "LeadsTo" 60) |
15 definition LeadsTo :: "['a set, 'a set] => 'a program set" (infixl "LeadsTo" 60) where |
18 "A LeadsTo B == {F. F \<in> (reachable F \<inter> A) leadsTo B}" |
16 "A LeadsTo B == {F. F \<in> (reachable F \<inter> A) leadsTo B}" |
19 |
17 |
20 syntax (xsymbols) |
18 syntax (xsymbols) |
21 "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \<longmapsto>w " 60) |
19 "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \<longmapsto>w " 60) |
22 |
20 |