# Theory RefCorrectness

theory RefCorrectness
imports RefMappings
```(*  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
```