src/HOLCF/IOA/meta_theory/RefMappings.thy

New meta theory for IOA based on HOLCF.

(*  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