theory Floyd_Warshall imports Main begin chapter ‹Floyd-Warshall Algorithm for the All-Pairs Shortest Paths Problem› subsubsection ‹Auxiliary› lemma distinct_list_single_elem_decomp: "{xs. set xs ⊆ {0} ∧ distinct xs} = {[], [0]}" proof (standard, goal_cases) case 1 { fix xs :: "'a list" assume xs: "xs ∈ {xs. set xs ⊆ {0} ∧ distinct xs}" have "xs ∈ {[], [0]}" proof (cases xs) case (Cons y ys) hence y: "y = 0" using xs by auto with Cons xs have "ys = []" by (cases ys, auto) thus ?thesis using y Cons by simp qed simp } thus ?case by blast qed simp section ‹Cycles in Lists› abbreviation "cnt x xs ≡ length (filter (λy. x = y) xs)" fun remove_cycles :: "'a list ⇒ 'a ⇒ 'a list ⇒ 'a list" where "remove_cycles [] _ acc = rev acc" | "remove_cycles (x#xs) y acc = (if x = y then remove_cycles xs y [x] else remove_cycles xs y (x#acc))" lemma cnt_rev: "cnt x (rev xs) = cnt x xs" by (metis length_rev rev_filter) value "as @ [x] @ bs @ [x] @ cs @ [x] @ ds" lemma remove_cycles_removes: "cnt x (remove_cycles xs x ys) ≤ max 1 (cnt x ys)" proof (induction xs arbitrary: ys) case Nil thus ?case by (simp, cases "x ∈ set ys", (auto simp: cnt_rev[of x ys])) next case (Cons y xs) thus ?case proof (cases "x = y") case True thus ?thesis using Cons[of "[y]"] True by auto next case False thus ?thesis using Cons[of "y # ys"] by auto qed qed lemma remove_cycles_id: "x ∉ set xs ⟹ remove_cycles xs x ys = rev ys @ xs" by (induction xs arbitrary: ys) auto lemma remove_cycles_cnt_id: "x ≠ y ⟹ cnt y (remove_cycles xs x ys) ≤ cnt y ys + cnt y xs" proof (induction xs arbitrary: ys x) case Nil thus ?case by (simp add: cnt_rev) next case (Cons z xs) thus ?case proof (cases "x = z") case True thus ?thesis using Cons.IH[of z "[z]"] Cons.prems by auto next case False thus ?thesis using Cons.IH[of x "z # ys"] Cons.prems False by auto qed qed lemma remove_cycles_ends_cycle: "remove_cycles xs x ys ≠ rev ys @ xs ⟹ x ∈ set xs" using remove_cycles_id by fastforce lemma remove_cycles_begins_with: "x ∈ set xs ⟹ ∃ zs. remove_cycles xs x ys = x # zs ∧ x ∉ set zs" proof (induction xs arbitrary: ys) case Nil thus ?case by auto next case (Cons y xs) thus ?case proof (cases "x = y") case True thus ?thesis proof (cases "x ∈ set xs", goal_cases) case 1 with Cons show ?case by auto next case 2 with remove_cycles_id[of x xs "[y]"] show ?case by auto qed next case False with Cons show ?thesis by auto qed qed lemma remove_cycles_self: "x ∈ set xs ⟹ remove_cycles (remove_cycles xs x ys) x zs = remove_cycles xs x ys" proof - assume x:"x ∈ set xs" then obtain ws where ws: "remove_cycles xs x ys = x # ws" "x ∉ set ws" using remove_cycles_begins_with[OF x, of ys] by blast from remove_cycles_id[OF this(2)] have "remove_cycles ws x [x] = x # ws" by auto with ws(1) show "remove_cycles (remove_cycles xs x ys) x zs = remove_cycles xs x ys" by simp qed lemma remove_cycles_one: "remove_cycles (as @ x # xs) x ys = remove_cycles (x#xs) x ys" by (induction as arbitrary: ys) auto lemma remove_cycles_cycles: "x ∈ set xs ⟹ ∃ xxs as. as @ concat (map (λ xs. x # xs) xxs) @ remove_cycles xs x ys = xs ∧ x ∉ set as" proof (induction xs arbitrary: ys) case Nil thus ?case by auto next case (Cons y xs) thus ?case proof (cases "x = y") case True thus ?thesis proof (cases "x ∈ set xs", goal_cases) case 1 then obtain as xxs where "as @ concat (map (λxs. y#xs) xxs) @ remove_cycles xs y [y] = xs" using Cons.IH[of "[y]"] by auto hence "[] @ concat (map (λxs. x#xs) (as#xxs)) @ remove_cycles (y#xs) x ys = y # xs" by (simp add: ‹x = y›) thus ?thesis by fastforce next case 2 hence "remove_cycles (y # xs) x ys = y # xs" using remove_cycles_id[of x xs "[y]"] by auto hence "[] @ concat (map (λxs. x # xs) []) @ remove_cycles (y#xs) x ys = y # xs" by auto thus ?thesis by fastforce qed next case False then obtain as xxs where as: "as @ concat (map (λxs. x # xs) xxs) @ remove_cycles xs x (y#ys) = xs" "x ∉ set as" using Cons.IH[of "y # ys"] Cons.prems by auto hence "(y # as) @ concat (map (λxs. x # xs) xxs) @ remove_cycles (y#xs) x ys = y # xs" using ‹x ≠ y› by auto thus ?thesis using as(2) ‹x ≠ y› by fastforce qed qed fun start_remove :: "'a list ⇒ 'a ⇒ 'a list ⇒ 'a list" where "start_remove [] _ acc = rev acc" | "start_remove (x#xs) y acc = (if x = y then rev acc @ remove_cycles xs y [y] else start_remove xs y (x # acc))" lemma start_remove_decomp: "x ∈ set xs ⟹ ∃ as bs. xs = as @ x # bs ∧ start_remove xs x ys = rev ys @ as @ remove_cycles bs x [x]" proof (induction xs arbitrary: ys) case Nil thus ?case by auto next case (Cons y xs) thus ?case proof (auto, goal_cases) case 1 from 1(1)[of "y # ys"] obtain as bs where "xs = as @ x # bs" "start_remove xs x (y # ys) = rev (y # ys) @ as @ remove_cycles bs x [x]" by blast hence "y # xs = (y # as) @ x # bs" "start_remove xs x (y # ys) = rev ys @ (y # as) @ remove_cycles bs x [x]" by simp+ thus ?case by blast qed qed lemma start_remove_removes: "cnt x (start_remove xs x ys) ≤ Suc (cnt x ys)" proof (induction xs arbitrary: ys) case Nil thus ?case using cnt_rev[of x ys] by auto next case (Cons y xs) thus ?case proof (cases "x = y") case True thus ?thesis using remove_cycles_removes[of y xs "[y]"] cnt_rev[of y ys] by auto next case False thus ?thesis using Cons[of "y # ys"] by auto qed qed lemma start_remove_id[simp]: "x ∉ set xs ⟹ start_remove xs x ys = rev ys @ xs" by (induction xs arbitrary: ys) auto lemma start_remove_cnt_id: "x ≠ y ⟹ cnt y (start_remove xs x ys) ≤ cnt y ys + cnt y xs" proof (induction xs arbitrary: ys) case Nil thus ?case by (simp add: cnt_rev) next case (Cons z xs) thus ?case proof (cases "x = z", goal_cases) case 1 thus ?case using remove_cycles_cnt_id[of x y xs "[x]"] by (simp add: cnt_rev) next case 2 from this(1)[of "(z # ys)"] this(2,3) show ?case by auto qed qed fun remove_all_cycles :: "'a list ⇒ 'a list ⇒ 'a list" where "remove_all_cycles [] xs = xs" | "remove_all_cycles (x # xs) ys = remove_all_cycles xs (start_remove ys x [])" lemma cnt_remove_all_mono:"cnt y (remove_all_cycles xs ys) ≤ max 1 (cnt y ys)" proof (induction xs arbitrary: ys) case Nil thus ?case by auto next case (Cons x xs) thus ?case proof (cases "x = y") case True thus ?thesis using start_remove_removes[of y ys "[]"] Cons[of "start_remove ys y []"] by auto next case False hence "cnt y (start_remove ys x []) ≤ cnt y ys" using start_remove_cnt_id[of x y ys "[]"] by auto thus ?thesis using Cons[of "start_remove ys x []"] by auto qed qed lemma cnt_remove_all_cycles: "x ∈ set xs ⟹ cnt x (remove_all_cycles xs ys) ≤ 1" proof (induction xs arbitrary: ys) case Nil thus ?case by auto next case (Cons y xs) thus ?case using start_remove_removes[of x ys "[]"] cnt_remove_all_mono[of y xs "start_remove ys y []"] by auto qed lemma cnt_mono: "cnt a (b # xs) ≤ cnt a (b # c # xs)" by (induction xs) auto lemma cnt_distinct_intro: "∀ x ∈ set xs. cnt x xs ≤ 1 ⟹ distinct xs" proof (induction xs) case Nil thus ?case by auto next case (Cons x xs) from this(2) have "∀ x ∈ set xs. cnt x xs ≤ 1" by (metis filter.simps(2) impossible_Cons linorder_class.linear list.set_intros(2) preorder_class.order_trans) with Cons.IH have "distinct xs" by auto moreover have "x ∉ set xs" using Cons.prems proof (induction xs) case Nil then show ?case by auto next case (Cons a xs) from this(2) have "∀xa∈set (x # xs). cnt xa (x # a # xs) ≤ 1" by auto then have *: "∀xa∈set (x # xs). cnt xa (x # xs) ≤ 1" proof (safe, goal_cases) case (1 b) then have "cnt b (x # a # xs) ≤ 1" by auto with cnt_mono[of b x xs a] show ?case by fastforce qed with Cons(1) have "x ∉ set xs" by auto moreover have "x ≠ a" by (metis (full_types) Cons.prems One_nat_def * empty_iff filter.simps(2) impossible_Cons le_0_eq le_Suc_eq length_0_conv list.set(1) list.set_intros(1)) ultimately show ?case by auto qed ultimately show ?case by auto qed lemma remove_cycles_subs: "set (remove_cycles xs x ys) ⊆ set xs ∪ set ys" by (induction xs arbitrary: ys; auto; fastforce) lemma start_remove_subs: "set (start_remove xs x ys) ⊆ set xs ∪ set ys" using remove_cycles_subs by (induction xs arbitrary: ys; auto; fastforce) lemma remove_all_cycles_subs: "set (remove_all_cycles xs ys) ⊆ set ys" using start_remove_subs by (induction xs arbitrary: ys, auto) (fastforce+) lemma remove_all_cycles_distinct: "set ys ⊆ set xs ⟹ distinct (remove_all_cycles xs ys)" proof - assume "set ys ⊆ set xs" hence "∀ x ∈ set ys. cnt x (remove_all_cycles xs ys) ≤ 1" using cnt_remove_all_cycles by fastforce hence "∀ x ∈ set (remove_all_cycles xs ys). cnt x (remove_all_cycles xs ys) ≤ 1" using remove_all_cycles_subs by fastforce thus "distinct (remove_all_cycles xs ys)" using cnt_distinct_intro by auto qed lemma distinct_remove_cycles_inv: "distinct (xs @ ys) ⟹ distinct (remove_cycles xs x ys)" proof (induction xs arbitrary: ys) case Nil thus ?case by auto next case (Cons y xs) thus ?case by auto qed definition "remove_all x xs = (if x ∈ set xs then tl (remove_cycles xs x []) else xs)" definition "remove_all_rev x xs = (if x ∈ set xs then rev (tl (remove_cycles (rev xs) x [])) else xs)" lemma remove_all_distinct: "distinct xs ⟹ distinct (x # remove_all x xs)" proof (cases "x ∈ set xs", goal_cases) case 1 from remove_cycles_begins_with[OF 1(2), of "[]"] obtain zs where "remove_cycles xs x [] = x # zs" "x ∉ set zs" by auto thus ?thesis using 1(1) distinct_remove_cycles_inv[of "xs" "[]" x] by (simp add: remove_all_def) next case 2 thus ?thesis by (simp add: remove_all_def) qed lemma remove_all_removes: "x ∉ set (remove_all x xs)" by (metis list.sel(3) remove_all_def remove_cycles_begins_with) lemma remove_all_subs: "set (remove_all x xs) ⊆ set xs" using remove_cycles_subs remove_all_def by (metis (no_types, lifting) append_Nil2 list.sel(2) list.set_sel(2) set_append subsetCE subsetI) lemma remove_all_rev_distinct: "distinct xs ⟹ distinct (x # remove_all_rev x xs)" proof (cases "x ∈ set xs", goal_cases) case 1 then have "x ∈ set (rev xs)" by auto from remove_cycles_begins_with[OF this, of "[]"] obtain zs where "remove_cycles (rev xs) x [] = x # zs" "x ∉ set zs" by auto thus ?thesis using 1(1) distinct_remove_cycles_inv[of "rev xs" "[]" x] by (simp add: remove_all_rev_def) next case 2 thus ?thesis by (simp add: remove_all_rev_def) qed lemma remove_all_rev_removes: "x ∉ set (remove_all_rev x xs)" by (metis remove_all_def remove_all_removes remove_all_rev_def set_rev) lemma remove_all_rev_subs: "set (remove_all_rev x xs) ⊆ set xs" by (metis remove_all_def remove_all_subs set_rev remove_all_rev_def) abbreviation "rem_cycles i j xs ≡ remove_all i (remove_all_rev j (remove_all_cycles xs xs))" lemma rem_cycles_distinct': "i ≠ j ⟹ distinct (i # j # rem_cycles i j xs)" proof - assume "i ≠ j" have "distinct (remove_all_cycles xs xs)" by (simp add: remove_all_cycles_distinct) from remove_all_rev_distinct[OF this] have "distinct (remove_all_rev j (remove_all_cycles xs xs))" by simp from remove_all_distinct[OF this] have "distinct (i # rem_cycles i j xs)" by simp moreover have "j ∉ set (rem_cycles i j xs)" using remove_all_subs remove_all_rev_removes remove_all_removes by fastforce ultimately show ?thesis by (simp add: ‹i ≠ j›) qed lemma rem_cycles_removes_last: "j ∉ set (rem_cycles i j xs)" by (meson remove_all_rev_removes remove_all_subs rev_subsetD) lemma rem_cycles_distinct: "distinct (rem_cycles i j xs)" by (meson distinct.simps(2) order_refl remove_all_cycles_distinct remove_all_distinct remove_all_rev_distinct) lemma rem_cycles_subs: "set (rem_cycles i j xs) ⊆ set xs" by (meson order_trans remove_all_cycles_subs remove_all_subs remove_all_rev_subs) section ‹Definition of the Algorithm› text ‹ We formalize the Floyd-Warshall algorithm on a linearly ordered abelian semigroup. However, we would not need an ‹abelian› monoid if we had the right type class. › class linordered_ab_monoid_add = linordered_ab_semigroup_add + fixes neutral :: 'a ("𝟭") assumes neutl[simp]: "𝟭 + x = x" assumes neutr[simp]: "x + 𝟭 = x" begin lemmas assoc = add.assoc type_synonym 'c mat = "nat ⇒ nat ⇒ 'c" definition (in -) upd :: "'c mat ⇒ nat ⇒ nat ⇒ 'c ⇒ 'c mat" where "upd m x y v = m (x := (m x) (y := v))" definition fw_upd :: "'a mat ⇒ nat ⇒ nat ⇒ nat ⇒ 'a mat" where "fw_upd m k i j ≡ upd m i j (min (m i j) (m i k + m k j))" lemma fw_upd_mono: "fw_upd m k i j i' j' ≤ m i' j'" by (cases "i = i'", cases "j = j'") (auto simp: fw_upd_def upd_def) fun fw :: "'a mat ⇒ nat ⇒ nat ⇒ nat ⇒ nat ⇒ 'a mat" where "fw m n 0 0 0 = fw_upd m 0 0 0" | "fw m n (Suc k) 0 0 = fw_upd (fw m n k n n) (Suc k) 0 0" | "fw m n k (Suc i) 0 = fw_upd (fw m n k i n) k (Suc i) 0" | "fw m n k i (Suc j) = fw_upd (fw m n k i j) k i (Suc j)" lemma fw_invariant_aux_1: "j'' ≤ j ⟹ i ≤ n ⟹ j ≤ n ⟹ k ≤ n ⟹ fw m n k i j i' j' ≤ fw m n k i j'' i' j'" proof (induction j) case 0 thus ?case by simp next case (Suc j) thus ?case proof (cases "j'' = Suc j") case True thus ?thesis by simp next case False have "fw_upd (fw m n k i j) k i (Suc j) i' j' ≤ fw m n k i j i' j'" by (simp add: fw_upd_mono) thus ?thesis using Suc False by simp qed qed lemma fw_invariant_aux_2: "i ≤ n ⟹ j ≤ n ⟹ k ≤ n ⟹ i'' ≤ i ⟹ j'' ≤ j ⟹ fw m n k i j i' j' ≤ fw m n k i'' j'' i' j'" proof (induction i) case 0 thus ?case using fw_invariant_aux_1 by auto next case (Suc i) thus ?case proof (cases "i'' = Suc i") case True thus ?thesis using Suc fw_invariant_aux_1 by simp next case False have "fw m n k (Suc i) j i' j' ≤ fw m n k (Suc i) 0 i' j'" using fw_invariant_aux_1[of 0 j "Suc i" n k] Suc(2-) by simp also have "… ≤ fw m n k i n i' j'" by (simp add: fw_upd_mono) also have "… ≤ fw m n k i j i' j'" using fw_invariant_aux_1[of j n i n k] False Suc by simp also have "… ≤ fw m n k i'' j'' i' j'" using Suc False by simp finally show ?thesis by simp qed qed lemma fw_invariant: "k' ≤ k ⟹ i ≤ n ⟹ j ≤ n ⟹ k ≤ n ⟹ j'' ≤ j ⟹ i'' ≤ i ⟹ fw m n k i j i' j' ≤ fw m n k' i'' j'' i' j'" proof (induction k) case 0 thus ?case using fw_invariant_aux_2 by auto next case (Suc k) thus ?case proof (cases "k' = Suc k") case True thus ?thesis using Suc fw_invariant_aux_2 by simp next case False have "fw m n (Suc k) i j i' j' ≤ fw m n (Suc k) 0 0 i' j'" using fw_invariant_aux_2[of i n j "Suc k" 0 0] Suc(2-) by simp also have "… ≤ fw m n k n n i' j'" by (simp add: fw_upd_mono) also have "… ≤ fw m n k i j i' j'" using fw_invariant_aux_2[of n n n k] False Suc by simp also have "… ≤ fw m n k' i'' j'' i' j'" using Suc False by simp finally show ?thesis by simp qed qed lemma single_row_inv: "j' < j ⟹ j ≤ n ⟹ i' ≤ n ⟹ fw m n k i' j i' j' = fw m n k i' j' i' j'" proof (induction j) case 0 thus ?case by simp next case (Suc j) thus ?case by (cases "j' = j") (simp add: fw_upd_def upd_def)+ qed lemma single_iteration_inv': "i' < i ⟹ j' ≤ n ⟹ j ≤ n ⟹ i ≤ n ⟹ fw m n k i j i' j' = fw m n k i' j' i' j'" proof (induction i arbitrary: j) case 0 thus ?case by simp next case (Suc i) thus ?case proof (induction j) case 0 thus ?case proof (cases "i = i'", goal_cases) case 2 thus ?case by (simp add: fw_upd_def upd_def) next case 1 thus ?case using single_row_inv[of j' n n i' m k] by (cases "j' = n") (fastforce simp add: fw_upd_def upd_def)+ qed next case (Suc j) thus ?case by (simp add: fw_upd_def upd_def) qed qed lemma single_iteration_inv: "i' ≤ i ⟹ j' ≤ j ⟹ i ≤ n ⟹ j ≤ n⟹ fw m n k i j i' j' = fw m n k i' j' i' j'" proof (induction i arbitrary: j) case 0 thus ?case proof (induction j) case 0 thus ?case by simp next case (Suc j) thus ?case using 0 by (cases "j' = Suc j") (simp add: fw_upd_def upd_def)+ qed next case (Suc i) thus ?case proof (induction j) case 0 thus ?case by (cases "i' = Suc i") (simp add: fw_upd_def upd_def)+ next case (Suc j) thus ?case proof (cases "i' = Suc i", goal_cases) case 1 thus ?case proof (cases "j' = Suc j", goal_cases) case 1 thus ?case by simp next case 2 thus ?case by (simp add: fw_upd_def upd_def) qed next case 2 thus ?case proof (cases "j' = Suc j", goal_cases) case 1 thus ?case using single_iteration_inv'[of i' "Suc i" j' n "Suc j" m k] by simp next case 2 thus ?case by (simp add: fw_upd_def upd_def) qed qed qed qed lemma fw_innermost_id: "i ≤ n ⟹ j ≤ n ⟹ j' ≤ n ⟹ i' < i ⟹ fw m n 0 i' j' i j = m i j" proof (induction i' arbitrary: j') case 0 thus ?case proof (induction j') case 0 thus ?case by (simp add: fw_upd_def upd_def) next case (Suc j') thus ?case by (auto simp: fw_upd_def upd_def) qed next case (Suc i') thus ?case proof (induction j') case 0 thus ?case by (auto simp add: fw_upd_def upd_def) next case (Suc j') thus ?case by (auto simp add: fw_upd_def upd_def) qed qed lemma fw_middle_id: "i ≤ n ⟹ j ≤ n ⟹ j' < j ⟹ i' ≤ i ⟹ fw m n 0 i' j' i j = m i j" proof (induction i' arbitrary: j') case 0 thus ?case proof (induction j') case 0 thus ?case by (simp add: fw_upd_def upd_def) next case (Suc j') thus ?case by (auto simp: fw_upd_def upd_def) qed next case (Suc i') thus ?case proof (induction j') case 0 thus ?case using fw_innermost_id by (auto simp add: fw_upd_def upd_def) next case (Suc j') thus ?case by (auto simp add: fw_upd_def upd_def) qed qed lemma fw_outermost_mono: "i ≤ n ⟹ j ≤ n ⟹ fw m n 0 i j i j ≤ m i j" proof (cases j) case 0 assume "i ≤ n" thus ?thesis proof (cases i) case 0 thus ?thesis using ‹j = 0› by (simp add: fw_upd_def upd_def) next case (Suc i') hence "fw m n 0 i' n (Suc i') 0 = m (Suc i') 0" using fw_innermost_id[of "Suc i'" n 0 n i' m] using ‹i ≤ n› by simp thus ?thesis using ‹j = 0› Suc by (simp add: fw_upd_def upd_def) qed next case (Suc j') assume "i ≤ n" "j ≤ n" hence "fw m n 0 i j' i (Suc j') = m i (Suc j')" using fw_middle_id[of i n "Suc j'" j' i m] Suc by simp thus ?thesis using Suc by (simp add: fw_upd_def upd_def) qed lemma Suc_innermost_id1: "i ≤ n ⟹ j ≤ n ⟹ j' ≤ n ⟹ i' < i ⟹ fw m n (Suc k) i' j' i j = fw m n k i j i j" proof (induction i' arbitrary: j') case 0 thus ?case proof (induction j') case 0 hence "fw m n k n n i j = fw m n k i j i j" using single_iteration_inv[of i n j n n m k] by simp thus ?case using 0 by (simp add: fw_upd_def upd_def) next case (Suc j') thus ?case by (auto simp: fw_upd_def upd_def) qed next case (Suc i') thus ?case proof (induction j') case 0 thus ?case by (auto simp add: fw_upd_def upd_def) next case (Suc j') thus ?case by (auto simp add: fw_upd_def upd_def) qed qed lemma Suc_innermost_id2: "i ≤ n ⟹ j ≤ n ⟹ j' < j ⟹ i' ≤ i ⟹ fw m n (Suc k) i' j' i j = fw m n k i j i j" proof (induction i' arbitrary: j') case 0 hence "fw m n k n n i j = fw m n k i j i j" using single_iteration_inv[of i n j n n m k] by simp with 0 show ?case proof (induction j') case 0 thus ?case by (auto simp add: fw_upd_def upd_def) next case (Suc j') thus ?case by (auto simp: fw_upd_def upd_def) qed next case (Suc i') thus ?case proof (induction j') case 0 thus ?case using Suc_innermost_id1 by (auto simp add: fw_upd_def upd_def) next case (Suc j') thus ?case by (auto simp add: fw_upd_def upd_def) qed qed lemma Suc_innermost_id1': "i ≤ n ⟹ j ≤ n ⟹ j' ≤ n ⟹ i' < i ⟹ fw m n (Suc k) i' j' i j = fw m n k n n i j" proof goal_cases case 1 hence "fw m n (Suc k) i' j' i j = fw m n k i j i j" using Suc_innermost_id1 by simp thus ?thesis using 1 single_iteration_inv[of i n] by simp qed lemma Suc_innermost_id2': "i ≤ n ⟹ j ≤ n ⟹ j' < j ⟹ i' ≤ i ⟹ fw m n (Suc k) i' j' i j = fw m n k n n i j" proof goal_cases case 1 hence "fw m n (Suc k) i' j' i j = fw m n k i j i j" using Suc_innermost_id2 by simp thus ?thesis using 1 single_iteration_inv[of i n] by simp qed lemma Suc_innermost_mono: "i ≤ n ⟹ j ≤ n ⟹ fw m n (Suc k) i j i j ≤ fw m n k i j i j" proof (cases j) case 0 assume "i ≤ n" thus ?thesis proof (cases i) case 0 thus ?thesis using ‹j = 0› single_iteration_inv[of 0 n 0 n n m k] by (simp add: fw_upd_def upd_def) next case (Suc i') thus ?thesis using Suc_innermost_id1 ‹i ≤ n› ‹j = 0› by (auto simp: fw_upd_def upd_def local.min.coboundedI1) qed next case (Suc j') assume "i ≤ n" "j ≤ n" thus ?thesis using Suc Suc_innermost_id2 by (auto simp: fw_upd_def upd_def local.min.coboundedI1) qed lemma fw_mono': "i ≤ n ⟹ j ≤ n ⟹ fw m n k i j i j ≤ m i j" proof (induction k) case 0 thus ?case using fw_outermost_mono by simp next case (Suc k) thus ?case using Suc_innermost_mono[OF Suc.prems, of m k] by simp qed lemma fw_mono: "i ≤ n ⟹ j ≤ n ⟹ i' ≤ n ⟹ j' ≤ n ⟹ fw m n k i j i' j' ≤ m i' j'" proof (cases k) case 0 assume 0: "i ≤ n" "j ≤ n" "i' ≤ n" "j' ≤ n" "k = 0" thus ?thesis proof (cases "i' ≤ i") case False thus ?thesis using 0 fw_innermost_id by simp next case True thus ?thesis proof (cases "j' ≤ j") case True have "fw m n 0 i j i' j' ≤ fw m n 0 i' j' i' j'" using fw_invariant True ‹i' ≤ i› 0 by simp also have "fw m n 0 i' j' i' j' ≤ m i' j'" using 0 fw_outermost_mono by blast finally show ?thesis by (simp add: ‹k = 0›) next case False thus ?thesis proof (cases "i = i'", goal_cases) case 1 then show ?thesis using fw_middle_id[of i' n j' j i' m] 0 by simp next case 2 then show ?case using single_iteration_inv'[of i' i j' n j m 0] ‹i' ≤ i› fw_middle_id[of i' n j' j i' m] fw_outermost_mono[of i' n j' m] 0 by simp qed qed qed next case (Suc k) assume prems: "i ≤ n" "j ≤ n" "i' ≤ n" "j' ≤ n" thus ?thesis proof (cases "i' ≤ i ∧ j' ≤ j") case True hence "fw m n (Suc k) i j i' j' = fw m n (Suc k) i' j' i' j'" using prems single_iteration_inv by blast thus ?thesis using Suc prems fw_mono' by auto next case False thus ?thesis proof auto assume "¬ i' ≤ i" thus ?thesis using Suc prems fw_mono' Suc_innermost_id1 by auto next assume "¬ j' ≤ j" hence "j < j'" by simp show ?thesis proof (cases "i ≤ i'") case True thus ?thesis using Suc prems Suc_innermost_id2 ‹j < j'› fw_mono' by auto next case False thus ?thesis using single_iteration_inv' Suc prems fw_mono' by auto qed qed qed qed lemma add_mono_neutr: assumes "𝟭 ≤ b" shows "a ≤ a + b" using neutr add_mono assms by force lemma add_mono_neutl: assumes "𝟭 ≤ b" shows "a ≤ b + a" using neutr add_mono assms by force lemma fw_step_0: "m 0 0 ≥ 𝟭 ⟹ i ≤ n ⟹ j ≤ n ⟹ fw m n 0 i j i j = min (m i j) (m i 0 + m 0 j)" proof (induction i) case 0 thus ?case proof (cases j) case 0 thus ?thesis by (simp add: fw_upd_def upd_def) next case (Suc j) hence "fw m n 0 0 j 0 (Suc j) = m 0 (Suc j)" using 0 fw_middle_id[of 0 n "Suc j" j 0 m] by fast moreover have "fw m n 0 0 j 0 0 = m 0 0" using single_iteration_inv[of 0 0 0 j n m 0] Suc 0 by (auto simp add: fw_upd_def upd_def min_def intro: add_mono_neutl) ultimately show ?thesis using Suc by (simp add: fw_upd_def upd_def) qed next case (Suc i) note A = this show ?case proof (cases j) case 0 have "fw m n 0 i n (Suc i) 0 = m (Suc i) 0" using fw_innermost_id[of "Suc i" n 0 n i m] Suc by simp moreover have "fw m n 0 i n 0 0 = m 0 0" using Suc single_iteration_inv[of 0 i 0 n n m 0] by (auto simp add: fw_upd_def upd_def min_def intro: add_mono_neutl) ultimately show ?thesis using 0 by (simp add: fw_upd_def upd_def) next case (Suc j) have *: "fw m n 0 0 j 0 0 = m 0 0" using single_iteration_inv[ of 0 0 0 j n m 0] A Suc by (auto simp add: fw_upd_def upd_def min_def intro: add_mono_neutl) have **: "fw m n 0 i n 0 0 = m 0 0" using single_iteration_inv[of 0 i 0 n n m 0] A by (auto simp add: fw_upd_def upd_def min_def intro: add_mono_neutl) have "m 0 (Suc j) = fw_upd m 0 0 (Suc j) 0 (Suc j)" using ‹m 0 0 >= 𝟭› by (auto simp add: fw_upd_def upd_def min_def intro: add_mono_neutl) also have "… = fw m n 0 0 (Suc j) 0 (Suc j)" using fw_middle_id[of 0 n "Suc j" j 0 m] Suc A(4) by (simp add: fw_upd_def upd_def *) finally have ***: "fw m n 0 (Suc i) j 0 (Suc j) = m 0 (Suc j)" using single_iteration_inv'[of 0 "Suc i" "Suc j" n j m 0] A Suc by simp have "m (Suc i) 0 = fw_upd m 0 (Suc i) 0 (Suc i) 0" using ‹m 0 0 >= 𝟭› by (auto simp add: fw_upd_def upd_def min_def intro: add_mono_neutr) also have "… = fw m n 0 (Suc i) 0 (Suc i) 0" using fw_innermost_id[of "Suc i" n 0 n i m] ‹Suc i ≤ n› ** by (simp add: fw_upd_def upd_def) finally have "fw m n 0 (Suc i) j (Suc i) 0 = m (Suc i) 0" using single_iteration_inv A Suc by auto moreover have "fw m n 0 (Suc i) j (Suc i) (Suc j) = m (Suc i) (Suc j)" using fw_middle_id A Suc by simp ultimately show ?thesis using Suc *** by (simp add: fw_upd_def upd_def) qed qed lemma fw_step_Suc: "∀ k'≤n. fw m n k n n k' k' ≥ 𝟭 ⟹ i ≤ n ⟹ j ≤ n ⟹ Suc k ≤ n ⟹ fw m n (Suc k) i j i j = min (fw m n k n n i j) (fw m n k n n i (Suc k) + fw m n k n n (Suc k) j)" proof (induction i) case 0 thus ?case proof (cases j) case 0 thus ?thesis by (simp add: fw_upd_def upd_def) next case (Suc j) then have "fw m n k n n 0 (Suc j) = fw m n (Suc k) 0 j 0 (Suc j)" using 0(2-) Suc_innermost_id2' by simp moreover have "fw m n (Suc k) 0 j 0 (Suc k) = fw m n k n n 0 (Suc k)" proof (cases "j < Suc k") case True thus ?thesis using 0 Suc_innermost_id2' by simp next case False hence "fw m n (Suc k) 0 k 0 (Suc k) = fw m n k n n 0 (Suc k)" using 0(2-) Suc Suc_innermost_id2' by simp moreover have "fw m n (Suc k) 0 k (Suc k) (Suc k) = fw m n k n n (Suc k) (Suc k)" using 0(2-) Suc Suc_innermost_id2' by simp moreover have "fw m n (Suc k) 0 j 0 (Suc k) = fw m n (Suc k) 0 (Suc k) 0 (Suc k)" using False single_iteration_inv 0(2-) Suc by force ultimately show ?thesis using 0(1) by (auto simp add: fw_upd_def upd_def ‹Suc k ≤ n› min_def intro: add_mono_neutr) qed moreover have "fw m n k n n (Suc k) (Suc j) = fw m n (Suc k) 0 j (Suc k) (Suc j)" using 0(2-) Suc Suc_innermost_id2' by simp ultimately show ?thesis using Suc by (simp add: fw_upd_def upd_def) qed next case (Suc i) note A = this show ?case proof (cases j) case 0 hence "fw m n (Suc k) i n (Suc i) 0 = fw m n k n n (Suc i) 0" using Suc_innermost_id1' ‹Suc i ≤ n› by simp moreover have "fw m n (Suc k) i n (Suc i) (Suc k) = fw m n k n n (Suc i) (Suc k)" using Suc_innermost_id1' A(3,5) by simp moreover have "fw m n (Suc k) i n (Suc k) 0 = fw m n k n n (Suc k) 0" proof (cases "i < Suc k") case True thus ?thesis using Suc_innermost_id1' A(3,5) by simp next case False have "fw m n (Suc k) k n (Suc k) (Suc k) = fw m n k n n (Suc k) (Suc k)" using Suc_innermost_id1' ‹Suc i ≤ n› False by simp moreover have "fw m n (Suc k) k n (Suc k) 0 = fw m n k n n (Suc k) 0" using Suc_innermost_id1' ‹Suc i ≤ n› False by simp moreover have "fw m n (Suc k) i n (Suc k) 0 = fw m n (Suc k) (Suc k) 0 (Suc k) 0" using single_iteration_inv ‹Suc i ≤ n› False by simp ultimately show ?thesis using Suc(2) by (auto simp add: fw_upd_def upd_def ‹Suc k ≤ n› min_def intro: add_mono_neutl) qed ultimately show ?thesis using 0 by (simp add: fw_upd_def upd_def) next case (Suc j) hence "fw m n (Suc k) (Suc i) j (Suc i) (Suc j) = fw m n k n n (Suc i) (Suc j)" using Suc_innermost_id2' A(3,4) by simp moreover have "fw m n (Suc k) (Suc i) j (Suc i) (Suc k) = fw m n k n n (Suc i) (Suc k)" proof (cases "j < Suc k") case True thus ?thesis using Suc A(3-) Suc_innermost_id2' by simp next case False have *:"fw m n (Suc k) (Suc i) k (Suc i) (Suc k) = fw m n k n n (Suc i) (Suc k)" using Suc_innermost_id2' A(3,5) by simp have **:"fw m n (Suc k) (Suc i) k (Suc k) (Suc k) = fw m n k n n (Suc k) (Suc k)" proof (cases "Suc i ≤ Suc k") case True thus ?thesis using Suc_innermost_id2' A(5) by simp next case False hence "fw m n (Suc k) (Suc i) k (Suc k) (Suc k) = fw m n (Suc k) (Suc k) (Suc k) (Suc k) (Suc k)" using single_iteration_inv'[of "Suc k" "Suc i" "Suc k" n k m "Suc k"] A(3) by simp moreover have "fw m n (Suc k) (Suc k) k (Suc k) (Suc k) = fw m n k n n (Suc k) (Suc k)" using Suc_innermost_id2' A(5) by simp ultimately show ?thesis using A(2) by (auto simp add: fw_upd_def upd_def ‹Suc k ≤ n› min_def intro: add_mono_neutl) qed have "fw m n (Suc k) (Suc i) j (Suc i) (Suc k) = fw m n (Suc k) (Suc i) (Suc k) (Suc i) (Suc k)" using False single_iteration_inv[of "Suc i" "Suc i" "Suc k" j n m "Suc k"] A(3-) Suc by simp also have "… = fw m n k n n (Suc i) (Suc k)" using * ** A(2) by (auto simp add: fw_upd_def upd_def ‹Suc k ≤ n› min_def intro: add_mono_neutr) finally show ?thesis by simp qed moreover have "fw m n (Suc k) (Suc i) j (Suc k) (Suc j) = fw m n k n n (Suc k) (Suc j)" proof (cases "Suc i ≤ Suc k") case True thus ?thesis using Suc_innermost_id2' Suc A(3-5) by simp next case False have "fw m n (Suc k) (Suc k) j (Suc k) (Suc k) = fw m n k n n (Suc k) (Suc k)" proof (cases "j < Suc k") case True thus ?thesis using Suc_innermost_id2' A(5) by simp next case False hence "fw m n (Suc k) (Suc k) j (Suc k) (Suc k) = fw m n (Suc k) (Suc k) (Suc k) (Suc k) (Suc k)" using single_iteration_inv A(3,4) Suc by simp moreover have "fw m n (Suc k) (Suc k) k (Suc k) (Suc k) = fw m n k n n (Suc k) (Suc k)" using Suc_innermost_id2' A(5) by simp ultimately show ?thesis using A(2) by (auto simp add: fw_upd_def upd_def ‹Suc k ≤ n› min_def intro: add_mono_neutl) qed moreover have "fw m n (Suc k) (Suc k) j (Suc k) (Suc j) = fw m n k n n (Suc k) (Suc j)" using Suc_innermost_id2' Suc A(3-5) by simp ultimately have "fw m n (Suc k) (Suc k) (Suc j) (Suc k) (Suc j) = fw m n k n n (Suc k) (Suc j)" using A(2) by (auto simp add: fw_upd_def upd_def ‹Suc k ≤ n› min_def intro: add_mono_neutl) moreover have "fw m n (Suc k) (Suc i) j (Suc k) (Suc j) = fw m n (Suc k) (Suc k) (Suc j) (Suc k) (Suc j)" using single_iteration_inv'[of "Suc k" "Suc i" "Suc j" n j m "Suc k"] Suc A(3-) False by simp moreover have "fw m n (Suc k) (Suc k) k (Suc k) (Suc k) = fw m n k n n (Suc k) (Suc k)" using Suc_innermost_id2' A(5) by simp ultimately show ?thesis using A(2) by (simp add: fw_upd_def upd_def) qed ultimately show ?thesis using Suc by (simp add: fw_upd_def upd_def) qed qed subsection ‹Length of Paths› fun len :: "'a mat ⇒ nat ⇒ nat ⇒ nat list ⇒ 'a" where "len m u v [] = m u v" | "len m u v (w#ws) = m u w + len m w v ws" lemma len_decomp: "xs = ys @ y # zs ⟹ len m x z xs = len m x y ys + len m y z zs" by (induction ys arbitrary: x xs) (simp add: assoc)+ lemma len_comp: "len m a c (xs @ b # ys) = len m a b xs + len m b c ys" by (induction xs arbitrary: a) (auto simp: assoc) subsection ‹Shortening Negative Cycles› lemma remove_cycles_neg_cycles_aux: fixes i xs ys defines "xs' ≡ i # ys" assumes "i ∉ set ys" assumes "i ∈ set xs" assumes "xs = as @ concat (map ((#) i) xss) @ xs'" assumes "len m i j ys > len m i j xs" shows "∃ ys. set ys ⊆ set xs ∧ len m i i ys < 𝟭" using assms proof (induction xss arbitrary: xs as) case Nil with Nil show ?case proof (cases "len m i i as ≥ 𝟭", goal_cases) case 1 from this(4,6) len_decomp[of xs as i ys m i j] have "len m i j xs = len m i i as + len m i j ys" by simp with 1(11) have "len m i j ys ≤ len m i j xs" using add_mono by fastforce thus ?thesis using Nil(5) by auto next case 2 thus ?case by auto qed next case (Cons zs xss) let ?xs = "zs @ concat (map ((#) i) xss) @ xs'" from Cons show ?case proof (cases "len m i i as ≥ 𝟭", goal_cases) case 1 from this(5,7) len_decomp add_mono have "len m i j ?xs ≤ len m i j xs" by fastforce hence 4:"len m i j ?xs < len m i j ys" using 1(6) by simp have 2:"i ∈ set ?xs" using Cons(2) by auto have "set ?xs ⊆ set xs" using Cons(5) by auto moreover from Cons(1)[OF 1(2,3) 2 _ 4] have "∃ys. set ys ⊆ set ?xs ∧ len m i i ys < 𝟭" by auto ultimately show ?case by blast next case 2 from this(5,7) show ?case by auto qed qed lemma add_lt_neutral: "a + b < b ⟹ a < 𝟭" proof (rule ccontr) assume "a + b < b" "¬ a < 𝟭" hence "a ≥ 𝟭" by auto from add_mono[OF this, of b b] ‹a + b < b› show False by auto qed lemma remove_cycles_neg_cycles_aux': fixes j xs ys assumes "j ∉ set ys" assumes "j ∈ set xs" assumes "xs = ys @ j # concat (map (λ xs. xs @ [j]) xss) @ as" assumes "len m i j ys > len m i j xs" shows "∃ ys. set ys ⊆ set xs ∧ len m j j ys < 𝟭" using assms proof (induction xss arbitrary: xs as) case Nil show ?case proof (cases "len m j j as ≥ 𝟭") case True from Nil(3) len_decomp[of xs ys j as m i j] have "len m i j xs = len m i j ys + len m j j as" by simp with True have "len m i j ys ≤ len m i j xs" using add_mono by fastforce with Nil show ?thesis by auto next case False with Nil show ?thesis by auto qed next case (Cons zs xss) let ?xs = "ys @ j # concat (map (λxs. xs @ [j]) xss) @ as" let ?t = "concat (map (λxs. xs @ [j]) xss) @ as" show ?case proof (cases "len m i j ?xs ≤ len m i j xs") case True hence 4:"len m i j ?xs < len m i j ys" using Cons(5) by simp have 2:"j ∈ set ?xs" using Cons(2) by auto have "set ?xs ⊆ set xs" using Cons(4) by auto moreover from Cons(1)[OF Cons(2) 2 _ 4] have "∃ys. set ys ⊆ set ?xs ∧ len m j j ys < 𝟭" by blast ultimately show ?thesis by blast next case False hence "len m i j xs < len m i j ?xs" by auto from this len_decomp Cons(4) add_mono have "len m j j (concat (map (λxs. xs @ [j]) (zs # xss)) @ as) < len m j j ?t" using False local.leI by fastforce hence "len m j j (zs @ j # ?t) < len m j j ?t" by simp with len_decomp[of "zs @ j # ?t" zs j ?t m j j] have "len m j j zs + len m j j ?t < len m j j ?t" by auto hence "len m j j zs < 𝟭" using add_lt_neutral by auto thus ?thesis using Cons.prems(3) by auto qed qed lemma add_le_impl: "a + b < a + c ⟹ b < c" proof (rule ccontr) assume "a + b < a + c" "¬ b < c" hence "b ≥ c" by auto from add_mono[OF _ this, of a a] ‹a + b < a + c› show False by auto qed lemma start_remove_neg_cycles: "len m i j (start_remove xs k []) > len m i j xs ⟹ ∃ ys. set ys ⊆ set xs ∧ len m k k ys < 𝟭" proof- let ?xs = "start_remove xs k []" assume len_lt:"len m i j ?xs > len m i j xs" hence "k ∈ set xs" using start_remove_id by fastforce from start_remove_decomp[OF this, of "[]"] obtain as bs where as_bs: "xs = as @ k # bs" "?xs = as @ remove_cycles bs k [k]" by fastforce let ?xs' = "remove_cycles bs k [k]" have "k ∈ set bs" using as_bs len_lt remove_cycles_id by fastforce then obtain ys where ys: "?xs = as @ k # ys" "?xs' = k # ys" "k ∉ set ys" using as_bs(2) remove_cycles_begins_with[OF ‹k ∈ set bs›] by auto have len_lt': "len m k j bs < len m k j ys" using len_decomp[OF as_bs(1), of m i j] len_decomp[OF ys(1), of m i j] len_lt add_le_impl by metis from remove_cycles_cycles[OF ‹k ∈ set bs›] obtain xss as' where "as' @ concat (map ((#) k) xss) @ ?xs' = bs" by fastforce hence "as' @ concat (map ((#) k) xss) @ k # ys = bs" using ys(2) by simp from remove_cycles_neg_cycles_aux[OF ‹k ∉ set ys› ‹k ∈ set bs› this[symmetric] len_lt'] show ?thesis using as_bs(1) by auto qed lemma remove_all_cycles_neg_cycles: "len m i j (remove_all_cycles ys xs) > len m i j xs ⟹ ∃ ys k. set ys ⊆ set xs ∧ k ∈ set xs ∧ len m k k ys < 𝟭" proof (induction ys arbitrary: xs) case Nil thus ?case by auto next case (Cons y ys) let ?xs = "start_remove xs y []" show ?case proof (cases "len m i j xs < len m i j ?xs") case True with start_remove_id have "y ∈ set xs" by fastforce with start_remove_neg_cycles[OF True] show ?thesis by blast next case False with Cons(2) have "len m i j ?xs < len m i j (remove_all_cycles (y # ys) xs)" by auto hence "len m i j ?xs < len m i j (remove_all_cycles ys ?xs)" by auto from Cons(1)[OF this] show ?thesis using start_remove_subs[of xs y "[]"] by auto qed qed lemma (in -) concat_map_cons_rev: "rev (concat (map ((#) j) xss)) = concat (map (λ xs. xs @ [j]) (rev (map rev xss)))" by (induction xss) auto lemma negative_cycle_dest: "len m i j (rem_cycles i j xs) > len m i j xs ⟹ ∃ i' ys. len m i' i' ys < 𝟭 ∧ set ys ⊆ set xs ∧ i' ∈ set (i # j # xs)" proof - let ?xsij = "rem_cycles i j xs" let ?xsj = "remove_all_rev j (remove_all_cycles xs xs)" let ?xs = "remove_all_cycles xs xs" assume len_lt: "len m i j ?xsij > len m i j xs" show ?thesis proof (cases "len m i j ?xsij ≤ len m i j ?xsj") case True hence len_lt: "len m i j ?xsj > len m i j xs" using len_lt by simp show ?thesis proof (cases "len m i j ?xsj ≤ len m i j ?xs") case True hence "len m i j ?xs > len m i j xs" using len_lt by simp with remove_all_cycles_neg_cycles[OF this] show ?thesis by auto next case False then have len_lt': "len m i j ?xsj > len m i j ?xs" by simp show ?thesis proof (cases "j ∈ set ?xs") case False thus ?thesis using len_lt' by (simp add: remove_all_rev_def) next case True from remove_all_rev_removes[of j] have 1: "j ∉ set ?xsj" by simp from True have "j ∈ set (rev ?xs)" by auto from remove_cycles_cycles[OF this] obtain xss as where as: "as @ concat (map ((#) j) xss) @ remove_cycles (rev ?xs) j [] = rev ?xs" "j ∉ set as" by blast from True have "?xsj = rev (tl (remove_cycles (rev ?xs) j []))" by (simp add: remove_all_rev_def) with remove_cycles_begins_with[OF ‹j ∈ set (rev ?xs)›, of "[]"] have "remove_cycles (rev ?xs) j [] = j # rev ?xsj" "j ∉ set ?xsj" by auto with as(1) have xss: "as @ concat (map ((#) j) xss) @ j # rev ?xsj = rev ?xs" by simp hence "rev (as @ concat (map ((#) j) xss) @ j # rev ?xsj) = ?xs" by simp hence "?xsj @ j # rev (concat (map ((#) j) xss)) @ rev as = ?xs" by simp hence "?xsj @ j # concat (map (λ xs. xs @ [j]) (rev (map rev xss))) @ rev as = ?xs" by (simp add: concat_map_cons_rev) from remove_cycles_neg_cycles_aux'[OF 1 True this[symmetric] len_lt'] show ?thesis using remove_all_cycles_subs by fastforce qed qed next case False hence len_lt': "len m i j ?xsij > len m i j ?xsj" by simp show ?thesis proof (cases "i ∈ set ?xsj") case False thus ?thesis using len_lt' by (simp add: remove_all_def) next case True from remove_all_removes[of i] have 1: "i ∉ set ?xsij" by (simp add: remove_all_def) from remove_cycles_cycles[OF True] obtain xss as where as: "as @ concat (map ((#) i) xss) @ remove_cycles ?xsj i [] = ?xsj" "i ∉ set as" by blast from True have "?xsij = tl (remove_cycles ?xsj i [])" by (simp add: remove_all_def) with remove_cycles_begins_with[OF True, of "[]"] have "remove_cycles ?xsj i [] = i # ?xsij" "i ∉ set ?xsij" by auto with as(1) have xss: "as @ concat (map ((#) i) xss) @ i # ?xsij = ?xsj" by simp from remove_cycles_neg_cycles_aux[OF 1 True this[symmetric] len_lt'] show ?thesis using remove_all_rev_subs remove_all_cycles_subs by fastforce qed qed qed section ‹Definition of Shortest Paths› definition D :: "'a mat ⇒ nat ⇒ nat ⇒ nat ⇒ 'a" where "D m i j k ≡ Min {len m i j xs | xs. set xs ⊆ {0..k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}" lemma (in -) distinct_length_le:"finite s ⟹ set xs ⊆ s ⟹ distinct xs ⟹ length xs ≤ card s" by (metis card_mono distinct_card) lemma D_base_finite: "finite {len m i j xs | xs. set xs ⊆ {0..k} ∧ distinct xs}" using finite_subset_distinct finite_image_set by blast lemma D_base_finite': "finite {len m i j xs | xs. set xs ⊆ {0..k} ∧ distinct (i # j # xs)}" proof - have "{len m i j xs | xs. set xs ⊆ {0..k} ∧ distinct (i # j # xs)} ⊆ {len m i j xs | xs. set xs ⊆ {0..k} ∧ distinct xs}" by auto with D_base_finite[of m i j k] show ?thesis by (rule rev_finite_subset) qed lemma D_base_finite'': "finite {len m i j xs |xs. set xs ⊆ {0..k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}" using D_base_finite[of m i j k] by - (rule finite_subset, auto) definition cycle_free :: "'a mat ⇒ nat ⇒ bool" where "cycle_free m n ≡ ∀ i xs. i ≤ n ∧ set xs ⊆ {0..n} ⟶ (∀ j. j ≤ n ⟶ len m i j (rem_cycles i j xs) ≤ len m i j xs) ∧ len m i i xs ≥ 𝟭" lemma D_eqI: fixes m n i j k defines "A ≡ {len m i j xs | xs. set xs ⊆ {0..k}}" defines "A_distinct ≡ {len m i j xs |xs. set xs ⊆ {0..k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}" assumes "cycle_free m n" "i ≤ n" "j ≤ n" "k ≤ n" "(⋀y. y ∈ A_distinct ⟹ x ≤ y)" "x ∈ A" shows "D m i j k = x" using assms proof - let ?S = "{len m i j xs |xs. set xs ⊆ {0..k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}" show ?thesis unfolding D_def proof (rule Min_eqI) have "?S ⊆ {len m i j xs |xs. set xs ⊆ {0..k} ∧ distinct xs}" by auto thus "finite {len m i j xs |xs. set xs ⊆ {0..k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}" using D_base_finite[of m i j k] by (rule finite_subset) next fix y assume "y ∈ ?S" hence "y ∈ A_distinct" using assms(2,7) by fastforce thus "x ≤ y" using assms by meson next from assms obtain xs where xs: "x = len m i j xs" "set xs ⊆ {0..k}" by auto let ?ys = "rem_cycles i j xs" let ?y = "len m i j ?ys" from assms(3-6) xs have *:"?y ≤ x" by (fastforce simp add: cycle_free_def) have distinct: "i ∉ set ?ys" "j ∉ set ?ys" "distinct ?ys" using rem_cycles_distinct remove_all_removes rem_cycles_removes_last by fast+ with xs(2) have "?y ∈ A_distinct" unfolding A_distinct_def using rem_cycles_subs by fastforce hence "x ≤ ?y" using assms by meson moreover have "?y ≤ x" using assms(3-6) xs by (fastforce simp add: cycle_free_def) ultimately have "x = ?y" by simp thus "x ∈ ?S" using distinct xs(2) rem_cycles_subs[of i j xs] by fastforce qed qed lemma D_base_not_empty: "{len m i j xs |xs. set xs ⊆ {0..k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs} ≠ {}" proof - have "len m i j [] ∈ {len m i j xs |xs. set xs ⊆ {0..k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}" by fastforce thus ?thesis by auto qed lemma Min_elem_dest: "finite A ⟹ A ≠ {} ⟹ x = Min A ⟹ x ∈ A" by simp lemma D_dest: "x = D m i j k ⟹ x ∈ {len m i j xs |xs. set xs ⊆ {0..Suc k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}" using Min_elem_dest[OF D_base_finite'' D_base_not_empty] by (fastforce simp add: D_def) lemma D_dest': "x = D m i j k ⟹ x ∈ {len m i j xs |xs. set xs ⊆ {0..Suc k}}" using Min_elem_dest[OF D_base_finite'' D_base_not_empty] by (fastforce simp add: D_def) lemma D_dest'': "x = D m i j k ⟹ x ∈ {len m i j xs |xs. set xs ⊆ {0..k}}" using Min_elem_dest[OF D_base_finite'' D_base_not_empty] by (fastforce simp add: D_def) lemma cycle_free_loop_dest: "i ≤ n ⟹ set xs ⊆ {0..n} ⟹ cycle_free m n ⟹ len m i i xs ≥ 𝟭" unfolding cycle_free_def by auto lemma cycle_free_dest: "cycle_free m n ⟹ i ≤ n ⟹ j ≤ n ⟹ set xs ⊆ {0..n} ⟹ len m i j (rem_cycles i j xs) ≤ len m i j xs" by (auto simp add: cycle_free_def) definition cycle_free_up_to :: "'a mat ⇒ nat ⇒ nat ⇒ bool" where "cycle_free_up_to m k n ≡ ∀ i xs. i ≤ n ∧ set xs ⊆ {0..k} ⟶ (∀ j. j ≤ n ⟶ len m i j (rem_cycles i j xs) ≤ len m i j xs) ∧ len m i i xs ≥ 𝟭" lemma cycle_free_up_to_loop_dest: "i ≤ n ⟹ set xs ⊆ {0..k} ⟹ cycle_free_up_to m k n ⟹ len m i i xs ≥ 𝟭" unfolding cycle_free_up_to_def by auto lemma cycle_free_up_to_diag: assumes "cycle_free_up_to m k n" "i ≤ n" shows "m i i ≥ 𝟭" using cycle_free_up_to_loop_dest[OF assms(2) _ assms(1), of "[]"] by auto lemma D_eqI2: fixes m n i j k defines "A ≡ {len m i j xs | xs. set xs ⊆ {0..k}}" defines "A_distinct ≡ {len m i j xs | xs. set xs ⊆ {0..k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}" assumes "cycle_free_up_to m k n" "i ≤ n" "j ≤ n" "k ≤ n" "(⋀y. y ∈ A_distinct ⟹ x ≤ y)" "x ∈ A" shows "D m i j k = x" using assms proof - show ?thesis proof (simp add: D_def A_distinct_def[symmetric], rule Min_eqI) show<