src/HOLCF/IOA/meta_theory/Simulations.thy
author mueller
Tue Jan 13 14:26:21 1998 +0100 (1998-01-13)
changeset 4565 ea467ce15040
child 10798 0a1446ff6aff
permissions -rw-r--r--
added forward simulation correectness;
mueller@4565
     1
(*  Title:      HOLCF/IOA/meta_theory/Simulations.thy
mueller@4565
     2
    ID:         $Id$
mueller@4565
     3
    Author:     Olaf Mueller
mueller@4565
     4
    Copyright   1997  TU Muenchen
mueller@4565
     5
mueller@4565
     6
Simulations in HOLCF/IOA
mueller@4565
     7
*)
mueller@4565
     8
mueller@4565
     9
Simulations = RefCorrectness  +
mueller@4565
    10
mueller@4565
    11
default term
mueller@4565
    12
mueller@4565
    13
consts
mueller@4565
    14
mueller@4565
    15
  is_simulation            ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
mueller@4565
    16
  is_backward_simulation   ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
mueller@4565
    17
  is_forw_back_simulation  ::"[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
mueller@4565
    18
  is_back_forw_simulation  ::"[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
mueller@4565
    19
  is_history_relation      ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
mueller@4565
    20
  is_prophecy_relation     ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
mueller@4565
    21
mueller@4565
    22
defs
mueller@4565
    23
mueller@4565
    24
is_simulation_def
mueller@4565
    25
  "is_simulation R C A ==                          
mueller@4565
    26
   (!s:starts_of C. R^^{s} Int starts_of A ~= {}) &        
mueller@4565
    27
   (!s s' t a. reachable C s &                      
mueller@4565
    28
               s -a--C-> t   &
mueller@4565
    29
               (s,s') : R              
mueller@4565
    30
               --> (? t' ex. (t,t'):R & move A ex s' a t'))"
mueller@4565
    31
mueller@4565
    32
is_backward_simulation_def
mueller@4565
    33
  "is_backward_simulation R C A ==                          
mueller@4565
    34
   (!s:starts_of C. R^^{s} <= starts_of A) &        
mueller@4565
    35
   (!s t t' a. reachable C s &                      
mueller@4565
    36
               s -a--C-> t   &
mueller@4565
    37
               (t,t') : R              
mueller@4565
    38
               --> (? ex s'. (s,s'):R & move A ex s' a t'))"
mueller@4565
    39
mueller@4565
    40
is_forw_back_simulation_def
mueller@4565
    41
  "is_forw_back_simulation R C A ==                          
mueller@4565
    42
   (!s:starts_of C. ? S'. (s,S'):R & S'<= starts_of A) &        
mueller@4565
    43
   (!s S' t a. reachable C s &                      
mueller@4565
    44
               s -a--C-> t   &
mueller@4565
    45
               (s,S') : R              
mueller@4565
    46
               --> (? T'. (t,T'):R & (! t':T'. ? s':S'. ? ex. move A ex s' a t')))"
mueller@4565
    47
mueller@4565
    48
is_back_forw_simulation_def
mueller@4565
    49
  "is_back_forw_simulation R C A ==                          
mueller@4565
    50
   (!s:starts_of C. ! S'. (s,S'):R --> S' Int starts_of A ~={}) &        
mueller@4565
    51
   (!s t T' a. reachable C s &                      
mueller@4565
    52
               s -a--C-> t   &
mueller@4565
    53
               (t,T') : R              
mueller@4565
    54
               --> (? S'. (s,S'):R & (! s':S'. ? t':T'. ? ex. move A ex s' a t')))"
mueller@4565
    55
mueller@4565
    56
is_history_relation_def
mueller@4565
    57
  "is_history_relation R C A == is_simulation R C A & 
mueller@4565
    58
                                is_ref_map (%x.(@y. (x,y):(R^-1))) A C"
mueller@4565
    59
mueller@4565
    60
is_prophecy_relation_def
mueller@4565
    61
  "is_prophecy_relation R C A == is_backward_simulation R C A & 
mueller@4565
    62
                                 is_ref_map (%x.(@y. (x,y):(R^-1))) A C"
mueller@4565
    63
                      
mueller@4565
    64
end