Quelle  DFS.thy

theory DFS
  imports Pair_Graph_Specs Set2_Addons Set_Addons  
begin

section‹Depth-Frist Search›

subsection ‹The program state›

datatype return = Reachable | NotReachable

record ('ver, 'vset) DFS_state = stack:: "'ver list" seen:: "'vset"  return:: return

subsection ‹Setup for automation›

named_theorems call_cond_elims
named_theorems call_cond_intros
named_theorems ret_holds_intros
named_theorems invar_props_intros
named_theorems invar_props_elims
named_theorems invar_holds_intros
named_theorems state_rel_intros
named_theorems state_rel_holds_intros 


subsection ‹A \emph{locale} for fixing data structures and their implemenations›

locale DFS =
  (*set_ops: Set2 where empty = empty and insert = insert and isin = vset_isin +*)
  Graph: Pair_Graph_Specs
    where lookup = lookup +
 set_ops: Set2 vset_empty vset_delete _ t_set vset_inv insert


for lookup :: "'adjmap==> 'v ==> 'vset option" +

fixes G::"'adjmap" and s::"'v" and t::"'v" (*
fixes T_diff::"'vset \<Rightarrow> 'vset \<Rightarrow> nat"
and T_sel::"'vset \<Rightarrow> nat" and T_insert::"'v \<Rightarrow> 'vset \<Rightarrow> nat"
and T_lookup::"'adjmap\<Rightarrow> 'v \<Rightarrow> nat" and T_G::nat and T_vset_empty::nat*)

begin

definition "DFS_axioms = ( Graph.graph_inv G ∧ Graph.finite_graph G ∧ Graph.finite_vsets
                         ∧ s ∈ dVs (Graph.digraph_abs G))"

abbreviation "neighb' v == Graph.neighb G v"

notation "neighb'" ("N_G _" 100)

subsection ‹Defining the Algorithm›

function (domintros) DFS::"('v, 'vset) DFS_state ==> ('v, 'vset) DFS_state" where
  "DFS dfs_state =
     (case (stack dfs_state) of (v # stack_tl) ==>
       (if v = t then
          (dfs_state (return := Reachable))
        else ((if (N_G v -_G (seen dfs_state)) ≠ ∅_V then
                  let u = (sel ((N_G v) -_G (seen dfs_state)));
                      stack' = u# (stack dfs_state);
                      seen' = insert u (seen dfs_state)
                  in
                    (DFS (dfs_state (stack := stack',
                                     seen := seen' )))
                else
                  let stack' = stack_tl in
                     DFS (dfs_state (stack := stack')))
              )
      )
     | _ ==> (dfs_state (return := NotReachable))
    )"
  by pat_completeness auto

subsection ‹Setup for Reasoning About the Algorithm›

definition initial_state::"('v,'vset) DFS_state" where
  "initial_state = (stack = [s], seen = insert s ∅_V, return = NotReachable)"

definition "DFS_call_1_conds dfs_state =
    (case stack dfs_state of (v # stack_tl) ==>
       (if v = t then
          False
        else ((if ((N_G v) -_G (seen dfs_state)) ≠ (∅_V) then
                  True
                 else False)
              )
      )
     | _ ==> False
    )"

lemma DFS_call_1_conds[call_cond_elims]: 
  "DFS_call_1_conds dfs_state ==>
   [[∃v stack_tl. stack dfs_state = v # stack_tl;
    hd (stack dfs_state) ≠ t;
    (N_G (hd (stack dfs_state))) -_G (seen dfs_state) ≠ (∅_V)] ==> P] ==>
   P"
  by(auto simp: DFS_call_1_conds_def split: list.splits option.splits if_splits)


definition "DFS_upd1 dfs_state = (
    let
      N = (N_G (hd (stack dfs_state)));
      u = (sel ((N -_G (seen dfs_state))));
      stack' = u # (stack dfs_state);
      seen' = insert u (seen dfs_state)
    in
      dfs_state (stack := stack', seen := seen'))" 

definition DFS_call_2_conds::"('v, 'vset) DFS_state ==> bool" where
"DFS_call_2_conds dfs_state =
(case stack dfs_state of (v # stack_tl) ==>
       (if v = t then
          False
        else (
                (if ((N_G v) -_G (seen dfs_state)) ≠ (∅_V) then
                  False
                 else True)
              )
      )
     | _ ==> False
    )"

lemma DFS_call_2_condsE[call_cond_elims]: 
  "DFS_call_2_conds dfs_state ==>
   [[∃v stack_tl. stack dfs_state = v # stack_tl;
    hd (stack dfs_state) ≠ t;
    (N_G (hd (stack dfs_state))) -_G (seen dfs_state) = (∅_V)] ==> P] ==>
   P"
  by(auto simp: DFS_call_2_conds_def split: list.splits option.splits if_splits)

definition "DFS_upd2 dfs_state =
  ((dfs_state (stack := tl (stack dfs_state))))"


definition "DFS_ret_1_conds dfs_state =
   (case stack dfs_state of (v # stack_tl) ==>
       (if v = t then
          False
        else (
                (if ((N_G v) -_G (seen dfs_state)) ≠ ∅_V then
                  False
                 else False)
              )
      )
     | _ ==> True
   )"

lemma DFS_ret_1_conds[call_cond_elims]:
  "DFS_ret_1_conds dfs_state ==>
   [[stack dfs_state = []] ==> P] ==>
   P"
  by(auto simp: DFS_ret_1_conds_def split: list.splits option.splits if_splits)

lemma DFS_call_4_condsI[call_cond_intros]:
  "[stack dfs_state = []] ==> DFS_ret_1_conds dfs_state"
  by(auto simp: DFS_ret_1_conds_def split: list.splits option.splits if_splits)

definition "DFS_ret1 dfs_state = (dfs_state (return := NotReachable))"

definition "DFS_ret_2_conds dfs_state =
   (case stack dfs_state of (v # stack_tl) ==>
       (if v = t then
          True
        else (
                (if (N_G v -_G (seen dfs_state)) ≠ ∅_V then
                  False
                 else False)
              )
      )
     | _ ==> False
   )"


lemma DFS_ret_2_conds[call_cond_elims]:
  "DFS_ret_2_conds dfs_state ==>
   [∧v stack_tl. [stack dfs_state = v # stack_tl;
    (hd (stack dfs_state)) = t] ==> P] ==>
   P"
  by(auto simp: DFS_ret_2_conds_def split: list.splits option.splits if_splits)

lemma DFS_ret_2_condsI[call_cond_intros]:
  "∧v stack_tl. [stack dfs_state = v # stack_tl; (hd (stack dfs_state)) = t] ==> DFS_ret_2_conds dfs_state"
  by(auto simp: DFS_ret_2_conds_def split: list.splits option.splits if_splits)

definition "DFS_ret2 dfs_state = (dfs_state (return := Reachable))"

lemma DFS_cases:
  assumes "DFS_call_1_conds dfs_state ==> P"
      "DFS_call_2_conds dfs_state ==> P"
      "DFS_ret_1_conds dfs_state ==> P"
      "DFS_ret_2_conds dfs_state ==> P"
  shows "P"
proof-
  have "DFS_call_1_conds dfs_state ∨ DFS_call_2_conds dfs_state ∨
        DFS_ret_1_conds dfs_state ∨ DFS_ret_2_conds dfs_state"
    by (auto simp add: DFS_call_1_conds_def DFS_call_2_conds_def
                        DFS_ret_1_conds_def DFS_ret_2_conds_def
           split: list.split_asm option.split_asm if_splits)
  then show ?thesis
    using assms
    by auto
qed

lemma DFS_simps:
  assumes "DFS_dom dfs_state" 
  shows"DFS_call_1_conds dfs_state ==> DFS dfs_state = DFS (DFS_upd1 dfs_state)"
      "DFS_call_2_conds dfs_state ==> DFS dfs_state = DFS (DFS_upd2 dfs_state)"
      "DFS_ret_1_conds dfs_state ==> DFS dfs_state = DFS_ret1 dfs_state"
      "DFS_ret_2_conds dfs_state ==> DFS dfs_state = DFS_ret2 dfs_state"
  by (auto simp add: DFS.psimps[OF assms] Let_def
                       DFS_call_1_conds_def DFS_upd1_def DFS_call_2_conds_def DFS_upd2_def
                       DFS_ret_1_conds_def DFS_ret1_def
                       DFS_ret_2_conds_def DFS_ret2_def
                       
            split: list.splits option.splits if_splits )

lemma DFS_induct: 
  assumes "DFS_dom dfs_state"
  assumes "∧dfs_state. [DFS_dom dfs_state;
                        DFS_call_1_conds dfs_state ==> P (DFS_upd1 dfs_state);
                        DFS_call_2_conds dfs_state ==> P (DFS_upd2 dfs_state)] ==> P dfs_state"
  shows "P dfs_state"
  apply(rule DFS.pinduct[OF assms(1)])
  apply(rule assms(2)[simplified DFS_call_1_conds_def DFS_upd1_def DFS_call_2_conds_def DFS_upd2_def])
  by (auto simp: Let_def split: list.splits option.splits if_splits)

lemma DFS_domintros: 
  assumes "DFS_call_1_conds dfs_state ==> DFS_dom (DFS_upd1 dfs_state)"
  assumes "DFS_call_2_conds dfs_state ==> DFS_dom (DFS_upd2 dfs_state)"
  shows "DFS_dom dfs_state"
proof(rule DFS.domintros, goal_cases)
  case (1 x21 x22)
  then show ?case
    using assms(1)[simplified DFS_call_1_conds_def DFS_upd1_def]
    by (force simp: Let_def split: list.splits option.splits if_splits)
next
  case (2 x21 x22)
  then show ?case
    using assms(2)[simplified DFS_call_2_conds_def DFS_upd2_def]
    by (force split: list.splits option.splits if_splits)
qed

subsection ‹Loop Invariants›

definition invar_well_formed::"('v,'vset) DFS_state ==> bool" where
  "invar_well_formed dfs_state = vset_inv (seen dfs_state)"

definition invar_stack_walk::"('v,'vset) DFS_state ==> bool" where 
  "invar_stack_walk dfs_state = (Vwalk.vwalk (Graph.digraph_abs G) (rev (stack dfs_state)))"

definition invar_seen_stack::"('v,'vset) DFS_state ==> bool" where 
  "invar_seen_stack dfs_state ⟷
    distinct (stack dfs_state)
    ∧ set (stack dfs_state) ⊆ t_set (seen dfs_state)
    ∧ t_set (seen dfs_state) ⊆ dVs (Graph.digraph_abs G)"

definition invar_s_in_stack::"('v,'vset) DFS_state ==> bool" where
  "invar_s_in_stack dfs_state ⟷
    (stack (dfs_state) ≠ [] ⟶ last (stack dfs_state) = s)"

definition invar_visited_through_seen::"('v,'vset) DFS_state ==> bool" where 
  "invar_visited_through_seen dfs_state =
    (∀v ∈ t_set (seen dfs_state).
       (∀p. Vwalk.vwalk_bet (Graph.digraph_abs G) v p t ∧ distinct p ⟶ (set p ∩ set (stack dfs_state) ≠ {})))"

definition call_1_measure::"('v,'vset) DFS_state ==> nat" where 
  "call_1_measure dfs_state = card (dVs (Graph.digraph_abs G) - t_set (seen dfs_state))"

definition call_2_measure::"('v,'vset) DFS_state ==> nat" where
  "call_2_measure dfs_state = card (set (stack dfs_state))"

definition DFS_term_rel::"(('v,'vset) DFS_state × ('v,'vset) DFS_state) set" where
  "DFS_term_rel = (call_1_measure) <*mlex*> (call_2_measure) <*mlex*> {}"

end

locale DFS_thms = DFS +

assumes DFS_axioms: DFS_axioms

begin

context
includes set_ops.automation and Graph.adjmap.automation and Graph.vset.set.automation 
begin

lemma graph_inv[simp,intro]:
          "Graph.graph_inv G"
          "Graph.finite_graph G"
          "Graph.finite_vsets"
  using DFS_axioms
  by (auto simp: DFS_axioms_def)

lemma s_in_G[simp,intro]: "s ∈ dVs (Graph.digraph_abs G)"
  using DFS_axioms
  by (auto simp: DFS_axioms_def)

lemma finite_neighbourhoods[simp]:                                                 
          "finite (t_set N)"
  using graph_inv(3)
  by fastforce

lemmas simps[simp] = Graph.neighbourhood_abs[OF graph_inv(1)] Graph.are_connected_abs[OF graph_inv(1)]

lemma invar_well_formed_props[invar_props_elims]:
  "invar_well_formed dfs_state ==>
     ([vset_inv (seen dfs_state)] ==> P) ==>
     P"
  by (auto simp: invar_well_formed_def)

lemma invar_well_formed_intro[invar_props_intros]: "[vset_inv (seen dfs_state)]
                     ==> invar_well_formed dfs_state"
  by (auto simp: invar_well_formed_def)

lemma invar_well_formed_holds_1[invar_holds_intros]:
  "[DFS_call_1_conds dfs_state; invar_well_formed dfs_state] ==>
      invar_well_formed (DFS_upd1 dfs_state)"
  by (auto simp: Let_def DFS_upd1_def elim!: invar_props_elims intro!: invar_props_intros)

lemma invar_well_formed_holds_2[invar_holds_intros]: "[DFS_call_2_conds dfs_state; invar_well_formed dfs_state] ==> invar_well_formed (DFS_upd2 dfs_state)"
  by (auto simp: DFS_upd2_def elim!: invar_props_elims intro: invar_props_intros)

lemma invar_well_formed_holds_4[invar_holds_intros]: "[DFS_ret_1_conds dfs_state; invar_well_formed dfs_state] ==> invar_well_formed (DFS_ret1 dfs_state)"
  by (auto elim!: invar_props_elims  intro: invar_props_intros simp: DFS_ret1_def)

lemma invar_well_formed_holds_5[invar_holds_intros]: "[DFS_ret_2_conds dfs_state; invar_well_formed dfs_state] ==> invar_well_formed (DFS_ret2 dfs_state)"
  by (auto elim!: invar_props_elims intro: invar_props_intros simp: DFS_ret2_def)

lemma invar_well_formed_holds[invar_holds_intros]: 
   assumes "DFS_dom dfs_state" "invar_well_formed dfs_state"
   shows "invar_well_formed (DFS dfs_state)"
  using assms(2)
proof(induction rule: DFS_induct[OF assms(1)])
  case IH: (1 dfs_state)
  show ?case
    apply(rule DFS_cases[where dfs_state = dfs_state])
    by (auto intro!: IH(2-4) invar_holds_intros  simp: DFS_simps[OF IH(1)])
qed

lemma invar_stack_walk_props[invar_props_elims]: 
  "invar_stack_walk dfs_state ==>
     ((Vwalk.vwalk (Graph.digraph_abs G) (rev (stack dfs_state))) ==> P) ==> P"
  by (auto simp: invar_stack_walk_def)

lemma invar_stack_walk_intro[invar_props_intros]: "Vwalk.vwalk (Graph.digraph_abs G) (rev (stack dfs_state)) ==> invar_stack_walk dfs_state"
  by (auto simp: invar_stack_walk_def)


lemma invar_stack_walk_holds_1[invar_holds_intros]:
  assumes "DFS_call_1_conds dfs_state" "invar_well_formed dfs_state" "invar_stack_walk dfs_state"
  shows "invar_stack_walk (DFS_upd1 dfs_state)"
    using assms graph_inv 
    by (force simp: Let_def DFS_upd1_def elim!: call_cond_elims elim!: invar_props_elims
                intro!: Vwalk.vwalk_append2 neighbourhoodI invar_props_intros)


lemma invar_stack_walk_holds_2[invar_holds_intros]: "[DFS_call_2_conds dfs_state; invar_stack_walk dfs_state] ==> invar_stack_walk (DFS_upd2 dfs_state)"
  by (auto simp: DFS_upd2_def dest!: append_vwalk_pref elim!: invar_props_elims intro!: invar_props_intros elim: call_cond_elims)

lemma invar_stack_walk_holds_4[invar_holds_intros]: "[DFS_ret_1_conds dfs_state; invar_stack_walk dfs_state] ==> invar_stack_walk (DFS_ret1 dfs_state)"
  by (auto elim!: invar_props_elims intro: invar_props_intros simp: DFS_ret1_def)

lemma invar_2_holds_5[invar_holds_intros]: "[DFS_ret_2_conds dfs_state; invar_stack_walk dfs_state] ==> invar_stack_walk (DFS_ret2 dfs_state)"
  by (auto elim!: invar_props_elims intro: invar_props_intros simp: DFS_ret2_def)

lemma invar_2_holds[invar_holds_intros]:
   assumes "DFS_dom dfs_state" "invar_well_formed dfs_state" "invar_stack_walk dfs_state"
   shows "invar_stack_walk (DFS dfs_state)"
  using assms(2-3)
proof(induction rule: DFS_induct[OF assms(1)])
  case IH: (1 dfs_state)
  show ?case
    apply(rule DFS_cases[where dfs_state = dfs_state])
    by (auto intro!: IH(2-5) invar_holds_intros simp: DFS_simps[OF IH(1)])
qed

lemma invar_seen_stack_props[invar_props_elims]:
   "invar_seen_stack dfs_state ==>
     ([distinct (stack dfs_state); set (stack dfs_state) ⊆ t_set (seen dfs_state);
       t_set (seen dfs_state) ⊆ dVs (Graph.digraph_abs G)] ==> P) ==> P "
  by (auto simp: invar_seen_stack_def)

lemma invar_seen_stack_intro[invar_props_intros]:
  "[distinct (stack dfs_state); set (stack dfs_state) ⊆ t_set (seen dfs_state); t_set (seen dfs_state) ⊆ dVs (Graph.digraph_abs G)] ==> invar_seen_stack dfs_state"
  by (auto simp: invar_seen_stack_def)

lemma invar_seen_stack_holds_1[invar_holds_intros]:
  "[DFS_call_1_conds dfs_state; invar_well_formed dfs_state; invar_seen_stack dfs_state] ==> invar_seen_stack (DFS_upd1 dfs_state)"
  by (force simp: Let_def DFS_upd1_def dest!: append_vwalk_pref elim!: call_cond_elims
            elim!: invar_props_elims intro!: invar_props_intros)

lemma invar_seen_stack_holds_2[invar_holds_intros]: 
  "[DFS_call_2_conds dfs_state; invar_well_formed dfs_state; invar_seen_stack dfs_state] ==>
     invar_seen_stack (DFS_upd2 dfs_state)"
  by (auto elim!: call_cond_elims simp: DFS_upd2_def elim: vwalk_betE
           elim!: invar_props_elims dest!: Graph.vset.emptyD append_vwalk_pref intro!: invar_props_intros)

lemma invar_seen_stack_holds_4[invar_holds_intros]:
   "[DFS_ret_1_conds dfs_state; invar_seen_stack dfs_state] ==>
       invar_seen_stack (DFS_ret1 dfs_state)"
  by (auto elim!: invar_props_elims intro!: invar_props_intros simp: DFS_ret1_def)

lemma invar_seen_stack_holds_5[invar_holds_intros]: "[DFS_ret_2_conds dfs_state; invar_seen_stack dfs_state] ==> invar_seen_stack (DFS_ret2 dfs_state)"
  by (auto elim!: invar_props_elims intro!: invar_props_intros simp: DFS_ret2_def)

lemma invar_seen_stack_holds[invar_holds_intros]:
   assumes "DFS_dom dfs_state" "invar_well_formed dfs_state" "invar_seen_stack dfs_state"
   shows "invar_seen_stack (DFS dfs_state)" 
   using assms(2-)
proof(induction rule: DFS_induct[OF assms(1)])
  case IH: (1 dfs_state)
  show ?case
    apply(rule DFS_cases[where dfs_state = dfs_state])
    by (auto intro!: IH(2-5) invar_holds_intros simp: DFS_simps[OF IH(1)])
qed


lemma invar_s_in_stack_props[invar_props_elims]:
   "invar_s_in_stack dfs_state ==>
     ([(stack (dfs_state) ≠ [] ==> last (stack dfs_state) = s)] ==> P) ==> P "
  by (auto simp: invar_s_in_stack_def)

lemma invar_s_in_stack_intro[invar_props_intros]:
  "[(stack (dfs_state) ≠ [] ==> last (stack dfs_state) = s)] ==> invar_s_in_stack dfs_state"
  by (auto simp: invar_s_in_stack_def)

lemma invar_s_in_stack_holds_1[invar_holds_intros]:
  "[DFS_call_1_conds dfs_state; invar_well_formed dfs_state; invar_s_in_stack dfs_state] ==> invar_s_in_stack (DFS_upd1 dfs_state)"
  by (force simp: Let_def DFS_upd1_def dest!: append_vwalk_pref elim!: call_cond_elims
            elim!: invar_props_elims intro!: invar_props_intros)

lemma invar_s_in_stack_holds_2[invar_holds_intros]: 
  "[DFS_call_2_conds dfs_state; invar_well_formed dfs_state; invar_s_in_stack dfs_state] ==>
     invar_s_in_stack (DFS_upd2 dfs_state)"
  by (auto elim!: call_cond_elims simp: DFS_upd2_def elim: vwalk_betE
           elim!: invar_props_elims dest!: Graph.vset.emptyD append_vwalk_pref intro!: invar_props_intros)

lemma invar_s_in_stack_holds_4[invar_holds_intros]:
   "[DFS_ret_1_conds dfs_state; invar_s_in_stack dfs_state] ==>
       invar_s_in_stack (DFS_ret1 dfs_state)"
  by (auto elim!: invar_props_elims intro!: invar_props_intros simp: DFS_ret1_def)

lemma invar_s_in_stack_holds_5[invar_holds_intros]: "[DFS_ret_2_conds dfs_state; invar_s_in_stack dfs_state] ==> invar_s_in_stack (DFS_ret2 dfs_state)"
  by (auto elim!: invar_props_elims intro!: invar_props_intros simp: DFS_ret2_def)

lemma invar_s_in_stack_holds[invar_holds_intros]: 
   assumes "DFS_dom dfs_state" "invar_well_formed dfs_state" "invar_s_in_stack dfs_state"
   shows "invar_s_in_stack (DFS dfs_state)" 
   using assms(2-)
proof(induction rule: DFS_induct[OF assms(1)])
  case IH: (1 dfs_state)
  show ?case
    apply(rule DFS_cases[where dfs_state = dfs_state])
    by (auto intro!: IH(2-5) invar_holds_intros simp: DFS_simps[OF IH(1)])
qed


lemma invar_visited_through_seen_props[elim!]:
   "invar_visited_through_seen dfs_state ==>
     ([∧v p. [v ∈ t_set (seen dfs_state);
              (Vwalk.vwalk_bet (Graph.digraph_abs G) v p t); distinct p ] ==>
              set p ∩ set (stack dfs_state) ≠ {}] ==> P) ==> P "
  by (auto simp: invar_visited_through_seen_def)


lemma invar_visited_through_seen_intro[invar_props_intros]:
  "[∧v p. [v ∈ t_set (seen dfs_state);
           (Vwalk.vwalk_bet (Graph.digraph_abs G) v p t); distinct p] ==>
           set p ∩ set (stack dfs_state) ≠ {}] ==> invar_visited_through_seen dfs_state"
  by (auto simp: invar_visited_through_seen_def)


subsection ‹Proofs that the Invariants Hold›

lemma invar_visited_through_seen_holds_1[invar_holds_intros]:
  "[DFS_call_1_conds dfs_state; invar_well_formed dfs_state; invar_seen_stack dfs_state;
    invar_visited_through_seen dfs_state]
    ==> invar_visited_through_seen (DFS_upd1 dfs_state)"
  by(fastforce simp: Let_def DFS_upd1_def dest: append_vwalk_pref hd_of_vwalk_bet''
               elim!: invar_props_elims intro!: invar_props_intros)


lemma invar_visited_through_seen_holds_2[invar_holds_intros]: 
  "[DFS_call_2_conds dfs_state; invar_well_formed dfs_state; invar_seen_stack dfs_state;
    invar_visited_through_seen dfs_state] ==> invar_visited_through_seen (DFS_upd2 dfs_state)"
proof(rule invar_props_intros, elim invar_visited_through_seen_props call_cond_elims exE,  goal_cases)
  case (1 v1 p v2 stack_tl)
  text ‹We know one thing: a path starting at @{term v1} and ending at @{term t} intersects with the
 old stack @{term "v2 # stack_tl"}.
 We have two cases:›
  hence "set p ∩ set (stack dfs_state) ≠ {}"
    by (auto simp: DFS_upd2_def)
  then obtain u where "u ∈ set p ∩ set (stack dfs_state)"
    by auto
  show ?case
  proof(cases "u ∈ set stack_tl")
    case True
    text ‹
 Case 1: If the point of intersection of the path is in @{term stack_tl}, then we are done.›
    thus ?thesis
      using 1 ‹u ∈ set p ∩ set (stack dfs_state)›
      by (auto simp: DFS_upd2_def)
  next
    case False
    hence "u = v2"
      using 1 ‹u ∈ set p ∩ set (stack dfs_state)›
      by auto
    
    text ‹
 Case 2: If it intersects the old stack at @{term v2}, which is the more interesting case as
 @{term v2} will not be in the new stack.›
    then obtain p1 p2 where [simp]: "p = p1 @ [v2] @ p2"
      using ‹u ∈ set p ∩ set (stack dfs_state)›
      by (auto simp: in_set_conv_decomp)
    text ‹
 Let @{term "p = p1 @ [v2] @ p2"}.›

    hence "set (v2 # p2) ∩ set (stack dfs_state) ≠ {}"
      using 1
      by (auto simp: DFS_upd2_def)
    text ‹
 Since the invariant holds for the old state, then @{term "[v2] @ p2"}
 intersects the old stack @{term "v2 # stack_tl"}.›

    show ?thesis
    proof(cases "p2 = []")
      case True
    text ‹
 There are two cases we need to consider
 here:
 Case a: @{term "p2 = []"} This cannot be the case, since it would imply that @{term "v2 = t"}, which
 violates the assumption of us being in this execution branch.›
      thus ?thesis
        using 1
          by (auto simp: vwalk_bet_snoc)
    next
      case False
      text ‹
 Case b: @{term "p2 ≠ []"} From the current branch's assumptions, we know that @{term "hd p2"}, who
 is a neighbour of @{term v2}, is in @{term "seen dfs_state"}. This means that, from the
 invariant at @{term dfs_state}, we can conclude that @{term "v2#p2"} intersects with the
 old stack. However, since it is distinct, that means that @{term p2}
 cannot contain @{term v2}. This means that it intersects @{term stack_tl},
 which implies that @{term p} with @{term stack_tl}. This finishes our proof.›
      hence "hd p2 ∈ t_set (N_G v2)"
        using ‹vwalk_bet (Graph.digraph_abs G) v1 p t›
        by (auto dest!: split_vwalk simp:  neq_Nil_conv)
      hence "hd p2 ∈ t_set (seen dfs_state)"
        using 1
        by (fastforce elim!: invar_props_elims simp del: ‹p = p1 @ [v2] @ p2›)
      hence "set p2 ∩ set (stack dfs_state) ≠ {}" 
        using 1 False 
        by (fastforce simp: DFS_upd2_def neq_Nil_conv dest!: split_vwalk)
      moreover have "v2 ∉ set p2"
        using ‹distinct p›
        by auto
      ultimately have "set p2 ∩ set (stack (DFS_upd2 dfs_state)) ≠ {}" 
        using 1 
        by (auto simp: DFS_upd2_def)
      thus ?thesis
        by auto
    qed
  qed
qed

lemma invar_visited_through_seen_holds_4[invar_holds_intros]: "[DFS_ret_1_conds dfs_state; invar_visited_through_seen dfs_state] ==> invar_visited_through_seen (DFS_ret1 dfs_state)"
  by (auto simp: intro: invar_props_intros simp: DFS_ret1_def)

lemma invar_visited_through_seen_holds_5[invar_holds_intros]: "[DFS_ret_2_conds dfs_state; invar_visited_through_seen dfs_state] ==> invar_visited_through_seen (DFS_ret2 dfs_state)"
  by (auto simp: intro: invar_props_intros simp: DFS_ret2_def)

lemma invar_visited_through_seen_holds[invar_holds_intros]: 
   assumes "DFS_dom dfs_state" "invar_well_formed dfs_state" "invar_seen_stack dfs_state"
           "invar_visited_through_seen dfs_state"
   shows "invar_visited_through_seen (DFS dfs_state)" 
   using assms(2-)
proof(induction rule: DFS_induct[OF assms(1)])
  case IH: (1 dfs_state)
  show ?case
    apply(rule DFS_cases[where dfs_state = dfs_state])
    by (auto intro!: IH(2-6) invar_holds_intros simp: DFS_simps[OF IH(1)])
qed

(*abbreviation "seen_verts dfs_state \<equiv> (set (stack dfs_state) \<union> t_set (visited dfs_state))"*)
                                      
definition "state_rel_1 dfs_state_1 dfs_state_2
              = ( t_set (seen dfs_state_1) ⊆ t_set (seen dfs_state_2))"

lemma state_rel_1_props[elim!]: "state_rel_1 dfs_state_1 dfs_state_2 ==>
                                  (t_set (seen dfs_state_1) ⊆ t_set (seen dfs_state_2) ==> P) ==> P "
  by (auto simp: state_rel_1_def)

lemma state_rel_1_intro[state_rel_intros]:
  "[t_set (seen dfs_state_1) ⊆ t_set (seen dfs_state_2)] ==> state_rel_1 dfs_state_1 dfs_state_2"
  by (auto simp: state_rel_1_def)

lemma state_rel_1_trans:
  "[state_rel_1 dfs_state_1 dfs_state_2; state_rel_1 dfs_state_2 dfs_state_3] ==>
   state_rel_1 dfs_state_1 dfs_state_3"
  by (auto intro!: state_rel_intros)

lemma state_rel_1_holds_1[state_rel_holds_intros]:
  "[DFS_call_1_conds dfs_state; invar_well_formed dfs_state] ==> state_rel_1 dfs_state (DFS_upd1 dfs_state)"
  by (auto simp: Let_def DFS_upd1_def elim!: invar_props_elims intro!: state_rel_intros)

lemma state_rel_1_holds_2[state_rel_holds_intros]:
  "[DFS_call_2_conds dfs_state; invar_well_formed dfs_state] ==> state_rel_1 dfs_state (DFS_upd2 dfs_state)"
  by (auto simp: DFS_upd2_def intro!: state_rel_intros elim: call_cond_elims)

lemma state_rel_1_holds_4[state_rel_holds_intros]:
  "[DFS_ret_1_conds dfs_state] ==> state_rel_1 dfs_state (DFS_ret1 dfs_state)"
  by (auto simp: intro!: state_rel_intros simp: DFS_ret1_def)

lemma state_rel_1_holds_5[state_rel_holds_intros]:
  "[DFS_ret_2_conds dfs_state] ==> state_rel_1 dfs_state (DFS_ret2 dfs_state)"
  by (auto simp: intro!: state_rel_intros simp: DFS_ret2_def)

lemma state_rel_1_holds[state_rel_holds_intros]:
   assumes "DFS_dom dfs_state" "invar_well_formed dfs_state"
   shows "state_rel_1 dfs_state (DFS dfs_state)" 
   using assms(2-)
proof(induction rule: DFS_induct[OF assms(1)])
  case IH: (1 dfs_state)
  show ?case
    apply(rule DFS_cases[where dfs_state = dfs_state])
    by (auto intro: state_rel_1_trans invar_holds_intros state_rel_holds_intros intro!: IH(2-) simp: DFS_simps[OF IH(1)])
qed

lemma DFS_ret_1[ret_holds_intros]: "DFS_ret_1_conds (dfs_state) ==> DFS_ret_1_conds (DFS_ret1 dfs_state)"
  by (auto simp: elim!: call_cond_elims intro!: call_cond_intros simp: DFS_ret1_def)

lemma ret1_holds[ret_holds_intros]:
   assumes "DFS_dom dfs_state" "return (DFS dfs_state) = NotReachable"
   shows "DFS_ret_1_conds (DFS dfs_state)" 
   using assms(2-)
proof(induction  rule: DFS_induct[OF assms(1)])
  case IH: (1 dfs_state)
  show ?case
    apply(rule DFS_cases[where dfs_state = dfs_state])
    using IH(4)                                                                
    by (auto intro: ret_holds_intros intro!: IH(2-) simp: DFS_simps[OF IH(1)] DFS_ret2_def)
qed

lemma DFS_correct_ret_1:
  "[invar_visited_through_seen dfs_state; DFS_ret_1_conds dfs_state; u ∈ t_set (seen dfs_state)]
         ==> ∄p. distinct p ∧ vwalk_bet (Graph.digraph_abs G) u p t"
  by (auto elim!: call_cond_elims invar_props_elims)

lemma DFS_ret_2[ret_holds_intros]: "DFS_ret_2_conds (dfs_state) ==> DFS_ret_2_conds (DFS_ret2 dfs_state)"
  by (auto simp: elim!: call_cond_elims intro!: call_cond_intros simp: DFS_ret2_def)

lemma ret2_holds[ret_holds_intros]:
   assumes "DFS_dom dfs_state" "return (DFS dfs_state) = Reachable"
   shows "DFS_ret_2_conds (DFS dfs_state)" 
   using assms(2-)
proof(induction  rule: DFS_induct[OF assms(1)])
  case IH: (1 dfs_state)
  show ?case
    apply(rule DFS_cases[where dfs_state = dfs_state])
    using IH(4)                                                                
    by (auto intro: ret_holds_intros intro!: IH(2-) simp: DFS_simps[OF IH(1)] DFS_ret1_def)
qed

lemma DFS_correct_ret_2:
  "[invar_stack_walk dfs_state; DFS_ret_2_conds dfs_state]
         ==> vwalk_bet (Graph.digraph_abs G) (last (stack dfs_state)) (rev (stack dfs_state)) t"
  by (auto elim!: call_cond_elims invar_props_elims simp: hd_rev vwalk_bet_def)

subsection ‹Termination›

named_theorems termination_intros

declare termination_intros

lemma in_prod_relI[intro!,termination_intros]:
  "[f1 a = f1 a'; (a, a') ∈ f2 <*mlex*> r] ==> (a,a') ∈ (f1 <*mlex*> f2 <*mlex*> r)"
   by (simp add: mlex_iff)+

definition "less_rel = {(x::nat, y::nat). x < y}"

lemma wf_less_rel[intro!]: "wf less_rel"
  by(auto simp: less_rel_def wf_less)

lemma call_1_measure_nonsym[simp]: "(call_1_measure dfs_state, call_1_measure dfs_state) ∉ less_rel"
  by (auto simp: less_rel_def)

lemma call_1_terminates[termination_intros]:
  "[DFS_call_1_conds dfs_state; invar_well_formed dfs_state; invar_seen_stack dfs_state] ==>
     (DFS_upd1 dfs_state, dfs_state) ∈ call_1_measure <*mlex*> r"
  by(fastforce elim!: invar_props_elims call_cond_elims
          simp add: DFS_upd1_def call_1_measure_def Let_def 
          intro!: mlex_less psubset_card_mono
          dest!: Graph.vset.choose')

lemma call_2_measure_nonsym[simp]: "(call_2_measure dfs_state, call_2_measure dfs_state) ∉ less_rel"
  by (auto simp: less_rel_def)

lemma call_2_measure_1[termination_intros]:
  "[DFS_call_2_conds dfs_state; invar_well_formed dfs_state] ==>
    call_1_measure dfs_state = call_1_measure (DFS_upd2 dfs_state)"
  by(auto simp add: DFS_upd2_def call_1_measure_def Let_def
          intro!: psubset_card_mono)

lemma call_2_terminates[termination_intros]:
  "[DFS_call_2_conds dfs_state; invar_well_formed dfs_state; invar_seen_stack dfs_state] ==>
     (DFS_upd2 dfs_state, dfs_state) ∈ call_2_measure <*mlex*> r"
  by(auto elim!: invar_props_elims elim!: call_cond_elims
          simp add: DFS_upd2_def call_2_measure_def
          intro!: mlex_less)

lemma wf_term_rel: "wf DFS_term_rel"
  by(auto simp: wf_mlex DFS_term_rel_def)

lemma in_DFS_term_rel[termination_intros]:
  "[DFS_call_1_conds dfs_state; invar_well_formed dfs_state; invar_seen_stack dfs_state] ==>
            (DFS_upd1 dfs_state, dfs_state) ∈ DFS_term_rel" 
  "[DFS_call_2_conds dfs_state; invar_well_formed dfs_state; invar_seen_stack dfs_state] ==>
            (DFS_upd2 dfs_state, dfs_state) ∈ DFS_term_rel"
  by (simp add: DFS_term_rel_def termination_intros)+

lemma DFS_terminates[termination_intros]:
  assumes "invar_well_formed dfs_state" "invar_seen_stack dfs_state"
  shows "DFS_dom dfs_state"
  using wf_term_rel assms
proof(induction rule: wf_induct_rule)
  case (less x)
  show ?case
    by (rule DFS_domintros) (auto intro!: invar_holds_intros less in_DFS_term_rel)
qed

subsection ‹Final Correctness Theorems›

lemma initial_state_props[invar_holds_intros, termination_intros]:
  "invar_well_formed (initial_state)" "invar_stack_walk (initial_state)" "invar_seen_stack (initial_state)"
  "invar_visited_through_seen (initial_state)" "invar_s_in_stack initial_state" 
  "DFS_dom initial_state"
  by (auto simp: initial_state_def
                 hd_of_vwalk_bet''
           elim: vwalk_betE
           intro!: termination_intros invar_props_intros)

lemma DFS_correct_1:
  assumes "return (DFS initial_state) = NotReachable"
  shows   "∄p. distinct p ∧ vwalk_bet (Graph.digraph_abs G) s p t"
proof-
  have "s ∈ t_set (seen (DFS initial_state))"
    by(auto intro!: invar_holds_intros ret_holds_intros state_rel_holds_intros
            intro: state_rel_1_props[where ?dfs_state_1.0 = initial_state]
            simp add: initial_state_def)
  thus ?thesis
    using assms
    by(intro DFS_correct_ret_1[where dfs_state = "DFS initial_state"])
      (auto intro!: invar_holds_intros ret_holds_intros state_rel_holds_intros)
qed

lemma DFS_correct_2:
  assumes  "return (DFS initial_state) = Reachable"
  shows "vwalk_bet (Graph.digraph_abs G) s (rev (stack (DFS initial_state))) t"
proof-
  have "vwalk_bet
              (Graph.digraph_abs G)
              (last (stack (DFS initial_state)))
              (rev (stack (DFS initial_state))) t"
    using assms
    by(auto intro!: invar_holds_intros ret_holds_intros state_rel_holds_intros
                       DFS_correct_ret_2[where dfs_state = "DFS initial_state"])
  moreover hence "(last (stack (DFS initial_state))) = s"
    by(fastforce intro!: invar_holds_intros
                 intro: invar_s_in_stack_props[where dfs_state = "DFS initial_state"])+
  ultimately show ?thesis
    by auto
qed
end
end

end