# Theory 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 (in -) 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 ≥ 𝟭"

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

section ‹Result Under The Absence of Negative Cycles›

text ‹
This proves that the algorithm correctly computes shortest paths under the absence of negative
cycles by a standard argument.
›

theorem fw_shortest_path_up_to:
"cycle_free_up_to m k n ⟹ i' ≤ i ⟹ j' ≤ j ⟹ i ≤ n ⟹ j ≤ n ⟹ k ≤ n
⟹ D m i' j' k = fw m n k i j i' j'"
proof (induction k arbitrary: i j i' j')
case 0
from cycle_free_up_to_diag[OF 0(1)] have diag: "∀ k ≤ n. m k k ≥ 𝟭" by auto
then have m_diag: "m 0 0 ≥ 𝟭" by simp
let ?S = "{len m i' j' xs |xs. set xs ⊆ {0} ∧ i' ∉ set xs ∧ j' ∉ set xs ∧ distinct xs}"
show ?case unfolding D_def
proof (simp, rule Min_eqI)
have "?S ⊆ {len m i' j' xs |xs. set xs ⊆ {0..0} ∧ distinct xs}" by auto
thus "finite ?S" using D_base_finite[of m i' j' 0] by (rule finite_subset)
next
fix l assume "l ∈ ?S"
then obtain xs where l: "l = len m i' j' xs" and xs: "xs = [] ∨ xs = [0]"
using distinct_list_single_elem_decomp by auto
{ assume "xs = []"
have "fw m n 0 i j i' j' ≤ fw m n 0 0 0 i' j'" using fw_invariant 0 by blast
also have "… ≤ m i' j'" by (cases "i' = 0 ∧ j' = 0") (simp add: fw_upd_def upd_def)+
finally have "fw m n 0 i j i' j' ≤ l" using ‹xs = []› l by simp
}
moreover
{ assume "xs = [0]"
have "fw m n 0 i j i' j' ≤ fw m n 0 i' j' i' j'" using fw_invariant 0 by blast
also have "… ≤ m i' 0 + m 0 j'"
proof (cases j')
assume "j' = 0"
show ?thesis
proof (cases i')
assume "i' = 0"
thus ?thesis using ‹j' = 0› by (simp add: fw_upd_def upd_def)
next
fix i'' assume i'': "i' = Suc i''"
have "fw_upd (fw m n 0 i'' n) 0 (Suc i'') 0 (Suc i'') 0 ≤ fw m n 0 i'' n (Suc i'') 0"
also have "… ≤ m (Suc i'') 0" using fw_mono 0 i'' by simp
finally show ?thesis using ‹j' = 0› m_diag i'' neutr add_mono by fastforce
qed
next
fix j'' assume j'': "j' = Suc j''"
have "fw_upd (fw m n 0 i' j'') 0 i' (Suc j'') i' (Suc j'')
≤ fw m n 0 i' j'' i' 0 + fw m n 0 i' j'' 0 (Suc j'') "
also have "… ≤ m i' 0 + m 0 (Suc j'')"
using fw_mono[of i' n j'' i' 0 m 0] fw_mono[of i' n j'' 0 "Suc j''" m 0 ] j'' 0
finally show ?thesis using j'' by simp
qed
finally have "fw m n 0 i j i' j' ≤ l" using ‹xs = [0]› l by simp
}
ultimately show "fw m n 0 i j i' j' ≤ l" using xs by auto
next
have A: "fw m n 0 i j i' j' = fw m n 0 i' j' i' j'" using single_iteration_inv 0 by blast
have "fw m n 0 i' j' i' j' = min (m i' j') (m i' 0 + m 0 j')"
using 0 by (simp add: fw_step_0[of m, OF m_diag])
hence
"fw m n 0 i' j' i' j' = m i' j'
∨ (fw m n 0 i' j' i' j' = m i' 0 + m 0 j'∧ m i' 0 + m 0 j' ≤ m i' j')"
thus "fw m n 0 i j i' j' ∈ ?S"
proof (standard, goal_cases)
case 1
hence "fw m n 0 i j i' j' = len m i' j' []" using A by auto
thus ?case by fastforce
next
case 2
hence *:"fw m n 0 i j i' j' = len m i' j' [0]" using A by auto
thus ?case
proof (cases "i' = 0 ∨ j' = 0")
case False thus ?thesis using * by fastforce
next
case True
{ assume "i' = 0"
from diag have "m 0 0 + m 0 j' ≥ m 0 j'" by (auto intro: add_mono_neutl)
with ‹i' = 0› have "fw m n 0 i j i' j' = len m 0 j' []" using 0 A 2 by auto
} moreover
{ assume "j' = 0"
from diag have "m i' 0 + m 0 0 ≥ m i' 0" by (auto intro: add_mono_neutr)
with ‹j' = 0› have "fw m n 0 i j i' j' = len m i' 0 []" using 0 A 2 by auto
}
ultimately have "fw m n 0 i j i' j' = len m i' j' []" using True by auto
then show ?thesis by fastforce
qed
qed
qed
next
case (Suc k)
from cycle_free_up_to_diag[OF Suc.prems(1)] have diag: "∀ k ≤ n. m k k ≥ 𝟭" by auto
from Suc.prems have cycle_free_to_k:
"cycle_free_up_to m k n" by (fastforce simp add: cycle_free_up_to_def)
{ fix k' assume "k' ≤ n"
with Suc cycle_free_to_k have "D m k' k' k = fw m n k n n k' k'" by auto
from D_dest''[OF this[symmetric]] obtain xs where
"set xs ⊆ {0..k}" "fw m n k n n k' k'= len m k' k' xs"
by auto
with Suc(2) ‹Suc k ≤ n› ‹k' ≤ n› have "fw m n k n n k' k' ≥ 𝟭"
unfolding cycle_free_up_to_def by force
}
hence K: "∀k'≤n. fw m n k n n k' k' ≥ 𝟭" by simp
let ?S = "λ k i j. {len m i j xs |xs. set xs ⊆ {0..k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}"
show ?case
proof (rule D_eqI2)
show "cycle_free_up_to m (Suc k) n" using Suc.prems(1) .
next
show "i' ≤ n" using Suc.prems by simp
next
show "j' ≤ n" using Suc.prems by simp
next
show "Suc k ≤ n" using Suc.prems by simp
next
fix l assume "l ∈ {len m i' j' xs | xs. set xs ⊆ {0..Suc k} ∧ i' ∉ set xs ∧ j' ∉ set xs ∧ distinct xs}"
then obtain xs where xs:
"l = len m i' j' xs" "set xs ⊆ {0..Suc k}" "i' ∉ set xs" "j' ∉ set xs" "distinct xs"
by auto
have IH: "D m i' j' k = fw m n k i j i' j'" using cycle_free_to_k Suc by auto
have fin:
"finite {len m i' j' xs |xs. set xs ⊆ {0..k} ∧ i' ∉ set xs ∧ j' ∉ set xs ∧ distinct xs}"
using D_base_finite'' by simp
show "fw m n (Suc k) i j i' j' ≤ l"
proof (cases "Suc k ∈ set xs")
case False
hence "set xs ⊆ {0..k}" using xs(2) using atLeastAtMostSuc_conv by auto
hence
"l ∈ {len m i' j' xs | xs. set xs ⊆ {0..k} ∧ i' ∉ set xs ∧ j' ∉ set xs ∧ distinct xs}"
using xs by auto
with Min_le[OF fin this] have "fw m n k i j i' j' ≤ l" using IH by (simp add: D_def)
thus ?thesis using fw_invariant[of k "Suc k" i n j j i m i' j'] Suc.prems by simp
next
case True
then obtain ys zs where ys_zs_id: "xs = ys @ Suc k # zs" by (meson split_list)
with xs(5) have ys_zs: "distinct ys" "distinct zs" "Suc k ∉ set ys" "Suc k ∉ set zs"
"set ys ∩ set zs = {}" by auto
have "i' ≠ Suc k" "j' ≠ Suc k" using xs(3,4) True by auto

have "set ys ⊆ {0..k}" using ys_zs(3) xs(2) ys_zs_id using atLeastAtMostSuc_conv by auto
hence "len m i' (Suc k) ys ∈ ?S k i' (Suc k)" using ys_zs_id ys_zs xs(3) by fastforce
with Min_le[OF _ this] have "Min (?S k i' (Suc k)) ≤ len m i' (Suc k) ys"
using D_base_finite'[of m i' "Suc k" k] ‹i' ≠ Suc k› by fastforce
moreover have "fw m n k n n i' (Suc k)  =  D m i' (Suc k) k"
using Suc.IH[OF cycle_free_to_k, of i' n] Suc.prems by auto
ultimately have *:"fw m n k n n i' (Suc k) ≤ len m i' (Suc k) ys" using ‹i' ≠ Suc k›
by (auto simp: D_def)

have "set zs ⊆ {0..k}" using ys_zs(4) xs(2) ys_zs_id using atLeastAtMostSuc_conv by auto
hence "len m (Suc k) j' zs ∈ ?S k (Suc k) j'" using ys_zs_id ys_zs xs(3,4,5) by fastforce
with Min_le[OF _ this] have "Min (?S k (Suc k) j') ≤ len m (Suc k) j' zs"
using D_base_finite'[of m "Suc k" j' k] ‹j' ≠ Suc k› by fastforce
moreover have "fw m n k n n (Suc k) j'  =  D m (Suc k) j' k"
using Suc.IH[OF cycle_free_to_k, of "Suc k" n j' n] Suc.prems by auto
ultimately have **:"fw m n k n n (Suc k) j' ≤ len m (Suc k) j' zs" using ‹j' ≠ Suc k›
by (auto simp: D_def)

have len_eq: "l = len m i' (Suc k) ys + len m (Suc k) j' zs"
by (simp add: xs(1) len_decomp[OF ys_zs_id, symmetric] ys_zs_id)
have "fw m n (Suc k) i' j' i' j' ≤ fw m n k n n i' (Suc k) + fw m n k n n (Suc k) j'"
using fw_step_Suc[of n m k i' j', OF K] Suc.prems(2-) by simp
hence "fw m n (Suc k) i' j' i' j' ≤ l"
using fw_step_Suc[of n m k i j] Suc.prems(3-) * ** len_eq add_mono by fastforce
thus ?thesis using fw_invariant[of "Suc k" "Suc k" i n j j' i' m i' j'] Suc.prems(2-) by simp
qed
next
have "fw m n (Suc k) i j i' j' = fw m n (Suc k) i' j' i' j'"
using single_iteration_inv[OF Suc.prems(2-5)] .
also have "… = 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')"
using fw_step_Suc[OF K] Suc.prems(2-) by simp
finally show "fw m n (Suc k) i j i' j' ∈ {len m i' j' xs | xs. set xs ⊆ {0..Suc k}}"
proof (cases "fw m n (Suc k) i j i' j' = fw m n k n n i' j'", goal_cases)
case True
have "fw m n (Suc k) i j i' j' = D m i' j' k"
using Suc.IH[OF cycle_free_to_k, of i' n j' n] Suc.prems(2-) True by simp
from D_dest'[OF this] show ?thesis by blast
next
case 2
hence A:"fw m n (Suc k) i j i' j' = fw m n k n n i' (Suc k) + fw m n k n n (Suc k) j'"
by (metis ord.min_def)
have "fw m n k n n i' j' = D m i' j' k"
using Suc.IH[OF cycle_free_to_k, of i' n j' n] Suc.prems by simp
from D_dest[OF this] have B:"fw m n k n n i' j' ∈ ?S (Suc k) i' j'"
by blast
have "fw m n k n n i' (Suc k) = D m i' (Suc k) k"
using Suc.IH[OF cycle_free_to_k, of i' n "Suc k" n] Suc.prems by simp
from D_dest'[OF this] obtain xs where xs:
"fw m n k n n i' (Suc k) = len m i' (Suc k) xs" "set xs ⊆ {0..Suc k}" by blast
have "fw m n k n n (Suc k) j' = D m (Suc k) j' k"
using Suc.IH[OF cycle_free_to_k, of "Suc k" n j' n] Suc.prems by simp
from D_dest'[OF this] obtain ys where ys:
"fw m n k n n (Suc k) j' = len m (Suc k) j' ys" "set ys ⊆ {0..Suc k}" by blast
from A xs(1) ys(1) len_comp
have "fw m n (Suc k) i j i' j' = len m i' j' (xs @ Suc k # ys)" by simp
moreover have "set (xs @ Suc k # ys) ⊆ {0..Suc k}" using xs(2) ys(2) by auto
ultimately show ?thesis by blast
qed
qed
qed

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 ⟹ 𝟭 ≤ m i i"
using cycle_free_up_to_diag[OF cycle_free_cycle_free_up_to] by blast

corollary fw_shortest_path:
"cycle_free m n ⟹ i' ≤ i ⟹ j' ≤ j ⟹ i ≤ n ⟹ j ≤ n ⟹ k ≤ n
⟹ D m i' j' k = fw m n k i j i' j'"
using fw_shortest_path_up_to[OF cycle_free_cycle_free_up_to] by auto

corollary fw_shortest:
assumes "cycle_free m n" "i ≤ n" "j ≤ n" "k ≤ n"
shows "fw m n n n n i j ≤ fw m n n n n i k + fw m n n n n k j"
proof (rule ccontr, goal_cases)
case 1
let ?S = "λ i j. {len m i j xs |xs. set xs ⊆ {0..n}}"
let ?FW = "fw m n n n n"
from assms fw_shortest_path
have FW: "?FW i j = D m i j n" "?FW i k = D m i k n" "?FW k j = D m k j n" by auto
with D_dest'' FW have "?FW i k ∈ ?S i k" "?FW k j ∈ ?S k j" by auto
then obtain xs ys where xs_ys:
"?FW i k = len m i k xs" "set xs ⊆ {0..n}" "?FW k j = len m k j ys" "set ys ⊆ {0..n}" by auto
let ?zs = "rem_cycles i j (xs @ k # ys)"
have *:"?FW i j = Min {len m i j xs |xs. set xs ⊆ {0..n} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}"
using FW(1) unfolding D_def .
have "set (xs @ k # ys) ⊆ {0..n}" using assms xs_ys by fastforce
from cycle_free_dest [OF ‹cycle_free m n› ‹i ≤ n› ‹j ≤ n› this]
have **:"len m i j ?zs ≤ len m i j (xs @ k # ys)" by auto
moreover have "i ∉ set ?zs" "j ∉ set ?zs" "distinct ?zs"
using rem_cycles_distinct remove_all_removes rem_cycles_removes_last by fast+
moreover have "set ?zs ⊆ {0..n}" using rem_cycles_subs[of i j"xs @ k # ys"] xs_ys assms by fastforce
ultimately have
"len m i j ?zs ∈ {len m i j xs |xs. set xs ⊆ {0..n} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}"
by blast
with * have "?FW i j ≤ len m i j ?zs" using D_base_finite'' by auto
with ** xs_ys len_comp 1 show ?case by auto
qed

section ‹Result Under the Presence of Negative Cycles›

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

lemma fw_Suc:
"i ≤ n ⟹ j ≤ n ⟹ i' ≤ n ⟹ j' ≤ n ⟹ fw m n (Suc k) i' j' i j ≤ fw m n k n n i j"
by (metis Suc_innermost_id1' Suc_innermost_id2 Suc_innermost_mono linorder_class.not_le order.eq_iff
preorder_class.order_refl single_iteration_inv single_iteration_inv')

lemma negative_len_shortest:
"length xs = n ⟹ len m i i xs < 𝟭
⟹ ∃ j ys. distinct (j # ys) ∧ len m j j ys < 𝟭 ∧ 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 < 𝟭")
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 < 𝟭"
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 < 𝟭")
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 ≥ 𝟭" 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 < 𝟭" by auto
with len_comp have "len m i i (as @ a # cs) < 𝟭" by auto
from less.IH[OF _ _ this, of "length (as @ a # cs)"] xs less.prems
show ?thesis by auto
qed
qed
qed
qed
qed

theorem FW_neg_cycle_detect:
"¬ cycle_free m n ⟹ ∃ i ≤ n. fw m n n n n i i < 𝟭"
proof -
assume A: "¬ cycle_free m n"
let ?K = "{k. k ≤ n ∧ ¬ cycle_free_up_to m k n}"
let ?k = "Min ?K"
have not_empty_K: "?K ≠ {}" using not_cylce_free_dest[OF A(1)] by auto
have "finite ?K" by auto
with not_empty_K have *:
"∀ k' < ?k. cycle_free_up_to m k' n"
by (auto, metis le_trans less_or_eq_imp_le preorder_class.less_irrefl)
from linorder_class.Min_in[OF ‹finite ?K› ‹?K ≠ {}›] have
"¬ cycle_free_up_to m ?k n" "?k ≤ n"
by auto
then have "∃ xs j. j ≤ n ∧ len m j j xs < 𝟭 ∧ set xs ⊆ {0..?k}" unfolding cycle_free_up_to_def
proof (auto, goal_cases)
case (2 i xs) then have "len m i i xs < 𝟭" by auto
with 2 show ?case by auto
next
case (1 i xs j)
then have "len m i j (rem_cycles i j xs) > len m i j xs" by auto
from negative_cycle_dest[OF this]
obtain i' ys where ys: "i' ∈ set (i # j # xs)" "len m i' i' ys < 𝟭" "set ys ⊆ set xs" by blast
from ys(1) 1(2-4) show ?case
proof (auto, goal_cases)
case 1
with ys(2,3) show ?case by auto
next
case 2
with ys(2,3) show ?case by auto
next
case 3
with ‹?k ≤ n› have "i' ≤ n" unfolding cycle_free_up_to_def by auto
with 3 ys(2,3) show ?case by auto
qed
qed
then obtain a as where a_as: "a ≤ n ∧ len m a a as < 𝟭 ∧ 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 < 𝟭 ∧ 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 < 𝟭" "distinct (j # xs)"
by auto
{ assume "?k > 0"
then have "?k - 1 < ?k" by simp
with * have **:"cycle_free_up_to m (?k - 1) n" 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
from cycle_free_up_to_loop_dest[OF ‹j ≤ n› this ‹cycle_free_up_to m (?k - 1) n›] cyc(3)
show ?case by auto
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) n n j ?k"
using ‹?k ≤ n› ‹j ≤ n› fw_shortest_path_up_to[OF **, of j n ?k n] by auto
moreover have "D m ?k j (?k - 1) = fw m n (?k - 1) n n ?k j"
using ‹?k ≤ n› ‹j ≤ n› fw_shortest_path_up_to[OF **, of ?k n j n] by auto
ultimately have "fw m n (?k - 1) n n j ?k + fw m n (?k - 1) n n ?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) n n j ?k + fw m n (?k - 1) n n ?k j < 𝟭"
using xs(1) ‹len m j j xs < 𝟭› len_comp by auto
have "fw m n ?k j j j j ≤ fw m n (?k - 1) n n j ?k + fw m n (?k - 1) n n ?k j"
proof (cases "j = 0")
case True
with‹?k > 0› fw.simps(2)[of m n "?k - 1"]
have "fw m n ?k j j = fw_upd (fw m n (?k - 1) n n) ?k j j" by auto
then have "fw m n ?k j j j j ≤ fw m n (?k - 1) n n j ?k + fw m n (?k - 1) n n ?k j"
then show ?thesis by auto
next
case False
with fw.simps(4)[of m n ?k j "j - 1"]
have "fw m n ?k j j = fw_upd (fw m n ?k j (j -1)) ?k j j" by simp
then have *: "fw m n ?k j j j j ≤ fw m n ?k j (j -1) j ?k + fw m n ?k j (j -1) ?k j"
have "j - 1 < n" using ‹j ≤ n› False by auto
then have "fw m n ?k j (j -1) j ?k ≤ fw m n (?k - 1) n n j ?k"
using fw_Suc[of j n ?k j "j - 1" m "?k - 1"] ‹j ≤ n› ‹?k ≤ n› ‹?k > 0› by auto
moreover have "fw m n ?k j (j -1) ?k j ≤ fw m n (?k - 1) n n ?k j"
using fw_Suc[of ?k n j j "j - 1" m "?k - 1"] ‹j ≤ n› ‹?k ≤ n› ‹?k > 0› by auto
ultimately have "fw m n ?k j j j j ≤ fw m n (?k - 1) n n j ?k + fw m n (?k - 1) n n ?k j"
then show ?thesis by auto
qed
with neg have "fw m n ?k j j j j < 𝟭" by auto
moreover have "fw m n n n n j j ≤ fw m n ?k j j j j" using fw_invariant ‹j≤n› ‹?k ≤ n› by auto
ultimately have "fw m n n n n j j < 𝟭" using neg by auto
with ‹j≤n› have ?thesis 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 < 𝟭" by auto
with fw_mono[of n n n j j m n] ‹j ≤ n› have "fw m n n n n j j < 𝟭" by auto
with ‹j ≤ n› show ?thesis by auto
next
assume xs: "xs = [0]"
with cyc have "m j 0 + m 0 j < 𝟭" by auto
then have "fw m n 0 j j j j < 𝟭"
proof (cases "j = 0", goal_cases)
case 1
have "m j j < 𝟭"
proof (rule ccontr)
assume "¬ m j j < 𝟭"
with 1 have "m 0 0 ≥ 𝟭" by simp
with add_mono have "m 0 0 + m 0 0 ≥ 𝟭" by fastforce
with 1 show False by simp
qed
with fw_mono[of j n j j j m 0] ‹j ≤ n› show ?thesis by auto
next
case 2
with fw.simps(4)[of m n 0 j "j - 1"]
have "fw m n 0 j j = fw_upd (fw m n 0 j (j - 1)) 0 j j" by simp
then have "fw m n 0 j j j j ≤ fw m n 0 j (j - 1) j 0 + fw m n 0 j (j - 1) 0 j"
also have "… ≤ m j 0 + m 0 j" using ‹j ≤ n› add_mono fw_mono by auto
finally show ?thesis using 2 by auto
qed
then have "fw m n 0 n n j j < 𝟭" by (metis cyc(1) less_or_eq_imp_le single_iteration_inv)
with fw_invariant[of 0 n n n n n n m j j] ‹j ≤ n› have "fw m n n n n j j < 𝟭" by auto
with ‹j ≤ n› show ?thesis by blast
qed
}
ultimately show ?thesis by auto
qed

end (* End of local class context *)
end (* End of theory *)


# Theory Timed_Automata

theory Timed_Automata
imports Main
begin

chapter ‹Basic Definitions and Semantics›

section ‹Time›

assumes dense: "x < y ⟹ ∃z. x < z ∧ z < y"
assumes non_trivial: "∃ x. x ≠ 0"

begin

lemma non_trivial_neg: "∃ x. x < 0"
proof -
from non_trivial obtain x where "x ≠ 0" by auto
then show ?thesis
proof (cases "x < 0", auto, goal_cases)
case 1
then have "x > 0" by auto
then have "(-x) < 0" by auto
then show ?case by blast
qed
qed

end

datatype ('c, 't :: time) cconstraint =
AND "('c, 't) cconstraint" "('c, 't) cconstraint" |
LT 'c 't |
LE 'c 't |
EQ 'c 't |
GT 'c 't |
GE 'c 't

section ‹Syntactic Definition›

text ‹
For an informal description of timed automata we refer to Bengtsson and Yi \cite{BengtssonY03}.
We define a timed automaton ‹A›
›

type_synonym
('c, 'time, 's) invassn = "'s ⇒ ('c, 'time) cconstraint"

type_synonym
('a, 'c, 'time, 's) transition = "'s * ('c, 'time) cconstraint * 'a * 'c list * 's"

type_synonym
('a, 'c, 'time, 's) ta = "('a, 'c, 'time, 's) transition set * ('c, 'time, 's) invassn"

definition trans_of :: "('a, 'c, 'time, 's) ta ⇒ ('a, 'c, 'time, 's) transition set" where
"trans_of ≡ fst"
definition inv_of  :: "('a, 'c, 'time, 's) ta ⇒ ('c, 'time, 's) invassn" where
"inv_of ≡ snd"

abbreviation transition ::
"('a, 'c, 'time, 's) ta ⇒ 's ⇒ ('c, 'time) cconstraint ⇒ 'a ⇒ 'c list ⇒ 's ⇒ bool"
("_ ⊢ _ ⟶⇗_,_,_⇖ _" [61,61,61,61,61,61] 61) where
"(A ⊢ l ⟶⇗g,a,r⇖ l') ≡ (l,g,a,r,l') ∈ trans_of A"

fun collect_clks :: "('c, 't :: time) cconstraint ⇒ 'c set"
where
"collect_clks (AND cc1 cc2) = collect_clks cc1 ∪ collect_clks cc2" |
"collect_clks (LT c _) = {c}" |
"collect_clks (LE c _) = {c}" |
"collect_clks (EQ c _) = {c}" |
"collect_clks (GE c _) = {c}" |
"collect_clks (GT c _) = {c}"

fun collect_clock_pairs :: "('c, 't :: time) cconstraint ⇒ ('c * 't) set"
where
"collect_clock_pairs (LT x m) = {(x, m)}" |
"collect_clock_pairs (LE x m) = {(x, m)}" |
"collect_clock_pairs (EQ x m) = {(x, m)}" |
"collect_clock_pairs (GE x m) = {(x, m)}" |
"collect_clock_pairs (GT x m) = {(x, m)}" |
"collect_clock_pairs (AND cc1 cc2) = (collect_clock_pairs cc1 ∪ collect_clock_pairs cc2)"

definition collect_clkt :: "('a, 'c, 't::time, 's) transition set ⇒ ('c *'t) set"
where
"collect_clkt S = ⋃ {collect_clock_pairs (fst (snd t)) | t . t ∈ S}"

definition collect_clki :: "('c, 't :: time, 's) invassn ⇒ ('c *'t) set"
where
"collect_clki I = ⋃ {collect_clock_pairs (I x) | x. True}"

definition clkp_set :: "('a, 'c, 't :: time, 's) ta ⇒ ('c *'t) set"
where
"clkp_set A = collect_clki (inv_of A) ∪ collect_clkt (trans_of A)"

definition collect_clkvt :: "('a, 'c, 't::time, 's) transition set ⇒ 'c set"
where
"collect_clkvt S = ⋃ {set ((fst o snd o snd o snd) t) | t . t ∈ S}"

abbreviation clk_set where "clk_set A ≡ fst  clkp_set A ∪ collect_clkvt (trans_of A)"

(* We don not need this here but most other theories will make use of this predicate *)
inductive valid_abstraction
where
"⟦∀(x,m) ∈ clkp_set A. m ≤ k x ∧ x ∈ X ∧ m ∈ ℕ; collect_clkvt (trans_of A) ⊆ X; finite X⟧
⟹ valid_abstraction A X k"

section ‹Operational Semantics›

type_synonym ('c, 't) cval = "'c ⇒ 't"

definition cval_add :: "('c,'t) cval ⇒ 't::time ⇒ ('c,'t) cval" (infixr "⊕" 64)
where
"u ⊕ d = (λ x. u x + d)"

inductive clock_val :: "('c, 't) cval ⇒ ('c, 't::time) cconstraint ⇒ bool" ("_ ⊢ _" [62, 62] 62)
where
"⟦u ⊢ cc1; u ⊢ cc2⟧ ⟹ u ⊢ AND cc1 cc2" |
"⟦u c < d⟧ ⟹ u ⊢ LT c d" |
"⟦u c ≤ d⟧ ⟹ u ⊢ LE c d" |
"⟦u c = d⟧ ⟹ u ⊢ EQ c d" |
"⟦u c ≥ d⟧ ⟹ u ⊢ GE c d" |
"⟦u c > d⟧ ⟹ u ⊢ GT c d"

declare clock_val.intros[intro]

inductive_cases[elim!]: "u ⊢ AND cc1 cc2"
inductive_cases[elim!]: "u ⊢ LT c d"
inductive_cases[elim!]: "u ⊢ LE c d"
inductive_cases[elim!]: "u ⊢ EQ c d"
inductive_cases[elim!]: "u ⊢ GE c d"
inductive_cases[elim!]: "u ⊢ GT c d"

fun clock_set :: "'c list ⇒ 't::time ⇒ ('c,'t) cval ⇒ ('c,'t) cval"
where
"clock_set [] _ u = u" |
"clock_set (c#cs) t u = (clock_set cs t u)(c:=t)"

abbreviation clock_set_abbrv :: "'c list ⇒ 't::time ⇒ ('c,'t) cval ⇒ ('c,'t) cval"
("[_→_]_" [65,65,65] 65)
where
"[r → t]u ≡ clock_set r t u"

inductive step_t ::
"('a, 'c, 't, 's) ta ⇒ 's ⇒ ('c, 't) cval ⇒ ('t::time) ⇒ 's ⇒ ('c, 't) cval ⇒ bool"
("_ ⊢ ⟨_, _⟩ →⇗_⇖ ⟨_, _⟩" [61,61,61] 61)
where
"⟦u ⊢ inv_of A l; u ⊕ d ⊢ inv_of A l; d ≥ 0⟧ ⟹ A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l, u ⊕ d⟩"

declare step_t.intros[intro!]

inductive_cases[elim!]: "A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l',u'⟩"

lemma step_t_determinacy1:
"A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l',u'⟩ ⟹  A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l'',u''⟩ ⟹ l' = l''"
by auto

lemma step_t_determinacy2:
"A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l',u'⟩ ⟹  A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l'',u''⟩ ⟹ u' = u''"
by auto

lemma step_t_cont1:
"d ≥ 0 ⟹ e ≥ 0 ⟹ A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l',u'⟩ ⟹ A ⊢ ⟨l', u'⟩ →⇗e⇖ ⟨l'',u''⟩
⟹ A ⊢ ⟨l, u⟩ →⇗d+e⇖ ⟨l'',u''⟩"
proof -
assume A: "d ≥ 0" "e ≥ 0" "A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l',u'⟩" "A ⊢ ⟨l', u'⟩ →⇗e⇖ ⟨l'',u''⟩"
hence "u' = (u ⊕ d)" "u'' = (u' ⊕ e)" by auto
hence "u'' = (u ⊕ (d + e))" unfolding cval_add_def by auto
with A show ?thesis by auto
qed

inductive step_a ::
"('a, 'c, 't, 's) ta ⇒ 's ⇒ ('c, ('t::time)) cval ⇒ 'a ⇒ 's ⇒ ('c, 't) cval ⇒ bool"
("_ ⊢ ⟨_, _⟩ →⇘_⇙ ⟨_, _⟩" [61,61,61] 61)
where
"⟦A ⊢ l ⟶⇗g,a,r⇖ l'; u ⊢ g; u' ⊢ inv_of A l'; u' = [r → 0]u⟧ ⟹ (A ⊢ ⟨l, u⟩ →⇘a⇙ ⟨l', u'⟩)"

inductive step ::
"('a, 'c, 't, 's) ta ⇒ 's ⇒ ('c, ('t::time)) cval ⇒ 's ⇒ ('c, 't) cval ⇒ bool"
("_ ⊢ ⟨_, _⟩ → ⟨_,_⟩" [61,61,61] 61)
where
step_a: "A ⊢ ⟨l, u⟩ →⇘a⇙ ⟨l',u'⟩ ⟹ (A ⊢ ⟨l, u⟩ → ⟨l',u'⟩)" |
step_t: "A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l',u'⟩ ⟹ (A ⊢ ⟨l, u⟩ → ⟨l',u'⟩)"

inductive_cases[elim!]: "A ⊢ ⟨l, u⟩ → ⟨l',u'⟩"

declare step.intros[intro]

inductive
steps :: "('a, 'c, 't, 's) ta ⇒ 's ⇒ ('c, ('t::time)) cval ⇒ 's ⇒ ('c, 't) cval ⇒ bool"
("_ ⊢ ⟨_, _⟩ →* ⟨_, _⟩" [61,61,61] 61)
where
refl: "A ⊢ ⟨l, u⟩ →* ⟨l, u⟩" |
step: "A ⊢ ⟨l, u⟩ → ⟨l', u'⟩ ⟹ A ⊢ ⟨l', u'⟩ →* ⟨l'', u''⟩ ⟹ A ⊢ ⟨l, u⟩ →* ⟨l'', u''⟩"

declare steps.intros[intro]

section ‹Zone Semantics›

type_synonym ('c, 't) zone = "('c, 't) cval set"

definition zone_delay :: "('c, ('t::time)) zone ⇒ ('c, 't) zone"
("_⇧↑" [71] 71)
where
"Z⇧↑ = {u ⊕ d|u d. u ∈ Z ∧ d ≥ (0::'t)}"

definition zone_set :: "('c, 't::time) zone ⇒ 'c list ⇒ ('c, 't) zone"
("_⇘_ → 0⇙" [71] 71)
where
"zone_set Z r = {[r → (0::'t)]u | u . u ∈ Z}"

inductive step_z ::
"('a, 'c, 't, 's) ta ⇒ 's ⇒ ('c, ('t::time)) zone ⇒ 's ⇒ ('c, 't) zone ⇒ bool"
("_ ⊢ ⟨_, _⟩ ↝ ⟨_, _⟩" [61,61,61] 61)
where
step_t_z: "A ⊢ ⟨l, Z⟩ ↝ ⟨l, (Z ∩ {u. u ⊢ inv_of A l})⇧↑ ∩ {u. u ⊢ inv_of A l}⟩" |
step_a_z: "⟦A ⊢ l ⟶⇗g,a,r⇖ l'⟧
⟹ (A ⊢ ⟨l, Z⟩ ↝ ⟨l', zone_set (Z ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}⟩ )"

inductive_cases[elim!]: "A ⊢ ⟨l, u⟩ ↝ ⟨l', u'⟩"

declare step_z.intros[intro]

lemma step_z_sound:
"A ⊢ ⟨l, Z⟩ ↝ ⟨l',Z'⟩ ⟹ (∀ u' ∈ Z'. ∃ u ∈ Z.  A ⊢ ⟨l, u⟩ → ⟨l',u'⟩)"
proof (induction rule: step_z.induct, goal_cases)
case 1 thus ?case unfolding zone_delay_def by blast
next
case (2 A l g a r l' Z)
show ?case
proof
fix u' assume "u' ∈ zone_set (Z ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}"
then obtain u where
"u ⊢ g" "u' ⊢ inv_of A l'" "u' = [r→0]u" "u ∈ Z"
unfolding zone_set_def by auto
with step_a.intros[OF 2 this(1-3)] show "∃u∈Z. A ⊢ ⟨l, u⟩ → ⟨l',u'⟩" by fast
qed
qed

lemma step_z_complete:
"A ⊢ ⟨l, u⟩ → ⟨l', u'⟩ ⟹ u ∈ Z ⟹ ∃ Z'. A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩ ∧ u' ∈ Z'"
proof (induction rule: step.induct, goal_cases)
case (1 A l u a l' u')
then obtain g r
where u': "u' = [r→0]u" "A ⊢ l ⟶⇗g,a,r⇖ l'" "u ⊢ g" "[r→0]u ⊢ inv_of A l'"
by (cases rule: step_a.cases) auto
hence "u' ∈ zone_set (Z ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}"
unfolding zone_set_def using ‹u ∈ Z› by blast
with u'(1,2) show ?case by blast
next
case (2 A l u d l' u')
hence u': "u' = (u ⊕ d)" "u ⊢ inv_of A l" "u ⊕ d ⊢ inv_of A l" "0 ≤ d" and "l = l'" by auto
with u' ‹u ∈ Z› have
"u' ∈ {u'' ⊕ d |u'' d. u'' ∈ Z ∩ {u. u ⊢ inv_of A l} ∧ 0 ≤ d} ∩ {u. u ⊢ inv_of A l}"
by fastforce
thus ?case using ‹l = l'›  step_t_z[unfolded zone_delay_def, of A l] by blast
qed

text ‹
Corresponds to version in old papers --
not strong enough for inductive proof over transitive closure relation.
›
lemma step_z_complete1:
"A ⊢ ⟨l, u⟩ → ⟨l', u'⟩ ⟹ ∃ Z. A ⊢ ⟨l, {u}⟩ ↝ ⟨l', Z⟩ ∧ u' ∈ Z"
proof (induction rule: step.induct, goal_cases)
case (1 A l u a l' u')
then obtain g r
where u': "u' = [r→0]u" "A ⊢ l ⟶⇗g,a,r⇖ l'" "u ⊢ g" "[r→0]u ⊢ inv_of A l'"
by (cases rule: step_a.cases) auto
hence "{[r→0]u} = zone_set ({u} ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}"
unfolding zone_set_def by blast
with u'(1,2) show ?case by auto
next
case (2 A l u d l' u')
hence u': "u' = (u ⊕ d)" "u ⊢ inv_of A l" "u ⊕ d ⊢ inv_of A l" "0 ≤ d" and "l = l'" by auto
hence "{u} = {u} ∩ {u''. u'' ⊢ inv_of A l}" by fastforce
with u'(1) have "{u'} = {u'' ⊕ d |u''. u'' ∈ {u} ∩ {u''. u'' ⊢ inv_of A l}}" by fastforce
with u' have
"u' ∈ {u'' ⊕ d |u'' d. u'' ∈ {u} ∩ {u. u ⊢ inv_of A l} ∧ 0 ≤ d} ∩ {u. u ⊢ inv_of A l}"
by fastforce
thus ?case using ‹l = l'› step_t_z[unfolded zone_delay_def, of A l "{u}"] by blast
qed

text ‹
Easier proof.
›
lemma step_z_complete2:
"A ⊢ ⟨l, u⟩ → ⟨l', u'⟩ ⟹ ∃ Z. A ⊢ ⟨l, {u}⟩ ↝ ⟨l', Z⟩ ∧ u' ∈ Z"
using step_z_complete by fast

inductive
steps_z :: "('a, 'c, 't, 's) ta ⇒ 's ⇒ ('c, ('t::time)) zone ⇒ 's ⇒ ('c, 't) zone ⇒ bool"
("_ ⊢ ⟨_, _⟩ ↝* ⟨_, _⟩" [61,61,61] 61)
where
refl: "A ⊢ ⟨l, Z⟩ ↝* ⟨l, Z⟩" |
step: "A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩ ⟹ A ⊢ ⟨l', Z'⟩ ↝* ⟨l'', Z''⟩ ⟹ A ⊢ ⟨l, Z⟩ ↝* ⟨l'', Z''⟩"

declare steps_z.intros[intro]

lemma steps_z_sound:
"A ⊢ ⟨l, Z⟩ ↝* ⟨l', Z'⟩ ⟹ u' ∈ Z' ⟹ ∃ u ∈ Z. A ⊢ ⟨l, u⟩ →* ⟨l', u'⟩"
proof (induction A l _ l' _ arbitrary: rule: steps_z.induct, goal_cases)
case refl thus ?case by fast
next
case (step A l Z l' Z' l'' Z'')
then obtain u'' where u'': "A ⊢ ⟨l', u''⟩ →* ⟨l'',u'⟩" "u'' ∈ Z'" by auto
then obtain u where "u ∈ Z" "A ⊢ ⟨l, u⟩ → ⟨l',u''⟩" using step_z_sound[OF step(1)] by blast
with u'' show ?case by blast
qed

lemma steps_z_complete:
"A ⊢ ⟨l, u⟩ →* ⟨l', u'⟩ ⟹ u ∈ Z ⟹ ∃ Z'. A ⊢ ⟨l, Z⟩ ↝* ⟨l', Z'⟩ ∧ u' ∈ Z'"
proof (induction arbitrary: Z rule: steps.induct)
case refl thus ?case by auto
next
case (step A l u l' u' l'' u'' Z)
from step_z_complete[OF this(1,4)] obtain Z' where Z': "A ⊢ ⟨l, Z⟩ ↝ ⟨l',Z'⟩" "u' ∈ Z'" by auto
then obtain Z'' where "A ⊢ ⟨l', Z'⟩ ↝* ⟨l'',Z''⟩" "u'' ∈ Z''" using step by metis
with Z' show ?case by blast
qed

end


# Theory DBM

theory DBM
imports Floyd_Warshall Timed_Automata
begin

chapter ‹Difference Bound Matrices›

section ‹Definitions›

text ‹
Difference Bound Matrices (DBMs) constrain differences of clocks
(or more precisely, the difference of values assigned to individual clocks by a valuation).
The possible constraints are given by the following datatype:
›

datatype ('t::time) DBMEntry = Le 't | Lt 't | INF ("∞")

text ‹\noindent This yields a simple definition of DBMs:›

type_synonym 't DBM = "nat ⇒ nat ⇒ 't DBMEntry"

text ‹\noindent
To relate clocks with rows and columns of
a DBM, we use a clock numbering ‹v› of type @{typ "'c ⇒ nat"} to map clocks to indices.
DBMs will regularly be  accompanied by a natural number $n$,
which designates the number of clocks constrained by the matrix.
To be able to represent the full set of clock constraints with DBMs, we add an imaginary
clock ‹𝟬›, which shall be assigned to 0 in every valuation.
In the following predicate we explicitly keep track of ‹𝟬›.
›

inductive dbm_entry_val :: "('c, 't) cval ⇒ 'c option ⇒ 'c option ⇒ ('t::time) DBMEntry ⇒ bool"
where
"u r ≤ d ⟹ dbm_entry_val u (Some r) None (Le d)" |
"-u c ≤ d ⟹ dbm_entry_val u None (Some c) (Le d)" |
"u r < d ⟹ dbm_entry_val u (Some r) None (Lt d)" |
"-u c < d ⟹ dbm_entry_val u None (Some c) (Lt d)" |
"u r - u c ≤ d ⟹ dbm_entry_val u (Some r) (Some c) (Le d)" |
"u r - u c < d ⟹ dbm_entry_val u (Some r) (Some c) (Lt d)" |
"dbm_entry_val _ _ _ ∞"

declare dbm_entry_val.intros[intro]
inductive_cases[elim!]: "dbm_entry_val u None (Some c) (Le d)"
inductive_cases[elim!]: "dbm_entry_val u (Some c) None (Le d)"
inductive_cases[elim!]: "dbm_entry_val u None (Some c) (Lt d)"
inductive_cases[elim!]: "dbm_entry_val u (Some c) None (Lt d)"
inductive_cases[elim!]: "dbm_entry_val u (Some r) (Some c) (Le d)"
inductive_cases[elim!]: "dbm_entry_val u (Some r) (Some c) (Lt d)"

fun dbm_entry_bound :: "('t::time) DBMEntry ⇒ 't"
where
"dbm_entry_bound (Le t) = t" |
"dbm_entry_bound (Lt t) = t" |
"dbm_entry_bound ∞ = 0"

inductive dbm_lt :: "('t::time) DBMEntry ⇒ 't DBMEntry ⇒ bool"
("_ ≺ _" [51, 51] 50)
where
"dbm_lt (Lt _) ∞" |
"dbm_lt (Le _) ∞" |
"a < b  ⟹ dbm_lt (Le a) (Le b)" |
"a < b  ⟹ dbm_lt (Le a) (Lt b)" |
"a ≤ b  ⟹ dbm_lt (Lt a) (Le b)" |
"a < b  ⟹ dbm_lt (Lt a) (Lt b)"

declare dbm_lt.intros[intro]

definition dbm_le :: "('t::time) DBMEntry ⇒ 't DBMEntry ⇒ bool"
("_ ≼ _" [51, 51] 50)
where
"dbm_le a b ≡ (a ≺ b) ∨ a = b"

text ‹
Now a valuation is contained in the zone represented by a DBM if it fulfills all individual
constraints:
›

definition DBM_val_bounded :: "('c ⇒ nat) ⇒ ('c, 't) cval ⇒ ('t::time) DBM ⇒ nat ⇒ bool"
where
"DBM_val_bounded v u m n ≡ Le 0 ≼ m 0 0 ∧
(∀ c. v c ≤ n ⟶ (dbm_entry_val u None (Some c) (m 0 (v c))
∧ dbm_entry_val u (Some c) None (m (v c) 0)))
∧ (∀ c1 c2. v c1 ≤ n ∧ v c2 ≤ n ⟶ dbm_entry_val u (Some c1) (Some c2) (m (v c1) (v c2)))"

abbreviation DBM_val_bounded_abbrev ::
"('c, 't) cval ⇒ ('c ⇒ nat) ⇒ nat ⇒ ('t::time) DBM ⇒ bool"
("_ ⊢⇘_,_⇙ _")
where
"u ⊢⇘v,n⇙ M ≡ DBM_val_bounded v u M n"

abbreviation
"dmin a b ≡ if a ≺ b then a else b"

lemma dbm_le_dbm_min:
"a ≼ b ⟹ a = dmin a b" unfolding dbm_le_def
by auto

lemma dbm_lt_asym:
assumes "e ≺ f"
shows "~ f ≺ e"
using assms
proof (safe, cases e f rule: dbm_lt.cases, goal_cases)
case 1 from this(2) show ?case using 1(3-) by (cases f e rule: dbm_lt.cases) auto
next
case 2 from this(2) show ?case using 2(3-) by (cases f e rule: dbm_lt.cases) auto
next
case 3 from this(2) show ?case using 3(3-) by (cases f e rule: dbm_lt.cases) auto
next
case 4 from this(2) show ?case using 4(3-) by (cases f e rule: dbm_lt.cases) auto
next
case 5 from this(2) show ?case using 5(3-) by (cases f e rule: dbm_lt.cases) auto
next
case 6 from this(2) show ?case using 6(3-) by (cases f e rule: dbm_lt.cases) auto
qed

lemma dbm_le_dbm_min2:
"a ≼ b ⟹ a = dmin b a"
using dbm_lt_asym by (auto simp: dbm_le_def)

lemma dmb_le_dbm_entry_bound_inf:
"a ≼ b ⟹ a = ∞ ⟹ b = ∞"
apply (auto simp: dbm_le_def)
apply (cases rule: dbm_lt.cases)
by auto

lemma dbm_not_lt_eq: "¬ a ≺ b ⟹ ¬ b ≺ a ⟹ a = b"
apply (cases a)
apply (cases b, fastforce+)+
done

lemma dbm_not_lt_impl: "¬ a ≺ b ⟹ b ≺ a ∨ a = b" using dbm_not_lt_eq by auto

lemma "dmin a b = dmin b a"
proof (cases "a ≺ b")
case True thus ?thesis by (simp add: dbm_lt_asym)
next
case False thus ?thesis by (simp add: dbm_not_lt_eq)
qed

lemma dbm_lt_trans: "a ≺ b ⟹ b ≺ c ⟹ a ≺ c"
proof (cases a b rule: dbm_lt.cases, goal_cases)
case 1 thus ?case by simp
next
case 2 from this(2-) show ?case by (cases rule: dbm_lt.cases) simp+
next
case 3 from this(2-) show ?case by (cases rule: dbm_lt.cases) simp+
next
case 4 from this(2-) show ?case by (cases rule: dbm_lt.cases) auto
next
case 5 from this(2-) show ?case by (cases rule: dbm_lt.cases) auto
next
case 6 from this(2-) show ?case by (cases rule: dbm_lt.cases) auto
next
case 7 from this(2-) show ?case by (cases rule: dbm_lt.cases) auto
qed

lemma aux_3: "¬ a ≺ b ⟹ ¬ b ≺ c ⟹ a ≺ c ⟹ c = a"
proof goal_cases
case 1 thus ?case
proof (cases "c ≺ b")
case True
with ‹a ≺ c› have "a ≺ b" by (rule dbm_lt_trans)
thus ?thesis using 1 by auto
next
case False thus ?thesis using dbm_not_lt_eq 1 by auto
qed
qed

inductive_cases[elim!]: "∞ ≺ x"

lemma dbm_lt_asymmetric[simp]: "x ≺ y ⟹ y ≺ x ⟹ False"
by (cases x y rule: dbm_lt.cases) (auto elim: dbm_lt.cases)

lemma le_dbm_le: "Le a ≼ Le b ⟹ a ≤ b" unfolding dbm_le_def by (auto elim: dbm_lt.cases)

lemma le_dbm_lt: "Le a ≼ Lt b ⟹ a < b" unfolding dbm_le_def by (auto elim: dbm_lt.cases)

lemma lt_dbm_le: "Lt a ≼ Le b ⟹ a ≤ b" unfolding dbm_le_def by (auto elim: dbm_lt.cases)

lemma lt_dbm_lt: "Lt a ≼ Lt b ⟹ a ≤ b" unfolding dbm_le_def by (auto elim: dbm_lt.cases)

lemma not_dbm_le_le_impl: "¬ Le a ≺ Le b ⟹ a ≥ b" by (metis dbm_lt.intros(3) not_less)

lemma not_dbm_lt_le_impl: "¬ Lt a ≺ Le b ⟹ a > b" by (metis dbm_lt.intros(5) not_less)

lemma not_dbm_lt_lt_impl: "¬ Lt a ≺ Lt b ⟹ a ≥ b" by (metis dbm_lt.intros(6) not_less)

lemma not_dbm_le_lt_impl: "¬ Le a ≺ Lt b ⟹ a ≥ b" by (metis dbm_lt.intros(4) not_less)

(*>*)

(*<*)

fun dbm_add :: "('t::time) DBMEntry ⇒ 't DBMEntry ⇒ 't DBMEntry" (infixl "⊗" 70)
where
"dbm_add ∞     _      = ∞" |
"dbm_add _      ∞     = ∞" |
"dbm_add (Le a) (Le b) = (Le (a+b))" |
"dbm_add (Le a) (Lt b) = (Lt (a+b))" |
"dbm_add (Lt a) (Le b) = (Lt (a+b))" |
"dbm_add (Lt a) (Lt b) = (Lt (a+b))"

by (cases x y rule: dbm_lt.cases) ((cases z), auto)+

proof -
assume lt: "dbm_add x z ≺ dbm_add y z" "¬ x ≺ y"
hence "x = y ∨ y ≺ x" by (auto simp: dbm_not_lt_eq)
thus ?thesis
proof
assume "x = y" thus ?thesis by simp
next
assume "y ≺ x"
thus ?thesis
proof (cases y x rule: dbm_lt.cases, goal_cases)
case 1 thus ?case using lt by auto
next
case 2 thus ?case using lt by auto
next
case 3 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+
next
case 4 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+
next
case 5 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+
next
case 6 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+
qed
qed
qed

by (cases x y rule: dbm_lt.cases) ((cases z), auto)+

proof -
assume lt: "dbm_add z x ≺ dbm_add z y" "¬ x ≺ y"
hence "x = y ∨ y ≺ x" by (auto simp: dbm_not_lt_eq)
thus ?thesis
proof
assume "x = y" thus ?thesis by simp
next
assume "y ≺ x"
thus ?thesis
proof (cases y x rule: dbm_lt.cases, goal_cases)
case 1 thus ?case using lt by (cases z) fastforce+
next
case 2 thus ?case using lt by (cases z) fastforce+
next
case 3 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+
next
case 4 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+
next
case 5 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+
next
case 6 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+
qed
qed
qed

"a ≠ ∞ ⟹ b ≠ ∞ ⟹ dbm_add a b ≠ ∞"
by (cases a, auto, cases b, auto, cases b, auto)

lemma dbm_le_not_inf:
"a ≼ b ⟹ b ≠ ∞ ⟹ a ≠ ∞"
by (cases "a = b") (auto simp: dbm_le_def)

section ‹DBM Entries Form a Linearly Ordered Abelian Monoid›

instantiation DBMEntry :: (time) linorder
begin
definition less_eq: "(≤) ≡ dbm_le"
definition less: "(<) = dbm_lt"
instance
proof ((standard; unfold less less_eq), goal_cases)
case 1 thus ?case unfolding dbm_le_def using dbm_lt_asymmetric by auto
next
case 2 thus ?case by (simp add: dbm_le_def)
next
case 3 thus ?case unfolding dbm_le_def using dbm_lt_trans by auto
next
case 4 thus ?case unfolding dbm_le_def using dbm_lt_asymmetric by auto
next
case 5 thus ?case unfolding dbm_le_def using dbm_not_lt_eq by auto
qed
end

begin
definition neutral: "neutral = Le 0"
instance proof ((standard; unfold mult neutral less less_eq), goal_cases)
case (1 a b c) thus ?case by (cases a; cases b; cases c; auto)
next
case (2 a b) thus ?case by (cases a; cases b) auto
next
case (3 a b c)
thus ?case unfolding dbm_le_def
apply safe
apply (rule dbm_lt.cases)
apply assumption
by (cases c; fastforce)+
next
case (4 x) thus ?case by (cases x) auto
next
case (5 x) thus ?case by (cases x) auto
qed
end

apply (standard, fold neutral mult less_eq less)

lemma Le_Le_dbm_lt_D[dest]: "Le a ≺ Lt b ⟹ a < b" by (cases rule: dbm_lt.cases) auto
lemma Le_Lt_dbm_lt_D[dest]: "Le a ≺ Le b ⟹ a < b" by (cases rule: dbm_lt.cases) auto
lemma Lt_Le_dbm_lt_D[dest]: "Lt a ≺ Le b ⟹ a ≤ b" by (cases rule: dbm_lt.cases) auto
lemma Lt_Lt_dbm_lt_D[dest]: "Lt a ≺ Lt b ⟹ a < b" by (cases rule: dbm_lt.cases) auto

lemma Le_le_LeI[intro]: "a ≤ b ⟹ Le a ≤ Le b" unfolding less_eq dbm_le_def by auto
lemma Lt_le_LeI[intro]: "a ≤ b ⟹ Lt a ≤ Le b" unfolding less_eq dbm_le_def by auto
lemma Lt_le_LtI[intro]: "a ≤ b ⟹ Lt a ≤ Lt b" unfolding less_eq dbm_le_def by auto
lemma Le_le_LtI[intro]: "a < b ⟹ Le a ≤ Lt b" unfolding less_eq dbm_le_def by auto
lemma Lt_lt_LeI: "x ≤ y ⟹ Lt x < Le y" unfolding less by auto

lemma Le_le_LeD[dest]: "Le a ≤ Le b ⟹ a ≤ b" unfolding dbm_le_def less_eq by auto
lemma Le_le_LtD[dest]: "Le a ≤ Lt b ⟹ a < b" unfolding dbm_le_def less_eq by auto
lemma Lt_le_LeD[dest]: "Lt a ≤ Le b ⟹ a ≤ b" unfolding less_eq dbm_le_def by auto
lemma Lt_le_LtD[dest]: "Lt a ≤ Lt b ⟹ a ≤ b" unfolding less_eq dbm_le_def by auto

lemma inf_not_le_Le[simp]: "∞ ≤ Le x = False" unfolding less_eq dbm_le_def by auto
lemma inf_not_le_Lt[simp]: "∞ ≤ Lt x = False" unfolding less_eq dbm_le_def by auto
lemma inf_not_lt[simp]: "∞ ≺ x = False" by auto

lemma any_le_inf: "x ≤ ∞" by (metis less_eq dmb_le_dbm_entry_bound_inf le_cases)

section ‹Basic Properties of DBMs›

subsection ‹DBMs and Length of Paths›

lemma dbm_entry_val_add_1: "dbm_entry_val u (Some c) (Some d) a ⟹  dbm_entry_val u (Some d) None b
⟹ dbm_entry_val u (Some c) None (dbm_add a b)"
proof (cases a, goal_cases)
case 1 thus ?thesis
apply (cases b)
apply auto
next
case 2 thus ?thesis
apply (cases b)
apply auto
apply (simp add: dbm_entry_val.intros(3) diff_less_eq less_le_trans)
next
case 3 thus ?thesis by (cases b) auto
qed

lemma dbm_entry_val_add_2: "dbm_entry_val u None (Some c) a ⟹ dbm_entry_val u (Some c) (Some d) b
⟹ dbm_entry_val u None (Some d) (dbm_add a b)"
proof (cases a, goal_cases)
case 1 thus ?thesis
apply (cases b)
apply auto
next
case 2 thus ?thesis
apply (cases b)
apply auto
next
case 3 thus ?thesis by (cases b) auto
qed

"dbm_entry_val u (Some c) (Some d) a ⟹  dbm_entry_val u (Some d) (Some e) b
⟹ dbm_entry_val u (Some c) (Some e) (dbm_add a b)"
proof (cases a, goal_cases)
case 1 thus ?thesis
apply (cases b)
apply auto
next
case 2 thus ?thesis
apply (cases b)
apply auto
next
case 3 thus ?thesis by (cases b) auto
qed

"dbm_entry_val u (Some c) None a ⟹ dbm_entry_val u None (Some d) b
⟹ dbm_entry_val u (Some c) (Some d) (dbm_add a b)"
proof (cases a, goal_cases)
case 1 thus ?thesis
apply (cases b)
apply auto
next
case 2 thus ?thesis
apply (cases b)
apply auto
next
case 3 thus ?thesis by (cases b) auto
qed

lemma DBM_val_bounded_len_1'_aux:
assumes "DBM_val_bounded v u m n" "v c ≤ n" "∀ k ∈ set vs. k > 0 ∧ k ≤ n ∧ (∃ c. v c = k)"
shows "dbm_entry_val u (Some c) None (len m (v c) 0 vs)" using assms
proof (induction vs arbitrary: c)
case Nil then show ?case unfolding DBM_val_bounded_def by auto
next
case (Cons k vs)
then obtain c' where c': "k > 0" "k ≤ n" "v c' = k" by auto
with Cons have "dbm_entry_val u (Some c') None (len m (v c') 0 vs)" by auto
moreover have "dbm_entry_val u (Some c) (Some c') (m (v c) (v c'))" using Cons.prems c'
ultimately have "dbm_entry_val u (Some c) None (m (v c) (v c') + len m (v c') 0 vs)"
using dbm_entry_val_add_1 unfolding mult by fastforce
with c' show ?case unfolding DBM_val_bounded_def by simp
qed

lemma DBM_val_bounded_len_3'_aux:
"DBM_val_bounded v u m n ⟹ v c ≤ n ⟹ v d ≤ n ⟹ ∀ k ∈ set vs. k > 0 ∧ k ≤ n ∧ (∃ c. v c = k)
⟹ dbm_entry_val u (Some c) (Some d) (len m (v c) (v d) vs)"
proof (induction vs arbitrary: c)
case Nil thus ?case unfolding DBM_val_bounded_def by auto
next
case (Cons k vs)
then obtain c' where c': "k > 0" "k ≤ n" "v c' = k" by auto
with Cons have "dbm_entry_val u (Some c') (Some d) (len m (v c') (v d) vs)" by auto
moreover have "dbm_entry_val u (Some c) (Some c') (m (v c) (v c'))" using Cons.prems c'
ultimately have "dbm_entry_val u (Some c) (Some d) (m (v c) (v c') + len m (v c') (v d) vs)"
using dbm_entry_val_add_3 unfolding mult by fastforce
with c' show ?case unfolding DBM_val_bounded_def by simp
qed

lemma DBM_val_bounded_len_2'_aux:
"DBM_val_bounded v u m n ⟹ v c ≤ n ⟹ ∀ k ∈ set vs. k > 0 ∧ k ≤ n ∧ (∃ c. v c = k)
⟹ dbm_entry_val u None (Some c) (len m 0 (v c) vs)"
proof (cases vs, goal_cases)
case 1 then show ?thesis unfolding DBM_val_bounded_def by auto
next
case (2 k vs)
then obtain c' where c': "k > 0" "k ≤ n" "v c' = k" by auto
with 2 have "dbm_entry_val u (Some c') (Some c) (len m (v c') (v c) vs)"
using DBM_val_bounded_len_3'_aux by auto
moreover have "dbm_entry_val u None (Some c') (m 0 (v c'))"
using 2 c' by (auto simp add: DBM_val_bounded_def)
ultimately have "dbm_entry_val u None (Some c) (m 0 (v c') + len m (v c') (v c) vs)"
using dbm_entry_val_add_2 unfolding mult by fastforce
with 2(4) c' show ?case unfolding DBM_val_bounded_def by simp
qed

lemma cnt_0_D:
"cnt x xs = 0 ⟹ x ∉ set xs"
apply (induction xs)
apply simp
apply (rename_tac a xs)
apply (case_tac "x = a")
by simp+

lemma cnt_at_most_1_D:
"cnt x (xs @ x # ys) ≤ 1 ⟹ x ∉ set xs ∧ x ∉ set ys"
apply (induction xs)
apply auto[]
using cnt_0_D apply force
apply (rename_tac a xs)
apply (case_tac "a = x")
apply simp
apply simp
done

lemma nat_list_0 [intro]:
"x ∈ set xs ⟹ 0 ∉ set (xs :: nat list) ⟹ x > 0"
by (induction xs) auto

lemma DBM_val_bounded_len':
fixes v
defines "vo ≡ λ k. if k = 0 then None else Some (SOME c. v c = k)"
assumes "DBM_val_bounded v u m n" "cnt 0 (i # j # vs) ≤ 1"
"∀ k ∈ set (i # j # vs). k > 0 ⟶ k ≤ n ∧ (∃ c. v c = k)"
shows "dbm_entry_val u (vo i) (vo j) (len m i j vs)"
proof -
show ?thesis
proof (cases "∀ k ∈ set vs. k > 0")
case True
with assms have *: "∀ k ∈ set vs. k > 0 ∧ k ≤ n ∧ (∃ c. v c = k)" by auto
show ?thesis
proof (cases "i = 0")
case True
then have i: "vo i = None" by (simp add: vo_def)
show ?thesis
proof (cases "j = 0")
case True with assms ‹i = 0› show ?thesis by auto
next
case False
with assms obtain c2 where c2: "j ≤ n" "v c2 = j" "vo j = Some c2"
unfolding vo_def by (fastforce intro: someI)
with ‹i = 0› i DBM_val_bounded_len_2'_aux[OF assms(2) _ *] show ?thesis by auto
qed
next
case False
with assms(4) obtain c1 where c1: "i ≤ n" "v c1 = i" "vo i = Some c1"
unfolding vo_def by (fastforce intro: someI)
show ?thesis
proof (cases "j = 0")
case True
with DBM_val_bounded_len_1'_aux[OF assms(2) _ *] c1 show ?thesis by (auto simp: vo_def)
next
case False
with assms obtain c2 where c2: "j ≤ n" "v c2 = j" "vo j = Some c2"
unfolding vo_def by (fastforce intro: someI)
with c1 DBM_val_bounded_len_3'_aux[OF assms(2) _ _ *] show ?thesis by auto
qed
qed
next
case False
then have "∃ k ∈ set vs. k = 0" by auto
then obtain us ws where vs: "vs = us @ 0 # ws" by (meson split_list_last)
with cnt_at_most_1_D[of 0 "i # j # us"] assms(3) have
"0 ∉ set us" "0 ∉ set ws" "i ≠ 0" "j ≠ 0"
by auto
with vs have vs: "vs = us @ 0 # ws" "∀ k ∈ set us. k > 0" "∀ k ∈ set ws. k > 0" by auto
with assms(4) have v:
"∀k∈set us. 0 < k ∧ k ≤ n ∧ (∃c. v c = k)" "∀k∈set ws. 0 < k ∧ k ≤ n ∧ (∃c. v c = k)"
by auto
from ‹i ≠ 0› ‹j ≠ 0› assms obtain c1 c2 where
c1: "i ≤ n" "v c1 = i" "vo i = Some c1" and c2: "j ≤ n" "v c2 = j" "vo j = Some c2"
unfolding vo_def by (fastforce intro: someI)
with dbm_entry_val_add_4 [OF DBM_val_bounded_len_1'_aux[OF assms(2) _ v(1)] DBM_val_bounded_len_2'_aux[OF assms(2) _ v(2)]]
have "dbm_entry_val u (Some c1) (Some c2) (dbm_add (len m (v c1) 0 us) (len m 0 (v c2) ws))" by auto
moreover from vs have "len m (v c1) (v c2) vs = dbm_add (len m (v c1) 0 us) (len m 0 (v c2) ws)"
ultimately show ?thesis using c1 c2 by auto
qed
qed

lemma DBM_val_bounded_len'1:
fixes v
assumes "DBM_val_bounded v u m n" "0 ∉ set vs" "v c ≤ n"
"∀ k ∈ set vs. k > 0 ⟶ k ≤ n ∧ (∃ c. v c = k)"
shows "dbm_entry_val u (Some c) None (len m (v c) 0 vs)"
using DBM_val_bounded_len_1'_aux[OF assms(1,3)] assms(2,4) by fastforce

lemma DBM_val_bounded_len'2:
fixes v
assumes "DBM_val_bounded v u m n" "0 ∉ set vs" "v c ≤ n"
"∀ k ∈ set vs. k > 0 ⟶ k ≤ n ∧ (∃ c. v c = k)"
shows "dbm_entry_val u None (Some c) (len m 0 (v c) vs)"
using DBM_val_bounded_len_2'_aux[OF assms(1,3)] assms(2,4) by fastforce

lemma DBM_val_bounded_len'3:
fixes v
assumes "DBM_val_bounded v u m n" "cnt 0 vs ≤ 1" "v c1 ≤ n" "v c2 ≤ n"
"∀ k ∈ set vs. k > 0 ⟶ k ≤ n ∧ (∃ c. v c = k)"
shows "dbm_entry_val u (Some c1) (Some c2) (len m (v c1) (v c2) vs)"
proof -
show ?thesis
proof (cases "∀ k ∈ set vs. k > 0")
case True
with assms have "∀ k ∈ set vs. k > 0 ∧ k ≤ n ∧ (∃ c. v c = k)" by auto
with DBM_val_bounded_len_3'_aux[OF assms(1,3,4)] show ?thesis by auto
next
case False
then have "∃ k ∈ set vs. k = 0" by auto
then obtain us ws where vs: "vs = us @ 0 # ws" by (meson split_list_last)
with cnt_at_most_1_D[of 0 "us"] assms(2) have
"0 ∉ set us" "0 ∉ set ws"
by auto
with vs have vs: "vs = us @ 0 # ws" "∀ k ∈ set us. k > 0" "∀ k ∈ set ws. k > 0" by auto
with assms(5) have v:
"∀k∈set us. 0 < k ∧ k ≤ n ∧ (∃c. v c = k)" "∀k∈set ws. 0 < k ∧ k ≤ n ∧ (∃c. v c = k)"
by auto
with dbm_entry_val_add_4 [OF DBM_val_bounded_len_1'_aux[OF assms(1,3) v(1)] DBM_val_bounded_len_2'_aux[OF assms(1,4) v(2)]]
have "dbm_entry_val u (Some c1) (Some c2) (dbm_add (len m (v c1) 0 us) (len m 0 (v c2) ws))" by auto
moreover from vs have "len m (v c1) (v c2) vs = dbm_add (len m (v c1) 0 us) (len m 0 (v c2) ws)"
ultimately show ?thesis by auto
qed
qed

lemma DBM_val_bounded_len'':
fixes v
defines "vo ≡ λ k. if k = 0 then None else Some (SOME c. v c = k)"
assumes "DBM_val_bounded v u m n" "i ≠ 0 ∨ j ≠ 0"
"∀ k ∈ set (i # j # vs). k > 0 ⟶ k ≤ n ∧ (∃ c. v c = k)"
shows "dbm_entry_val u (vo i) (vo j) (len m i j vs)" using assms
proof (induction "length vs" arbitrary: i vs rule: less_induct)
case less
show ?case
proof (cases "∀ k ∈ set vs. k > 0")
case True
with less.prems have *: "∀ k ∈ set vs. k > 0 ∧ k ≤ n ∧ (∃ c. v c = k)" by auto
show ?thesis
proof (cases "i = 0")
case True
then have i: "vo i = None" by (simp add: vo_def)
show ?thesis
proof (cases "j = 0")
case True with less.prems ‹i = 0› show ?thesis by auto
next
case False
with less.prems obtain c2 where c2: "j ≤ n" "v c2 = j" "vo j = Some c2"
unfolding vo_def by (fastforce intro: someI)
with ‹i = 0› i DBM_val_bounded_len_2'_aux[OF less.prems(1) _ *] show ?thesis by auto
qed
next
case False
with less.prems obtain c1 where c1: "i ≤ n" "v c1 = i" "vo i = Some c1"
unfolding vo_def by (fastforce intro: someI)
show ?thesis
proof (cases "j = 0")
case True
with DBM_val_bounded_len_1'_aux[OF less.prems(1) _ *] c1 show ?thesis by (auto simp: vo_def)
next
case False
with less.prems obtain c2 where c2: "j ≤ n" "v c2 = j" "vo j = Some c2"
unfolding vo_def by (fastforce intro: someI)
with c1 DBM_val_bounded_len_3'_aux[OF less.prems(1) _ _ *] show ?thesis by auto
qed
qed
next
case False
then have "∃ us ws. vs = us @ 0 # ws ∧ (∀ k ∈ set us. k > 0)"
proof (induction vs)
case Nil then show ?case by auto
next
case (Cons x vs)
show ?case
proof (cases "x = 0")
case True then show ?thesis by fastforce
next
case False
with Cons.prems have "¬ (∀a∈set vs. 0 < a)" by auto
from Cons.IH[OF this] obtain us ws where "vs = us @ 0 # ws" "∀a∈set us. 0 < a" by auto
with False have "x # vs = (x # us) @ 0 # ws" "∀a∈set (x # us). 0 < a" by auto
then show ?thesis by blast
qed
qed
then obtain us ws where vs: "vs = us @ 0 # ws" "∀ k ∈ set us. k > 0" by blast
then show ?thesis
oops

lemma DBM_val_bounded_len_1: "DBM_val_bounded v u m n ⟹ v c ≤ n ⟹ ∀ c ∈ set cs. v c ≤ n
⟹ dbm_entry_val u (Some c) None (len m (v c) 0 (map v cs))"
proof (induction cs arbitrary: c)
case Nil thus ?case unfolding DBM_val_bounded_def by auto
next
case (Cons c' cs)
hence "dbm_entry_val u (Some c') None (len m (v c') 0 (map v cs))" by auto
moreover have "dbm_entry_val u (Some c) (Some c') (m (v c) (v c'))" using Cons.prems
ultimately have "dbm_entry_val u (Some c) None (m (v c) (v c') + len m (v c') 0 (map v cs))"
using dbm_entry_val_add_1 unfolding mult by fastforce
thus ?case unfolding DBM_val_bounded_def by simp
qed

lemma DBM_val_bounded_len_3: "DBM_val_bounded v u m n ⟹ v c ≤ n ⟹ v d ≤ n ⟹ ∀ c ∈ set cs. v c ≤ n
⟹ dbm_entry_val u (Some c) (Some d) (len m (v c) (v d) (map v cs))"
proof (induction cs arbitrary: c)
case Nil thus ?case unfolding DBM_val_bounded_def by auto
next
case (Cons c' cs)
hence "dbm_entry_val u (Some c') (Some d) (len m (v c') (v d) (map v cs))" by auto
moreover have "dbm_entry_val u (Some c) (Some c') (m (v c) (v c'))" using Cons.prems
ultimately have "dbm_entry_val u (Some c) (Some d) (m (v c) (v c') + len m (v c') (v d) (map v cs))"
using dbm_entry_val_add_3 unfolding mult by fastforce
thus ?case unfolding DBM_val_bounded_def by simp
qed

lemma DBM_val_bounded_len_2: "DBM_val_bounded v u m n ⟹ v c ≤ n ⟹ ∀ c ∈ set cs. v c ≤ n
⟹ dbm_entry_val u None (Some c) (len m 0 (v c) (map v cs))"
proof (cases cs, goal_cases)
case 1 thus ?thesis unfolding DBM_val_bounded_def by auto
next
case (2 c' cs)
hence "dbm_entry_val u (Some c') (Some c) (len m (v c') (v c) (map v cs))"
using DBM_val_bounded_len_3 by auto
moreover have "dbm_entry_val u None (Some c') (m 0 (v c'))"
using 2 by (simp add: DBM_val_bounded_def)
ultimately have "dbm_entry_val u None (Some c) (m 0 (v c') + len m (v c') (v c) (map v cs))"
using dbm_entry_val_add_2 unfolding mult by fastforce
thus ?case using 2(4) unfolding DBM_val_bounded_def by simp
qed

end


# Theory Paths_Cycles

theory Paths_Cycles
imports Floyd_Warshall Timed_Automata
begin

chapter ‹Library for Paths, Arcs and Lengths›

lemma length_eq_distinct:
assumes "set xs = set ys" "distinct xs" "length xs = length ys"
shows "distinct ys"
using assms card_distinct distinct_card by fastforce

section ‹Arcs›

fun arcs :: "nat ⇒ nat ⇒ nat list ⇒ (nat * nat) list" where
"arcs a b [] = [(a,b)]" |
"arcs a b (x # xs) = (a, x) # arcs x b xs"

definition arcs' :: "nat list ⇒ (nat * nat) set" where
"arcs' xs = set (arcs (hd xs) (last xs) (butlast (tl xs)))"

lemma arcs'_decomp:
"length xs > 1 ⟹ (i, j) ∈ arcs' xs ⟹ ∃ zs ys. xs = zs @ i # j # ys"
proof (induction xs)
case Nil thus ?case by auto
next
case (Cons x xs)
then have "length xs > 0" by auto
then obtain y ys where xs: "xs = y # ys" by (metis Suc_length_conv less_imp_Suc_add)
show ?case
proof (cases "(i, j) = (x, y)")
case True
with xs have "x # xs = [] @ i # j # ys" by simp
then show ?thesis by auto
next
case False
then show ?thesis
proof (cases "length ys > 0", goal_cases)
case 2
then have "ys = []" by auto
then have "arcs' (x#xs) = {(x,y)}" using xs by (auto simp add: arcs'_def)
with Cons.prems(2) 2(1) show ?case by auto
next
case True
with xs Cons.prems(2) False have "(i, j) ∈ arcs' xs" by (auto simp add: arcs'_def)
with Cons.IH[OF _ this] True xs obtain zs ys where "xs = zs @ i # j # ys" by auto
then have "x # xs = (x # zs) @ i # j # ys" by simp
then show ?thesis by blast
qed
qed
qed

lemma arcs_decomp_tail:
"arcs j l (ys @ [i]) = arcs j i ys @ [(i, l)]"
by (induction ys arbitrary: j) auto

lemma arcs_decomp: "xs = ys @ y # zs ⟹ arcs x z xs = arcs x y ys @ arcs y z zs"
by (induction ys arbitrary: x xs) simp+

lemma distinct_arcs_ex:
"distinct xs ⟹ i ∉ set xs ⟹ xs ≠ [] ⟹ ∃ a b. a ≠ x ∧ (a,b) ∈ set (arcs i j xs)"
apply (induction xs arbitrary: i)
apply simp
apply (rename_tac a xs i)
apply (case_tac xs)
apply simp
apply metis
by auto

lemma cycle_rotate_2_aux:
"(i, j) ∈ set (arcs a b (xs @ [c])) ⟹ (i,j) ≠ (c,b) ⟹ (i, j) ∈ set (arcs a c xs)"
by (induction xs arbitrary: a) auto

lemma arcs_set_elem1:
assumes "j ≠ k" "k ∈ set (i # xs)"
shows "∃ l. (k, l) ∈ set (arcs i j xs)" using assms
by (induction xs arbitrary: i) auto

lemma arcs_set_elem2:
assumes "i ≠ k" "k ∈ set (j # xs)"
shows "∃ l. (l, k) ∈ set (arcs i j xs)" using assms
proof (induction xs arbitrary: i)
case Nil then show ?case by simp
next
case (Cons x xs)
then show ?case by (cases "k = x") auto
qed

section ‹Length of Paths›

fixes M :: "('a :: linordered_ab_monoid_add) mat"
shows "len M i j xs + len M i j xs = len (λi j. M i j + M i j) i j xs"
proof (induction xs arbitrary: i j)
case Nil thus ?case by auto
next
case (Cons x xs)
have "M i x + len M x j xs + (M i x + len M x j xs) = M i x + (len M x j xs + M i x) + len M x j xs"
also have "… = M i x + (M i x + len M x j xs) + len M x j xs" by (simp add: comm)
also have "… = (M i x + M i x) + (len M x j xs + len M x j xs)" by (simp add: assoc)
finally have "M i x + len M x j xs + (M i x + len M x j xs)
= (M i x + M i x) + len (λi j. M i j + M i j) x j xs"
using Cons by simp
thus ?case by simp
qed

section ‹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 fw_canonical:
"cycle_free m n ⟹ canonical (fw m n n n n) n"
proof (clarify, goal_cases)
case 1
with fw_shortest[OF ‹cycle_free m n›] show ?case
by auto
qed

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 ‹Cycle Rotation›

lemma cycle_rotate:
fixes M :: "('a :: linordered_ab_monoid_add) mat"
assumes "length xs > 1" "(i, j) ∈ arcs' xs"
shows "∃ ys zs. len M a a xs = len M i i (j # ys @ a # zs) ∧ xs = zs @ i # j # ys" using assms
proof -
assume A: "length xs > 1" "(i, j) ∈ arcs' xs"
from arcs'_decomp[OF this] obtain ys zs where xs: "xs = zs @ i # j # ys" by blast
from len_decomp[OF this, of M a a]
have "len M a a xs = len M a i zs + len M i a (j # ys)" .
also have "… = len M i a (j # ys) + len M a i zs" by (simp add: comm)
also from len_comp[of M i i "j # ys" a zs] have "… = len M i i (j # ys @ a # zs)" by auto
finally show ?thesis using xs by auto
qed

lemma cycle_rotate_2:
fixes M :: "('a :: linordered_ab_monoid_add) mat"
assumes "xs ≠ []" "(i, j) ∈ set (arcs a a xs)"
shows "∃ ys. len M a a xs = len M i i (j # ys) ∧ set ys ⊆ set (a # xs) ∧ length ys < length xs"
using assms proof -
assume A:"xs ≠ []" "(i, j) ∈ set (arcs a a xs)"
{ fix ys assume A:"a = i" "xs = j # ys"
then have ?thesis by auto
} note * = this
{ fix b ys assume A:"a = j" "xs = ys @ [i]"
then have ?thesis
proof (auto, goal_cases)
case 1
have "len M j j (ys @ [i]) = M i j + len M j i ys"
using len_decomp[of "ys @ [i]" ys i "[]" M j j] by (auto simp: comm)
thus ?case by blast
qed
} note ** = this
{ assume "length xs = 1"
then obtain b where xs: "xs = [b]" by (metis One_nat_def length_0_conv length_Suc_conv)
with A(2) have "a = i ∧ b = j ∨ a = j ∧ b = i" by auto
then have ?thesis using * ** xs by auto
} note *** = this
show ?thesis
proof (cases "length xs = 0")
case True with A show ?thesis by auto
next
case False
thus ?thesis
proof (cases "length xs = 1", goal_cases)
case True with *** show ?thesis by auto
next
case 2
hence "length xs > 1" by linarith
then obtain b c ys where ys:"xs = b # ys @ [c]"
by (metis One_nat_def assms(1) 2(2) length_0_conv length_Cons list.exhaust rev_exhaust)
thus ?thesis
proof (cases "(i,j) = (a,b)", goal_cases)
case True
with ys * show ?thesis by auto
next
case False
then show ?thesis
proof (cases "(i,j) = (c,a)", goal_cases)
case True
with ys ** show ?thesis by auto
next
case 2
with A(2) ys have "(i, j) ∈ arcs' xs"
using cycle_rotate_2_aux by (auto simp: arcs'_def) (* slow *)
from cycle_rotate[OF ‹length xs > 1› this, of M a] show ?thesis by auto
qed
qed
qed
qed
qed

lemma cycle_rotate_len_arcs:
fixes M :: "('a :: linordered_ab_monoid_add) mat"
assumes "length xs > 1" "(i, j) ∈ arcs' xs"
shows "∃ ys zs. len M a a xs = len M i i (j # ys @ a # zs)
∧ set (arcs a a xs) = set (arcs i i (j # ys @ a # zs)) ∧ xs = zs @ i # j # ys"
using assms
proof -
assume A: "length xs > 1" "(i, j) ∈ arcs' xs"
from arcs'_decomp[OF this] obtain ys zs where xs: "xs = zs @ i # j # ys" by blast
from len_decomp[OF this, of M a a]
have "len M a a xs = len M a i zs + len M i a (j # ys)" .
also have "… = len M i a (j # ys) + len M a i zs" by (simp add: comm)
also from len_comp[of M i i "j # ys" a zs] have "… = len M i i (j # ys @ a # zs)" by auto
finally show ?thesis
using xs arcs_decomp[OF xs, of a a] arcs_decomp[of "j # ys @ a # zs" "j # ys" a zs i i] by force
qed

lemma cycle_rotate_2':
fixes M :: "('a :: linordered_ab_monoid_add) mat"
assumes "xs ≠ []" "(i, j) ∈ set (arcs a a xs)"
shows "∃ ys. len M a a xs = len M i i (j # ys) ∧ set (i # j # ys) = set (a # xs)
∧ 1 + length ys = length xs ∧ set (arcs a a xs) = set (arcs i i (j # ys))"
proof -
note A = assms
{ fix ys assume A:"a = i" "xs = j # ys"
then have ?thesis by auto
} note * = this
{ fix b ys assume A:"a = j" "xs = ys @ [i]"
then have ?thesis
proof (auto, goal_cases)
case 1
have "len M j j (ys @ [i]) = M i j + len M j i ys"
using len_decomp[of `