Up to index of Isabelle/HOLCF/IOA
theory SimCorrectness(* Title: HOLCF/IOA/meta_theory/SimCorrectness.thy ID: $Id: SimCorrectness.thy,v 1.5 2005/09/02 15:24:02 wenzelm Exp $ Author: Olaf Müller *) header {* Correctness of Simulations in HOLCF/IOA *} theory SimCorrectness imports Simulations begin consts corresp_ex_sim ::"('a,'s2)ioa => (('s1 *'s2)set) => ('a,'s1)execution => ('a,'s2)execution" (* Note: s2 instead of s1 in last argument type !! *) corresp_ex_simC ::"('a,'s2)ioa => (('s1 * 's2)set) => ('a,'s1)pairs -> ('s2 => ('a,'s2)pairs)" defs corresp_ex_sim_def: "corresp_ex_sim A R ex == let S'= (@s'.(fst ex,s'):R & s': starts_of A) in (S',(corresp_ex_simC A R$(snd ex)) S')" corresp_ex_simC_def: "corresp_ex_simC A R == (fix$(LAM h ex. (%s. case ex of nil => nil | x##xs => (flift1 (%pr. let a = (fst pr); t = (snd pr); T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t' in (@cex. move A cex s a T') @@ ((h$xs) T')) $x) )))" ML {* use_legacy_bindings (the_context ()) *} end
theorem corresp_ex_simC_unfold:
corresp_ex_simC A R = (LAM ex. (%s. case ex of nil => nil | x ## xs => (FLIFT pr. let a >>= fst pr; t >>= snd pr; T' >>= (SOME t'. ∃ex1. (t, t') ∈ R ∧ move A ex1 s a t') in (SOME cex. move A cex s a T') @@ (corresp_ex_simC A R·xs) T')·x))
theorem corresp_ex_simC_UU:
(corresp_ex_simC A R·UU) s = UU
theorem corresp_ex_simC_nil:
(corresp_ex_simC A R·nil) s = nil
theorem corresp_ex_simC_cons:
(corresp_ex_simC A R·((a, t)>>xs)) s = (let T' >>= (SOME t'. ∃ex1. (t, t') ∈ R ∧ move A ex1 s a t') in (SOME cex. move A cex s a T') @@ (corresp_ex_simC A R·xs) T')
theorem move_is_move_sim:
[| is_simulation R C A; reachable C s; s -a--C-> t; (s, s') ∈ R |] ==> let T' >>= (SOME t'. ∃ex1. (t, t') ∈ R ∧ move A ex1 s' a t') in (t, T') ∈ R ∧ move A (SOME ex2. move A ex2 s' a T') s' a T'
theorem move_subprop1_sim:
[| is_simulation R C A; reachable C s; s -a--C-> t; (s, s') ∈ R |] ==> let T' >>= (SOME t'. ∃ex1. (t, t') ∈ R ∧ move A ex1 s' a t') in is_exec_frag A (s', SOME x. move A x s' a T')
theorem move_subprop2_sim:
[| is_simulation R C A; reachable C s; s -a--C-> t; (s, s') ∈ R |] ==> let T' >>= (SOME t'. ∃ex1. (t, t') ∈ R ∧ move A ex1 s' a t') in Finite (SOME x. move A x s' a T')
theorem move_subprop3_sim:
[| is_simulation R C A; reachable C s; s -a--C-> t; (s, s') ∈ R |] ==> let T' >>= (SOME t'. ∃ex1. (t, t') ∈ R ∧ move A ex1 s' a t') in laststate (s', SOME x. move A x s' a T') = T'
theorem move_subprop4_sim:
[| is_simulation R C A; reachable C s; s -a--C-> t; (s, s') ∈ R |] ==> let T' >>= (SOME t'. ∃ex1. (t, t') ∈ R ∧ move A ex1 s' a t') in mk_trace A·(SOME x. move A x s' a T') = (if a ∈ ext A then [a!] else nil)
theorem move_subprop5_sim:
[| is_simulation R C A; reachable C s; s -a--C-> t; (s, s') ∈ R |] ==> let T' >>= (SOME t'. ∃ex1. (t, t') ∈ R ∧ move A ex1 s' a t') in (t, T') ∈ R
theorem traces_coincide_sim:
[| is_simulation R C A; ext C = ext A; reachable C s ∧ is_exec_frag C (s, ex) ∧ (s, s') ∈ R |] ==> mk_trace C·ex = mk_trace A·((corresp_ex_simC A R·ex) s')
theorem correspsim_is_execution:
[| is_simulation R C A; reachable C s ∧ is_exec_frag C (s, ex) ∧ (s, s') ∈ R |] ==> is_exec_frag A (s', (corresp_ex_simC A R·ex) s')
theorem simulation_starts:
[| is_simulation R C A; s ∈ starts_of C |] ==> let S' >>= (SOME s'. (s, s') ∈ R ∧ s' ∈ starts_of A) in (s, S') ∈ R ∧ S' ∈ starts_of A
theorem sim_starts1:
[| is_simulation R C A; s ∈ starts_of C |] ==> (s, SOME s'. (s, s') ∈ R ∧ s' ∈ starts_of A) ∈ R
theorem sim_starts2:
[| is_simulation R C A; s ∈ starts_of C |] ==> (SOME s'. (s, s') ∈ R ∧ s' ∈ starts_of A) ∈ starts_of A
theorem trace_inclusion_for_simulations:
[| ext C = ext A; is_simulation R C A |] ==> traces C ⊆ traces A