(* 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
