Theory RefCorrectness

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

section ‹Correctness of Refinement Mappings in HOLCF/IOA›

theory RefCorrectness
imports RefMappings
begin

definition corresp_exC ::
    "('a, 's2) ioa ⇒ ('s1 ⇒ 's2) ⇒ ('a, 's1) pairs → ('s1 ⇒ ('a, 's2) pairs)"
  where "corresp_exC A f =
    (fix ⋅
      (LAM h ex.
        (λs. case ex of
          nil ⇒ nil
        | x ## xs ⇒
            flift1 (λpr.
              (SOME cex. move A cex (f s) (fst pr) (f (snd pr))) @@ ((h ⋅ xs) (snd pr))) ⋅ x)))"

definition corresp_ex ::
    "('a, 's2) ioa ⇒ ('s1 ⇒ 's2) ⇒ ('a, 's1) execution ⇒ ('a, 's2) execution"
  where "corresp_ex A f ex = (f (fst ex), (corresp_exC A f ⋅ (snd ex)) (fst ex))"

definition is_fair_ref_map ::
    "('s1 ⇒ 's2) ⇒ ('a, 's1) ioa ⇒ ('a, 's2) ioa ⇒ bool"
  where "is_fair_ref_map f C A ⟷
    is_ref_map f C A ∧ (∀ex ∈ executions C. fair_ex C ex ⟶ fair_ex A (corresp_ex A f ex))"

text ‹
  Axioms for fair trace inclusion proof support, not for the correctness proof
  of refinement mappings!

  Note: Everything is superseded by 🗏‹LiveIOA.thy›.
›

axiomatization where
  corresp_laststate:
    "Finite ex ⟹ laststate (corresp_ex A f (s, ex)) = f (laststate (s, ex))"

axiomatization where
  corresp_Finite: "Finite (snd (corresp_ex A f (s, ex))) = Finite ex"

axiomatization where
  FromAtoC:
    "fin_often (λx. P (snd x)) (snd (corresp_ex A f (s, ex))) ⟹
      fin_often (λy. P (f (snd y))) ex"

axiomatization where
  FromCtoA:
    "inf_often (λy. P (fst y)) ex ⟹
      inf_often (λx. P (fst x)) (snd (corresp_ex A f (s,ex)))"


text ‹
  Proof by case on ‹inf W› in ex: If so, ok. If not, only ‹fin W› in ex, ie.
  there is an index ‹i› from which on no ‹W› in ex. But ‹W› inf enabled, ie at
  least once after ‹i› ‹W› is enabled. As ‹W› does not occur after ‹i› and ‹W›
  is ‹enabling_persistent›, ‹W› keeps enabled until infinity, ie. indefinitely
›

axiomatization where
  persistent:
    "inf_often (λx. Enabled A W (snd x)) ex ⟹ en_persistent A W ⟹
      inf_often (λx. fst x ∈ W) ex ∨ fin_often (λx. ¬ Enabled A W (snd x)) ex"

axiomatization where
  infpostcond:
    "is_exec_frag A (s,ex) ⟹ inf_often (λx. fst x ∈ W) ex ⟹
      inf_often (λx. set_was_enabled A W (snd x)) ex"


subsection ‹‹corresp_ex››

lemma corresp_exC_unfold:
  "corresp_exC A f =
    (LAM ex.
      (λs.
        case ex of
          nil ⇒ nil
        | x ## xs ⇒
            (flift1 (λpr.
              (SOME cex. move A cex (f s) (fst pr) (f (snd pr))) @@
              ((corresp_exC A f ⋅ xs) (snd pr))) ⋅ x)))"
  apply (rule trans)
  apply (rule fix_eq2)
  apply (simp only: corresp_exC_def)
  apply (rule beta_cfun)
  apply (simp add: flift1_def)
  done

lemma corresp_exC_UU: "(corresp_exC A f ⋅ UU) s = UU"
  apply (subst corresp_exC_unfold)
  apply simp
  done

lemma corresp_exC_nil: "(corresp_exC A f ⋅ nil) s = nil"
  apply (subst corresp_exC_unfold)
  apply simp
  done

lemma corresp_exC_cons:
  "(corresp_exC A f ⋅ (at ↝ xs)) s =
     (SOME cex. move A cex (f s) (fst at) (f (snd at))) @@
     ((corresp_exC A f ⋅ xs) (snd at))"
  apply (rule trans)
  apply (subst corresp_exC_unfold)
  apply (simp add: Consq_def flift1_def)
  apply simp
  done

declare corresp_exC_UU [simp] corresp_exC_nil [simp] corresp_exC_cons [simp]


subsection ‹Properties of move›

lemma move_is_move:
  "is_ref_map f C A ⟹ reachable C s ⟹ (s, a, t) ∈ trans_of C ⟹
    move A (SOME x. move A x (f s) a (f t)) (f s) a (f t)"
  apply (unfold is_ref_map_def)
  apply (subgoal_tac "∃ex. move A ex (f s) a (f t) ")
  prefer 2
  apply simp
  apply (erule exE)
  apply (rule someI)
  apply assumption
  done

lemma move_subprop1:
  "is_ref_map f C A ⟹ reachable C s ⟹ (s, a, t) ∈ trans_of C ⟹
    is_exec_frag A (f s, SOME x. move A x (f s) a (f t))"
  apply (cut_tac move_is_move)
  defer
  apply assumption+
  apply (simp add: move_def)
  done

lemma move_subprop2:
  "is_ref_map f C A ⟹ reachable C s ⟹ (s, a, t) ∈ trans_of C ⟹
    Finite ((SOME x. move A x (f s) a (f t)))"
  apply (cut_tac move_is_move)
  defer
  apply assumption+
  apply (simp add: move_def)
  done

lemma move_subprop3:
  "is_ref_map f C A ⟹ reachable C s ⟹ (s, a, t) ∈ trans_of C ⟹
     laststate (f s, SOME x. move A x (f s) a (f t)) = (f t)"
  apply (cut_tac move_is_move)
  defer
  apply assumption+
  apply (simp add: move_def)
  done

lemma move_subprop4:
  "is_ref_map f C A ⟹ reachable C s ⟹ (s, a, t) ∈ trans_of C ⟹
    mk_trace A ⋅ ((SOME x. move A x (f s) a (f t))) =
      (if a ∈ ext A then a ↝ nil else nil)"
  apply (cut_tac move_is_move)
  defer
  apply assumption+
  apply (simp add: move_def)
  done


subsection ‹TRACE INCLUSION Part 1: Traces coincide›

subsubsection ‹Lemmata for ‹⟸››

text ‹Lemma 1.1: Distribution of ‹mk_trace› and ‹@@››

lemma mk_traceConc:
  "mk_trace C ⋅ (ex1 @@ ex2) = (mk_trace C ⋅ ex1) @@ (mk_trace C ⋅ ex2)"
  by (simp add: mk_trace_def filter_act_def MapConc)


text ‹Lemma 1 : Traces coincide›

lemma lemma_1:
  "is_ref_map f C A ⟹ ext C = ext A ⟹
    ∀s. reachable C s ∧ is_exec_frag C (s, xs) ⟶
      mk_trace C ⋅ xs = mk_trace A ⋅ (snd (corresp_ex A f (s, xs)))"
  supply if_split [split del]
  apply (unfold corresp_ex_def)
  apply (pair_induct xs simp: is_exec_frag_def)
  text ‹cons case›
  apply (auto simp add: mk_traceConc)
  apply (frule reachable.reachable_n)
  apply assumption
  apply (auto simp add: move_subprop4 split: if_split)
  done


subsection ‹TRACE INCLUSION Part 2: corresp_ex is execution›

subsubsection ‹Lemmata for ‹==>››

text ‹Lemma 2.1›

lemma lemma_2_1 [rule_format]:
  "Finite xs ⟶
    (∀s. is_exec_frag A (s, xs) ∧ is_exec_frag A (t, ys) ∧
      t = laststate (s, xs) ⟶ is_exec_frag A (s, xs @@ ys))"
  apply (rule impI)
  apply Seq_Finite_induct
  text ‹main case›
  apply (auto simp add: split_paired_all)
  done


text ‹Lemma 2 : ‹corresp_ex› is execution›

lemma lemma_2:
  "is_ref_map f C A ⟹
    ∀s. reachable C s ∧ is_exec_frag C (s, xs) ⟶
      is_exec_frag A (corresp_ex A f (s, xs))"
  apply (unfold corresp_ex_def)

  apply simp
  apply (pair_induct xs simp: is_exec_frag_def)

  text ‹main case›
  apply auto
  apply (rule_tac t = "f x2" in lemma_2_1)

  text ‹‹Finite››
  apply (erule move_subprop2)
  apply assumption+
  apply (rule conjI)

  text ‹‹is_exec_frag››
  apply (erule move_subprop1)
  apply assumption+
  apply (rule conjI)

  text ‹Induction hypothesis›
  text ‹‹reachable_n› looping, therefore apply it manually›
  apply (erule_tac x = "x2" in allE)
  apply simp
  apply (frule reachable.reachable_n)
  apply assumption
  apply simp

  text ‹‹laststate››
  apply (erule move_subprop3 [symmetric])
  apply assumption+
  done


subsection ‹Main Theorem: TRACE -- INCLUSION›

theorem trace_inclusion:
  "ext C = ext A ⟹ is_ref_map f 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 A f ex" in bexI)

  text ‹Traces coincide, Lemma 1›
  apply (pair ex)
  apply (erule lemma_1 [THEN spec, THEN mp])
  apply assumption+
  apply (simp add: executions_def reachable.reachable_0)

  text ‹‹corresp_ex› is execution, Lemma 2›
  apply (pair ex)
  apply (simp add: executions_def)
  text ‹start state›
  apply (rule conjI)
  apply (simp add: is_ref_map_def corresp_ex_def)
  text ‹‹is_execution_fragment››
  apply (erule lemma_2 [THEN spec, THEN mp])
  apply (simp add: reachable.reachable_0)
  done


subsection ‹Corollary:  FAIR TRACE -- INCLUSION›

lemma fininf: "(~inf_often P s) = fin_often P s"
  by (auto simp: fin_often_def)

lemma WF_alt: "is_wfair A W (s, ex) =
  (fin_often (λx. ¬ Enabled A W (snd x)) ex ⟶ inf_often (λx. fst x ∈ W) ex)"
  by (auto simp add: is_wfair_def fin_often_def)

lemma WF_persistent:
  "is_wfair A W (s, ex) ⟹ inf_often (λx. Enabled A W (snd x)) ex ⟹
    en_persistent A W ⟹ inf_often (λx. fst x ∈ W) ex"
  apply (drule persistent)
  apply assumption
  apply (simp add: WF_alt)
  apply auto
  done

lemma fair_trace_inclusion:
  assumes "is_ref_map f C A"
    and "ext C = ext A"
    and "⋀ex. ex ∈ executions C ⟹ fair_ex C ex ⟹
      fair_ex A (corresp_ex A f ex)"
  shows "fairtraces C ⊆ fairtraces A"
  apply (insert assms)
  apply (simp add: fairtraces_def fairexecutions_def)
  apply auto
  apply (rule_tac x = "corresp_ex A f ex" in exI)
  apply auto

  text ‹Traces coincide, Lemma 1›
  apply (pair ex)
  apply (erule lemma_1 [THEN spec, THEN mp])
  apply assumption+
  apply (simp add: executions_def reachable.reachable_0)

  text ‹‹corresp_ex› is execution, Lemma 2›
  apply (pair ex)
  apply (simp add: executions_def)
  text ‹start state›
  apply (rule conjI)
  apply (simp add: is_ref_map_def corresp_ex_def)
  text ‹‹is_execution_fragment››
  apply (erule lemma_2 [THEN spec, THEN mp])
  apply (simp add: reachable.reachable_0)
  done

lemma fair_trace_inclusion2:
  "inp C = inp A ⟹ out C = out A ⟹ is_fair_ref_map f C A ⟹
    fair_implements C A"
  apply (simp add: is_fair_ref_map_def fair_implements_def fairtraces_def fairexecutions_def)
  apply auto
  apply (rule_tac x = "corresp_ex A f ex" in exI)
  apply auto

  text ‹Traces coincide, Lemma 1›
  apply (pair ex)
  apply (erule lemma_1 [THEN spec, THEN mp])
  apply (simp (no_asm) add: externals_def)
  apply (auto)[1]
  apply (simp add: executions_def reachable.reachable_0)

  text ‹‹corresp_ex› is execution, Lemma 2›
  apply (pair ex)
  apply (simp add: executions_def)
  text ‹start state›
  apply (rule conjI)
  apply (simp add: is_ref_map_def corresp_ex_def)
  text ‹‹is_execution_fragment››
  apply (erule lemma_2 [THEN spec, THEN mp])
  apply (simp add: reachable.reachable_0)
  done

end