# Theory Floyd_Warshall

theory Floyd_Warshall imports Main begin chapter ‹Floyd-Warshall Algorithm for the All-Pairs Shortest Paths Problem› subsubsection ‹Auxiliary› lemma distinct_list_single_elem_decomp: "{xs. set xs ⊆ {0} ∧ distinct xs} = {[], [0]}" proof (standard, goal_cases) case 1 { fix xs :: "'a list" assume xs: "xs ∈ {xs. set xs ⊆ {0} ∧ distinct xs}" have "xs ∈ {[], [0]}" proof (cases xs) case (Cons y ys) hence y: "y = 0" using xs by auto with Cons xs have "ys = []" by (cases ys, auto) thus ?thesis using y Cons by simp qed simp } thus ?case by blast qed simp section ‹Cycles in Lists› abbreviation "cnt x xs ≡ length (filter (λy. x = y) xs)" fun remove_cycles :: "'a list ⇒ 'a ⇒ 'a list ⇒ 'a list" where "remove_cycles [] _ acc = rev acc" | "remove_cycles (x#xs) y acc = (if x = y then remove_cycles xs y [x] else remove_cycles xs y (x#acc))" lemma cnt_rev: "cnt x (rev xs) = cnt x xs" by (metis length_rev rev_filter) value "as @ [x] @ bs @ [x] @ cs @ [x] @ ds" lemma remove_cycles_removes: "cnt x (remove_cycles xs x ys) ≤ max 1 (cnt x ys)" proof (induction xs arbitrary: ys) case Nil thus ?case by (simp, cases "x ∈ set ys", (auto simp: cnt_rev[of x ys])) next case (Cons y xs) thus ?case proof (cases "x = y") case True thus ?thesis using Cons[of "[y]"] True by auto next case False thus ?thesis using Cons[of "y # ys"] by auto qed qed lemma remove_cycles_id: "x ∉ set xs ⟹ remove_cycles xs x ys = rev ys @ xs" by (induction xs arbitrary: ys) auto lemma remove_cycles_cnt_id: "x ≠ y ⟹ cnt y (remove_cycles xs x ys) ≤ cnt y ys + cnt y xs" proof (induction xs arbitrary: ys x) case Nil thus ?case by (simp add: cnt_rev) next case (Cons z xs) thus ?case proof (cases "x = z") case True thus ?thesis using Cons.IH[of z "[z]"] Cons.prems by auto next case False thus ?thesis using Cons.IH[of x "z # ys"] Cons.prems False by auto qed qed lemma remove_cycles_ends_cycle: "remove_cycles xs x ys ≠ rev ys @ xs ⟹ x ∈ set xs" using remove_cycles_id by fastforce lemma remove_cycles_begins_with: "x ∈ set xs ⟹ ∃ zs. remove_cycles xs x ys = x # zs ∧ x ∉ set zs" proof (induction xs arbitrary: ys) case Nil thus ?case by auto next case (Cons y xs) thus ?case proof (cases "x = y") case True thus ?thesis proof (cases "x ∈ set xs", goal_cases) case 1 with Cons show ?case by auto next case 2 with remove_cycles_id[of x xs "[y]"] show ?case by auto qed next case False with Cons show ?thesis by auto qed qed lemma remove_cycles_self: "x ∈ set xs ⟹ remove_cycles (remove_cycles xs x ys) x zs = remove_cycles xs x ys" proof - assume x:"x ∈ set xs" then obtain ws where ws: "remove_cycles xs x ys = x # ws" "x ∉ set ws" using remove_cycles_begins_with[OF x, of ys] by blast from remove_cycles_id[OF this(2)] have "remove_cycles ws x [x] = x # ws" by auto with ws(1) show "remove_cycles (remove_cycles xs x ys) x zs = remove_cycles xs x ys" by simp qed lemma remove_cycles_one: "remove_cycles (as @ x # xs) x ys = remove_cycles (x#xs) x ys" by (induction as arbitrary: ys) auto lemma remove_cycles_cycles: "x ∈ set xs ⟹ ∃ xxs as. as @ concat (map (λ xs. x # xs) xxs) @ remove_cycles xs x ys = xs ∧ x ∉ set as" proof (induction xs arbitrary: ys) case Nil thus ?case by auto next case (Cons y xs) thus ?case proof (cases "x = y") case True thus ?thesis proof (cases "x ∈ set xs", goal_cases) case 1 then obtain as xxs where "as @ concat (map (λxs. y#xs) xxs) @ remove_cycles xs y [y] = xs" using Cons.IH[of "[y]"] by auto hence "[] @ concat (map (λxs. x#xs) (as#xxs)) @ remove_cycles (y#xs) x ys = y # xs" by (simp add: ‹x = y›) thus ?thesis by fastforce next case 2 hence "remove_cycles (y # xs) x ys = y # xs" using remove_cycles_id[of x xs "[y]"] by auto hence "[] @ concat (map (λxs. x # xs) []) @ remove_cycles (y#xs) x ys = y # xs" by auto thus ?thesis by fastforce qed next case False then obtain as xxs where as: "as @ concat (map (λxs. x # xs) xxs) @ remove_cycles xs x (y#ys) = xs" "x ∉ set as" using Cons.IH[of "y # ys"] Cons.prems by auto hence "(y # as) @ concat (map (λxs. x # xs) xxs) @ remove_cycles (y#xs) x ys = y # xs" using ‹x ≠ y› by auto thus ?thesis using as(2) ‹x ≠ y› by fastforce qed qed fun start_remove :: "'a list ⇒ 'a ⇒ 'a list ⇒ 'a list" where "start_remove [] _ acc = rev acc" | "start_remove (x#xs) y acc = (if x = y then rev acc @ remove_cycles xs y [y] else start_remove xs y (x # acc))" lemma start_remove_decomp: "x ∈ set xs ⟹ ∃ as bs. xs = as @ x # bs ∧ start_remove xs x ys = rev ys @ as @ remove_cycles bs x [x]" proof (induction xs arbitrary: ys) case Nil thus ?case by auto next case (Cons y xs) thus ?case proof (auto, goal_cases) case 1 from 1(1)[of "y # ys"] obtain as bs where "xs = as @ x # bs" "start_remove xs x (y # ys) = rev (y # ys) @ as @ remove_cycles bs x [x]" by blast hence "y # xs = (y # as) @ x # bs" "start_remove xs x (y # ys) = rev ys @ (y # as) @ remove_cycles bs x [x]" by simp+ thus ?case by blast qed qed lemma start_remove_removes: "cnt x (start_remove xs x ys) ≤ Suc (cnt x ys)" proof (induction xs arbitrary: ys) case Nil thus ?case using cnt_rev[of x ys] by auto next case (Cons y xs) thus ?case proof (cases "x = y") case True thus ?thesis using remove_cycles_removes[of y xs "[y]"] cnt_rev[of y ys] by auto next case False thus ?thesis using Cons[of "y # ys"] by auto qed qed lemma start_remove_id[simp]: "x ∉ set xs ⟹ start_remove xs x ys = rev ys @ xs" by (induction xs arbitrary: ys) auto lemma start_remove_cnt_id: "x ≠ y ⟹ cnt y (start_remove xs x ys) ≤ cnt y ys + cnt y xs" proof (induction xs arbitrary: ys) case Nil thus ?case by (simp add: cnt_rev) next case (Cons z xs) thus ?case proof (cases "x = z", goal_cases) case 1 thus ?case using remove_cycles_cnt_id[of x y xs "[x]"] by (simp add: cnt_rev) next case 2 from this(1)[of "(z # ys)"] this(2,3) show ?case by auto qed qed fun remove_all_cycles :: "'a list ⇒ 'a list ⇒ 'a list" where "remove_all_cycles [] xs = xs" | "remove_all_cycles (x # xs) ys = remove_all_cycles xs (start_remove ys x [])" lemma cnt_remove_all_mono:"cnt y (remove_all_cycles xs ys) ≤ max 1 (cnt y ys)" proof (induction xs arbitrary: ys) case Nil thus ?case by auto next case (Cons x xs) thus ?case proof (cases "x = y") case True thus ?thesis using start_remove_removes[of y ys "[]"] Cons[of "start_remove ys y []"] by auto next case False hence "cnt y (start_remove ys x []) ≤ cnt y ys" using start_remove_cnt_id[of x y ys "[]"] by auto thus ?thesis using Cons[of "start_remove ys x []"] by auto qed qed lemma cnt_remove_all_cycles: "x ∈ set xs ⟹ cnt x (remove_all_cycles xs ys) ≤ 1" proof (induction xs arbitrary: ys) case Nil thus ?case by auto next case (Cons y xs) thus ?case using start_remove_removes[of x ys "[]"] cnt_remove_all_mono[of y xs "start_remove ys y []"] by auto qed lemma cnt_mono: "cnt a (b # xs) ≤ cnt a (b # c # xs)" by (induction xs) auto lemma cnt_distinct_intro: "∀ x ∈ set xs. cnt x xs ≤ 1 ⟹ distinct xs" proof (induction xs) case Nil thus ?case by auto next case (Cons x xs) from this(2) have "∀ x ∈ set xs. cnt x xs ≤ 1" by (metis filter.simps(2) impossible_Cons linorder_class.linear list.set_intros(2) preorder_class.order_trans) with Cons.IH have "distinct xs" by auto moreover have "x ∉ set xs" using Cons.prems proof (induction xs) case Nil then show ?case by auto next case (Cons a xs) from this(2) have "∀xa∈set (x # xs). cnt xa (x # a # xs) ≤ 1" by auto then have *: "∀xa∈set (x # xs). cnt xa (x # xs) ≤ 1" proof (safe, goal_cases) case (1 b) then have "cnt b (x # a # xs) ≤ 1" by auto with cnt_mono[of b x xs a] show ?case by fastforce qed with Cons(1) have "x ∉ set xs" by auto moreover have "x ≠ a" by (metis (full_types) Cons.prems One_nat_def * empty_iff filter.simps(2) impossible_Cons le_0_eq le_Suc_eq length_0_conv list.set(1) list.set_intros(1)) ultimately show ?case by auto qed ultimately show ?case by auto qed lemma remove_cycles_subs: "set (remove_cycles xs x ys) ⊆ set xs ∪ set ys" by (induction xs arbitrary: ys; auto; fastforce) lemma start_remove_subs: "set (start_remove xs x ys) ⊆ set xs ∪ set ys" using remove_cycles_subs by (induction xs arbitrary: ys; auto; fastforce) lemma remove_all_cycles_subs: "set (remove_all_cycles xs ys) ⊆ set ys" using start_remove_subs by (induction xs arbitrary: ys, auto) (fastforce+) lemma remove_all_cycles_distinct: "set ys ⊆ set xs ⟹ distinct (remove_all_cycles xs ys)" proof - assume "set ys ⊆ set xs" hence "∀ x ∈ set ys. cnt x (remove_all_cycles xs ys) ≤ 1" using cnt_remove_all_cycles by fastforce hence "∀ x ∈ set (remove_all_cycles xs ys). cnt x (remove_all_cycles xs ys) ≤ 1" using remove_all_cycles_subs by fastforce thus "distinct (remove_all_cycles xs ys)" using cnt_distinct_intro by auto qed lemma distinct_remove_cycles_inv: "distinct (xs @ ys) ⟹ distinct (remove_cycles xs x ys)" proof (induction xs arbitrary: ys) case Nil thus ?case by auto next case (Cons y xs) thus ?case by auto qed definition "remove_all x xs = (if x ∈ set xs then tl (remove_cycles xs x []) else xs)" definition "remove_all_rev x xs = (if x ∈ set xs then rev (tl (remove_cycles (rev xs) x [])) else xs)" lemma remove_all_distinct: "distinct xs ⟹ distinct (x # remove_all x xs)" proof (cases "x ∈ set xs", goal_cases) case 1 from remove_cycles_begins_with[OF 1(2), of "[]"] obtain zs where "remove_cycles xs x [] = x # zs" "x ∉ set zs" by auto thus ?thesis using 1(1) distinct_remove_cycles_inv[of "xs" "[]" x] by (simp add: remove_all_def) next case 2 thus ?thesis by (simp add: remove_all_def) qed lemma remove_all_removes: "x ∉ set (remove_all x xs)" by (metis list.sel(3) remove_all_def remove_cycles_begins_with) lemma remove_all_subs: "set (remove_all x xs) ⊆ set xs" using remove_cycles_subs remove_all_def by (metis (no_types, lifting) append_Nil2 list.sel(2) list.set_sel(2) set_append subsetCE subsetI) lemma remove_all_rev_distinct: "distinct xs ⟹ distinct (x # remove_all_rev x xs)" proof (cases "x ∈ set xs", goal_cases) case 1 then have "x ∈ set (rev xs)" by auto from remove_cycles_begins_with[OF this, of "[]"] obtain zs where "remove_cycles (rev xs) x [] = x # zs" "x ∉ set zs" by auto thus ?thesis using 1(1) distinct_remove_cycles_inv[of "rev xs" "[]" x] by (simp add: remove_all_rev_def) next case 2 thus ?thesis by (simp add: remove_all_rev_def) qed lemma remove_all_rev_removes: "x ∉ set (remove_all_rev x xs)" by (metis remove_all_def remove_all_removes remove_all_rev_def set_rev) lemma remove_all_rev_subs: "set (remove_all_rev x xs) ⊆ set xs" by (metis remove_all_def remove_all_subs set_rev remove_all_rev_def) abbreviation "rem_cycles i j xs ≡ remove_all i (remove_all_rev j (remove_all_cycles xs xs))" lemma rem_cycles_distinct': "i ≠ j ⟹ distinct (i # j # rem_cycles i j xs)" proof - assume "i ≠ j" have "distinct (remove_all_cycles xs xs)" by (simp add: remove_all_cycles_distinct) from remove_all_rev_distinct[OF this] have "distinct (remove_all_rev j (remove_all_cycles xs xs))" by simp from remove_all_distinct[OF this] have "distinct (i # rem_cycles i j xs)" by simp moreover have "j ∉ set (rem_cycles i j xs)" using remove_all_subs remove_all_rev_removes remove_all_removes by fastforce ultimately show ?thesis by (simp add: ‹i ≠ j›) qed lemma rem_cycles_removes_last: "j ∉ set (rem_cycles i j xs)" by (meson remove_all_rev_removes remove_all_subs rev_subsetD) lemma rem_cycles_distinct: "distinct (rem_cycles i j xs)" by (meson distinct.simps(2) order_refl remove_all_cycles_distinct remove_all_distinct remove_all_rev_distinct) lemma rem_cycles_subs: "set (rem_cycles i j xs) ⊆ set xs" by (meson order_trans remove_all_cycles_subs remove_all_subs remove_all_rev_subs) section ‹Definition of the Algorithm› text ‹ We formalize the Floyd-Warshall algorithm on a linearly ordered abelian semigroup. However, we would not need an ‹abelian› monoid if we had the right type class. › 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 (in -) finite_distinct: "finite s ⟹ finite {xs . set xs ⊆ s ∧ distinct xs}" proof - assume "finite s" hence "{xs . set xs ⊆ s ∧ distinct xs} ⊆ {xs. set xs ⊆ s ∧ length xs ≤ card s}" using distinct_length_le by auto moreover have "finite {xs. set xs ⊆ s ∧ length xs ≤ card s}" using finite_lists_length_le[OF ‹finite s›] by auto ultimately show ?thesis by (rule finite_subset) qed lemma D_base_finite: "finite {len m i j xs | xs. set xs ⊆ {0..k} ∧ distinct xs}" using finite_distinct finite_image_set by blast lemma D_base_finite': "finite {len m i j xs | xs. set xs ⊆ {0..k} ∧ distinct (i # j # xs)}" proof - have "{len m i j xs | xs. set xs ⊆ {0..k} ∧ distinct (i # j # xs)} ⊆ {len m i j xs | xs. set xs ⊆ {0..k} ∧ distinct xs}" by auto with D_base_finite[of m i j k] show ?thesis by (rule rev_finite_subset) qed lemma D_base_finite'': "finite {len m i j xs |xs. set xs ⊆ {0..k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}" using D_base_finite[of m i j k] by - (rule finite_subset, auto) definition cycle_free :: "'a mat ⇒ nat ⇒ bool" where "cycle_free m n ≡ ∀ i xs. i ≤ n ∧ set xs ⊆ {0..n} ⟶ (∀ j. j ≤ n ⟶ len m i j (rem_cycles i j xs) ≤ len m i j xs) ∧ len m i i xs ≥ 𝟭" lemma D_eqI: fixes m n i j k defines "A ≡ {len m i j xs | xs. set xs ⊆ {0..k}}" defines "A_distinct ≡ {len m i j xs |xs. set xs ⊆ {0..k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}" assumes "cycle_free m n" "i ≤ n" "j ≤ n" "k ≤ n" "(⋀y. y ∈ A_distinct ⟹ x ≤ y)" "x ∈ A" shows "D m i j k = x" using assms proof - let ?S = "{len m i j xs |xs. set xs ⊆ {0..k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}" show ?thesis unfolding D_def proof (rule Min_eqI) have "?S ⊆ {len m i j xs |xs. set xs ⊆ {0..k} ∧ distinct xs}" by auto thus "finite {len m i j xs |xs. set xs ⊆ {0..k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}" using D_base_finite[of m i j k] by (rule finite_subset) next fix y assume "y ∈ ?S" hence "y ∈ A_distinct" using assms(2,7) by fastforce thus "x ≤ y" using assms by meson next from assms obtain xs where xs: "x = len m i j xs" "set xs ⊆ {0..k}" by auto let ?ys = "rem_cycles i j xs" let ?y = "len m i j ?ys" from assms(3-6) xs have *:"?y ≤ x" by (fastforce simp add: cycle_free_def) have distinct: "i ∉ set ?ys" "j ∉ set ?ys" "distinct ?ys" using rem_cycles_distinct remove_all_removes rem_cycles_removes_last by fast+ with xs(2) have "?y ∈ A_distinct" unfolding A_distinct_def using rem_cycles_subs by fastforce hence "x ≤ ?y" using assms by meson moreover have "?y ≤ x" using assms(3-6) xs by (fastforce simp add: cycle_free_def) ultimately have "x = ?y" by simp thus "x ∈ ?S" using distinct xs(2) rem_cycles_subs[of i j xs] by fastforce qed qed lemma D_base_not_empty: "{len m i j xs |xs. set xs ⊆ {0..k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs} ≠ {}" proof - have "len m i j [] ∈ {len m i j xs |xs. set xs ⊆ {0..k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}" by fastforce thus ?thesis by auto qed lemma Min_elem_dest: "finite A ⟹ A ≠ {} ⟹ x = Min A ⟹ x ∈ A" by simp lemma D_dest: "x = D m i j k ⟹ x ∈ {len m i j xs |xs. set xs ⊆ {0..Suc k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}" using Min_elem_dest[OF D_base_finite'' D_base_not_empty] by (fastforce simp add: D_def) lemma D_dest': "x = D m i j k ⟹ x ∈ {len m i j xs |xs. set xs ⊆ {0..Suc k}}" using Min_elem_dest[OF D_base_finite'' D_base_not_empty] by (fastforce simp add: D_def) lemma D_dest'': "x = D m i j k ⟹ x ∈ {len m i j xs |xs. set xs ⊆ {0..k}}" using Min_elem_dest[OF D_base_finite'' D_base_not_empty] by (fastforce simp add: D_def) lemma cycle_free_loop_dest: "i ≤ n ⟹ set xs ⊆ {0..n} ⟹ cycle_free m n ⟹ len m i i xs ≥ 𝟭" unfolding cycle_free_def by auto lemma cycle_free_dest: "cycle_free m n ⟹ i ≤ n ⟹ j ≤ n ⟹ set xs ⊆ {0..n} ⟹ len m i j (rem_cycles i j xs) ≤ len m i j xs" 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 "finite A_distinct" using D_base_finite''[of m i j k] unfolding A_distinct_def by auto next fix y assume "y ∈ A_distinct" thus "x ≤ y" using assms by meson next from assms obtain xs where xs: "x = len m i j xs" "set xs ⊆ {0..k}" by auto let ?ys = "rem_cycles i j xs" let ?y = "len m i j ?ys" from assms(3-6) xs have *:"?y ≤ x" by (fastforce simp add: cycle_free_up_to_def) have distinct: "i ∉ set ?ys" "j ∉ set ?ys" "distinct ?ys" using rem_cycles_distinct remove_all_removes rem_cycles_removes_last by fast+ with xs(2) have "?y ∈ A_distinct" unfolding A_distinct_def using rem_cycles_subs by fastforce hence "x ≤ ?y" using assms by meson moreover have "?y ≤ x" using assms(3-6) xs by (fastforce simp add: cycle_free_up_to_def) ultimately have "x = ?y" by simp then show "x ∈ A_distinct" using distinct xs(2) rem_cycles_subs[of i j xs] unfolding A_distinct_def by fastforce qed qed section ‹Result Under The Absence of Negative Cycles› text ‹ This proves that the algorithm correctly computes shortest paths under the absence of negative cycles by a standard argument. › theorem fw_shortest_path_up_to: "cycle_free_up_to m k n ⟹ i' ≤ i ⟹ j' ≤ j ⟹ i ≤ n ⟹ j ≤ n ⟹ k ≤ n ⟹ D m i' j' k = fw m n k i j i' j'" proof (induction k arbitrary: i j i' j') case 0 from cycle_free_up_to_diag[OF 0(1)] have diag: "∀ k ≤ n. m k k ≥ 𝟭" by auto then have m_diag: "m 0 0 ≥ 𝟭" by simp let ?S = "{len m i' j' xs |xs. set xs ⊆ {0} ∧ i' ∉ set xs ∧ j' ∉ set xs ∧ distinct xs}" show ?case unfolding D_def proof (simp, rule Min_eqI) have "?S ⊆ {len m i' j' xs |xs. set xs ⊆ {0..0} ∧ distinct xs}" by auto thus "finite ?S" using D_base_finite[of m i' j' 0] by (rule finite_subset) next fix l assume "l ∈ ?S" then obtain xs where l: "l = len m i' j' xs" and xs: "xs = [] ∨ xs = [0]" using distinct_list_single_elem_decomp by auto { assume "xs = []" have "fw m n 0 i j i' j' ≤ fw m n 0 0 0 i' j'" using fw_invariant 0 by blast also have "… ≤ m i' j'" by (cases "i' = 0 ∧ j' = 0") (simp add: fw_upd_def upd_def)+ finally have "fw m n 0 i j i' j' ≤ l" using ‹xs = []› l by simp } moreover { assume "xs = [0]" have "fw m n 0 i j i' j' ≤ fw m n 0 i' j' i' j'" using fw_invariant 0 by blast also have "… ≤ m i' 0 + m 0 j'" proof (cases j') assume "j' = 0" show ?thesis proof (cases i') assume "i' = 0" thus ?thesis using ‹j' = 0› by (simp add: fw_upd_def upd_def) next fix i'' assume i'': "i' = Suc i''" have "fw_upd (fw m n 0 i'' n) 0 (Suc i'') 0 (Suc i'') 0 ≤ fw m n 0 i'' n (Suc i'') 0" by (simp add: fw_upd_mono) also have "… ≤ m (Suc i'') 0" using fw_mono 0 i'' by simp finally show ?thesis using ‹j' = 0› m_diag i'' neutr add_mono by fastforce qed next fix j'' assume j'': "j' = Suc j''" have "fw_upd (fw m n 0 i' j'') 0 i' (Suc j'') i' (Suc j'') ≤ fw m n 0 i' j'' i' 0 + fw m n 0 i' j'' 0 (Suc j'') " by (simp add: fw_upd_def upd_def) also have "… ≤ m i' 0 + m 0 (Suc j'')" using fw_mono[of i' n j'' i' 0 m 0] fw_mono[of i' n j'' 0 "Suc j''" m 0 ] j'' 0 by (simp add: add_mono) finally show ?thesis using j'' by simp qed finally have "fw m n 0 i j i' j' ≤ l" using ‹xs = [0]› l by simp } ultimately show "fw m n 0 i j i' j' ≤ l" using xs by auto next have A: "fw m n 0 i j i' j' = fw m n 0 i' j' i' j'" using single_iteration_inv 0 by blast have "fw m n 0 i' j' i' j' = min (m i' j') (m i' 0 + m 0 j')" using 0 by (simp add: fw_step_0[of m, OF m_diag]) hence "fw m n 0 i' j' i' j' = m i' j' ∨ (fw m n 0 i' j' i' j' = m i' 0 + m 0 j'∧ m i' 0 + m 0 j' ≤ m i' j')" by (auto simp add: ord.min_def) thus "fw m n 0 i j i' j' ∈ ?S" proof (standard, goal_cases) case 1 hence "fw m n 0 i j i' j' = len m i' j' []" using A by auto thus ?case by fastforce next case 2 hence *:"fw m n 0 i j i' j' = len m i' j' [0]" using A by auto thus ?case proof (cases "i' = 0 ∨ j' = 0") case False thus ?thesis using * by fastforce next case True { assume "i' = 0" from diag have "m 0 0 + m 0 j' ≥ m 0 j'" by (auto intro: add_mono_neutl) with ‹i' = 0› have "fw m n 0 i j i' j' = len m 0 j' []" using 0 A 2 by auto } moreover { assume "j' = 0" from diag have "m i' 0 + m 0 0 ≥ m i' 0" by (auto intro: add_mono_neutr) with ‹j' = 0› have "fw m n 0 i j i' j' = len m i' 0 []" using 0 A 2 by auto } ultimately have "fw m n 0 i j i' j' = len m i' j' []" using True by auto then show ?thesis by fastforce qed qed qed next case (Suc k) from cycle_free_up_to_diag[OF Suc.prems(1)] have diag: "∀ k ≤ n. m k k ≥ 𝟭" by auto from Suc.prems have cycle_free_to_k: "cycle_free_up_to m k n" by (fastforce simp add: cycle_free_up_to_def) { fix k' assume "k' ≤ n" with Suc cycle_free_to_k have "D m k' k' k = fw m n k n n k' k'" by auto from D_dest''[OF this[symmetric]] obtain xs where "set xs ⊆ {0..k}" "fw m n k n n k' k'= len m k' k' xs" by auto with Suc(2) ‹Suc k ≤ n› ‹k' ≤ n› have "fw m n k n n k' k' ≥ 𝟭" unfolding cycle_free_up_to_def by force } hence K: "∀k'≤n. fw m n k n n k' k' ≥ 𝟭" by simp let ?S = "λ k i j. {len m i j xs |xs. set xs ⊆ {0..k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}" show ?case proof (rule D_eqI2) show "cycle_free_up_to m (Suc k) n" using Suc.prems(1) . next show "i' ≤ n" using Suc.prems by simp next show "j' ≤ n" using Suc.prems by simp next show "Suc k ≤ n" using Suc.prems by simp next fix l assume "l ∈ {len m i' j' xs | xs. set xs ⊆ {0..Suc k} ∧ i' ∉ set xs ∧ j' ∉ set xs ∧ distinct xs}" then obtain xs where xs: "l = len m i' j' xs" "set xs ⊆ {0..Suc k}" "i' ∉ set xs" "j' ∉ set xs" "distinct xs" by auto have IH: "D m i' j' k = fw m n k i j i' j'" using cycle_free_to_k Suc by auto have fin: "finite {len m i' j' xs |xs. set xs ⊆ {0..k} ∧ i' ∉ set xs ∧ j' ∉ set xs ∧ distinct xs}" using D_base_finite'' by simp show "fw m n (Suc k) i j i' j' ≤ l" proof (cases "Suc k ∈ set xs") case False hence "set xs ⊆ {0..k}" using xs(2) using atLeastAtMostSuc_conv by auto hence "l ∈ {len m i' j' xs | xs. set xs ⊆ {0..k} ∧ i' ∉ set xs ∧ j' ∉ set xs ∧ distinct xs}" using xs by auto with Min_le[OF fin this] have "fw m n k i j i' j' ≤ l" using IH by (simp add: D_def) thus ?thesis using fw_invariant[of k "Suc k" i n j j i m i' j'] Suc.prems by simp next case True then obtain ys zs where ys_zs_id: "xs = ys @ Suc k # zs" by (meson split_list) with xs(5) have ys_zs: "distinct ys" "distinct zs" "Suc k ∉ set ys" "Suc k ∉ set zs" "set ys ∩ set zs = {}" by auto have "i' ≠ Suc k" "j' ≠ Suc k" using xs(3,4) True by auto have "set ys ⊆ {0..k}" using ys_zs(3) xs(2) ys_zs_id using atLeastAtMostSuc_conv by auto hence "len m i' (Suc k) ys ∈ ?S k i' (Suc k)" using ys_zs_id ys_zs xs(3) by fastforce with Min_le[OF _ this] have "Min (?S k i' (Suc k)) ≤ len m i' (Suc k) ys" using D_base_finite'[of m i' "Suc k" k] ‹i' ≠ Suc k› by fastforce moreover have "fw m n k n n i' (Suc k) = D m i' (Suc k) k" using Suc.IH[OF cycle_free_to_k, of i' n] Suc.prems by auto ultimately have *:"fw m n k n n i' (Suc k) ≤ len m i' (Suc k) ys" using ‹i' ≠ Suc k› by (auto simp: D_def) have "set zs ⊆ {0..k}" using ys_zs(4) xs(2) ys_zs_id using atLeastAtMostSuc_conv by auto hence "len m (Suc k) j' zs ∈ ?S k (Suc k) j'" using ys_zs_id ys_zs xs(3,4,5) by fastforce with Min_le[OF _ this] have "Min (?S k (Suc k) j') ≤ len m (Suc k) j' zs" using D_base_finite'[of m "Suc k" j' k] ‹j' ≠ Suc k› by fastforce moreover have "fw m n k n n (Suc k) j' = D m (Suc k) j' k" using Suc.IH[OF cycle_free_to_k, of "Suc k" n j' n] Suc.prems by auto ultimately have **:"fw m n k n n (Suc k) j' ≤ len m (Suc k) j' zs" using ‹j' ≠ Suc k› by (auto simp: D_def) have len_eq: "l = len m i' (Suc k) ys + len m (Suc k) j' zs" by (simp add: xs(1) len_decomp[OF ys_zs_id, symmetric] ys_zs_id) have "fw m n (Suc k) i' j' i' j' ≤ fw m n k n n i' (Suc k) + fw m n k n n (Suc k) j'" using fw_step_Suc[of n m k i' j', OF K] Suc.prems(2-) by simp hence "fw m n (Suc k) i' j' i' j' ≤ l" using fw_step_Suc[of n m k i j] Suc.prems(3-) * ** len_eq add_mono by fastforce thus ?thesis using fw_invariant[of "Suc k" "Suc k" i n j j' i' m i' j'] Suc.prems(2-) by simp qed next have "fw m n (Suc k) i j i' j' = fw m n (Suc k) i' j' i' j'" using single_iteration_inv[OF Suc.prems(2-5)] . also have "… = min (fw m n k n n i' j') (fw m n k n n i' (Suc k) + fw m n k n n (Suc k) j')" using fw_step_Suc[OF K] Suc.prems(2-) by simp finally show "fw m n (Suc k) i j i' j' ∈ {len m i' j' xs | xs. set xs ⊆ {0..Suc k}}" proof (cases "fw m n (Suc k) i j i' j' = fw m n k n n i' j'", goal_cases) case True have "fw m n (Suc k) i j i' j' = D m i' j' k" using Suc.IH[OF cycle_free_to_k, of i' n j' n] Suc.prems(2-) True by simp from D_dest'[OF this] show ?thesis by blast next case 2 hence A:"fw m n (Suc k) i j i' j' = fw m n k n n i' (Suc k) + fw m n k n n (Suc k) j'" by (metis ord.min_def) have "fw m n k n n i' j' = D m i' j' k" using Suc.IH[OF cycle_free_to_k, of i' n j' n] Suc.prems by simp from D_dest[OF this] have B:"fw m n k n n i' j' ∈ ?S (Suc k) i' j'" by blast have "fw m n k n n i' (Suc k) = D m i' (Suc k) k" using Suc.IH[OF cycle_free_to_k, of i' n "Suc k" n] Suc.prems by simp from D_dest'[OF this] obtain xs where xs: "fw m n k n n i' (Suc k) = len m i' (Suc k) xs" "set xs ⊆ {0..Suc k}" by blast have "fw m n k n n (Suc k) j' = D m (Suc k) j' k" using Suc.IH[OF cycle_free_to_k, of "Suc k" n j' n] Suc.prems by simp from D_dest'[OF this] obtain ys where ys: "fw m n k n n (Suc k) j' = len m (Suc k) j' ys" "set ys ⊆ {0..Suc k}" by blast from A xs(1) ys(1) len_comp have "fw m n (Suc k) i j i' j' = len m i' j' (xs @ Suc k # ys)" by simp moreover have "set (xs @ Suc k # ys) ⊆ {0..Suc k}" using xs(2) ys(2) by auto ultimately show ?thesis by blast qed qed qed lemma cycle_free_cycle_free_up_to: "cycle_free m n ⟹ k ≤ n ⟹ cycle_free_up_to m k n" unfolding cycle_free_def cycle_free_up_to_def by force lemma cycle_free_diag: "cycle_free m n ⟹ i ≤ n ⟹ 𝟭 ≤ m i i" using cycle_free_up_to_diag[OF cycle_free_cycle_free_up_to] by blast corollary fw_shortest_path: "cycle_free m n ⟹ i' ≤ i ⟹ j' ≤ j ⟹ i ≤ n ⟹ j ≤ n ⟹ k ≤ n ⟹ D m i' j' k = fw m n k i j i' j'" using fw_shortest_path_up_to[OF cycle_free_cycle_free_up_to] by auto corollary fw_shortest: assumes "cycle_free m n" "i ≤ n" "j ≤ n" "k ≤ n" shows "fw m n n n n i j ≤ fw m n n n n i k + fw m n n n n k j" proof (rule ccontr, goal_cases) case 1 let ?S = "λ i j. {len m i j xs |xs. set xs ⊆ {0..n}}" let ?FW = "fw m n n n n" from assms fw_shortest_path have FW: "?FW i j = D m i j n" "?FW i k = D m i k n" "?FW k j = D m k j n" by auto with D_dest'' FW have "?FW i k ∈ ?S i k" "?FW k j ∈ ?S k j" by auto then obtain xs ys where xs_ys: "?FW i k = len m i k xs" "set xs ⊆ {0..n}" "?FW k j = len m k j ys" "set ys ⊆ {0..n}" by auto let ?zs = "rem_cycles i j (xs @ k # ys)" have *:"?FW i j = Min {len m i j xs |xs. set xs ⊆ {0..n} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}" using FW(1) unfolding D_def . have "set (xs @ k # ys) ⊆ {0..n}" using assms xs_ys by fastforce from cycle_free_dest [OF ‹cycle_free m n› ‹i ≤ n› ‹j ≤ n› this] have **:"len m i j ?zs ≤ len m i j (xs @ k # ys)" by auto moreover have "i ∉ set ?zs" "j ∉ set ?zs" "distinct ?zs" using rem_cycles_distinct remove_all_removes rem_cycles_removes_last by fast+ moreover have "set ?zs ⊆ {0..n}" using rem_cycles_subs[of i j"xs @ k # ys"] xs_ys assms by fastforce ultimately have "len m i j ?zs ∈ {len m i j xs |xs. set xs ⊆ {0..n} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs}" by blast with * have "?FW i j ≤ len m i j ?zs" using D_base_finite'' by auto with ** xs_ys len_comp 1 show ?case by auto qed section ‹Result Under the Presence of Negative Cycles› lemma not_cylce_free_dest: "¬ cycle_free m n ⟹ ∃ k ≤ n. ¬ cycle_free_up_to m k n" by (auto simp add: cycle_free_def cycle_free_up_to_def) lemma D_not_diag_le: "(x :: 'a) ∈ {len m i j xs |xs. set xs ⊆ {0..k} ∧ i ∉ set xs ∧ j ∉ set xs ∧ distinct xs} ⟹ D m i j k ≤ x" using Min_le[OF D_base_finite''] by (auto simp add: D_def) lemma D_not_diag_le': "set xs ⊆ {0..k} ⟹ i ∉ set xs ⟹ j ∉ set xs ⟹ distinct xs ⟹ D m i j k ≤ len m i j xs" using Min_le[OF D_base_finite''] by (fastforce simp add: D_def) lemma (in -) nat_upto_subs_top_removal': "S ⊆ {0..Suc n} ⟹ Suc n ∉ S ⟹ S ⊆ {0..n}" apply (induction n) apply safe apply (rename_tac x) apply (case_tac "x = Suc 0"; fastforce) apply (rename_tac n x) apply (case_tac "x = Suc (Suc n)"; fastforce) done lemma (in -) nat_upto_subs_top_removal: "S ⊆ {0..n::nat} ⟹ n ∉ S ⟹ S ⊆ {0..n - 1}" using nat_upto_subs_top_removal' by (cases n; simp) lemma fw_Suc: "i ≤ n ⟹ j ≤ n ⟹ i' ≤ n ⟹ j' ≤ n ⟹ fw m n (Suc k) i' j' i j ≤ fw m n k n n i j" by (metis Suc_innermost_id1' Suc_innermost_id2 Suc_innermost_mono linorder_class.not_le order.eq_iff preorder_class.order_refl single_iteration_inv single_iteration_inv') lemma negative_len_shortest: "length xs = n ⟹ len m i i xs < 𝟭 ⟹ ∃ j ys. distinct (j # ys) ∧ len m j j ys < 𝟭 ∧ j ∈ set (i # xs) ∧ set ys ⊆ set xs" proof (induction n arbitrary: xs i rule: less_induct) case (less n) show ?case proof (cases xs) case Nil thus ?thesis using less.prems by auto next case (Cons y ys) then have "length xs ≥ 1" by auto show ?thesis proof (cases "i ∈ set xs") assume i: "i ∈ set xs" then obtain as bs where xs: "xs = as @ i # bs" by (meson split_list) show ?thesis proof (cases "len m i i as < 𝟭") case True from xs less.prems have "length as < n" by auto from less.IH[OF this _ True] xs show ?thesis by auto next case False from len_decomp[OF xs] have "len m i i xs = len m i i as + len m i i bs" by auto with False less.prems have *: "len m i i bs < 𝟭" by (metis add_lt_neutral local.dual_order.strict_trans local.neqE) from xs less.prems have "length bs < n" by auto from less.IH[OF this _ *] xs show ?thesis by auto qed next assume i: "i ∉ set xs" show ?thesis proof (cases "distinct xs") case True with i less.prems show ?thesis by auto next case False from not_distinct_decomp[OF this] obtain a as bs cs where xs: "xs = as @ a # bs @ a # cs" by auto show ?thesis proof (cases "len m a a bs < 𝟭") case True from xs less.prems have "length bs < n" by auto from less.IH[OF this _ True] xs show ?thesis by auto next case False from len_decomp[OF xs, of m i i] len_decomp[of "bs @ a # cs" bs a cs m a i] have *:"len m i i xs = len m i a as + (len m a a bs + len m a i cs)" by auto from False have "len m a a bs ≥ 𝟭" by auto with add_mono have "len m a a bs + len m a i cs ≥ len m a i cs" by fastforce with * have "len m i i xs ≥ len m i a as + len m a i cs" by (simp add: add_mono) with less.prems(2) have "len m i a as + len m a i cs < 𝟭" by auto with len_comp have "len m i i (as @ a # cs) < 𝟭" by auto from less.IH[OF _ _ this, of "length (as @ a # cs)"] xs less.prems show ?thesis by auto qed qed qed qed qed theorem FW_neg_cycle_detect: "¬ cycle_free m n ⟹ ∃ i ≤ n. fw m n n n n i i < 𝟭" proof - assume A: "¬ cycle_free m n" let ?K = "{k. k ≤ n ∧ ¬ cycle_free_up_to m k n}" let ?k = "Min ?K" have not_empty_K: "?K ≠ {}" using not_cylce_free_dest[OF A(1)] by auto have "finite ?K" by auto with not_empty_K have *: "∀ k' < ?k. cycle_free_up_to m k' n" by (auto, metis le_trans less_or_eq_imp_le preorder_class.less_irrefl) from linorder_class.Min_in[OF ‹finite ?K› ‹?K ≠ {}›] have "¬ cycle_free_up_to m ?k n" "?k ≤ n" by auto then have "∃ xs j. j ≤ n ∧ len m j j xs < 𝟭 ∧ set xs ⊆ {0..?k}" unfolding cycle_free_up_to_def proof (auto, goal_cases) case (2 i xs) then have "len m i i xs < 𝟭" by auto with 2 show ?case by auto next case (1 i xs j) then have "len m i j (rem_cycles i j xs) > len m i j xs" by auto from negative_cycle_dest[OF this] obtain i' ys where ys: "i' ∈ set (i # j # xs)" "len m i' i' ys < 𝟭" "set ys ⊆ set xs" by blast from ys(1) 1(2-4) show ?case proof (auto, goal_cases) case 1 with ys(2,3) show ?case by auto next case 2 with ys(2,3) show ?case by auto next case 3 with ‹?k ≤ n› have "i' ≤ n" unfolding cycle_free_up_to_def by auto with 3 ys(2,3) show ?case by auto qed qed then obtain a as where a_as: "a ≤ n ∧ len m a a as < 𝟭 ∧ set as ⊆ {0..?k}" by auto with negative_len_shortest[of as "length as" m a] obtain j xs where j_xs: "distinct (j # xs) ∧ len m j j xs < 𝟭 ∧ j ∈ set (a # as) ∧ set xs ⊆ set as" by auto with a_as ‹?k ≤ n› have cyc: "j ≤ n" "set xs ⊆ {0..?k}" "len m j j xs < 𝟭" "distinct (j # xs)" by auto { assume "?k > 0" then have "?k - 1 < ?k" by simp with * have **:"cycle_free_up_to m (?k - 1) n" by blast have "?k ∈ set xs" proof (rule ccontr, goal_cases) case 1 with ‹set xs ⊆ {0..?k}› nat_upto_subs_top_removal have "set xs ⊆ {0..?k-1}" by auto from cycle_free_up_to_loop_dest[OF ‹j ≤ n› this ‹cycle_free_up_to m (?k - 1) n›] cyc(3) show ?case by auto qed with cyc(4) have "j ≠ ?k" by auto from ‹?k ∈ set xs› obtain ys zs where "xs = ys @ ?k # zs" by (meson split_list) with ‹distinct (j # xs)› have xs: "xs = ys @ ?k # zs" "distinct ys" "distinct zs" "?k ∉ set ys" "?k ∉ set zs" "j ∉ set ys" "j ∉ set zs" by auto from xs(1,4) ‹set xs ⊆ {0..?k}› nat_upto_subs_top_removal have ys: "set ys ⊆ {0..?k-1}" by auto from xs(1,5) ‹set xs ⊆ {0..?k}› nat_upto_subs_top_removal have zs: "set zs ⊆ {0..?k-1}" by auto have "D m j ?k (?k - 1) = fw m n (?k - 1) n n j ?k" using ‹?k ≤ n› ‹j ≤ n› fw_shortest_path_up_to[OF **, of j n ?k n] by auto moreover have "D m ?k j (?k - 1) = fw m n (?k - 1) n n ?k j" using ‹?k ≤ n› ‹j ≤ n› fw_shortest_path_up_to[OF **, of ?k n j n] by auto ultimately have "fw m n (?k - 1) n n j ?k + fw m n (?k - 1) n n ?k j ≤ len m j ?k ys + len m ?k j zs" using D_not_diag_le'[OF zs(1) xs(5,7,3), of m] D_not_diag_le'[OF ys(1) xs(6,4,2), of m] by (auto simp: add_mono) then have neg: "fw m n (?k - 1) n n j ?k + fw m n (?k - 1) n n ?k j < 𝟭" using xs(1) ‹len m j j xs < 𝟭› len_comp by auto have "fw m n ?k j j j j ≤ fw m n (?k - 1) n n j ?k + fw m n (?k - 1) n n ?k j" proof (cases "j = 0") case True with‹?k > 0› fw.simps(2)[of m n "?k - 1"] have "fw m n ?k j j = fw_upd (fw m n (?k - 1) n n) ?k j j" by auto then have "fw m n ?k j j j j ≤ fw m n (?k - 1) n n j ?k + fw m n (?k - 1) n n ?k j" by (simp add: fw_upd_def upd_def) then show ?thesis by auto next case False with fw.simps(4)[of m n ?k j "j - 1"] have "fw m n ?k j j = fw_upd (fw m n ?k j (j -1)) ?k j j" by simp then have *: "fw m n ?k j j j j ≤ fw m n ?k j (j -1) j ?k + fw m n ?k j (j -1) ?k j" by (simp add: fw_upd_def upd_def) have "j - 1 < n" using ‹j ≤ n› False by auto then have "fw m n ?k j (j -1) j ?k ≤ fw m n (?k - 1) n n j ?k" using fw_Suc[of j n ?k j "j - 1" m "?k - 1"] ‹j ≤ n› ‹?k ≤ n› ‹?k > 0› by auto moreover have "fw m n ?k j (j -1) ?k j ≤ fw m n (?k - 1) n n ?k j" using fw_Suc[of ?k n j j "j - 1" m "?k - 1"] ‹j ≤ n› ‹?k ≤ n› ‹?k > 0› by auto ultimately have "fw m n ?k j j j j ≤ fw m n (?k - 1) n n j ?k + fw m n (?k - 1) n n ?k j" using * add_mono by fastforce then show ?thesis by auto qed with neg have "fw m n ?k j j j j < 𝟭" by auto moreover have "fw m n n n n j j ≤ fw m n ?k j j j j" using fw_invariant ‹j≤n› ‹?k ≤ n› by auto ultimately have "fw m n n n n j j < 𝟭" using neg by auto with ‹j≤n› have ?thesis by auto } moreover { assume "?k = 0" with cyc(2,4) have "xs = [] ∨ xs = [0]" apply safe apply (case_tac xs) apply fastforce apply (rename_tac ys) apply (case_tac ys) apply auto done then have ?thesis proof assume "xs = []" with cyc have "m j j < 𝟭" by auto with fw_mono[of n n n j j m n] ‹j ≤ n› have "fw m n n n n j j < 𝟭" by auto with ‹j ≤ n› show ?thesis by auto next assume xs: "xs = [0]" with cyc have "m j 0 + m 0 j < 𝟭" by auto then have "fw m n 0 j j j j < 𝟭" proof (cases "j = 0", goal_cases) case 1 have "m j j < 𝟭" proof (rule ccontr) assume "¬ m j j < 𝟭" with 1 have "m 0 0 ≥ 𝟭" by simp with add_mono have "m 0 0 + m 0 0 ≥ 𝟭" by fastforce with 1 show False by simp qed with fw_mono[of j n j j j m 0] ‹j ≤ n› show ?thesis by auto next case 2 with fw.simps(4)[of m n 0 j "j - 1"] have "fw m n 0 j j = fw_upd (fw m n 0 j (j - 1)) 0 j j" by simp then have "fw m n 0 j j j j ≤ fw m n 0 j (j - 1) j 0 + fw m n 0 j (j - 1) 0 j" by (simp add: fw_upd_def upd_def) also have "… ≤ m j 0 + m 0 j" using ‹j ≤ n› add_mono fw_mono by auto finally show ?thesis using 2 by auto qed then have "fw m n 0 n n j j < 𝟭" by (metis cyc(1) less_or_eq_imp_le single_iteration_inv) with fw_invariant[of 0 n n n n n n m j j] ‹j ≤ n› have "fw m n n n n j j < 𝟭" by auto with ‹j ≤ n› show ?thesis by blast qed } ultimately show ?thesis by auto qed end (* End of local class context *) end (* End of theory *)

# Theory Timed_Automata

theory Timed_Automata imports Main begin chapter ‹Basic Definitions and Semantics› section ‹Time› class time = linordered_ab_group_add + assumes dense: "x < y ⟹ ∃z. x < z ∧ z < y" assumes non_trivial: "∃ x. x ≠ 0" begin lemma non_trivial_neg: "∃ x. x < 0" proof - from non_trivial obtain x where "x ≠ 0" by auto then show ?thesis proof (cases "x < 0", auto, goal_cases) case 1 then have "x > 0" by auto then have "(-x) < 0" by auto then show ?case by blast qed qed end datatype ('c, 't :: time) cconstraint = AND "('c, 't) cconstraint" "('c, 't) cconstraint" | LT 'c 't | LE 'c 't | EQ 'c 't | GT 'c 't | GE 'c 't section ‹Syntactic Definition› text ‹ For an informal description of timed automata we refer to Bengtsson and Yi \cite{BengtssonY03}. We define a timed automaton ‹A› › type_synonym ('c, 'time, 's) invassn = "'s ⇒ ('c, 'time) cconstraint" type_synonym ('a, 'c, 'time, 's) transition = "'s * ('c, 'time) cconstraint * 'a * 'c list * 's" type_synonym ('a, 'c, 'time, 's) ta = "('a, 'c, 'time, 's) transition set * ('c, 'time, 's) invassn" definition trans_of :: "('a, 'c, 'time, 's) ta ⇒ ('a, 'c, 'time, 's) transition set" where "trans_of ≡ fst" definition inv_of :: "('a, 'c, 'time, 's) ta ⇒ ('c, 'time, 's) invassn" where "inv_of ≡ snd" abbreviation transition :: "('a, 'c, 'time, 's) ta ⇒ 's ⇒ ('c, 'time) cconstraint ⇒ 'a ⇒ 'c list ⇒ 's ⇒ bool" ("_ ⊢ _ ⟶⇗_,_,_⇖ _" [61,61,61,61,61,61] 61) where "(A ⊢ l ⟶⇗^{g,a,r}⇖ l') ≡ (l,g,a,r,l') ∈ trans_of A" subsection ‹Collecting Information About Clocks› fun collect_clks :: "('c, 't :: time) cconstraint ⇒ 'c set" where "collect_clks (AND cc1 cc2) = collect_clks cc1 ∪ collect_clks cc2" | "collect_clks (LT c _) = {c}" | "collect_clks (LE c _) = {c}" | "collect_clks (EQ c _) = {c}" | "collect_clks (GE c _) = {c}" | "collect_clks (GT c _) = {c}" fun collect_clock_pairs :: "('c, 't :: time) cconstraint ⇒ ('c * 't) set" where "collect_clock_pairs (LT x m) = {(x, m)}" | "collect_clock_pairs (LE x m) = {(x, m)}" | "collect_clock_pairs (EQ x m) = {(x, m)}" | "collect_clock_pairs (GE x m) = {(x, m)}" | "collect_clock_pairs (GT x m) = {(x, m)}" | "collect_clock_pairs (AND cc1 cc2) = (collect_clock_pairs cc1 ∪ collect_clock_pairs cc2)" definition collect_clkt :: "('a, 'c, 't::time, 's) transition set ⇒ ('c *'t) set" where "collect_clkt S = ⋃ {collect_clock_pairs (fst (snd t)) | t . t ∈ S}" definition collect_clki :: "('c, 't :: time, 's) invassn ⇒ ('c *'t) set" where "collect_clki I = ⋃ {collect_clock_pairs (I x) | x. True}" definition clkp_set :: "('a, 'c, 't :: time, 's) ta ⇒ ('c *'t) set" where "clkp_set A = collect_clki (inv_of A) ∪ collect_clkt (trans_of A)" definition collect_clkvt :: "('a, 'c, 't::time, 's) transition set ⇒ 'c set" where "collect_clkvt S = ⋃ {set ((fst o snd o snd o snd) t) | t . t ∈ S}" abbreviation clk_set where "clk_set A ≡ fst ` clkp_set A ∪ collect_clkvt (trans_of A)" (* We don not need this here but most other theories will make use of this predicate *) inductive valid_abstraction where "⟦∀(x,m) ∈ clkp_set A. m ≤ k x ∧ x ∈ X ∧ m ∈ ℕ; collect_clkvt (trans_of A) ⊆ X; finite X⟧ ⟹ valid_abstraction A X k" section ‹Operational Semantics› type_synonym ('c, 't) cval = "'c ⇒ 't" definition cval_add :: "('c,'t) cval ⇒ 't::time ⇒ ('c,'t) cval" (infixr "⊕" 64) where "u ⊕ d = (λ x. u x + d)" inductive clock_val :: "('c, 't) cval ⇒ ('c, 't::time) cconstraint ⇒ bool" ("_ ⊢ _" [62, 62] 62) where "⟦u ⊢ cc1; u ⊢ cc2⟧ ⟹ u ⊢ AND cc1 cc2" | "⟦u c < d⟧ ⟹ u ⊢ LT c d" | "⟦u c ≤ d⟧ ⟹ u ⊢ LE c d" | "⟦u c = d⟧ ⟹ u ⊢ EQ c d" | "⟦u c ≥ d⟧ ⟹ u ⊢ GE c d" | "⟦u c > d⟧ ⟹ u ⊢ GT c d" declare clock_val.intros[intro] inductive_cases[elim!]: "u ⊢ AND cc1 cc2" inductive_cases[elim!]: "u ⊢ LT c d" inductive_cases[elim!]: "u ⊢ LE c d" inductive_cases[elim!]: "u ⊢ EQ c d" inductive_cases[elim!]: "u ⊢ GE c d" inductive_cases[elim!]: "u ⊢ GT c d" fun clock_set :: "'c list ⇒ 't::time ⇒ ('c,'t) cval ⇒ ('c,'t) cval" where "clock_set [] _ u = u" | "clock_set (c#cs) t u = (clock_set cs t u)(c:=t)" abbreviation clock_set_abbrv :: "'c list ⇒ 't::time ⇒ ('c,'t) cval ⇒ ('c,'t) cval" ("[_→_]_" [65,65,65] 65) where "[r → t]u ≡ clock_set r t u" inductive step_t :: "('a, 'c, 't, 's) ta ⇒ 's ⇒ ('c, 't) cval ⇒ ('t::time) ⇒ 's ⇒ ('c, 't) cval ⇒ bool" ("_ ⊢ ⟨_, _⟩ →⇗_⇖ ⟨_, _⟩" [61,61,61] 61) where "⟦u ⊢ inv_of A l; u ⊕ d ⊢ inv_of A l; d ≥ 0⟧ ⟹ A ⊢ ⟨l, u⟩ →⇗^{d}⇖ ⟨l, u ⊕ d⟩" declare step_t.intros[intro!] inductive_cases[elim!]: "A ⊢ ⟨l, u⟩ →⇗^{d}⇖ ⟨l',u'⟩" lemma step_t_determinacy1: "A ⊢ ⟨l, u⟩ →⇗^{d}⇖ ⟨l',u'⟩ ⟹ A ⊢ ⟨l, u⟩ →⇗^{d}⇖ ⟨l'',u''⟩ ⟹ l' = l''" by auto lemma step_t_determinacy2: "A ⊢ ⟨l, u⟩ →⇗^{d}⇖ ⟨l',u'⟩ ⟹ A ⊢ ⟨l, u⟩ →⇗^{d}⇖ ⟨l'',u''⟩ ⟹ u' = u''" by auto lemma step_t_cont1: "d ≥ 0 ⟹ e ≥ 0 ⟹ A ⊢ ⟨l, u⟩ →⇗^{d}⇖ ⟨l',u'⟩ ⟹ A ⊢ ⟨l', u'⟩ →⇗^{e}⇖ ⟨l'',u''⟩ ⟹ A ⊢ ⟨l, u⟩ →⇗^{d+e}⇖ ⟨l'',u''⟩" proof - assume A: "d ≥ 0" "e ≥ 0" "A ⊢ ⟨l, u⟩ →⇗^{d}⇖ ⟨l',u'⟩" "A ⊢ ⟨l', u'⟩ →⇗^{e}⇖ ⟨l'',u''⟩" hence "u' = (u ⊕ d)" "u'' = (u' ⊕ e)" by auto hence "u'' = (u ⊕ (d + e))" unfolding cval_add_def by auto with A show ?thesis by auto qed inductive step_a :: "('a, 'c, 't, 's) ta ⇒ 's ⇒ ('c, ('t::time)) cval ⇒ 'a ⇒ 's ⇒ ('c, 't) cval ⇒ bool" ("_ ⊢ ⟨_, _⟩ →⇘_⇙ ⟨_, _⟩" [61,61,61] 61) where "⟦A ⊢ l ⟶⇗^{g,a,r}⇖ l'; u ⊢ g; u' ⊢ inv_of A l'; u' = [r → 0]u⟧ ⟹ (A ⊢ ⟨l, u⟩ →⇘_{a}⇙ ⟨l', u'⟩)" inductive step :: "('a, 'c, 't, 's) ta ⇒ 's ⇒ ('c, ('t::time)) cval ⇒ 's ⇒ ('c, 't) cval ⇒ bool" ("_ ⊢ ⟨_, _⟩ → ⟨_,_⟩" [61,61,61] 61) where step_a: "A ⊢ ⟨l, u⟩ →⇘_{a}⇙ ⟨l',u'⟩ ⟹ (A ⊢ ⟨l, u⟩ → ⟨l',u'⟩)" | step_t: "A ⊢ ⟨l, u⟩ →⇗^{d}⇖ ⟨l',u'⟩ ⟹ (A ⊢ ⟨l, u⟩ → ⟨l',u'⟩)" inductive_cases[elim!]: "A ⊢ ⟨l, u⟩ → ⟨l',u'⟩" declare step.intros[intro] inductive steps :: "('a, 'c, 't, 's) ta ⇒ 's ⇒ ('c, ('t::time)) cval ⇒ 's ⇒ ('c, 't) cval ⇒ bool" ("_ ⊢ ⟨_, _⟩ →* ⟨_, _⟩" [61,61,61] 61) where refl: "A ⊢ ⟨l, u⟩ →* ⟨l, u⟩" | step: "A ⊢ ⟨l, u⟩ → ⟨l', u'⟩ ⟹ A ⊢ ⟨l', u'⟩ →* ⟨l'', u''⟩ ⟹ A ⊢ ⟨l, u⟩ →* ⟨l'', u''⟩" declare steps.intros[intro] section ‹Zone Semantics› type_synonym ('c, 't) zone = "('c, 't) cval set" definition zone_delay :: "('c, ('t::time)) zone ⇒ ('c, 't) zone" ("_⇧^{↑}" [71] 71) where "Z⇧^{↑}= {u ⊕ d|u d. u ∈ Z ∧ d ≥ (0::'t)}" definition zone_set :: "('c, 't::time) zone ⇒ 'c list ⇒ ('c, 't) zone" ("_⇘_ → 0⇙" [71] 71) where "zone_set Z r = {[r → (0::'t)]u | u . u ∈ Z}" inductive step_z :: "('a, 'c, 't, 's) ta ⇒ 's ⇒ ('c, ('t::time)) zone ⇒ 's ⇒ ('c, 't) zone ⇒ bool" ("_ ⊢ ⟨_, _⟩ ↝ ⟨_, _⟩" [61,61,61] 61) where step_t_z: "A ⊢ ⟨l, Z⟩ ↝ ⟨l, (Z ∩ {u. u ⊢ inv_of A l})⇧^{↑}∩ {u. u ⊢ inv_of A l}⟩" | step_a_z: "⟦A ⊢ l ⟶⇗^{g,a,r}⇖ l'⟧ ⟹ (A ⊢ ⟨l, Z⟩ ↝ ⟨l', zone_set (Z ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}⟩ )" inductive_cases[elim!]: "A ⊢ ⟨l, u⟩ ↝ ⟨l', u'⟩" declare step_z.intros[intro] lemma step_z_sound: "A ⊢ ⟨l, Z⟩ ↝ ⟨l',Z'⟩ ⟹ (∀ u' ∈ Z'. ∃ u ∈ Z. A ⊢ ⟨l, u⟩ → ⟨l',u'⟩)" proof (induction rule: step_z.induct, goal_cases) case 1 thus ?case unfolding zone_delay_def by blast next case (2 A l g a r l' Z) show ?case proof fix u' assume "u' ∈ zone_set (Z ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}" then obtain u where "u ⊢ g" "u' ⊢ inv_of A l'" "u' = [r→0]u" "u ∈ Z" unfolding zone_set_def by auto with step_a.intros[OF 2 this(1-3)] show "∃u∈Z. A ⊢ ⟨l, u⟩ → ⟨l',u'⟩" by fast qed qed lemma step_z_complete: "A ⊢ ⟨l, u⟩ → ⟨l', u'⟩ ⟹ u ∈ Z ⟹ ∃ Z'. A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩ ∧ u' ∈ Z'" proof (induction rule: step.induct, goal_cases) case (1 A l u a l' u') then obtain g r where u': "u' = [r→0]u" "A ⊢ l ⟶⇗^{g,a,r}⇖ l'" "u ⊢ g" "[r→0]u ⊢ inv_of A l'" by (cases rule: step_a.cases) auto hence "u' ∈ zone_set (Z ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}" unfolding zone_set_def using ‹u ∈ Z› by blast with u'(1,2) show ?case by blast next case (2 A l u d l' u') hence u': "u' = (u ⊕ d)" "u ⊢ inv_of A l" "u ⊕ d ⊢ inv_of A l" "0 ≤ d" and "l = l'" by auto with u' ‹u ∈ Z› have "u' ∈ {u'' ⊕ d |u'' d. u'' ∈ Z ∩ {u. u ⊢ inv_of A l} ∧ 0 ≤ d} ∩ {u. u ⊢ inv_of A l}" by fastforce thus ?case using ‹l = l'› step_t_z[unfolded zone_delay_def, of A l] by blast qed text ‹ Corresponds to version in old papers -- not strong enough for inductive proof over transitive closure relation. › lemma step_z_complete1: "A ⊢ ⟨l, u⟩ → ⟨l', u'⟩ ⟹ ∃ Z. A ⊢ ⟨l, {u}⟩ ↝ ⟨l', Z⟩ ∧ u' ∈ Z" proof (induction rule: step.induct, goal_cases) case (1 A l u a l' u') then obtain g r where u': "u' = [r→0]u" "A ⊢ l ⟶⇗^{g,a,r}⇖ l'" "u ⊢ g" "[r→0]u ⊢ inv_of A l'" by (cases rule: step_a.cases) auto hence "{[r→0]u} = zone_set ({u} ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}" unfolding zone_set_def by blast with u'(1,2) show ?case by auto next case (2 A l u d l' u') hence u': "u' = (u ⊕ d)" "u ⊢ inv_of A l" "u ⊕ d ⊢ inv_of A l" "0 ≤ d" and "l = l'" by auto hence "{u} = {u} ∩ {u''. u'' ⊢ inv_of A l}" by fastforce with u'(1) have "{u'} = {u'' ⊕ d |u''. u'' ∈ {u} ∩ {u''. u'' ⊢ inv_of A l}}" by fastforce with u' have "u' ∈ {u'' ⊕ d |u'' d. u'' ∈ {u} ∩ {u. u ⊢ inv_of A l} ∧ 0 ≤ d} ∩ {u. u ⊢ inv_of A l}" by fastforce thus ?case using ‹l = l'› step_t_z[unfolded zone_delay_def, of A l "{u}"] by blast qed text ‹ Easier proof. › lemma step_z_complete2: "A ⊢ ⟨l, u⟩ → ⟨l', u'⟩ ⟹ ∃ Z. A ⊢ ⟨l, {u}⟩ ↝ ⟨l', Z⟩ ∧ u' ∈ Z" using step_z_complete by fast inductive steps_z :: "('a, 'c, 't, 's) ta ⇒ 's ⇒ ('c, ('t::time)) zone ⇒ 's ⇒ ('c, 't) zone ⇒ bool" ("_ ⊢ ⟨_, _⟩ ↝* ⟨_, _⟩" [61,61,61] 61) where refl: "A ⊢ ⟨l, Z⟩ ↝* ⟨l, Z⟩" | step: "A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩ ⟹ A ⊢ ⟨l', Z'⟩ ↝* ⟨l'', Z''⟩ ⟹ A ⊢ ⟨l, Z⟩ ↝* ⟨l'', Z''⟩" declare steps_z.intros[intro] lemma steps_z_sound: "A ⊢ ⟨l, Z⟩ ↝* ⟨l', Z'⟩ ⟹ u' ∈ Z' ⟹ ∃ u ∈ Z. A ⊢ ⟨l, u⟩ →* ⟨l', u'⟩" proof (induction A l _ l' _ arbitrary: rule: steps_z.induct, goal_cases) case refl thus ?case by fast next case (step A l Z l' Z' l'' Z'') then obtain u'' where u'': "A ⊢ ⟨l', u''⟩ →* ⟨l'',u'⟩" "u'' ∈ Z'" by auto then obtain u where "u ∈ Z" "A ⊢ ⟨l, u⟩ → ⟨l',u''⟩" using step_z_sound[OF step(1)] by blast with u'' show ?case by blast qed lemma steps_z_complete: "A ⊢ ⟨l, u⟩ →* ⟨l', u'⟩ ⟹ u ∈ Z ⟹ ∃ Z'. A ⊢ ⟨l, Z⟩ ↝* ⟨l', Z'⟩ ∧ u' ∈ Z'" proof (induction arbitrary: Z rule: steps.induct) case refl thus ?case by auto next case (step A l u l' u' l'' u'' Z) from step_z_complete[OF this(1,4)] obtain Z' where Z': "A ⊢ ⟨l, Z⟩ ↝ ⟨l',Z'⟩" "u' ∈ Z'" by auto then obtain Z'' where "A ⊢ ⟨l', Z'⟩ ↝* ⟨l'',Z''⟩" "u'' ∈ Z''" using step by metis with Z' show ?case by blast qed end

# Theory DBM

theory DBM imports Floyd_Warshall Timed_Automata begin chapter ‹Difference Bound Matrices› section ‹Definitions› text ‹ Difference Bound Matrices (DBMs) constrain differences of clocks (or more precisely, the difference of values assigned to individual clocks by a valuation). The possible constraints are given by the following datatype: › datatype ('t::time) DBMEntry = Le 't | Lt 't | INF ("∞") text ‹\noindent This yields a simple definition of DBMs:› type_synonym 't DBM = "nat ⇒ nat ⇒ 't DBMEntry" text ‹\noindent To relate clocks with rows and columns of a DBM, we use a clock numbering ‹v› of type @{typ "'c ⇒ nat"} to map clocks to indices. DBMs will regularly be accompanied by a natural number $n$, which designates the number of clocks constrained by the matrix. To be able to represent the full set of clock constraints with DBMs, we add an imaginary clock ‹𝟬›, which shall be assigned to 0 in every valuation. In the following predicate we explicitly keep track of ‹𝟬›. › inductive dbm_entry_val :: "('c, 't) cval ⇒ 'c option ⇒ 'c option ⇒ ('t::time) DBMEntry ⇒ bool" where "u r ≤ d ⟹ dbm_entry_val u (Some r) None (Le d)" | "-u c ≤ d ⟹ dbm_entry_val u None (Some c) (Le d)" | "u r < d ⟹ dbm_entry_val u (Some r) None (Lt d)" | "-u c < d ⟹ dbm_entry_val u None (Some c) (Lt d)" | "u r - u c ≤ d ⟹ dbm_entry_val u (Some r) (Some c) (Le d)" | "u r - u c < d ⟹ dbm_entry_val u (Some r) (Some c) (Lt d)" | "dbm_entry_val _ _ _ ∞" declare dbm_entry_val.intros[intro] inductive_cases[elim!]: "dbm_entry_val u None (Some c) (Le d)" inductive_cases[elim!]: "dbm_entry_val u (Some c) None (Le d)" inductive_cases[elim!]: "dbm_entry_val u None (Some c) (Lt d)" inductive_cases[elim!]: "dbm_entry_val u (Some c) None (Lt d)" inductive_cases[elim!]: "dbm_entry_val u (Some r) (Some c) (Le d)" inductive_cases[elim!]: "dbm_entry_val u (Some r) (Some c) (Lt d)" fun dbm_entry_bound :: "('t::time) DBMEntry ⇒ 't" where "dbm_entry_bound (Le t) = t" | "dbm_entry_bound (Lt t) = t" | "dbm_entry_bound ∞ = 0" inductive dbm_lt :: "('t::time) DBMEntry ⇒ 't DBMEntry ⇒ bool" ("_ ≺ _" [51, 51] 50) where "dbm_lt (Lt _) ∞" | "dbm_lt (Le _) ∞" | "a < b ⟹ dbm_lt (Le a) (Le b)" | "a < b ⟹ dbm_lt (Le a) (Lt b)" | "a ≤ b ⟹ dbm_lt (Lt a) (Le b)" | "a < b ⟹ dbm_lt (Lt a) (Lt b)" declare dbm_lt.intros[intro] definition dbm_le :: "('t::time) DBMEntry ⇒ 't DBMEntry ⇒ bool" ("_ ≼ _" [51, 51] 50) where "dbm_le a b ≡ (a ≺ b) ∨ a = b" text ‹ Now a valuation is contained in the zone represented by a DBM if it fulfills all individual constraints: › definition DBM_val_bounded :: "('c ⇒ nat) ⇒ ('c, 't) cval ⇒ ('t::time) DBM ⇒ nat ⇒ bool" where "DBM_val_bounded v u m n ≡ Le 0 ≼ m 0 0 ∧ (∀ c. v c ≤ n ⟶ (dbm_entry_val u None (Some c) (m 0 (v c)) ∧ dbm_entry_val u (Some c) None (m (v c) 0))) ∧ (∀ c1 c2. v c1 ≤ n ∧ v c2 ≤ n ⟶ dbm_entry_val u (Some c1) (Some c2) (m (v c1) (v c2)))" abbreviation DBM_val_bounded_abbrev :: "('c, 't) cval ⇒ ('c ⇒ nat) ⇒ nat ⇒ ('t::time) DBM ⇒ bool" ("_ ⊢⇘_,_⇙ _") where "u ⊢⇘_{v,n}⇙ M ≡ DBM_val_bounded v u M n" abbreviation "dmin a b ≡ if a ≺ b then a else b" lemma dbm_le_dbm_min: "a ≼ b ⟹ a = dmin a b" unfolding dbm_le_def by auto lemma dbm_lt_asym: assumes "e ≺ f" shows "~ f ≺ e" using assms proof (safe, cases e f rule: dbm_lt.cases, goal_cases) case 1 from this(2) show ?case using 1(3-) by (cases f e rule: dbm_lt.cases) auto next case 2 from this(2) show ?case using 2(3-) by (cases f e rule: dbm_lt.cases) auto next case 3 from this(2) show ?case using 3(3-) by (cases f e rule: dbm_lt.cases) auto next case 4 from this(2) show ?case using 4(3-) by (cases f e rule: dbm_lt.cases) auto next case 5 from this(2) show ?case using 5(3-) by (cases f e rule: dbm_lt.cases) auto next case 6 from this(2) show ?case using 6(3-) by (cases f e rule: dbm_lt.cases) auto qed lemma dbm_le_dbm_min2: "a ≼ b ⟹ a = dmin b a" using dbm_lt_asym by (auto simp: dbm_le_def) lemma dmb_le_dbm_entry_bound_inf: "a ≼ b ⟹ a = ∞ ⟹ b = ∞" apply (auto simp: dbm_le_def) apply (cases rule: dbm_lt.cases) by auto lemma dbm_not_lt_eq: "¬ a ≺ b ⟹ ¬ b ≺ a ⟹ a = b" apply (cases a) apply (cases b, fastforce+)+ done lemma dbm_not_lt_impl: "¬ a ≺ b ⟹ b ≺ a ∨ a = b" using dbm_not_lt_eq by auto lemma "dmin a b = dmin b a" proof (cases "a ≺ b") case True thus ?thesis by (simp add: dbm_lt_asym) next case False thus ?thesis by (simp add: dbm_not_lt_eq) qed lemma dbm_lt_trans: "a ≺ b ⟹ b ≺ c ⟹ a ≺ c" proof (cases a b rule: dbm_lt.cases, goal_cases) case 1 thus ?case by simp next case 2 from this(2-) show ?case by (cases rule: dbm_lt.cases) simp+ next case 3 from this(2-) show ?case by (cases rule: dbm_lt.cases) simp+ next case 4 from this(2-) show ?case by (cases rule: dbm_lt.cases) auto next case 5 from this(2-) show ?case by (cases rule: dbm_lt.cases) auto next case 6 from this(2-) show ?case by (cases rule: dbm_lt.cases) auto next case 7 from this(2-) show ?case by (cases rule: dbm_lt.cases) auto qed lemma aux_3: "¬ a ≺ b ⟹ ¬ b ≺ c ⟹ a ≺ c ⟹ c = a" proof goal_cases case 1 thus ?case proof (cases "c ≺ b") case True with ‹a ≺ c› have "a ≺ b" by (rule dbm_lt_trans) thus ?thesis using 1 by auto next case False thus ?thesis using dbm_not_lt_eq 1 by auto qed qed inductive_cases[elim!]: "∞ ≺ x" lemma dbm_lt_asymmetric[simp]: "x ≺ y ⟹ y ≺ x ⟹ False" by (cases x y rule: dbm_lt.cases) (auto elim: dbm_lt.cases) lemma le_dbm_le: "Le a ≼ Le b ⟹ a ≤ b" unfolding dbm_le_def by (auto elim: dbm_lt.cases) lemma le_dbm_lt: "Le a ≼ Lt b ⟹ a < b" unfolding dbm_le_def by (auto elim: dbm_lt.cases) lemma lt_dbm_le: "Lt a ≼ Le b ⟹ a ≤ b" unfolding dbm_le_def by (auto elim: dbm_lt.cases) lemma lt_dbm_lt: "Lt a ≼ Lt b ⟹ a ≤ b" unfolding dbm_le_def by (auto elim: dbm_lt.cases) lemma not_dbm_le_le_impl: "¬ Le a ≺ Le b ⟹ a ≥ b" by (metis dbm_lt.intros(3) not_less) lemma not_dbm_lt_le_impl: "¬ Lt a ≺ Le b ⟹ a > b" by (metis dbm_lt.intros(5) not_less) lemma not_dbm_lt_lt_impl: "¬ Lt a ≺ Lt b ⟹ a ≥ b" by (metis dbm_lt.intros(6) not_less) lemma not_dbm_le_lt_impl: "¬ Le a ≺ Lt b ⟹ a ≥ b" by (metis dbm_lt.intros(4) not_less) (*>*) (*<*) fun dbm_add :: "('t::time) DBMEntry ⇒ 't DBMEntry ⇒ 't DBMEntry" (infixl "⊗" 70) where "dbm_add ∞ _ = ∞" | "dbm_add _ ∞ = ∞" | "dbm_add (Le a) (Le b) = (Le (a+b))" | "dbm_add (Le a) (Lt b) = (Lt (a+b))" | "dbm_add (Lt a) (Le b) = (Lt (a+b))" | "dbm_add (Lt a) (Lt b) = (Lt (a+b))" thm dbm_add.simps lemma aux_4: "x ≺ y ⟹ ¬ dbm_add x z ≺ dbm_add y z ⟹ dbm_add x z = dbm_add y z" by (cases x y rule: dbm_lt.cases) ((cases z), auto)+ lemma aux_5: "¬ x ≺ y ⟹ dbm_add x z ≺ dbm_add y z ⟹ dbm_add y z = dbm_add x z" proof - assume lt: "dbm_add x z ≺ dbm_add y z" "¬ x ≺ y" hence "x = y ∨ y ≺ x" by (auto simp: dbm_not_lt_eq) thus ?thesis proof assume "x = y" thus ?thesis by simp next assume "y ≺ x" thus ?thesis proof (cases y x rule: dbm_lt.cases, goal_cases) case 1 thus ?case using lt by auto next case 2 thus ?case using lt by auto next case 3 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+ next case 4 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+ next case 5 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+ next case 6 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+ qed qed qed lemma aux_42: "x ≺ y ⟹ ¬ dbm_add z x ≺ dbm_add z y ⟹ dbm_add z x = dbm_add z y" by (cases x y rule: dbm_lt.cases) ((cases z), auto)+ lemma aux_52: "¬ x ≺ y ⟹ dbm_add z x ≺ dbm_add z y ⟹ dbm_add z y = dbm_add z x" proof - assume lt: "dbm_add z x ≺ dbm_add z y" "¬ x ≺ y" hence "x = y ∨ y ≺ x" by (auto simp: dbm_not_lt_eq) thus ?thesis proof assume "x = y" thus ?thesis by simp next assume "y ≺ x" thus ?thesis proof (cases y x rule: dbm_lt.cases, goal_cases) case 1 thus ?case using lt by (cases z) fastforce+ next case 2 thus ?case using lt by (cases z) fastforce+ next case 3 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+ next case 4 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+ next case 5 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+ next case 6 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+ qed qed qed lemma dbm_add_not_inf: "a ≠ ∞ ⟹ b ≠ ∞ ⟹ dbm_add a b ≠ ∞" by (cases a, auto, cases b, auto, cases b, auto) lemma dbm_le_not_inf: "a ≼ b ⟹ b ≠ ∞ ⟹ a ≠ ∞" by (cases "a = b") (auto simp: dbm_le_def) section ‹DBM Entries Form a Linearly Ordered Abelian Monoid› instantiation DBMEntry :: (time) linorder begin definition less_eq: "(≤) ≡ dbm_le" definition less: "(<) = dbm_lt" instance proof ((standard; unfold less less_eq), goal_cases) case 1 thus ?case unfolding dbm_le_def using dbm_lt_asymmetric by auto next case 2 thus ?case by (simp add: dbm_le_def) next case 3 thus ?case unfolding dbm_le_def using dbm_lt_trans by auto next case 4 thus ?case unfolding dbm_le_def using dbm_lt_asymmetric by auto next case 5 thus ?case unfolding dbm_le_def using dbm_not_lt_eq by auto qed end instantiation DBMEntry :: (time) linordered_ab_monoid_add begin definition mult: "(+) = dbm_add" definition neutral: "neutral = Le 0" instance proof ((standard; unfold mult neutral less less_eq), goal_cases) case (1 a b c) thus ?case by (cases a; cases b; cases c; auto) next case (2 a b) thus ?case by (cases a; cases b) auto next case (3 a b c) thus ?case unfolding dbm_le_def apply safe apply (rule dbm_lt.cases) apply assumption by (cases c; fastforce)+ next case (4 x) thus ?case by (cases x) auto next case (5 x) thus ?case by (cases x) auto qed end interpretation linordered_monoid: linordered_ab_monoid_add dbm_add dbm_le dbm_lt "Le 0" apply (standard, fold neutral mult less_eq less) using add.commute add.commute add_left_mono assoc by auto lemma Le_Le_dbm_lt_D[dest]: "Le a ≺ Lt b ⟹ a < b" by (cases rule: dbm_lt.cases) auto lemma Le_Lt_dbm_lt_D[dest]: "Le a ≺ Le b ⟹ a < b" by (cases rule: dbm_lt.cases) auto lemma Lt_Le_dbm_lt_D[dest]: "Lt a ≺ Le b ⟹ a ≤ b" by (cases rule: dbm_lt.cases) auto lemma Lt_Lt_dbm_lt_D[dest]: "Lt a ≺ Lt b ⟹ a < b" by (cases rule: dbm_lt.cases) auto lemma Le_le_LeI[intro]: "a ≤ b ⟹ Le a ≤ Le b" unfolding less_eq dbm_le_def by auto lemma Lt_le_LeI[intro]: "a ≤ b ⟹ Lt a ≤ Le b" unfolding less_eq dbm_le_def by auto lemma Lt_le_LtI[intro]: "a ≤ b ⟹ Lt a ≤ Lt b" unfolding less_eq dbm_le_def by auto lemma Le_le_LtI[intro]: "a < b ⟹ Le a ≤ Lt b" unfolding less_eq dbm_le_def by auto lemma Lt_lt_LeI: "x ≤ y ⟹ Lt x < Le y" unfolding less by auto lemma Le_le_LeD[dest]: "Le a ≤ Le b ⟹ a ≤ b" unfolding dbm_le_def less_eq by auto lemma Le_le_LtD[dest]: "Le a ≤ Lt b ⟹ a < b" unfolding dbm_le_def less_eq by auto lemma Lt_le_LeD[dest]: "Lt a ≤ Le b ⟹ a ≤ b" unfolding less_eq dbm_le_def by auto lemma Lt_le_LtD[dest]: "Lt a ≤ Lt b ⟹ a ≤ b" unfolding less_eq dbm_le_def by auto lemma inf_not_le_Le[simp]: "∞ ≤ Le x = False" unfolding less_eq dbm_le_def by auto lemma inf_not_le_Lt[simp]: "∞ ≤ Lt x = False" unfolding less_eq dbm_le_def by auto lemma inf_not_lt[simp]: "∞ ≺ x = False" by auto lemma any_le_inf: "x ≤ ∞" by (metis less_eq dmb_le_dbm_entry_bound_inf le_cases) section ‹Basic Properties of DBMs› subsection ‹DBMs and Length of Paths› lemma dbm_entry_val_add_1: "dbm_entry_val u (Some c) (Some d) a ⟹ dbm_entry_val u (Some d) None b ⟹ dbm_entry_val u (Some c) None (dbm_add a b)" proof (cases a, goal_cases) case 1 thus ?thesis apply (cases b) apply auto using add_mono_thms_linordered_semiring(1) apply fastforce using add_le_less_mono by fastforce next case 2 thus ?thesis apply (cases b) apply auto apply (simp add: dbm_entry_val.intros(3) diff_less_eq less_le_trans) by (metis add_le_less_mono dbm_entry_val.intros(3) diff_add_cancel less_imp_le) next case 3 thus ?thesis by (cases b) auto qed lemma dbm_entry_val_add_2: "dbm_entry_val u None (Some c) a ⟹ dbm_entry_val u (Some c) (Some d) b ⟹ dbm_entry_val u None (Some d) (dbm_add a b)" proof (cases a, goal_cases) case 1 thus ?thesis apply (cases b) apply auto using add_mono_thms_linordered_semiring(1) apply fastforce using add_le_less_mono by fastforce next case 2 thus ?thesis apply (cases b) apply auto using add_mono_thms_linordered_field(3) apply fastforce using add_strict_mono by fastforce next case 3 thus ?thesis by (cases b) auto qed lemma dbm_entry_val_add_3: "dbm_entry_val u (Some c) (Some d) a ⟹ dbm_entry_val u (Some d) (Some e) b ⟹ dbm_entry_val u (Some c) (Some e) (dbm_add a b)" proof (cases a, goal_cases) case 1 thus ?thesis apply (cases b) apply auto using add_mono_thms_linordered_semiring(1) apply fastforce using add_le_less_mono by fastforce next case 2 thus ?thesis apply (cases b) apply auto using add_mono_thms_linordered_field(3) apply fastforce using add_strict_mono by fastforce next case 3 thus ?thesis by (cases b) auto qed lemma dbm_entry_val_add_4: "dbm_entry_val u (Some c) None a ⟹ dbm_entry_val u None (Some d) b ⟹ dbm_entry_val u (Some c) (Some d) (dbm_add a b)" proof (cases a, goal_cases) case 1 thus ?thesis apply (cases b) apply auto using add_mono_thms_linordered_semiring(1) apply fastforce using add_le_less_mono by fastforce next case 2 thus ?thesis apply (cases b) apply auto using add_mono_thms_linordered_field(3) apply fastforce using add_strict_mono by fastforce next case 3 thus ?thesis by (cases b) auto qed no_notation dbm_add (infixl "⊗" 70) lemma DBM_val_bounded_len_1'_aux: assumes "DBM_val_bounded v u m n" "v c ≤ n" "∀ k ∈ set vs. k > 0 ∧ k ≤ n ∧ (∃ c. v c = k)" shows "dbm_entry_val u (Some c) None (len m (v c) 0 vs)" using assms proof (induction vs arbitrary: c) case Nil then show ?case unfolding DBM_val_bounded_def by auto next case (Cons k vs) then obtain c' where c': "k > 0" "k ≤ n" "v c' = k" by auto with Cons have "dbm_entry_val u (Some c') None (len m (v c') 0 vs)" by auto moreover have "dbm_entry_val u (Some c) (Some c') (m (v c) (v c'))" using Cons.prems c' by (auto simp add: DBM_val_bounded_def) ultimately have "dbm_entry_val u (Some c) None (m (v c) (v c') + len m (v c') 0 vs)" using dbm_entry_val_add_1 unfolding mult by fastforce with c' show ?case unfolding DBM_val_bounded_def by simp qed lemma DBM_val_bounded_len_3'_aux: "DBM_val_bounded v u m n ⟹ v c ≤ n ⟹ v d ≤ n ⟹ ∀ k ∈ set vs. k > 0 ∧ k ≤ n ∧ (∃ c. v c = k) ⟹ dbm_entry_val u (Some c) (Some d) (len m (v c) (v d) vs)" proof (induction vs arbitrary: c) case Nil thus ?case unfolding DBM_val_bounded_def by auto next case (Cons k vs) then obtain c' where c': "k > 0" "k ≤ n" "v c' = k" by auto with Cons have "dbm_entry_val u (Some c') (Some d) (len m (v c') (v d) vs)" by auto moreover have "dbm_entry_val u (Some c) (Some c') (m (v c) (v c'))" using Cons.prems c' by (auto simp add: DBM_val_bounded_def) ultimately have "dbm_entry_val u (Some c) (Some d) (m (v c) (v c') + len m (v c') (v d) vs)" using dbm_entry_val_add_3 unfolding mult by fastforce with c' show ?case unfolding DBM_val_bounded_def by simp qed lemma DBM_val_bounded_len_2'_aux: "DBM_val_bounded v u m n ⟹ v c ≤ n ⟹ ∀ k ∈ set vs. k > 0 ∧ k ≤ n ∧ (∃ c. v c = k) ⟹ dbm_entry_val u None (Some c) (len m 0 (v c) vs)" proof (cases vs, goal_cases) case 1 then show ?thesis unfolding DBM_val_bounded_def by auto next case (2 k vs) then obtain c' where c': "k > 0" "k ≤ n" "v c' = k" by auto with 2 have "dbm_entry_val u (Some c') (Some c) (len m (v c') (v c) vs)" using DBM_val_bounded_len_3'_aux by auto moreover have "dbm_entry_val u None (Some c') (m 0 (v c'))" using 2 c' by (auto simp add: DBM_val_bounded_def) ultimately have "dbm_entry_val u None (Some c) (m 0 (v c') + len m (v c') (v c) vs)" using dbm_entry_val_add_2 unfolding mult by fastforce with 2(4) c' show ?case unfolding DBM_val_bounded_def by simp qed lemma cnt_0_D: "cnt x xs = 0 ⟹ x ∉ set xs" apply (induction xs) apply simp apply (rename_tac a xs) apply (case_tac "x = a") by simp+ lemma cnt_at_most_1_D: "cnt x (xs @ x # ys) ≤ 1 ⟹ x ∉ set xs ∧ x ∉ set ys" apply (induction xs) apply auto[] using cnt_0_D apply force apply (rename_tac a xs) apply (case_tac "a = x") apply simp apply simp done lemma nat_list_0 [intro]: "x ∈ set xs ⟹ 0 ∉ set (xs :: nat list) ⟹ x > 0" by (induction xs) auto lemma DBM_val_bounded_len': fixes v defines "vo ≡ λ k. if k = 0 then None else Some (SOME c. v c = k)" assumes "DBM_val_bounded v u m n" "cnt 0 (i # j # vs) ≤ 1" "∀ k ∈ set (i # j # vs). k > 0 ⟶ k ≤ n ∧ (∃ c. v c = k)" shows "dbm_entry_val u (vo i) (vo j) (len m i j vs)" proof - show ?thesis proof (cases "∀ k ∈ set vs. k > 0") case True with assms have *: "∀ k ∈ set vs. k > 0 ∧ k ≤ n ∧ (∃ c. v c = k)" by auto show ?thesis proof (cases "i = 0") case True then have i: "vo i = None" by (simp add: vo_def) show ?thesis proof (cases "j = 0") case True with assms ‹i = 0› show ?thesis by auto next case False with assms obtain c2 where c2: "j ≤ n" "v c2 = j" "vo j = Some c2" unfolding vo_def by (fastforce intro: someI) with ‹i = 0› i DBM_val_bounded_len_2'_aux[OF assms(2) _ *] show ?thesis by auto qed next case False with assms(4) obtain c1 where c1: "i ≤ n" "v c1 = i" "vo i = Some c1" unfolding vo_def by (fastforce intro: someI) show ?thesis proof (cases "j = 0") case True with DBM_val_bounded_len_1'_aux[OF assms(2) _ *] c1 show ?thesis by (auto simp: vo_def) next case False with assms obtain c2 where c2: "j ≤ n" "v c2 = j" "vo j = Some c2" unfolding vo_def by (fastforce intro: someI) with c1 DBM_val_bounded_len_3'_aux[OF assms(2) _ _ *] show ?thesis by auto qed qed next case False then have "∃ k ∈ set vs. k = 0" by auto then obtain us ws where vs: "vs = us @ 0 # ws" by (meson split_list_last) with cnt_at_most_1_D[of 0 "i # j # us"] assms(3) have "0 ∉ set us" "0 ∉ set ws" "i ≠ 0" "j ≠ 0" by auto with vs have vs: "vs = us @ 0 # ws" "∀ k ∈ set us. k > 0" "∀ k ∈ set ws. k > 0" by auto with assms(4) have v: "∀k∈set us. 0 < k ∧ k ≤ n ∧ (∃c. v c = k)" "∀k∈set ws. 0 < k ∧ k ≤ n ∧ (∃c. v c = k)" by auto from ‹i ≠ 0› ‹j ≠ 0› assms obtain c1 c2 where c1: "i ≤ n" "v c1 = i" "vo i = Some c1" and c2: "j ≤ n" "v c2 = j" "vo j = Some c2" unfolding vo_def by (fastforce intro: someI) with dbm_entry_val_add_4 [OF DBM_val_bounded_len_1'_aux[OF assms(2) _ v(1)] DBM_val_bounded_len_2'_aux[OF assms(2) _ v(2)]] have "dbm_entry_val u (Some c1) (Some c2) (dbm_add (len m (v c1) 0 us) (len m 0 (v c2) ws))" by auto moreover from vs have "len m (v c1) (v c2) vs = dbm_add (len m (v c1) 0 us) (len m 0 (v c2) ws)" by (simp add: len_comp mult) ultimately show ?thesis using c1 c2 by auto qed qed lemma DBM_val_bounded_len'1: fixes v assumes "DBM_val_bounded v u m n" "0 ∉ set vs" "v c ≤ n" "∀ k ∈ set vs. k > 0 ⟶ k ≤ n ∧ (∃ c. v c = k)" shows "dbm_entry_val u (Some c) None (len m (v c) 0 vs)" using DBM_val_bounded_len_1'_aux[OF assms(1,3)] assms(2,4) by fastforce lemma DBM_val_bounded_len'2: fixes v assumes "DBM_val_bounded v u m n" "0 ∉ set vs" "v c ≤ n" "∀ k ∈ set vs. k > 0 ⟶ k ≤ n ∧ (∃ c. v c = k)" shows "dbm_entry_val u None (Some c) (len m 0 (v c) vs)" using DBM_val_bounded_len_2'_aux[OF assms(1,3)] assms(2,4) by fastforce lemma DBM_val_bounded_len'3: fixes v assumes "DBM_val_bounded v u m n" "cnt 0 vs ≤ 1" "v c1 ≤ n" "v c2 ≤ n" "∀ k ∈ set vs. k > 0 ⟶ k ≤ n ∧ (∃ c. v c = k)" shows "dbm_entry_val u (Some c1) (Some c2) (len m (v c1) (v c2) vs)" proof - show ?thesis proof (cases "∀ k ∈ set vs. k > 0") case True with assms have "∀ k ∈ set vs. k > 0 ∧ k ≤ n ∧ (∃ c. v c = k)" by auto with DBM_val_bounded_len_3'_aux[OF assms(1,3,4)] show ?thesis by auto next case False then have "∃ k ∈ set vs. k = 0" by auto then obtain us ws where vs: "vs = us @ 0 # ws" by (meson split_list_last) with cnt_at_most_1_D[of 0 "us"] assms(2) have "0 ∉ set us" "0 ∉ set ws" by auto with vs have vs: "vs = us @ 0 # ws" "∀ k ∈ set us. k > 0" "∀ k ∈ set ws. k > 0" by auto with assms(5) have v: "∀k∈set us. 0 < k ∧ k ≤ n ∧ (∃c. v c = k)" "∀k∈set ws. 0 < k ∧ k ≤ n ∧ (∃c. v c = k)" by auto with dbm_entry_val_add_4 [OF DBM_val_bounded_len_1'_aux[OF assms(1,3) v(1)] DBM_val_bounded_len_2'_aux[OF assms(1,4) v(2)]] have "dbm_entry_val u (Some c1) (Some c2) (dbm_add (len m (v c1) 0 us) (len m 0 (v c2) ws))" by auto moreover from vs have "len m (v c1) (v c2) vs = dbm_add (len m (v c1) 0 us) (len m 0 (v c2) ws)" by (simp add: len_comp mult) ultimately show ?thesis by auto qed qed lemma DBM_val_bounded_len'': fixes v defines "vo ≡ λ k. if k = 0 then None else Some (SOME c. v c = k)" assumes "DBM_val_bounded v u m n" "i ≠ 0 ∨ j ≠ 0" "∀ k ∈ set (i # j # vs). k > 0 ⟶ k ≤ n ∧ (∃ c. v c = k)" shows "dbm_entry_val u (vo i) (vo j) (len m i j vs)" using assms proof (induction "length vs" arbitrary: i vs rule: less_induct) case less show ?case proof (cases "∀ k ∈ set vs. k > 0") case True with less.prems have *: "∀ k ∈ set vs. k > 0 ∧ k ≤ n ∧ (∃ c. v c = k)" by auto show ?thesis proof (cases "i = 0") case True then have i: "vo i = None" by (simp add: vo_def) show ?thesis proof (cases "j = 0") case True with less.prems ‹i = 0› show ?thesis by auto next case False with less.prems obtain c2 where c2: "j ≤ n" "v c2 = j" "vo j = Some c2" unfolding vo_def by (fastforce intro: someI) with ‹i = 0› i DBM_val_bounded_len_2'_aux[OF less.prems(1) _ *] show ?thesis by auto qed next case False with less.prems obtain c1 where c1: "i ≤ n" "v c1 = i" "vo i = Some c1" unfolding vo_def by (fastforce intro: someI) show ?thesis proof (cases "j = 0") case True with DBM_val_bounded_len_1'_aux[OF less.prems(1) _ *] c1 show ?thesis by (auto simp: vo_def) next case False with less.prems obtain c2 where c2: "j ≤ n" "v c2 = j" "vo j = Some c2" unfolding vo_def by (fastforce intro: someI) with c1 DBM_val_bounded_len_3'_aux[OF less.prems(1) _ _ *] show ?thesis by auto qed qed next case False then have "∃ us ws. vs = us @ 0 # ws ∧ (∀ k ∈ set us. k > 0)" proof (induction vs) case Nil then show ?case by auto next case (Cons x vs) show ?case proof (cases "x = 0") case True then show ?thesis by fastforce next case False with Cons.prems have "¬ (∀a∈set vs. 0 < a)" by auto from Cons.IH[OF this] obtain us ws where "vs = us @ 0 # ws" "∀a∈set us. 0 < a" by auto with False have "x # vs = (x # us) @ 0 # ws" "∀a∈set (x # us). 0 < a" by auto then show ?thesis by blast qed qed then obtain us ws where vs: "vs = us @ 0 # ws" "∀ k ∈ set us. k > 0" by blast then show ?thesis oops lemma DBM_val_bounded_len_1: "DBM_val_bounded v u m n ⟹ v c ≤ n ⟹ ∀ c ∈ set cs. v c ≤ n ⟹ dbm_entry_val u (Some c) None (len m (v c) 0 (map v cs))" proof (induction cs arbitrary: c) case Nil thus ?case unfolding DBM_val_bounded_def by auto next case (Cons c' cs) hence "dbm_entry_val u (Some c') None (len m (v c') 0 (map v cs))" by auto moreover have "dbm_entry_val u (Some c) (Some c') (m (v c) (v c'))" using Cons.prems by (simp add: DBM_val_bounded_def) ultimately have "dbm_entry_val u (Some c) None (m (v c) (v c') + len m (v c') 0 (map v cs))" using dbm_entry_val_add_1 unfolding mult by fastforce thus ?case unfolding DBM_val_bounded_def by simp qed lemma DBM_val_bounded_len_3: "DBM_val_bounded v u m n ⟹ v c ≤ n ⟹ v d ≤ n ⟹ ∀ c ∈ set cs. v c ≤ n ⟹ dbm_entry_val u (Some c) (Some d) (len m (v c) (v d) (map v cs))" proof (induction cs arbitrary: c) case Nil thus ?case unfolding DBM_val_bounded_def by auto next case (Cons c' cs) hence "dbm_entry_val u (Some c') (Some d) (len m (v c') (v d) (map v cs))" by auto moreover have "dbm_entry_val u (Some c) (Some c') (m (v c) (v c'))" using Cons.prems by (simp add: DBM_val_bounded_def) ultimately have "dbm_entry_val u (Some c) (Some d) (m (v c) (v c') + len m (v c') (v d) (map v cs))" using dbm_entry_val_add_3 unfolding mult by fastforce thus ?case unfolding DBM_val_bounded_def by simp qed lemma DBM_val_bounded_len_2: "DBM_val_bounded v u m n ⟹ v c ≤ n ⟹ ∀ c ∈ set cs. v c ≤ n ⟹ dbm_entry_val u None (Some c) (len m 0 (v c) (map v cs))" proof (cases cs, goal_cases) case 1 thus ?thesis unfolding DBM_val_bounded_def by auto next case (2 c' cs) hence "dbm_entry_val u (Some c') (Some c) (len m (v c') (v c) (map v cs))" using DBM_val_bounded_len_3 by auto moreover have "dbm_entry_val u None (Some c') (m 0 (v c'))" using 2 by (simp add: DBM_val_bounded_def) ultimately have "dbm_entry_val u None (Some c) (m 0 (v c') + len m (v c') (v c) (map v cs))" using dbm_entry_val_add_2 unfolding mult by fastforce thus ?case using 2(4) unfolding DBM_val_bounded_def by simp qed end

# Theory Paths_Cycles

theory Paths_Cycles imports Floyd_Warshall Timed_Automata begin chapter ‹Library for Paths, Arcs and Lengths› lemma length_eq_distinct: assumes "set xs = set ys" "distinct xs" "length xs = length ys" shows "distinct ys" using assms card_distinct distinct_card by fastforce section ‹Arcs› fun arcs :: "nat ⇒ nat ⇒ nat list ⇒ (nat * nat) list" where "arcs a b [] = [(a,b)]" | "arcs a b (x # xs) = (a, x) # arcs x b xs" definition arcs' :: "nat list ⇒ (nat * nat) set" where "arcs' xs = set (arcs (hd xs) (last xs) (butlast (tl xs)))" lemma arcs'_decomp: "length xs > 1 ⟹ (i, j) ∈ arcs' xs ⟹ ∃ zs ys. xs = zs @ i # j # ys" proof (induction xs) case Nil thus ?case by auto next case (Cons x xs) then have "length xs > 0" by auto then obtain y ys where xs: "xs = y # ys" by (metis Suc_length_conv less_imp_Suc_add) show ?case proof (cases "(i, j) = (x, y)") case True with xs have "x # xs = [] @ i # j # ys" by simp then show ?thesis by auto next case False then show ?thesis proof (cases "length ys > 0", goal_cases) case 2 then have "ys = []" by auto then have "arcs' (x#xs) = {(x,y)}" using xs by (auto simp add: arcs'_def) with Cons.prems(2) 2(1) show ?case by auto next case True with xs Cons.prems(2) False have "(i, j) ∈ arcs' xs" by (auto simp add: arcs'_def) with Cons.IH[OF _ this] True xs obtain zs ys where "xs = zs @ i # j # ys" by auto then have "x # xs = (x # zs) @ i # j # ys" by simp then show ?thesis by blast qed qed qed lemma arcs_decomp_tail: "arcs j l (ys @ [i]) = arcs j i ys @ [(i, l)]" by (induction ys arbitrary: j) auto lemma arcs_decomp: "xs = ys @ y # zs ⟹ arcs x z xs = arcs x y ys @ arcs y z zs" by (induction ys arbitrary: x xs) simp+ lemma distinct_arcs_ex: "distinct xs ⟹ i ∉ set xs ⟹ xs ≠ [] ⟹ ∃ a b. a ≠ x ∧ (a,b) ∈ set (arcs i j xs)" apply (induction xs arbitrary: i) apply simp apply (rename_tac a xs i) apply (case_tac xs) apply simp apply metis by auto lemma cycle_rotate_2_aux: "(i, j) ∈ set (arcs a b (xs @ [c])) ⟹ (i,j) ≠ (c,b) ⟹ (i, j) ∈ set (arcs a c xs)" by (induction xs arbitrary: a) auto lemma arcs_set_elem1: assumes "j ≠ k" "k ∈ set (i # xs)" shows "∃ l. (k, l) ∈ set (arcs i j xs)" using assms by (induction xs arbitrary: i) auto lemma arcs_set_elem2: assumes "i ≠ k" "k ∈ set (j # xs)" shows "∃ l. (l, k) ∈ set (arcs i j xs)" using assms proof (induction xs arbitrary: i) case Nil then show ?case by simp next case (Cons x xs) then show ?case by (cases "k = x") auto qed section ‹Length of Paths› 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