# Theory Simulations

theory Simulations
imports RefCorrectness
```(*  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¯)) 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¯)) A C"

lemma set_non_empty: "A ≠ {} ⟷ (∃x. x ∈ A)"
by auto

lemma Int_non_empty: "A ∩ B ≠ {} ⟷ (∃x. x ∈ A ∧ x ∈ B)"