Theory DPN_implEx

(*  Title:       Implementation of DPN pre$^*$-algorithm
    ID:
    Author:      Peter Lammich <peter.lammich@uni-muenster.de>
    Maintainer:  Peter Lammich <peter.lammich@uni-muenster.de>
*)

section ‹Implementation of DPN pre$^*$-algorithm›

theory DPN_implEx
imports DPN FSM_ex
begin
text ‹
  In this section, we provide a straightforward executable specification of the DPN-algorithm. 
  It has a polynomial complexity, but is far from having optimal complexity.
›

subsection ‹ Representation of DPN and M-automata ›
type_synonym 'c rule_ex = "'c×'c×'c×'c list" 
type_synonym 'c DPN_ex = "'c rule_ex list"

definition "rule_repr == { ((p,γ,p',c'),(p#[γ],a,p'#c')) | p γ p' c' a . True }"
definition "rules_repr == { (l,l') . rule_repr `` set l = l' }"

lemma rules_repr_cons: "⟦ (R,S)∈rules_repr ⟧ ⟹ ((p,γ,p',c')∈set R) = (∃a. (p#[γ] ↪⇘a⇙ p'#c') ∈ S)"
  by (unfold rules_repr_def rule_repr_def) blast

text ‹ We define the mapping to sp-states explicitely, well-knowing that it makes the algorithm even more inefficient ›
definition "find_sp d s p == first_that (λt. let (sh,ph,qh)=t in if s=sh ∧ p=ph then Some qh else None) d"

text ‹ This locale describes an M-automata together with its representation used in the implementation ›
locale MFSM_ex = MFSM +
  fixes R and D
  assumes rules_repr: "(R,rules M)∈rules_repr"
  assumes D_above: "δ A ⊆ set D" and D_below: "set D ⊆ ps_upper M A"

text ‹ This lemma exports the additional conditions of locale MFSM\_ex to locale MFSM ›
lemma (in MFSM) MFSM_ex_alt: "MFSM_ex M A R D ⟷ (R,rules M)∈rules_repr ∧ δ A ⊆ set D ∧ set D ⊆ ps_upper M A"
  using MFSM_axioms by (unfold MFSM_def MFSM_ex_def MFSM_ex_axioms_def) (auto)

lemmas (in MFSM_ex) D_between = D_above D_below

text ‹ The representation of the sp-states behaves as expected ›
lemma (in MFSM_ex) find_sp_cons:
  assumes A: "s∈cstates A" "p∈csyms M"
  shows "find_sp D s p = Some (sp A s p)"
proof -
  let ?f = "(λt. let (sh,ph,qh)=t in if s=sh ∧ p=ph then Some qh else None)"
  from A have "(s,p,sp A s p)∈set D" using cstate_succ_ex' D_between by simp
  moreover have "?f (s,p,sp A s p) = Some (sp A s p)" by auto
  ultimately obtain sp' where G: "find_sp D s p = Some sp'"
    using first_thatI1[of "(s,p,sp A s p)" D ?f "sp A s p"] by (unfold find_sp_def, blast)
  with first_thatE1[of ?f D sp'] obtain t where "t∈set D ∧ ?f t=Some sp'" by (unfold find_sp_def, blast)
  hence "(s,p,sp')∈set D" by (cases t, auto split: if_splits)
  with A D_between have "sp'=sp A s p" using cstate_succ_unique' by simp
  with G show ?thesis by simp
qed

subsection ‹ Next-element selection ›
text ‹ The implementation goes straightforward by implementing a function to return the next transition to be added to the transition relation of the automata being saturated ›

definition sel_next:: "'c DPN_ex ⇒ ('s,'c) delta ⇒ ('s × 'c × 's) option" where
  "sel_next R D == 
     first_that (λr. let (p,γ,p',c') = r in
       first_that (λt. let (q,pp',sp') = t in 
         if pp'=p' then
           case find_sp D q p of
             Some spt ⇒ (case lookup (λq'. (spt,γ,q') ∉ set D) D sp' c' of
               Some q' ⇒ Some (spt,γ,q') |
               None ⇒ None
             ) | _ ⇒ None
         else None
       ) D
     ) R"
  
text ‹ The state of our algorithm consists of a representation of the DPN-rules and a representation of the transition relations of the automata being saturated ›
type_synonym ('c,'s) seln_state = "'c DPN_ex × ('s,'c) delta"

text ‹ As long as the next-element function returns elements, these are added to the transition relation and the algorithm is applied recursively. @{text "sel_next_state"} describes the next-state selector function, 
  and @{text "seln_R"} describes the corresponding recursion relation. ›
 
definition
  "sel_next_state S == let (R,D)=S in case sel_next R D of None ⇒ None | Some t ⇒ Some (R,t#D)"

definition
  "seln_R == graph sel_next_state"

lemma seln_R_alt: "seln_R == {((R,D),(R,t#D)) | R D t. sel_next R D = Some t}"
  by (rule eq_reflection, unfold seln_R_def graph_def sel_next_state_def) (auto split: option.split_asm)

subsection ‹ Termination ›
subsubsection ‹ Saturation upper bound ›
text ‹ Before we can define the algorithm as recursive function, we have to prove termination, that is well-foundedness of the corresponding recursion relation @{text "seln_R"} ›

text ‹ We start by defining a trivial finite upper bound for the saturation, simply as the set of all possible transitions in the automata. Intuitively, this bound is valid because the
  saturation algorithm only adds transitions, but never states to the automata ›
definition
  "seln_triv_upper R D == states D × ((fst∘snd) ` (set R) ∪ alpha D) × states D"

lemma seln_triv_upper_finite: "finite (seln_triv_upper R D)" by (unfold seln_triv_upper_def) (auto simp add: states_finite alpha_finite)

lemma D_below_triv_upper: "set D ⊆ seln_triv_upper R D" using statesAlpha_subset 
  by (unfold seln_triv_upper_def) auto

lemma seln_triv_upper_subset_preserve: "set D ⊆ seln_triv_upper A D' ⟹ seln_triv_upper A D ⊆ seln_triv_upper A D'" 
  by (unfold seln_triv_upper_def) (blast intro: statesAlphaI dest: statesE alphaE)

lemma seln_triv_upper_mono: "set D ⊆ set D' ⟹ seln_triv_upper R D ⊆ seln_triv_upper R D'"
  by (unfold seln_triv_upper_def) (auto dest: states_mono alpha_mono)
  
lemma seln_triv_upper_mono_list: "seln_triv_upper R D ⊆ seln_triv_upper R (t#D)" by (auto intro!: seln_triv_upper_mono)
lemma seln_triv_upper_mono_list': "x∈seln_triv_upper R D ⟹ x∈seln_triv_upper R (t#D)" using seln_triv_upper_mono_list by (fast)

text ‹ The trivial upper bound is not changed by inserting a transition to the automata that was already below the upper bound ›
lemma seln_triv_upper_inv: "⟦t∈seln_triv_upper R D; set D' = insert t (set D)⟧ ⟹ seln_triv_upper R D = seln_triv_upper R D'"
  by (unfold seln_triv_upper_def) (auto dest: statesAlpha_insert)

text ‹ States returned by @{text "find_sp"} are valid states of the underlying automaton ›
lemma find_sp_in_states: "find_sp D s p = Some qh ⟹ qh∈states D" by (unfold find_sp_def) (auto dest: first_thatE1 split: if_splits simp add: statesAlphaI)

text ‹ The next-element selection function returns a new transition, that is below the trivial upper bound ›
lemma sel_next_below: 
  assumes A: "sel_next R D = Some t"
  shows "t∉set D ∧ t∈seln_triv_upper R D"
proof -
  {
    fix q a qh b q'
    assume A: "(q,a,qh)∈set D" and B: "(qh,b,q')∈trcl (set D)"
    from B statesAlpha_subset[of D] have "q'∈states D"
      apply -
      apply (erule (1) trcl_structE)
      using A by (simp_all add: statesAlphaI)
  }
  thus ?thesis
    using A
    apply (unfold sel_next_def seln_triv_upper_def)
    apply (clarsimp dest!: first_thatE1 lookupE1 split: if_splits option.split_asm)
    apply (force simp add: find_sp_in_states dest!: first_thatE1 lookupE1 split: if_splits option.split_asm)
    done
qed

text ‹ Hence, it does not change the upper bound ›
corollary sel_next_upper_preserve: "⟦sel_next R D = Some t⟧ ⟹ seln_triv_upper R D = seln_triv_upper R (t#D)" proof -
  have "set (t#D) = insert t (set D)" by auto
  moreover assume "sel_next R D = Some t"
  with sel_next_below have "t∈seln_triv_upper R D" by blast
  ultimately show ?thesis by (blast dest: seln_triv_upper_inv)
qed

subsubsection ‹ Well-foundedness of recursion relation ›
lemma seln_R_wf: "wf (seln_R¯)" proof -
  let ?rel="{((R,D),(R,D')) | R D D'. set D⊂set D' ∧ seln_triv_upper R D = seln_triv_upper R D'}"
  have "seln_R¯ ⊆ ?rel¯"
    apply (unfold seln_R_alt)
    apply (clarsimp, safe)
    apply (blast dest: sel_next_below)
    apply (simp add: seln_triv_upper_mono_list')
    apply (simp add: sel_next_upper_preserve)
    done
  also
  let ?alpha="λx. let (R,D)=x in seln_triv_upper R D - set D"
  let ?rel2="finite_psubset¯"
  have "?rel¯ ⊆ inv_image (?rel2¯) ?alpha" using D_below_triv_upper by (unfold finite_psubset_def, fastforce simp add: inv_image_def seln_triv_upper_finite)
  finally have "seln_R¯ ⊆ inv_image (?rel2¯) ?alpha" .
  moreover
  have "wf (?rel2¯)" using wf_finite_psubset by simp
  hence "wf (inv_image (?rel2¯) ?alpha)" by (rule wf_inv_image)
  ultimately show ?thesis by (blast intro: wf_subset)
qed

subsubsection ‹ Definition of recursive function ›
function pss_algo_rec :: "('c,'s) seln_state ⇒ ('c,'s) seln_state"
  where "pss_algo_rec (R,D) = (case sel_next R D of Some t ⇒ pss_algo_rec (R,t#D) | None ⇒ (R,D))"
  by pat_completeness auto

termination
  apply (relation "seln_R¯")
  apply (simp add: seln_R_wf)
  unfolding seln_R_alt by blast

lemma pss_algo_rec_newsimps[simp]: 
  "⟦sel_next R D = None⟧ ⟹ pss_algo_rec (R,D) = (R,D)"
  "⟦sel_next R D = Some t⟧ ⟹ pss_algo_rec (R,D) = pss_algo_rec (R,t#D)"
  by auto
  
declare pss_algo_rec.simps[simp del]


subsection ‹ Correctness ›
subsubsection ‹ seln\_R refines ps\_R ›
text ‹
  We show that @{term seln_R} refines @{term ps_R}, that is that every step made by our implementation corresponds to a step
  in the nondeterministic algorithm, that we already have proved correct in theory DPN.
›
    
  (* FIXME: Spaghetti-proof*)
lemma (in MFSM_ex) sel_nextE1:
  assumes A: "sel_next R D = Some (s,γ,q')"
  shows "(s,γ,q')∉set D ∧ (∃ q p a c'. s=sp A q p ∧ [p,γ]↪⇘a⇙ c' ∈ rules M ∧ (q,c',q')∈trclAD A (set D))" 
proof -
  let ?f = "λp γ p' c' t. let (q,pp',sp') = t in 
       if pp'=p' then
         case find_sp D q p of
           Some s ⇒ (case lookup (λq'. (s,γ,q') ∉ set D) D sp' c' of
             Some q' ⇒ Some (s,γ,q') |
             None ⇒ None
           ) | _ ⇒ None
       else None"

  let ?f1 = "λr. let (p,γ,p',c') = r in first_that (?f p γ p' c') D"

  from A[unfolded sel_next_def] obtain r where 1: "r∈set R ∧ ?f1 r = Some (s,γ,q')" by (blast dest: first_thatE1)
  then obtain p γh p' c' where 2: "r=(p,γh,p',c') ∧ first_that (?f p γh p' c') D = Some (s,γ,q')" by (cases r) simp 
  then obtain t where 3: "t∈set D ∧ ?f p γh p' c' t = Some (s,γ,q')" by (blast dest: first_thatE1)
  then obtain q sp' where 4: "t=(q,p',sp') ∧ (case find_sp D q p of                
             Some s ⇒ (case lookup (λq'. (s,γh,q') ∉ set D) D sp' c' of
               Some q' ⇒ Some (s,γh,q') |
               None ⇒ None
             ) | _ ⇒ None) = Some (s,γ,q')"
    by (cases t, auto split: if_splits)
  hence 5: "find_sp D q p = Some s ∧ lookup (λq'. (s,γh,q') ∉ set D) D sp' c' = Some q' ∧ γ=γh"
    by (simp split: option.split_asm)
  with 1 2 rules_repr obtain a where 6: "(p#[γ],a,p'#c')∈rules M" by (blast dest: rules_repr_cons)
  hence 7: "p∈csyms M ∧ p'∈csyms M ∧ γ∈ssyms M" by (blast dest: rule_fmt_fs)
  with 3 4 D_below have 8: "q∈cstates A ∧ sp'=sp A q p'" by (blast dest: csym_from_cstate' cstate_succ_unique')
  with 5 7 have 9: "s=sp A q p" using D_above D_below by (auto simp add: find_sp_cons)
  have 10: "(s,γ,q')∉set D ∧ (sp',c',q')∈trclAD A (set D)" using 5 8 uniqueSp 7 states_part D_below ps_upper_below_trivial
    apply - apply (rule lookup_trclAD_E1)
    by auto
  moreover have "(q,p'#c',q')∈trclAD A (set D)" proof -
    from 7 8 sp_pred_ex D_above have "(q,p',sp')∈set D" by auto
    with 10 trclAD.cons show ?thesis using 7 8 alpha_cons states_part by auto
  qed
  ultimately show ?thesis using 9 6 by blast
qed


lemma (in MFSM_ex) sel_nextE2:
  assumes A: "sel_next R D = None"
  shows "¬(∃ q p γ q' a c' t. t∉set D ∧ t=(sp A q p,γ,q') ∧ [p,γ]↪⇘a⇙ c' ∈ rules M ∧ (q,c',q')∈trclAD A (set D))"
proof (clarify) ― ‹ Assume we have such a rule and transition, and infer @{term "sel_next R D ≠ None"} ›
  fix q p γ q' a pc'
  assume C: "(sp A q p, γ, q') ∉ set D" "([p, γ], a, pc') ∈ rules M" "(q, pc', q') ∈ trclAD A (set D)"

  from C obtain p' c' where SYMS: "p∈csyms M ∧ p'∈csyms M ∧ γ∈ssyms M ∧ pc'=p'#c'" by (blast dest: rule_fmt)
  have QCS: "q∈cstates A" "(q,p',sp A q p')∈set D" "(sp A q p',c',q')∈trclAD A (set D)" proof -
    from C SYMS obtain sp' where "(q,p',sp')∈set D ∧ (sp',c',q')∈trclAD A (set D)" by (blast dest: trclAD_uncons)
    moreover with D_below SYMS show "q∈cstates A" by (auto intro: csym_from_cstate')
    ultimately show "(q,p',sp A q p')∈set D" "(sp A q p',c',q')∈trclAD A (set D)" using D_below cstate_succ_unique' by auto
  qed

  from C QCS lookup_trclAD_I1[of "D" "set D" "sp A q p'" c' q' A "(λq''. (sp A q p,γ,q'') ∉ set D)"] obtain q'' where N1: "lookup (λq''. (sp A q p,γ,q'') ∉ set D) D (sp A q p') c' = Some q''" by blast

  let ?f = "λp γ p' c' q pp' sp'.            
         if pp'=p' then
           case find_sp D q p of
             Some s ⇒ (case lookup (λq'. (s,γ,q') ∉ set D) D sp' c' of
               Some q' ⇒ Some (s,γ,q') |
               None ⇒ None
             ) | _ ⇒ None
         else None"


  from SYMS QCS have FIND_SP: "find_sp D q p = Some (sp A q p)" using D_below D_above by (simp add: find_sp_cons)
  let ?f1 = "(λp γ p' c'. (λt. let (q,pp',sp')=t in ?f p γ p' c' q pp' sp'))"
  from N1 FIND_SP have N2: "?f1 p γ p' c' (q,p',sp A q p') = Some (sp A q p, γ, q'')" by auto
  with QCS first_thatI1[of "(q,p',sp A q p')" D "?f1 p γ p' c'"] obtain t' where N3: "first_that (?f1 p γ p' c') D = Some t'" by (blast)
  let ?f2 = "(λr. let (p,γ,p',c') = r in first_that (?f1 p γ p' c') D)"
  from N3 have "?f2 (p,γ,p',c') = Some t'" by auto
  moreover from SYMS C rules_repr have "(p,γ,p',c')∈set R" by (blast dest: rules_repr_cons)
  ultimately obtain t'' where "first_that ?f2 R = Some t''" using first_thatI1[of "(p, γ, p', c')" R ?f2] by (blast)
  hence "sel_next R D = Some t''" by (unfold sel_next_def)
  with A show False by simp
qed

lemmas (in MFSM_ex) sel_nextE = sel_nextE1 sel_nextE2

lemma (in MFSM_ex) seln_cons1: "⟦sel_next R D = Some t⟧ ⟹ (set D,insert t (set D))∈ps_R M A" using D_below by (cases t, auto dest: sel_nextE intro: ps_R.intros)
lemma (in MFSM_ex) seln_cons2: "sel_next R D = None ⟹ set D∉Domain (ps_R M A)" by (blast dest: sel_nextE elim: ps_R.cases)

lemma (in MFSM_ex) seln_cons1_rev: "⟦set D∉Domain (ps_R M A)⟧ ⟹ sel_next R D = None" by (cases "sel_next R D") (auto iff add: seln_cons1 seln_cons2)
lemma (in MFSM_ex) seln_cons2_rev: "⟦set D∈Domain (ps_R M A)⟧ ⟹ ∃t. sel_next R D = Some t ∧ (set D,insert t (set D))∈ps_R M A" 
  by (cases "sel_next R D") (auto iff add: seln_cons1 seln_cons2 ps_R_dom_below)

text ‹ DPN-specific abstraction relation, to associate states of deterministic algorithm with states of @{term ps_R} ›
definition "αseln M A == { (set D, (R,D)) | D R. MFSM_ex M A R D}"

lemma αselnI: "⟦S=set D; MFSM_ex M A R D⟧ ⟹ (S,(R,D))∈αseln M A"
  by (unfold αseln_def) auto

lemma αselnD: "(S,(R,D))∈αseln M A ⟹ S=set D ∧ MFSM_ex M A R D"
  by (unfold αseln_def) auto

lemma αselnD': "(S,C)∈αseln M A ⟹ S=set (snd C) ∧ MFSM_ex M A (fst C) (snd C)" by (cases C, simp add: αselnD)

lemma αseln_single_valued: "single_valued ((αseln M A)¯)"
  by  (unfold αseln_def) (auto intro: single_valuedI)

theorem (in MFSM) seln_refines: "seln_R ≤⇘αseln M A⇙ (ps_R M A)" proof (rule refinesI)
  show "αseln M A O seln_R ⊆ ps_R M A O αseln M A" proof (rule refines_compI)
    fix a c c'
    assume ABS: "(a,c)∈αseln M A" and R: "(c,c')∈seln_R"
    then obtain R D t where 1: "c=(R,D) ∧ c'=(R,t#D) ∧ sel_next R D = Some t" by (unfold seln_R_alt, blast)
    moreover with ABS have 2: "a=set D ∧ MFSM_ex M A R D" by (unfold αseln_def, auto)
    ultimately have 3: "(set D,(set (t#D))) ∈ ps_R M A" using MFSM_ex.seln_cons1[of M A R D] by auto
    moreover have "(set (t#D), (R,t#D))∈αseln M A"
    proof -
      from 2 have "δ A ⊆ set D" using MFSM_ex.D_above[of M A R D] by auto 
      with 3 have "δ A ⊆ set (t#D)" "set (t#D) ⊆ ps_upper M A" using ps_R_below by (fast+)
      with 2 have "MFSM_ex M A R (t#D)" by (unfold MFSM_ex_alt, simp)
      thus ?thesis unfolding αseln_def by auto
    qed
    ultimately show "∃a'. (a, a') ∈ ps_R M A ∧ (a', c') ∈ αseln M A" using 1 2 by blast
  qed
next
  show "αseln M A `` Domain (ps_R M A) ⊆ Domain seln_R"
    apply (rule refines_domI)
    apply (unfold αseln_def seln_R_alt)
    apply (unfold Domain_iff)
    apply (clarsimp)
    apply (fast dest: MFSM_ex.seln_cons2_rev)
    done
qed

subsubsection ‹ Computing transitions only ›
definition pss_algo :: "'c DPN_ex ⇒ ('s,'c) delta ⇒ ('s,'c) delta" where "pss_algo R D ≡ snd (pss_algo_rec (R,D))"


subsubsection ‹ Correctness ›

text ‹ We have to show that the next-state selector function's graph refines @{text "seln_R"}. This is trivial because we defined @{text "seln_R"} to be that graph ›
lemma sns_refines: "graph sel_next_state ≤⇘Id⇙ seln_R" by (unfold seln_R_def) simp

interpretation det_impl: detRef_impl pss_algo_rec sel_next_state seln_R
  apply (rule detRef_impl.intro)
  apply (simp_all only: detRef_wf_transfer[OF seln_R_wf] sns_refines)
  apply (unfold sel_next_state_def)
  apply (auto split: option.splits)
  done

text ‹ And then infer correctness of the deterministic algorithm ›

theorem (in MFSM_ex) pss_correct: 
  assumes D_init: "set D = δ A"
  shows "lang (A⦇ δ:=set (pss_algo R D) ⦈) = pre_star (rules M) A"
proof (rule correct)
  have "(set D, (R,D))∈αseln M A" by (intro refl αselnI) unfold_locales
  moreover have "((R,D),pss_algo_rec (R,D))∈ndet_algo (seln_R)" by (simp add: det_impl.algo_correct)
  ultimately obtain d' where 1: "(d',pss_algo_rec (R,D))∈αseln M A ∧ (set D,d')∈ndet_algo (ps_R M A)" using refines_ndet_algo[OF seln_refines] by blast
  hence "d'=set (snd (pss_algo_rec (R,D)))" by (blast dest: αselnD')
  with 1 show "(δ A, set (pss_algo R D)) ∈ ndet_algo (ps_R M A)" using D_init unfolding pss_algo_def by simp
qed
  
corollary (in MFSM) pss_correct:
  assumes repr: "set D = δ A" "(R,rules M)∈rules_repr"
  shows "lang (A⦇ δ:=set (pss_algo R D) ⦈) = pre_star (rules M) A"
proof -
  interpret MFSM_ex "sep M" M A R D
    apply simp_all
    apply unfold_locales
    apply (simp_all add: repr initial_delta_below)
    done
  from repr show ?thesis by (simp add: pss_correct)
qed

text ‹ Generate executable code ›

export_code pss_algo checking SML


end