Theory Simple_Impl

section ‹Simple Data Structures›
theory Simple_Impl
imports 
  "../Structural/Rec_Impl"
  "../Structural/Tailrec_Impl"
begin

text ‹
  We provide some very basic data structures to implement the DFS state
›

subsection ‹ Stack, Pending Stack, and Visited Set ›
record 'v simple_state =
  ss_stack :: "('v × 'v set) list"
  on_stack :: "'v set"
  visited :: "'v set"

definition [to_relAPP]: "simple_state_rel erel ≡ { (s,s') .
  ss_stack s = map (λu. (u,pending s' `` {u})) (stack s') ∧
  on_stack s = set (stack s') ∧
  visited s = dom (discovered s') ∧
  dom (finished s') = dom (discovered s') - set (stack s') ∧ ― ‹TODO: Hmm, this is an invariant of the abstract›
  set (stack s') ⊆ dom (discovered s') ∧
  (simple_state.more s, state.more s') ∈ erel
}"

lemma simple_state_relI:
  assumes 
  "dom (finished s') = dom (discovered s') - set (stack s')"
  "set (stack s') ⊆ dom (discovered s')"
  "(m', state.more s') ∈ erel"
  shows "(⦇
    ss_stack = map (λu. (u,pending s' `` {u})) (stack s'),
    on_stack = set (stack s'),
    visited = dom (discovered s'),
    … = m'
  ⦈, s')∈⟨erel⟩simple_state_rel"
  using assms
  unfolding simple_state_rel_def
  by auto

lemma simple_state_more_refine[param]: 
  "(simple_state.more_update, state.more_update)
    ∈ (R → R) → ⟨R⟩simple_state_rel → ⟨R⟩simple_state_rel"
  apply (clarsimp simp: simple_state_rel_def) 
  apply parametricity
  done


text ‹ We outsource the definitions in a separate locale, as we want to re-use them
  for similar implementations ›
locale pre_simple_impl = graph_defs
begin

  definition "init_impl e 
    ≡ RETURN ⦇ ss_stack = [], on_stack = {}, visited = {}, … = e ⦈"

  definition "is_empty_stack_impl s ≡ (ss_stack s = [])"
  definition "is_discovered_impl u s ≡ (u∈visited s)"
  definition "is_finished_impl u s ≡ (u∈visited s - (on_stack s))"

  definition "finish_impl u s ≡ do {
    ASSERT (ss_stack s ≠ [] ∧ u∈on_stack s);
    let s = s⦇ss_stack := tl (ss_stack s)⦈;
    let s = s⦇on_stack := on_stack s - {u}⦈;
    RETURN s
    }"
  
  definition "get_pending_impl s ≡ do {
      ASSERT (ss_stack s ≠ []);
      let (u,Vs) = hd (ss_stack s);
      if Vs = {} then
        RETURN (u,None,s)
      else do {
        v ← SPEC (λv. v∈Vs);
        let Vs = Vs - {v};
        let s = s⦇ ss_stack := (u,Vs) # tl (ss_stack s) ⦈;
        RETURN (u, Some v, s)
      }
    }"
  
  definition "discover_impl u v s ≡ do {
    ASSERT (v∉on_stack s ∧ v∉visited s);
    let s = s⦇ss_stack := (v,E``{v}) # ss_stack s⦈;
    let s = s⦇on_stack := insert v (on_stack s)⦈;
    let s = s⦇visited := insert v (visited s)⦈;
    RETURN s
    }"
  
  definition "new_root_impl v0 s ≡ do {
    ASSERT (v0∉visited s);
    let s = s⦇ss_stack := [(v0,E``{v0})]⦈;
    let s = s⦇on_stack := {v0}⦈;
    let s = s⦇visited := insert v0 (visited s)⦈;
    RETURN s
    }"

  definition "gbs ≡ ⦇
    gbs_init = init_impl,
    gbs_is_empty_stack = is_empty_stack_impl ,
    gbs_new_root =  new_root_impl ,
    gbs_get_pending = get_pending_impl ,
    gbs_finish =  finish_impl ,
    gbs_is_discovered = is_discovered_impl ,
    gbs_is_finished = is_finished_impl ,
    gbs_back_edge = (λu v s. RETURN s) ,
    gbs_cross_edge = (λu v s. RETURN s) ,
    gbs_discover = discover_impl
  ⦈"

  lemmas gbs_simps[simp, DFS_code_unfold] = gen_basic_dfs_struct.simps[mk_record_simp, OF gbs_def]

  lemmas impl_defs[DFS_code_unfold] 
  = init_impl_def is_empty_stack_impl_def new_root_impl_def
    get_pending_impl_def finish_impl_def is_discovered_impl_def 
    is_finished_impl_def discover_impl_def

end

text ‹
  Simple implementation of a DFS. This locale assumes a refinement of the
  parameters, and provides an implementation via a stack and a visited set.
›
locale simple_impl_defs =
  a: param_DFS_defs G param
  + c: pre_simple_impl
  + gen_param_dfs_refine_defs 
    where gbsi = c.gbs 
    and gbs = a.gbs
    and upd_exti = simple_state.more_update
    and upd_ext = state.more_update
    and V0i = a.V0
    and V0 = a.V0
begin

  sublocale tailrec_impl_defs G c.gds .


  definition "get_pending s ≡ ⋃(set (map (λ(u,Vs). {u}×Vs) (ss_stack s)))"
  definition "get_stack s ≡ map fst (ss_stack s)"
  definition choose_pending 
    :: "'v ⇒ 'v option ⇒ ('v,'d) simple_state_scheme ⇒ ('v,'d) simple_state_scheme nres"
    where [DFS_code_unfold]: 
  "choose_pending u vo s ≡ 
    case vo of
      None ⇒ RETURN s
    | Some v ⇒ do {
        ASSERT (ss_stack s ≠ []);
        let (u,Vs) = hd (ss_stack s);
        RETURN (s⦇ ss_stack := (u,Vs-{v})#tl (ss_stack s)⦈)
      }"

  sublocale rec_impl_defs G c.gds get_pending get_stack choose_pending .
end
  

locale simple_impl =
  a: param_DFS
  + simple_impl_defs
  + param_refinement
    where gbsi = c.gbs
    and gbs = a.gbs
    and upd_exti = simple_state.more_update
    and upd_ext = state.more_update
    and V0i = a.V0
    and V0 = a.V0
    and V=Id
    and S = "⟨ES⟩simple_state_rel"
begin

  lemma init_impl: "(ei, e) ∈ ES ⟹
    c.init_impl ei ≤⇓(⟨ES⟩simple_state_rel) (RETURN (a.empty_state e))"
    unfolding c.init_impl_def a.empty_state_def simple_state_rel_def
    by (auto)

  lemma new_root_impl: 
    "⟦a.gen_dfs.pre_new_root v0 s; 
      (v0i, v0)∈Id; (si, s) ∈ ⟨ES⟩simple_state_rel⟧
      ⟹ c.new_root_impl v0 si ≤⇓(⟨ES⟩simple_state_rel) (RETURN (a.new_root v0 s))"
      unfolding simple_state_rel_def a.gen_dfs.pre_new_root_def c.new_root_impl_def
      by (auto simp add: a.pred_defs)
  
  lemma get_pending_impl: "
    ⟦a.gen_dfs.pre_get_pending s; (si, s) ∈ ⟨ES⟩simple_state_rel⟧
      ⟹ c.get_pending_impl si 
          ≤ ⇓ (Id ×⇩r Id ×⇩r ⟨ES⟩simple_state_rel) (a.get_pending s)"
    apply (unfold a.get_pending_def c.get_pending_impl_def) []
    apply (refine_rcg bind_refine' Let_refine' IdI)
    apply (refine_dref_type)
    apply (auto 
        simp: simple_state_rel_def a.gen_dfs.pre_defs a.pred_defs neq_Nil_conv
        dest: DFS_invar.stack_distinct
      )
    done

  lemma inres_get_pending_None_conv: "inres (a.get_pending s0) (v, None, s) 
      ⟷ s=s0 ∧ v=hd (stack s0) ∧ pending s0``{hd (stack s0)} = {}" 
    unfolding a.get_pending_def
    by (auto simp add: refine_pw_simps)
  
  lemma inres_get_pending_Some_conv: "inres (a.get_pending s0) (v,Some Vs,s) 
      ⟷ v = hd (stack s) ∧ s = s0⦇pending := pending s0 - {(hd (stack s0), Vs)}⦈
       ∧ (hd (stack s0), Vs) ∈ pending s0"
    unfolding a.get_pending_def
    by (auto simp add: refine_pw_simps)
  
  lemma finish_impl:
    "⟦a.gen_dfs.pre_finish v s0 s; (vi, v)∈Id; (si, s) ∈ ⟨ES⟩simple_state_rel⟧
     ⟹ c.finish_impl v si ≤⇓(⟨ES⟩simple_state_rel) (RETURN (a.finish v s))"
      unfolding simple_state_rel_def a.gen_dfs.pre_defs c.finish_impl_def
       
      (* Proof is fine-tuned to optimize speed *)
      apply (clarsimp simp: inres_get_pending_None_conv)
      apply (frule DFS_invar.stack_distinct)
      apply (simp add: a.pred_defs map_tl) 
      apply (clarsimp simp: neq_Nil_conv) 
      apply blast
      done
  
  lemma cross_edge_impl: "
    ⟦a.gen_dfs.pre_cross_edge u v s0 s; 
      (ui, u)∈Id; (vi, v)∈Id; (si, s) ∈ ⟨ES⟩simple_state_rel⟧
      ⟹ (si, a.cross_edge u v s) ∈ ⟨ES⟩simple_state_rel"
    unfolding simple_state_rel_def a.gen_dfs.pre_defs
    by simp
  
  lemma back_edge_impl: "
    ⟦a.gen_dfs.pre_back_edge u v s0 s; 
      (ui, u)∈Id; (vi, v)∈Id; (si, s) ∈ ⟨ES⟩simple_state_rel⟧
      ⟹ (si, a.back_edge u v s) ∈ ⟨ES⟩simple_state_rel"
    unfolding simple_state_rel_def a.gen_dfs.pre_defs
    by simp
  
  lemma discover_impl:
    "⟦a.gen_dfs.pre_discover u v s0 s; (ui, u)∈Id; (vi, v)∈Id; (si, s) ∈ ⟨ES⟩simple_state_rel⟧
     ⟹ c.discover_impl ui vi si ≤⇓(⟨ES⟩simple_state_rel) (RETURN (a.discover u v s))"
      unfolding simple_state_rel_def a.gen_dfs.pre_defs c.discover_impl_def
      apply (rule ASSERT_leI)
      apply (clarsimp simp: inres_get_pending_Some_conv)
      apply (frule DFS_invar.stack_discovered)
      apply (auto simp: a.pred_defs) []

      apply (clarsimp simp: inres_get_pending_Some_conv)
      apply (frule DFS_invar.stack_discovered)
      apply (frule DFS_invar.pending_ssE)
      apply (clarsimp simp: a.pred_defs)
      apply blast
      done

  sublocale gen_param_dfs_refine 
    where gbsi = c.gbs 
    and gbs = a.gbs
    and upd_exti = simple_state.more_update
    and upd_ext = state.more_update
    and V0i = a.V0
    and V0 = a.V0
    and V = Id
    and S = "⟨ES⟩simple_state_rel"
    apply unfold_locales
    apply (simp_all add: is_break_param) (* TODO: Strange effect,   
      the is_break_param subgoal should not be visible at all!*)
    
    apply (auto simp: a.is_discovered_def c.is_discovered_impl_def simple_state_rel_def) []

    apply (auto simp: a.is_finished_def c.is_finished_impl_def simple_state_rel_def) []

    apply (auto simp: a.is_empty_stack_def c.is_empty_stack_impl_def simple_state_rel_def) []

    apply (refine_rcg init_impl)
    
    apply (refine_rcg new_root_impl, simp_all) []

    apply (refine_rcg get_pending_impl) []

    apply (refine_rcg finish_impl, simp_all) []

    apply (refine_rcg cross_edge_impl, simp_all) []

    apply (refine_rcg back_edge_impl, simp_all) []

    apply (refine_rcg discover_impl, simp_all) []
    done

  text ‹ Main outcome of this locale: The simple DFS-Algorithm, which is
    a general DFS scheme itself (and thus open to further refinements),
    and a refinement theorem that states correct refinement of the original DFS ›

  lemma simple_refine[refine]: "c.gen_dfs ≤ ⇓(⟨ES⟩simple_state_rel) a.it_dfs"
    using gen_dfs_refine
    by simp

  lemma simple_refineT[refine]: "c.gen_dfsT ≤ ⇓(⟨ES⟩simple_state_rel) a.it_dfsT"
    using gen_dfsT_refine
    by simp


  text ‹Link with tail-recursive implementation›

  sublocale tailrec_impl G c.gds
    apply unfold_locales
    apply (simp_all add: c.do_action_defs c.impl_defs[abs_def])
    apply (auto simp: pw_leof_iff refine_pw_simps split: prod.splits)
    done

  lemma simple_tailrec_refine[refine]: "tailrec_impl ≤ ⇓(⟨ES⟩simple_state_rel) a.it_dfs"
  proof -
    note tailrec_impl also note simple_refine finally show ?thesis .
  qed

  lemma simple_tailrecT_refine[refine]: "tailrec_implT ≤ ⇓(⟨ES⟩simple_state_rel) a.it_dfsT"
  proof -
    note tailrecT_impl also note simple_refineT finally show ?thesis .
  qed

  text ‹Link to recursive implementation›
  (* TODO: Currently, we have to prove this invar at several places.
    Maybe it's worth to share in a common locale!?
  *)
  lemma reachable_invar: 
    assumes "c.gen_rwof s" 
    shows "set (map fst (ss_stack s)) ⊆ visited s 
      ∧ distinct (map fst (ss_stack s))"
    using assms
    apply (induct rule: establish_rwof_invar[rotated -1, consumes 1])
    apply (simp add: c.do_action_defs c.impl_defs[abs_def])
    apply (refine_rcg refine_vcg)
    apply simp

    unfolding c.gen_step_def c.do_action_defs c.impl_defs[abs_def] c.gds_simps c.gbs_simps
    apply (refine_rcg refine_vcg)
    apply simp_all
    apply (fastforce simp: neq_Nil_conv) [] 
    apply (fastforce simp: neq_Nil_conv) [] 
    apply (fastforce simp: neq_Nil_conv) [] 
    apply (fastforce simp: neq_Nil_conv) [] 
    done


  sublocale rec_impl G c.gds get_pending get_stack choose_pending
    apply unfold_locales
    unfolding get_pending_def get_stack_def choose_pending_def
    apply (simp_all add: c.do_action_defs c.impl_defs[abs_def])
    apply (auto simp: pw_leof_iff refine_pw_simps pw_le_iff select_def
      split: prod.split) []
    apply (auto simp: pw_leof_iff refine_pw_simps pw_le_iff select_def
      split: prod.split) []

    apply (rule le_ASSERTI)
    apply (unfold c.pre_defs, clarify) []
    apply (frule reachable_invar)
      
    apply (fastforce simp add: pw_leof_iff refine_pw_simps pw_le_iff neq_Nil_conv
      split: prod.split option.split) []  

    apply (unfold c.pre_defs, clarify) []
    apply (frule reachable_invar)
    apply (auto simp: pw_leof_iff refine_pw_simps pw_le_iff select_def c.impl_defs neq_Nil_conv
      split: prod.split option.split) []

    apply (auto simp: pw_leof_iff refine_pw_simps pw_le_iff select_def neq_Nil_conv c.pre_defs c.impl_defs
      split: prod.split if_split_asm) []

    apply (auto simp: pw_leof_iff refine_pw_simps pw_le_iff split: prod.split) []

    apply (auto simp: pw_leof_iff refine_pw_simps pw_le_iff split: prod.split) []

    apply (auto simp: pw_leof_iff refine_pw_simps pw_le_iff split: prod.split) []
    done

  lemma simple_rec_refine[refine]: "rec_impl ≤ ⇓(⟨ES⟩simple_state_rel) a.it_dfs"
  proof -
    note rec_impl also note simple_refine finally show ?thesis .
  qed

end

text ‹ Autoref Setup ›

record ('si,'nsi)simple_state_impl =
  ss_stack_impl :: 'si
  ss_on_stack_impl :: 'nsi
  ss_visited_impl :: 'nsi

definition [to_relAPP]: "ss_impl_rel s_rel vis_rel erel ≡ 
  {(⦇ss_stack_impl = si, ss_on_stack_impl = osi, ss_visited_impl = visi, … = mi⦈,
    ⦇ss_stack = s, on_stack = os, visited = vis, … = m⦈) |
    si osi visi mi s os vis m.
    (si, s) ∈ s_rel ∧
    (osi, os) ∈ vis_rel ∧
    (visi, vis) ∈ vis_rel ∧
    (mi, m) ∈ erel
  }"

consts 
  i_simple_state :: "interface ⇒ interface ⇒ interface ⇒ interface"

lemmas [autoref_rel_intf] = REL_INTFI[of ss_impl_rel i_simple_state]

term simple_state_ext

lemma [autoref_rules, param]:
  fixes s_rel ps_rel vis_rel erel
  defines "R ≡ ⟨s_rel,vis_rel,erel⟩ss_impl_rel"
  shows
  "(ss_stack_impl, ss_stack) ∈  R → s_rel"
  "(ss_on_stack_impl, on_stack) ∈  R → vis_rel"
  "(ss_visited_impl, visited) ∈ R → vis_rel"
  "(simple_state_impl.more, simple_state.more) ∈ R → erel"
  "(ss_stack_impl_update, ss_stack_update) ∈ (s_rel → s_rel) → R → R"
  "(ss_on_stack_impl_update, on_stack_update) ∈ (vis_rel → vis_rel) → R → R"
  "(ss_visited_impl_update, visited_update) ∈ (vis_rel → vis_rel) → R → R"
  "(simple_state_impl.more_update, simple_state.more_update) ∈ (erel → erel) → R → R"
  "(simple_state_impl_ext, simple_state_ext) ∈ s_rel → vis_rel → vis_rel → erel → R"
  unfolding ss_impl_rel_def R_def
  apply auto
  apply parametricity+
  done

subsection ‹ Simple state without on-stack ›
text ‹ We can further refine the simple implementation and drop the on-stack set ›
record ('si,'nsi)simple_state_nos_impl =
  ssnos_stack_impl :: 'si
  ssnos_visited_impl :: 'nsi

definition [to_relAPP]: "ssnos_impl_rel s_rel vis_rel erel ≡ 
  {(⦇ssnos_stack_impl = si, ssnos_visited_impl = visi, … = mi⦈,
    ⦇ss_stack = s, on_stack = os, visited = vis, … = m⦈) |
    si visi mi s os vis m.
    (si, s) ∈ s_rel ∧
    (visi, vis) ∈ vis_rel ∧
    (mi, m) ∈ erel
  }"

lemmas [autoref_rel_intf] = REL_INTFI[of ssnos_impl_rel i_simple_state]

definition op_nos_on_stack_update 
  :: "(_ set ⇒ _ set) ⇒ (_,_)simple_state_scheme ⇒ _"
  where "op_nos_on_stack_update ≡ on_stack_update"

context begin interpretation autoref_syn .
lemma [autoref_op_pat_def]: "op_nos_on_stack_update f s 
  ≡ OP (op_nos_on_stack_update f)$s" by simp

end

lemmas ssnos_unfolds ― ‹To be unfolded before autoref when using @{term ssnos_impl_rel}›
  = op_nos_on_stack_update_def[symmetric]

lemma [autoref_rules, param]:
  fixes s_rel vis_rel erel
  defines "R ≡ ⟨s_rel,vis_rel,erel⟩ssnos_impl_rel"
  shows
  "(ssnos_stack_impl, ss_stack) ∈  R → s_rel"
  "(ssnos_visited_impl, visited) ∈ R → vis_rel"
  "(simple_state_nos_impl.more, simple_state.more) ∈ R → erel"
  "(ssnos_stack_impl_update, ss_stack_update) ∈ (s_rel → s_rel) → R → R"
  "(λx. x, op_nos_on_stack_update f) ∈ R → R"
  "(ssnos_visited_impl_update, visited_update) ∈ (vis_rel → vis_rel) → R → R"
  "(simple_state_nos_impl.more_update, simple_state.more_update) ∈ (erel → erel) → R → R"
  "(λns _ ps vs. simple_state_nos_impl_ext ns ps vs, simple_state_ext) 
    ∈ s_rel → ANY_rel → vis_rel → erel → R"
  unfolding ssnos_impl_rel_def R_def op_nos_on_stack_update_def
  apply auto
  apply parametricity+
  done

subsection ‹Simple state without stack and on-stack›
text ‹Even further refinement yields an implementation without a stack.
  Note that this only works for structural implementations that provide their own
  stack (e.g., recursive)!›
record ('si,'nsi)simple_state_ns_impl =
  ssns_visited_impl :: 'nsi

definition [to_relAPP]: "ssns_impl_rel (R::('a×'b) set) vis_rel erel ≡ 
  {(⦇ssns_visited_impl = visi, … = mi⦈,
    ⦇ss_stack = s, on_stack = os, visited = vis, … = m⦈) |
    visi mi s os vis m.
    (visi, vis) ∈ vis_rel ∧
    (mi, m) ∈ erel
  }"

lemmas [autoref_rel_intf] = REL_INTFI[of ssns_impl_rel i_simple_state]

definition op_ns_on_stack_update 
  :: "(_ set ⇒ _ set) ⇒ (_,_)simple_state_scheme ⇒ _"
  where "op_ns_on_stack_update ≡ on_stack_update"

definition op_ns_stack_update 
  :: "(_ list ⇒ _ list) ⇒ (_,_)simple_state_scheme ⇒ _"
  where "op_ns_stack_update ≡ ss_stack_update"

context begin interpretation autoref_syn .
lemma [autoref_op_pat_def]: "op_ns_on_stack_update f s 
  ≡ OP (op_ns_on_stack_update f)$s" by simp

lemma [autoref_op_pat_def]: "op_ns_stack_update f s 
  ≡ OP (op_ns_stack_update f)$s" by simp

end


context simple_impl_defs begin
  thm choose_pending_def[unfolded op_ns_stack_update_def[symmetric], no_vars]

  lemma choose_pending_ns_unfold: "choose_pending u vo s = (
    case vo of None ⇒ RETURN s
    | Some v ⇒ do {
          _ ← ASSERT (ss_stack s ≠ []);
          RETURN
           (op_ns_stack_update 
             ( let 
                 (u, Vs) = hd (ss_stack s) 
               in (λ_. (u, Vs - {v}) # tl (ss_stack s))
             )
             s
           )
        })"
    unfolding choose_pending_def op_ns_stack_update_def
    by (auto split: option.split prod.split)

  lemmas ssns_unfolds ― ‹To be unfolded before autoref when using @{term ssns_impl_rel}.
    Attention: This lemma conflicts with the standard unfolding lemma in 
    @{text DFS_code_unfold}, so has to be placed first in an unfold-statement!›
  = op_ns_on_stack_update_def[symmetric] op_ns_stack_update_def[symmetric]
    choose_pending_ns_unfold

end

lemma [autoref_rules, param]:
  fixes s_rel vis_rel erel ANY_rel
  defines "R ≡ ⟨ANY_rel,vis_rel,erel⟩ssns_impl_rel"
  shows
  "(ssns_visited_impl, visited) ∈ R → vis_rel"
  "(simple_state_ns_impl.more, simple_state.more) ∈ R → erel"
  "⋀f. (λx. x, op_ns_stack_update f) ∈ R → R"
  "⋀f. (λx. x, op_ns_on_stack_update f) ∈ R → R"
  "(ssns_visited_impl_update, visited_update) ∈ (vis_rel → vis_rel) → R → R"
  "(simple_state_ns_impl.more_update, simple_state.more_update) ∈ (erel → erel) → R → R"
  "(λ_ _ ps vs. simple_state_ns_impl_ext ps vs, simple_state_ext) 
    ∈ ANY1_rel → ANY2_rel → vis_rel → erel → R"
  unfolding ssns_impl_rel_def R_def op_ns_on_stack_update_def op_ns_stack_update_def
  apply auto
  apply parametricity+
  done


lemma [refine_transfer_post_simp]:
  "⋀a m. a⦇simple_state_nos_impl.more := m::unit⦈ = a"
  "⋀a m. a⦇simple_state_impl.more := m::unit⦈ = a"
  "⋀a m. a⦇simple_state_ns_impl.more := m::unit⦈ = a"
  by auto


end