src/HOLCF/IOA/meta_theory/Simulations.thy
author wenzelm
Sun Oct 21 16:27:42 2007 +0200 (2007-10-21)
changeset 25135 4f8176c940cf
parent 19741 f65265d71426
child 35174 e15040ae75d7
permissions -rw-r--r--
modernized specifications ('definition', 'axiomatization');
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
wenzelm@25135
    14
definition
wenzelm@25135
    15
  is_simulation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
wenzelm@25135
    16
  "is_simulation R C A =
wenzelm@25135
    17
   ((!s:starts_of C. R``{s} Int starts_of A ~= {}) &
wenzelm@17233
    18
   (!s s' t a. reachable C s &
mueller@4565
    19
               s -a--C-> t   &
wenzelm@17233
    20
               (s,s') : R
wenzelm@25135
    21
               --> (? t' ex. (t,t'):R & move A ex s' a t')))"
mueller@4565
    22
wenzelm@25135
    23
definition
wenzelm@25135
    24
  is_backward_simulation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
wenzelm@25135
    25
  "is_backward_simulation R C A =
wenzelm@25135
    26
   ((!s:starts_of C. R``{s} <= starts_of A) &
wenzelm@17233
    27
   (!s t t' a. reachable C s &
mueller@4565
    28
               s -a--C-> t   &
wenzelm@17233
    29
               (t,t') : R
wenzelm@25135
    30
               --> (? ex s'. (s,s'):R & move A ex s' a t')))"
mueller@4565
    31
wenzelm@25135
    32
definition
wenzelm@25135
    33
  is_forw_back_simulation :: "[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
wenzelm@25135
    34
  "is_forw_back_simulation R C A =
wenzelm@25135
    35
   ((!s:starts_of C. ? S'. (s,S'):R & S'<= starts_of A) &
wenzelm@17233
    36
   (!s S' t a. reachable C s &
mueller@4565
    37
               s -a--C-> t   &
wenzelm@17233
    38
               (s,S') : R
wenzelm@25135
    39
               --> (? T'. (t,T'):R & (! t':T'. ? s':S'. ? ex. move A ex s' a t'))))"
mueller@4565
    40
wenzelm@25135
    41
definition
wenzelm@25135
    42
  is_back_forw_simulation :: "[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
wenzelm@25135
    43
  "is_back_forw_simulation R C A =
wenzelm@25135
    44
   ((!s:starts_of C. ! S'. (s,S'):R --> S' Int starts_of A ~={}) &
wenzelm@17233
    45
   (!s t T' a. reachable C s &
mueller@4565
    46
               s -a--C-> t   &
wenzelm@17233
    47
               (t,T') : R
wenzelm@25135
    48
               --> (? S'. (s,S'):R & (! s':S'. ? t':T'. ? ex. move A ex s' a t'))))"
mueller@4565
    49
wenzelm@25135
    50
definition
wenzelm@25135
    51
  is_history_relation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
wenzelm@25135
    52
  "is_history_relation R C A = (is_simulation R C A &
wenzelm@25135
    53
                                is_ref_map (%x.(@y. (x,y):(R^-1))) A C)"
mueller@4565
    54
wenzelm@25135
    55
definition
wenzelm@25135
    56
  is_prophecy_relation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
wenzelm@25135
    57
  "is_prophecy_relation R C A = (is_backward_simulation R C A &
wenzelm@25135
    58
                                 is_ref_map (%x.(@y. (x,y):(R^-1))) A C)"
wenzelm@17233
    59
wenzelm@19741
    60
wenzelm@19741
    61
lemma set_non_empty: "(A~={}) = (? x. x:A)"
wenzelm@19741
    62
apply auto
wenzelm@19741
    63
done
wenzelm@19741
    64
wenzelm@19741
    65
lemma Int_non_empty: "(A Int B ~= {}) = (? x. x: A & x:B)"
wenzelm@19741
    66
apply (simp add: set_non_empty)
wenzelm@19741
    67
done
wenzelm@19741
    68
wenzelm@19741
    69
wenzelm@25135
    70
lemma Sim_start_convert:
wenzelm@19741
    71
"(R``{x} Int S ~= {}) = (? y. (x,y):R & y:S)"
wenzelm@19741
    72
apply (unfold Image_def)
wenzelm@19741
    73
apply (simp add: Int_non_empty)
wenzelm@19741
    74
done
wenzelm@19741
    75
wenzelm@19741
    76
declare Sim_start_convert [simp]
wenzelm@19741
    77
wenzelm@19741
    78
wenzelm@25135
    79
lemma ref_map_is_simulation:
wenzelm@19741
    80
"!! f. is_ref_map f C A ==> is_simulation {p. (snd p) = f (fst p)} C A"
wenzelm@19741
    81
wenzelm@19741
    82
apply (unfold is_ref_map_def is_simulation_def)
wenzelm@19741
    83
apply simp
wenzelm@19741
    84
done
wenzelm@17233
    85
mueller@4565
    86
end