Theory Difference_Bound_Matrices.Paths_Cycles
theory Paths_Cycles
imports Floyd_Warshall.Floyd_Warshall
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
subgoal for a xs i
apply (cases xs)
apply (simp, metis)
by auto
done
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›
lemmas (in linordered_ab_monoid_add) comm = add.commute
lemma len_add:
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"
by (simp add: add.assoc)
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: 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 ‹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]"
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)
with A have ?thesis
by auto
} 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)
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]"
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 have ?thesis using A by auto
} 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)
from cycle_rotate_len_arcs[OF ‹length xs > 1› this, of M a] show ?thesis by auto
qed
qed
qed
qed
qed
section ‹More on Cycle-Freeness›
lemma cyc_free_diag_dest:
assumes "cyc_free M n" "i ≤ n" "set xs ⊆ {0..n}"
shows "len M i i xs ≥ 0"
using assms by auto
lemma cycle_free_0_0:
fixes M :: "('a::linordered_ab_monoid_add) mat"
assumes "cycle_free M n"
shows "M 0 0 ≥ 0"
using cyc_free_diag_dest[OF cycle_free_diag_dest[OF assms], of 0 "[]"] by auto
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
subgoal for a' xs i
by (cases xs) 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
subgoal for aa xs i
by (cases xs) auto
done
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
proof (elim disjE, goal_cases)
case 1
then show ?case using xs by blast
next
case 2
then have "∃y ys. ws = ys @ [y]" if "ws ≠ []"
using list_last[of ws] that by fastforce
with 2 show ?case
using xs by (cases "ws = []") auto
next
case 3
then have "x # xs = [x] @ y # a # b # zs" if "ws = []"
using that by (simp add: xs)
with 3 show ?case
apply (cases "ws = []")
apply blast
by (metis append.left_neutral append_Cons append_assoc list_last xs)
qed
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)
lemma arcs_ex_head:
"∃ 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
subgoal for y ys
by (cases ys) auto
done
lemma successive_step_2: "successive P (x # y # xs) ⟹ ¬ P y ⟹ successive P xs"
apply (cases xs)
apply simp
subgoal for z zs
by (cases zs) auto
done
lemma successive_stepI:
"successive P xs ⟹ ¬ P x ⟹ successive P (x # xs)"
by (cases xs) auto
lemmas list_two_induct[case_names Nil Single Cons] = induct_list012
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)
lemma successive_dest_head:
"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+
subgoal for _ _ _ zs
apply (cases zs)
apply simp
subgoal for _ ws
by (cases ws) auto
done
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
subgoal for _ ys
by (cases ys; simp)
subgoal for _ _ _ ys
apply (cases ys; simp)
subgoal for list
by (cases list) (auto intro: successive_stepI)
done
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
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
lemmas add_mono_right = add_mono[OF order_refl]
lemmas add_mono_left = add_mono[OF _ order_refl]
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: add.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
moreover from add_mono_right[OF ys(1)] have
"len M i j (x # y # ys) ≤ len M i j (x # y # xs)"
by (auto simp: add.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: add.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
moreover from add_mono_right[OF ys(1)] have
"len M i j (x # y # ys) ≤ len M i j (x # y # xs)"
by (auto simp: add.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 < 0"
shows "∃ j ys. len M j j ys < 0 ∧ 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 < 0" "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: add.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
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
subgoal for _ _ _ _ ys
apply (cases ys)
apply fastforce
subgoal for _ list
apply (cases list)
apply fastforce+
done
done
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)")
apply (simp add: arcs_decomp)
using successive_split[of "((a, z) # arcs z i zs') @ [(i, j), (j, a)]" _ "[(j, a)]" P]
apply auto[]
by (metis append_Cons arcs.simps(1,2) arcs1 successive.simps(1) successive_dest_tail
successive_ends_1 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)] ys Nil arcs_decomp have
"successive P (arcs i i (j # ys @ a # zs))"
by fastforce
moreover from * have "¬ P (a, i) ∨ ¬ P (i, j)" by auto
ultimately show ?thesis
by (metis append_Cons last_snoc list.distinct(1) list.sel(1) Nil successive_arcs_extend_last)
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)] ys Cons arcs_decomp have **:
"successive P (arcs i i (j # ys @ a # zs))"
by fastforce
from Cons have "zs ≠ []" by auto
then obtain w ws where ws: "zs = ws @ [w]" by (induction zs) auto
with A(3,4) xs ys have *:
"successive P (arcs a a (ws @ [w] @ i # j # ys' @ [y]))"
by simp
moreover from successive_successors[OF _ this] have "¬ P (w, i) ∨ ¬ P (i, j)" by auto
ultimately show ?thesis
by (metis ** append_is_Nil_conv last.simps last_append list.distinct(2) list.sel(1)
successive_arcs_extend_last ws)
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 cycle_rotate_3:
fixes M :: "('a :: linordered_ab_monoid_add) mat"
assumes "xs ≠ []" "(i, j) ∈ set (arcs a a xs)" "successive P (arcs a a xs)" "¬ P (a, hd xs) ∨ ¬ P (last xs, a)"
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))
∧ successive P (arcs i i (j # ys))"
proof -
note A = assms
{ fix ys assume A:"a = i" "xs = j # ys"
with assms(3) have ?thesis by auto
} note * = this
have **: ?thesis if A: "a = j" "xs = ys @ [i]" for ys using A
proof (safe, 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
moreover with assms(3,4) A have "successive P ((i,j) # arcs j i ys)"
apply simp
apply (cases ys)
apply simp
by (simp, metis arcs.simps(2) calculation(2) 1(1) successive_split successive_step)
ultimately show ?case by auto
qed
{ 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)
from cycle_rotate_len_arcs_successive[OF ‹length xs > 1› this A(3,4), of M] show ?thesis
by auto
qed
qed
qed
qed
qed
lemma cycle_rotate_3':
fixes M :: "('a :: linordered_ab_monoid_add) mat"
assumes "xs ≠ []" "(i, j) ∈ set (arcs a a xs)" "successive P (arcs a a xs)" "¬ P (a, hd xs) ∨ ¬ P (last xs, a)"
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))
∧ successive P (arcs i i (j # ys) @ [(i, j)])"
proof -
note A = assms
have *: ?thesis if "a = i" "xs = j # ys" for ys
using that assms(3) successive_arcs_extend_last[OF assms(3,4)] by auto
have **: ?thesis if A:"a = j" "xs = ys @ [i]" for ys
using A proof (safe, 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
moreover with assms(3,4) A have "successive P ((i,j) # arcs j i ys @ [(i, j)])"
apply simp
apply (cases ys)
apply simp
by (simp, metis successive_step)
ultimately show ?case by auto
qed
{ 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