(* Title: HOL/HOLCF/IOA/RefCorrectness.thy
Author: Olaf Müller
*)
section \<open>Correctness of Refinement Mappings in HOLCF/IOA\<close>
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 \<cdot>
(LAM h ex.
(\<lambda>s. case ex of
nil \<Rightarrow> nil
| x ## xs \<Rightarrow>
flift1 (\<lambda>pr.
(SOME cex. move A cex (f s) (fst pr) (f (snd pr))) @@ ((h \<cdot> xs) (snd pr))) \<cdot> 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 \<and> (\<forall>ex \<in> executions C. fair_ex C ex \<longrightarrow> fair_ex A (corresp_ex A f ex))"
text \<open>
Axioms for fair trace inclusion proof support, not for the correctness proof
of refinement mappings!
Note: Everything is superseded by \<^file>\<open>LiveIOA.thy\<close>.
\<close>
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 (\<lambda>y. P (f (snd y))) ex"
axiomatization where
FromCtoA:
"inf_often (\y. P (fst y)) ex \
inf_often (\<lambda>x. P (fst x)) (snd (corresp_ex A f (s,ex)))"
text \<open>
Proof by case on \<open>inf W\<close> in ex: If so, ok. If not, only \<open>fin W\<close> in ex, ie.
there is an index \<open>i\<close> from which on no \<open>W\<close> in ex. But \<open>W\<close> inf enabled, ie at
least once after \<open>i\<close> \<open>W\<close> is enabled. As \<open>W\<close> does not occur after \<open>i\<close> and \<open>W\<close>
is \<open>enabling_persistent\<close>, \<open>W\<close> keeps enabled until infinity, ie. indefinitely
\<close>
axiomatization where
persistent:
"inf_often (\x. Enabled A W (snd x)) ex \ en_persistent A W \
inf_often (\<lambda>x. fst x \<in> W) ex \<or> fin_often (\<lambda>x. \<not> Enabled A W (snd x)) ex"
axiomatization where
infpostcond:
"is_exec_frag A (s,ex) \ inf_often (\x. fst x \ W) ex \
inf_often (\<lambda>x. set_was_enabled A W (snd x)) ex"
subsection \<open>\<open>corresp_ex\<close>\<close>
lemma corresp_exC_unfold:
"corresp_exC A f =
(LAM ex.
(\<lambda>s.
case ex of
nil \<Rightarrow> nil
| x ## xs \<Rightarrow>
(flift1 (\<lambda>pr.
(SOME cex. move A cex (f s) (fst pr) (f (snd pr))) @@
((corresp_exC A f \<cdot> xs) (snd pr))) \<cdot> 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 \<cdot> 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 \<open>Properties of move\<close>
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 \<cdot> ((SOME x. move A x (f s) a (f t))) =
(if a \<in> ext A then a \<leadsto> nil else nil)"
apply (cut_tac move_is_move)
defer
apply assumption+
apply (simp add: move_def)
done
subsection \<open>TRACE INCLUSION Part 1: Traces coincide\<close>
subsubsection \<open>Lemmata for \<open>\<Longleftarrow>\<close>\<close>
text \<open>Lemma 1.1: Distribution of \<open>mk_trace\<close> and \<open>@@\<close>\<close>
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 \<open>Lemma 1 : Traces coincide\<close>
lemma lemma_1:
"is_ref_map f C A \ ext C = ext A \
\<forall>s. reachable C s \<and> is_exec_frag C (s, xs) \<longrightarrow>
mk_trace C \<cdot> xs = mk_trace A \<cdot> (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 \<open>cons case\<close>
apply (auto simp add: mk_traceConc)
apply (frule reachable.reachable_n)
apply assumption
apply (auto simp add: move_subprop4 split: if_split)
done
subsection \<open>TRACE INCLUSION Part 2: corresp_ex is execution\<close>
subsubsection \<open>Lemmata for \<open>==>\<close>\<close>
text \<open>Lemma 2.1\<close>
lemma lemma_2_1 [rule_format]:
"Finite xs \
(\<forall>s. is_exec_frag A (s, xs) \<and> is_exec_frag A (t, ys) \<and>
t = laststate (s, xs) \<longrightarrow> is_exec_frag A (s, xs @@ ys))"
apply (rule impI)
apply Seq_Finite_induct
text \<open>main case\<close>
apply (auto simp add: split_paired_all)
done
text \<open>Lemma 2 : \<open>corresp_ex\<close> is execution\<close>
lemma lemma_2:
"is_ref_map f C A \
\<forall>s. reachable C s \<and> is_exec_frag C (s, xs) \<longrightarrow>
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 \<open>main case\<close>
apply auto
apply (rule_tac t = "f x2" in lemma_2_1)
text \<open>\<open>Finite\<close>\<close>
apply (erule move_subprop2)
apply assumption+
apply (rule conjI)
text \<open>\<open>is_exec_frag\<close>\<close>
apply (erule move_subprop1)
apply assumption+
apply (rule conjI)
text \<open>Induction hypothesis\<close>
text \<open>\<open>reachable_n\<close> looping, therefore apply it manually\<close>
apply (erule_tac x = "x2" in allE)
apply simp
apply (frule reachable.reachable_n)
apply assumption
apply simp
text \<open>\<open>laststate\<close>\<close>
apply (erule move_subprop3 [symmetric])
apply assumption+
done
subsection \<open>Main Theorem: TRACE -- INCLUSION\<close>
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 \<open>give execution of abstract automata\<close>
apply (rule_tac x = "corresp_ex A f ex" in bexI)
text \<open>Traces coincide, Lemma 1\<close>
apply (pair ex)
apply (erule lemma_1 [THEN spec, THEN mp])
apply assumption+
apply (simp add: executions_def reachable.reachable_0)
text \<open>\<open>corresp_ex\<close> is execution, Lemma 2\<close>
apply (pair ex)
apply (simp add: executions_def)
text \<open>start state\<close>
apply (rule conjI)
apply (simp add: is_ref_map_def corresp_ex_def)
text \<open>\<open>is_execution_fragment\<close>\<close>
apply (erule lemma_2 [THEN spec, THEN mp])
apply (simp add: reachable.reachable_0)
done
subsection \<open>Corollary: FAIR TRACE -- INCLUSION\<close>
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 (\<lambda>x. \<not> Enabled A W (snd x)) ex \<longrightarrow> inf_often (\<lambda>x. fst x \<in> 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 \<Longrightarrow> inf_often (\<lambda>x. fst x \<in> 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 \<open>Traces coincide, Lemma 1\<close>
apply (pair ex)
apply (erule lemma_1 [THEN spec, THEN mp])
apply assumption+
apply (simp add: executions_def reachable.reachable_0)
text \<open>\<open>corresp_ex\<close> is execution, Lemma 2\<close>
apply (pair ex)
apply (simp add: executions_def)
text \<open>start state\<close>
apply (rule conjI)
apply (simp add: is_ref_map_def corresp_ex_def)
text \<open>\<open>is_execution_fragment\<close>\<close>
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 \<open>Traces coincide, Lemma 1\<close>
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 \<open>\<open>corresp_ex\<close> is execution, Lemma 2\<close>
apply (pair ex)
apply (simp add: executions_def)
text \<open>start state\<close>
apply (rule conjI)
apply (simp add: is_ref_map_def corresp_ex_def)
text \<open>\<open>is_execution_fragment\<close>\<close>
apply (erule lemma_2 [THEN spec, THEN mp])
apply (simp add: reachable.reachable_0)
done
end
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
