Theory Gabow_SCC.Find_Path_Impl

section ‹Implementation of Safety Property Model Checker \label{sec:find_path_impl}›
theory Find_Path_Impl
imports 
  Find_Path
  CAVA_Automata.Digraph_Impl
begin

  section ‹Workset Algorithm›
  text ‹A simple implementation is by a workset algorithm.›
  definition "ws_update E u p V ws  RETURN (
             V  E``{u}, 
             ws ++ (λv. if (u,v)E  vV then Some (u#p) else None))"

  definition "s_init U0  RETURN (None,U0,λu. if uU0 then Some [] else None)"

  definition "wset_find_path E U0 P  do {
    ASSERT (finite U0);
    s0  s_init U0;
    (res,_,_)  WHILET 
      (λ(res,V,ws). res=None  wsMap.empty)
      (λ(res,V,ws). do {
        ASSERT (wsMap.empty);
        (u,p)  SPEC (λ(u,p). ws u = Some p);
        let ws=ws |` (-{u});
        
        if P u then
          RETURN (Some (rev p,u),V,ws)
        else do {
          ASSERT (finite (E``{u}));
          ASSERT (dom ws  V);
          (V,ws)  ws_update E u p V ws;
          RETURN (None,V,ws)
        }
      }) s0;
      RETURN res
    }"

  lemma wset_find_path_correct:
    fixes E :: "('v×'v) set"
    shows "wset_find_path E U0 P  find_path E U0 P"
  proof -

    define inv where "inv = (λ(res,V,ws). case res of
        None  
          dom wsV 
         finite (dom ws)  ― ‹Derived›
         VE*``U0 
         E``(V-dom ws)  V 
         (vV-dom ws. ¬ P v)
         U0  V
         (v p. ws v = Some p 
           ((vset p. ¬P v)  (u0U0. path E u0 (rev p) v)))
      | Some (p,v)  (u0U0. path E u0 p v  P v  (vset p. ¬P v)))"

    define var where "var = inv_image 
        (brk_rel (finite_psupset (E*``U0) <*lex*> measure (card o dom)))
        (λ(res::('v list × 'v) option,V::'v set,ws::'v'v list). 
            (resNone,V,ws))"

    (*have [simp, intro!]: "wf var"
      unfolding var_def
      by (auto intro: FIN)*)

    have [simp]: "u p V. dom (λv. if (u, v)  E  v  V then Some (u # p)
                     else None) = E``{u} - V"
      by (auto split: if_split_asm)


    {
      fix V ws u p
      assume INV: "inv (None,V,ws)"
      assume WSU: "ws u = Some p"

      from INV WSU have 
        [simp]: "V  E*``U0"
        and [simp]: "u  V"
        and UREACH: "u0U0. (u0,u)E*"
        and [simp]: "finite (dom ws)"
        unfolding inv_def
        apply simp_all
        apply auto []
        apply clarsimp
        apply blast
        done
      have "(V  E `` {u}, V)  finite_psupset (E* `` U0) 
          V  E `` {u} = V 
          card (E `` {u} - V  (dom ws - {u})) < card (dom ws)"
      proof (subst disj_commute, intro disjCI conjI)
        assume "(V  E `` {u}, V)  finite_psupset (E* `` U0)"
        thus "V  E `` {u} = V" using UREACH 
          by (auto simp: finite_psupset_def intro: rev_ImageI)

        hence [simp]: "E``{u} - V = {}" by force
        show "card (E `` {u} - V  (dom ws - {u})) < card (dom ws)"
          using WSU
          by (auto intro: card_Diff1_less)
      qed
    } note wf_aux=this

    {
      fix V ws u p
      assume FIN: "finite (E*``U0)"
      assume "inv (None,V,ws)" "ws u = Some p"
      then obtain u0 where "u0U0" "(u0,u)E*" unfolding inv_def 
        by clarsimp blast
      hence "E``{u}  E*``U0" by (auto intro: rev_ImageI)
      hence "finite (E``{u})" using FIN(1) by (rule finite_subset)
    } note succs_finite=this

    {
      fix V ws u p
      assume FIN: "finite (E*``U0)"
      assume INV: "inv (None,V,ws)"
      assume WSU: "ws u = Some p"
      assume NVD: "¬ P u"

      have "inv (None, V  E `` {u},
               ws |` (- {u}) ++
               (λv. if (u, v)  E  v  V then Some (u # p)
                    else None))" 
        unfolding inv_def
        
        apply (simp, intro conjI)
        using INV WSU apply (auto simp: inv_def) []
        using INV WSU apply (auto simp: inv_def) []
        using INV WSU apply (auto simp: succs_finite FIN) []
        using INV apply (auto simp: inv_def) []
        using INV apply (auto simp: inv_def) []

        using INV WSU apply (auto 
          simp: inv_def 
          intro: rtrancl_image_advance
        ) []

        using INV WSU apply (auto simp: inv_def) []

        using INV NVD apply (auto simp: inv_def) []
        using INV NVD apply (auto simp: inv_def) []

        using INV WSU NVD apply (fastforce
          simp: inv_def restrict_map_def 
          intro!: path_conc path1
          split: if_split_asm
        ) []
        done
    } note ip_aux=this

    show ?thesis
      unfolding wset_find_path_def find_path_def ws_update_def s_init_def

      apply (refine_rcg refine_vcg le_ASSERTI
        WHILET_rule[where 
          R = var and I = inv]
      )
      
      using [[goals_limit = 1]]

      apply (auto simp: var_def) []

      apply (auto 
        simp: inv_def dom_def
        split: if_split_asm) []
      apply simp
      apply (auto simp: inv_def) []
      apply (auto simp: var_def brk_rel_def) []

      apply (simp add: succs_finite)

      apply (auto simp: inv_def) []

      apply clarsimp
      apply (simp add: ip_aux)

      apply clarsimp
      apply (simp add: var_def brk_rel_def wf_aux) []

      apply (fastforce
        simp: inv_def 
        split: option.splits 
        intro: rev_ImageI
        dest: Image_closed_trancl) []
      done
  qed

  text ‹We refine the algorithm to use a foreach-loop›
  definition "ws_update_foreach E u p V ws  
    FOREACH (LIST_SET_REV_TAG (E``{u})) (λv (V,ws). 
      if vV then 
        RETURN (V,ws) 
      else do {
        ASSERT (vdom ws);
        RETURN (insert v V,ws( v  u#p))
      }
    ) (V,ws)"

  lemma ws_update_foreach_refine[refine]:
    assumes FIN: "finite (E``{u})"
    assumes WSS: "dom ws  V"
    assumes ID: "(E',E)Id" "(u',u)Id" "(p',p)Id" "(V',V)Id" "(ws',ws)Id"
    shows "ws_update_foreach E' u' p' V' ws'  Id (ws_update E u p V ws)"
    unfolding ID[simplified]
    unfolding ws_update_foreach_def ws_update_def LIST_SET_REV_TAG_def
    apply (refine_rcg refine_vcg FIN
      FOREACH_rule[where I="λit (V',ws'). 
        V'=V  (E``{u}-it)
       dom ws'  V'
       ws' = ws ++ (λv. if (u,v)E  vit  vV then Some (u#p) else None)"]
    )
    using WSS
    apply (auto 
      simp: Map.map_add_def
      split: option.splits if_split_asm
      intro!: ext[where 'a='a and 'b="'b list option"])

    done

  definition "s_init_foreach U0  do {
      (U0,ws)  FOREACH U0 (λx (U0,ws). 
        RETURN (insert x U0,ws(x[]))) ({},Map.empty);
      RETURN (None,U0,ws)
    }"

  lemma s_init_foreach_refine[refine]:
    assumes FIN: "finite U0"
    assumes ID: "(U0',U0)Id"
    shows "s_init_foreach U0' Id (s_init U0)"
    unfolding s_init_foreach_def s_init_def ID[simplified]
    
    apply (refine_rcg refine_vcg
      FOREACH_rule[where 
        I = "λit (U,ws). 
          U = U0-it 
         ws = (λx. if xU0-it then Some [] else None)"]
    )

    apply (auto
      simp: FIN
      intro!: ext
    )
    done

  definition "wset_find_path' E U0 P  do {
    ASSERT (finite U0);
    s0s_init_foreach U0;
    (res,_,_)  WHILET 
      (λ(res,V,ws). res=None  wsMap.empty)
      (λ(res,V,ws). do {
        ASSERT (wsMap.empty);
        ((u,p),ws)  op_map_pick_remove ws;
        
        if P u then
          RETURN (Some (rev p,u),V,ws)
        else do {
          (V,ws)  ws_update_foreach E u p V ws;
          RETURN (None,V,ws)
        }
      })
      s0;
      RETURN res
    }"

  lemma wset_find_path'_refine: 
    "wset_find_path' E U0 P  Id (wset_find_path E U0 P)"
    unfolding wset_find_path'_def wset_find_path_def
    unfolding op_map_pick_remove_alt
    apply (refine_rcg IdI)
    apply assumption
    apply simp_all
    done

  section ‹Refinement to efficient data structures›
  schematic_goal wset_find_path'_refine_aux:
    fixes U0::"'a set" and P::"'a  bool" and E::"('a×'a) set"
      and Pimpl :: "'ai  bool"
      and node_rel :: "('ai × 'a) set"
      and node_eq_impl :: "'ai  'ai  bool"
      and node_hash_impl
      and node_def_hash_size
    
    assumes [autoref_rules]: 
      "(succi,E)node_relslg_rel"
      "(Pimpl,P)node_rel  bool_rel"
      "(node_eq_impl, (=))  node_rel  node_rel  bool_rel"
      "(U0',U0)node_rellist_set_rel"
    assumes [autoref_ga_rules]: 
      "is_bounded_hashcode node_rel node_eq_impl node_hash_impl"  
      "is_valid_def_hm_size TYPE('ai) node_def_hash_size"
    notes [autoref_tyrel] = 
      TYRELI[where 
        R="node_rel,node_rellist_rellist_map_rel"]
      TYRELI[where R="node_relmap2set_rel (ahm_rel node_hash_impl)"]

    (*notes [autoref_rules] = 
      IdI[of P, unfolded fun_rel_id_simp[symmetric]]*)

    shows "(?c::?'c,wset_find_path' E U0 P)  ?R"
    unfolding wset_find_path'_def ws_update_foreach_def s_init_foreach_def
    using [[autoref_trace_failed_id]]
    using [[autoref_trace_intf_unif]]
    using [[autoref_trace_pat]]
    apply (autoref (keep_goal))
    done

  concrete_definition wset_find_path_impl for node_eq_impl succi U0' Pimpl 
    uses wset_find_path'_refine_aux

  section ‹Autoref Setup›
  context begin interpretation autoref_syn .
    lemma [autoref_itype]: 
      "find_path ::i Iii_slg i Iii_set i (Iii_bool) 
        i Iii_list, Iii_prodii_optionii_nres" by simp

    lemma wset_find_path_autoref[autoref_rules]:
      fixes node_rel :: "('ai × 'a) set"
      assumes eq: "GEN_OP node_eq_impl (=) (node_relnode_relbool_rel)"
      assumes hash: "SIDE_GEN_ALGO (is_bounded_hashcode node_rel node_eq_impl node_hash_impl)"
      assumes hash_dsz: "SIDE_GEN_ALGO (is_valid_def_hm_size TYPE('ai) node_def_hash_size)"
      shows "(
        wset_find_path_impl node_hash_impl node_def_hash_size node_eq_impl, 
        find_path)
         node_relslg_rel  node_rellist_set_rel  (node_relbool_rel) 
           node_rellist_rel×rnode_reloption_relnres_rel"
    proof -
      note EQI = GEN_OP_D[OF eq]
      note HASHI = SIDE_GEN_ALGO_D[OF hash]
      note DSZI = SIDE_GEN_ALGO_D[OF hash_dsz]
    
    
      note wset_find_path_impl.refine[THEN nres_relD, OF _ _ EQI _ HASHI DSZI]
      also note wset_find_path'_refine
      also note wset_find_path_correct
      finally show ?thesis 
        by (fastforce intro!: nres_relI)
    qed
  end
    
  schematic_goal wset_find_path_transfer_aux: 
    "RETURN ?c  wset_find_path_impl hashi dszi eqi E U0 P"
    unfolding wset_find_path_impl_def
    by (refine_transfer (post))
  concrete_definition wset_find_path_code 
    for E ?U0.0 P uses wset_find_path_transfer_aux
  lemmas [refine_transfer] = wset_find_path_code.refine

  export_code wset_find_path_code checking SML

section ‹Nontrivial paths›

definition "find_path1_gen E u0 P  do {
  res  find_path E (E``{u0}) P;
  case res of None  RETURN None
    | Some (p,v)  RETURN (Some (u0#p,v))
  }"

lemma find_path1_gen_correct: "find_path1_gen E u0 P  find_path1 E u0 P"
  unfolding find_path1_gen_def find_path_def find_path1_def
  apply (refine_rcg refine_vcg le_ASSERTI)
  apply (auto 
    intro: path_prepend 
    dest: tranclD
    elim: finite_subset[rotated]
  )
  done

schematic_goal find_path1_impl_aux:
  fixes node_rel :: "('ai × 'a) set"
  assumes [autoref_rules]: "(node_eq_impl, (=))  node_rel  node_rel  bool_rel"
  assumes [autoref_ga_rules]: 
    "is_bounded_hashcode node_rel node_eq_impl node_hash_impl"  
    "is_valid_def_hm_size TYPE('ai) node_def_hash_size"

  shows "(?c,find_path1_gen::(_×_) set  _)  node_relslg_rel  node_rel  (node_rel  bool_rel)  node_rellist_rel ×r node_reloption_relnres_rel"
  unfolding find_path1_gen_def[abs_def]
  apply (autoref (trace,keep_goal))
  done

lemma [autoref_itype]: 
  "find_path1 ::i Iii_slg i I i (Iii_bool) 
    i Iii_list, Iii_prodii_optionii_nres" by simp

concrete_definition find_path1_impl uses find_path1_impl_aux

lemma find_path1_autoref[autoref_rules]: 
  fixes node_rel :: "('ai × 'a) set"
  assumes eq: "GEN_OP node_eq_impl (=) (node_relnode_relbool_rel)"
  assumes hash: "SIDE_GEN_ALGO (is_bounded_hashcode node_rel node_eq_impl node_hash_impl)"
  assumes hash_dsz: "SIDE_GEN_ALGO (is_valid_def_hm_size TYPE('ai) node_def_hash_size)"
  
  shows "(find_path1_impl node_eq_impl node_hash_impl node_def_hash_size,find_path1) 
     node_relslg_rel node_rel  (node_rel  bool_rel)  
      node_rellist_rel ×r node_relRelators.option_relnres_rel"
proof -

  note EQI = GEN_OP_D[OF eq]
  note HASHI = SIDE_GEN_ALGO_D[OF hash]
  note DSZI = SIDE_GEN_ALGO_D[OF hash_dsz]
  
  note R = find_path1_impl.refine[param_fo, THEN nres_relD, OF EQI HASHI DSZI]
  
  note R
  also note find_path1_gen_correct
  finally show ?thesis by (blast intro: nres_relI)
qed
  
schematic_goal find_path1_transfer_aux: 
  "RETURN ?c  find_path1_impl eqi hashi dszi E u P"
  unfolding find_path1_impl_def
  by refine_transfer
concrete_definition find_path1_code for E u P uses find_path1_transfer_aux
lemmas [refine_transfer] = find_path1_code.refine

end