# Theory Timed_Automata.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 "ys @ [i]" ys i "[]" M j j] by (auto simp: comm)
moreover have "arcs j j (ys @ [i]) = arcs j i ys @ [(i, j)]" using arcs_decomp_tail by auto
ultimately show ?case by auto
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)")
case True
with ys * show ?thesis by blast
next
case False
then show ?thesis
proof (cases "(i,j) = (c,a)", goal_cases)
case True
with ys ** show ?thesis by force
next
case 2
with A(2) ys have "(i, j) ∈ arcs' xs"
using cycle_rotate_2_aux by (auto simp add: arcs'_def) (* slow *)
from cycle_rotate_len_arcs[OF ‹length xs > 1› this, of M a] show ?thesis by auto
qed
qed
qed
qed
qed

section ‹Equivalent Characterizations of Cycle-Freeness›

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

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

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

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

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

lemma cyc_free_diag_dest:
assumes "cyc_free M n" "i ≤ n" "set xs ⊆ {0..n}"
shows "len M i i xs ≥ 𝟭"
using assms by auto

lemma cycle_free_0_0:
assumes "cycle_free M n"
shows "M 0 0 ≥ 𝟭"
using cyc_free_diag_dest[OF cycle_free_diag_dest[OF assms], of 0 "[]"] by auto

section ‹More Theorems Related to Floyd-Warshall›

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

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

abbreviation "FW m n ≡ fw m n n n n"

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

lemma cyc_free_diag_dest':
"cyc_free m n ⟹ i ≤ n ⟹ m i i ≥ 𝟭"
proof goal_cases
case 1
then have "i ≤ n ∧ set [] ⊆ {0..n}" by auto
with 1(1) have "𝟭 ≤ len m i i []" by blast
then show ?case by auto
qed

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

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

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

lemma fw_upd_canonical_id:
"canonical M n ⟹ i ≤ n ⟹ j ≤ n ⟹ k ≤ n ⟹ fw_upd M k i j = M"
by (auto simp: fw_upd_def upd_def)

lemma fw_canonical_id:
"canonical M n ⟹ i ≤ n ⟹ j ≤ n ⟹ k ≤ n ⟹ fw M n k i j = M"
proof (induction k arbitrary: i j)
case 0
then show ?case
proof (induction i arbitrary: j)
case 0
then show ?case
proof (induction j)
case 0 thus ?case by (auto intro: fw_upd_canonical_id)
next
case Suc thus ?case by (auto intro: fw_upd_canonical_id)
qed
next
case Suc
then show ?case
proof (induction j)
case 0 thus ?case by (auto intro: fw_upd_canonical_id)
next
case Suc thus ?case by (auto intro: fw_upd_canonical_id)
qed
qed
next
case Suc
then show ?case
proof (induction i arbitrary: j)
case 0
then show ?case
proof (induction j)
case 0 thus ?case by (auto intro: fw_upd_canonical_id)
next
case Suc thus ?case by (auto intro: fw_upd_canonical_id)
qed
next
case Suc
then show ?case
proof (induction j)
case 0 thus ?case by (auto intro: fw_upd_canonical_id)
next
case Suc thus ?case by (auto intro: fw_upd_canonical_id)
qed
qed
qed

lemmas FW_canonical_id = fw_canonical_id[OF _ order.refl order.refl order.refl]

section ‹Helper Lemmas for Bouyer's Theorem on Approximation›

lemma aux1: "i ≤ n ⟹ j ≤ n ⟹ set xs ⊆ {0..n} ⟹ (a,b) ∈ set (arcs i j xs) ⟹ a ≤ n ∧ b ≤ n"
by (induction xs arbitrary: i) auto

lemma arcs_distinct1:
"i ∉ set xs ⟹ j ∉ set xs ⟹ distinct xs ⟹ xs ≠ [] ⟹ (a,b) ∈ set (arcs i j xs) ⟹ a ≠ b"
apply (induction xs arbitrary: i)
apply fastforce
apply (rename_tac a' xs i)
apply (case_tac xs)
apply auto
done

lemma arcs_distinct2:
"i ∉ set xs ⟹ j ∉ set xs ⟹ distinct xs ⟹ i ≠ j ⟹ (a,b) ∈ set (arcs i j xs) ⟹ a ≠ b"
by (induction xs arbitrary: i) auto

lemma arcs_distinct3: "distinct (a # b # c # xs) ⟹ (i,j) ∈ set (arcs a b xs) ⟹ i ≠ c ∧ j ≠ c"
by (induction xs arbitrary: a) force+

lemma arcs_elem:
assumes "(a, b) ∈ set (arcs i j xs)" shows "a ∈ set (i # xs)" "b ∈ set (j # xs)"
using assms by (induction xs arbitrary: i) auto

lemma arcs_distinct_dest1:
"distinct (i # a # zs) ⟹ (b,c) ∈ set (arcs a j zs) ⟹ b ≠ i"
using arcs_elem by fastforce

lemma arcs_distinct_fix:
"distinct (a # x # xs @ [b]) ⟹ (a,c) ∈ set (arcs a b (x # xs)) ⟹ c = x"
using arcs_elem(1) by fastforce

lemma disjE3: "A ∨ B ∨ C ⟹ (A ⟹ G) ⟹ (B ⟹ G) ⟹ (C ⟹ G) ⟹ G"
by auto

lemma arcs_predecessor:
assumes "(a, b) ∈ set (arcs i j xs)" "a ≠ i"
shows "∃ c. (c, a) ∈ set (arcs i j xs)" using assms
by (induction xs arbitrary: i) auto

lemma arcs_successor:
assumes "(a, b) ∈ set (arcs i j xs)" "b ≠ j"
shows "∃ c. (b,c) ∈ set (arcs i j xs)" using assms
apply (induction xs arbitrary: i)
apply simp
apply (rename_tac aa xs i)
apply (case_tac xs)
by auto

lemma arcs_predecessor':
assumes "(a, b) ∈ set (arcs i j (x # xs))" "(a,b) ≠ (i, x)"
shows "∃ c. (c, a) ∈ set (arcs i j (x # xs))" using assms
by (induction xs arbitrary: i x) auto

lemma arcs_cases:
assumes "(a, b) ∈ set (arcs i j xs)" "xs ≠ []"
shows "(∃ ys. xs = b # ys ∧ a = i) ∨ (∃ ys. xs = ys @ [a] ∧ b = j)
∨ (∃ c d ys. (a,b) ∈ set (arcs c d ys) ∧ xs = c # ys @ [d])"
using assms
proof (induction xs arbitrary: i)
case Nil then show ?case by auto
next
case (Cons x xs)
show ?case
proof (cases "(a, b) = (i, x)")
case True
with Cons.prems show ?thesis by auto
next
case False
note F = this
show ?thesis
proof (cases "xs = []")
case True
with F Cons.prems show ?thesis by auto
next
case False
from F Cons.prems have "(a, b) ∈ set (arcs x j xs)" by auto
from Cons.IH[OF this False] have
"(∃ys. xs = b # ys ∧ a = x) ∨ (∃ys. xs = ys @ [a] ∧ b = j)
∨ (∃c d ys. (a, b) ∈ set (arcs c d ys) ∧ xs = c # ys @ [d])"
.
then show ?thesis
proof (rule disjE3, goal_cases)
case 1
from 1 obtain ys where *: "xs = b # ys ∧ a = x" by auto
show ?thesis
proof (cases "ys = []")
case True
with * show ?thesis by auto
next
case False
then obtain z zs where zs: "ys = zs @ [z]" by (metis append_butlast_last_id)
with * show ?thesis by auto
qed
next
case 2 then show ?case by auto
next
case 3 with False show ?case by auto
qed
qed
qed
qed

lemma arcs_cases':
assumes "(a, b) ∈ set (arcs i j xs)" "xs ≠ []"
shows "(∃ ys. xs = b # ys ∧ a = i) ∨ (∃ ys. xs = ys @ [a] ∧ b = j) ∨ (∃ ys zs. xs = ys @ a # b # zs)"
using assms
proof (induction xs arbitrary: i)
case Nil then show ?case by auto
next
case (Cons x xs)
show ?case
proof (cases "(a, b) = (i, x)")
case True
with Cons.prems show ?thesis by auto
next
case False
note F = this
show ?thesis
proof (cases "xs = []")
case True
with F Cons.prems show ?thesis by auto
next
case False
from F Cons.prems have "(a, b) ∈ set (arcs x j xs)" by auto
from Cons.IH[OF this False] have
"(∃ys. xs = b # ys ∧ a = x) ∨ (∃ys. xs = ys @ [a] ∧ b = j)
∨ (∃ys zs. xs = ys @ a # b # zs)"
.
then show ?thesis
proof (rule disjE3, goal_cases)
case 1
from 1 obtain ys where *: "xs = b # ys ∧ a = x" by auto
show ?thesis
proof (cases "ys = []")
case True
with * show ?thesis by auto
next
case False
then obtain z zs where zs: "ys = zs @ [z]" by (metis append_butlast_last_id)
with * show ?thesis by auto
qed
next
case 2 then show ?case by auto
next
case 3
then obtain ys zs where "xs = ys @ a # b # zs" by auto
then have "x # xs = (x # ys) @ a # b # zs" by auto
then show ?thesis by blast
qed
qed
qed
qed

lemma arcs_successor':
assumes "(a, b) ∈ set (arcs i j xs)" "b ≠ j"
shows "∃ c. xs = [b] ∧ a = i ∨ (∃ ys. xs = b # c # ys ∧ a = i) ∨ (∃ ys. xs = ys @ [a,b] ∧ c = j)
∨ (∃ ys zs. xs = ys @ a # b # c # zs)"
using assms
proof (induction xs arbitrary: i)
case Nil then show ?case by auto
next
case (Cons x xs)
show ?case
proof (cases "(a, b) = (i, x)")
case True
with Cons.prems show ?thesis by (cases xs) auto
next
case False
note F = this
show ?thesis
proof (cases "xs = []")
case True
with F Cons.prems show ?thesis by auto
next
case False
from F Cons.prems have "(a, b) ∈ set (arcs x j xs)" by auto
from Cons.IH[OF this ‹b ≠ j›] obtain c where c:
"xs = [b] ∧ a = x ∨ (∃ys. xs = b # c # ys ∧ a = x) ∨ (∃ys. xs = ys @ [a, b] ∧ c = j)
∨ (∃ys zs. xs = ys @ a # b # c # zs)"
..
then show ?thesis
proof (standard, goal_cases)
case 1 with Cons.prems show ?case by auto
next
case 2
then show ?thesis
proof (rule disjE3, goal_cases)
case 1
from 1 obtain ys where *: "xs = b # ys ∧ a = x" by auto
show ?thesis
proof (cases "ys = []")
case True
with * show ?thesis by auto
next
case False
then obtain z zs where zs: "ys = z # zs" by (cases ys) auto
with * show ?thesis by fastforce
qed
next
case 2 then show ?case by auto
next
case 3
then obtain ys zs where "xs = ys @ a # b # c # zs" by auto
then have "x # xs = (x # ys) @ a # b # c # zs" by auto
then show ?thesis by blast
qed
qed
qed
qed
qed

lemma list_last:
"xs = [] ∨ (∃ y ys. xs = ys @ [y])"
by (induction xs) auto

lemma arcs_predecessor'':
assumes "(a, b) ∈ set (arcs i j xs)" "a ≠ i"
shows "∃ c. xs = [a] ∨ (∃ ys. xs = a # b # ys) ∨ (∃ ys. xs = ys @ [c,a] ∧ b = j)
∨ (∃ ys zs. xs = ys @ c # a # b # zs)"
using assms
proof (induction xs arbitrary: i)
case Nil then show ?case by auto
next
case (Cons x xs)
show ?case
proof (cases "(a, b) = (i, x)")
case True
with Cons.prems show ?thesis by (cases xs) auto
next
case False
note F = this
show ?thesis
proof (cases "xs = []")
case True
with F Cons.prems show ?thesis by auto
next
case False
from F Cons.prems have *: "(a, b) ∈ set (arcs x j xs)" by auto
from False obtain y ys where xs: "xs = y # ys" by (cases xs) auto
show ?thesis
proof (cases "(a,b) = (x,y)")
case True with * xs show ?thesis by auto
next
case False
with * xs have **: "(a, b) ∈ set (arcs y j ys)" by auto
show ?thesis
proof (cases "ys = []")
case True with ** xs show ?thesis by force
next
case False
from arcs_cases'[OF ** this] obtain ws zs where ***:
"ys = b # ws ∧ a = y ∨ ys = ws @ [a] ∧ b = j ∨ ys = ws @ a # b # zs"
by auto
then show ?thesis
apply rule
using xs apply blast
apply safe
using xs list_last[of ws] apply -
apply (rotate_tac 3)
apply (case_tac "ws = []")
apply auto[]
apply (subgoal_tac "∃y ys. ws = ys @ [y]")
apply fastforce
apply simp
apply (case_tac "ws = []")
apply (subgoal_tac "x # xs = [x] @ y # a # b # zs")
apply (rule exI[where x = y])
apply blast
apply simp
subgoal
proof goal_cases
case 1
then obtain u us where "ws = us @ [u]" by auto
with 1(1,2) have "x # xs = (x # y # us) @ u # a # b # zs" by auto
then show ?case by blast
qed
done
qed
qed
qed
qed
qed

lemma arcs_ex_middle:
"∃ b. (a, b) ∈ set (arcs i j (ys @ a # xs))"
by (induction xs arbitrary: i ys) (auto simp: arcs_decomp)

"∃ b. (i, b) ∈ set (arcs i j xs)"
by (cases xs) auto

subsection ‹Successive›

fun successive where
"successive _ [] = True" |
"successive P [_] = True" |
"successive P (x # y # xs) ⟷ ¬ P y ∧ successive P xs ∨ ¬ P x ∧ successive P (y # xs)"

lemma "¬ successive (λ x. x > (0 :: nat)) [Suc 0, Suc 0]" by simp
lemma "successive (λ x. x > (0 :: nat)) [Suc 0]" by simp
lemma "successive (λ x. x > (0 :: nat)) [Suc 0, 0, Suc 0]" by simp
lemma "¬ successive (λ x. x > (0 :: nat)) [Suc 0, 0, Suc 0, Suc 0]" by simp
lemma "¬ successive (λ x. x > (0 :: nat)) [Suc 0, 0, 0, Suc 0, Suc 0]" by simp
lemma "successive (λ x. x > (0 :: nat)) [Suc 0, 0, Suc 0, 0, Suc 0]" by simp
lemma "¬ successive (λ x. x > (0 :: nat)) [Suc 0, Suc 0, 0, Suc 0]" by simp
lemma "successive (λ x. x > (0 :: nat)) [0, 0, Suc 0, 0]" by simp

lemma successive_step: "successive P (x # xs) ⟹ ¬ P x ⟹ successive P xs"
apply (cases xs)
apply simp
apply (rename_tac y ys)
apply (case_tac ys)
apply auto
done

lemma successive_step_2: "successive P (x # y # xs) ⟹ ¬ P y ⟹ successive P xs"
apply (cases xs)
apply simp
apply (rename_tac z zs)
apply (case_tac zs)
apply auto
done

lemma successive_stepI:
"successive P xs ⟹ ¬ P x ⟹ successive P (x # xs)"
by (cases xs) auto

theorem list_two_induct[case_names Nil Single Cons]:
fixes P :: "'a list ⇒ bool"
and list :: "'a list"
assumes Nil: "P []"
assumes Single: "⋀ x. P [x]"
and Cons: "⋀x1 x2 xs. P xs ⟹ P (x2 # xs) ⟹ P (x1 # x2 # xs)"
shows "P xs"
using assms
apply (induction "length xs" arbitrary: xs rule: less_induct)
apply (rename_tac xs)
apply (case_tac xs)
apply simp
apply (rename_tac ys)
apply (case_tac ys)
apply simp
apply (rename_tac zs)
apply (case_tac zs)
by auto

lemma successive_end_1:
"successive P xs ⟹ ¬ P x ⟹ successive P (xs @ [x])"
by (induction _ xs rule: list_two_induct) auto

lemma successive_ends_1:
"successive P xs ⟹ ¬ P x ⟹ successive P ys ⟹ successive P (xs @ x # ys)"
by (induction _ xs rule: list_two_induct) (fastforce intro: successive_stepI)+

lemma successive_ends_1':
"successive P xs ⟹ ¬ P x ⟹ P y ⟹ ¬ P z ⟹ successive P ys ⟹ successive P (xs @ x # y # z # ys)"
by (induction _ xs rule: list_two_induct) (fastforce intro: successive_stepI)+

lemma successive_end_2:
"successive P xs ⟹ ¬ P x ⟹ successive P (xs @ [x,y])"
by (induction _ xs rule: list_two_induct) auto

lemma successive_end_2':
"successive P (xs @ [x]) ⟹ ¬ P x ⟹ successive P (xs @ [x,y])"
by (induction _ xs rule: list_two_induct) auto

lemma successive_end_3:
"successive P (xs @ [x]) ⟹ ¬ P x ⟹ P y ⟹ ¬ P z ⟹ successive P (xs @ [x,y,z])"
by (induction _ xs rule: list_two_induct) auto

lemma successive_step_rev:
"successive P (xs @ [x]) ⟹ ¬ P x ⟹ successive P xs"
by (induction _ xs rule: list_two_induct) auto

lemma successive_glue:
"successive P (zs @ [z]) ⟹ successive P (x # xs) ⟹ ¬ P z ∨ ¬ P x ⟹ successive P (zs @ [z] @ x # xs)"
proof goal_cases
case A: 1
show ?thesis
proof (cases "P x")
case False
with A(1,2) successive_ends_1 successive_step show ?thesis by fastforce
next
case True
with A(1,3) successive_step_rev have "¬ P z" "successive P zs" by fastforce+
with A(2) successive_ends_1 show ?thesis by fastforce
qed
qed

lemma successive_glue':
"successive P (zs @ [y]) ∧ ¬ P z ∨ successive P zs ∧ ¬ P y
⟹ successive P (x # xs) ∧ ¬ P w ∨ successive P xs ∧ ¬ P x
⟹ ¬ P z ∨ ¬ P w ⟹ successive P (zs @ y # z # w # x # xs)"
by (metis append_Cons append_Nil successive.simps(3) successive_ends_1 successive_glue successive_stepI)

"xs = w # x # ys ⟹ successive P xs ⟹ successive P (x # xs) ∧ ¬ P w ∨ successive P xs ∧ ¬ P x"
by auto

lemma successive_dest_tail:
"xs = zs @ [y,z] ⟹ successive P xs ⟹ successive P (zs @ [y]) ∧ ¬ P z ∨ successive P zs ∧ ¬ P y"
apply (induction _ xs arbitrary: zs rule: list_two_induct)
apply simp+
apply (rename_tac zs)
apply (case_tac zs)
apply simp
apply (rename_tac ws)
apply (case_tac ws)
apply force+
done

lemma successive_split:
"xs = ys @ zs ⟹ successive P xs ⟹ successive P ys ∧ successive P zs"
apply (induction _ xs arbitrary: ys rule: list_two_induct)
apply simp
apply (rename_tac ys, case_tac ys)
apply simp
apply simp
apply (rename_tac ys, case_tac ys)
apply simp
apply (rename_tac list, case_tac list)
apply (auto intro: successive_stepI)
done

lemma successive_decomp:
"xs = x # ys @ zs @ [z] ⟹ successive P xs ⟹ ¬ P x ∨ ¬ P z ⟹ successive P (zs @ [z] @ (x # ys))"
by (metis Cons_eq_appendI successive_glue successive_split)

lemma successive_predecessor:
assumes "(a, b) ∈ set (arcs i j xs)" "a ≠ i" "successive P (arcs i j xs)" "P (a,b)" "xs ≠ []"
shows "∃ c. (xs = [a] ∧ c = i ∨ (∃ ys. xs = a # b # ys ∧ c = i) ∨ (∃ ys. xs = ys @ [c,a] ∧ b = j)
∨ (∃ ys zs. xs = ys @ c # a # b # zs)) ∧ ¬ P (c,a)"
proof -
from arcs_predecessor''[OF assms(1,2)] obtain c where c:
"xs = [a] ∨ (∃ys. xs = a # b # ys) ∨ (∃ys. xs = ys @ [c, a] ∧ b = j)
∨ (∃ys zs. xs = ys @ c # a # b # zs)"
by auto
then show ?thesis
proof (safe, goal_cases)
case 1
with assms have "arcs i j xs = [(i, a), (a, j)]" by auto
with assms have "¬ P (i, a)" by auto
with 1 show ?case by simp
next
case 2
with assms have "¬ P (i, a)" by fastforce
with 2 show ?case by auto
next
case 3
with assms have "¬ P (c, a)" using arcs_decomp successive_dest_tail by fastforce
with 3 show ?case by auto
next
case 4
with assms(3,4) have "¬ P (c, a)" using arcs_decomp successive_split by fastforce
with 4 show ?case by auto
qed
qed

thm arcs_successor'

lemma successive_successor:
assumes "(a, b) ∈ set (arcs i j xs)" "b ≠ j" "successive P (arcs i j xs)" "P (a,b)" "xs ≠ []"
shows "∃ c. (xs = [b] ∧ c = j ∨ (∃ ys. xs = b # c # ys) ∨ (∃ ys. xs = ys @ [a,b] ∧ c = j)
∨ (∃ ys zs. xs = ys @ a # b # c # zs)) ∧ ¬ P (b,c)"
proof -
from arcs_successor'[OF assms(1,2)] obtain c where c:
"xs = [b] ∧ a = i ∨ (∃ys. xs = b # c # ys ∧ a = i) ∨ (∃ys. xs = ys @ [a, b] ∧ c = j)
∨ (∃ys zs. xs = ys @ a # b # c # zs)"
..
then show ?thesis
proof (safe, goal_cases)
case 1
with assms(1,2) have "arcs i j xs = [(a,b), (b,j)]" by auto
with assms have "¬ P (b,j)" by auto
with 1 show ?case by simp
next
case 2
with assms have "¬ P (b, c)" by fastforce
with 2 show ?case by auto
next
case 3
with assms have "¬ P (b, c)" using arcs_decomp successive_dest_tail by fastforce
with 3 show ?case by auto
next
case 4
with assms(3,4) have "¬ P (b, c)" using arcs_decomp successive_split by fastforce
with 4 show ?case by auto
qed
qed

subsubsection ‹Obtaining successive and distinct paths›

lemma canonical_successive:
fixes A B
defines "M ≡ λ i j. min (A i j) (B i j)"
assumes "canonical A n"
assumes "set xs ⊆ {0..n}"
assumes "i ≤ n" "j ≤ n"
shows "∃ ys. len M i j ys ≤ len M i j xs ∧ set ys ⊆ {0..n}
∧ successive (λ (a, b). M a b = A a b) (arcs i j ys)"
using assms
proof (induction xs arbitrary: i rule: list_two_induct)
case Nil show ?case by fastforce
next
case 2: (Single x i)
show ?case
proof (cases "M i x = A i x ∧ M x j = A x j")
case False
then have "successive (λ(a, b). M a b = A a b) (arcs i j [x])" by auto
with 2 show ?thesis by blast
next
case True
with 2 have "M i j ≤ M i x + M x j" unfolding min_def by fastforce
with 2(3-) show ?thesis apply simp apply (rule exI[where x = "[]"]) by auto
qed
next
case 3: (Cons x y xs i)
show ?case
proof (cases "M i y ≤ M i x + M x y", goal_cases)
case 1
from 3 obtain ys where
"len M i j ys ≤ len M i j (y # xs) ∧ set ys ⊆ {0..n}
∧ successive (λa. case a of (a, b) ⇒ M a b = A a b) (arcs i j ys)"
by fastforce
moreover from 1 have "len M i j (y # xs) ≤ len M i j (x # y # xs)"
using add_mono by (auto simp: assoc[symmetric])
ultimately show ?case by force
next
case False
{ assume "M i x = A i x" "M x y = A x y"
with 3(3-) have "A i y ≤ M i x + M x y" by auto
then have "M i y ≤ M i x + M x y" unfolding M_def min_def by auto
} note * = this
with False have "M i x ≠ A i x ∨ M x y ≠ A x y" by auto
then show ?thesis
proof (standard, goal_cases)
case 1
from 3 obtain ys where ys:
"len M x j ys ≤ len M x j (y # xs)" "set ys ⊆ {0..n}"
"successive (λa. case a of (a, b) ⇒ M a b = A a b) (arcs x j ys)"
by force+
from 1 successive_stepI[OF ys(3), of "(i, x)"] have
"successive (λa. case a of (a, b) ⇒ M a b = A a b) (arcs i j (x # ys))"
by auto
moreover have "len M i j (x # ys) ≤ len M i j (x # y # xs)" using add_mono_right[OF ys(1)]
by auto
ultimately show ?case using 3(5) ys(2) by fastforce
next
case 2
from 3 obtain ys where ys:
"len M y j ys ≤ len M y j xs" "set ys ⊆ {0..n}"
"successive (λa. case a of (a, b) ⇒ M a b = A a b) (arcs y j ys)"
by force+
from this(3) 2 have
"successive (λa. case a of (a, b) ⇒ M a b = A a b) (arcs i j (x # y # ys))"
by simp
"len M i j (x # y # ys) ≤ len M i j (x # y # xs)"
by (auto simp: assoc[symmetric])
ultimately show ?thesis using ys(2) 3(5) by fastforce
qed
qed
qed

lemma canonical_successive_distinct:
fixes A B
defines "M ≡ λ i j. min (A i j) (B i j)"
assumes "canonical A n"
assumes "set xs ⊆ {0..n}"
assumes "i ≤ n" "j ≤ n"
assumes "distinct xs" "i ∉ set xs" "j ∉ set xs"
shows "∃ ys. len M i j ys ≤ len M i j xs ∧ set ys ⊆ set xs
∧ successive (λ (a, b). M a b = A a b) (arcs i j ys)
∧ distinct ys ∧ i ∉ set ys ∧ j ∉ set ys"
using assms
proof (induction xs arbitrary: i rule: list_two_induct)
case Nil show ?case by fastforce
next
case 2: (Single x i)
show ?case
proof (cases "M i x = A i x ∧ M x j = A x j")
case False
then have "successive (λ(a, b). M a b = A a b) (arcs i j [x])" by auto
with 2 show ?thesis by blast
next
case True
with 2 have "M i j ≤ M i x + M x j" unfolding min_def by fastforce
with 2(3-) show ?thesis apply simp apply (rule exI[where x = "[]"]) by auto
qed
next
case 3: (Cons x y xs i)
show ?case
proof (cases "M i y ≤ M i x + M x y")
case 1: True
from 3(2)[OF 3(3,4)] 3(5-10) obtain ys where ys:
"len M i j ys ≤ len M i j (y # xs)" "set ys ⊆ set (x # y # xs)"
"successive (λa. case a of (a, b) ⇒ M a b = A a b) (arcs i j ys)"
"distinct ys ∧ i ∉ set ys ∧ j ∉ set ys"
by fastforce
moreover from 1 have "len M i j (y # xs) ≤ len M i j (x # y # xs)"
using add_mono by (auto simp: assoc[symmetric])
ultimately have "len M i j ys ≤ len M i j (x # y # xs)" by auto
then show ?thesis using ys(2-) by blast
next
case False
{ assume "M i x = A i x" "M x y = A x y"
with 3(3-) have "A i y ≤ M i x + M x y" by auto
then have "M i y ≤ M i x + M x y" unfolding M_def min_def by auto
} note * = this
with False have "M i x ≠ A i x ∨ M x y ≠ A x y" by auto
then show ?thesis
proof (standard, goal_cases)
case 1
from 3(2)[OF 3(3,4)] 3(5-10) obtain ys where ys:
"len M x j ys ≤ len M x j (y # xs)" "set ys ⊆ set (y # xs)"
"successive (λa. case a of (a, b) ⇒ M a b = A a b) (arcs x j ys)"
"distinct ys" "i ∉ set ys" "x ∉ set ys" "j ∉ set ys"
by fastforce
from 1 successive_stepI[OF ys(3), of "(i, x)"] have
"successive (λa. case a of (a, b) ⇒ M a b = A a b) (arcs i j (x # ys))"
by auto
moreover have "len M i j (x # ys) ≤ len M i j (x # y # xs)" using add_mono_right[OF ys(1)]
by auto
moreover have "distinct (x # ys)" "i ∉ set (x # ys)" "j ∉ set (x # ys)" using ys(4-) 3(8-)
by auto
moreover from ys(2) have "set (x # ys) ⊆ set (x # y # xs)" by auto
ultimately show ?case by fastforce
next
case 2
from 3(1)[OF 3(3,4)] 3(5-) obtain ys where ys:
"len M y j ys ≤ len M y j xs" "set ys ⊆ set xs"
"successive (λa. case a of (a, b) ⇒ M a b = A a b) (arcs y j ys)"
"distinct ys" "j ∉ set ys" "y ∉ set ys" "i ∉ set ys" "x ∉ set ys"
by fastforce
from this(3) 2 have
"successive (λa. case a of (a, b) ⇒ M a b = A a b) (arcs i j (x # y # ys))"
by simp
"len M i j (x # y # ys) ≤ len M i j (x # y # xs)"
by (auto simp: assoc[symmetric])
moreover have "distinct (x # y # ys)" "i ∉ set (x # y # ys)" "j ∉ set (x # y # ys)"
using ys(4-) 3(8-) by auto
ultimately show ?thesis using ys(2) by fastforce
qed
qed
qed

lemma successive_snd_last: "successive P (xs @ [x, y]) ⟹ P y ⟹ ¬ P x"
by (induction _ xs rule: list_two_induct) auto

lemma canonical_shorten_rotate_neg_cycle:
fixes A B
defines "M ≡ λ i j. min (A i j) (B i j)"
assumes "canonical A n"
assumes "set xs ⊆ {0..n}"
assumes "i ≤ n"
assumes "len M i i xs < 𝟭"
shows "∃ j ys. len M j j ys < 𝟭 ∧ set (j # ys) ⊆ set (i # xs)
∧ successive (λ (a, b). M a b = A a b) (arcs j j ys)
∧ distinct ys ∧ j ∉ set ys ∧
(ys ≠ [] ⟶ M j (hd ys) ≠ A j (hd ys) ∨ M (last ys) j ≠ A (last ys) j)"
using assms
proof -
note A = assms
from negative_len_shortest[OF _ A(5)] obtain j ys where ys:
"distinct (j # ys)" "len M j j ys < 𝟭" "j ∈ set (i # xs)" "set ys ⊆ set xs"
by blast
from this(1,3) canonical_successive_distinct[OF A(2) subset_trans[OF this(4) A(3)], of j j B] A(3,4)
obtain zs where zs:
"len M j j zs ≤ len M j j ys"
"set zs ⊆ set ys" "successive (λ(a, b). M a b = A a b) (arcs j j zs)"
"distinct zs" "j ∉ set zs"
by (force simp: M_def)
show ?thesis
proof (cases "zs = []")
assume "zs ≠ []"
then obtain w ws where ws: "zs = w # ws" by (cases zs) auto
show ?thesis
proof (cases "ws = []")
case False
then obtain u us where us: "ws = us @ [u]" by (induction ws) auto
show ?thesis
proof (cases "M j w = A j w ∧ M u j = A u j")
case True
have "u ≤ n" "j ≤ n" "w ≤ n" using us ws zs(2) ys(3,4) A(3,4) by auto
with A(2) True have "M u w ≤ M u j + M j w" unfolding M_def min_def by fastforce
then have
"len M u u (w # us) ≤ len M j j zs"
using ws us by (simp add: len_comp comm) (auto intro: add_mono simp: assoc[symmetric])
moreover have "set (u # w # us) ⊆ set (i # xs)" using ws us zs(2) ys(3,4) by auto
moreover have "distinct (w # us)" "u ∉ set (w # us)" using ws us zs(4) by auto
moreover have "successive (λ(a, b). M a b = A a b) (arcs u u (w # us))"
proof (cases us)
case Nil
with zs(3) ws us True show ?thesis by auto
next
case (Cons v vs)
with zs(3) ws us True have "M w v ≠ A w v" by auto
with ws us Cons zs(3) True arcs_decomp_tail successive_split show ?thesis by (simp, blast)
qed
moreover have "M (last (w # us)) u ≠ A (last (w # us)) u"
proof (cases "us = []")
case T: True
with zs(3) ws us True show ?thesis by auto
next
case False
then obtain v vs where vs: "us = vs @ [v]" by (induction us) auto
with ws us have "arcs j j zs = arcs j v (w # vs) @ [(v, u), (u,j)]" by (simp add: arcs_decomp)
with zs(3) True have "M v u ≠ A v u"
using successive_snd_last[of "λ(a, b). M a b = A a b" "arcs j v (w # vs)"] by auto
with vs show ?thesis by simp
qed
ultimately show ?thesis using zs(1) ys(2)
by (intro exI[where x = u], intro exI[where x = "w # us"]) fastforce
next
case False
with zs ws us ys show ?thesis by (intro exI[where x = j], intro exI[where x = "zs"]) auto
qed
next
case True
with True ws zs ys show ?thesis by (intro exI[where x = j], intro exI[where x = "zs"]) fastforce
qed
next
case True
with ys zs show ?thesis by (intro exI[where x = j], intro exI[where x = "zs"]) fastforce
qed
qed

(* Generated by sledgehammer/z3 *)
lemma successive_arcs_extend_last:
"successive P (arcs i j xs) ⟹ ¬ P (i, hd xs) ∨ ¬ P (last xs, j) ⟹ xs ≠ []
⟹ successive P (arcs i j xs @ [(i, hd xs)])"
proof -
assume a1: "¬ P (i, hd xs) ∨ ¬ P (last xs, j)"
assume a2: "successive P (arcs i j xs)"
assume a3: "xs ≠ []"
then have f4: "¬ P (last xs, j) ⟶ successive P (arcs i (last xs) (butlast xs))"
using a2 by (metis (no_types) append_butlast_last_id arcs_decomp_tail successive_step_rev)
have f5: "arcs i j xs = arcs i (last xs) (butlast xs) @ [(last xs, j)]"
using a3 by (metis (no_types) append_butlast_last_id arcs_decomp_tail)
have "([] @ arcs i j xs @ [(i, hd xs)]) @ [(i, hd xs)] = arcs i j xs @ [(i, hd xs), (i, hd xs)]"
by simp
then have "P (last xs, j) ⟶ successive P (arcs i j xs @ [(i, hd xs)])"
using a2 a1 by (metis (no_types) self_append_conv2 successive_end_2 successive_step_rev)
then show ?thesis
using f5 f4 successive_end_2 by fastforce
qed

lemma cycle_rotate_arcs:
fixes M :: "('a :: linordered_ab_monoid_add) mat"
assumes "length xs > 1" "(i, j) ∈ arcs' xs"
shows "∃ ys 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
with arcs_decomp[OF this, of a a] arcs_decomp[of "j # ys @ a # zs" "j # ys" a zs i i]
show ?thesis by force
qed

lemma cycle_rotate_len_arcs_successive:
fixes M :: "('a :: linordered_ab_monoid_add) mat"
assumes "length xs > 1" "(i, j) ∈ arcs' xs" "successive P (arcs a a xs)" "¬ P (a, hd xs) ∨ ¬ P (last xs, a)"
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
∧ successive P (arcs i i (j # ys @ a # zs))"
using assms
proof -
note A = assms
from arcs'_decomp[OF A(1,2)] obtain ys zs where xs: "xs = zs @ i # j # ys" by blast
note arcs1 = arcs_decomp[OF xs, of a a]
note arcs2 = arcs_decomp[of "j # ys @ a # zs" "j # ys" a zs i i]
have *:"successive P (arcs i i (j # ys @ a # zs))"
proof (cases "ys = []")
case True
show ?thesis
proof (cases zs)
case Nil
with A(3,4) xs True show ?thesis by auto
next
case (Cons z zs')
with True arcs2 A(3,4) xs show ?thesis apply simp
by (metis arcs.simps(1,2) arcs1 successive.simps(3) successive_split successive_step)
qed
next
case False
then obtain y ys' where ys: "ys = ys' @ [y]" by (metis append_butlast_last_id)
show ?thesis
proof (cases zs)
case Nil
with A(3,4) xs ys have
"¬ P (a, i) ∨ ¬ P (y, a)" "successive P (arcs a a (i # j # ys' @ [y]))"
by simp+
from successive_decomp[OF _ this(2,1)] show ?thesis using ys Nil arcs_decomp by fastforce
next
case (Cons z zs')
with A(3,4) xs ys have
"¬ P (a, z) ∨ ¬ P (y, a)" "successive P (arcs a a (z # zs' @ i # j # ys' @ [y]))"
by simp+
from successive_decomp[OF _ this(2,1)] show ?thesis using ys Cons arcs_decomp by fastforce
qed
qed
from len_decomp[OF xs, 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 successive_successors:
"xs = ys @ a # b # c # zs ⟹ successive P (arcs i j xs) ⟹ ¬ P (a,b) ∨ ¬ P (b, c)"
apply (induction _ xs arbitrary: i ys rule: list_two_induct)
apply fastforce
apply fastforce
apply (rename_tac ys, case_tac ys)
apply fastforce
apply (rename_tac list, case_tac list)
apply fastforce+
done

lemma successive_successors':
"xs = ys @ a # b # zs ⟹ successive P xs ⟹ ¬ P a ∨ ¬ P b"
using successive_split by fastforce

lemma cycle_rotate_len_arcs_successive':
fixes M :: "('a :: linordered_ab_monoid_add) mat"
assumes "length xs > 1" "(i, j) ∈ arcs' xs" "successive P (arcs a a xs)"
"¬ P (a, hd xs) ∨ ¬ P (last xs, a)"
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
∧ successive P (arcs i i (j # ys @ a # zs) @ [(i,j)])"
using assms
proof -
note A = assms
from arcs'_decomp[OF A(1,2)] obtain ys zs where xs: "xs = zs @ i # j # ys" by blast
note arcs1 = arcs_decomp[OF xs, of a a]
note arcs2 = arcs_decomp[of "j # ys @ a # zs" "j # ys" a zs i i]
have *:"successive P (arcs i i (j # ys @ a # zs) @ [(i,j)])"
proof (cases "ys = []")
case True
show ?thesis
proof (cases zs)
case Nil
with A(3,4) xs True show ?thesis by auto
next
case (Cons z zs')
with True arcs2 A(3,4) xs show ?thesis
apply simp
apply (cases "P (a, z)")