--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,50 @@
+(* Title: HOLCF/IOA/meta_theory/RefMappings.thy
+ ID: $$
+ Author: Olaf Mueller
+ Copyright 1996 TU Muenchen
+
+Refinement Mappings in HOLCF/IOA
+*)
+
+RefMappings = Traces +
+
+default term
+
+consts
+ laststate ::"('a,'s)execution => 's"
+ move ::"[('a,'s)ioa,('a,'s)execution,'s,'a,'s] => bool"
+ is_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"
+ is_weak_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"
+
+defs
+
+laststate_def
+ "laststate ex == case Last`(snd ex) of
+ Undef => fst ex
+ | Def at => snd at"
+
+(* FIX: see paper, move should be defined on pairs, not on execs, then fst ex=s can
+ be omitted *)
+move_def
+ "move ioa ex s a t ==
+ (is_execution_fragment ioa ex & Finite (snd ex) &
+ fst ex=s & laststate ex=t &
+ mk_trace ioa`(snd ex) = (if a:ext(ioa) then a>>nil else nil))"
+
+is_ref_map_def
+ "is_ref_map f C A ==
+ (!s:starts_of(C). f(s):starts_of(A)) &
+ (!s t a. reachable C s &
+ s -a--C-> t
+ --> (? ex. move A ex (f s) a (f t)))"
+
+is_weak_ref_map_def
+ "is_weak_ref_map f C A ==
+ (!s:starts_of(C). f(s):starts_of(A)) &
+ (!s t a. reachable C s &
+ s -a--C-> t
+ --> (if a:ext(C)
+ then (f s) -a--A-> (f t)
+ else (f s)=(f t)))"
+
+end