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')erelsimple_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)  Rsimple_state_rel  Rsimple_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  (uvisited s)"
  definition "is_finished_impl u s  (uvisited s - (on_stack s))"

  definition "finish_impl u s  do {
    ASSERT (ss_stack s  []  uon_stack s);
    let s = sss_stack := tl (ss_stack s);
    let s = son_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. vVs);
        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 (von_stack s  vvisited s);
    let s = sss_stack := (v,E``{v}) # ss_stack s;
    let s = son_stack := insert v (on_stack s);
    let s = svisited := insert v (visited s);
    RETURN s
    }"
  
  definition "new_root_impl v0 s  do {
    ASSERT (v0visited s);
    let s = sss_stack := [(v0,E``{v0})];
    let s = son_stack := {v0};
    let s = svisited := 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 = "ESsimple_state_rel"
begin

  lemma init_impl: "(ei, e)  ES 
    c.init_impl ei (ESsimple_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)  ESsimple_state_rel
       c.new_root_impl v0 si (ESsimple_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)  ESsimple_state_rel
       c.get_pending_impl si 
            (Id ×r Id ×r ESsimple_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 = s0pending := 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)  ESsimple_state_rel
      c.finish_impl v si (ESsimple_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)  ESsimple_state_rel
       (si, a.cross_edge u v s)  ESsimple_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)  ESsimple_state_rel
       (si, a.back_edge u v s)  ESsimple_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)  ESsimple_state_rel
      c.discover_impl ui vi si (ESsimple_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 = "ESsimple_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  (ESsimple_state_rel) a.it_dfs"
    using gen_dfs_refine
    by simp

  lemma simple_refineT[refine]: "c.gen_dfsT  (ESsimple_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  (ESsimple_state_rel) a.it_dfs"
  proof -
    note tailrec_impl also note simple_refine finally show ?thesis .
  qed

  lemma simple_tailrecT_refine[refine]: "tailrec_implT  (ESsimple_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  (ESsimple_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,erelss_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,erelssnos_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,erelssns_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. asimple_state_nos_impl.more := m::unit = a"
  "a m. asimple_state_impl.more := m::unit = a"
  "a m. asimple_state_ns_impl.more := m::unit = a"
  by auto


end