Quelle  Simulations.thy   Sprache: Isabelle

(*  Title:      HOL/HOLCF/IOA/Simulations.thy
    Author:     Olaf Müller
*)

section ‹Simulations in HOLCF/IOA›

theory Simulations
imports RefCorrectness
begin

default_sort type

definition is_simulation :: "('s1 \ 's2) set \ ('a, 's1) ioa \ ('a, 's2) ioa \ bool"
  where "is_simulation R C A \
    (∀s ∈ starts_of C. R``{s} ∩ 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'))"

definition is_backward_simulation :: "('s1 \ 's2) set \ ('a, 's1) ioa \ ('a, 's2) ioa \ bool"
  where "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'))"

definition is_forw_back_simulation ::
    "('s1 \ 's2 set) set \ ('a, 's1) ioa \ ('a, 's2) ioa \ bool"
  where "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')))"

definition is_back_forw_simulation ::
    "('s1 \ 's2 set) set \ ('a, 's1) ioa \ ('a, 's2) ioa \ bool"
  where "is_back_forw_simulation R C A \
    ((∀s ∈ starts_of C. ∀S'. (s, S') ∈ R ⟶ S' \ 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'))))"

definition is_history_relation :: "('s1 \ 's2) set \ ('a, 's1) ioa \ ('a, 's2) ioa \ bool"
  where "is_history_relation R C A \
    is_simulation R C A ∧ is_ref_map (λx. (SOME y. (x, y) ∈ R^-1)) A C"

definition is_prophecy_relation :: "('s1 \ 's2) set \ ('a, 's1) ioa \ ('a, 's2) ioa \ bool"
  where "is_prophecy_relation R C A \
    is_backward_simulation R C A ∧ is_ref_map (λx. (SOME y. (x, y) ∈ R^-1)) A C"


lemma set_non_empty: "A \ {} \ (\x. x \ A)"
  by auto

lemma Int_non_empty: "A \ B \ {} \ (\x. x \ A \ x \ B)"
  by (simp add: set_non_empty)

lemma Sim_start_convert [simp]: "R``{x} \ S \ {} \ (\y. (x, y) \ R \ y \ S)"
  by (simp add: Image_def Int_non_empty)

lemma ref_map_is_simulation: "is_ref_map f C A \ is_simulation {p. snd p = f (fst p)} C A"
  by (simp add: is_ref_map_def is_simulation_def)

end