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--
```     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
```