author | wenzelm |
Sat, 01 Dec 2001 18:52:32 +0100 | |
changeset 12338 | de0f4a63baa5 |
parent 12218 | 6597093b77e7 |
child 14981 | e73f8140af78 |
permissions | -rw-r--r-- |
3071 | 1 |
(* Title: HOLCF/IOA/meta_theory/RefMappings.thy |
3275 | 2 |
ID: $Id$ |
12218 | 3 |
Author: Olaf Müller |
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
3071 | 5 |
|
12218 | 6 |
Refinement Mappings in HOLCF/IOA. |
3071 | 7 |
*) |
8 |
||
9 |
RefMappings = Traces + |
|
10 |
||
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12218
diff
changeset
|
11 |
default type |
3071 | 12 |
|
13 |
consts |
|
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
14 |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
15 |
move ::"[('a,'s)ioa,('a,'s)pairs,'s,'a,'s] => bool" |
3071 | 16 |
is_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" |
17 |
is_weak_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" |
|
18 |
||
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
19 |
|
3071 | 20 |
defs |
21 |
||
22 |
||
23 |
move_def |
|
24 |
"move ioa ex s a t == |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
25 |
(is_exec_frag ioa (s,ex) & Finite ex & |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
26 |
laststate (s,ex)=t & |
10835 | 27 |
mk_trace ioa$ex = (if a:ext(ioa) then a>>nil else nil))" |
3071 | 28 |
|
29 |
is_ref_map_def |
|
30 |
"is_ref_map f C A == |
|
31 |
(!s:starts_of(C). f(s):starts_of(A)) & |
|
32 |
(!s t a. reachable C s & |
|
33 |
s -a--C-> t |
|
34 |
--> (? ex. move A ex (f s) a (f t)))" |
|
35 |
||
36 |
is_weak_ref_map_def |
|
37 |
"is_weak_ref_map f C A == |
|
38 |
(!s:starts_of(C). f(s):starts_of(A)) & |
|
39 |
(!s t a. reachable C s & |
|
40 |
s -a--C-> t |
|
41 |
--> (if a:ext(C) |
|
42 |
then (f s) -a--A-> (f t) |
|
43 |
else (f s)=(f t)))" |
|
44 |
||
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
45 |
|
3071 | 46 |
end |