src/HOLCF/IOA/meta_theory/Simulations.thy

tuned checklist;

(*  Title:      HOLCF/IOA/meta_theory/Simulations.thy
    ID:         $Id$
    Author:     Olaf Mueller
    Copyright   1997  TU Muenchen

Simulations in HOLCF/IOA
*)

Simulations = RefCorrectness  +

default term

consts

  is_simulation            ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
  is_backward_simulation   ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
  is_forw_back_simulation  ::"[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
  is_back_forw_simulation  ::"[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
  is_history_relation      ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
  is_prophecy_relation     ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool"

defs

is_simulation_def
  "is_simulation R C A ==                          
   (!s:starts_of C. R^^{s} Int starts_of A ~= {}) &        
   (!s s' t a. reachable C s &                      
               s -a--C-> t   &
               (s,s') : R              
               --> (? t' ex. (t,t'):R & move A ex s' a t'))"

is_backward_simulation_def
  "is_backward_simulation R C A ==                          
   (!s:starts_of C. R^^{s} <= starts_of A) &        
   (!s t t' a. reachable C s &                      
               s -a--C-> t   &
               (t,t') : R              
               --> (? ex s'. (s,s'):R & move A ex s' a t'))"

is_forw_back_simulation_def
  "is_forw_back_simulation R C A ==                          
   (!s:starts_of C. ? S'. (s,S'):R & S'<= starts_of A) &        
   (!s S' t a. reachable C s &                      
               s -a--C-> t   &
               (s,S') : R              
               --> (? T'. (t,T'):R & (! t':T'. ? s':S'. ? ex. move A ex s' a t')))"

is_back_forw_simulation_def
  "is_back_forw_simulation R C A ==                          
   (!s:starts_of C. ! S'. (s,S'):R --> S' Int starts_of A ~={}) &        
   (!s t T' a. reachable C s &                      
               s -a--C-> t   &
               (t,T') : R              
               --> (? S'. (s,S'):R & (! s':S'. ? t':T'. ? ex. move A ex s' a t')))"

is_history_relation_def
  "is_history_relation R C A == is_simulation R C A & 
                                is_ref_map (%x.(@y. (x,y):(R^-1))) A C"

is_prophecy_relation_def
  "is_prophecy_relation R C A == is_backward_simulation R C A & 
                                 is_ref_map (%x.(@y. (x,y):(R^-1))) A C"
                      
end