src/HOLCF/IOA/meta_theory/Simulations.thy
author wenzelm
Fri Sep 02 17:23:59 2005 +0200 (2005-09-02)
changeset 17233 41eee2e7b465
parent 14981 e73f8140af78
child 19741 f65265d71426
permissions -rw-r--r--
converted specifications to Isar theories;
mueller@4565
     1
(*  Title:      HOLCF/IOA/meta_theory/Simulations.thy
mueller@4565
     2
    ID:         $Id$
wenzelm@12218
     3
    Author:     Olaf Müller
mueller@4565
     4
*)
mueller@4565
     5
wenzelm@17233
     6
header {* Simulations in HOLCF/IOA *}
mueller@4565
     7
wenzelm@17233
     8
theory Simulations
wenzelm@17233
     9
imports RefCorrectness
wenzelm@17233
    10
begin
wenzelm@17233
    11
wenzelm@17233
    12
defaultsort type
mueller@4565
    13
mueller@4565
    14
consts
mueller@4565
    15
mueller@4565
    16
  is_simulation            ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
mueller@4565
    17
  is_backward_simulation   ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
mueller@4565
    18
  is_forw_back_simulation  ::"[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
mueller@4565
    19
  is_back_forw_simulation  ::"[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
mueller@4565
    20
  is_history_relation      ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
mueller@4565
    21
  is_prophecy_relation     ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
mueller@4565
    22
mueller@4565
    23
defs
mueller@4565
    24
wenzelm@17233
    25
is_simulation_def:
wenzelm@17233
    26
  "is_simulation R C A ==
wenzelm@17233
    27
   (!s:starts_of C. R``{s} Int starts_of A ~= {}) &
wenzelm@17233
    28
   (!s s' t a. reachable C s &
mueller@4565
    29
               s -a--C-> t   &
wenzelm@17233
    30
               (s,s') : R
mueller@4565
    31
               --> (? t' ex. (t,t'):R & move A ex s' a t'))"
mueller@4565
    32
wenzelm@17233
    33
is_backward_simulation_def:
wenzelm@17233
    34
  "is_backward_simulation R C A ==
wenzelm@17233
    35
   (!s:starts_of C. R``{s} <= starts_of A) &
wenzelm@17233
    36
   (!s t t' a. reachable C s &
mueller@4565
    37
               s -a--C-> t   &
wenzelm@17233
    38
               (t,t') : R
mueller@4565
    39
               --> (? ex s'. (s,s'):R & move A ex s' a t'))"
mueller@4565
    40
wenzelm@17233
    41
is_forw_back_simulation_def:
wenzelm@17233
    42
  "is_forw_back_simulation R C A ==
wenzelm@17233
    43
   (!s:starts_of C. ? S'. (s,S'):R & S'<= starts_of A) &
wenzelm@17233
    44
   (!s S' t a. reachable C s &
mueller@4565
    45
               s -a--C-> t   &
wenzelm@17233
    46
               (s,S') : R
mueller@4565
    47
               --> (? T'. (t,T'):R & (! t':T'. ? s':S'. ? ex. move A ex s' a t')))"
mueller@4565
    48
wenzelm@17233
    49
is_back_forw_simulation_def:
wenzelm@17233
    50
  "is_back_forw_simulation R C A ==
wenzelm@17233
    51
   (!s:starts_of C. ! S'. (s,S'):R --> S' Int starts_of A ~={}) &
wenzelm@17233
    52
   (!s t T' a. reachable C s &
mueller@4565
    53
               s -a--C-> t   &
wenzelm@17233
    54
               (t,T') : R
mueller@4565
    55
               --> (? S'. (s,S'):R & (! s':S'. ? t':T'. ? ex. move A ex s' a t')))"
mueller@4565
    56
wenzelm@17233
    57
is_history_relation_def:
wenzelm@17233
    58
  "is_history_relation R C A == is_simulation R C A &
mueller@4565
    59
                                is_ref_map (%x.(@y. (x,y):(R^-1))) A C"
mueller@4565
    60
wenzelm@17233
    61
is_prophecy_relation_def:
wenzelm@17233
    62
  "is_prophecy_relation R C A == is_backward_simulation R C A &
mueller@4565
    63
                                 is_ref_map (%x.(@y. (x,y):(R^-1))) A C"
wenzelm@17233
    64
wenzelm@17233
    65
ML {* use_legacy_bindings (the_context ()) *}
wenzelm@17233
    66
mueller@4565
    67
end