author | mueller |
Mon, 19 Oct 1998 16:13:13 +0200 | |
changeset 5677 | 4feffde494cf |
parent 4559 | 8e604d885b54 |
child 10835 | f4745d77e620 |
permissions | -rw-r--r-- |
3071 | 1 |
(* Title: HOLCF/IOA/meta_theory/RefMappings.thy |
3275 | 2 |
ID: $Id$ |
3071 | 3 |
Author: Olaf Mueller |
4 |
Copyright 1996 TU Muenchen |
|
5 |
||
6 |
Refinement Mappings in HOLCF/IOA |
|
7 |
*) |
|
8 |
||
9 |
RefMappings = Traces + |
|
10 |
||
11 |
default term |
|
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 & |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
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 |