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› 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: 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: 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: fixes M :: "('a::linordered_ab_monoid_add) mat" 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: fixes M :: "('a::linordered_ab_monoid_add) mat" 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) 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 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) 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+ 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 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: 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: 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 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: 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)") apply (simp add: arcs_decomp) apply (simp only: append_Cons[symmetric]) using successive_split[of "((a, z) # arcs z i zs') @ [(i, j), (j, a)]" _ "[(j, a)]" P] apply auto[] subgoal (* Generated by sledgehammer *) proof simp assume a1: "successive P ((a, z) # arcs z a (zs' @ [i, j]))" assume a2: "¬ P (a, z)" assume a3: "zs = z # zs'" assume a4: "ys = []" assume a5: "xs = z # zs' @ [i, j]" have f6: "∀p pa ps. ¬ successive p ((pa::nat × nat) # ps) ∨ p pa ∨ successive p ps" by (meson successive_step