author | wenzelm |
Sat, 01 Dec 2001 18:52:32 +0100 | |
changeset 12338 | de0f4a63baa5 |
parent 12218 | 6597093b77e7 |
child 14981 | e73f8140af78 |
permissions | -rw-r--r-- |
4565 | 1 |
(* Title: HOLCF/IOA/meta_theory/Simulations.thy |
2 |
ID: $Id$ |
|
12218 | 3 |
Author: Olaf Müller |
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
4565 | 5 |
|
12218 | 6 |
Simulations in HOLCF/IOA. |
4565 | 7 |
*) |
8 |
||
9 |
Simulations = RefCorrectness + |
|
10 |
||
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12218
diff
changeset
|
11 |
default type |
4565 | 12 |
|
13 |
consts |
|
14 |
||
15 |
is_simulation ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" |
|
16 |
is_backward_simulation ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" |
|
17 |
is_forw_back_simulation ::"[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool" |
|
18 |
is_back_forw_simulation ::"[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool" |
|
19 |
is_history_relation ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" |
|
20 |
is_prophecy_relation ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" |
|
21 |
||
22 |
defs |
|
23 |
||
24 |
is_simulation_def |
|
25 |
"is_simulation R C A == |
|
10835 | 26 |
(!s:starts_of C. R``{s} Int starts_of A ~= {}) & |
4565 | 27 |
(!s s' t a. reachable C s & |
28 |
s -a--C-> t & |
|
29 |
(s,s') : R |
|
30 |
--> (? t' ex. (t,t'):R & move A ex s' a t'))" |
|
31 |
||
32 |
is_backward_simulation_def |
|
33 |
"is_backward_simulation R C A == |
|
10835 | 34 |
(!s:starts_of C. R``{s} <= starts_of A) & |
4565 | 35 |
(!s t t' a. reachable C s & |
36 |
s -a--C-> t & |
|
37 |
(t,t') : R |
|
38 |
--> (? ex s'. (s,s'):R & move A ex s' a t'))" |
|
39 |
||
40 |
is_forw_back_simulation_def |
|
41 |
"is_forw_back_simulation R C A == |
|
42 |
(!s:starts_of C. ? S'. (s,S'):R & S'<= starts_of A) & |
|
43 |
(!s S' t a. reachable C s & |
|
44 |
s -a--C-> t & |
|
45 |
(s,S') : R |
|
46 |
--> (? T'. (t,T'):R & (! t':T'. ? s':S'. ? ex. move A ex s' a t')))" |
|
47 |
||
48 |
is_back_forw_simulation_def |
|
49 |
"is_back_forw_simulation R C A == |
|
50 |
(!s:starts_of C. ! S'. (s,S'):R --> S' Int starts_of A ~={}) & |
|
51 |
(!s t T' a. reachable C s & |
|
52 |
s -a--C-> t & |
|
53 |
(t,T') : R |
|
54 |
--> (? S'. (s,S'):R & (! s':S'. ? t':T'. ? ex. move A ex s' a t')))" |
|
55 |
||
56 |
is_history_relation_def |
|
57 |
"is_history_relation R C A == is_simulation R C A & |
|
58 |
is_ref_map (%x.(@y. (x,y):(R^-1))) A C" |
|
59 |
||
60 |
is_prophecy_relation_def |
|
61 |
"is_prophecy_relation R C A == is_backward_simulation R C A & |
|
62 |
is_ref_map (%x.(@y. (x,y):(R^-1))) A C" |
|
63 |
||
64 |
end |