# Theory Simulations

Up to index of Isabelle/HOLCF/IOA

theory Simulations
imports RefCorrectness
uses [Simulations.ML]
begin

    (*  Title:      HOLCF/IOA/meta_theory/Simulations.thy
        ID:         $Id: Simulations.thy,v 1.7 2005/09/02 15:24:02 wenzelm Exp $
        Author:     Olaf Müller
    *)

    header {* Simulations in HOLCF/IOA *}

    theory Simulations
    imports RefCorrectness
    begin

    defaultsort type

    consts

      is_simulation            ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
      is_backward_simulation   ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
      is_forw_back_simulation  ::"[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
      is_back_forw_simulation  ::"[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
      is_history_relation      ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
      is_prophecy_relation     ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool"

    defs

    is_simulation_def:
      "is_simulation R C A ==
       (!s:starts_of C. R``{s} Int starts_of A ~= {}) &
       (!s s' t a. reachable C s &
                   s -a--C-> t   &
                   (s,s') : R
                   --> (? t' ex. (t,t'):R & move A ex s' a t'))"

    is_backward_simulation_def:
      "is_backward_simulation R C A ==
       (!s:starts_of C. R``{s} <= starts_of A) &
       (!s t t' a. reachable C s &
                   s -a--C-> t   &
                   (t,t') : R
                   --> (? ex s'. (s,s'):R & move A ex s' a t'))"

    is_forw_back_simulation_def:
      "is_forw_back_simulation R C A ==
       (!s:starts_of C. ? S'. (s,S'):R & S'<= starts_of A) &
       (!s S' t a. reachable C s &
                   s -a--C-> t   &
                   (s,S') : R
                   --> (? T'. (t,T'):R & (! t':T'. ? s':S'. ? ex. move A ex s' a t')))"

    is_back_forw_simulation_def:
      "is_back_forw_simulation R C A ==
       (!s:starts_of C. ! S'. (s,S'):R --> S' Int starts_of A ~={}) &
       (!s t T' a. reachable C s &
                   s -a--C-> t   &
                   (t,T') : R
                   --> (? S'. (s,S'):R & (! s':S'. ? t':T'. ? ex. move A ex s' a t')))"

    is_history_relation_def:
      "is_history_relation R C A == is_simulation R C A &
                                    is_ref_map (%x.(@y. (x,y):(R^-1))) A C"

    is_prophecy_relation_def:
      "is_prophecy_relation R C A == is_backward_simulation R C A &
                                     is_ref_map (%x.(@y. (x,y):(R^-1))) A C"

    ML {* use_legacy_bindings (the_context ()) *}

    end

theorem set_non_empty:

      (A ≠ {}) = (∃x. x ∈ A)

theorem Int_non_empty:

      (A ∩ B ≠ {}) = (∃x. x ∈ A ∧ x ∈ B)

theorem Sim_start_convert:

      (R `` {x} ∩ S ≠ {}) = (∃y. (x, y) ∈ R ∧ y ∈ S)

theorem ref_map_is_simulation:

      is_ref_map f C A ==> is_simulation {p. snd p = f (fst p)} C A