Theory SimCorrectness

(*  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)
  apply (simp add: flift1_def)
  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 add: Consq_def flift1_def)
  apply simp
  done


subsection ‹Properties of move›

lemma move_is_move_sim:
   "is_simulation R C A  reachable C s  s aC 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 (simp add: Let_def)
  apply (rule_tac x = "ex" in someI)
  apply assumption
  done

lemma move_subprop1_sim:
  "is_simulation R C A  reachable C s  s aC 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+
  apply (simp add: move_def)
  done

lemma move_subprop2_sim:
  "is_simulation R C A  reachable C s  s aC 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+
  apply (simp add: move_def)
  done

lemma move_subprop3_sim:
  "is_simulation R C A  reachable C s  s aC 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+
  apply (simp add: move_def)
  done

lemma move_subprop4_sim:
  "is_simulation R C A  reachable C s  s aC 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+
  apply (simp add: move_def)
  done

lemma move_subprop5_sim:
  "is_simulation R C A  reachable C s  s aC 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+
  apply (simp add: move_def)
  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 (simp add: mk_traceConc)
  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  sstarts_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 (simp add: has_trace_def2)
  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 (simp add: corresp_ex_sim_def)
  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 (simp add: executions_def)
  apply (rename_tac s ex)

  text ‹start state›
  apply (rule conjI)
  apply (simp add: sim_starts2 corresp_ex_sim_def)

  text is_execution-fragment›
  apply (simp add: corresp_ex_sim_def)
  apply (rule_tac s = s in correspsim_is_execution)
  apply assumption
  apply (simp add: reachable.reachable_0 sim_starts1)
  done

end