src/HOL/HOLCF/IOA/meta_theory/Simulations.thy
author wenzelm
Sun Nov 02 17:16:01 2014 +0100 (2014-11-02)
changeset 58880 0baae4311a9f
parent 42151 4da4fc77664b
child 62002 f1599e98c4d0
permissions -rw-r--r--
modernized header;
     1 (*  Title:      HOL/HOLCF/IOA/meta_theory/Simulations.thy
     2     Author:     Olaf Müller
     3 *)
     4 
     5 section {* Simulations in HOLCF/IOA *}
     6 
     7 theory Simulations
     8 imports RefCorrectness
     9 begin
    10 
    11 default_sort type
    12 
    13 definition
    14   is_simulation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
    15   "is_simulation R C A =
    16    ((!s:starts_of C. R``{s} Int starts_of A ~= {}) &
    17    (!s s' t a. reachable C s &
    18                s -a--C-> t   &
    19                (s,s') : R
    20                --> (? t' ex. (t,t'):R & move A ex s' a t')))"
    21 
    22 definition
    23   is_backward_simulation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
    24   "is_backward_simulation R C A =
    25    ((!s:starts_of C. R``{s} <= starts_of A) &
    26    (!s t t' a. reachable C s &
    27                s -a--C-> t   &
    28                (t,t') : R
    29                --> (? ex s'. (s,s'):R & move A ex s' a t')))"
    30 
    31 definition
    32   is_forw_back_simulation :: "[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
    33   "is_forw_back_simulation R C A =
    34    ((!s:starts_of C. ? S'. (s,S'):R & S'<= starts_of A) &
    35    (!s S' t a. reachable C s &
    36                s -a--C-> t   &
    37                (s,S') : R
    38                --> (? T'. (t,T'):R & (! t':T'. ? s':S'. ? ex. move A ex s' a t'))))"
    39 
    40 definition
    41   is_back_forw_simulation :: "[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
    42   "is_back_forw_simulation R C A =
    43    ((!s:starts_of C. ! S'. (s,S'):R --> S' Int starts_of A ~={}) &
    44    (!s t T' a. reachable C s &
    45                s -a--C-> t   &
    46                (t,T') : R
    47                --> (? S'. (s,S'):R & (! s':S'. ? t':T'. ? ex. move A ex s' a t'))))"
    48 
    49 definition
    50   is_history_relation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
    51   "is_history_relation R C A = (is_simulation R C A &
    52                                 is_ref_map (%x.(@y. (x,y):(R^-1))) A C)"
    53 
    54 definition
    55   is_prophecy_relation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
    56   "is_prophecy_relation R C A = (is_backward_simulation R C A &
    57                                  is_ref_map (%x.(@y. (x,y):(R^-1))) A C)"
    58 
    59 
    60 lemma set_non_empty: "(A~={}) = (? x. x:A)"
    61 apply auto
    62 done
    63 
    64 lemma Int_non_empty: "(A Int B ~= {}) = (? x. x: A & x:B)"
    65 apply (simp add: set_non_empty)
    66 done
    67 
    68 
    69 lemma Sim_start_convert:
    70 "(R``{x} Int S ~= {}) = (? y. (x,y):R & y:S)"
    71 apply (unfold Image_def)
    72 apply (simp add: Int_non_empty)
    73 done
    74 
    75 declare Sim_start_convert [simp]
    76 
    77 
    78 lemma ref_map_is_simulation:
    79 "!! f. is_ref_map f C A ==> is_simulation {p. (snd p) = f (fst p)} C A"
    80 
    81 apply (unfold is_ref_map_def is_simulation_def)
    82 apply simp
    83 done
    84 
    85 end