# Theory Timed_Automata.Floyd_Warshall

```theory Floyd_Warshall
imports Main
begin

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

subsubsection ‹Auxiliary›

lemma distinct_list_single_elem_decomp: "{xs. set xs ⊆ {0} ∧ distinct xs} = {[], [0]}"
proof (standard, goal_cases)
case 1
{ fix xs :: "'a list" assume xs: "xs ∈ {xs. set xs ⊆ {0} ∧ distinct xs}"
have "xs ∈ {[], [0]}"
proof (cases xs)
case (Cons y ys)
hence y: "y = 0" using xs by auto
with Cons xs have "ys = []" by (cases ys, auto)
thus ?thesis using y Cons by simp
qed simp
}
thus ?case by blast
qed simp

section ‹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:
"x ∈ set xs ⟹ ∃ xxs as. as @ concat (map (λ xs. x # xs) xxs) @ remove_cycles xs x ys = xs ∧ x ∉ set as"
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 rev_subsetD)

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›

text ‹
We formalize the Floyd-Warshall algorithm on a linearly ordered abelian semigroup.
However, we would not need an ‹abelian› monoid if we had the right type class.
›

fixes neutral :: 'a ("𝟭")
assumes neutl[simp]: "𝟭 + x = x"
assumes neutr[simp]: "x + 𝟭 = x"
begin

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

definition (in -) 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))"

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)

fun fw :: "'a mat ⇒ nat ⇒ nat ⇒ nat ⇒ nat ⇒ 'a mat" where
"fw m n 0       0       0        = fw_upd m 0 0 0" |
"fw m n (Suc k) 0       0        = fw_upd (fw m n k n n) (Suc k) 0 0" |
"fw m n k       (Suc i) 0        = fw_upd (fw m n k i n) k (Suc i) 0" |
"fw m n k       i       (Suc j)  = fw_upd (fw m n k i j) k i (Suc j)"

lemma fw_invariant_aux_1:
"j'' ≤ j ⟹ i ≤ n ⟹ j ≤ n ⟹ k ≤ n ⟹ fw m n k i j i' j' ≤ fw 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 (fw m n k i j) k i (Suc j) i' j' ≤ fw m n k i j i' j'" by (simp add: fw_upd_mono)
thus ?thesis using Suc False by simp
qed
qed

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

lemma fw_invariant:
"k' ≤ k ⟹ i ≤ n ⟹ j ≤ n ⟹ k ≤ n ⟹ j'' ≤ j ⟹ i'' ≤ i
⟹ fw m n k i j i' j' ≤ fw m n k' i'' j'' i' j'"
proof (induction k)
case 0 thus ?case using fw_invariant_aux_2 by auto
next
case (Suc k) thus ?case
proof (cases "k' = Suc k")
case True thus ?thesis using Suc fw_invariant_aux_2 by simp
next
case False
have "fw m n (Suc k) i j i' j' ≤ fw m n (Suc k) 0 0 i' j'"
using fw_invariant_aux_2[of i n j "Suc k" 0 0] Suc(2-) by simp
also have "… ≤ fw m n k n n i' j'" by (simp add: fw_upd_mono)
also have "… ≤ fw m n k i j i' j'" using fw_invariant_aux_2[of n n n k] False Suc by simp
also have "… ≤ fw 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 ⟹ j ≤ n ⟹ i' ≤ n ⟹ fw m n k i' j i' j' = fw 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 ⟹ j ≤ n ⟹ i ≤ n ⟹ fw m n k i j i' j' = fw 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 n i' m k]
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 ⟹ i ≤ n ⟹ j ≤ n⟹ fw m n k i j i' j' = fw 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 using single_iteration_inv'[of i' "Suc i" j' n "Suc j" m k] by simp
next
case 2 thus ?case by (simp add: fw_upd_def upd_def)
qed
qed
qed
qed

lemma fw_innermost_id:
"i ≤ n ⟹ j ≤ n ⟹ j' ≤ n ⟹ i' < i ⟹ fw m n 0 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 fw_middle_id:
"i ≤ n ⟹ j ≤ n ⟹ j' < j ⟹ i' ≤ i ⟹ fw m n 0 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 fw_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 fw_outermost_mono:
"i ≤ n ⟹ j ≤ n ⟹ fw m n 0 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 "fw m n 0 i' n (Suc i') 0 = m (Suc i') 0" using fw_innermost_id[of "Suc i'" n 0 n i' m]
using ‹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 "fw m n 0 i j' i (Suc j') = m i (Suc j')"
using fw_middle_id[of i n "Suc j'" j' i m] Suc by simp
thus ?thesis using Suc by (simp add: fw_upd_def upd_def)
qed

lemma Suc_innermost_id1:
"i ≤ n ⟹ j ≤ n ⟹ j' ≤ n ⟹ i' < i ⟹ fw m n (Suc k) i' j' i j = fw m n k i j i j"
proof (induction i' arbitrary: j')
case 0 thus ?case
proof (induction j')
case 0
hence "fw m n k n n i j = fw m n k i j i j" using single_iteration_inv[of i n j n n m k] by simp
thus ?case using 0 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 Suc_innermost_id2:
"i ≤ n ⟹ j ≤ n ⟹ j' < j ⟹ i' ≤ i ⟹ fw m n (Suc k) i' j' i j = fw m n k i j i j"
proof (induction i' arbitrary: j')
case 0
hence "fw m n k n n i j = fw m n k i j i j" using single_iteration_inv[of i n j n n m k] by simp
with 0 show ?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: fw_upd_def upd_def)
qed
next
case (Suc i') thus ?case
proof (induction j')
case 0 thus ?case using Suc_innermost_id1 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 Suc_innermost_id1':
"i ≤ n ⟹ j ≤ n ⟹ j' ≤ n ⟹ i' < i ⟹ fw m n (Suc k) i' j' i j = fw m n k n n i j"
proof goal_cases
case 1
hence "fw m n (Suc k) i' j' i j = fw m n k i j i j" using Suc_innermost_id1 by simp
thus ?thesis using 1 single_iteration_inv[of i n] by simp
qed

lemma Suc_innermost_id2':
"i ≤ n ⟹ j ≤ n ⟹ j' < j ⟹ i' ≤ i ⟹ fw m n (Suc k) i' j' i j = fw m n k n n i j"
proof goal_cases
case 1
hence "fw m n (Suc k) i' j' i j = fw m n k i j i j" using Suc_innermost_id2 by simp
thus ?thesis using 1 single_iteration_inv[of i n] by simp
qed

lemma Suc_innermost_mono:
"i ≤ n ⟹ j ≤ n ⟹ fw m n (Suc k) i j i j ≤ fw m n k i j i j"
proof (cases j)
case 0
assume "i ≤ n"
thus ?thesis
proof (cases i)
case 0 thus ?thesis using ‹j = 0› single_iteration_inv[of 0 n 0 n n m k]
next
case (Suc i')
thus ?thesis using Suc_innermost_id1 ‹i ≤ n› ‹j = 0›
by (auto simp: fw_upd_def upd_def local.min.coboundedI1)
qed
next
case (Suc j')
assume "i ≤ n" "j ≤ n"
thus ?thesis using Suc Suc_innermost_id2 by (auto simp: fw_upd_def upd_def local.min.coboundedI1)
qed

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

lemma fw_mono:
"i ≤ n ⟹ j ≤ n ⟹ i' ≤ n ⟹ j' ≤ n ⟹ fw m n k i j i' j' ≤ m i' j'"
proof (cases k)
case 0
assume 0: "i ≤ n" "j ≤ n" "i' ≤ n" "j' ≤ n" "k = 0"
thus ?thesis
proof (cases "i' ≤ i")
case False thus ?thesis using 0 fw_innermost_id by simp
next
case True thus ?thesis
proof (cases "j' ≤ j")
case True
have "fw m n 0 i j i' j' ≤ fw m n 0 i' j' i' j'" using fw_invariant True ‹i' ≤ i› 0 by simp
also have "fw m n 0 i' j' i' j' ≤ m i' j'" using 0 fw_outermost_mono by blast
finally show ?thesis by (simp add: ‹k = 0›)
next
case False thus ?thesis
proof (cases "i = i'", goal_cases)
case 1 then show ?thesis using fw_middle_id[of i' n j' j i' m] 0 by simp
next
case 2
then show ?case
using single_iteration_inv'[of i' i j' n j m 0] ‹i' ≤ i› fw_middle_id[of i' n j' j i' m]
fw_outermost_mono[of i' n j' m] 0
by simp
qed
qed
qed
next
case (Suc k)
assume prems: "i ≤ n" "j ≤ n" "i' ≤ n" "j' ≤ n"
thus ?thesis
proof (cases "i' ≤ i ∧ j' ≤ j")
case True
hence "fw m n (Suc k) i j i' j' = fw m n (Suc k) i' j' i' j'"
using prems single_iteration_inv by blast
thus ?thesis using Suc prems fw_mono' by auto
next
case False thus ?thesis
proof auto
assume "¬ i' ≤ i"
thus ?thesis using Suc prems fw_mono' Suc_innermost_id1 by auto
next
assume "¬ j' ≤ j"
hence "j < j'" by simp
show ?thesis
proof (cases "i ≤ i'")
case True
thus ?thesis using Suc prems Suc_innermost_id2 ‹j < j'› fw_mono' by auto
next
case False
thus ?thesis using single_iteration_inv' Suc prems fw_mono' by auto
qed
qed
qed
qed

assumes "𝟭 ≤ b"
shows "a ≤ a + b"
using neutr add_mono assms by force

assumes "𝟭 ≤ b"
shows "a ≤ b + a"
using neutr add_mono assms by force

lemma fw_step_0:
"m 0 0 ≥ 𝟭 ⟹ i ≤ n ⟹ j ≤ n ⟹ fw m n 0 i j i j = min (m i j) (m i 0 + m 0 j)"
proof (induction i)
case 0 thus ?case
proof (cases j)
case 0 thus ?thesis by (simp add: fw_upd_def upd_def)
next
case (Suc j)
hence "fw m n 0 0 j 0 (Suc j) = m 0 (Suc j)" using 0 fw_middle_id[of 0 n "Suc j" j 0 m] by fast
moreover have "fw m n 0 0 j 0 0 = m 0 0" using single_iteration_inv[of 0 0 0 j n m 0] Suc 0
ultimately show ?thesis using Suc by (simp add: fw_upd_def upd_def)
qed
next
case (Suc i)
note A = this
show ?case
proof (cases j)
case 0
have "fw m n 0 i n (Suc i) 0 = m (Suc i) 0" using fw_innermost_id[of "Suc i" n 0 n i m] Suc by simp
moreover have "fw m n 0 i n 0 0 = m 0 0" using Suc single_iteration_inv[of 0 i 0 n n m 0]
ultimately show ?thesis using 0 by (simp add: fw_upd_def upd_def)
next
case (Suc j)
have *: "fw m n 0 0 j 0 0 = m 0 0" using single_iteration_inv[ of 0 0 0 j n m 0] A Suc
have **: "fw m n 0 i n 0 0 = m 0 0" using single_iteration_inv[of 0 i 0 n n m 0] A
have "m 0 (Suc j) = fw_upd m 0 0 (Suc j) 0 (Suc j)" using ‹m 0 0 >= 𝟭›
also have "… = fw m n 0 0 (Suc j) 0 (Suc j)" using fw_middle_id[of 0 n "Suc j" j 0 m] Suc A(4)
by (simp add: fw_upd_def upd_def *)
finally have ***: "fw m n 0 (Suc i) j 0 (Suc j) = m 0 (Suc j)"
using single_iteration_inv'[of 0 "Suc i" "Suc j" n j m 0] A Suc by simp
have "m (Suc i) 0 = fw_upd m 0 (Suc i) 0 (Suc i) 0" using ‹m 0 0 >= 𝟭›
also have "… = fw m n 0 (Suc i) 0 (Suc i) 0"
using fw_innermost_id[of "Suc i" n 0 n i m] ‹Suc i ≤ n› ** by (simp add: fw_upd_def upd_def)
finally have "fw m n 0 (Suc i) j (Suc i) 0 = m (Suc i) 0"
using single_iteration_inv A Suc by auto
moreover have "fw m n 0 (Suc i) j (Suc i) (Suc j) = m (Suc i) (Suc j)"
using fw_middle_id A Suc by simp
ultimately show ?thesis using Suc *** by (simp add: fw_upd_def upd_def)
qed
qed

lemma fw_step_Suc:
"∀ k'≤n. fw m n k n n k' k' ≥ 𝟭 ⟹ i ≤ n ⟹ j ≤ n ⟹ Suc k ≤ n
⟹ fw m n (Suc k) i j i j = min (fw m n k n n i j) (fw m n k n n i (Suc k) + fw m n k n n (Suc k) j)"
proof (induction i)
case 0 thus ?case
proof (cases j)
case 0 thus ?thesis by (simp add: fw_upd_def upd_def)
next
case (Suc j)
then have
"fw m n k n n 0 (Suc j) = fw m n (Suc k) 0 j 0 (Suc j)"
using 0(2-) Suc_innermost_id2' by simp
moreover have "fw m n (Suc k) 0 j 0 (Suc k) = fw m n k n n 0 (Suc k)"
proof (cases "j < Suc k")
case True thus ?thesis using 0 Suc_innermost_id2' by simp
next
case False
hence
"fw m n (Suc k) 0 k 0 (Suc k) = fw m n k n n 0 (Suc k)"
using 0(2-) Suc Suc_innermost_id2' by simp
moreover have "fw m n (Suc k) 0 k (Suc k) (Suc k) = fw m n k n n (Suc k) (Suc k)"
using 0(2-) Suc Suc_innermost_id2' by simp
moreover have "fw m n (Suc k) 0 j 0 (Suc k) = fw m n (Suc k) 0 (Suc k) 0 (Suc k)"
using False single_iteration_inv 0(2-) Suc by force
ultimately show ?thesis using 0(1)
by (auto simp add: fw_upd_def upd_def ‹Suc k ≤ n› min_def intro: add_mono_neutr)
qed
moreover have "fw m n k n n (Suc k) (Suc j) = fw m n (Suc k) 0 j (Suc k) (Suc j)"
using 0(2-) Suc Suc_innermost_id2' by simp
ultimately show ?thesis using Suc by (simp add: fw_upd_def upd_def)
qed
next
case (Suc i)
note A = this
show ?case
proof (cases j)
case 0
hence
"fw m n (Suc k) i n (Suc i) 0 = fw m n k n n (Suc i) 0"
using Suc_innermost_id1' ‹Suc i ≤ n› by simp
moreover have "fw m n (Suc k) i n (Suc i) (Suc k) = fw m n k n n (Suc i) (Suc k)"
using Suc_innermost_id1' A(3,5) by simp
moreover have "fw m n (Suc k) i n (Suc k) 0 = fw m n k n n (Suc k) 0"
proof (cases "i < Suc k")
case True thus ?thesis using Suc_innermost_id1' A(3,5) by simp
next
case False
have "fw m n (Suc k) k n (Suc k) (Suc k) = fw m n k n n (Suc k) (Suc k)"
using Suc_innermost_id1' ‹Suc i ≤ n› False by simp
moreover have "fw m n (Suc k) k n (Suc k) 0 = fw m n k n n (Suc k) 0"
using Suc_innermost_id1' ‹Suc i ≤ n› False by simp
moreover have "fw m n (Suc k) i n (Suc k) 0 = fw m n (Suc k) (Suc k) 0 (Suc k) 0"
using single_iteration_inv ‹Suc i ≤ n› False by simp
ultimately show ?thesis using Suc(2)
by (auto simp add: fw_upd_def upd_def ‹Suc k ≤ n› min_def intro: add_mono_neutl)
qed
ultimately show ?thesis using 0 by (simp add: fw_upd_def upd_def)
next
case (Suc j)
hence "fw m n (Suc k) (Suc i) j (Suc i) (Suc j) = fw m n k n n (Suc i) (Suc j)"
using Suc_innermost_id2' A(3,4) by simp
moreover have "fw m n (Suc k) (Suc i) j (Suc i) (Suc k) = fw m n k n n (Suc i) (Suc k)"
proof (cases "j < Suc k")
case True thus ?thesis using Suc A(3-) Suc_innermost_id2' by simp
next
case False
have *:"fw m n (Suc k) (Suc i) k (Suc i) (Suc k) = fw m n k n n (Suc i) (Suc k)"
using Suc_innermost_id2' A(3,5) by simp
have **:"fw m n (Suc k) (Suc i) k (Suc k) (Suc k) = fw m n k n n (Suc k) (Suc k)"
proof (cases "Suc i ≤ Suc k")
case True thus ?thesis using Suc_innermost_id2' A(5) by simp
next
case False
hence "fw m n (Suc k) (Suc i) k (Suc k) (Suc k) = fw m n (Suc k) (Suc k) (Suc k) (Suc k) (Suc k)"
using single_iteration_inv'[of "Suc k" "Suc i" "Suc k" n k m "Suc k"] A(3) by simp
moreover have "fw m n (Suc k) (Suc k) k (Suc k) (Suc k) = fw m n k n n (Suc k) (Suc k)"
using Suc_innermost_id2' A(5) by simp
ultimately show ?thesis using A(2)
by (auto simp add: fw_upd_def upd_def ‹Suc k ≤ n› min_def intro: add_mono_neutl)
qed
have "fw m n (Suc k) (Suc i) j (Suc i) (Suc k) = fw m n (Suc k) (Suc i) (Suc k) (Suc i) (Suc k)"
using False single_iteration_inv[of "Suc i" "Suc i" "Suc k" j n m "Suc k"] A(3-) Suc by simp
also have "… = fw m n k n n (Suc i) (Suc k)" using * ** A(2)
by (auto simp add: fw_upd_def upd_def ‹Suc k ≤ n› min_def intro: add_mono_neutr)
finally show ?thesis by simp
qed
moreover have "fw m n (Suc k) (Suc i) j (Suc k) (Suc j) = fw m n k n n (Suc k) (Suc j)"
proof (cases "Suc i ≤ Suc k")
case True thus ?thesis using Suc_innermost_id2' Suc A(3-5) by simp
next
case False
have "fw m n (Suc k) (Suc k) j (Suc k) (Suc k) = fw m n k n n (Suc k) (Suc k)"
proof (cases "j < Suc k")
case True thus ?thesis using Suc_innermost_id2' A(5) by simp
next
case False
hence "fw m n (Suc k) (Suc k) j (Suc k) (Suc k) = fw m n (Suc k) (Suc k) (Suc k) (Suc k) (Suc k)"
using single_iteration_inv A(3,4) Suc by simp
moreover have "fw m n (Suc k) (Suc k) k (Suc k) (Suc k) = fw m n k n n (Suc k) (Suc k)"
using Suc_innermost_id2' A(5) by simp
ultimately show ?thesis using A(2)
by (auto simp add: fw_upd_def upd_def ‹Suc k ≤ n› min_def intro: add_mono_neutl)
qed
moreover have "fw m n (Suc k) (Suc k) j (Suc k) (Suc j) = fw m n k n n (Suc k) (Suc j)"
using Suc_innermost_id2' Suc A(3-5) by simp
ultimately have "fw m n (Suc k) (Suc k) (Suc j) (Suc k) (Suc j) = fw m n k n n (Suc k) (Suc j)"
using A(2) by (auto simp add: fw_upd_def upd_def ‹Suc k ≤ n› min_def intro: add_mono_neutl)
moreover have "fw m n (Suc k) (Suc i) j (Suc k) (Suc j) = fw m n (Suc k) (Suc k) (Suc j) (Suc k) (Suc j)"
using single_iteration_inv'[of "Suc k" "Suc i" "Suc j" n j m "Suc k"] Suc A(3-) False  by simp
moreover have "fw m n (Suc k) (Suc k) k (Suc k) (Suc k) = fw m n k n n (Suc k) (Suc k)"
using Suc_innermost_id2' A(5) by simp
ultimately show ?thesis using A(2) by (simp add: fw_upd_def upd_def)
qed
ultimately show ?thesis using Suc by (simp add: fw_upd_def upd_def)
qed
qed

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: 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: assoc)

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 < 𝟭" using assms
proof (induction xss arbitrary: xs as)
case Nil
with Nil show ?case
proof (cases "len m i i as ≥ 𝟭", 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 ≥ 𝟭", goal_cases)
case 1
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 < 𝟭" 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 < 𝟭"
proof (rule ccontr)
assume "a + b < b" "¬ a < 𝟭"
hence "a ≥ 𝟭" 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 < 𝟭" using assms
proof (induction xss arbitrary: xs as)
case Nil
show ?case
proof (cases "len m j j as ≥ 𝟭")
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 < 𝟭" by blast
ultimately show ?thesis by blast
next
case False
hence "len m i j xs < len m i j ?xs" by auto
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 < 𝟭" 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 < 𝟭"
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 < 𝟭"
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 (in -) 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 < 𝟭 ∧ 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"
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

section ‹Definition of Shortest Paths›

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 (in -) distinct_length_le:"finite s ⟹ set xs ⊆ s ⟹ distinct xs ⟹ length xs ≤ card s"
by (metis card_mono distinct_card)

lemma D_base_finite:
"finite {len m i j xs | xs. set xs ⊆ {0..k} ∧ distinct xs}"
using finite_subset_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 ≥ 𝟭"

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 ≥ 𝟭"
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"

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 ≥ 𝟭"

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 ≥ 𝟭"
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 ≥ 𝟭"
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<```