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>
*)
section ‹\isaheader{DFS Implementation by Hashset}›
theory Exploration_DFS
imports 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 ==
    { 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: if_split_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 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
    done
qed
    
― ‹Show that concrete algo is a deterministic while-algo›
lemmas hs_dfs_det_while_algo = det_while_algo_intro[OF hs_dfs_while_algo]

  ― ‹Transferred correctness theorem›
lemmas 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 finite[simp]: "finite ((hs_R post)⇧* `` hs.α Σi)"
  shows "hs.α (hs_dfs Σi post) = (hs_R post)⇧*``hs.α Σi" (is ?T1)
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]
    done
  thus ?T1  by auto
qed

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

end