|
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 +
|
|
|
11 |
|
|
|
12 |
consts
|
|
|
13 |
|
|
|
14 |
corresp_ex ::"('a,'s2)ioa => ('s1 => 's2) =>
|
|
|
15 |
('a,'s1)execution => ('a,'s2)execution"
|
|
|
16 |
corresp_ex2 ::"('a,'s2)ioa => ('s1 => 's2) => ('a,'s1)pairs
|
|
|
17 |
-> ('s2 => ('a,'s2)pairs)"
|
|
|
18 |
|
|
|
19 |
|
|
|
20 |
defs
|
|
|
21 |
|
|
|
22 |
corresp_ex_def
|
|
|
23 |
"corresp_ex A f ex == (f (fst ex),(corresp_ex2 A f`(snd ex)) (f (fst ex)))"
|
|
|
24 |
|
|
|
25 |
|
|
|
26 |
corresp_ex2_def
|
|
|
27 |
"corresp_ex2 A f == (fix`(LAM h ex. (%s. case ex of
|
|
|
28 |
nil => nil
|
|
|
29 |
| x##xs => (flift1 (%pr. (snd(@cex. move A cex s (fst pr) (f (snd pr))))
|
|
|
30 |
@@ ((h`xs) (f (snd pr))))
|
|
|
31 |
`x) )))"
|
|
|
32 |
|
|
|
33 |
|
|
|
34 |
|
|
|
35 |
end |