author | paulson |
Fri, 29 Jan 1999 16:23:56 +0100 | |
changeset 6161 | bc2a76ce1ea3 |
parent 5976 | 44290b71a85f |
child 10835 | f4745d77e620 |
permissions | -rw-r--r-- |
3071 | 1 |
(* Title: HOLCF/IOA/meta_theory/RefCorrectness.thy |
3275 | 2 |
ID: $Id$ |
3071 | 3 |
Author: Olaf Mueller |
4 |
Copyright 1996 TU Muenchen |
|
5 |
||
6 |
Correctness of Refinement Mappings in HOLCF/IOA |
|
7 |
*) |
|
8 |
||
9 |
||
10 |
RefCorrectness = RefMappings + |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
11 |
|
3071 | 12 |
consts |
13 |
||
14 |
corresp_ex ::"('a,'s2)ioa => ('s1 => 's2) => |
|
15 |
('a,'s1)execution => ('a,'s2)execution" |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
16 |
corresp_exC ::"('a,'s2)ioa => ('s1 => 's2) => ('a,'s1)pairs |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
17 |
-> ('s1 => ('a,'s2)pairs)" |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
18 |
is_fair_ref_map :: "('s1 => 's2) => ('a,'s1)ioa => ('a,'s2)ioa => bool" |
3071 | 19 |
|
20 |
defs |
|
21 |
||
22 |
corresp_ex_def |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
23 |
"corresp_ex A f ex == (f (fst ex),(corresp_exC A f`(snd ex)) (fst ex))" |
3071 | 24 |
|
25 |
||
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
26 |
corresp_exC_def |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
27 |
"corresp_exC A f == (fix`(LAM h ex. (%s. case ex of |
3071 | 28 |
nil => nil |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
29 |
| x##xs => (flift1 (%pr. (@cex. move A cex (f s) (fst pr) (f (snd pr))) |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
30 |
@@ ((h`xs) (snd pr))) |
3071 | 31 |
`x) )))" |
32 |
||
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
33 |
is_fair_ref_map_def |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
34 |
"is_fair_ref_map f C A == |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
35 |
is_ref_map f C A & |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
36 |
(! ex : executions(C). fair_ex C ex --> fair_ex A (corresp_ex A f ex))" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
37 |
|
3071 | 38 |
|
39 |
||
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
40 |
rules |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
41 |
(* Axioms for fair trace inclusion proof support, not for the correctness proof |
5976 | 42 |
of refinement mappings ! |
43 |
Note: Everything is superseded by LiveIOA.thy! *) |
|
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
44 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
45 |
corresp_laststate |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
46 |
"Finite ex ==> laststate (corresp_ex A f (s,ex)) = f (laststate (s,ex))" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
47 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
48 |
corresp_Finite |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
49 |
"Finite (snd (corresp_ex A f (s,ex))) = Finite ex" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
50 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
51 |
FromAtoC |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
52 |
"fin_often (%x. P (snd x)) (snd (corresp_ex A f (s,ex))) ==> fin_often (%y. P (f (snd y))) ex" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
53 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
54 |
FromCtoA |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
55 |
"inf_often (%y. P (fst y)) ex ==> inf_often (%x. P (fst x)) (snd (corresp_ex A f (s,ex)))" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
56 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
57 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
58 |
(* Proof by case on inf W in ex: If so, ok. If not, only fin W in ex, ie there is |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
59 |
an index i from which on no W in ex. But W inf enabled, ie at least once after i |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
60 |
W is enabled. As W does not occur after i and W is enabling_persistent, W keeps |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
61 |
enabled until infinity, ie. indefinitely *) |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
62 |
persistent |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
63 |
"[|inf_often (%x. Enabled A W (snd x)) ex; en_persistent A W|] |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
64 |
==> inf_often (%x. fst x :W) ex | fin_often (%x. ~Enabled A W (snd x)) ex" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
65 |
|
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
66 |
infpostcond |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
67 |
"[| is_exec_frag A (s,ex); inf_often (%x. fst x:W) ex|] |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
68 |
==> inf_often (% x. set_was_enabled A W (snd x)) ex" |
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
69 |
|
3071 | 70 |
end |