Theory Floyd_Warshall

theory Floyd_Warshall
imports Main
(* Author: Wimmer *)
theory Floyd_Warshall
  imports Main
begin

chapter ‹Floyd-Warshall Algorithm for the All-Pairs Shortest Paths Problem›

section ‹Introduction›
text ‹
  The \fw @{cite floyd and roy and warshall} is a classic dynamic programming algorithm to compute
  the length of all shortest paths between any two vertices in a graph
  (i.e. to solve the all-pairs shortest path problem, or ‹APSP› for short).
  Given a representation of the graph as a matrix of weights ‹M›, it computes another matrix ‹M'›
  which represents a graph with the same path lengths and contains the length of the shortest path
  between any two vertices ‹i› and ‹j›.
  This is only possible if the graph does not contain any negative cycles (then the length
  of the shortest path is ‹-∞›). However, in this case the \fw will detect the situation by
  calculating a negative diagonal entry corresponding to the negative cycle.
  In the following, we present a formalization of the algorithm and of the aforementioned
  key properties.

  Abstractly, the algorithm corresponds to the following imperative pseudo-code:
  ▩‹
  for k = 1 .. n do
    for i = 1 .. n do
      for j = 1 .. n do
        m[i, j] := min(m[i, j], m[i, k] + m[k, j])
  ›

  However, we will carry out the whole formalization on a recursive version of the algorithm, and
  refine it to an efficient imperative version corresponding to the above pseudo-code in the end.
  The main observation underlying the algorithm is that the shortest path from ‹i› to ‹j› which only
  uses intermediate vertices from the set ‹{0…k+1}›, is: either the shortest path from ‹i› to ‹j›
  using intermediate vertices from the set ‹{0…k}›;
  or a combination of the shortest path from ‹i› to ‹k› and the shortest path from ‹k› to ‹j›,
  each of them only using intermediate vertices from ‹{0…k}›.
  Our presentation we be slightly more general than the typical textbook version, in that we will
  factor our the inner two loops as a separate algorithm and show that it has similar properties
  as the full algorithm for a single intermediate vertex ‹k›.
›


section ‹Preliminaries›

subsection ‹Cycles in Lists›

abbreviation "cnt x xs ≡ length (filter (λy. x = y) xs)"

fun remove_cycles :: "'a list ⇒ 'a ⇒ 'a list ⇒ 'a list"
where
  "remove_cycles [] _ acc = rev acc" |
  "remove_cycles (x#xs) y acc =
    (if x = y then remove_cycles xs y [x] else remove_cycles xs y (x#acc))"

lemma cnt_rev: "cnt x (rev xs) = cnt x xs" by (metis length_rev rev_filter)

value "as @ [x] @ bs @ [x] @ cs @ [x] @ ds"

lemma remove_cycles_removes: "cnt x (remove_cycles xs x ys) ≤ max 1 (cnt x ys)"
proof (induction xs arbitrary: ys)
  case Nil thus ?case
  by (simp, cases "x ∈ set ys", (auto simp: cnt_rev[of x ys]))
next
  case (Cons y xs)
  thus ?case
  proof (cases "x = y")
    case True
    thus ?thesis using Cons[of "[y]"] True by auto
  next
    case False
    thus ?thesis using Cons[of "y # ys"] by auto
  qed
qed

lemma remove_cycles_id: "x ∉ set xs ⟹ remove_cycles xs x ys = rev ys @ xs"
by (induction xs arbitrary: ys) auto

lemma remove_cycles_cnt_id:
  "x ≠ y ⟹ cnt y (remove_cycles xs x ys) ≤ cnt y ys + cnt y xs"
proof (induction xs arbitrary: ys x)
  case Nil thus ?case by (simp add: cnt_rev)
next
  case (Cons z xs)
  thus ?case
  proof (cases "x = z")
    case True thus ?thesis using Cons.IH[of z "[z]"] Cons.prems by auto
  next
    case False
    thus ?thesis using Cons.IH[of x "z # ys"] Cons.prems False by auto
  qed
qed

lemma remove_cycles_ends_cycle: "remove_cycles xs x ys ≠ rev ys @ xs ⟹ x ∈ set xs"
using remove_cycles_id by fastforce

lemma remove_cycles_begins_with: "x ∈ set xs ⟹ ∃ zs. remove_cycles xs x ys = x # zs ∧ x ∉ set zs"
proof (induction xs arbitrary: ys)
  case Nil thus ?case by auto
next
  case (Cons y xs)
  thus ?case
  proof (cases "x = y")
    case True thus ?thesis
    proof (cases "x ∈ set xs", goal_cases)
      case 1 with Cons show ?case by auto
    next
      case 2 with remove_cycles_id[of x xs "[y]"] show ?case by auto
    qed
  next
    case False
    with Cons show ?thesis by auto
  qed
qed

lemma remove_cycles_self:
  "x ∈ set xs ⟹ remove_cycles (remove_cycles xs x ys) x zs = remove_cycles xs x ys"
proof -
  assume x:"x ∈ set xs"
  then obtain ws where ws: "remove_cycles xs x ys = x # ws" "x ∉ set ws"
  using remove_cycles_begins_with[OF x, of ys] by blast
  from remove_cycles_id[OF this(2)] have "remove_cycles ws x [x] = x # ws" by auto
  with ws(1) show "remove_cycles (remove_cycles xs x ys) x zs = remove_cycles xs x ys" by simp
qed

lemma remove_cycles_one: "remove_cycles (as @ x # xs) x ys = remove_cycles (x#xs) x ys"
by (induction as arbitrary: ys) auto

lemma remove_cycles_cycles:
  "∃ xxs as. as @ concat (map (λ xs. x # xs) xxs) @ remove_cycles xs x ys = xs ∧ x ∉ set as"
  if "x ∈ set xs"
using that proof (induction xs arbitrary: ys)
  case Nil thus ?case by auto
next
  case (Cons y xs)
  thus ?case
  proof (cases "x = y")
    case True thus ?thesis
    proof (cases "x ∈ set xs", goal_cases)
      case 1
      then obtain as xxs where "as @ concat (map (λxs. y#xs) xxs) @ remove_cycles xs y [y] = xs"
      using Cons.IH[of "[y]"] by auto
      hence "[] @ concat (map (λxs. x#xs) (as#xxs)) @ remove_cycles (y#xs) x ys = y # xs"
      by (simp add: ‹x = y›)
      thus ?thesis by fastforce
    next
      case 2
      hence "remove_cycles (y # xs) x ys = y # xs" using remove_cycles_id[of x xs "[y]"] by auto
      hence "[] @ concat (map (λxs. x # xs) []) @ remove_cycles (y#xs) x ys = y # xs" by auto
      thus ?thesis by fastforce
    qed
  next
    case False
    then obtain as xxs where as:
      "as @ concat (map (λxs. x # xs) xxs) @ remove_cycles xs x (y#ys) = xs" "x ∉ set as"
    using Cons.IH[of "y # ys"] Cons.prems by auto
    hence "(y # as) @ concat (map (λxs. x # xs) xxs) @ remove_cycles (y#xs) x ys = y # xs"
    using ‹x ≠ y› by auto
    thus ?thesis using as(2) ‹x ≠ y› by fastforce
  qed
qed

fun start_remove :: "'a list ⇒ 'a ⇒ 'a list ⇒ 'a list"
where
  "start_remove [] _ acc = rev acc" |
  "start_remove (x#xs) y acc =
    (if x = y then rev acc @ remove_cycles xs y [y] else start_remove xs y (x # acc))"

lemma start_remove_decomp:
  "x ∈ set xs ⟹ ∃ as bs. xs = as @ x # bs ∧ start_remove xs x ys = rev ys @ as @ remove_cycles bs x [x]"
proof (induction xs arbitrary: ys)
  case Nil thus ?case by auto
next
  case (Cons y xs)
  thus ?case
  proof (auto, goal_cases)
    case 1
    from 1(1)[of "y # ys"]
    obtain as bs where
      "xs = as @ x # bs" "start_remove xs x (y # ys) = rev (y # ys) @ as @ remove_cycles bs x [x]"
    by blast
    hence "y # xs = (y # as) @ x # bs"
          "start_remove xs x (y # ys) = rev ys @ (y # as) @ remove_cycles bs x [x]" by simp+
    thus ?case by blast
  qed
qed

lemma start_remove_removes: "cnt x (start_remove xs x ys) ≤ Suc (cnt x ys)"
proof (induction xs arbitrary: ys)
  case Nil thus ?case using cnt_rev[of x ys] by auto
next
  case (Cons y xs)
  thus ?case
  proof (cases "x = y")
    case True
    thus ?thesis using remove_cycles_removes[of y xs "[y]"] cnt_rev[of y ys] by auto
  next
    case False
    thus ?thesis using Cons[of "y # ys"] by auto
  qed
qed

lemma start_remove_id[simp]: "x ∉ set xs ⟹ start_remove xs x ys = rev ys @ xs"
by (induction xs arbitrary: ys) auto

lemma start_remove_cnt_id:
  "x ≠ y ⟹ cnt y (start_remove xs x ys) ≤ cnt y ys + cnt y xs"
proof (induction xs arbitrary: ys)
  case Nil thus ?case by (simp add: cnt_rev)
next
  case (Cons z xs)
  thus ?case
  proof (cases "x = z", goal_cases)
    case 1 thus ?case using remove_cycles_cnt_id[of x y xs "[x]"] by (simp add: cnt_rev)
  next
    case 2 from this(1)[of "(z # ys)"] this(2,3) show ?case by auto
  qed
qed

fun remove_all_cycles :: "'a list ⇒ 'a list ⇒ 'a list"
where
  "remove_all_cycles [] xs = xs" |
  "remove_all_cycles (x # xs) ys = remove_all_cycles xs (start_remove ys x [])"

lemma cnt_remove_all_mono:"cnt y (remove_all_cycles xs ys) ≤ max 1 (cnt y ys)"
proof (induction xs arbitrary: ys)
  case Nil thus ?case by auto
next
  case (Cons x xs)
  thus ?case
  proof (cases "x = y")
    case True thus ?thesis using start_remove_removes[of y ys "[]"] Cons[of "start_remove ys y []"]
    by auto
  next
    case False
    hence "cnt y (start_remove ys x []) ≤ cnt y ys"
    using start_remove_cnt_id[of x y ys "[]"] by auto
    thus ?thesis using Cons[of "start_remove ys x []"] by auto
  qed
qed


lemma cnt_remove_all_cycles: "x ∈ set xs ⟹ cnt x (remove_all_cycles xs ys) ≤ 1"
proof (induction xs arbitrary: ys)
  case Nil thus ?case by auto
next
  case (Cons y xs)
  thus ?case
  using start_remove_removes[of x ys "[]"] cnt_remove_all_mono[of y xs "start_remove ys y []"]
  by auto
qed

lemma cnt_mono:
  "cnt a (b # xs) ≤ cnt a (b # c # xs)"
by (induction xs) auto

lemma cnt_distinct_intro: "∀ x ∈ set xs. cnt x xs ≤ 1 ⟹ distinct xs"
proof (induction xs)
  case Nil thus ?case by auto
next
  case (Cons x xs)
  from this(2) have "∀ x ∈ set xs. cnt x xs ≤ 1"
  by (metis filter.simps(2) impossible_Cons linorder_class.linear list.set_intros(2)
      preorder_class.order_trans)
  with Cons.IH have "distinct xs" by auto
  moreover have "x ∉ set xs" using Cons.prems
  proof (induction xs)
    case Nil then show ?case by auto
  next
    case (Cons a xs)
    from this(2) have "∀xa∈set (x # xs). cnt xa (x # a # xs) ≤ 1"
    by auto
    then have *: "∀xa∈set (x # xs). cnt xa (x # xs) ≤ 1"
    proof (safe, goal_cases)
      case (1 b)
      then have "cnt b (x # a # xs) ≤ 1" by auto
      with cnt_mono[of b x xs a] show ?case by fastforce
    qed
    with Cons(1) have "x ∉ set xs" by auto
    moreover have "x ≠ a"
    by (metis (full_types) Cons.prems One_nat_def * empty_iff filter.simps(2) impossible_Cons
                           le_0_eq le_Suc_eq length_0_conv list.set(1) list.set_intros(1))
    ultimately show ?case by auto
  qed
  ultimately show ?case by auto
qed

lemma remove_cycles_subs:
  "set (remove_cycles xs x ys) ⊆ set xs ∪ set ys"
by (induction xs arbitrary: ys; auto; fastforce)

lemma start_remove_subs:
  "set (start_remove xs x ys) ⊆ set xs ∪ set ys"
using remove_cycles_subs by (induction xs arbitrary: ys; auto; fastforce)

lemma remove_all_cycles_subs:
  "set (remove_all_cycles xs ys) ⊆ set ys"
using start_remove_subs by (induction xs arbitrary: ys, auto) (fastforce+)

lemma remove_all_cycles_distinct: "set ys ⊆ set xs ⟹ distinct (remove_all_cycles xs ys)"
proof -
  assume "set ys ⊆ set xs"
  hence "∀ x ∈ set ys. cnt x (remove_all_cycles xs ys) ≤ 1" using cnt_remove_all_cycles
    by fastforce
  hence "∀ x ∈ set (remove_all_cycles xs ys). cnt x (remove_all_cycles xs ys) ≤ 1"
  using remove_all_cycles_subs by fastforce
  thus "distinct (remove_all_cycles xs ys)" using cnt_distinct_intro by auto
qed

lemma distinct_remove_cycles_inv: "distinct (xs @ ys) ⟹ distinct (remove_cycles xs x ys)"
proof (induction xs arbitrary: ys)
  case Nil thus ?case by auto
next
  case (Cons y xs)
  thus ?case by auto
qed

definition
  "remove_all x xs = (if x ∈ set xs then tl (remove_cycles xs x []) else xs)"

definition
  "remove_all_rev x xs = (if x ∈ set xs then rev (tl (remove_cycles (rev xs) x [])) else xs)"

lemma remove_all_distinct:
  "distinct xs ⟹ distinct (x # remove_all x xs)"
proof (cases "x ∈ set xs", goal_cases)
  case 1
  from remove_cycles_begins_with[OF 1(2), of "[]"] obtain zs
  where "remove_cycles xs x [] = x # zs" "x ∉ set zs" by auto
  thus ?thesis using 1(1) distinct_remove_cycles_inv[of "xs" "[]" x] by (simp add: remove_all_def)
next
  case 2 thus ?thesis by (simp add: remove_all_def)
qed

lemma remove_all_removes:
  "x ∉ set (remove_all x xs)"
by (metis list.sel(3) remove_all_def remove_cycles_begins_with)

lemma remove_all_subs:
  "set (remove_all x xs) ⊆ set xs"
using remove_cycles_subs remove_all_def
by (metis (no_types, lifting) append_Nil2 list.sel(2) list.set_sel(2) set_append subsetCE subsetI)

lemma remove_all_rev_distinct: "distinct xs ⟹ distinct (x # remove_all_rev x xs)"
proof (cases "x ∈ set xs", goal_cases)
  case 1
  then have "x ∈ set (rev xs)" by auto
  from remove_cycles_begins_with[OF this, of "[]"] obtain zs
  where "remove_cycles (rev xs) x [] = x # zs" "x ∉ set zs" by auto
  thus ?thesis using 1(1) distinct_remove_cycles_inv[of "rev xs" "[]" x]
    by (simp add: remove_all_rev_def)
next
  case 2 thus ?thesis by (simp add: remove_all_rev_def)
qed

lemma remove_all_rev_removes: "x ∉ set (remove_all_rev x xs)"
by (metis remove_all_def remove_all_removes remove_all_rev_def set_rev)

lemma remove_all_rev_subs: "set (remove_all_rev x xs) ⊆ set xs"
by (metis remove_all_def remove_all_subs set_rev remove_all_rev_def)

abbreviation "rem_cycles i j xs ≡ remove_all i (remove_all_rev j (remove_all_cycles xs xs))"

lemma rem_cycles_distinct': "i ≠ j ⟹ distinct (i # j # rem_cycles i j xs)"
proof -
  assume "i ≠ j"
  have "distinct (remove_all_cycles xs xs)" by (simp add: remove_all_cycles_distinct)
  from remove_all_rev_distinct[OF this] have
    "distinct (remove_all_rev j (remove_all_cycles xs xs))"
  by simp
  from remove_all_distinct[OF this] have "distinct (i # rem_cycles i j xs)" by simp
  moreover have
    "j ∉ set (rem_cycles i j xs)"
  using remove_all_subs remove_all_rev_removes remove_all_removes by fastforce
  ultimately show ?thesis by (simp add: ‹i ≠ j›)
qed

lemma rem_cycles_removes_last: "j ∉ set (rem_cycles i j xs)"
by (meson remove_all_rev_removes remove_all_subs set_rev_mp)

lemma rem_cycles_distinct: "distinct (rem_cycles i j xs)"
by (meson distinct.simps(2) order_refl remove_all_cycles_distinct
          remove_all_distinct remove_all_rev_distinct)

lemma rem_cycles_subs: "set (rem_cycles i j xs) ⊆ set xs"
by (meson order_trans remove_all_cycles_subs remove_all_subs remove_all_rev_subs)


section ‹Definition of the Algorithm›

subsection ‹Definitions›

text ‹
  In our formalization of the \fw, edge weights are from a linearly ordered abelian monoid.
›

class linordered_ab_monoid_add = linorder + ordered_comm_monoid_add
begin

subclass linordered_ab_semigroup_add ..

end

subclass (in linordered_ab_group_add) linordered_ab_monoid_add ..


context linordered_ab_monoid_add
begin

type_synonym 'c mat = "nat ⇒ nat ⇒ 'c"

definition upd :: "'c mat ⇒ nat ⇒ nat ⇒ 'c ⇒ 'c mat"
where
  "upd m x y v = m (x := (m x) (y := v))"

definition fw_upd :: "'a mat ⇒ nat ⇒ nat ⇒ nat ⇒ 'a mat" where
  "fw_upd m k i j ≡ upd m i j (min (m i j) (m i k + m k j))"

text ‹Recursive version of the two inner loops.›
fun fwi :: "'a mat ⇒ nat ⇒ nat ⇒ nat ⇒ nat ⇒ 'a mat" where
  "fwi m n k 0       0        = fw_upd m k 0 0" |
  "fwi m n k (Suc i) 0        = fw_upd (fwi m n k i n) k (Suc i) 0" |
  "fwi m n k i       (Suc j)  = fw_upd (fwi m n k i j) k i (Suc j)"

text ‹Recursive version of the full algorithm.›
fun fw :: "'a mat ⇒ nat ⇒ nat ⇒ 'a mat" where
  "fw m n 0       = fwi m n 0 n n" |
  "fw m n (Suc k) = fwi (fw m n k) n (Suc k) n n"


subsection ‹Elementary Properties›

lemma fw_upd_mono:
  "fw_upd m k i j i' j' ≤ m i' j'"
by (cases "i = i'", cases "j = j'") (auto simp: fw_upd_def upd_def)

lemma fw_upd_out_of_bounds1:
  assumes "i' > i"
  shows "(fw_upd M k i j) i' j' = M i' j'"
using assms unfolding fw_upd_def upd_def by (auto split: split_min)

lemma fw_upd_out_of_bounds2:
  assumes "j' > j"
  shows "(fw_upd M k i j) i' j' = M i' j'"
using assms unfolding fw_upd_def upd_def by (auto split: split_min)

lemma fwi_out_of_bounds1:
  assumes "i' > n" "i ≤ n"
  shows "(fwi M n k i j) i' j' = M i' j'"
  using assms
  apply (induction _ "(i, j)" arbitrary: i j rule: wf_induct[of "less_than <*lex*> less_than"])
   apply (auto; fail)
  subgoal for i j
    by (cases i; cases j; auto simp add: fw_upd_out_of_bounds1)
  done

lemma fw_out_of_bounds1:
  assumes "i' > n"
  shows "(fw M n k) i' j' = M i' j'"
  using assms by (induction k; simp add: fwi_out_of_bounds1)

lemma fwi_out_of_bounds2:
  assumes "j' > n" "j ≤ n"
  shows "(fwi M n k i j) i' j' = M i' j'"
using assms
 apply (induction _ "(i, j)" arbitrary: i j rule: wf_induct[of "less_than <*lex*> less_than"])
 apply (auto; fail)
 subgoal for i j
 by (cases i; cases j; auto simp add: fw_upd_out_of_bounds2)
  done

lemma fw_out_of_bounds2:
  assumes "j' > n"
  shows "(fw M n k) i' j' = M i' j'"
  using assms by (induction k; simp add: fwi_out_of_bounds2)

lemma fwi_invariant_aux_1:
  "j'' ≤ j ⟹ fwi m n k i j i' j' ≤ fwi m n k i j'' i' j'"
proof (induction j)
  case 0 thus ?case by simp
next
  case (Suc j) thus ?case
  proof (cases "j'' = Suc j")
    case True thus ?thesis by simp
  next
    case False
    have "fw_upd (fwi m n k i j) k i (Suc j) i' j' ≤ fwi m n k i j i' j'"
      by (simp add: fw_upd_mono)
    thus ?thesis using Suc False by simp
  qed
qed

lemma fwi_invariant:
  "j ≤ n ⟹ i'' ≤ i ⟹ j'' ≤ j
   ⟹ fwi m n k i j i' j' ≤ fwi m n k i'' j'' i' j'"
proof (induction i)
  case 0 thus ?case using fwi_invariant_aux_1 by auto
next
  case (Suc i) thus ?case
  proof (cases "i'' = Suc i")
    case True thus ?thesis using Suc fwi_invariant_aux_1 by simp
  next
    case False
    have "fwi m n k (Suc i) j i' j' ≤ fwi m n k (Suc i) 0 i' j'"
      by (rule fwi_invariant_aux_1[of 0]; simp)
    also have "… ≤ fwi m n k i n i' j'" by (simp add: fw_upd_mono)
    also have "… ≤ fwi m n k i j i' j'" using fwi_invariant_aux_1 False Suc by simp
    also have "… ≤ fwi m n k i'' j'' i' j'" using Suc False by simp
    finally show ?thesis by simp
  qed
qed

lemma single_row_inv:
  "j' < j ⟹ fwi m n k i' j i' j' = fwi m n k i' j' i' j'"
proof (induction j)
  case 0 thus ?case by simp
next
  case (Suc j) thus ?case by (cases "j' = j") (simp add: fw_upd_def upd_def)+
qed

lemma single_iteration_inv':
  "i' < i ⟹ j' ≤ n ⟹ fwi m n k i j i' j' = fwi m n k i' j' i' j'"
proof (induction i arbitrary: j)
  case 0 thus ?case by simp
next
  case (Suc i) thus ?case
  proof (induction j)
    case 0 thus ?case
    proof (cases "i = i'", goal_cases)
      case 2 thus ?case by (simp add: fw_upd_def upd_def)
    next
      case 1 thus ?case using single_row_inv[of j' n]
      by (cases "j' = n") (fastforce simp add: fw_upd_def upd_def)+
    qed
  next
    case (Suc j) thus ?case by (simp add: fw_upd_def upd_def)
  qed
qed

lemma single_iteration_inv:
  "i' ≤ i ⟹ j' ≤ j ⟹ j ≤ n ⟹ fwi m n k i j i' j' = fwi m n k i' j' i' j'"
proof (induction i arbitrary: j)
  case 0 thus ?case
  proof (induction j)
    case 0 thus ?case by simp
  next
    case (Suc j) thus ?case using 0 by (cases "j' = Suc j") (simp add: fw_upd_def upd_def)+
  qed
next
  case (Suc i) thus ?case
  proof (induction j)
    case 0 thus ?case by (cases "i' = Suc i") (simp add: fw_upd_def upd_def)+
  next
    case (Suc j) thus ?case
    proof (cases "i' = Suc i", goal_cases)
      case 1 thus ?case
      proof (cases "j' = Suc j", goal_cases)
        case 1 thus ?case by simp
      next
        case 2 thus ?case by (simp add: fw_upd_def upd_def)
      qed
    next
      case 2 thus ?case
      proof (cases "j' = Suc j", goal_cases)
        case 1 thus ?case by - (rule single_iteration_inv'; simp)
      next
        case 2 thus ?case by (simp add: fw_upd_def upd_def)
      qed
    qed
  qed
qed

lemma fwi_innermost_id:
  "i' < i ⟹ fwi m n k i' j' i j = m i j"
proof (induction i' arbitrary: j')
  case 0 thus ?case
  proof (induction j')
    case 0 thus ?case by (simp add: fw_upd_def upd_def)
  next
    case (Suc j') thus ?case by (auto simp: fw_upd_def upd_def)
  qed
next
  case (Suc i') thus ?case
  proof (induction j')
    case 0 thus ?case by (auto simp add: fw_upd_def upd_def)
  next
    case (Suc j') thus ?case by (auto simp add: fw_upd_def upd_def)
  qed
qed

lemma fwi_middle_id:
  "j' < j ⟹ i' ≤ i ⟹ fwi m n k i' j' i j = m i j"
proof (induction i' arbitrary: j')
  case 0 thus ?case
  proof (induction j')
    case 0 thus ?case by (simp add: fw_upd_def upd_def)
  next
    case (Suc j') thus ?case by (auto simp: fw_upd_def upd_def)
  qed
next
  case (Suc i') thus ?case
  proof (induction j')
    case 0 thus ?case using fwi_innermost_id by (auto simp add: fw_upd_def upd_def)
  next
    case (Suc j') thus ?case by (auto simp add: fw_upd_def upd_def)
  qed
qed

lemma fwi_outermost_mono:
  "i ≤ n ⟹ j ≤ n ⟹ fwi m n k i j i j ≤ m i j"
proof (cases j)
  case 0
  assume "i ≤ n"
  thus ?thesis
  proof (cases i)
    case 0 thus ?thesis using ‹j = 0› by (simp add: fw_upd_def upd_def)
  next
    case (Suc i')
    hence "fwi m n k i' n (Suc i') 0 = m (Suc i') 0" using fwi_innermost_id ‹i ≤ n› by simp
    thus ?thesis using ‹j = 0› Suc by (simp add: fw_upd_def upd_def)
  qed
next
  case (Suc j')
  assume "i ≤ n" "j ≤ n"
  hence "fwi m n k i j' i (Suc j') = m i (Suc j')"
  using fwi_middle_id Suc by simp
  thus ?thesis using Suc by (simp add: fw_upd_def upd_def)
qed

lemma fwi_mono:
  "fwi m n k i' j' i j ≤ m i j" if "i ≤ n" "j ≤ n"
proof (cases "i' < i")
  case True
  then have "fwi m n k i' j' i j = m i j"
    by (simp add: fwi_innermost_id)
  then show ?thesis by simp
next
  case False
  show ?thesis
  proof (cases "i' > i")
    case True
    then have "fwi m n k i' j' i j = fwi m n k i j i j"
      by (simp add: single_iteration_inv' that(2))
    with fwi_outermost_mono[OF that] show ?thesis by simp
  next
    case False
    with ‹¬ i' < i› have [simp]: "i' = i" by simp
    show ?thesis
    proof (cases "j' < j")
      case True
      then have "fwi m n k i' j' i j = m i j"
        by (simp add: fwi_middle_id)
      then show ?thesis by simp
    next
      case False
      then have "fwi m n k i' j' i j = fwi m n k i j i j"
        by (cases "j' = j"; simp add: single_row_inv)
      with fwi_outermost_mono[OF that] show ?thesis by simp
    qed
  qed
qed

lemma Suc_innermost_mono:
  "i ≤ n ⟹ j ≤ n ⟹ fw m n (Suc k) i j ≤ fw m n k i j"
  by (simp add: fwi_mono)

lemma fw_mono:
  "i ≤ n ⟹ j ≤ n ⟹ fw m n k i j ≤ m i j"
proof (induction k)
  case 0 thus ?case using fwi_mono by simp
next
  case (Suc k) thus ?case using Suc_innermost_mono[OF Suc.prems, of m k] by simp
qed

text ‹
  Justifies the use of destructive updates in the case that there is no negative cycle for ‹k›.
›
lemma fwi_step:
  "m k k ≥ 0 ⟹ i ≤ n ⟹ j ≤ n ⟹ k ≤ n ⟹ fwi m n k i j i j = min (m i j) (m i k + m k j)"
proof (induction _ "(i, j)" arbitrary: i j rule: wf_induct[of "less_than <*lex*> less_than"],
      (auto; fail), goal_cases)
  case (1 i' j')
  note assms = 1(2-)
  note IH = 1(1)
  note [simp] = fwi_innermost_id fwi_middle_id
  note simps = add_increasing add_increasing2 ord.min_def fw_upd_def upd_def
  show ?case
  proof (cases i')
    case [simp]: 0 thus ?thesis
    proof (cases j')
      case 0 thus ?thesis by (simp add: fw_upd_def upd_def)
    next
      case (Suc j)
      hence "fwi m n k 0 j 0 (Suc j) = m 0 (Suc j)" by simp
      moreover have "fwi m n k 0 j k (Suc j) = m k (Suc j)" by simp
      moreover have "fwi m n k 0 j 0 k = m 0 k"
      proof (cases "j < k")
        case True
        then show ?thesis by simp
      next
        case False
        then show ?thesis
          apply (subst single_iteration_inv; simp)
          subgoal
            using assms Suc by auto
          using assms by (cases k; simp add: simps)
      qed
      ultimately show ?thesis using Suc assms by (simp add: fw_upd_def upd_def)
    qed
  next
    case [simp]: (Suc i)
    show ?thesis
    proof (cases j')
      case 0
      have "fwi m n k i n (Suc i) 0 = m (Suc i) 0" by simp
      moreover have "fwi m n k i n (Suc i) k = m (Suc i) k" by simp
      moreover have "fwi m n k i n k 0 = m k 0"
      proof (cases "i < k")
        case True
        then show ?thesis by simp
      next
        case False
        then show ?thesis
          apply (subst single_iteration_inv; simp)
          using 0 ‹m k k ≥ _› by (cases k; simp add: simps)
      qed
      ultimately show ?thesis using 0 by (simp add: fw_upd_def upd_def)
    next
      case Suc_j: (Suc j)
      from ‹j' ≤ n› ‹j' = _› have [simp]: "j ≤ n" "Suc j ≤ n" by simp+
      have diag: "fwi m n k k k k k = m k k" if "k ≤ i"
      proof -
        from that IH assms have "fwi m n k k k k k = min (m k k) (m k k + m k k)" by auto
        with ‹m k k ≥ 0› ‹k ≤ n› show ?thesis by (simp add: simps)
      qed
      have **: "fwi m n k i n k k = m k k"
      proof (cases "i < k")
        case True
        then show ?thesis by simp
      next
        case False
        then show ?thesis
          by (subst single_iteration_inv; simp add: diag ‹k ≤ n›)
      qed
      have diag2: "fwi m n k k j k k = m k k" if "k ≤ i"
      proof (cases "j < k")
        case True
        then show ?thesis by simp
      next
        case False
        with ‹k ≤ i› show ?thesis
          by (subst single_iteration_inv; simp add: diag)
      qed
      have ***: "fwi m n k (Suc i) j k (Suc j) = m k (Suc j)"
      proof (cases "Suc i ≤ k")
        case True
        then show ?thesis by simp
      next
        case False
        then have "fwi m n k k j k (Suc j) = m k (Suc j)"
          by simp
        with False ‹m k k ≥ 0› show ?thesis
          by (subst single_iteration_inv'; simp add: simps diag2)
      qed
      have "fwi m n k (Suc i) j (Suc i) k = m (Suc i) k"
      proof (cases "j < k")
        case True thus ?thesis by simp
      next
        case False
        then show ?thesis
          apply (subst single_iteration_inv; simp)
          apply (cases k)
          subgoal premises prems
          proof -
            have "fwi m n 0 i n 0 0 ≥ 0"
              using ** assms(1) prems(2) by force
            moreover have "fwi m n 0 i n (Suc i) 0 = m (Suc i) 0"
              by simp
            ultimately show ?thesis
              using prems by (simp add: simps)
          qed
          subgoal premises prems for k'
          proof -
            have "fwi m n (Suc k') (Suc i) k' (Suc k') (Suc k') ≥ 0"
              by (metis ** assms(1,4) fwi_innermost_id fwi_middle_id le_SucE lessI
                    linorder_class.not_le_imp_less prems(2) preorder_class.order_refl
                    single_iteration_inv single_iteration_inv'
                 )
            with prems show ?thesis
              by (simp add: simps)
          qed
          done
      qed
      moreover have "fwi m n k (Suc i) j (Suc i) (Suc j) = m (Suc i) (Suc j)" by simp
      ultimately show ?thesis using ‹j' = _› by (simp add: simps ***)
    qed
  qed
qed


section ‹Result Under The Absence of Negative Cycles›

text ‹
  If the given input graph does not contain any negative cycles, the \fw computes the
  unique› shortest paths matrix corresponding to the graph. It contains the shortest path
  between any two nodes ‹i, j ≤ n›.
›


subsection ‹Length of Paths›

fun len :: "'a mat ⇒ nat ⇒ nat ⇒ nat list ⇒ 'a" where
  "len m u v [] = m u v" |
  "len m u v (w#ws) = m u w + len m w v ws"

lemma len_decomp: "xs = ys @ y # zs ⟹ len m x z xs = len m x y ys + len m y z zs"
by (induction ys arbitrary: x xs) (simp add: add.assoc)+

lemma len_comp: "len m a c (xs @ b # ys) = len m a b xs + len m b c ys"
by (induction xs arbitrary: a) (auto simp: add.assoc)


subsection ‹Canonicality›

text ‹
  The unique shortest path matrices are in a so-called ‹canonical form›.
  We will say that a matrix ‹m› is in canonical form for a set of indices ‹I›
  if the following holds:
›

definition canonical_subs :: "nat ⇒ nat set ⇒ 'a mat ⇒ bool" where
  "canonical_subs n I m = (∀ i j k. i ≤ n ∧ k ≤ n ∧ j ∈ I ⟶ m i k ≤ m i j + m j k)"

text ‹
  Similarly we express that ‹m› does not contain a negative cycle which only uses intermediate
  vertices from the set ‹I› as follows:
›
abbreviation cyc_free_subs :: "nat ⇒ nat set ⇒ 'a mat ⇒ bool" where
  "cyc_free_subs n I m ≡ ∀ i xs. i ≤ n ∧ set xs ⊆ I ⟶ len m i i xs ≥ 0"

text ‹
  To prove the main result under ‹the absence of negative cycles›, we will proceed as follows:
  ▪ we show that an invocation of ‹fwi m n k n n› extends canonicality to index ‹k›,
  ▪ we show that an invocation of ‹fw m n n› computes a matrix in canonical form,
  ▪ and finally we show that canonical forms specify the lengths of ‹shortest paths›,
    provided that there are no negative cycles.
›

text ‹Canonical forms specify lower bounds for the length of any path.›
lemma canonical_subs_len:
  "M i j ≤ len M i j xs" if "canonical_subs n I M" "i ≤ n" "j ≤ n" "set xs ⊆ I" "I ⊆ {0..n}"
using that
proof (induction xs arbitrary: i)
  case Nil thus ?case by auto
next
  case (Cons x xs)
  then have "M x j ≤ len M x j xs" by auto
  from Cons.prems ‹canonical_subs n I M› have "M i j ≤ M i x + M x j"
    unfolding canonical_subs_def by auto
  also with Cons have "… ≤ M i x + len M x j xs" by (auto simp add: add_mono)
  finally show ?case by simp
qed

text ‹
  This lemma justifies the use of destructive updates under the absence of negative cycles.
›
lemma fwi_step':
  "fwi m n k i' j' i j = min (m i j) (m i k + m k j)" if
  "m k k ≥ 0" "i' ≤ n" "j' ≤ n" "k ≤ n" "i ≤ i'" "j ≤ j'"
  using that by (subst single_iteration_inv; auto simp: fwi_step)

text ‹An invocation of ‹fwi› extends canonical forms.›
lemma fwi_canonical_extend:
  "canonical_subs n (I ∪ {k}) (fwi m n k n n)" if
  "canonical_subs n I m" "I ⊆ {0..n}" "0 ≤ m k k" "k ≤ n"
  using that
  unfolding canonical_subs_def
  apply safe
  subgoal for i j k'
    apply (subst fwi_step', (auto; fail)+)+
    unfolding min_def
  proof (clarsimp, safe, goal_cases)
    case 1
    then show ?case by force
  next
    case prems: 2
    from prems have "m i k ≤ m i j + m j k"
      by auto
    with prems(10) show ?case
      by (auto simp: add.assoc[symmetric] add_mono intro: order.trans)
  next
    case prems: 3
    from prems have "m i k ≤ m i j + m j k"
      by auto
    with prems(10) show ?case
      by (auto simp: add.assoc[symmetric] add_mono intro: order.trans)
  next
    case prems: 4
    from prems have "m k k' ≤ m k j + m j k'"
      by auto
    with prems(10) show ?case
      by (auto simp: add_mono add.assoc intro: order.trans)
  next
    case prems: 5
    from prems have "m k k' ≤ m k j + m j k'"
      by auto
    with prems(10) show ?case
      by (auto simp: add_mono add.assoc intro: order.trans)
  next
    case prems: 6
    from prems have "0 ≤ m k j + m j k"
      by (auto intro: order.trans)
    with prems(10) show ?case
      apply -
      apply (rule order.trans, assumption)
      apply (simp add: add.assoc[symmetric])
      by (rule add_mono, auto simp: add_increasing2 add.assoc intro: order.trans)
  next
    case prems: 7
    from prems have "0 ≤ m k j + m j k"
      by (auto intro: order.trans)
    with prems(10) show ?case
      by (simp add: add.assoc[symmetric])
        (rule add_mono, auto simp: add_increasing2 add.assoc intro: order.trans)
  qed
  subgoal for i j k'
    apply (subst fwi_step', (auto; fail)+)+
    unfolding min_def by (auto intro: add_increasing add_increasing2)
  done

text ‹
  An invocation of ‹fwi› will not produce a negative diagonal entry if there is no negative cycle.
›
lemma fwi_cyc_free_diag:
  "fwi m n k n n i i ≥ 0" if
  "cyc_free_subs n I m" "0 ≤ m k k" "k ≤ n" "k ∈ I" "i ≤ n"
  using that
  apply (subst fwi_step', (auto; fail)+)+
  unfolding min_def
  proof (clarsimp; safe, goal_cases)
    case 1
    have "set [] ⊆ I"
      by simp
    with 1(1) ‹i ≤ n› show ?case
      by fastforce
  next
    case 2
    then have "set [k] ⊆ I"
      by simp
    with 2(1) ‹i ≤ n› show ?case by fastforce
  qed

lemma cyc_free_subs_diag:
  "m i i ≥ 0" if "cyc_free_subs n I m" "i ≤ n"
proof -
  have "set [] ⊆ I" by auto
  with that show ?thesis by fastforce
qed

lemma fwi_cyc_free_subs':
  "cyc_free_subs n (I ∪ {k}) (fwi m n k n n)" if
  "cyc_free_subs n I m" "canonical_subs n I m" "I ⊆ {0..n}" "k ≤ n"
  "∀ i ≤ n. fwi m n k n n i i ≥ 0"
proof (safe, goal_cases)
  case prems: (1 i xs)
  from that(1) ‹k ≤ n› have "0 ≤ m k k" by (rule cyc_free_subs_diag)
  from that ‹0 ≤ m k k› have *: "canonical_subs n (I ∪ {k}) (fwi m n k n n)"
    by - (rule fwi_canonical_extend; auto)
  from prems that have "0 ≤ fwi m n k n n i i" by blast
  also from * prems that have "fwi m n k n n i i ≤ len (fwi m n k n n) i i xs"
    by (auto intro: canonical_subs_len)
  finally show ?case .
qed

lemma fwi_cyc_free_subs:
  "cyc_free_subs n (I ∪ {k}) (fwi m n k n n)" if
  "cyc_free_subs n (I ∪ {k}) m" "canonical_subs n I m" "I ⊆ {0..n}" "k ≤ n"
proof (safe, goal_cases)
  case prems: (1 i xs)
  from that(1) ‹k ≤ n› have "0 ≤ m k k" by (rule cyc_free_subs_diag)
  from that ‹0 ≤ m k k› have *: "canonical_subs n (I ∪ {k}) (fwi m n k n n)"
    by - (rule fwi_canonical_extend; auto)
  from prems that ‹0 ≤ m k k› have "0 ≤ fwi m n k n n i i" by (auto intro!: fwi_cyc_free_diag)
  also from * prems that have "fwi m n k n n i i ≤ len (fwi m n k n n) i i xs"
    by (auto intro: canonical_subs_len)
  finally show ?case .
qed

lemma canonical_subs_empty [simp]:
  "canonical_subs n {} m"
  unfolding canonical_subs_def by simp

lemma fwi_neg_diag_neg_cycle:
  "∃ i ≤ n. ∃ xs. set xs ⊆ {0..k} ∧ len m i i xs < 0" if "fwi m n k n n i i < 0" "i ≤ n" "k ≤ n"
proof (cases "m k k ≥ 0")
  case True
  from fwi_step'[of m, OF True] that have "min (m i i) (m i k + m k i) < 0"
    by auto
  then show ?thesis
    unfolding min_def
  proof (clarsimp split: if_split_asm, goal_cases)
    case 1
    then have "len m i i [] < 0" "set [] ⊆ {}" by auto
    with ‹i ≤ n› show ?case by fastforce
  next
    case 2
    then have "len m i i [k] < 0" "set [k] ⊆ {0..k}" by auto
    with ‹i ≤ n› show ?case by fastforce
  qed
next
  case False
  with ‹k ≤ n› have "len m k k [] < 0" "set [] ⊆ {}" by auto
  with ‹k ≤ n› show ?thesis by fastforce
qed

text ‹‹fwi› preserves the length of paths.›
lemma fwi_len:
  "∃ ys. set ys ⊆ set xs ∪ {k} ∧ len (fwi m n k n n) i j xs = len m i j ys"
  if "i ≤ n" "j ≤ n" "k ≤ n" "m k k ≥ 0" "set xs ⊆ {0..n}"
  using that
proof (induction xs arbitrary: i)
  case Nil
  then show ?case
    apply (simp add: fwi_step')
    unfolding min_def
    apply (clarsimp; safe)
     apply (rule exI[where x = "[]"]; simp)
    by (rule exI[where x = "[k]"]; simp)
next
  case (Cons x xs)
  then obtain ys where "set ys ⊆ set xs ∪ {k}" "len (fwi m n k n n) x j xs = len m x j ys"
    by force
  with Cons.prems show ?case
    apply (simp add: fwi_step')
    unfolding min_def
    apply (clarsimp; safe)
     apply (rule exI[where x = "x # ys"]; auto; fail)
    by (rule exI[where x = "k # x # ys"]; auto simp: add.assoc)
qed

lemma fwi_neg_cycle_neg_cycle:
  "∃ i ≤ n. ∃ ys. set ys ⊆ set xs ∪ {k} ∧ len m i i ys < 0" if
  "len (fwi m n k n n) i i xs < 0" "i ≤ n" "k ≤ n" "set xs ⊆ {0..n}"
proof (cases "m k k ≥ 0")
  case True
  from fwi_len[OF that(2,2,3), of m, OF True that(4)] that(1,2) show ?thesis
    by safe (rule exI conjI | simp)+
next
  case False
  then have "len m k k [] < 0" "set [] ⊆ set xs ∪ {k}"
    by auto
  with ‹k ≤ n› show ?thesis by (intro exI conjI)
qed

text ‹
  If the \fw produces a negative diagonal entry, then there is a negative cycle.
›
lemma fw_neg_diag_neg_cycle:
  "∃ i ≤ n. ∃ ys. set ys ⊆ set xs ∪ {0..k} ∧ len m i i ys < 0" if
  "len (fw m n k) i i xs < 0" "i ≤ n" "k ≤ n" "set xs ⊆ {0..n}"
  using that
  proof (induction k arbitrary: i xs)
    case 0
    then show ?case by simp (drule fwi_neg_cycle_neg_cycle; auto)
  next
    case (Suc k)
    from fwi_neg_cycle_neg_cycle[OF Suc.prems(1)[simplified]] Suc.prems obtain i' ys where
      "i' ≤ n"  "set ys ⊆ set xs ∪ {Suc k}" "len (fw m n k) i' i' ys < 0"
      by auto
    with Suc.prems obtain i'' zs where
      "i'' ≤ n" "set zs ⊆ set ys ∪ {0..k}" "len m i'' i'' zs < 0"
      by atomize_elim (auto intro!: Suc.IH)
    with ‹set ys ⊆ _› have "set zs ⊆ set xs ∪ {0..Suc k} ∧ len m i'' i'' zs < 0"
      by force
    with ‹i'' ≤ n› show ?case by blast
  qed

text ‹Main theorem under the absence of negative cycles.›
theorem fw_correct:
  "canonical_subs n {0..k} (fw m n k) ∧ cyc_free_subs n {0..k} (fw m n k)"
  if "cyc_free_subs n {0..k} m" "k ≤ n"
  using that
proof (induction k)
  case 0
  then show ?case
    using fwi_cyc_free_subs[of n "{}" 0 m] fwi_canonical_extend[of n "{}"]
    by (auto simp: cyc_free_subs_diag)
next
  case (Suc k)
  then have IH:
    "canonical_subs n {0..k} (fw m n k) ∧ cyc_free_subs n {0..k} (fw m n k)"
    by fastforce
  have *: "{0..Suc k} = {0..k} ∪ {Suc k}" by auto
  then have **: "canonical_subs n {0..Suc k} (fw m n (Suc k))"
    apply simp
    apply (rule fwi_canonical_extend[of n "{0..k}" _ "Suc k", simplified])
    subgoal
      using IH ..
    subgoal
      using IH Suc.prems by (auto intro: cyc_free_subs_diag[of n "{0..k}" "fw m n k"])
    by (rule Suc)
  show ?case
  proof (cases "∃i≤n. fw m n (Suc k) i i < 0")
    case True
    then obtain i where "i ≤ n" "len (fw m n (Suc k)) i i [] < 0"
      by auto
    from fw_neg_diag_neg_cycle[OF this(2,1) ‹Suc k ≤ n›] Suc.prems show ?thesis by fastforce
  next
    case False
    have "cyc_free_subs n {0..Suc k} (fw m n (Suc k))"
      apply (simp add: *)
      apply (rule fwi_cyc_free_subs'[of n "{0..k}", simplified])
      using Suc IH False by force+
    with ** show ?thesis by blast
  qed
qed

lemmas fw_canonical_subs = fw_correct[THEN conjunct1]
lemmas fw_cyc_free_subs = fw_correct[THEN conjunct2]
lemmas cyc_free_diag = cyc_free_subs_diag


section ‹Definition of Shortest Paths›

text ‹
  We define the notion of the length of the shortest ‹simple› path between two vertices,
  using only intermediate vertices from the set ‹{0…k}›.
›
definition D :: "'a mat ⇒ nat ⇒ nat ⇒ nat ⇒ 'a" where
  "D m i j k ≡ Min {len m i j xs | xs. set xs ⊆ {0..k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}"

lemma distinct_length_le:"finite s ⟹ set xs ⊆ s ⟹ distinct xs ⟹ length xs ≤ card s"
by (metis card_mono distinct_card)

lemma finite_distinct: "finite s ⟹ finite {xs . set xs ⊆ s ∧ distinct xs}"
proof -
  assume "finite s"
  hence "{xs . set xs ⊆ s ∧ distinct xs} ⊆ {xs. set xs ⊆ s ∧ length xs ≤ card s}"
  using distinct_length_le by auto
  moreover have "finite {xs. set xs ⊆ s ∧ length xs ≤ card s}"
  using finite_lists_length_le[OF ‹finite s›] by auto
  ultimately show ?thesis by (rule finite_subset)
qed

lemma D_base_finite:
  "finite {len m i j xs | xs. set xs ⊆ {0..k} ∧ distinct xs}"
using finite_distinct finite_image_set by blast

lemma D_base_finite':
  "finite {len m i j xs | xs. set xs ⊆ {0..k} ∧ distinct (i # j # xs)}"
proof -
  have "{len m i j xs | xs. set xs ⊆ {0..k} ∧ distinct (i # j # xs)}
        ⊆ {len m i j xs | xs. set xs ⊆ {0..k} ∧ distinct xs}" by auto
  with D_base_finite[of m i j k] show ?thesis by (rule rev_finite_subset)
qed

lemma D_base_finite'':
  "finite {len m i j xs |xs. set xs ⊆ {0..k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}"
using D_base_finite[of m i j k] by - (rule finite_subset, auto)

definition cycle_free :: "'a mat ⇒ nat ⇒ bool" where
  "cycle_free m n ≡ ∀ i xs. i ≤ n ∧ set xs ⊆ {0..n} ⟶
  (∀ j. j ≤ n ⟶ len m i j (rem_cycles i j xs) ≤ len m i j xs) ∧ len m i i xs ≥ 0"

lemma D_eqI:
  fixes m n i j k
  defines "A ≡ {len m i j xs | xs. set xs ⊆ {0..k}}"
  defines "A_distinct ≡ {len m i j xs |xs. set xs ⊆ {0..k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}"
  assumes "cycle_free m n" "i ≤ n" "j ≤ n" "k ≤ n" "(⋀y. y ∈ A_distinct ⟹ x ≤ y)" "x ∈ A"
  shows "D m i j k = x" using assms
proof -
  let ?S = "{len m i j xs |xs. set xs ⊆ {0..k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}"
  show ?thesis unfolding D_def
  proof (rule Min_eqI)
    have "?S ⊆ {len m i j xs |xs. set xs ⊆ {0..k} ∧ distinct xs}" by auto
    thus "finite {len m i j xs |xs. set xs ⊆ {0..k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}"
    using D_base_finite[of m i j k] by (rule finite_subset)
  next
    fix y assume "y ∈ ?S"
    hence "y ∈ A_distinct" using assms(2,7) by fastforce
    thus "x ≤ y" using assms by meson
  next
    from assms obtain xs where xs: "x = len m i j xs" "set xs ⊆ {0..k}" by auto
    let ?ys = "rem_cycles i j xs"
    let ?y = "len m i j ?ys"
    from assms(3-6) xs have *:"?y ≤ x" by (fastforce simp add: cycle_free_def)
    have distinct: "i ∉ set ?ys" "j ∉ set ?ys" "distinct ?ys"
    using rem_cycles_distinct remove_all_removes rem_cycles_removes_last by fast+
    with xs(2) have "?y ∈ A_distinct" unfolding A_distinct_def using rem_cycles_subs by fastforce
    hence "x ≤ ?y" using assms by meson
    moreover have "?y ≤ x" using assms(3-6) xs by (fastforce simp add: cycle_free_def)
    ultimately have "x = ?y" by simp
    thus "x ∈ ?S" using distinct xs(2) rem_cycles_subs[of i j xs] by fastforce
  qed
qed

lemma D_base_not_empty:
   "{len m i j xs |xs. set xs ⊆ {0..k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs} ≠ {}"
proof -
  have "len m i j [] ∈ {len m i j xs |xs. set xs ⊆ {0..k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}"
  by fastforce
  thus ?thesis by auto
qed

lemma Min_elem_dest: "finite A ⟹ A ≠ {} ⟹ x = Min A ⟹ x ∈ A" by simp

lemma D_dest: "x = D m i j k ⟹
  x ∈ {len m i j xs |xs. set xs ⊆ {0..Suc k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}"
using Min_elem_dest[OF D_base_finite'' D_base_not_empty] by (fastforce simp add: D_def)

lemma D_dest': "x = D m i j k ⟹ x ∈ {len m i j xs |xs. set xs ⊆ {0..Suc k}}"
using Min_elem_dest[OF D_base_finite'' D_base_not_empty] by (fastforce simp add: D_def)

lemma D_dest'': "x = D m i j k ⟹ x ∈ {len m i j xs |xs. set xs ⊆ {0..k}}"
using Min_elem_dest[OF D_base_finite'' D_base_not_empty] by (fastforce simp add: D_def)

lemma cycle_free_loop_dest: "i ≤ n ⟹ set xs ⊆ {0..n} ⟹ cycle_free m n ⟹ len m i i xs ≥ 0"
unfolding cycle_free_def by auto

lemma cycle_free_dest:
  "cycle_free m n ⟹ i ≤ n ⟹ j ≤ n ⟹ set xs ⊆ {0..n}
    ⟹ len m i j (rem_cycles i j xs) ≤ len m i j xs"
by (auto simp add: cycle_free_def)

definition cycle_free_up_to :: "'a mat ⇒ nat ⇒ nat ⇒ bool" where
  "cycle_free_up_to m k n ≡ ∀ i xs. i ≤ n ∧ set xs ⊆ {0..k} ⟶
  (∀ j. j ≤ n ⟶ len m i j (rem_cycles i j xs) ≤ len m i j xs) ∧ len m i i xs ≥ 0"

lemma cycle_free_up_to_loop_dest:
  "i ≤ n ⟹ set xs ⊆ {0..k} ⟹ cycle_free_up_to m k n ⟹ len m i i xs ≥ 0"
unfolding cycle_free_up_to_def by auto

lemma cycle_free_up_to_diag:
  assumes "cycle_free_up_to m k n" "i ≤ n"
  shows "m i i ≥ 0"
using cycle_free_up_to_loop_dest[OF assms(2) _ assms(1), of "[]"] by auto

lemma D_eqI2:
  fixes m n i j k
  defines "A ≡ {len m i j xs | xs. set xs ⊆ {0..k}}"
  defines "A_distinct ≡ {len m i j xs | xs. set xs ⊆ {0..k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}"
  assumes "cycle_free_up_to m k n" "i ≤ n" "j ≤ n" "k ≤ n"
          "(⋀y. y ∈ A_distinct ⟹ x ≤ y)" "x ∈ A"
  shows "D m i j k = x" using assms
proof -
  show ?thesis
  proof (simp add: D_def A_distinct_def[symmetric], rule Min_eqI)
    show "finite A_distinct" using D_base_finite''[of m i j k] unfolding A_distinct_def by auto
  next
    fix y assume "y ∈ A_distinct"
    thus "x ≤ y" using assms by meson
  next
    from assms obtain xs where xs: "x = len m i j xs" "set xs ⊆ {0..k}" by auto
    let ?ys = "rem_cycles i j xs"
    let ?y = "len m i j ?ys"
    from assms(3-6) xs have *:"?y ≤ x" by (fastforce simp add: cycle_free_up_to_def)
    have distinct: "i ∉ set ?ys" "j ∉ set ?ys" "distinct ?ys"
    using rem_cycles_distinct remove_all_removes rem_cycles_removes_last by fast+
    with xs(2) have "?y ∈ A_distinct" unfolding A_distinct_def using rem_cycles_subs by fastforce
    hence "x ≤ ?y" using assms by meson
    moreover have "?y ≤ x" using assms(3-6) xs by (fastforce simp add: cycle_free_up_to_def)
    ultimately have "x = ?y" by simp
    then show "x ∈ A_distinct" using distinct xs(2) rem_cycles_subs[of i j xs]
    unfolding A_distinct_def by fastforce
  qed
qed

subsection ‹Connecting the Algorithm to the Notion of Shortest Paths›

text ‹
  Under the absence of negative cycles, the \fw correctly computes the length of the shortest path
  between any pair of vertices ‹i, j›.
›
lemma canonical_D:
  assumes
    "cycle_free_up_to m k n" "canonical_subs n {0..k} m" "i ≤ n" "j ≤ n" "k ≤ n"
  shows "D m i j k = m i j"
  using assms
  apply -
  apply (rule D_eqI2)
       apply (assumption | simp; fail)+
  subgoal
    by (auto intro: canonical_subs_len)
  apply clarsimp
  by (rule exI[where x = "[]"]) auto


theorem fw_subs_len:
  "(fw m n k) i j ≤ len m i j xs" if
  "cyc_free_subs n {0..k} m" "k ≤ n" "i ≤ n" "j ≤ n" "set xs ⊆ I" "I ⊆ {0..k}"
proof -
  from fw_correct[OF that(1,2)] have "canonical_subs n {0..k} (fw m n k)" ..
  from canonical_subs_len[OF this, of i j xs] that have "fw m n k i j ≤ len (fw m n k) i j xs"
    by auto
  also from that(2-) have "… ≤ len m i j xs"
  proof (induction xs arbitrary: i)
    case Nil
    then show ?case by (auto intro: fw_mono)
  next
    case (Cons x xs)
    then have "len (fw m n k) x j xs ≤ len m x j xs"
      by auto
    moreover from Cons.prems have "fw m n k i x ≤ m i x" by - (rule fw_mono; auto)
    ultimately show ?case by (auto simp: add_mono)
  qed
  finally show ?thesis by auto
qed

text ‹
  This shows that the value calculated by ‹fwi› for a pair ‹i, j› always corresponds to the length
  of an actual path between ‹i› and ‹j›.
›
lemma fwi_len':
  "∃ xs. set xs ⊆ {k} ∧ fwi m n k i' j' i j = len m i j xs" if
  "m k k ≥ 0" "i' ≤ n" "j' ≤ n" "k ≤ n" "i ≤ i'" "j ≤ j'"
  using that apply (subst fwi_step'; auto)
  unfolding min_def
  apply (clarsimp; safe)
   apply (rule exI[where x = "[]"]; auto; fail)
  by (rule exI[where x = "[k]"]; auto; fail)

text ‹
  The same result for ‹fw›.
›
lemma fw_len:
  "∃ xs. set xs ⊆ {0..k} ∧ fw m n k i j = len m i j xs" if
  "cyc_free_subs n {0..k} m" "i ≤ n" "j ≤ n" "k ≤ n"
  using that
proof (induction k arbitrary: i j)
  case 0
  from cyc_free_subs_diag[OF this(1)] have "m 0 0 ≥ 0" by blast
  with 0 show ?case by (auto intro: fwi_len')
next
  case (Suc k)
  have IH: "∃ xs. set xs ⊆ {0..k} ∧ fw m n k i j = len m i j xs" if "i ≤ n" "j ≤ n" for i j
    apply (rule Suc.IH)
    using Suc.prems that by force+
  from fw_cyc_free_subs[OF Suc.prems(1,4)] have "cyc_free_subs n {0..Suc k} (fw m n (Suc k))" .
  then have "0 ≤ fw m n k (Suc k) (Suc k)" using IH Suc.prems(1, 4) by fastforce
  with Suc.prems fwi_len'[of "fw m n k" "Suc k" n n n i j] obtain xs where
    "set xs ⊆ {Suc k}" "fwi (fw m n k) n (Suc k) n n i j = len (fw m n k) i j xs"
    by auto
  moreover from Suc.prems(2-) this(1) have
    "∃ ys. set ys ⊆ {0..Suc k} ∧ len (fw m n k) i j xs = len m i j ys"
  proof (induction xs arbitrary: i)
    case Nil
    then show ?case by (force dest: IH)
  next
    case (Cons x xs)
    then obtain ys where ys:
      "set ys ⊆ {0..Suc k}" "len (fw m n k) x j xs = len m x j ys"
      by force
    moreover from IH[of i x] Cons.prems obtain zs where
      "set zs ⊆ {0..k}" "fw m n k i x = len m i x zs"
      by auto
    ultimately have
      "set (zs @ x # ys) ⊆ {0..Suc k}" "len (fw m n k) i j (x # xs) = len m i j (zs @ x # ys)"
      using ‹Suc k ≤ n› ‹set (x # xs) ⊆ _› by (auto simp: len_comp)
    then show ?case by (intro exI conjI)
  qed
  ultimately show ?case by auto
qed


section ‹Intermezzo: Equivalent Characterizations of Cycle-Freeness›

subsection ‹Shortening Negative Cycles›

lemma remove_cycles_neg_cycles_aux:
  fixes i xs ys
  defines "xs' ≡ i # ys"
  assumes "i ∉ set ys"
  assumes "i ∈ set xs"
  assumes "xs = as @ concat (map ((#) i) xss) @ xs'"
  assumes "len m i j ys > len m i j xs"
  shows "∃ ys. set ys ⊆ set xs ∧ len m i i ys < 0" using assms
proof (induction xss arbitrary: xs as)
  case Nil
  with Nil show ?case
  proof (cases "len m i i as ≥ 0", goal_cases)
    case 1
    from this(4,6) len_decomp[of xs as i ys m i j]
    have "len m i j xs = len m i i as + len m i j ys" by simp
    with 1(11)
    have "len m i j ys ≤ len m i j xs" using add_mono by fastforce
    thus ?thesis using Nil(5) by auto
  next
    case 2 thus ?case by auto
  qed
next
  case (Cons zs xss)
  let ?xs = "zs @ concat (map ((#) i) xss) @ xs'"
  from Cons show ?case
  proof (cases "len m i i as ≥ 0", goal_cases)
    case 1
    from this(5,7) len_decomp add_mono
    have "len m i j ?xs ≤ len m i j xs" by fastforce
    hence 4:"len m i j ?xs < len m i j ys" using 1(6) by simp
    have 2:"i ∈ set ?xs" using Cons(2) by auto
    have "set ?xs ⊆ set xs" using Cons(5) by auto
    moreover from Cons(1)[OF 1(2,3) 2 _ 4] have "∃ys. set ys ⊆ set ?xs ∧ len m i i ys < 0" by auto
    ultimately show ?case by blast
  next
    case 2
    from this(5,7) show ?case by auto
  qed
qed

lemma add_lt_neutral: "a + b < b ⟹ a < 0"
proof (rule ccontr)
  assume "a + b < b" "¬ a < 0"
  hence "a ≥ 0" by auto
  from add_mono[OF this, of b b] ‹a + b < b› show False by auto
qed

lemma remove_cycles_neg_cycles_aux':
  fixes j xs ys
  assumes "j ∉ set ys"
  assumes "j ∈ set xs"
  assumes "xs = ys @ j # concat (map (λ xs. xs @ [j]) xss) @ as"
  assumes "len m i j ys > len m i j xs"
  shows "∃ ys. set ys ⊆ set xs ∧ len m j j ys < 0" using assms
proof (induction xss arbitrary: xs as)
  case Nil
  show ?case
  proof (cases "len m j j as ≥ 0")
    case True
    from Nil(3) len_decomp[of xs ys j as m i j]
    have "len m i j xs = len m i j ys + len m j j as" by simp
    with True
    have "len m i j ys ≤ len m i j xs" using add_mono by fastforce
    with Nil show ?thesis by auto
  next
    case False with Nil show ?thesis by auto
  qed
next
  case (Cons zs xss)
  let ?xs = "ys @ j # concat (map (λxs. xs @ [j]) xss) @ as"
  let ?t = "concat (map (λxs. xs @ [j]) xss) @ as"
  show ?case
  proof (cases "len m i j ?xs ≤ len m i j xs")
    case True
    hence 4:"len m i j ?xs < len m i j ys" using Cons(5) by simp
    have 2:"j ∈ set ?xs" using Cons(2) by auto
    have "set ?xs ⊆ set xs" using Cons(4) by auto
    moreover from Cons(1)[OF Cons(2) 2 _ 4] have "∃ys. set ys ⊆ set ?xs ∧ len m j j ys < 0" by blast
    ultimately show ?thesis by blast
  next
    case False
    hence "len m i j xs < len m i j ?xs" by auto
    from this len_decomp Cons(4) add_mono
    have "len m j j (concat (map (λxs. xs @ [j]) (zs # xss)) @ as) < len m j j ?t"
    using False local.leI by fastforce
    hence "len m j j (zs @ j # ?t) < len m j j ?t" by simp
    with len_decomp[of "zs @ j # ?t" zs j ?t m j j]
    have "len m j j zs + len m j j ?t < len m j j ?t" by auto
    hence "len m j j zs < 0" using add_lt_neutral by auto
    thus ?thesis using Cons.prems(3) by auto
  qed
qed

lemma add_le_impl: "a + b < a + c ⟹ b < c"
proof (rule ccontr)
  assume "a + b < a + c" "¬ b < c"
  hence "b ≥ c" by auto
  from add_mono[OF _ this, of a a] ‹a + b < a + c› show False by auto
qed

lemma start_remove_neg_cycles:
  "len m i j (start_remove xs k []) > len m i j xs ⟹ ∃ ys. set ys ⊆ set xs ∧ len m k k ys < 0"
proof-
  let ?xs = "start_remove xs k []"
  assume len_lt:"len m i j ?xs > len m i j xs"
  hence "k ∈ set xs" using start_remove_id by fastforce
  from start_remove_decomp[OF this, of "[]"] obtain as bs where as_bs:
    "xs = as @ k # bs" "?xs = as @ remove_cycles bs k [k]"
  by fastforce
  let ?xs' = "remove_cycles bs k [k]"
  have "k ∈ set bs" using as_bs len_lt remove_cycles_id by fastforce
  then obtain ys where ys: "?xs = as @ k # ys" "?xs' = k # ys" "k ∉ set ys"
  using as_bs(2) remove_cycles_begins_with[OF ‹k ∈ set bs›] by auto
  have len_lt': "len m k j bs < len m k j ys"
  using len_decomp[OF as_bs(1), of m i j] len_decomp[OF ys(1), of m i j] len_lt add_le_impl by metis
  from remove_cycles_cycles[OF ‹k ∈ set bs›] obtain xss as'
  where "as' @ concat (map ((#) k) xss) @ ?xs' = bs" by fastforce
  hence "as' @ concat (map ((#) k) xss) @ k # ys = bs" using ys(2) by simp
  from remove_cycles_neg_cycles_aux[OF ‹k ∉ set ys› ‹k ∈ set bs› this[symmetric] len_lt']
  show ?thesis using as_bs(1) by auto
qed

lemma remove_all_cycles_neg_cycles:
  "len m i j (remove_all_cycles ys xs) > len m i j xs
  ⟹ ∃ ys k. set ys ⊆ set xs ∧ k ∈ set xs ∧ len m k k ys < 0"
proof (induction ys arbitrary: xs)
  case Nil thus ?case by auto
next
  case (Cons y ys)
  let ?xs = "start_remove xs y []"
  show ?case
  proof (cases "len m i j xs < len m i j ?xs")
    case True
    with start_remove_id have "y ∈ set xs" by fastforce
    with start_remove_neg_cycles[OF True] show ?thesis by blast
  next
    case False
    with Cons(2) have "len m i j ?xs < len m i j (remove_all_cycles (y # ys) xs)" by auto
    hence "len m i j ?xs < len m i j (remove_all_cycles ys ?xs)" by auto
    from Cons(1)[OF this] show ?thesis using start_remove_subs[of xs y "[]"] by auto
  qed
qed

lemma concat_map_cons_rev:
  "rev (concat (map ((#) j) xss)) = concat (map (λ xs. xs @ [j]) (rev (map rev xss)))"
by (induction xss) auto

lemma negative_cycle_dest: "len m i j (rem_cycles i j xs) > len m i j xs
       ⟹ ∃ i' ys. len m i' i' ys < 0 ∧ set ys ⊆ set xs ∧ i' ∈ set (i # j # xs)"
proof -
  let ?xsij = "rem_cycles i j xs"
  let ?xsj  = "remove_all_rev j (remove_all_cycles xs xs)"
  let ?xs   = "remove_all_cycles xs xs"
  assume len_lt: "len m i j ?xsij > len m i j xs"
  show ?thesis
  proof (cases "len m i j ?xsij ≤ len m i j ?xsj")
    case True
    hence len_lt: "len m i j ?xsj > len m i j xs" using len_lt by simp
    show ?thesis
    proof (cases "len m i j ?xsj ≤ len m i j ?xs")
      case True
      hence "len m i j ?xs > len m i j xs" using len_lt by simp
      with remove_all_cycles_neg_cycles[OF this] show ?thesis by auto
    next
      case False
      then have len_lt': "len m i j ?xsj > len m i j ?xs" by simp
      show ?thesis
      proof (cases "j ∈ set ?xs")
        case False
        thus ?thesis using len_lt' by (simp add: remove_all_rev_def)
      next
        case True
          from remove_all_rev_removes[of j] have 1: "j ∉ set ?xsj" by simp
          from True have "j ∈ set (rev ?xs)" by auto
          from remove_cycles_cycles[OF this] obtain xss as where as:
          "as @ concat (map ((#) j) xss) @ remove_cycles (rev ?xs) j [] = rev ?xs" "j ∉ set as"
          by blast
          from True have "?xsj = rev (tl (remove_cycles (rev ?xs) j []))" by (simp add: remove_all_rev_def)
          with remove_cycles_begins_with[OF ‹j ∈ set (rev ?xs)›, of "[]"]
          have "remove_cycles (rev ?xs) j [] = j # rev ?xsj" "j ∉ set ?xsj"
          by auto
          with as(1) have xss: "as @ concat (map ((#) j) xss) @ j # rev ?xsj = rev ?xs" by simp
          hence "rev (as @ concat (map ((#) j) xss) @ j # rev ?xsj) = ?xs" by simp
          hence "?xsj @ j # rev (concat (map ((#) j) xss)) @ rev as = ?xs" by simp
          hence "?xsj @ j # concat (map (λ xs. xs @ [j]) (rev (map rev xss))) @ rev as = ?xs"
          by (simp add: concat_map_cons_rev)
          from remove_cycles_neg_cycles_aux'[OF 1 True this[symmetric] len_lt']
          show ?thesis using remove_all_cycles_subs by fastforce
      qed
    qed
  next
    case False
    hence len_lt': "len m i j ?xsij > len m i j ?xsj" by simp
    show ?thesis
    proof (cases "i ∈ set ?xsj")
      case False
      thus ?thesis using len_lt' by (simp add: remove_all_def)
    next
      case True
      from remove_all_removes[of i] have 1: "i ∉ set ?xsij" by (simp add: remove_all_def)
      from remove_cycles_cycles[OF True] obtain xss as where as:
      "as @ concat (map ((#) i) xss) @ remove_cycles ?xsj i [] = ?xsj" "i ∉ set as" by blast
      from True have "?xsij = tl (remove_cycles ?xsj i [])" by (simp add: remove_all_def)
      with remove_cycles_begins_with[OF True, of "[]"]
      have "remove_cycles ?xsj i [] = i # ?xsij" "i ∉ set ?xsij"
      by auto
      with as(1) have xss: "as @ concat (map ((#) i) xss) @ i # ?xsij = ?xsj" by simp
      from remove_cycles_neg_cycles_aux[OF 1 True this[symmetric] len_lt']
      show ?thesis using remove_all_rev_subs remove_all_cycles_subs by fastforce
    qed
  qed
qed


subsection ‹Cycle-Freeness›

lemma cycle_free_alt_def:
  "cycle_free M n ⟷ cycle_free_up_to M n n"
  unfolding cycle_free_def cycle_free_up_to_def ..

lemma negative_cycle_dest_diag:
  "¬ cycle_free_up_to m k n ⟹ k ≤ n ⟹ ∃ i xs. i ≤ n ∧ set xs ⊆ {0..k} ∧ len m i i xs < 0"
proof (auto simp: cycle_free_up_to_def, goal_cases)
  case (1 i xs j)
  from this(5) have "len m i j xs < len m i j (rem_cycles i j xs)" by auto
  from negative_cycle_dest[OF this] obtain i' ys
  where *:"len m i' i' ys < 0" "set ys ⊆ set xs" "i' ∈ set (i # j # xs)" by auto
  from this(2,3) 1(1-4) have "set ys ⊆ {0..k}" "i' ≤ n" by auto
  with * show ?case by auto
next
  case 2 then show ?case by fastforce
qed

lemma negative_cycle_dest_diag':
  "¬ cycle_free m n ⟹ ∃ i xs. i ≤ n ∧ set xs ⊆ {0..n} ∧ len m i i xs < 0"
  by (rule negative_cycle_dest_diag) (auto simp: cycle_free_alt_def)

abbreviation cyc_free :: "'a mat ⇒ nat ⇒ bool" where
  "cyc_free m n ≡ ∀ i xs. i ≤ n ∧ set xs ⊆ {0..n} ⟶ len m i i xs ≥ 0"

lemma cycle_free_diag_intro:
  "cyc_free m n ⟹ cycle_free m n"
  using negative_cycle_dest_diag' by force

lemma cycle_free_diag_equiv:
  "cyc_free m n ⟷ cycle_free m n" using negative_cycle_dest_diag'
  by (force simp: cycle_free_def)

lemma cycle_free_diag_dest:
  "cycle_free m n ⟹ cyc_free m n"
  using cycle_free_diag_equiv by blast

lemma cycle_free_upto_diag_equiv:
  "cycle_free_up_to m k n ⟷ cyc_free_subs n {0..k} m" if "k ≤ n"
  using negative_cycle_dest_diag[of m k n] that by (force simp: cycle_free_up_to_def)

theorem fw_shortest_path_up_to:
  "D m i j k = fw m n k i j" if "cyc_free_subs n {0..k} m" "i ≤ n" "j ≤ n" "k ≤ n"
proof -
  from that(1,4) have cycle_free: "cycle_free_up_to m k n" by (subst cycle_free_upto_diag_equiv)
  from that have "canonical_subs n {0..k} (fw m n k)" "cyc_free_subs n {0..k} (fw m n k)"
    by (auto dest: fw_correct)
  show ?thesis
  proof (rule D_eqI2[where n = n], safe, goal_cases)
      case (5 y xs)
    with that(1) that show ?case by (auto intro: fw_subs_len)
  next
    case 6
    from fw_len[OF that(1) that(2-)] show ?case by blast
  qed (rule that cycle_free)+
qed

text ‹We do not need to prove this because the definitions match.›
lemma
  "cyc_free m n ⟷ cyc_free_subs n {0..n} m" ..

lemma cycle_free_cycle_free_up_to:
  "cycle_free m n ⟹ k ≤ n ⟹ cycle_free_up_to m k n"
unfolding cycle_free_def cycle_free_up_to_def by force

lemma cycle_free_diag:
  "cycle_free m n ⟹ i ≤ n ⟹ 0 ≤ m i i"
using cycle_free_up_to_diag[OF cycle_free_cycle_free_up_to] by blast

corollary fw_shortest_path:
  "cyc_free m n ⟹ i ≤ n ⟹ j ≤ n ⟹ k ≤ n ⟹ D m i j k = fw m n k i j"
by (rule fw_shortest_path_up_to; force)

corollary fw_shortest:
  assumes "cyc_free m n" "i ≤ n" "j ≤ n" "k ≤ n"
  shows "fw m n n i j ≤ fw m n n i k + fw m n n k j"
  using fw_canonical_subs[OF assms(1)] assms(2-) unfolding canonical_subs_def by auto


section ‹Result Under the Presence of Negative Cycles›

text ‹
  Under the presence of negative cycles, the \fw will detect the situation by computing a negative
  diagonal entry.
›

lemma not_cylce_free_dest: "¬ cycle_free m n ⟹ ∃ k ≤ n. ¬ cycle_free_up_to m k n"
by (auto simp add: cycle_free_def cycle_free_up_to_def)

lemma D_not_diag_le:
  "(x :: 'a) ∈ {len m i j xs |xs. set xs ⊆ {0..k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}
  ⟹ D m i j k ≤ x" using Min_le[OF D_base_finite''] by (auto simp add: D_def)

lemma D_not_diag_le': "set xs ⊆ {0..k} ⟹ i ∉ set xs ⟹ j ∉ set xs ⟹ distinct xs
  ⟹ D m i j k ≤ len m i j xs" using Min_le[OF D_base_finite''] by (fastforce simp add: D_def)

lemma nat_upto_subs_top_removal':
  "S ⊆ {0..Suc n} ⟹ Suc n ∉ S ⟹ S ⊆ {0..n}"
apply (induction n)
 apply safe
 apply (rename_tac x)
 apply (case_tac "x = Suc 0"; fastforce)
apply (rename_tac n x)
apply (case_tac "x = Suc (Suc n)"; fastforce)
done

lemma nat_upto_subs_top_removal:
  "S ⊆ {0..n::nat} ⟹ n ∉ S ⟹ S ⊆ {0..n - 1}"
using nat_upto_subs_top_removal' by (cases n; simp)

text ‹Monotonicity with respect to ‹k›.›
lemma fw_invariant:
  "k' ≤ k ⟹ i ≤ n ⟹ j ≤ n ⟹ k ≤ n ⟹ fw m n k i j ≤ fw m n k' i j"
proof (induction k)
  case 0
  then show ?case by (auto intro: fwi_invariant)
next
  case (Suc k)
  show ?case
  proof (cases "k' = Suc k")
    case True
    then show ?thesis by simp
  next
    case False
    with Suc have "fw m n k i j ≤ fw m n k' i j"
      by auto
    moreover from ‹i ≤ n› ‹j ≤ n› have "fw m n (Suc k) i j ≤ fw m n k i j"
      by (auto intro: fwi_mono)
    ultimately show ?thesis by auto
  qed
qed

lemma negative_len_shortest:
  "length xs = n ⟹ len m i i xs < 0
    ⟹ ∃ j ys. distinct (j # ys) ∧ len m j j ys < 0 ∧ j ∈ set (i # xs) ∧ set ys ⊆ set xs"
proof (induction n arbitrary: xs i rule: less_induct)
  case (less n)
  show ?case
  proof (cases xs)
    case Nil
    thus ?thesis using less.prems by auto
  next
    case (Cons y ys)
    then have "length xs ≥ 1" by auto
    show ?thesis
    proof (cases "i ∈ set xs")
      assume i: "i ∈ set xs"
      then obtain as bs where xs: "xs = as @ i # bs" by (meson split_list)
      show ?thesis
      proof (cases "len m i i as < 0")
        case True
        from xs less.prems have "length as < n" by auto
        from less.IH[OF this _ True] xs show ?thesis by auto
      next
        case False
        from len_decomp[OF xs] have "len m i i xs = len m i i as + len m i i bs" by auto
        with False less.prems have *: "len m i i bs < 0"
        by (metis add_lt_neutral local.dual_order.strict_trans local.neqE)
        from xs less.prems have "length bs < n" by auto
        from less.IH[OF this _ *] xs show ?thesis by auto
      qed
    next
      assume i: "i ∉ set xs"
      show ?thesis
      proof (cases "distinct xs")
        case True
        with i less.prems show ?thesis by auto
      next
        case False
        from not_distinct_decomp[OF this] obtain a as bs cs where xs:
          "xs = as @ a # bs @ a # cs"
        by auto
        show ?thesis
        proof (cases "len m a a bs < 0")
          case True
          from xs less.prems have "length bs < n" by auto
          from less.IH[OF this _ True] xs show ?thesis by auto
        next
          case False
          from len_decomp[OF xs, of m  i i] len_decomp[of "bs @ a # cs" bs a cs m a i]
          have *:"len m i i xs = len m i a as + (len m a a bs + len m a i cs)" by auto
          from False have "len m a a bs ≥ 0" by auto
          with add_mono have "len m a a bs + len m a i cs ≥ len m a i cs" by fastforce
          with * have "len m i i xs ≥ len m i a as + len m a i cs" by (simp add: add_mono)
          with less.prems(2) have "len m i a as + len m a i cs < 0" by auto
          with len_comp have "len m i i (as @ a # cs) < 0" by auto
          from less.IH[OF _ _ this, of "length (as @ a # cs)"] xs less.prems
          show ?thesis by auto
        qed
      qed
    qed
  qed
qed

lemma fw_upd_leI:
  "fw_upd m' k i j i j ≤ fw_upd m k i j i j" if
  "m' i k ≤ m i k" "m' k j ≤ m k j" "m' i j ≤ m i j"
  using that unfolding fw_upd_def upd_def min_def using add_mono by fastforce

lemma fwi_fw_upd_mono:
  "fwi m n k i j i j ≤ fw_upd m k i j i j" if "k ≤ n" "i ≤ n" "j ≤ n"
  using that by (cases i; cases j) (auto intro: fw_upd_leI fwi_mono)

text ‹
  The \fw will always detect negative cycles. The argument goes as follows:
  In case there is a negative cycle, then we know that there is some smallest ‹k› for which
  there is a negative cycle containing only intermediate vertices from the set ‹{0…k}›.
  We will show that then ‹fwi m n k› computes a negative entry on the diagonal, and thus,
  by monotonicity, ‹fw m n n› will compute a negative entry on the diagonal.
›
theorem FW_neg_cycle_detect:
  "¬ cyc_free m n ⟹ ∃ i ≤ n. fw m n n i i < 0"
proof -
  assume A: "¬ cyc_free m n"
  let ?K = "{k. k ≤ n ∧ ¬ cyc_free_subs n {0..k} m}"
  define k where "k = Min ?K"
  have not_empty_K: "?K ≠ {}" using A by auto
  have "finite ?K" by auto
  with not_empty_K have *:
    "∀ k' < k. cyc_free_subs n {0..k'} m"
    unfolding k_def
    by simp (meson order_class.dual_order.trans preorder_class.less_le_not_le)
  from linorder_class.Min_in[OF ‹finite ?K› ‹?K ≠ {}›] have
    "¬ cyc_free_subs n {0..k} m" "k ≤ n"
    unfolding k_def by auto
  then have "∃ xs j. j ≤ n ∧ len m j j xs < 0 ∧ set xs ⊆ {0..k}"
    by force
  then obtain a as where a_as: "a ≤ n ∧ len m a a as < 0 ∧ set as ⊆ {0..k}" by auto
  with negative_len_shortest[of as "length as" m a] obtain j xs where j_xs:
  "distinct (j # xs) ∧ len m j j xs < 0 ∧ j ∈ set (a # as) ∧ set xs ⊆ set as" by auto
  with a_as ‹k ≤ n› have cyc: "j ≤ n" "set xs ⊆ {0..k}" "len m j j xs < 0" "distinct (j # xs)"
    by auto
  { assume "k > 0"
    then have "k - 1 < k" by simp
    with * have **:"cyc_free_subs n {0..k - 1} m" by blast
    have "k ∈ set xs"
    proof (rule ccontr, goal_cases)
      case 1
      with ‹set xs ⊆ {0..k}› nat_upto_subs_top_removal have "set xs ⊆ {0..k-1}" by auto
      with ‹cyc_free_subs n {0..k - 1} m› ‹j ≤ n› have "0 ≤ len m j j xs" by blast
      with cyc(3) show ?case by simp
    qed
    with cyc(4) have "j ≠ k" by auto
    from ‹k ∈ set xs› obtain ys zs where "xs = ys @ k # zs" by (meson split_list)
    with ‹distinct (j # xs)›
    have xs: "xs = ys @ k # zs" "distinct ys" "distinct zs" "k ∉ set ys" "k ∉ set zs"
             "j ∉ set ys" "j ∉ set zs" by auto
    from xs(1,4) ‹set xs ⊆ {0..k}› nat_upto_subs_top_removal have ys: "set ys ⊆ {0..k-1}" by auto
    from xs(1,5) ‹set xs ⊆ {0..k}› nat_upto_subs_top_removal have zs: "set zs ⊆ {0..k-1}" by auto
    have "D m j k (k - 1) = fw m n (k - 1) j k"
      using ‹k ≤ n› ‹j ≤ n› fw_shortest_path_up_to[OF **] by auto
    moreover have "D m k j (k - 1) = fw m n (k - 1) k j"
      using ‹k ≤ n› ‹j ≤ n› fw_shortest_path_up_to[OF **] by auto
    ultimately have "fw m n (k - 1) j k + fw m n (k - 1) k j ≤ len m j k ys + len m k j zs"
      using D_not_diag_le'[OF zs(1) xs(5,7,3), of m] D_not_diag_le'[OF ys(1) xs(6,4,2), of m]
      by (auto simp: add_mono)
    then have neg: "fw m n (k - 1) j k + fw m n (k - 1) k j < 0"
      using xs(1) ‹len m j j xs < 0› len_comp by auto
    have "fw m n k j j ≤ fw m n (k - 1) j k + fw m n (k - 1) k j"
    proof -
      from ‹k > 0› have *: "fw m n k = fwi (fw m n (k - 1)) n k n n"
        by (cases k) auto
      from fw_cyc_free_subs[OF **, THEN cyc_free_subs_diag] ‹k ≤ n› have
        "fw m n (k - 1) k k ≥ 0"
        by auto
      from fwi_step'[of "fw m n (k - 1)", OF this] ‹k ≤ n› ‹j ≤ n› show ?thesis
        by (auto intro: min.cobounded2 simp: *)
    qed
    with neg have "fw m n k j j < 0" by auto
    moreover from fw_invariant ‹j ≤ n› ‹k ≤ n› have "fw m n n j j ≤ fw m n k j j"
      by blast
    ultimately have ?thesis using ‹j ≤ n› by auto
  }
  moreover
  { assume "k = 0"
    with cyc(2,4) have "xs = [] ∨ xs = [0]"
      apply safe
      apply (case_tac xs)
       apply fastforce
      apply (rename_tac ys)
      apply (case_tac ys)
       apply auto
    done
    then have ?thesis
    proof
      assume "xs = []"
      with cyc have "m j j < 0" by auto
      with fw_mono[of j n j m n] ‹j ≤ n› have "fw m n n j j < 0" by auto
      with ‹j ≤ n› show ?thesis by auto
    next
      assume xs: "xs = [0]"
      with cyc have "m j 0 + m 0 j < 0" by auto
      moreover from ‹j ≤ n› have "fw m n 0 j j ≤ fw_upd m 0 j j j j"
        by (auto intro: order.trans[OF fwi_invariant fwi_fw_upd_mono])
      ultimately have "fw m n 0 j j < 0"
        unfolding fw_upd_def upd_def by auto
      then have "fw m n 0 j j < 0" by (metis cyc(1) less_or_eq_imp_le single_iteration_inv)
      with ‹j ≤ n› have "fw m n n j j < 0" using fw_invariant[of 0 n j n j m] by auto
      with ‹j ≤ n› show ?thesis by blast
    qed
  }
  ultimately show ?thesis by auto
qed

end (* End of local class context *)

section ‹More on Canonical Matrices›

abbreviation
  "canonical M n ≡ ∀ i j k. i ≤ n ∧ j ≤ n ∧ k ≤ n ⟶ M i k ≤ M i j + M j k"

lemma canonical_alt_def:
  "canonical M n ⟷ canonical_subs n {0..n} M"
  unfolding canonical_subs_def by auto

lemma fw_canonical:
 "canonical (fw m n n) n" if "cyc_free m n"
 using fw_canonical_subs[OF ‹cyc_free m n›] unfolding canonical_alt_def by auto

lemma canonical_len:
  "canonical M n ⟹ i ≤ n ⟹ j ≤ n ⟹ set xs ⊆ {0..n} ⟹ M i j ≤ len M i j xs"
proof (induction xs arbitrary: i)
  case Nil thus ?case by auto
next
  case (Cons x xs)
  then have "M x j ≤ len M x j xs" by auto
  from Cons.prems ‹canonical M n› have "M i j ≤ M i x + M x j" by simp
  also with Cons have "… ≤ M i x + len M x j xs" by (simp add: add_mono)
  finally show ?case by simp
qed


section ‹Additional Theorems›

lemma D_cycle_free_len_dest:
  "cycle_free m n
    ⟹ ∀ i ≤ n. ∀ j ≤ n. D m i j n = m' i j ⟹ i ≤ n ⟹ j ≤ n ⟹ set xs ⊆ {0..n}
    ⟹ ∃ ys. set ys ⊆ {0..n} ∧ len m' i j xs = len m i j ys"
proof (induction xs arbitrary: i)
  case Nil
  with Nil have "m' i j = D m i j n" by simp
  from D_dest''[OF this]
  obtain ys where "set ys ⊆ {0..n}" "len m' i j [] = len m i j ys"
  by auto
  then show ?case by auto
next
  case (Cons y ys)
  from Cons.IH[OF Cons.prems(1,2) _ ‹j ≤ n›, of y] Cons.prems(5)
  obtain zs where zs:"set zs ⊆ {0..n}" "len m' y j ys = len m y j zs" by auto
  with Cons have "m' i y = D m i y n" by simp
  from D_dest''[OF this] obtain ws where ws:"set ws ⊆ {0..n}" "m' i y = len m i y ws" by auto
  with len_comp[of m i j ws y zs] zs Cons.prems(5)
  have "len m' i j (y # ys) = len m i j (ws @ y # zs)" "set (ws @ y # zs) ⊆ {0..n}" by auto
  then show ?case by blast
qed

lemma D_cyc_free_preservation:
  "cyc_free m n ⟹ ∀ i ≤ n. ∀ j ≤ n. D m i j n = m' i j ⟹ cyc_free m' n"
proof (auto, goal_cases)
  case (1 i xs)
  from D_cycle_free_len_dest[OF _ 1(2,3,3,4)] 1(1) cycle_free_diag_equiv
  obtain ys where "set ys ⊆ {0..n} ∧ len m' i i xs = len m i i ys" by fast
  with 1(1,3) show ?case by auto
qed

abbreviation "FW m n ≡ fw m n n"

lemma FW_out_of_bounds1:
  assumes "i > n"
  shows "(FW M n) i j = M i j"
  using assms by (rule fw_out_of_bounds1)

lemma FW_out_of_bounds2:
  assumes "j > n"
  shows "(FW M n) i j = M i j"
  using assms by (rule fw_out_of_bounds2)

lemma FW_cyc_free_preservation:
  "cyc_free m n ⟹ cyc_free (FW m n) n"
  apply (rule D_cyc_free_preservation)
   apply assumption
  apply safe
  apply (rule fw_shortest_path)
  using cycle_free_diag_equiv by auto

lemma cyc_free_diag_dest':
  "cyc_free m n ⟹ i ≤ n ⟹ m i i ≥ 0"
  by (rule cyc_free_subs_diag)

lemma FW_diag_neutral_preservation:
  "∀ i ≤ n. M i i = 0 ⟹ cyc_free M n ⟹ ∀ i≤n. (FW M n) i i = 0"
proof (auto, goal_cases)
  case (1 i)
  from this(3) have "(FW M n) i i ≤ M i i" by (auto intro: fw_mono)
  with 1 have "(FW M n) i i ≤ 0" by auto
  with cyc_free_diag_dest'[OF FW_cyc_free_preservation[OF 1(2)] ‹i ≤ n›] show "FW M n i i = 0"
    by auto
qed

lemma FW_fixed_preservation:
  fixes M :: "('a::linordered_ab_monoid_add) mat"
  assumes A: "i ≤ n" "M 0 i + M i 0 = 0" "canonical (FW M n) n" "cyc_free (FW M n) n"
  shows "FW M n 0 i + FW M n i 0 = 0" using assms
proof -
  let ?M' = "FW M n"
  assume A: "i ≤ n" "M 0 i + M i 0 = 0" "canonical ?M' n" "cyc_free ?M' n"
  from ‹i ≤ n› have "?M' 0 i + ?M' i 0 ≤ M 0 i + M i 0" by (auto intro: fw_mono add_mono)
  with A(2) have "?M' 0 i + ?M' i 0 ≤ 0" by auto
  moreover from ‹canonical ?M' n› ‹i ≤ n›
  have "?M' 0 0 ≤ ?M' 0 i + ?M' i 0" by auto
  moreover from cyc_free_diag_dest'[OF  ‹cyc_free ?M' n›] have "0 ≤ ?M' 0 0" by simp
  ultimately show "?M' 0 i + ?M' i 0 = 0" by (auto simp: add_mono)
qed

lemma diag_cyc_free_neutral:
  "cyc_free M n ⟹ ∀k≤n. M k k ≤ 0 ⟹ ∀i≤n. M i i = 0"
proof (clarify, goal_cases)
  case (1 i)
  note A = this
  then have "i ≤ n ∧ set [] ⊆ {0..n}" by auto
  with A(1) have "0 ≤ M i i" by fastforce
  with A(2) ‹i ≤ n› show "M i i = 0" by auto
qed

lemma fw_upd_canonical_subs_id:
  "canonical_subs n {k} M ⟹ i ≤ n ⟹ j ≤ n ⟹ fw_upd M k i j = M"
proof (auto simp: fw_upd_def upd_def less_eq[symmetric] min.coboundedI2, goal_cases)
  case 1
  then have "M i j ≤ M i k + M k j" unfolding canonical_subs_def by auto
  then have "min (M i j) (M i k + M k j) = M i j" by (simp split: split_min)
  thus ?case by force
qed

lemma fw_upd_canonical_id:
  "canonical M n ⟹ i ≤ n ⟹ j ≤ n ⟹ k ≤ n ⟹ fw_upd M k i j = M"
  using fw_upd_canonical_subs_id[of n k M i j] unfolding canonical_subs_def by auto

lemma fwi_canonical_id:
  "fwi M n k i j = M" if "canonical_subs n {k} M" "i ≤ n" "j ≤ n" "k ≤ n"
  using that
proof (induction i arbitrary: j)
  case 0
  then show ?case by (induction j) (auto intro: fw_upd_canonical_subs_id)
next
  case Suc
  then show ?case by (induction j) (auto intro: fw_upd_canonical_subs_id)
qed

lemma fw_canonical_id:
  "fw M n k = M" if "canonical_subs n {0..k} M" "k ≤ n"
  using that by (induction k) (auto simp: canonical_subs_def fwi_canonical_id)

lemmas FW_canonical_id = fw_canonical_id[OF _ order.refl, unfolded canonical_alt_def[symmetric]]

definition "FWI M n k ≡ fwi M n k n n"

text ‹The characteristic property of ‹fwi›.›
theorem fwi_characteristic:
  "canonical_subs n (I ∪ {k::nat}) (FWI M n k) ∨ (∃ i ≤ n. FWI M n k i i < 0)" if
  "canonical_subs n I M" "I ⊆ {0..n}" "k ≤ n"
proof (cases "0 ≤ M k k")
  case True
  from fwi_canonical_extend[OF that(1,2) this ‹k ≤ n›] show ?thesis unfolding FWI_def ..
next
  case False
  with ‹k ≤ n› fwi_mono[OF ‹k ≤ n› ‹k ≤ n›, of M k n n] show ?thesis
    unfolding FWI_def by fastforce
qed

end (* End of theory *)