Theory Exploration_DFS

(*  Title:       Isabelle Collections Library
    Author:      Peter Lammich <peter dot lammich at uni-muenster.de>
    Maintainer:  Peter Lammich <peter dot lammich at uni-muenster.de>
*)
header {* \isaheader{DFS Implementation by Hashset} *}
theory Exploration_DFS
imports "../Collections" Exploration 
begin
text_raw {*\label{thy:Exploration_Example}*}

text {*
  This theory implements the DFS-algorithm by using a hashset to remember the
  explored states. It illustrates how to use data refinement with the Isabelle Collections 
  Framework in a realistic, non-trivial application.
*}

subsection "Definitions"
-- {*
  The concrete algorithm uses a hashset (@{typ [source] "'q hs"}) and a worklist. 
*}
type_synonym 'q hs_dfs_state = "'q hs × 'q list"

-- {* The loop terminates on empty worklist *}
definition hs_dfs_cond :: "'q hs_dfs_state => bool" 
  where "hs_dfs_cond S == let (Q,W) = S in W≠[]"

-- {* Refinement of a DFS-step, using hashset operations *}
definition hs_dfs_step 
  :: "('q::hashable => 'q ls) => 'q hs_dfs_state => 'q hs_dfs_state"
  where "hs_dfs_step post S == let 
    (Q,W) = S; 
    σ=hd W 
  in
    ls_iteratei (post σ) (λ_. True) (λx (Q,W). 
      if hs_memb x Q then 
        (Q,W) 
      else (hs_ins x Q,x#W)
      ) 
      (Q, tl W)
  "

-- {* Convert post-function to relation *}
definition hs_R :: "('q => 'q ls) => ('q×'q) set"
  where "hs_R post == {(q,q'). q'∈ls_α (post q)}"

-- {* Initial state: Set of initial states in discovered set and on worklist *}
definition hs_dfs_initial :: "'q::hashable hs => 'q hs_dfs_state"
  where "hs_dfs_initial Σi == (Σi,hs_to_list Σi)"

-- {* Abstraction mapping to abstract-DFS state *}
definition hs_dfs_α :: "'q::hashable hs_dfs_state => 'q dfs_state"
  where "hs_dfs_α S == let (Q,W)=S in (hs_α Q,W)"

(*-- {* Additional invariant on concrete level: The hashset invariant must hold *}
definition hs_dfs_invar_add :: "'q::hashable hs_dfs_state set" 
  where "hs_dfs_invar_add == { (Q,W). hs_invar Q }"*)

-- {* Combined concrete and abstract level invariant *}
definition hs_dfs_invar 
  :: "'q::hashable hs => ('q => 'q ls) => 'q hs_dfs_state set"
  where "hs_dfs_invar Σi post ==
    (*hs_dfs_invar_add ∩*) { s. (hs_dfs_α s) ∈ dfs_invar (hs_α Σi) (hs_R post) }"

-- "The deterministic while-algorithm"
definition "hs_dfs_dwa Σi post == (|
  dwa_cond = hs_dfs_cond,
  dwa_step = hs_dfs_step post,
  dwa_initial = hs_dfs_initial Σi,
  dwa_invar = hs_dfs_invar Σi post
|)),"


-- "Executable DFS-search. Given a set of initial states, and a successor 
      function, this function performs a DFS search to return the set of 
      reachable states."
definition "hs_dfs Σi post 
  == fst (while hs_dfs_cond (hs_dfs_step post) (hs_dfs_initial Σi))"


subsection "Refinement"

text {* We first show that a concrete step implements its abstract specification, and preserves the
  additional concrete invariant *}
lemma hs_dfs_step_correct:
  (*assumes [simp]: "hs_invar Q"
                  "!!s. ls_invar (post s)"*)
  assumes ne: "hs_dfs_cond (Q,W)"
  shows "(hs_dfs_α (Q,W),hs_dfs_α (hs_dfs_step post (Q,W)))
         ∈dfs_step (hs_R post)" (is ?T1)
        (*"(hs_dfs_step post (Q,W)) ∈ hs_dfs_invar_add" (is ?T2)*)
proof -

  from ne obtain σ Wtl where 
    [simp]: "W=σ#Wtl" 
    by (cases W) (auto simp add: hs_dfs_cond_def)

  have G: "let (Q',W') = hs_dfs_step post (Q,W) in
    hs_invar Q' ∧ (∃Wn. 
      distinct Wn 
      ∧ set Wn = ls_α (post σ) - hs_α Q 
      ∧ W'=Wn@Wtl 
      ∧ hs_α Q'=ls_α (post σ) ∪ hs_α Q)"
    apply (simp add: hs_dfs_step_def)
    apply (rule_tac 
      I="λit (Q',W'). hs_invar Q' ∧ (∃Wn. 
           distinct Wn 
           ∧ set Wn = (ls_α (post σ) - it) - hs_α Q 
           ∧ W'=Wn@Wtl 
           ∧ hs_α Q'=(ls_α (post σ) - it) ∪ hs_α Q)" 
      in ls.iterate_rule_P)
    apply simp
    apply simp
    apply (force split: split_if_asm simp add: hs_correct)
    apply force
    done
  from G show ?T1
    apply (cases "hs_dfs_step post (Q, W)")
    apply (auto simp add: hs_R_def hs_dfs_α_def intro!: dfs_step.intros)
    done
  (*from G show ?T2
    apply (cases "hs_dfs_step post (Q, W)")
    apply (auto simp add: hs_dfs_invar_add_def)
    done*)
qed

-- "Prove refinement"
theorem hs_dfs_pref_dfs: 
  (*assumes [simp]: "hs_invar Σi"
  assumes [simp]: "!!q. ls_invar (post q)"*)
  shows "wa_precise_refine 
    (det_wa_wa (hs_dfs_dwa Σi post)) 
    (dfs_algo (hs_α Σi) (hs_R post)) 
    hs_dfs_α"
  apply (unfold_locales)
  apply (auto simp add: det_wa_wa_def hs_dfs_dwa_def hs_dfs_α_def 
                        hs_dfs_cond_def dfs_algo_def dfs_cond_def) [1]
  apply (auto simp add: det_wa_wa_def hs_dfs_dwa_def dfs_algo_def 
                        hs_dfs_invar_def (*hs_dfs_invar_add_def *)
              intro!: hs_dfs_step_correct(1)) [1]
  apply (auto simp add: det_wa_wa_def hs_dfs_dwa_def hs_dfs_α_def 
                        hs_dfs_cond_def dfs_algo_def dfs_cond_def
                        hs_dfs_invar_def hs_dfs_step_def hs_dfs_initial_def 
                        hs.to_list_correct 
              intro: dfs_initial.intros
  ) [3]
  done

    -- "Show that concrete algorithm is a while-algo"
theorem hs_dfs_while_algo: 
  (*assumes INV [simp]: "hs_invar Σi"
                      "!!q. ls_invar (post q)"*)
  assumes finite[simp]: "finite ((hs_R post)⇧* `` hs_α Σi)"
  shows "while_algo (det_wa_wa (hs_dfs_dwa Σi post))"
proof -
  interpret ref: wa_precise_refine 
    "(det_wa_wa (hs_dfs_dwa Σi post))" 
    "(dfs_algo (hs_α Σi) (hs_R post))" 
    "hs_dfs_α" 
    using hs_dfs_pref_dfs .
  show ?thesis
    apply (rule ref.wa_intro[where addi=UNIV])
    apply (simp add: dfs_while_algo)
    apply (simp add: det_wa_wa_def hs_dfs_dwa_def hs_dfs_invar_def dfs_algo_def)

    apply (auto simp add: det_wa_wa_def hs_dfs_dwa_def) [1]
    apply simp
    (*
    apply (rule hs_dfs_step_correct(2))
    apply (auto simp add: hs_dfs_invar_add_def) [3]
    
    apply (simp add: det_wa_wa_def hs_dfs_dwa_def hs_dfs_initial_def 
                     hs_dfs_invar_add_def)
    *)
    done
qed
    
-- "Show that concrete algo is a deterministic while-algo"
theorems hs_dfs_det_while_algo = det_while_algo_intro[OF hs_dfs_while_algo]

  -- "Transferred correctness theorem"
theorems hs_dfs_invar_final = 
  wa_precise_refine.transfer_correctness[OF
     hs_dfs_pref_dfs dfs_invar_final]

  -- "The executable implementation is correct"
theorem hs_dfs_correct:
  (*assumes INV [simp]: "hs_invar Σi"
                      "!!q. ls_invar (post q)"*)
  assumes finite[simp]: "finite ((hs_R post)⇧* `` hs_α Σi)"
  shows "hs_α (hs_dfs Σi post) = (hs_R post)⇧*``hs_α Σi" (is ?T1)
        (*"hs_invar (hs_dfs Σi post)" (is ?T2)*)
proof -
  from hs_dfs_det_while_algo[OF finite] interpret 
    dwa: det_while_algo "(hs_dfs_dwa Σi post)" .

  have 
    LC: "(while hs_dfs_cond (hs_dfs_step post) (hs_dfs_initial Σi)) = dwa.loop"
    by (unfold dwa.loop_def) (simp add: hs_dfs_dwa_def)

  have "?T1 (*∧ ?T2*)"
    apply (unfold hs_dfs_def)
    apply (simp only: LC)
    apply (rule dwa.while_proof)
    apply (case_tac s)
    using hs_dfs_invar_final[of Σi "post"] (*[of id, simplified]*)
    apply (auto simp add: det_wa_wa_def hs_dfs_dwa_def 
                          dfs_α_def hs_dfs_α_def) [1]

    (*apply (rule conjI)
    using hs_dfs_invar_final[OF INV, of id, simplified]
    apply (auto simp add: det_wa_wa_def hs_dfs_dwa_def 
                          dfs_α_def hs_dfs_α_def) [1]
    apply (simp add: hs_dfs_invar_def hs_dfs_invar_add_def hs_dfs_dwa_def)
      *)
    done
  thus ?T1 (*?T2*) by auto
qed

subsection "Code Generation"
export_code hs_dfs in SML module_name DFS file -
export_code hs_dfs in OCaml module_name DFS file -
export_code hs_dfs in Haskell module_name DFS file -

end