SSL BFS_2.thy

theory BFS_2
  imports Pair_Graph_Specs Dist Set2_Addons More_Lists
begin

section ‹Breadth-First Search›

subsection ‹The Program State›
record ('parents, 'vset) BFS_state = parents:: "'parents" current:: "'vset" visited:: "'vset"

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 BFS =
  Graph: Pair_Graph_Specs
    where lookup = lookup +
  set_ops: Set2 vset_empty vset_delete _ t_set vset_inv insert
  
for lookup :: "'adjmap ==> 'ver ==> 'vset option" +

fixes  
srcs::"'vset" and
G::"'adjmap" and expand_tree::"'adjmap ==> 'vset ==> 'vset ==> 'adjmap" and
next_frontier::"'vset ==> 'vset ==> 'vset" 


assumes
   expand_tree[simp]:
     "[Graph.graph_inv BFS_tree; vset_inv frontier; vset_inv vis; Graph.graph_inv G] ==>
       Graph.graph_inv (expand_tree BFS_tree frontier vis)"
     "[Graph.graph_inv BFS_tree; vset_inv frontier; vset_inv vis; Graph.graph_inv G] ==>
        Graph.digraph_abs (expand_tree BFS_tree frontier vis) =
         (Graph.digraph_abs BFS_tree) ∪
         {(u,v) | u v. u ∈ t_set (frontier) ∧
                       v ∈ (Pair_Graph.neighbourhood (Graph.digraph_abs G) u -
                       t_set vis)}" and
   next_frontier[simp]:
    "[vset_inv frontier; vset_inv vis; Graph.graph_inv G] ==> vset_inv (next_frontier frontier vis)"
    "[vset_inv frontier; vset_inv vis; Graph.graph_inv G] ==>
       t_set (next_frontier frontier vis) =
         (∪ {Pair_Graph.neighbourhood (Graph.digraph_abs G) u | u . u ∈ t_set frontier}) - t_set vis"

begin

definition "BFS_axiom ⟷
  Graph.graph_inv G ∧ Graph.finite_graph G ∧ Graph.finite_vsets ∧
  t_set srcs ⊆ dVs (Graph.digraph_abs G) ∧
  (∀u. finite (Pair_Graph.neighbourhood (Graph.digraph_abs G) u)) ∧
  t_set srcs ≠ {} ∧ vset_inv srcs"

abbreviation "neighb' ≡ Graph.neighb G" 
notation "neighb'" ("N_G _" 100)

subsection ‹The Algorithm Definition›

function (domintros) BFS::"('adjmap, 'vset) BFS_state ==> ('adjmap, 'vset) BFS_state" where
  "BFS BFS_state =
     (
        if current BFS_state ≠ ∅_V then
          let
            visited' = visited BFS_state ∪_G current BFS_state;
            parents' = expand_tree (parents BFS_state) (current BFS_state) visited';
            current' = next_frontier (current BFS_state) visited'
          in
            BFS (BFS_state (parents:= parents', visited := visited', current := current'))
         else
          BFS_state)"
  by pat_completeness auto

subsection ‹Setup for Reasoning About the Algorithm›

definition "BFS_call_1_conds bfs_state = ( (current bfs_state) ≠ ∅_V)"

definition "BFS_upd1 BFS_state =
( let
          visited' = visited BFS_state ∪_G current BFS_state;
          parents' = expand_tree (parents BFS_state) (current BFS_state) visited';
          current' = next_frontier (current BFS_state) visited'
        in
          BFS_state (parents:= parents', visited := visited', current := current')

)" 


definition "BFS_ret_1_conds bfs_state = ((current bfs_state) = ∅_V)"

abbreviation "BFS_ret1 bfs_state ≡ bfs_state"


lemma DFS_call_1_conds[call_cond_elims]: 
  "BFS_call_1_conds bfs_state ==>
   [(current bfs_state) ≠ ∅_V ==> P]
   ==> P"
  by(auto simp: BFS_call_1_conds_def split: list.splits option.splits if_splits)


lemma BFS_ret_1_conds[call_cond_elims]:
  "BFS_ret_1_conds bfs_state ==>
   [(current bfs_state) = ∅_V ==> P]
   ==> P"
  by(auto simp: BFS_ret_1_conds_def split: list.splits option.splits if_splits)

lemma BFS_ret_1_condsI[call_cond_intros]:
  "[(current bfs_state) = ∅_V] ==> BFS_ret_1_conds bfs_state"
  by(auto simp: BFS_ret_1_conds_def split: list.splits option.splits if_splits)

lemma BFS_cases:
  assumes "BFS_call_1_conds bfs_state ==> P"
      "BFS_ret_1_conds bfs_state ==> P"
  shows "P"
proof-
  have "BFS_call_1_conds bfs_state ∨
        BFS_ret_1_conds bfs_state"
    by (auto simp add: BFS_call_1_conds_def
                        BFS_ret_1_conds_def
           split: list.split_asm option.split_asm if_splits)
  then show ?thesis
    using assms
    by auto
qed

lemma BFS_simps:
  assumes "BFS_dom BFS_state" 
  shows"BFS_call_1_conds BFS_state ==> BFS BFS_state = BFS (BFS_upd1 BFS_state)"
      "BFS_ret_1_conds BFS_state ==> BFS BFS_state = BFS_ret1 BFS_state"
  by (auto simp add: BFS.psimps[OF assms]
                     BFS_call_1_conds_def BFS_upd1_def 
                     BFS_ret_1_conds_def Let_def
            split: list.splits option.splits if_splits)

lemma BFS_induct: 
  assumes "BFS_dom bfs_state"
  assumes "∧bfs_state. [BFS_dom bfs_state;
                        (BFS_call_1_conds bfs_state ==> P (BFS_upd1 bfs_state))]
              ==> P bfs_state"
  shows "P bfs_state"
  apply(rule BFS.pinduct)
  subgoal using assms(1) .
  apply(rule assms(2))
  by (auto simp add: BFS_call_1_conds_def BFS_upd1_def Let_def
           split: list.splits option.splits if_splits)

lemma BFS_domintros: 
  assumes "BFS_call_1_conds BFS_state ==> BFS_dom (BFS_upd1 BFS_state)"
  shows "BFS_dom BFS_state"
proof(rule BFS.domintros, goal_cases)
  case (1)
  then show ?case
    using assms(1)[simplified BFS_call_1_conds_def BFS_upd1_def]
    by (force simp: Let_def split: list.splits option.splits if_splits)
qed

subsection ‹The Loop Invariants›

definition invar_well_formed::"('adjmap, 'vset) BFS_state ==> bool" where
  "invar_well_formed bfs_state = (
              vset_inv (visited bfs_state) ∧ vset_inv (current bfs_state) ∧
              Graph.graph_inv (parents bfs_state) ∧
              finite (t_set (current bfs_state)) ∧ finite (t_set (visited bfs_state)))"

definition invar_subsets::"('adjmap, 'vset) BFS_state ==> bool" where
  "invar_subsets bfs_state = (
  Graph.digraph_abs (parents bfs_state) ⊆ Graph.digraph_abs G ∧
  t_set (visited bfs_state) ⊆ dVs (Graph.digraph_abs G) ∧
  t_set (current bfs_state) ⊆ dVs (Graph.digraph_abs G) ∧
  dVs (Graph.digraph_abs (parents bfs_state)) ⊆ t_set (visited bfs_state) ∪ t_set (current bfs_state) ∧
  t_set srcs ⊆ t_set (visited bfs_state) ∪ t_set (current bfs_state))"

definition "invar_3_1 bfs_state =
  (∀v∈t_set (current bfs_state). ∀u. u ∈ t_set (current bfs_state) ⟷
      distance_set (Graph.digraph_abs G) (t_set srcs) v =
                           distance_set (Graph.digraph_abs G) (t_set srcs) u)"

definition "invar_3_2 bfs_state =
  (∀v∈t_set (current bfs_state). ∀u ∈ t_set (visited bfs_state) ∪ t_set (current bfs_state).
     distance_set (Graph.digraph_abs G) (t_set srcs) u ≤
       distance_set (Graph.digraph_abs G) (t_set srcs) v)"

definition "invar_3_3 bfs_state =
  (∀v∈t_set (visited bfs_state).
     neighbourhood (Graph.digraph_abs G) v ⊆ t_set (visited bfs_state) ∪ t_set (current bfs_state))"

definition invar_dist_bounded::"('adjmap, 'vset) BFS_state ==> bool" where
  "invar_dist_bounded bfs_state =
  (∀v∈ t_set (visited bfs_state) ∪ t_set (current bfs_state).
     ∀u. distance_set (Graph.digraph_abs G) (t_set srcs) u ≤
           distance_set (Graph.digraph_abs G) (t_set srcs) v
             ⟶ u ∈ t_set (visited bfs_state) ∪ t_set (current bfs_state))"

definition invar_goes_through_current::"('adjmap, 'vset) BFS_state ==> bool" where
  "invar_goes_through_current bfs_state =
         (∀u∈t_set (visited bfs_state) ∪ t_set (current bfs_state).
            ∀v. v ∉ t_set (visited bfs_state) ∪ t_set (current bfs_state) ⟶
              (∀p. Vwalk.vwalk_bet (Graph.digraph_abs G) u p v ⟶
                     set p ∩ t_set (current bfs_state) ≠ {}))"

definition invar_dist::"('adjmap, 'vset) BFS_state ==> bool" where
  "invar_dist bfs_state =
  (∀v ∈ dVs (Graph.digraph_abs G) - t_set srcs.
     (v ∈ (t_set (visited bfs_state) ∪ t_set (current bfs_state)) ⟶ distance_set (Graph.digraph_abs G) (t_set srcs) v =
         distance_set (Graph.digraph_abs (parents bfs_state)) (t_set srcs) v))"

definition invar_parents_shortest_paths::"('adjmap, 'vset) BFS_state ==> bool" where
"invar_parents_shortest_paths bfs_state =
  (∀u∈t_set srcs.
      ∀ p v. Vwalk.vwalk_bet (Graph.digraph_abs (parents bfs_state)) u p v ⟶
         length p - 1 = distance_set (Graph.digraph_abs G) (t_set srcs) v)"

subsection ‹Termination Measures and Relation›

definition call_1_measure_1::"('adjmap, 'vset) BFS_state ==> nat" where
"call_1_measure_1 bfs_state=
  card (dVs (Graph.digraph_abs G) - ((t_set (visited bfs_state)) ∪ t_set (current bfs_state)))"

definition call_1_measure_2::"('adjmap, 'vset) BFS_state ==> nat" where
  "call_1_measure_2 bfs_state =
  card (t_set (current bfs_state))"

definition BFS_term_rel::"(('adjmap, 'vset) BFS_state × ('adjmap, 'vset) BFS_state) set" where
  "BFS_term_rel = call_1_measure_1 <*mlex*> call_1_measure_2 <*mlex*> {}"

definition "initial_state = (parents = empty, current = srcs, visited = ∅_V)"

lemmas[code] = initial_state_def

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

lemma graph_inv[simp]:
     "Graph.graph_inv G" 
     "Graph.finite_graph G"
     "Graph.finite_vsets" and
   srcs_in_G[simp,intro]: 
     "t_set srcs ⊆ dVs (Graph.digraph_abs G)" and
   finite_vset:
     "finite (Pair_Graph.neighbourhood (Graph.digraph_abs G) u)" and
  srcs_invar[simp]:
     "t_set srcs ≠ {}" 
     "vset_inv srcs"
  using ‹BFS_axiom›
  by (auto simp: BFS_axiom_def)

lemma invar_well_formed_props[invar_props_elims]: 
  "invar_well_formed bfs_state ==>
  ([vset_inv (visited bfs_state) ; vset_inv (current bfs_state) ;
    Graph.graph_inv (parents bfs_state);
    finite (t_set (current bfs_state)); finite (t_set (visited bfs_state))] ==> P)
     ==> P"
  by (auto simp: invar_well_formed_def)

lemma invar_well_formed_intro[invar_props_intros]:
  "[vset_inv (visited bfs_state); vset_inv (current bfs_state);
    Graph.graph_inv (parents bfs_state);
    finite (t_set (current bfs_state)); finite (t_set (visited bfs_state))]
    ==> invar_well_formed bfs_state"
  by (auto simp: invar_well_formed_def)

lemma finite_simp:
   "{(u,v). u ∈ front ∧ v ∈ (Pair_Graph.neighbourhood (Graph.digraph_abs G) u) ∧ v ∉ vis} =
       {(u,v). u ∈ front} ∩ {(u,v). v ∈ (Pair_Graph.neighbourhood (Graph.digraph_abs G) u)} - {(u,v) . v ∈ vis}"
   "finite {(u, v)| v . v ∈ (s u)} = finite (s u)"
  using finite_image_iff[where f = snd and A = "{(u, v) |v. v ∈ s u}"]
  by (auto simp: inj_on_def image_def)
  
lemma invar_well_formed_holds_upd1[invar_holds_intros]:
  "[BFS_call_1_conds bfs_state; invar_well_formed bfs_state] ==> invar_well_formed (BFS_upd1 bfs_state)"
  using finite_vset
  by(auto elim!: invar_well_formed_props call_cond_elims simp: Let_def BFS_upd1_def BFS_call_1_conds_def intro!: invar_props_intros)+

lemma invar_well_formed_holds_ret_1[invar_holds_intros]:
  "[BFS_ret_1_conds bfs_state; invar_well_formed bfs_state] ==> invar_well_formed (BFS_ret1 bfs_state)"
  by (auto simp: intro: invar_props_intros)

lemma invar_well_formed_holds[invar_holds_intros]:
   assumes "BFS_dom bfs_state" "invar_well_formed bfs_state"
   shows "invar_well_formed (BFS bfs_state)"
  using assms(2-)
proof(induction rule: BFS_induct[OF assms(1)])
  case IH: (1 bfs_state)
  show ?case
    apply(rule BFS_cases[where bfs_state = bfs_state])
    by (auto intro!: IH(2-) intro: invar_holds_intros  simp: BFS_simps[OF IH(1)])
qed

lemma invar_subsets_props[invar_props_elims]: 
  "invar_subsets bfs_state ==>
  ([Graph.digraph_abs (parents bfs_state) ⊆ Graph.digraph_abs G;
    t_set (visited bfs_state) ⊆ dVs (Graph.digraph_abs G);
    t_set (current bfs_state) ⊆ dVs (Graph.digraph_abs G);
    dVs (Graph.digraph_abs (parents bfs_state)) ⊆ t_set (visited bfs_state) ∪ t_set (current bfs_state);
    t_set srcs ⊆ t_set (visited bfs_state) ∪ t_set (current bfs_state)] ==> P)
     ==> P"
  by (auto simp: invar_subsets_def)

lemma invar_subsets_intro[invar_props_intros]:
   "[Graph.digraph_abs (parents bfs_state) ⊆ Graph.digraph_abs G;
     t_set (visited bfs_state) ⊆ dVs (Graph.digraph_abs G);
     t_set (current bfs_state) ⊆ dVs (Graph.digraph_abs G);
     dVs (Graph.digraph_abs (parents bfs_state)) ⊆ t_set (visited bfs_state) ∪ t_set (current bfs_state);
     t_set srcs ⊆ t_set (visited bfs_state) ∪ t_set (current bfs_state)]
     ==> invar_subsets bfs_state"
  by (auto simp: invar_subsets_def)

lemma invar_subsets_holds_upd1[invar_holds_intros]: 
  "[BFS_call_1_conds bfs_state; invar_well_formed bfs_state; invar_subsets bfs_state] ==> invar_subsets (BFS_upd1 bfs_state)"
  apply(auto elim!: call_cond_elims invar_well_formed_props invar_subsets_props intro!: invar_props_intros simp: BFS_upd1_def Let_def)
  apply(auto simp: dVs_def)
  apply (metis Un_iff dVsI(1) dVs_def in_mono)
  by (metis Un_iff dVsI(2) dVs_def in_mono)

lemma invar_subsets_holds_ret_1[invar_holds_intros]:
  "[BFS_ret_1_conds bfs_state; invar_subsets bfs_state] ==> invar_subsets (BFS_ret1 bfs_state)"
  by (auto simp: intro: invar_props_intros)

lemma invar_subsets_holds[invar_holds_intros]:
   assumes "BFS_dom bfs_state" "invar_well_formed bfs_state" "invar_subsets bfs_state"
   shows "invar_subsets (BFS bfs_state)"
  using assms(2-)
proof(induction rule: BFS_induct[OF assms(1)])
  case IH: (1 bfs_state)
  show ?case
    apply(rule BFS_cases[where bfs_state = bfs_state])
    by (auto intro!: IH(2-) intro: invar_holds_intros  simp: BFS_simps[OF IH(1)])
qed

― ‹This is invar\_100 on the board›

lemma invar_3_1_props[invar_props_elims]: 
  "invar_3_1 bfs_state ==>
  ([[v ∈ t_set (current bfs_state); u ∈ t_set (current bfs_state)] ==>
            distance_set (Graph.digraph_abs G) (t_set srcs) v =
                 distance_set (Graph.digraph_abs G) (t_set srcs) u;
    [v ∈ t_set (current bfs_state);
            distance_set (Graph.digraph_abs G) (t_set srcs) v =
              distance_set (Graph.digraph_abs G) (t_set srcs) u] ==>
            u ∈ t_set (current bfs_state)] ==> P)
     ==> P"
  unfolding invar_3_1_def
  by blast

lemma invar_3_1_intro[invar_props_intros]:
   "[∧u v. [v ∈ t_set (current bfs_state); u ∈ t_set (current bfs_state)] ==>
            distance_set (Graph.digraph_abs G) (t_set srcs) v =
                           distance_set (Graph.digraph_abs G) (t_set srcs) u;
     ∧u v. [v ∈ t_set (current bfs_state); distance_set (Graph.digraph_abs G) (t_set srcs) v =
                 distance_set (Graph.digraph_abs G) (t_set srcs) u] ==>
            u ∈ t_set (current bfs_state)]
    ==> invar_3_1 bfs_state"
  unfolding invar_3_1_def
  by blast

lemma invar_3_2_props[elim]: 
  "invar_3_2 bfs_state ==>
  ([∧v u. [v∈t_set (current bfs_state); u ∈ t_set (visited bfs_state) ∪ t_set (current bfs_state)] ==>
          distance_set (Graph.digraph_abs G) (t_set srcs) u ≤
       distance_set (Graph.digraph_abs G) (t_set srcs) v] ==> P)
     ==> P"
  unfolding invar_3_2_def
  by blast

lemma invar_3_2_intro[invar_props_intros]:
   "[∧v u. [v∈t_set (current bfs_state); u ∈ t_set (visited bfs_state) ∪ t_set (current bfs_state)] ==>
          distance_set (Graph.digraph_abs G) (t_set srcs) u ≤
       distance_set (Graph.digraph_abs G) (t_set srcs) v]
    ==> invar_3_2 bfs_state"
  unfolding invar_3_2_def
  by blast

lemma invar_3_3_props[invar_props_elims]: 
  "invar_3_3 bfs_state ==>
  ([∧v. [v ∈ t_set (visited bfs_state)] ==>
          neighbourhood (Graph.digraph_abs G) v ⊆ t_set (visited bfs_state) ∪ t_set (current bfs_state)] ==> P)
     ==> P"
  unfolding invar_3_3_def
  by blast

lemma invar_3_3_intro[invar_props_intros]:
   "[∧v. [v ∈ t_set (visited bfs_state)] ==>
          neighbourhood (Graph.digraph_abs G) v ⊆ t_set (visited bfs_state) ∪ t_set (current bfs_state)]
    ==> invar_3_3 bfs_state"
  unfolding invar_3_3_def
  by blast

lemma invar_dist_bounded_props[invar_props_elims]: 
  "invar_dist_bounded bfs_state ==>
  ([∧u v. [v∈ t_set (visited bfs_state) ∪ t_set (current bfs_state);
             distance_set (Graph.digraph_abs G) (t_set srcs) u ≤ distance_set (Graph.digraph_abs G) (t_set srcs) v] ==>
            u ∈ t_set (visited bfs_state) ∪ t_set (current bfs_state)] ==> P)
     ==> P"
  unfolding invar_dist_bounded_def
  by blast

lemma invar_dist_bounded_intro[invar_props_intros]:
   "[∧u v. [v∈ t_set (visited bfs_state) ∪ t_set (current bfs_state);
               distance_set (Graph.digraph_abs G) (t_set srcs) u ≤ distance_set (Graph.digraph_abs G) (t_set srcs) v] ==>
            u ∈ t_set (visited bfs_state) ∪ t_set (current bfs_state)]
    ==> invar_dist_bounded bfs_state"
  unfolding invar_dist_bounded_def
  by blast

definition "invar_current_reachable bfs_state =
  (∀v∈ t_set (visited bfs_state) ∪ t_set (current bfs_state).
     distance_set (Graph.digraph_abs G) (t_set srcs) v < ∞)"

lemma invar_current_reachable_props[invar_props_elims]: 
  "invar_current_reachable bfs_state ==>
  ([∧v. [v ∈ t_set (visited bfs_state) ∪ t_set (current bfs_state)] ==>
         distance_set (Graph.digraph_abs G) (t_set srcs) v < ∞] ==> P)
     ==> P"
  by(auto simp: invar_current_reachable_def)

lemma invar_current_reachable_intro[invar_props_intros]:
   "[∧v. [v ∈ t_set (visited bfs_state) ∪ t_set (current bfs_state)] ==>
         distance_set (Graph.digraph_abs G) (t_set srcs) v < ∞]
    ==> invar_current_reachable bfs_state"
  by(auto simp add: invar_current_reachable_def)

subsection ‹Proofs that the Invariants Hold›

lemma invar_current_reachable_holds_upd1[invar_holds_intros]: 
  "[BFS_call_1_conds bfs_state; invar_well_formed bfs_state; invar_subsets bfs_state; invar_current_reachable bfs_state]
     ==> invar_current_reachable (BFS_upd1 bfs_state)"
proof(rule invar_props_intros, goal_cases)
  case assms: (1 v)
  have ?case (is "?dist v < ∞") if "v ∉ t_set (visited bfs_state) ∪ t_set (current bfs_state)"
  proof-
    have "v ∈ t_set (current (BFS_upd1 bfs_state))"
      using that assms
      by (auto simp: BFS_upd1_def Let_def elim: invar_props_elims)
    then obtain u where "v ∈ t_set (N_G u)" "u ∈ t_set (current bfs_state)"
      using assms
      by (auto simp: BFS_upd1_def Let_def elim!: invar_props_elims)
    hence "?dist u < ∞"
      using ‹invar_subsets bfs_state› ‹invar_current_reachable bfs_state›
      by (auto elim!: invar_props_elims)
    hence "?dist v ≤ ?dist u + 1"
      using ‹v ∈ t_set (N_G u)›
      by (auto intro!: distance_set_neighbourhood)
    thus ?thesis
      using add_mono1[OF ‹?dist u < \∞›] linorder_not_less
      by fastforce
  qed
  thus ?case
    using assms
    by(force elim!: call_cond_elims invar_props_elims intro!: invar_props_intros simp: BFS_upd1_def Let_def)
qed

lemma invar_current_reachable_holds_ret_1[invar_holds_intros]:
  "[BFS_ret_1_conds bfs_state; invar_current_reachable bfs_state] ==> invar_current_reachable (BFS_ret1 bfs_state)"
  by (auto simp: intro: invar_props_intros)

lemma dist_current_plus_1_new:                                               
  assumes
    "invar_well_formed bfs_state" "invar_subsets bfs_state" "invar_dist_bounded bfs_state" 
    "v ∈ neighbourhood (Graph.digraph_abs G) v'" 
    "v' ∈ t_set (current bfs_state)"
    "v ∈ t_set (current (BFS_upd1 bfs_state))"
  shows  "distance_set (Graph.digraph_abs G) (t_set srcs) v =
            distance_set (Graph.digraph_abs G) (t_set srcs) v' + 1" (is "?dv = ?dv' + 1")
  proof-
    have False if "?dv > ?dv' + 1"
      using distance_set_neighbourhood[OF ‹v ∈ neighbourhood (Graph.digraph_abs G) v'›] that
      by (simp add: leD)


    moreover have False if "?dv < ?dv' + 1"
    proof-
      have "?dv ≤ ?dv'"
        using that eSuc_plus_1 ileI1
        by force
      moreover have "?dv ≠ ∞"
        using that enat_ord_simps(4) 
        by fastforce
      moreover have "v ∉ t_set (visited bfs_state) ∪ t_set (current bfs_state)"
        using assms
        by (auto simp: BFS_upd1_def Let_def elim!: invar_well_formed_props invar_subsets_props)
        
      moreover have "v' ∈ t_set (visited bfs_state) ∪ t_set (current bfs_state)"
        using ‹v' ∈ t_set (current bfs_state)› ‹invar_subsets bfs_state›
        by (auto elim!: invar_subsets_props)

      ultimately show False
        using ‹invar_dist_bounded bfs_state›
        apply(elim invar_props_elims)
        apply(drule dist_set_not_inf)
        using dual_order.trans dist_set_mem
        by (smt (verit, best))
    qed
    ultimately show ?thesis
      by force
  qed

lemma plus_lt_enat: "[(a::enat) ≠ ∞; b < c] ==> a + b < a + c"
  using enat_add_left_cancel_less
  by presburger

lemma plus_one_side_lt_enat: "[(a::enat) ≠ ∞; 0 < b] ==> a < a + b"
  using plus_lt_enat
  by auto

lemma invar_3_1_holds_upd1_new[invar_holds_intros]: 
  "[BFS_call_1_conds bfs_state; invar_well_formed bfs_state; invar_subsets bfs_state ; invar_3_1 bfs_state;
    invar_3_2 bfs_state; invar_dist_bounded bfs_state; invar_current_reachable bfs_state]
     ==> invar_3_1 (BFS_upd1 bfs_state)"
proof(intro invar_props_intros, goal_cases)
  case assms: (1 u v)
  obtain u' v' where
    uv'[intro]: "u ∈ neighbourhood (Graph.digraph_abs G) u'" "u' ∈ t_set (current bfs_state)" 
                "v ∈ neighbourhood (Graph.digraph_abs G) v'" "v' ∈ t_set (current bfs_state)"
    using assms(1,2,8,9)    
    by (auto simp: BFS_upd1_def Let_def elim!: invar_well_formed_props)
  moreover hence "distance_set (Graph.digraph_abs G) (t_set srcs) v' =
                    distance_set (Graph.digraph_abs G) (t_set srcs) u'" (is "?d v' = ?d u'")
    using ‹invar_3_1 bfs_state›
    by (auto elim: invar_props_elims)
  moreover have "distance_set (Graph.digraph_abs G) (t_set srcs) v = ?d v' + 1"
    using assms               
    by (auto intro!: dist_current_plus_1_new)
  moreover have "distance_set (Graph.digraph_abs G) (t_set srcs) u = ?d u' + 1"
    using assms
    by (auto intro!: dist_current_plus_1_new)
  ultimately show ?case
    by auto
next
  case (2 u v)
  then obtain v' where uv'[intro]:
    "v ∈ neighbourhood (Graph.digraph_abs G) v'" "v' ∈ t_set (current bfs_state)"    
    by (auto simp: BFS_upd1_def Let_def elim!: invar_well_formed_props invar_subsets_props)
  hence "distance_set (Graph.digraph_abs G) (t_set srcs) v =
           distance_set (Graph.digraph_abs G) (t_set srcs) v' + 1" (is "?d v = ?d v' + _")
    using 2
    by(fastforce intro!: dist_current_plus_1_new)

  show ?case
  proof(cases "0 < ?d u")
    case in_srcs: True
    moreover have "?d v' < ∞"
      using ‹?d v = ?d u› ‹invar_well_formed bfs_state› ‹invar_subsets bfs_state› ‹v' ∈ t_set (current bfs_state)›
            ‹invar_current_reachable bfs_state›
      by (auto elim!: invar_well_formed_props invar_subsets_props invar_current_reachable_props)
    hence "?d v < ∞"
      using ‹?d v = ?d v' + 1›
      by (simp add: plus_eq_infty_iff_enat)
    hence "?d u < ∞"
      using ‹?d v = ?d u›
      by auto
    ultimately obtain u' where "?d u' + 1 = ?d u" "u ∈ neighbourhood (Graph.digraph_abs G) u'"
      using distance_set_parent'
      by (metis srcs_invar(1))
    hence "?d u' = ?d v'"
      using ‹?d v = ?d v' + 1› ‹?d v = ?d u›
      by auto
    hence "u' ∈ t_set (current bfs_state)"
      using ‹invar_3_1 bfs_state›
            ‹v' ∈ t_set (current bfs_state)›
      by (auto elim!: invar_3_1_props)
    moreover have "?d u' < ?d u"
      using ‹?d u < \∞›
      using zero_less_one not_infinity_eq 
      by (fastforce intro!: plus_one_side_lt_enat simp: ‹?d u' + 1 = ?d u›[symmetric])
    hence "u ∉ t_set (visited bfs_state) ∪ t_set (current bfs_state)"
      using ‹invar_3_2 bfs_state› ‹u' ∈ t_set (current bfs_state)›
      by (auto elim!: invar_3_2_props dest: leD)
    ultimately show ?thesis
      using ‹invar_well_formed bfs_state› ‹invar_subsets bfs_state› ‹u ∈ neighbourhood (Graph.digraph_abs G) u'›
      apply(auto simp: BFS_upd1_def Let_def elim!: invar_well_formed_props invar_subsets_props)
      by blast
  next
    case not_in_srcs: False
    text ‹Contradiction because if ‹u ∈ srcs› then distance srcs to a vertex in srcs is > 0. This is
 because the distance from srcs to ‹u› is the same as that to ‹v›.›
    then show ?thesis
      using ‹?d v = ?d u› ‹?d v = ?d v' + 1›
      by auto
  qed
qed

lemma invar_3_1_holds_ret_1[invar_holds_intros]:
  "[BFS_ret_1_conds bfs_state; invar_3_3 bfs_state] ==> invar_3_3 (BFS_ret1 bfs_state)"
  by (auto simp: intro: invar_props_intros)

lemma invar_3_2_holds_upd1_new[invar_holds_intros]: 
  "[BFS_call_1_conds bfs_state; invar_well_formed bfs_state; invar_subsets bfs_state ; invar_3_1 bfs_state;
    invar_3_2 bfs_state; invar_dist_bounded bfs_state; invar_current_reachable bfs_state]
   ==> invar_3_2 (BFS_upd1 bfs_state)"
proof(intro invar_props_intros, goal_cases)                                                                          
  case assms: (1 u v)
  show ?case
  proof(cases "v ∈ t_set (current (BFS_upd1 bfs_state))")
    case v_in_current: True
    moreover have "invar_3_1 (BFS_upd1 bfs_state)"
      using assms
      by (auto intro: invar_holds_intros)
    ultimately show ?thesis
      using ‹u ∈ t_set (current (BFS_upd1 bfs_state))›
      by (fastforce elim: invar_props_elims)
  next                     
    case v_not_in_current: False
    hence "v ∈ t_set (visited bfs_state) ∪ t_set (current bfs_state)"
      using assms(1,2,9)
      by (fastforce simp: BFS_upd1_def Let_def elim!: invar_well_formed_props)
    moreover obtain u' where uv'[intro]: "u ∈ neighbourhood (Graph.digraph_abs G) u'" "u' ∈ t_set (current bfs_state)" 
      using assms(1,2,8,9)    
      by (auto simp: BFS_upd1_def Let_def elim!: invar_well_formed_props)
    ultimately have "distance_set (Graph.digraph_abs G) (t_set srcs) v ≤
                       distance_set (Graph.digraph_abs G) (t_set srcs) u'"
      using ‹invar_3_2 bfs_state›
      by (auto elim!: invar_3_2_props)
    moreover have "distance_set (Graph.digraph_abs G) (t_set srcs) u =
           distance_set (Graph.digraph_abs G) (t_set srcs) u' + 1" (is "?d u = ?d u' + _")
      using assms
      by(fastforce intro!: dist_current_plus_1_new)
    ultimately show ?thesis
      by (metis le_iff_add order.trans)
  qed
qed

lemma invar_3_2_holds_ret_1[invar_holds_intros]:
  "[BFS_ret_1_conds bfs_state; invar_3_3 bfs_state] ==> invar_3_3 (BFS_ret1 bfs_state)"
  by (auto simp: intro: invar_props_intros)

lemma invar_3_3_holds_upd1[invar_holds_intros]: 
  "[BFS_call_1_conds bfs_state; invar_well_formed bfs_state; invar_subsets bfs_state; invar_3_3 bfs_state] ==> invar_3_3 (BFS_upd1 bfs_state)"
  by(fastforce elim!: call_cond_elims invar_well_formed_props invar_subsets_props invar_3_3_props intro!: invar_props_intros simp: BFS_upd1_def Let_def)

lemma invar_3_3_holds_ret_1[invar_holds_intros]:
  "[BFS_ret_1_conds bfs_state; invar_3_3 bfs_state] ==> invar_3_3 (BFS_ret1 bfs_state)"
  by (auto simp: intro: invar_props_intros)

lemma invar_dist_bounded_holds_upd1[invar_holds_intros]: 
  "[BFS_call_1_conds bfs_state; invar_well_formed bfs_state; invar_subsets bfs_state;
    invar_3_1 bfs_state; invar_3_2 bfs_state; invar_3_3 bfs_state; invar_dist_bounded bfs_state;
    invar_current_reachable bfs_state] ==>
    invar_dist_bounded (BFS_upd1 bfs_state)"
proof(intro invar_props_intros, goal_cases)                                                                                                    
  case assms: (1 u v)
  show ?case
  proof(cases ‹v ∈ t_set (visited bfs_state) ∪ t_set (current bfs_state)›)
    case v_visited: True
    hence "u ∈ t_set (visited bfs_state) ∪ t_set (current bfs_state)"
      using ‹invar_dist_bounded bfs_state› assms
      by (auto elim!: invar_dist_bounded_props)
    then show ?thesis 
      using ‹invar_well_formed bfs_state› ‹v ∈ t_set (visited (BFS_upd1 bfs_state)) ∪ t_set (current (BFS_upd1 bfs_state))›
      by (auto simp: BFS_upd1_def Let_def elim: invar_props_elims)
  next
    case v_not_visited: False
    hence "v ∈ t_set (current (BFS_upd1 bfs_state))"
      using ‹invar_well_formed bfs_state› ‹v ∈ t_set (visited (BFS_upd1 bfs_state)) ∪ t_set (current (BFS_upd1 bfs_state))›
      by (auto simp: BFS_upd1_def Let_def elim: invar_props_elims)
    then obtain v' where v'[intro]:
      "v ∈ neighbourhood (Graph.digraph_abs G) v'" "v' ∈ t_set (current bfs_state)"
      using ‹invar_well_formed bfs_state›
      by (auto simp: BFS_upd1_def Let_def elim!: invar_well_formed_props)
    have "distance_set (Graph.digraph_abs G) (t_set srcs) v =
            distance_set (Graph.digraph_abs G) (t_set srcs) v' + 1" (is "?dv = ?dv' + 1")
      using assms ‹v ∈ t_set (current (BFS_upd1 bfs_state))›
      by (auto intro!: dist_current_plus_1_new)
    moreover have "u ∈ t_set (visited (BFS_upd1 bfs_state)) ∪ t_set (current (BFS_upd1 bfs_state))"
      if "distance_set (Graph.digraph_abs G) (t_set srcs) u ≤ ?dv'" (is "?du ≤ ?dv'")
      using that ‹invar_well_formed bfs_state› ‹invar_subsets bfs_state› ‹invar_dist_bounded bfs_state›
      by (fastforce simp: BFS_upd1_def Let_def elim!: invar_well_formed_props invar_subsets_props invar_dist_bounded_props)
    moreover have "u ∈ t_set (visited (BFS_upd1 bfs_state)) ∪ t_set (current (BFS_upd1 bfs_state))"
      if "distance_set (Graph.digraph_abs G) (t_set srcs) u = ?dv"
    proof-
      have "invar_3_1 (BFS_upd1 bfs_state)"
        by (auto intro: assms invar_holds_intros)
      hence "u ∈ t_set (current (BFS_upd1 bfs_state))"
        using that ‹invar_3_1 bfs_state› ‹v ∈ t_set (current (BFS_upd1 bfs_state))›
        by (auto elim!: invar_3_1_props)
      moreover have "invar_well_formed (BFS_upd1 bfs_state)" "invar_subsets (BFS_upd1 bfs_state)"
        using ‹BFS_call_1_conds bfs_state› ‹invar_well_formed bfs_state› ‹invar_subsets bfs_state›
        by(auto intro!: invar_well_formed_holds_upd1 invar_subsets_holds_upd1)
      ultimately show ?thesis
        by (auto elim!: invar_props_elims)
    qed
    ultimately show ?thesis
      using ‹?du ≤ ?dv› ileI1 linorder_not_less plus_1_eSuc(2)
      by fastforce
  qed
qed

lemma invar_dist_bounded_holds_ret_1[invar_holds_intros]:
  "[BFS_ret_1_conds bfs_state; invar_dist_bounded bfs_state] ==> invar_dist_bounded (BFS_ret1 bfs_state)"
  by (auto simp: intro: invar_props_intros)

                                      
lemma invar_dist_props[invar_props_elims]: 
  "invar_dist bfs_state ==> v ∈ dVs (Graph.digraph_abs G) - t_set srcs ==>
   [
     [v ∈ (t_set (visited bfs_state) ∪ t_set (current bfs_state)) ==> distance_set (Graph.digraph_abs G) (t_set srcs) v =
         distance_set (Graph.digraph_abs (parents bfs_state)) (t_set srcs) v] ==> P
   ]
   ==> P"
  unfolding invar_dist_def
  by auto

lemma invar_dist_intro[invar_props_intros]:
   "[∧v. [v ∈ dVs (Graph.digraph_abs G) - t_set srcs; v ∈ t_set (visited bfs_state) ∪ t_set (current bfs_state)] ==>
           (distance_set (Graph.digraph_abs G) (t_set srcs) v =
             distance_set (Graph.digraph_abs (parents bfs_state)) (t_set srcs) v)]
        
    ==> invar_dist bfs_state"
  unfolding invar_dist_def
  by auto

lemma invar_goes_through_current_props[invar_props_elims]: 
  "invar_goes_through_current bfs_state ==>
   [[∧u v p. [u ∈t_set (visited bfs_state) ∪ t_set (current bfs_state);
              v ∉ t_set (visited bfs_state) ∪ t_set (current bfs_state);
              Vwalk.vwalk_bet (Graph.digraph_abs G) u p v]
      ==> set p ∩ t_set (current bfs_state) ≠ {}]
     ==> P]
   ==> P"
  unfolding invar_goes_through_current_def
  by auto

lemma invar_goes_through_current_intro[invar_props_intros]:
  "[∧u v p. [u ∈t_set (visited bfs_state) ∪ t_set (current bfs_state);
             v ∉ t_set (visited bfs_state) ∪ t_set (current bfs_state);
              Vwalk.vwalk_bet (Graph.digraph_abs G) u p v]
      ==> set p ∩ t_set (current bfs_state) ≠ {}]
    ==> invar_goes_through_current bfs_state"
  unfolding invar_goes_through_current_def
  by auto

lemma invar_goes_through_active_holds_upd1[invar_holds_intros]: 
  "[BFS_call_1_conds bfs_state; invar_well_formed bfs_state; invar_subsets bfs_state;
    invar_goes_through_current bfs_state]
    ==> invar_goes_through_current (BFS_upd1 bfs_state)"
proof(intro invar_props_intros, goal_cases)
  case (1 u v p)
  hence "v ∉ t_set (visited bfs_state) ∪ t_set (current bfs_state)"
    by (auto simp: Let_def BFS_upd1_def elim!: invar_well_formed_props invar_subsets_props)
  show ?case
  proof(cases "u ∈ t_set (visited bfs_state) ∪ t_set (current bfs_state)")
    case u_in_visited: True
      have "Vwalk.vwalk_bet (Graph.digraph_abs G) u p v" "set p ∩ t_set (current bfs_state) ≠ {}"
        using ‹invar_goes_through_current bfs_state›
              ‹v ∉ t_set (visited bfs_state) ∪ t_set (current bfs_state)›
          ‹vwalk_bet (Graph.digraph_abs G) u p v› u_in_visited
        by (auto elim!: invar_goes_through_current_props)
      moreover have "u ∈ set p"
        using ‹Vwalk.vwalk_bet (Graph.digraph_abs G) u p v›
        by(auto intro: hd_of_vwalk_bet'')
      ultimately have "∃ p1 x p2. p = p1 @ [x] @ p2 ∧
                          x ∈ t_set (current bfs_state) ∧
                          (∀y∈set p2. y ∉ (t_set (visited bfs_state) ∪ t_set (current bfs_state)) ∧
                                      y ∉ (t_set (current bfs_state)))"
        using ‹invar_goes_through_current bfs_state› u_in_visited
              ‹v ∉ t_set (visited bfs_state) ∪ t_set (current bfs_state)›
          ‹invar_well_formed bfs_state› ‹invar_subsets bfs_state›
        apply (intro list_2_preds[where ?P2.0 = "(λx. x ∈ t_set (current bfs_state))",
              simplified list_inter_mem_iff[symmetric]])
        by (fastforce elim!: invar_goes_through_current_props dest!: vwalk_bet_suff split_vwalk)+

    then obtain p1 x p2 where "p = p1 @ x # p2" and
      "x ∈ t_set (current bfs_state)" and
      unvisited:
      "(∧y. y∈set p2 ==> y ∉ t_set (visited bfs_state) ∪ t_set (current bfs_state))"
      by auto
    moreover have "last p = v"
      using ‹vwalk_bet (Graph.digraph_abs G) u p v›
      by auto
    ultimately have "v ∈ set p2"
      using ‹v ∉ t_set (visited bfs_state) ∪ t_set (current bfs_state)›
            ‹invar_well_formed bfs_state› ‹invar_subsets bfs_state›
      by (auto elim: invar_props_elims)
    then obtain v' p2' where "p2 = v' # p2'"
      by (cases p2) auto
    hence "v' ∈ neighbourhood (Graph.digraph_abs G) x"
      using ‹p = p1 @ x # p2› ‹Vwalk.vwalk_bet (Graph.digraph_abs G) u p v›
        split_vwalk
      by fastforce
    moreover have "v' ∈ set p2"
      using ‹p2 = v' # p2'›
      by auto
    ultimately have "v' ∈ t_set (current (BFS_upd1 bfs_state))"
      using ‹invar_well_formed bfs_state› ‹invar_subsets bfs_state› ‹x ∈ t_set (current bfs_state)›
      by(fastforce simp: BFS_upd1_def Let_def elim!: invar_well_formed_props invar_subsets_props dest!: unvisited)
    then show ?thesis
      by(auto intro!: invar_goes_through_current_intro simp: ‹p = p1 @ x # p2› ‹p2 = v' # p2'›) 
next
  case u_not_in_visited: False
  hence "u ∈ t_set (current (BFS_upd1 bfs_state))"
    using ‹invar_well_formed bfs_state›
      ‹u ∈ t_set (visited (BFS_upd1 bfs_state)) ∪ t_set (current (BFS_upd1 bfs_state))›
    by (auto simp: BFS_upd1_def Let_def elim: invar_props_elims)
  moreover have "u ∈ set p"
    using ‹Vwalk.vwalk_bet (Graph.digraph_abs G) u p v›
    by (auto intro: hd_of_vwalk_bet'')
  ultimately show ?thesis
    by(auto intro!: invar_goes_through_current_intro)
qed
qed


lemma invar_goes_through_current_holds_ret_1[invar_holds_intros]:
  "[BFS_ret_1_conds bfs_state; invar_goes_through_current bfs_state] ==> invar_goes_through_current (BFS_ret1 bfs_state)"
  by (auto simp: intro: invar_props_intros)

lemma invar_goes_through_current_holds[invar_holds_intros]: 
   assumes "BFS_dom bfs_state" "invar_well_formed bfs_state" "invar_subsets bfs_state"
            "invar_goes_through_current bfs_state"
   shows "invar_goes_through_current (BFS bfs_state)"
  using assms(2-)
proof(induction rule: BFS_induct[OF assms(1)])
  case IH: (1 bfs_state)
  show ?case
    apply(rule BFS_cases[where bfs_state = bfs_state])
    by (auto intro!: IH(2-) intro: invar_holds_intros  simp: BFS_simps[OF IH(1)])
qed

lemma invar_dist_holds_upd1_new[invar_holds_intros]: 
  "[BFS_call_1_conds bfs_state; invar_well_formed bfs_state; invar_subsets bfs_state;
    invar_dist_bounded bfs_state; invar_dist bfs_state]
    ==> invar_dist (BFS_upd1 bfs_state)"
proof(intro invar_props_intros, goal_cases)
  define bfs_state' where "bfs_state' = BFS_upd1 bfs_state"
  let ?dSrcsG = "distance_set (Graph.digraph_abs G) (t_set srcs)"
  let ?dSrcsT = "distance_set (Graph.digraph_abs (parents bfs_state)) (t_set srcs)"
  let ?dSrcsT' = "distance_set (Graph.digraph_abs (parents bfs_state')) (t_set srcs)"
  let ?dCurrG = "distance_set (Graph.digraph_abs G) (t_set (current bfs_state))"
  case (1 v)
  then show ?case
  proof(cases "distance_set (Graph.digraph_abs G) (t_set srcs) v = ∞")
    case infinite: True
    moreover have "?dSrcsG v ≤ ?dSrcsT' v"
      using ‹invar_well_formed bfs_state› ‹invar_subsets bfs_state›
      by(fastforce simp: bfs_state'_def BFS_upd1_def Let_def intro: distance_set_subset
                   elim: invar_props_elims)    
    ultimately show ?thesis
      by (simp add: bfs_state'_def)
  next
    case finite: False
    show ?thesis
    proof(cases "v ∈ t_set (visited bfs_state) ∪ t_set (current bfs_state)")
      case v_in_tree: True
      hence "?dSrcsT v = ?dSrcsG v"
        using ‹invar_dist bfs_state› ‹invar_well_formed bfs_state› ‹invar_subsets bfs_state›
              ‹v ∈ dVs (Graph.digraph_abs G) - t_set srcs›
        by (auto elim!: invar_dist_props invar_well_formed_props invar_subsets_props)

      moreover have "?dSrcsT v = ?dSrcsT' v"
      proof-
        have "?dSrcsT' v ≤ ?dSrcsT v"
          using ‹invar_well_formed bfs_state›
          by(fastforce simp: bfs_state'_def BFS_upd1_def Let_def
                       intro: distance_set_subset elim: invar_props_elims)

        moreover have "?dSrcsG v ≤ ?dSrcsT' v"
          using ‹invar_well_formed bfs_state› ‹invar_subsets bfs_state›
          by(fastforce simp: bfs_state'_def BFS_upd1_def Let_def intro: distance_set_subset
                       elim: invar_props_elims)

        ultimately show ?thesis
          using ‹?dSrcsT v = ?dSrcsG v›
          by auto
      qed
      ultimately show ?thesis
        by (auto simp: bfs_state'_def)
    next
      case v_not_in_tree: False


      show ?thesis
      proof(rule ccontr, goal_cases)
        case 1
        moreover have ‹invar_subsets bfs_state'›
          using ‹BFS_call_1_conds bfs_state› ‹invar_well_formed bfs_state› ‹invar_subsets bfs_state›
          by (auto intro!: invar_subsets_holds_upd1 simp: bfs_state'_def)
        hence ‹Graph.digraph_abs (parents bfs_state') ⊆ Graph.digraph_abs G›
          by (auto elim: invar_props_elims)
        ultimately have "?dSrcsG v < ?dSrcsT' v"
          by (simp add: distance_set_subset order_less_le bfs_state'_def)
        hence "?dSrcsG v < ?dSrcsT' v"
          text ‹because the tree is a subset of the Graph, which invar?›
          by (simp add: distance_set_subset order_less_le bfs_state'_def)

        have "v ∈ t_set (current (BFS_upd1 bfs_state))"
          using ‹v ∈ t_set (visited (BFS_upd1 bfs_state)) ∪ t_set (current (BFS_upd1 bfs_state))›
                v_not_in_tree ‹invar_well_formed bfs_state›
          by (auto simp: BFS_upd1_def Let_def elim: invar_props_elims)
        moreover then  obtain v' where v'[intro]: 
          "v ∈ neighbourhood (Graph.digraph_abs G) v'"
          "v' ∈ t_set (current bfs_state)"
          "v ∈ neighbourhood (Graph.digraph_abs (parents bfs_state')) v'"
          using v_not_in_tree ‹invar_well_formed bfs_state›
          by (auto simp: neighbourhoodD BFS_upd1_def Let_def bfs_state'_def elim!: invar_well_formed_props)
        ultimately have "?dSrcsG v = ?dSrcsG v' + 1"
          using ‹invar_well_formed bfs_state› ‹invar_dist_bounded bfs_state› ‹invar_subsets bfs_state›
          by (auto intro!: dist_current_plus_1_new)
        show False
        proof(cases "v' ∈ t_set srcs")
          case v'_in_srcs: True
          hence "?dSrcsT' v' = 0"
            by (meson dVsI(1) distance_set_0 neighbourhoodI v'(3))
          moreover have "?dSrcsG v' = 0"
            using v'_in_srcs
            by (metis ‹distance_set (Graph.digraph_abs G) (t_set srcs) v = distance_set (Graph.digraph_abs G) (t_set srcs) v' + 1› add.commute add.right_neutral dist_set_inf dist_set_mem distance_0 enat_add_left_cancel le_iff_add local.finite order_antisym)
          then show ?thesis
            by (metis ‹distance_set (Graph.digraph_abs G) (t_set srcs) v < distance_set (Graph.digraph_abs (parents bfs_state')) (t_set srcs) v› ‹distance_set (Graph.digraph_abs G) (t_set srcs) v = distance_set (Graph.digraph_abs G) (t_set srcs) v' + 1› calculation distance_set_neighbourhood leD srcs_invar(1) v'(3))
        next
          case v'_not_in_srcs: False
          have "?dSrcsG v = ?dSrcsG v' + 1"
            using ‹?dSrcsG v = ?dSrcsG v' + 1› .
          also have "... = ?dSrcsT v' + 1"
            text ‹From this current invariant›
            using ‹invar_dist bfs_state› ‹v' ∈ t_set (current bfs_state)› ‹invar_well_formed bfs_state›
              ‹invar_subsets bfs_state› v'_not_in_srcs 
            by (force elim!: invar_well_formed_props invar_subsets_props invar_dist_props)
          also have "... = ?dSrcsT' v' + 1"
          proof-
            have "?dSrcsT v' = ?dSrcsT' v'"
            proof-
              have "?dSrcsT' v' ≤ ?dSrcsT v'"
                using ‹invar_well_formed bfs_state›
                by(fastforce simp: bfs_state'_def BFS_upd1_def Let_def 
                    intro: distance_set_subset elim: invar_props_elims)

              moreover have "?dSrcsG v' ≤ ?dSrcsT' v'"
                using ‹invar_well_formed bfs_state› ‹invar_subsets bfs_state›
                by(fastforce simp: bfs_state'_def BFS_upd1_def Let_def intro: distance_set_subset
                    elim: invar_props_elims)
              moreover have ‹?dSrcsT v' = ?dSrcsG v'›
                using ‹invar_dist bfs_state› ‹v' ∈ t_set (current bfs_state)› ‹invar_well_formed bfs_state›
                  ‹invar_subsets bfs_state› v'_not_in_srcs
                by (force elim!: invar_well_formed_props invar_subsets_props invar_dist_props)
              ultimately show ?thesis
                by auto
            qed
            then show ?thesis
              by auto
          qed
          finally have "?dSrcsG v = ?dSrcsT' v' + 1"
            by auto
          hence "?dSrcsT' v' + 1 < ?dSrcsT' v"
            using ‹?dSrcsG v < ?dSrcsT' v›
            by auto
          moreover have "v ∈ neighbourhood (Graph.digraph_abs (parents bfs_state')) v'"
            using ‹v ∈ neighbourhood (Graph.digraph_abs (parents bfs_state')) v'› .
          hence "?dSrcsT' v ≤ ?dSrcsT' v' + 1"
            by (auto intro!: distance_set_neighbourhood)

          ultimately show False
            text ‹From the triangle ineq›
            by auto
        qed
      qed
    qed
  qed
qed

lemma invar_dist_holds_ret_1[invar_holds_intros]:
  "[BFS_ret_1_conds bfs_state; invar_dist bfs_state] ==> invar_dist (BFS_ret1 bfs_state)"
  by (auto simp: intro: invar_props_intros)

lemma invar_dist_holds[invar_holds_intros]: 
   assumes "BFS_dom bfs_state" "invar_well_formed bfs_state" "invar_subsets bfs_state"
           "invar_3_1 bfs_state" "invar_3_2 bfs_state" "invar_3_3 bfs_state" "invar_dist_bounded bfs_state"
            "invar_dist bfs_state" "invar_current_reachable bfs_state"
   shows "invar_dist (BFS bfs_state)"
  using assms(2-)
proof(induction rule: BFS_induct[OF assms(1)])
  case IH: (1 bfs_state)
  show ?case
    apply(rule BFS_cases[where bfs_state = bfs_state])
    by (auto intro!: IH(2-) intro: invar_holds_intros  simp: BFS_simps[OF IH(1)])
qed

definition "invar_current_no_out bfs_state =
  (∀u∈t_set(current bfs_state).
     ∀v. (u,v) ∉ Graph.digraph_abs (parents bfs_state))"

lemma invar_current_no_out_props[invar_props_elims]: 
  "invar_current_no_out bfs_state ==>
  ([∧u v. u∈t_set(current bfs_state) ==> (u,v) ∉ Graph.digraph_abs (parents bfs_state)] ==> P)
     ==> P"
  by (auto simp: invar_current_no_out_def)

lemma invar_current_no_out_intro[invar_props_intros]:
   "[∧u v. u∈t_set(current bfs_state) ==> (u,v) ∉ Graph.digraph_abs (parents bfs_state)]
     ==> invar_current_no_out bfs_state"
   by (auto simp: invar_current_no_out_def)

lemma invar_current_no_out_holds_upd1[invar_holds_intros]: 
  "[BFS_call_1_conds bfs_state; invar_well_formed bfs_state; invar_subsets bfs_state; invar_current_no_out bfs_state]
     ==> invar_current_no_out (BFS_upd1 bfs_state)"
  apply(auto elim!: call_cond_elims invar_well_formed_props invar_subsets_props intro!: invar_props_intros simp: BFS_upd1_def Let_def)
  apply blast+
  done

lemma invar_current_no_out_holds_ret_1[invar_holds_intros]:
  "[BFS_ret_1_conds bfs_state; invar_current_no_out bfs_state] ==> invar_current_no_out (BFS_ret1 bfs_state)"
  by (auto simp: intro: invar_props_intros)

lemma invar_current_no_out_holds[invar_holds_intros]: 
   assumes "BFS_dom bfs_state" "invar_well_formed bfs_state" "invar_subsets bfs_state" "invar_current_no_out bfs_state"
   shows "invar_current_no_out (BFS bfs_state)"
  using assms(2-)
proof(induction rule: BFS_induct[OF assms(1)])
  case IH: (1 bfs_state)
  show ?case
    apply(rule BFS_cases[where bfs_state = bfs_state])
    by (auto intro!: IH(2-) intro: invar_holds_intros  simp: BFS_simps[OF IH(1)])
qed
 
lemma invar_parents_shortest_paths_props[invar_props_elims]: 
  "invar_parents_shortest_paths bfs_state ==>
  ([∧u p v. [u ∈ t_set srcs; Vwalk.vwalk_bet (Graph.digraph_abs (parents bfs_state)) u p v] ==>
         length p - 1 = distance_set (Graph.digraph_abs G) (t_set srcs) v] ==> P)
     ==> P"
  by (auto simp: invar_parents_shortest_paths_def)

lemma invar_parents_shortest_paths_intro[invar_props_intros]:
  "[∧u p v. [u ∈ t_set srcs; Vwalk.vwalk_bet (Graph.digraph_abs (parents bfs_state)) u p v] ==>
         length p - 1 = distance_set (Graph.digraph_abs G) (t_set srcs) v]
     ==> invar_parents_shortest_paths bfs_state"
  by (auto simp: invar_parents_shortest_paths_def)

lemma invar_parents_shortest_paths_holds_upd1[invar_holds_intros]: 
  "[BFS_call_1_conds bfs_state; invar_well_formed bfs_state; invar_subsets bfs_state; invar_current_no_out bfs_state;
    invar_dist_bounded bfs_state; invar_parents_shortest_paths bfs_state]
     ==> invar_parents_shortest_paths (BFS_upd1 bfs_state)"
proof(intro invar_props_intros, goal_cases)
  case assms: (1 u p v)

  define bfs_state' where "bfs_state' = BFS_upd1 bfs_state"

  have "invar_subsets bfs_state'"
    using assms
    by (auto intro: invar_holds_intros simp: bfs_state'_def)

  hence ?case if "length p ≤ 1"
    using ‹length p ≤ 1› assms(7,8) ‹invar_subsets bfs_state›
    by(cases p) (auto elim!: Vwalk.vwalk_bet_props invar_props_elims dest!: dVs_subset
                      simp: bfs_state'_def[symmetric] zero_enat_def[symmetric])

  have "invar_current_no_out bfs_state'"
    using assms 
    by(auto intro: invar_holds_intros simp: bfs_state'_def)

  have **: "u ∈ t_set (current bfs_state') ∨ v ∈ t_set (current bfs_state')"
    if "(u,v) ∈ (Graph.digraph_abs (parents bfs_state')) -
              (Graph.digraph_abs (parents bfs_state))" for u v
    using ‹invar_well_formed bfs_state› ‹invar_subsets bfs_state› dVsI that
    by(fastforce dest: dVsI simp: bfs_state'_def dVs_def BFS_upd1_def Let_def
               elim!: invar_well_formed_props invar_subsets_props)

  have ?case if "length p > 1" 
  proof-
    have "u ∈ t_set (visited bfs_state) ∪ t_set (current bfs_state)"
    proof(rule ccontr, goal_cases)
      have "u ∈ dVs (Graph.digraph_abs (parents bfs_state'))"
        using assms(8)
        by (auto simp: bfs_state'_def)
      hence "u ∈ t_set (visited bfs_state') ∪ t_set (current bfs_state')"
        using ‹invar_subsets bfs_state'›
        by (auto elim: invar_props_elims)
      moreover case 1
      ultimately have "u ∈ t_set (current bfs_state')"
        using assms
        by(auto simp: Let_def bfs_state'_def BFS_upd1_def elim!: invar_well_formed_props invar_subsets_props)
      moreover obtain u' where "(u,u') ∈ Graph.digraph_abs (parents bfs_state')"
        using ‹length p > 1› assms(8) ‹invar_subsets bfs_state›
        by (auto elim!: Vwalk.vwalk_bet_props 
            simp: eval_nat_numeral Suc_le_length_iff Suc_le_eq[symmetric] bfs_state'_def
            split: if_splits)
      ultimately show ?case
        using ‹invar_current_no_out bfs_state'›
        by (auto elim!: invar_current_no_out_props)
    qed

    show ?thesis
    proof(cases "v ∉ t_set (visited bfs_state) ∪ t_set (current bfs_state)")
      case v_not_visited: True
      show ?thesis
      proof(rule ccontr, goal_cases)
        case 1

        moreover have "vwalk_bet (Graph.digraph_abs G) u p v"
          by (metis ‹invar_subsets bfs_state'› assms(8) bfs_state'_def invar_subsets_props vwalk_bet_subset)

        ultimately have "length p - 1 > distance_set (Graph.digraph_abs G) (t_set srcs) v"
          using ‹u ∈ t_set srcs› 1
          apply auto
          by (metis One_nat_def order_neq_le_trans vwalk_bet_dist_set)

        hence "length p - 2 ≥ distance_set (Graph.digraph_abs G) (t_set srcs) v"
          using ‹length p > 1›  
          apply (auto simp: eval_nat_numeral)
          by (metis leD leI Suc_diff_Suc Suc_ile_eq)
        moreover obtain p' v' where "p = p' @ [v', v]"
          using ‹length p > 1›
          apply (clarsimp
              simp: eval_nat_numeral Suc_le_length_iff Suc_le_eq[symmetric]
              split: if_splits)
          by (metis append.right_neutral append_butlast_last_cancel assms(8) length_Cons
              length_butlast length_tl list.sel(3) list.size(3) nat.simps(3) vwalk_bet_def)
        have "vwalk_bet (Graph.digraph_abs (parents bfs_state)) u (p' @ [v']) v'"
        proof(rule ccontr, goal_cases)
          case 1
          moreover have "vwalk_bet (Graph.digraph_abs (parents (BFS_upd1 bfs_state))) u (p' @ [v']) v'"
            using assms(8) ‹p = p' @ [v', v]›
            by (simp add: vwalk_bet_pref)
          ultimately show ?case
          proof(elim vwalk_bet_not_vwalk_bet_elim_2[OF _ "1"], goal_cases)
            case 1
            then show ?case
              by (metis ‹distance_set (Graph.digraph_abs G) (t_set srcs) v ≤ enat (length p - 2)›
                        ‹p = p' @ [v', v]› ‹vwalk_bet (Graph.digraph_abs G) u p v› assms(3)
                        diff_is_0_eq distance_set_0 invar_subsets_def le_zero_eq length_append_singleton
                        list.sel(3) not_less_eq_eq subset_eq v_not_visited vwalk_bet_endpoints(2) 
                        vwalk_bet_vertex_decompE zero_enat_def)
          next
            case (2 u'' v'')
            moreover hence "u'' ∉ t_set (current bfs_state')"
              using ‹invar_current_no_out bfs_state'› ‹invar_subsets bfs_state'›
              by (auto simp: bfs_state'_def[symmetric] elim: invar_props_elims)
            ultimately have "v'' ∈ t_set (current bfs_state')"
              using ** ‹invar_subsets bfs_state'›
              by (auto simp: bfs_state'_def[symmetric])
            moreover hence no_outgoing_v'': "(v'',u'') ∉ Graph.digraph_abs (parents bfs_state')"
              for u''
              using ‹invar_current_no_out bfs_state'› that 
              by (auto elim: invar_props_elims)
            hence "last (p @ [v']) = v''"
              using that ‹vwalk_bet (Graph.digraph_abs (parents (BFS_upd1 bfs_state))) u (p' @ [v']) v'›[simplified bfs_state'_def[symmetric]]
              apply (clarsimp dest: v_in_edge_in_vwalk elim!: vwalk_bet_props intro!: no_outgoing_last)
               by (metis "2"(2) last_snoc no_outgoing_last v_in_edge_in_vwalk(2))
            hence "v' = v''"
              using that
              by auto
            moreover have "(v',v) ∈ Graph.digraph_abs (parents bfs_state')"
              using ‹p = p' @ [v', v]› assms(8)
              by (fastforce simp: bfs_state'_def [symmetric] dest: split_vwalk)
            ultimately show ?case
              using that no_outgoing_v''
              by auto
          qed
        qed
        hence "length (p' @ [v']) - 1 = distance_set (Graph.digraph_abs G) (t_set srcs) v'"
          using ‹invar_parents_shortest_paths bfs_state› ‹u ∈ t_set srcs›
          by (force elim!: invar_props_elims)
        hence "length p - 2 = distance_set (Graph.digraph_abs G) (t_set srcs) v'" (is "_ = ?dist v'")
          by (auto simp: ‹p = p' @ [v', v]›)
        hence "?dist v ≤ ?dist v'"
          using ‹?dist v ≤ length p - 2› dual_order.trans
          by presburger
        hence "v ∈ t_set (visited bfs_state) ∪ t_set (current bfs_state) "
          using ‹invar_subsets bfs_state› ‹invar_dist_bounded bfs_state› ‹u ∈ t_set srcs›
                ‹vwalk_bet (Graph.digraph_abs (parents bfs_state)) u (p' @ [v']) v'›
          by(blast elim!: invar_props_elims dest!: vwalk_bet_endpoints(2))
        thus ?case
          using v_not_visited
          by auto
      qed
    next
      case v_visited: False

      have "Vwalk.vwalk_bet (Graph.digraph_abs (parents bfs_state)) u p v"
      proof(rule ccontr, goal_cases)
        case 1
        thus ?case
        proof(elim vwalk_bet_not_vwalk_bet_elim_2[OF assms(8)], goal_cases)
          case 1
          then show ?case
            using that by auto
        next
          case (2 u' v')
          moreover hence "u' ∉ t_set (current bfs_state')"
            using ‹invar_current_no_out bfs_state'› ‹invar_subsets bfs_state'›
            by (auto simp: bfs_state'_def[symmetric] elim: invar_props_elims)
          ultimately have "v' ∈ t_set (current bfs_state')"
            using ** ‹invar_subsets bfs_state'›
            by (auto simp: bfs_state'_def[symmetric])
          moreover hence "(v',u') ∉ Graph.digraph_abs (parents bfs_state')" for u'
            using ‹invar_current_no_out bfs_state'›
            by (auto elim: invar_props_elims)
          hence "last p = v'"
            using ‹vwalk_bet (Graph.digraph_abs (parents (BFS_upd1 bfs_state))) u p v›[simplified bfs_state'_def[symmetric]]
              ‹(u',v') ∈ set (edges_of_vwalk p)›
            by (auto dest: v_in_edge_in_vwalk elim!: vwalk_bet_props intro!: no_outgoing_last)
          hence "v' = v"
            using ‹vwalk_bet (Graph.digraph_abs (parents (BFS_upd1 bfs_state))) u p v›
            by auto
          ultimately show ?case
            using v_visited ‹invar_well_formed bfs_state›
            by (auto simp: bfs_state'_def BFS_upd1_def Let_def elim: invar_props_elims)
        qed
      qed
      then show ?thesis
        using ‹invar_parents_shortest_paths bfs_state› ‹u ∈ t_set srcs›
        by (auto elim!: invar_props_elims)
    qed
  qed
  show ?case
    using ‹1 < length p ==> length p - 1 = distance_set (Graph.digraph_abs G) (t_set srcs) v›
          ‹length p ≤ 1 ==> length p - 1 = distance_set (Graph.digraph_abs G) (t_set srcs) v›
    by fastforce
qed

lemma invar_parents_shortest_paths_holds_ret_1[invar_holds_intros]:
  "[BFS_ret_1_conds bfs_state; invar_parents_shortest_paths bfs_state] ==>
     invar_parents_shortest_paths (BFS_ret1 bfs_state)"
  by (auto simp: intro: invar_props_intros)

lemma invar_parents_shortest_paths_holds[invar_holds_intros]: 
   assumes "BFS_dom bfs_state" "invar_well_formed bfs_state" "invar_subsets bfs_state"
           "invar_current_no_out bfs_state" "invar_3_1 bfs_state"
           "invar_3_2 bfs_state" "invar_3_3 bfs_state"
           "invar_dist_bounded bfs_state" "invar_current_reachable bfs_state" 
           "invar_parents_shortest_paths bfs_state"
   shows "invar_parents_shortest_paths (BFS bfs_state)"
  using assms(2-)
proof(induction rule: BFS_induct[OF assms(1)])
  case IH: (1 bfs_state)
  show ?case
    apply(rule BFS_cases[where bfs_state = bfs_state])
    by (auto intro!: IH(2-) intro: invar_holds_intros  simp: BFS_simps[OF IH(1)])
qed

lemma BFS_ret_1[ret_holds_intros]:
  "BFS_ret_1_conds (bfs_state) ==> BFS_ret_1_conds (BFS_ret1 bfs_state)"
  by (auto simp: elim!: call_cond_elims intro!: call_cond_intros)

lemma ret1_holds[ret_holds_intros]:
   assumes "BFS_dom bfs_state" 
   shows "BFS_ret_1_conds (BFS bfs_state)" 
proof(induction  rule: BFS_induct[OF assms(1)])
  case IH: (1 bfs_state)
  show ?case
    apply(rule BFS_cases[where bfs_state = bfs_state])
    by (auto intro: ret_holds_intros intro!: IH(2-)
             simp: BFS_simps[OF IH(1)])
qed

lemma BFS_correct_1_ret_1:
  "[invar_subsets bfs_state; invar_goes_through_current bfs_state; BFS_ret_1_conds bfs_state;
    u ∈ t_set srcs; t ∉ t_set (visited bfs_state)]
         ==> ∄p. vwalk_bet (Graph.digraph_abs G) u p t"
    by (force elim!: call_cond_elims invar_props_elims)

lemma BFS_correct_2_ret_1:
  "[invar_well_formed bfs_state; invar_subsets bfs_state; invar_dist bfs_state; BFS_ret_1_conds bfs_state;
    t ∈ t_set (visited bfs_state) - t_set srcs]
         ==> distance_set (Graph.digraph_abs G) (t_set srcs) t =
         distance_set (Graph.digraph_abs (parents bfs_state)) (t_set srcs) t"
  apply(erule invar_props_elims)+
  by (auto elim!: call_cond_elims invar_props_elims)

lemma BFS_correct_3_ret_1:
  "[invar_parents_shortest_paths bfs_state; BFS_ret_1_conds bfs_state;
    u ∈ t_set srcs; Vwalk.vwalk_bet (Graph.digraph_abs (parents bfs_state)) u p v]
         ==> length p - 1 = distance_set (Graph.digraph_abs G) (t_set srcs) v"
  apply(erule invar_props_elims)+
  by (auto elim!: call_cond_elims invar_props_elims)

subsection ‹Termination›

named_theorems termination_intros

declare termination_intros[intro!]

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)

definition "state_measure_rel call_measure = inv_image less_rel call_measure"

lemma call_1_measure_nonsym[simp]:
  "(call_1_measure_1 BFS_state, call_1_measure_1 BFS_state) ∉ less_rel"
  by (auto simp: less_rel_def)

lemma call_1_terminates[termination_intros]:
  assumes  "BFS_call_1_conds BFS_state" "invar_well_formed BFS_state" "invar_subsets BFS_state"
           "invar_current_no_out BFS_state"
  shows "(BFS_upd1 BFS_state, BFS_state) ∈
           call_1_measure_1 <*mlex*> call_1_measure_2 <*mlex*> r"
proof(cases "t_set (next_frontier (current BFS_state) (visited BFS_state ∪_G current BFS_state)) = {}")
  case True
  hence "t_set (visited (BFS_upd1 BFS_state)) ∪ t_set (current (BFS_upd1 BFS_state)) =
           t_set (visited BFS_state) ∪ t_set (current BFS_state)"
    using ‹invar_well_formed BFS_state›
    by (fastforce simp: BFS_upd1_def Let_def elim!: invar_props_elims)
  hence "call_1_measure_1 (BFS_upd1 BFS_state) = call_1_measure_1 BFS_state"
    by (auto simp: call_1_measure_1_def)
  moreover have "t_set (current (BFS_upd1 BFS_state)) = {}"
    using True
    by (auto simp: BFS_upd1_def Let_def)
  ultimately show ?thesis
    using assms
  by(fastforce elim!: invar_props_elims call_cond_elims
          simp add: call_1_measure_2_def 
          intro!: psubset_card_mono 
          intro: mlex_less)
next
  case False
  have *: "{{v1, v2} |v1 v2. (v1, v2) ∈ [G]_G}
                 ⊆ (λ(x,y). {x,y} ) ` ({v. ∃y. lookup G v = Some y} ×
                                        (∪ {t_set N | v N. lookup G v = Some N}))"
    including Graph.adjmap.automation and Graph.vset.set.automation
    apply (clarsimp simp: Graph.digraph_abs_def Graph.neighb_def image_def
                split: option.splits)
    by (metis Graph.graph_invE Graph.vset.set.set_isin graph_inv(1))
  moreover have "{uu. ∃v N. uu = t_set N ∧ lookup G v = Some N} =
                   ((t_set o the o (lookup G)) ` {v | N v. lookup G v = Some N})"
    by (force simp: image_def)
  hence "finite (∪ {t_set N | v N. lookup G v = Some N})"
    using graph_inv(1,2,3)
    apply(subst (asm) Graph.finite_vsets_def )
    by (auto simp: Graph.finite_graph_def Graph.graph_inv_def
             split: option.splits)
  ultimately have "finite {{v1, v2} |v1 v2. (v1,v2) ∈ [G]_G}"
    using graph_inv(2)
    by (auto simp: Graph.finite_graph_def intro!: finite_subset[OF *])
  moreover have "finite {neighbourhood (Graph.digraph_abs G) u |u. u ∈ t_set (current BFS_state)}"
    using Graph.finite_vsets_def
    by (fastforce simp: ) 
  moreover have "t_set (visited (BFS_upd1 BFS_state)) ∪ t_set (current (BFS_upd1 BFS_state)) ⊆ dVs (Graph.digraph_abs G)"
    using ‹invar_well_formed BFS_state› ‹invar_subsets BFS_state›
    by(auto elim!: invar_props_elims call_cond_elims
          simp add: BFS_upd1_def Let_def dVs_def 
          intro!: mlex_less psubset_card_mono)+
  moreover have "t_set (visited (BFS_upd1 BFS_state)) ∪ t_set (current (BFS_upd1 BFS_state)) ≠
                   t_set (visited BFS_state) ∪ t_set (current BFS_state)"
    using ‹BFS_call_1_conds BFS_state› ‹invar_well_formed BFS_state› ‹invar_subsets BFS_state›
          ‹invar_current_no_out BFS_state› False
    by(fastforce elim!: invar_props_elims call_cond_elims
                 simp add: BFS_upd1_def Let_def dVs_def 
                 intro!: mlex_less psubset_card_mono)

  ultimately have **: "dVs (Graph.digraph_abs G) - (t_set (visited (BFS_upd1 BFS_state)) ∪
                                                      t_set (current (BFS_upd1 BFS_state)))≠
                          dVs (Graph.digraph_abs G) - (t_set (visited BFS_state) ∪ t_set (current BFS_state))"
    using ‹BFS_call_1_conds BFS_state› ‹invar_well_formed BFS_state› ‹invar_subsets BFS_state›
    by(auto elim!: invar_props_elims call_cond_elims
          simp add: BFS_upd1_def Let_def dVs_def
          intro!: mlex_less psubset_card_mono)

  hence "call_1_measure_1 (BFS_upd1 BFS_state) < call_1_measure_1 BFS_state"
    using assms 
  by(auto elim!: invar_props_elims call_cond_elims
          simp add: call_1_measure_1_def BFS_upd1_def Let_def 
          intro!: psubset_card_mono)
  thus ?thesis
    by(auto intro!: mlex_less psubset_card_mono)
qed  

lemma wf_term_rel: "wf BFS_term_rel"
  by(auto simp: wf_mlex BFS_term_rel_def)

lemma in_BFS_term_rel[termination_intros]:
  "[BFS_call_1_conds BFS_state; invar_well_formed BFS_state; invar_subsets BFS_state; invar_current_no_out BFS_state] ==>
            (BFS_upd1 BFS_state, BFS_state) ∈ BFS_term_rel" 
  by (simp add: BFS_term_rel_def termination_intros)+

lemma BFS_terminates[termination_intros]:
  assumes "invar_well_formed BFS_state" "invar_subsets BFS_state" "invar_current_no_out BFS_state"
  shows "BFS_dom BFS_state"
  using wf_term_rel assms
proof(induction rule: wf_induct_rule)
  case (less x)
  show ?case
    apply (rule BFS_domintros)
    by (auto intro: invar_holds_intros intro!: termination_intros less)
qed

lemma not_vwalk_bet_empty[simp]: "¬ Vwalk.vwalk_bet (Graph.digraph_abs empty) u p v"
  using not_vwalk_bet_empty
  by (force simp add: Graph.digraph_abs_def Graph.neighb_def)+

lemma not_edge_in_empty[simp]: "(u,v) ∉ (Graph.digraph_abs empty)"
  by (force simp add: Graph.digraph_abs_def Graph.neighb_def)+

subsection ‹Final Correctness Theorems›

lemma initial_state_props[invar_holds_intros, termination_intros, simp]:
  "invar_well_formed (initial_state)" (is ?g1)
  "invar_subsets (initial_state)" (is ?g2)
  "invar_current_no_out (initial_state)" (is ?g3)
  "BFS_dom initial_state" (is ?g4)
  "invar_dist initial_state" (is ?g5)
  "invar_3_1 initial_state"
  "invar_3_2 initial_state"
  "invar_3_3 initial_state"
  "invar_dist_bounded initial_state"
  "invar_current_reachable initial_state"
  "invar_goes_through_current initial_state"
  "invar_current_no_out initial_state"
  "invar_parents_shortest_paths initial_state"
proof-
  show ?g1
    using graph_inv(3)
    by (fastforce simp: initial_state_def dVs_def Graph.finite_vsets_def
        intro!: invar_props_intros)

  have "t_set (visited initial_state)∪ t_set (current initial_state) ⊆ dVs (Graph.digraph_abs G)"
    using srcs_in_G
    by(simp add: initial_state_def)
  thus ?g2 ?g3
    by(force  simp: initial_state_def dVs_def Graph.digraph_abs_def Graph.neighb_def 
                  intro!: invar_props_intros)+

  show ?g4
    using ‹?g1› ‹?g2› ‹?g3›
    by (auto intro!: termination_intros)

  show ?g5 "invar_3_3 initial_state" "invar_parents_shortest_paths initial_state"
       "invar_current_no_out initial_state"
    by (auto simp add: initial_state_def  intro!: invar_props_intros)

  have *: "distance_set (Graph.digraph_abs G) (t_set srcs) v = 0" if "v ∈ t_set srcs" for v
    using that srcs_in_G
    by (fastforce intro: iffD2[OF distance_set_0[ where G = "(Graph.digraph_abs G)"]])
  moreover have **: "v ∈ t_set srcs" if "distance_set (Graph.digraph_abs G) (t_set srcs) v = 0" for v
    using dist_set_inf i0_ne_infinity that
    by (force intro: iffD1[OF distance_set_0[ where G = "(Graph.digraph_abs G)"]])
  ultimately show "invar_3_1 initial_state" "invar_3_2 initial_state" "invar_dist_bounded initial_state"
                  "invar_current_reachable initial_state"
    using dist_set_inf
    by(auto dest:  dest: simp add: initial_state_def  intro!: invar_props_intros dest!:)

  show "invar_goes_through_current initial_state"
    by (auto simp add: initial_state_def dest:  hd_of_vwalk_bet'' intro!: invar_props_intros)
qed

lemma BFS_correct_1:
  "[u ∈ t_set srcs; t ∉ t_set (visited (BFS initial_state))]
         ==> ∄p. vwalk_bet (Graph.digraph_abs G) u p t"
  apply(intro BFS_correct_1_ret_1[where bfs_state = "BFS initial_state"])
  by(auto intro: invar_holds_intros ret_holds_intros)

lemma BFS_correct_2:
  "[t ∈ t_set (visited (BFS initial_state)) - t_set srcs]
         ==> distance_set (Graph.digraph_abs G) (t_set srcs) t =
         distance_set (Graph.digraph_abs (parents (BFS initial_state))) (t_set srcs) t"
  apply(intro BFS_correct_2_ret_1[where bfs_state = "BFS initial_state"])
  by(auto intro: invar_holds_intros ret_holds_intros)

lemma BFS_correct_3:
  "[u ∈ t_set srcs; Vwalk.vwalk_bet (Graph.digraph_abs (parents (BFS initial_state))) u p v]
         ==> length p - 1 = distance_set (Graph.digraph_abs G) (t_set srcs) v"
  apply(intro BFS_correct_3_ret_1[where bfs_state = "BFS initial_state"])
  by(auto intro: invar_holds_intros ret_holds_intros)

end text ‹context›

end text ‹locale @{const BFS}›
end