Theory SimCorrectness

theory SimCorrectness
imports Simulations
```(*  Title:      HOL/HOLCF/IOA/SimCorrectness.thy
Author:     Olaf MÃ¼ller
*)

section ‹Correctness of Simulations in HOLCF/IOA›

theory SimCorrectness
imports Simulations
begin

(*Note: s2 instead of s1 in last argument type!*)
definition corresp_ex_simC ::
"('a, 's2) ioa ⇒ ('s1 × 's2) set ⇒ ('a, 's1) pairs → ('s2 ⇒ ('a, 's2) pairs)"
where "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' = SOME t'. ∃ex1. (t, t') ∈ R ∧ move A ex1 s a t'
in (SOME cex. move A cex s a T') @@ ((h ⋅ xs) T')) ⋅ x))))"

definition corresp_ex_sim ::
"('a, 's2) ioa ⇒ ('s1 × 's2) set ⇒ ('a, 's1) execution ⇒ ('a, 's2) execution"
where "corresp_ex_sim A R ex ≡
let S' = SOME s'. (fst ex, s') ∈ R ∧ s' ∈ starts_of A
in (S', (corresp_ex_simC A R ⋅ (snd ex)) S')"

subsection ‹‹corresp_ex_sim››

lemma corresp_ex_simC_unfold:
"corresp_ex_simC A R =
(LAM ex. (λs. case ex of
nil ⇒ nil
| x ## xs ⇒
(flift1
(λ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)))"
apply (rule trans)
apply (rule fix_eq2)
apply (simp only: corresp_ex_simC_def)
apply (rule beta_cfun)
done

lemma corresp_ex_simC_UU [simp]: "(corresp_ex_simC A R ⋅ UU) s = UU"
apply (subst corresp_ex_simC_unfold)
apply simp
done

lemma corresp_ex_simC_nil [simp]: "(corresp_ex_simC A R ⋅ nil) s = nil"
apply (subst corresp_ex_simC_unfold)
apply simp
done

lemma corresp_ex_simC_cons [simp]:
"(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'))"
apply (rule trans)
apply (subst corresp_ex_simC_unfold)
apply simp
done

subsection ‹Properties of move›

lemma 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'"
supply Let_def [simp del]
apply (unfold is_simulation_def)
(* Does not perform conditional rewriting on assumptions automatically as
usual. Instantiate all variables per hand. Ask Tobias?? *)
apply (subgoal_tac "∃t' ex. (t, t') ∈ R ∧ move A ex s' a t'")
prefer 2
apply simp
apply (erule conjE)
apply (erule_tac x = "s" in allE)
apply (erule_tac x = "s'" in allE)
apply (erule_tac x = "t" in allE)
apply (erule_tac x = "a" in allE)
apply simp
(* Go on as usual *)
apply (erule exE)
apply (drule_tac x = "t'" and P = "λt'. ∃ex. (t, t') ∈ R ∧ move A ex s' a t'" in someI)
apply (erule exE)
apply (erule conjE)
apply (rule_tac x = "ex" in someI)
apply assumption
done

lemma 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')"
apply (cut_tac move_is_move_sim)
defer
apply assumption+
done

lemma 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')"
apply (cut_tac move_is_move_sim)
defer
apply assumption+
done

lemma 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'"
apply (cut_tac move_is_move_sim)
defer
apply assumption+
done

lemma 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 ↝ nil else nil)"
apply (cut_tac move_is_move_sim)
defer
apply assumption+
done

lemma 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"
apply (cut_tac move_is_move_sim)
defer
apply assumption+
done

subsection ‹TRACE INCLUSION Part 1: Traces coincide›

subsubsection "Lemmata for <=="

text ‹Lemma 1: Traces coincide›

lemma traces_coincide_sim [rule_format (no_asm)]:
"is_simulation R C A ⟹ ext C = ext A ⟹
∀s s'. 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')"
supply if_split [split del]
apply (pair_induct ex simp: is_exec_frag_def)
text ‹cons case›
apply auto
apply (rename_tac ex a t s s')
apply (frule reachable.reachable_n)
apply assumption
apply (erule_tac x = "t" in allE)
apply (erule_tac x = "SOME t'. ∃ex1. (t, t') ∈ R ∧ move A ex1 s' a t'" in allE)
apply (simp add: move_subprop5_sim [unfolded Let_def]
move_subprop4_sim [unfolded Let_def] split: if_split)
done

text ‹Lemma 2: ‹corresp_ex_sim› is execution›

lemma correspsim_is_execution [rule_format]:
"is_simulation R C A ⟹
∀s s'. reachable C s ∧ is_exec_frag C (s, ex) ∧ (s, s') ∈ R
⟶ is_exec_frag A (s', (corresp_ex_simC A R ⋅ ex) s')"
apply (pair_induct ex simp: is_exec_frag_def)
text ‹main case›
apply auto
apply (rename_tac ex a t s s')
apply (rule_tac t = "SOME t'. ∃ex1. (t, t') ∈ R ∧ move A ex1 s' a t'" in lemma_2_1)

text ‹Finite›
apply (erule move_subprop2_sim [unfolded Let_def])
apply assumption+
apply (rule conjI)

text ‹‹is_exec_frag››
apply (erule move_subprop1_sim [unfolded Let_def])
apply assumption+
apply (rule conjI)

text ‹Induction hypothesis›
text ‹‹reachable_n› looping, therefore apply it manually›
apply (erule_tac x = "t" in allE)
apply (erule_tac x = "SOME t'. ∃ex1. (t, t') ∈ R ∧ move A ex1 s' a t'" in allE)
apply simp
apply (frule reachable.reachable_n)
apply assumption
apply (simp add: move_subprop5_sim [unfolded Let_def])
text ‹laststate›
apply (erule move_subprop3_sim [unfolded Let_def, symmetric])
apply assumption+
done

subsection ‹Main Theorem: TRACE - INCLUSION›

text ‹
Generate condition ‹(s, S') ∈ R ∧ S' ∈ starts_of A›, the first being
interesting for the induction cases concerning the two lemmas
‹correpsim_is_execution› and ‹traces_coincide_sim›, the second for the start
state case.
‹S' := SOME s'. (s, s') ∈ R ∧ s' ∈ starts_of A›, where ‹s ∈ starts_of C›
›

lemma 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"
apply (simp add: is_simulation_def corresp_ex_sim_def Int_non_empty Image_def)
apply (erule conjE)+
apply (erule ballE)
prefer 2 apply blast
apply (erule exE)
apply (rule someI2)
apply assumption
apply blast
done

lemmas sim_starts1 = simulation_starts [unfolded Let_def, THEN conjunct1]
lemmas sim_starts2 = simulation_starts [unfolded Let_def, THEN conjunct2]

lemma trace_inclusion_for_simulations:
"ext C = ext A ⟹ is_simulation R C A ⟹ traces C ⊆ traces A"
apply (unfold traces_def)
apply auto

text ‹give execution of abstract automata›
apply (rule_tac x = "corresp_ex_sim A R ex" in bexI)

text ‹Traces coincide, Lemma 1›
apply (pair ex)
apply (rename_tac s ex)
apply (rule_tac s = "s" in traces_coincide_sim)
apply assumption+
apply (simp add: executions_def reachable.reachable_0 sim_starts1)

text ‹‹corresp_ex_sim› is execution, Lemma 2›
apply (pair ex)
apply (rename_tac s ex)

text ‹start state›
apply (rule conjI)