src/HOLCF/IOA/meta_theory/RefMappings.thy
author nipkow
Tue Jan 09 15:36:30 2001 +0100 (2001-01-09)
changeset 10835 f4745d77e620
parent 4559 8e604d885b54
child 12218 6597093b77e7
permissions -rw-r--r--
` -> $
mueller@3071
     1
(*  Title:      HOLCF/IOA/meta_theory/RefMappings.thy
mueller@3275
     2
    ID:         $Id$
mueller@3071
     3
    Author:     Olaf Mueller
mueller@3071
     4
    Copyright   1996  TU Muenchen
mueller@3071
     5
mueller@3071
     6
Refinement Mappings in HOLCF/IOA
mueller@3071
     7
*)
mueller@3071
     8
mueller@3071
     9
RefMappings = Traces  +
mueller@3071
    10
mueller@3071
    11
default term
mueller@3071
    12
mueller@3071
    13
consts
mueller@4559
    14
mueller@3433
    15
  move         ::"[('a,'s)ioa,('a,'s)pairs,'s,'a,'s] => bool"
mueller@3071
    16
  is_ref_map   ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"
mueller@3071
    17
  is_weak_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"
mueller@3071
    18
 
mueller@4559
    19
mueller@3071
    20
defs
mueller@3071
    21
mueller@3071
    22
mueller@3071
    23
move_def
mueller@3071
    24
  "move ioa ex s a t ==    
mueller@3433
    25
    (is_exec_frag ioa (s,ex) &  Finite ex & 
mueller@3433
    26
     laststate (s,ex)=t  &     
nipkow@10835
    27
     mk_trace ioa$ex = (if a:ext(ioa) then a>>nil else nil))"
mueller@3071
    28
mueller@3071
    29
is_ref_map_def
mueller@3071
    30
  "is_ref_map f C A ==                          
mueller@3071
    31
   (!s:starts_of(C). f(s):starts_of(A)) &        
mueller@3071
    32
   (!s t a. reachable C s &                      
mueller@3071
    33
            s -a--C-> t                 
mueller@3071
    34
            --> (? ex. move A ex (f s) a (f t)))"
mueller@3071
    35
 
mueller@3071
    36
is_weak_ref_map_def
mueller@3071
    37
  "is_weak_ref_map f C A ==                          
mueller@3071
    38
   (!s:starts_of(C). f(s):starts_of(A)) &        
mueller@3071
    39
   (!s t a. reachable C s &                      
mueller@3071
    40
            s -a--C-> t     
mueller@3071
    41
            --> (if a:ext(C) 
mueller@3071
    42
                 then (f s) -a--A-> (f t)
mueller@3071
    43
                 else (f s)=(f t)))" 
mueller@3071
    44
mueller@4559
    45
mueller@3071
    46
end