Theory DPN_impl
section ‹ Non-executable implementation of the DPN pre$^*$-algorithm ›
theory DPN_impl
imports DPN
begin
text ‹
This theory is to explore how to prove the correctness of straightforward implementations of the DPN pre$^*$ algorithm.
It does not provide an executable specification, but uses set-datatype and the SOME-operator to describe a deterministic refinement
of the nondeterministic pre$^*$-algorithm. This refinement is then characterized as a recursive function, using recdef.
This proof uses the same techniques to get the recursive function and prove its correctness as are used for the straightforward executable implementation in DPN\_implEx.
Differences from the executable specification are:
\begin{itemize}
\item The state of the algorithm contains the transition relation that is saturated, thus making the refinement abstraction just a projection onto this component. The executable specification, however, uses
list representation of sets, thus making the refinement abstraction more complex.
\item The termination proof is easier: In this approach, we only do recursion if our state contains a valid M-automata and a consistent transition relation. Using this property,
we can infer termination easily from the termination of @{text "ps_R"}. The executable implementation does not check wether the state is valid, and thus may also do recursion for
invalid states. Thus, the termination argument must also regard those invalid states, and hence must be more general.
\end{itemize}
›
subsection ‹ Definitions ›
type_synonym ('c,'l,'s,'m1,'m2) pss_state = "((('c,'l,'m1) DPN_rec_scheme * ('s,'c,'m2) MFSM_rec_scheme) * ('s,'c) LTS)"
text ‹ Function to select next transition to be added›
definition pss_isNext :: "('c,'l,'m1) DPN_rec_scheme ⇒ ('s,'c,'m2) MFSM_rec_scheme ⇒ ('s,'c) LTS ⇒ ('s*'c*'s) ⇒ bool" where
"pss_isNext M A D t == t∉D ∧ (∃q p γ q' a c'. t=(sp A q p,γ,q') ∧ [p,γ]↪⇘a⇙ c' ∈ rules M ∧ (q,c',q')∈trclAD A D)"
definition "pss_next M A D == if (∃ t. pss_isNext M A D t) then Some (SOME t. pss_isNext M A D t) else None"
text ‹ Next state selector function›
definition
"pss_next_state S == case S of ((M,A),D) ⇒ if MFSM M A ∧ D⊆ps_upper M A then (case pss_next M A D of None ⇒ None | Some t ⇒ Some ((M,A),insert t D) ) else None"
text ‹ Relation describing the deterministic algorithm ›
definition
"pss_R == graph pss_next_state"
lemma pss_nextE1: "pss_next M A D = Some t ⟹ t∉D ∧ (∃ q p γ q' a c'. t=(sp A q p,γ,q') ∧ [p,γ]↪⇘a⇙ c' ∈ rules M ∧ (q,c',q')∈trclAD A D)"
proof -
assume "pss_next M A D = Some t"
hence "pss_isNext M A D t"
apply (unfold pss_next_def)
apply (cases "∃t. pss_isNext M A D t")
by (auto intro: someI)
thus ?thesis by (unfold pss_isNext_def)
qed
lemma pss_nextE2: "pss_next M A D = None ⟹ ¬(∃ q p γ q' a c' t. t∉D ∧ t=(sp A q p,γ,q') ∧ [p,γ]↪⇘a⇙ c' ∈ rules M ∧ (q,c',q')∈trclAD A D)"
proof -
assume "pss_next M A D = None"
hence "¬(∃t. pss_isNext M A D t)"
apply (unfold pss_next_def)
apply (cases "∃t. pss_isNext M A D t")
by auto
thus ?thesis by (unfold pss_isNext_def) blast
qed
lemmas (in MFSM) pss_nextE = pss_nextE1 pss_nextE2
text ‹ The relation of the deterministic algorithm is also the recursion relation of the recursive characterization of the algorithm ›
lemma pss_R_alt[termination_simp]: "pss_R == {(((M,A),D),((M,A),insert t D)) | M A D t. MFSM M A ∧ D⊆ps_upper M A ∧ pss_next M A D = Some t}"
by (rule eq_reflection, unfold pss_R_def graph_def pss_next_state_def) (auto split: option.split_asm if_splits)
subsection ‹ Refining @{term "ps_R"} ›
text ‹ We first show that the next-step relation refines @{text "ps_R M A"}. From this, we will get both termination and correctness ›
text ‹ Abstraction relation to project on the second component of a tuple, with fixed first component ›
definition "αsnd f == { (s,(f,s)) | s. True }"
lemma αsnd_comp_simp: "R O αsnd f = {(s,(f,s'))| s s'. (s,s')∈R}" by (unfold αsnd_def, blast)
lemma αsndI[simp]: "(s,(f,s))∈αsnd f" by (unfold αsnd_def, auto)
lemma αsndE: "(s,(f,s'))∈αsnd f' ⟹ f=f' ∧ s=s'" by (unfold αsnd_def, auto)
text ‹ Relation of @{text "pss_next"} and @{text "ps_R M A"} ›
lemma (in MFSM) pss_cons1: "⟦pss_next M A D = Some t; D⊆ps_upper M A⟧ ⟹ (D,insert t D)∈ps_R M A" by (auto dest: pss_nextE intro: ps_R.intros)
lemma (in MFSM) pss_cons2: "pss_next M A D = None ⟹ D∉Domain (ps_R M A)" by (blast dest: pss_nextE elim: ps_R.cases)
lemma (in MFSM) pss_cons1_rev: "⟦D⊆ps_upper M A; D∉Domain (ps_R M A)⟧ ⟹ pss_next M A D = None" by (cases "pss_next M A D") (auto iff add: pss_cons1 pss_cons2)
lemma (in MFSM) pss_cons2_rev: "⟦D∈Domain (ps_R M A)⟧ ⟹ ∃t. pss_next M A D = Some t ∧ (D,insert t D)∈ps_R M A"
by (cases "pss_next M A D") (auto iff add: pss_cons1 pss_cons2 ps_R_dom_below)
text ‹ The refinement result ›
theorem (in MFSM) pss_refines: "pss_R ≤⇘αsnd (M,A)⇙ (ps_R M A)" proof (rule refinesI)
show "αsnd (M, A) O pss_R ⊆ ps_R M A O αsnd (M, A)" by (rule refines_compI, unfold αsnd_def pss_R_alt) (blast intro: pss_cons1)
next
show "αsnd (M, A) `` Domain (ps_R M A) ⊆ Domain pss_R"
apply (rule refines_domI)
unfolding αsnd_def pss_R_alt Domain_iff
apply (clarsimp, safe)
subgoal by unfold_locales
subgoal by (blast dest: ps_R_dom_below)
subgoal by (insert pss_cons2_rev, fast)
done
qed
subsection ‹ Termination ›
text ‹ We can infer termination directly from the well-foundedness of @{term ps_R} and @{thm [source] MFSM.pss_refines} ›
theorem pss_R_wf: "wf (pss_R¯)"
proof -
{
fix M A D M' A' D'
assume A: "(((M,A),D),((M',A'),D'))∈pss_R"
then interpret MFSM "sep M" M A
apply (unfold pss_R_alt MFSM_def)
apply blast
apply simp
done
from pss_refines ps_R_wf have "pss_R≤⇘αsnd (M, A)⇙ps_R M A ∧ wf ((ps_R M A)¯)" by simp
} note A=this
show ?thesis
apply (rule refines_wf[ of pss_R snd "λr. αsnd (fst r)" "λr. let (M,A)=fst r in ps_R M A"])
using A
by fastforce
qed
subsection "Recursive characterization"
text ‹ Having proved termination, we can characterize our algorithm as a recursive function ›
function pss_algo_rec :: "(('c,'l,'s,'m1,'m2) pss_state) ⇒ (('c,'l,'s,'m1,'m2) pss_state)" where
"pss_algo_rec ((M,A),D) = (if (MFSM M A ∧ D⊆ps_upper M A) then (case (pss_next M A D) of None ⇒ ((M,A),D) | (Some t) ⇒ pss_algo_rec ((M,A),insert t D)) else ((M,A),D))"
by pat_completeness auto
termination
apply (relation "pss_R¯")
apply (simp add: pss_R_wf)
using pss_R_alt by fastforce
lemma pss_algo_rec_newsimps[simp]:
"⟦MFSM M A; D⊆ps_upper M A; pss_next M A D = None⟧ ⟹ pss_algo_rec ((M,A),D) = ((M,A),D)"
"⟦MFSM M A; D⊆ps_upper M A; pss_next M A D = Some t⟧ ⟹ pss_algo_rec ((M,A),D) = pss_algo_rec ((M,A),insert t D)"
"¬MFSM M A ⟹ pss_algo_rec ((M,A),D) = ((M,A),D)"
"¬(D ⊆ ps_upper M A) ⟹ pss_algo_rec ((M,A),D) = ((M,A),D)"
by auto
declare pss_algo_rec.simps[simp del]
subsection ‹ Correctness ›
text ‹ The correctness of the recursive version of our algorithm can be inferred using the results from the locale @{text detRef_impl} ›
interpretation det_impl: detRef_impl pss_algo_rec pss_next_state pss_R
apply (rule detRef_impl.intro)
apply (simp_all add: detRef_wf_transfer[OF pss_R_wf] pss_R_def)
subgoal for s s'
unfolding pss_next_state_def
by (auto split: if_splits prod.splits option.splits)
subgoal for s
apply (unfold pss_next_state_def)
apply (clarsimp split: prod.splits if_splits option.splits)
using pss_algo_rec_newsimps(3,4) by blast
done
theorem (in MFSM) pss_correct: "lang (A⦇ δ:=snd (pss_algo_rec ((M,A),(δ A))) ⦈) = pre_star (rules M) A"
proof -
have "(((M,A),δ A), pss_algo_rec ((M,A),δ A))∈ndet_algo pss_R" by (rule det_impl.algo_correct)
moreover have "(δ A, ((M,A),δ A))∈αsnd (M,A)" by simp
ultimately obtain D' where 1: "(D', pss_algo_rec ((M,A),δ A)) ∈ αsnd (M,A)" and "(δ A,D')∈ndet_algo (ps_R M A)" using pss_refines by (blast dest: refines_ndet_algo)
with correct have "lang (A⦇δ := D'⦈) = pre⇧* (rules M) A" by auto
moreover from 1 have "snd (pss_algo_rec ((M,A),δ A)) = D'" by (unfold αsnd_def, auto)
ultimately show ?thesis by auto
qed
end