Theory Collections_Examples.Exploration

(*  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{State Space Exploration}›
theory Exploration
imports Main Collections.Collections
begin
text_raw ‹\label{thy:Exploration}›
  
text ‹
  In this theory, a workset algorithm for state-space exploration is defined.
  It explores the set of states that are reachable by a given relation, 
   starting at a given set of initial states.

  The specification makes use of the data refinement framework for 
  while-algorithms (cf. Section~\ref{thy:DatRef}), and is thus suited for 
  being refined to an executable algorithm, using the Isabelle Collections Framework
  to provide the necessary data structures.
›

subsection "Generic Search Algorithm"

  ― ‹The algorithm contains a set of discovered states and a workset›
type_synonym 'Σ sse_state = "'Σ set × 'Σ set"

  ― ‹Loop body›
inductive_set 
  sse_step :: "('Σ×'Σ) set ⇒ ('Σ sse_state × 'Σ sse_state) set" 
  for R where
  "⟦ σ∈W;
     Σ' = Σ ∪ (R``{σ});
     W' = (W-{σ}) ∪ ((R``{σ}) - Σ)
   ⟧ ⟹ ((Σ,W),(Σ',W'))∈sse_step R"
  
  ― ‹Loop condition›
definition sse_cond :: "'Σ sse_state set" where
  "sse_cond = {(Σ,W). W≠{}}"

  ― ‹Initial state›
definition sse_initial :: "'Σ set ⇒ 'Σ sse_state" where
  "sse_initial Σi == (Σi,Σi)"


  ― ‹Invariants: 
  \begin{itemize}
    \item The workset contains only states that are already 
      discovered.
    \item All discovered states are target states
    \item If there is a target state that is not discovered yet,
          then there is an element in the workset from that this 
          target state is reachable without using discovered 
          states as intermediate states. This supports the intuition 
          of the workset as a frontier between the sets of discovered 
          and undiscovered states.

  \end{itemize}›
definition sse_invar :: "'Σ set ⇒ ('Σ×'Σ) set ⇒ 'Σ sse_state set" where
  "sse_invar Σi R = {(Σ,W). 
    W⊆Σ ∧
    (Σ ⊆ R⇧*``Σi) ∧ 
    (∀σ∈(R⇧*``Σi)-Σ. ∃σh∈W. (σh,σ)∈(R - (UNIV × Σ))⇧*)
  }"

definition "sse_algo Σi R == 
  ⦇ wa_cond=sse_cond, 
    wa_step=sse_step R, 
    wa_initial = {sse_initial Σi}, 
    wa_invar = sse_invar Σi R ⦈"

definition "sse_term_rel Σi R == 
  { (σ',σ). σ∈sse_invar Σi R ∧ (σ,σ')∈sse_step R }"

  ― ‹Termination: Either a new state is discovered, or the workset shrinks›
theorem sse_term:
  assumes finite[simp, intro!]: "finite (R⇧*``Σi)"
  shows "wf (sse_term_rel Σi R)"
proof -
  have "wf (({(Σ',Σ). Σ ⊂ Σ' ∧ Σ' ⊆ (R⇧*``Σi)}) <*lex*> finite_psubset)"
    by (auto intro: wf_bounded_supset)
  moreover have "sse_term_rel Σi R ⊆ …" (is "_ ⊆ ?R")
  proof
    fix S
    assume A: "S∈sse_term_rel Σi R"
    obtain Σ W Σ' W' σ where
      [simp]: "S=((Σ',W'),(Σ,W))" and
      S: "(Σ,W) ∈ sse_invar Σi R"
         "σ∈W"
         "Σ' = Σ ∪ R``{σ}"
         "W' = (W-{σ}) ∪ (R``{σ} - Σ)"
    proof -
      obtain Σ W Σ' W' where SF[simp]: "S=((Σ',W'),(Σ,W))" by (cases S) force
      from A have R: "(Σ,W) ∈ sse_invar Σi R" "((Σ,W),(Σ',W'))∈sse_step R" 
        by (auto simp add: sse_term_rel_def)
      from sse_step.cases[OF R(2)] obtain σ where S:
        "σ∈W"
        "Σ' = Σ ∪ R``{σ}"
        "W' = (W-{σ}) ∪ (R``{σ} - Σ)"
        by metis
      thus ?thesis 
        by (rule_tac that[OF SF R(1) S])
    qed

    from S(1) have 
      [simp, intro!]: "finite Σ" "finite W" and
      WSS: "W⊆Σ" and
      SSS: "Σ⊆R⇧*``Σi"
      by (auto simp add: sse_invar_def intro: finite_subset)

    show "S∈?R" proof (cases "R``{σ} ⊆ Σ")
      case True with S have "Σ'=Σ" "W' ⊂ W" by auto
      thus ?thesis by (simp)
    next
      case False
      with S have "Σ' ⊃ Σ" by auto
      moreover from S(2) WSS SSS have "σ∈R⇧*``Σi" by auto
      hence "R``{σ} ⊆ R⇧*``Σi" 
        by (auto intro: rtrancl_into_rtrancl)
      with S(3) SSS have "Σ' ⊆ R⇧*``Σi" by auto
      ultimately show ?thesis by force
    qed
  qed
  ultimately show ?thesis by (auto intro: wf_subset)
qed
        
lemma sse_invar_initial: "(sse_initial Σi) ∈ sse_invar Σi R"
  by (unfold sse_invar_def sse_initial_def)
     (auto elim: rtrancl_last_touch)

  ― ‹Correctness theorem: If the loop terminates, the discovered states are
       exactly the reachable states›
theorem sse_invar_final: 
  "∀S. S∈wa_invar (sse_algo Σi R) ∧ S∉wa_cond (sse_algo Σi R) 
    ⟶ fst S = R⇧*``Σi"
  by (intro allI, case_tac S)
     (auto simp add: sse_invar_def sse_cond_def sse_algo_def)

lemma sse_invar_step: "⟦S∈sse_invar Σi R; (S,S')∈sse_step R⟧ 
  ⟹ S'∈sse_invar Σi R"
  ― ‹Split the goal by the invariant:›
  apply (cases S, cases S')
  apply clarsimp
  apply (erule sse_step.cases)
  apply clarsimp
  apply (subst sse_invar_def)
  apply (simp add: Let_def split_conv)
  apply (intro conjI)
  ― ‹Solve the easy parts automatically›
  apply (auto simp add: sse_invar_def) [3]
  apply (force simp add: sse_invar_def 
               dest: rtrancl_into_rtrancl) [1]
  ― ‹Tackle the complex part (last part of the invariant) in Isar›
proof (intro ballI)
  fix σ W Σ σ'
  assume A: 
    "(Σ,W)∈sse_invar Σi R"
    "σ∈W"
    "σ'∈R⇧* `` Σi - (Σ ∪ R `` {σ})"
    ― ‹Using the invariant of the original state, we obtain
        a state in the original workset and a path not touching
        the originally discovered states›
  from A(3) have "σ' ∈ R⇧* `` Σi - Σ" by auto
  with A(1) obtain σh where IP: 
    "σh∈W" 
    "(σh,σ')∈(R - (UNIV × Σ))⇧*" 
  and SS:
    "W⊆Σ"
    "Σ⊆R⇧* `` Σi"
    by (unfold sse_invar_def) force

  ― ‹We now make a case distinction, whether the obtained path contains
      states from @{term "post σ"} or not:›
  from IP(2) show "∃σh∈W - {σ} ∪ (R `` {σ} - Σ). 
                     (σh, σ') ∈ (R - UNIV × (Σ ∪ R `` {σ}))⇧*"
  proof (cases rule: rtrancl_last_visit[where S="R `` {σ}"])
    case no_visit
    ― ‹In the case that the obtained path contains no states from 
          @{term "post σ"}, we can take it.›
    hence G1: "(σh,σ')∈(R- (UNIV × (Σ∪R `` {σ})))⇧*" 
      by (simp add: set_diff_diff_left Sigma_Un_distrib2)
    moreover have "σh ≠ σ" 
      ― ‹We may exclude the case that our obtained path started at 
            @{text σ}, as all successors of @{text σ} are 
            in @{term "R `` {σ}"}›
    proof
      assume [simp]: "σh=σ"
      from A SS have "σ≠σ'" by auto
      with G1 show False
        by (auto simp add: elim: converse_rtranclE)
    qed
    ultimately show ?thesis using IP(1) by auto
  next
    case (last_visit_point σt)
    ― ‹If the obtained path contains a state from @{text "R `` {σ}"}, 
          we simply pick the last one:›
    hence "(σt,σ')∈(R- (UNIV × (Σ∪R `` {σ})))⇧*" 
      by (simp add: set_diff_diff_left Sigma_Un_distrib2)
    moreover from last_visit_point(2) have "σt∉Σ" 
      by (auto elim: trancl.cases)
    ultimately show ?thesis using last_visit_point(1) by auto
  qed
qed

― ‹The sse-algorithm is a well-defined while-algorithm›
theorem sse_while_algo: "finite (R⇧*``Σi) ⟹ while_algo (sse_algo Σi R)"
  apply unfold_locales
  apply (auto simp add: sse_algo_def intro: sse_invar_step sse_invar_initial)
  apply (drule sse_term)
  apply (erule_tac wf_subset)
  apply (unfold sse_term_rel_def)
  apply auto
  done

subsection "Depth First Search"
text_raw ‹\label{sec:sse:dfs}›
text ‹
  In this section, the generic state space exploration algorithm is refined
  to a DFS-algorithm, that uses a stack to implement the workset.
›

type_synonym 'Σ dfs_state = "'Σ set × 'Σ list"

definition dfs_α :: "'Σ dfs_state ⇒ 'Σ sse_state" 
  where "dfs_α S == let (Σ,W)=S in (Σ,set W)"

definition dfs_invar_add :: "'Σ dfs_state set"
  where "dfs_invar_add == {(Σ,W). distinct W}"

definition "dfs_invar Σi R == dfs_invar_add ∩ { s. dfs_α s ∈ sse_invar Σi R }"

inductive_set dfs_initial :: "'Σ set ⇒ 'Σ dfs_state set" for Σi
  where "⟦ distinct W; set W = Σi⟧ ⟹ (Σi,W)∈dfs_initial Σi"

inductive_set dfs_step :: "('Σ×'Σ) set ⇒ ('Σ dfs_state ×'Σ dfs_state) set" 
  for R where
  "⟦ W=σ#Wtl;
     distinct Wn;
     set Wn = R``{σ} - Σ;
     W' = Wn@Wtl;
     Σ' = R``{σ} ∪ Σ
  ⟧ ⟹ ((Σ,W),(Σ',W'))∈dfs_step R"

definition dfs_cond :: "'Σ dfs_state set" 
  where "dfs_cond == { (Σ,W). W≠[]}"

definition "dfs_algo Σi R == ⦇ 
  wa_cond = dfs_cond, 
  wa_step = dfs_step R, 
  wa_initial = dfs_initial Σi, 
  wa_invar = dfs_invar Σi R ⦈"

  ― ‹The DFS-algorithm refines the state-space exploration algorithm›
theorem dfs_pref_sse: 
  "wa_precise_refine (dfs_algo Σi R) (sse_algo Σi R) dfs_α"
  apply (unfold_locales)
  apply (auto simp add: dfs_algo_def sse_algo_def dfs_cond_def sse_cond_def 
                        dfs_α_def)
  apply (erule dfs_step.cases)
  apply (rule_tac σ=σ in sse_step.intros)
  apply (auto simp add: dfs_invar_def sse_invar_def dfs_invar_add_def 
                        sse_initial_def dfs_α_def 
              elim: dfs_initial.cases)
  done

  ― ‹The DFS-algorithm is a well-defined while-algorithm›
theorem dfs_while_algo:
  assumes finite[simp, intro!]: "finite (R⇧*``Σi)"
  shows "while_algo (dfs_algo Σi R)"
proof -
  interpret wa_precise_refine "(dfs_algo Σi R)" "(sse_algo Σi R)" dfs_α 
    using dfs_pref_sse .

  have [simp]: "wa_invar (sse_algo Σi R) = sse_invar Σi R" 
    by (simp add: sse_algo_def)

  show ?thesis 
    apply (rule wa_intro)
    apply (simp add: sse_while_algo)

    apply (simp add: dfs_invar_def dfs_algo_def)
    
    apply (auto simp add: dfs_invar_add_def dfs_algo_def dfs_α_def 
                          dfs_cond_def sse_invar_def 
                elim!: dfs_step.cases) [1]

    apply (auto simp add: dfs_invar_add_def dfs_algo_def 
                elim: dfs_initial.cases) [1]
    done 
qed

  ― ‹The result of the DFS-algorithm is correct›
lemmas dfs_invar_final = 
  wa_precise_refine.transfer_correctness[OF dfs_pref_sse sse_invar_final]

end