author | wenzelm |
Fri, 02 Sep 2005 17:23:59 +0200 | |
changeset 17233 | 41eee2e7b465 |
parent 14981 | e73f8140af78 |
child 19741 | f65265d71426 |
permissions | -rw-r--r-- |
3071 | 1 |
(* Title: HOLCF/IOA/meta_theory/RefCorrectness.thy |
3275 | 2 |
ID: $Id$ |
12218 | 3 |
Author: Olaf Müller |
3071 | 4 |
*) |
5 |
||
17233 | 6 |
header {* Correctness of Refinement Mappings in HOLCF/IOA *} |
3071 | 7 |
|
17233 | 8 |
theory RefCorrectness |
9 |
imports RefMappings |
|
10 |
begin |
|
11 |
||
3071 | 12 |
consts |
13 |
||
17233 | 14 |
corresp_ex ::"('a,'s2)ioa => ('s1 => 's2) => |
3071 | 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 |
||
17233 | 22 |
corresp_ex_def: |
10835 | 23 |
"corresp_ex A f ex == (f (fst ex),(corresp_exC A f$(snd ex)) (fst ex))" |
3071 | 24 |
|
25 |
||
17233 | 26 |
corresp_exC_def: |
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))) |
10835 | 30 |
@@ ((h$xs) (snd pr))) |
31 |
$x) )))" |
|
17233 | 32 |
|
33 |
is_fair_ref_map_def: |
|
34 |
"is_fair_ref_map f C A == |
|
4559
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 |
||
17233 | 40 |
axioms |
4559
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 |
17233 | 42 |
of refinement mappings! |
5976 | 43 |
Note: Everything is superseded by LiveIOA.thy! *) |
4559
8e604d885b54
added files containing temproal logic and abstraction;
mueller
parents:
3433
diff
changeset
|
44 |
|
17233 | 45 |
corresp_laststate: |
4559
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 |
|
17233 | 48 |
corresp_Finite: |
4559
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 |
|
17233 | 51 |
FromAtoC: |
4559
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 |
|
17233 | 54 |
FromCtoA: |
4559
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 *) |
17233 | 62 |
persistent: |
4559
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 |
|
17233 | 66 |
infpostcond: |
4559
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 |
|
17233 | 70 |
ML {* use_legacy_bindings (the_context ()) *} |
71 |
||
72 |
end |