theory DBM_Basics imports DBM Paths_Cycles begin fun get_const where "get_const (Le c) = c" | "get_const (Lt c) = c" | "get_const ∞ = undefined" subsection ‹Discourse on updating DBMs› abbreviation DBM_update :: "('t::time) DBM ⇒ nat ⇒ nat ⇒ ('t DBMEntry) ⇒ ('t::time) DBM" where "DBM_update M m n v ≡ (λ x y. if m = x ∧ n = y then v else M x y)" fun DBM_upd :: "('t::time) DBM ⇒ (nat ⇒ nat ⇒ 't DBMEntry) ⇒ nat ⇒ nat ⇒ nat ⇒ 't DBM" where "DBM_upd M f 0 0 _ = DBM_update M 0 0 (f 0 0)" | "DBM_upd M f (Suc i) 0 n = DBM_update (DBM_upd M f i n n) (Suc i) 0 (f (Suc i) 0)" | "DBM_upd M f i (Suc j) n = DBM_update (DBM_upd M f i j n) i (Suc j) (f i (Suc j))" lemma upd_1: assumes "j ≤ n" shows "DBM_upd M1 f (Suc m) n N (Suc m) j = DBM_upd M1 f (Suc m) j N (Suc m) j" using assms by (induction n) auto lemma upd_2: assumes "i ≤ m" shows "DBM_upd M1 f (Suc m) n N i j = DBM_upd M1 f (Suc m) 0 N i j" using assms proof (induction n) case 0 thus ?case by blast next case (Suc n) thus ?case by simp qed lemma upd_3: assumes "m ≤ N" "n ≤ N" "j ≤ n" "i ≤ m" shows "(DBM_upd M1 f m n N) i j = (DBM_upd M1 f i j N) i j" using assms proof (induction m arbitrary: n i j, goal_cases) case (1 n) thus ?case by (induction n) auto next case (2 m n i j) thus ?case proof (cases "i = Suc m") case True thus ?thesis using upd_1[OF ‹j ≤ n›] by blast next case False with ‹i ≤ Suc m› have "i ≤ m" by auto with upd_2[OF this] have "DBM_upd M1 f (Suc m) n N i j = DBM_upd M1 f m N N i j" by force also have "… = DBM_upd M1 f i j N i j" using False 2 by force finally show ?thesis . qed qed lemma upd_id: assumes "m ≤ N" "n ≤ N" "i ≤ m" "j ≤ n" shows "(DBM_upd M1 f m n N) i j = f i j" proof - from assms upd_3 have "DBM_upd M1 f m n N i j = DBM_upd M1 f i j N i j" by blast also have "… = f i j" by (cases i; cases j; fastforce) finally show ?thesis . qed subsection ‹Zones and DBMs› definition DBM_zone_repr :: "('t::time) DBM ⇒ ('c ⇒ nat) ⇒ nat ⇒ ('c, 't :: time) zone" ("[_]⇘_,_⇙" [72,72,72] 72) where "[M]⇘v,n⇙ = {u . DBM_val_bounded v u M n}" lemma dbm_entry_val_mono_1: "dbm_entry_val u (Some c) (Some c') b ⟹ b ≼ b' ⟹ dbm_entry_val u (Some c) (Some c') b'" proof (induction b, goal_cases) case 1 thus ?case using le_dbm_le le_dbm_lt by (induction b'; fastforce) next case 2 thus ?case using lt_dbm_le lt_dbm_lt by (induction b'; fastforce) next case 3 thus ?case unfolding dbm_le_def by auto qed lemma dbm_entry_val_mono_2: "dbm_entry_val u None (Some c) b ⟹ b ≼ b' ⟹ dbm_entry_val u None (Some c) b'" proof (induction b, goal_cases) case 1 thus ?case using le_dbm_le le_dbm_lt by (induction b'; fastforce) next case 2 thus ?case using lt_dbm_le lt_dbm_lt by (induction b'; fastforce) next case 3 thus ?case unfolding dbm_le_def by auto qed lemma dbm_entry_val_mono_3: "dbm_entry_val u (Some c) None b ⟹ b ≼ b' ⟹ dbm_entry_val u (Some c) None b'" proof (induction b, goal_cases) case 1 thus ?case using le_dbm_le le_dbm_lt by (induction b'; fastforce) next case 2 thus ?case using lt_dbm_le lt_dbm_lt by (induction b'; fastforce) next case 3 thus ?case unfolding dbm_le_def by auto qed lemma DBM_le_subset: "∀ i j. i ≤ n ⟶ j ≤ n ⟶ M i j ≼ M' i j ⟹ u ∈ [M]⇘v,n⇙ ⟹ u ∈ [M']⇘v,n⇙" proof - assume A: "∀i j. i ≤ n ⟶ j ≤ n ⟶ M i j ≼ M' i j" "u ∈ [M]⇘v,n⇙" hence "DBM_val_bounded v u M n" by (simp add: DBM_zone_repr_def) with A(1) have "DBM_val_bounded v u M' n" unfolding DBM_val_bounded_def proof (auto, goal_cases) case 1 from this(1,2) show ?case unfolding less_eq[symmetric] by fastforce next case (2 c) hence "dbm_entry_val u None (Some c) (M 0 (v c))" "M 0 (v c) ≼ M' 0 (v c)" by auto thus ?case using dbm_entry_val_mono_2 by fast next case (3 c) hence "dbm_entry_val u (Some c) None (M (v c) 0)" "M (v c) 0 ≼ M' (v c) 0" by auto thus ?case using dbm_entry_val_mono_3 by fast next case (4 c1 c2) hence "dbm_entry_val u (Some c1) (Some c2) (M (v c1) (v c2))" "M (v c1) (v c2) ≼ M' (v c1) (v c2)" by auto thus ?case using dbm_entry_val_mono_1 by fast qed thus "u ∈ [M']⇘v,n⇙" by (simp add: DBM_zone_repr_def) qed subsection ‹DBMs Without Negative Cycles are Non-Empty› text ‹ We need all of these assumptions for the proof that matrices without negative cycles represent non-negative zones: * Abelian (linearly ordered) monoid * Time is non-trivial * Time is dense › lemmas (in linordered_ab_monoid_add) comm = add.commute lemma sum_gt_neutral_dest': "(a :: (('a :: time) DBMEntry)) ≥ 𝟭 ⟹ a + b > 𝟭 ⟹ ∃ d. Le d ≤ a ∧ Le (-d) ≤ b ∧ d ≥ 0" proof - assume "a + b > 𝟭" "a ≥ 𝟭" show ?thesis proof (cases "b ≥ 𝟭") case True with ‹a ≥ 𝟭› show ?thesis by (auto simp: neutral) next case False hence "b < Le 0" by (auto simp: neutral) with ‹a ≥ 𝟭› ‹a + b > 𝟭› show ?thesis proof (cases a, cases b, auto simp: neutral, goal_cases) case (1 a' b') from 1(2) have "a' + b' > 0" by (auto elim: dbm_lt.cases simp: less mult) hence "b' > -a'" by (metis add.commute diff_0 diff_less_eq) with ‹Le 0 ≤ Le a'› show ?case by (auto simp: dbm_le_def less_eq le_dbm_le) next case (2 a' b') from this(2) have "a' + b' > 0" by (auto elim: dbm_lt.cases simp: less mult) hence "b' > -a'" by (metis add.commute diff_0 diff_less_eq) with ‹Le 0 ≤ Le a'› show ?case by (auto simp: dbm_le_def less_eq le_dbm_le) next case (3 a') thus ?case by (auto simp: dbm_le_def less_eq) next case (4 a') thus ?case proof (cases b, auto, goal_cases) case (1 b') have "b' < 0" using 1(2) by (metis dbm_lt.intros(3) less less_asym neqE) from 1 have "a' + b' > 0" by (auto elim: dbm_lt.cases simp: less mult) then have "-b' < a'" by (metis diff_0 diff_less_eq) with ‹b' < 0› show ?case by (auto simp: dbm_le_def less_eq) next case (2 b') then have A: "b' ≤ 0" "a' > 0" by (auto elim: dbm_lt.cases simp: less less_eq dbm_le_def) show ?case proof (cases "b' = 0") case True from dense[OF A(2)] obtain d where d: "d > 0" "d < a'" by auto then have "Le (-d) < Lt b'" "Le d < Lt a'" unfolding less using True by auto with d(1) show ?thesis by - (rule exI[where x = "d"], auto) next case False with A(1) have *: "- b' > 0" by simp from 2 have "a' + b' > 0" by (auto elim: dbm_lt.cases simp: less mult) then have "-b' < a'" by (metis less_add_same_cancel1 minus_add_cancel minus_less_iff) from dense[OF this] obtain d where d: "d > -b'" "-d < b'" "d < a'" by (auto simp add: minus_less_iff) then have "Le (-d) < Lt b'" "Le d < Lt a'" unfolding less by auto with d(1) * show ?thesis by - (rule exI[where x = "d"], auto, meson d(2) dual_order.order_iff_strict less_trans neg_le_0_iff_le) qed next case 3 thus ?case by (auto simp: dbm_le_def less_eq) qed next case 5 thus ?case proof (cases b, auto, goal_cases) case (1 b') from this(2) have "-b' ≥ 0" by (metis dbm_lt.intros(3) leI less less_asym neg_less_0_iff_less) let ?d = "- b'" have "Le ?d ≤ ∞" "Le (- ?d) ≤ Le b'" by (auto simp: any_le_inf) with ‹-b' ≥ 0› show ?case by auto next case (2 b') then have "b' ≤ 0" by (auto elim: dbm_lt.cases simp: less) from non_trivial_neg obtain e :: 'a where e:"e < 0" by blast let ?d = "- (b' + e)" from e ‹b' ≤ 0› have "Le ?d ≤ ∞" "Le (- ?d) ≤ Lt b'" "b' + e < 0" by (auto simp: dbm_lt.intros(4) less less_imp_le any_le_inf add_nonpos_neg) then have "Le ?d ≤ ∞" "Le (- ?d) ≤ Lt b'" "?d ≥ 0" using less_imp_le neg_0_le_iff_le by blast+ thus ?case by auto qed qed qed qed lemma sum_gt_neutral_dest: "(a :: (('a :: time) DBMEntry)) + b > 𝟭 ⟹ ∃ d. Le d ≤ a ∧ Le (-d) ≤ b" proof - assume A: "a + b > 𝟭" then have A': "b + a > 𝟭" by (simp add: comm) show ?thesis proof (cases "a ≥ 𝟭") case True with A sum_gt_neutral_dest' show ?thesis by auto next case False { assume "b ≤ 𝟭" with False have "a ≤ 𝟭" "b ≤ 𝟭" by auto from add_mono[OF this] have "a + b ≤ 𝟭" by auto with A have False by auto } then have "b ≥ 𝟭" by fastforce with sum_gt_neutral_dest'[OF this A'] show ?thesis by auto qed qed subsection ‹ Negative Cycles in DBMs › lemma DBM_val_bounded_neg_cycle1: fixes i xs assumes bounded: "DBM_val_bounded v u M n" and A:"i ≤ n" "set xs ⊆ {0..n}" "len M i i xs < 𝟭" and surj_on: "∀ k ≤ n. k > 0 ⟶ (∃ c. v c = k)" and at_most: "i ≠ 0" "cnt 0 xs ≤ 1" shows False proof - from A(1) surj_on at_most obtain c where c: "v c = i" by auto with DBM_val_bounded_len'3[OF bounded at_most(2), of c c] A(1,2) surj_on have bounded:"dbm_entry_val u (Some c) (Some c) (len M i i xs)" by force from A(3) have "len M i i xs ≺ Le 0" by (simp add: neutral less) then show False using bounded by (cases rule: dbm_lt.cases) (auto elim: dbm_entry_val.cases) qed lemma cnt_0_I: "x ∉ set xs ⟹ cnt x xs = 0" by (induction xs) auto lemma distinct_cnt: "distinct xs ⟹ cnt x xs ≤ 1" apply (induction xs) apply simp apply (rename_tac a xs) apply (case_tac "x = a") using cnt_0_I by fastforce+ lemma DBM_val_bounded_neg_cycle: fixes i xs assumes bounded: "DBM_val_bounded v u M n" and A:"i ≤ n" "set xs ⊆ {0..n}" "len M i i xs < 𝟭" and surj_on: "∀ k ≤ n. k > 0 ⟶ (∃ c. v c = k)" shows False proof - from negative_len_shortest[OF _ A(3)] obtain j ys where ys: "distinct (j # ys)" "len M j j ys < 𝟭" "j ∈ set (i # xs)" "set ys ⊆ set xs" by blast show False proof (cases "ys = []") case True show ?thesis proof (cases "j = 0") case True with ‹ys = []› ys bounded show False unfolding DBM_val_bounded_def neutral less_eq[symmetric] by auto next case False with ‹ys = []› DBM_val_bounded_neg_cycle1[OF bounded _ _ ys(2) surj_on] ys(3) A(1,2) show False by auto qed next case False from distinct_arcs_ex[OF _ _ this, of j 0 j] ys(1) obtain a b where arc: "a ≠ 0" "(a, b) ∈ set (arcs j j ys)" by auto from cycle_rotate_2'[OF False this(2)] obtain zs where zs: "len M j j ys = len M a a (b # zs)" "set (a # b # zs) = set (j # ys)" "1 + length zs = length ys" "set (arcs j j ys) = set (arcs a a (b # zs))" by blast with distinct_card[OF ys(1)] have "distinct (a # b # zs)" by (intro card_distinct) auto with distinct_cnt[of "b # zs"] have *: "cnt 0 (b # zs) ≤ 1" by fastforce show ?thesis apply (rule DBM_val_bounded_neg_cycle1[OF bounded _ _ _ surj_on ‹a ≠ 0› *]) using zs(2) ys(3,4) A(1,2) apply fastforce+ using zs(1) ys(2) by simp qed qed subsection ‹Floyd-Warshall Algorithm Preservers Zones› lemma D_dest: "x = D m i j k ⟹ x ∈ {len m i j xs |xs. set xs ⊆ {0..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 FW_zone_equiv: "∀ k ≤ n. k > 0 ⟶ (∃ c. v c = k) ⟹ [M]⇘v,n⇙ = [FW M n]⇘v,n⇙" proof safe fix u assume A: "u ∈ [FW M n]⇘v,n⇙" { fix i j assume "i ≤ n" "j ≤ n" hence "FW M n i j ≤ M i j" using fw_mono[of n n n i j M n] by simp hence "FW M n i j ≼ M i j" by (simp add: less_eq) } with DBM_le_subset[of n "FW M n" M] A show "u ∈ [M]⇘v,n⇙" by auto next fix u assume u:"u ∈ [M]⇘v,n⇙" and surj_on: "∀ k ≤ n. k > 0 ⟶ (∃ c. v c = k)" hence *:"DBM_val_bounded v u M n" by (simp add: DBM_zone_repr_def) note ** = DBM_val_bounded_neg_cycle[OF this _ _ _ surj_on] have cyc_free: "cyc_free M n" using ** by fastforce with cycle_free_diag_equiv have cycle_free: "cycle_free M n" by auto from cycle_free_diag[OF this] have diag_ge_zero: "∀k≤n. M k k ≥ Le 0" unfolding neutral by auto have "DBM_val_bounded v u (FW M n) n" unfolding DBM_val_bounded_def proof (auto, goal_cases) case 1 from fw_shortest_path[OF cycle_free, of 0 n 0 n n] have **: "D M 0 0 n = FW M n 0 0" by (simp add: neutral) from D_dest[OF **[symmetric]] obtain xs where xs: "FW M n 0 0 = len M 0 0 xs" "set xs ⊆ {0..n}" "0 ∉ set xs" "distinct xs" by auto with cyc_free have "FW M n 0 0 ≥ 𝟭" by auto then show ?case unfolding neutral less_eq by simp next case (2 c) with fw_shortest_path[OF cycle_free, of 0 n "v c" n n] have **: "D M 0 (v c) n = FW M n 0 (v c)" by (simp add: neutral) from D_dest[OF **[symmetric]] obtain xs where xs: "FW M n 0 (v c) = len M 0 (v c) xs" "set xs ⊆ {0..n}" "0 ∉ set xs" "v c ∉ set xs" "distinct xs" by auto show ?case unfolding xs(1) using xs surj_on ‹v c ≤ n› by - (rule DBM_val_bounded_len'2[OF * xs(3)]; auto) next case (3 c) with fw_shortest_path[OF cycle_free, of "v c" n 0 n n] have **: "D M (v c) 0 n = FW M n (v c) 0" by (simp add: neutral) with D_dest[OF **[symmetric]] obtain xs where xs: "FW M n (v c) 0 = len M (v c) 0 xs" "set xs ⊆ {0..n}" "0 ∉ set xs" "v c ∉ set xs" "distinct xs" by auto show ?case unfolding xs(1) using xs surj_on ‹v c ≤ n› by - (rule DBM_val_bounded_len'1[OF * xs(3)]; auto) next case (4 c1 c2) with fw_shortest_path[OF cycle_free, of "v c1" n "v c2" n n] have "D M (v c1) (v c2) n = FW M n (v c1) (v c2)" by (simp add: neutral) from D_dest[OF this[symmetric]] obtain xs where xs: "FW M n (v c1) (v c2) = len M (v c1) (v c2) xs" "set xs ⊆ {0..n}" "v c1 ∉ set xs" "v c2 ∉ set xs" "distinct xs" by auto show ?case unfolding xs(1) apply (rule DBM_val_bounded_len'3[OF *]) using xs surj_on ‹v c1 ≤ n› ‹v c2 ≤ n› apply auto apply (drule distinct_cnt[of _ 0]) by auto qed then show "u ∈ [FW M n]⇘v,n⇙" unfolding DBM_zone_repr_def by simp qed lemma new_negative_cycle_aux': fixes M :: "('a :: time) DBM" fixes i j d defines "M' ≡ λ i' j'. if (i' = i ∧ j' = j) then Le d else if (i' = j ∧ j' = i) then Le (-d) else M i' j'" assumes "i ≤ n" "j ≤ n" "set xs ⊆ {0..n}" "cycle_free M n" "length xs = m" assumes "len M' i i (j # xs) < 𝟭 ∨ len M' j j (i # xs) < 𝟭" assumes "i ≠ j" shows "∃xs. set xs ⊆ {0..n} ∧ j ∉ set xs ∧ i ∉ set xs ∧ (len M' i i (j # xs) < 𝟭 ∨ len M' j j (i # xs) < 𝟭)" using assms proof (induction _ m arbitrary: xs rule: less_induct) case (less x) { fix b a xs assume A: "(i, j) ∉ set (arcs b a xs)" "(j, i) ∉ set (arcs b a xs)" with ‹i ≠ j› have "len M' b a xs = len M b a xs" unfolding M'_def by (induction xs arbitrary: b) auto } note * = this { fix a xs assume A:"(i, j) ∉ set (arcs a a xs)" "(j, i) ∉ set (arcs a a xs)" assume a: "a ≤ n" and xs: "set xs ⊆ {0..n}" and cycle: "¬ len M' a a xs ≥ 𝟭" from *[OF A] have "len M' a a xs = len M a a xs" . with ‹cycle_free M n› ‹i ≤ n› cycle xs a have False unfolding cycle_free_def by auto } note ** = this { fix a :: nat fix ys :: "nat list" assume A: "ys ≠ []" "length ys ≤ length xs" "set ys ⊆ set xs" "a ≤ n" assume cycle: "len M' a a ys < 𝟭" assume arcs: "(i, j) ∈ set (arcs a a ys) ∨ (j, i) ∈ set (arcs a a ys)" from arcs have ?thesis proof assume "(i, j) ∈ set (arcs a a ys)" from cycle_rotate_2[OF ‹ys ≠ []› this, of M'] obtain ws where ws: "len M' a a ys = len M' i i (j # ws)" "set ws ⊆ set (a # ys)" "length ws < length ys" by auto with cycle less.hyps(1)[OF _ less.hyps(2) , of "length ws" ws] less.prems A show ?thesis by fastforce next assume "(j, i) ∈ set (arcs a a ys)" from cycle_rotate_2[OF ‹ys ≠ []› this, of M'] obtain ws where ws: "len M' a a ys = len M' j j (i # ws)" "set ws ⊆ set (a # ys)" "length ws < length ys" by auto with cycle less.hyps(1)[OF _ less.hyps(2) , of "length ws" ws] less.prems A show ?thesis by fastforce qed } note *** = this { fix a :: nat fix ys :: "nat list" assume A: "ys ≠ []" "length ys ≤ length xs" "set ys ⊆ set xs" "a ≤ n" assume cycle: "¬ len M' a a ys ≥ 𝟭" with A **[of a ys] less.prems have "(i, j) ∈ set (arcs a a ys) ∨ (j, i) ∈ set (arcs a a ys)" by auto with ***[OF A] cycle have ?thesis by auto } note neg_cycle_IH = this from cycle_free_diag[OF ‹cycle_free M n›] have "∀i. i ≤ n ⟶ Le 0 ≤ M i i" unfolding neutral by auto then have M'_diag: "∀i. i ≤ n ⟶ Le 0 ≤ M' i i" unfolding M'_def using ‹i ≠ j› by auto from less(8) show ?thesis proof standard assume cycle:"len M' i i (j # xs) < 𝟭" show ?thesis proof (cases "i ∈ set xs") case False then show ?thesis proof (cases "j ∈ set xs") case False with ‹i ∉ set xs› show ?thesis using less.prems(3,6) by auto next case True then obtain ys zs where ys_zs: "xs = ys @ j # zs" by (meson split_list) with len_decomp[of "j # xs" "j # ys" j zs M' i i] have len: "len M' i i (j # xs) = M' i j + len M' j j ys + len M' j i zs" by auto show ?thesis proof (cases "len M' j j ys ≥ 𝟭") case True have "len M' i i (j # zs) = M' i j + len M' j i zs" by simp also from len True have "M' i j + len M' j i zs ≤ len M' i i (j # xs)" by (metis add_le_impl add_lt_neutral comm not_le) finally have cycle': "len M' i i (j # zs) < 𝟭" using cycle by auto from ys_zs less.prems(5) have "x > length zs" by auto from cycle' less.prems ys_zs less.hyps(1)[OF this less.hyps(2) , of zs] show ?thesis by auto next case False with M'_diag less.prems have "ys ≠ []" by (auto simp: neutral) from neg_cycle_IH[OF this] ys_zs False less.prems(1,2) show ?thesis by auto qed qed next case True then obtain ys zs where ys_zs: "xs = ys @ i # zs" by (meson split_list) with len_decomp[of "j # xs" "j # ys" i zs M' i i] have len: "len M' i i (j # xs) = M' i j + len M' j i ys + len M' i i zs" by auto show ?thesis proof (cases "len M' i i zs ≥ 𝟭") case True have "len M' i i (j # ys) = M' i j + len M' j i ys" by simp also from len True have "M' i j + len M' j i ys ≤ len M' i i (j # xs)" by (metis add_lt_neutral comm not_le) finally have cycle': "len M' i i (j # ys) < 𝟭" using cycle by auto from ys_zs less.prems(5) have "x > length ys" by auto from cycle' less.prems ys_zs less.hyps(1)[OF this less.hyps(2) , of ys] show ?thesis by auto next case False with less.prems(1,7) M'_diag have "zs ≠ []" by (auto simp: neutral) from neg_cycle_IH[OF this] ys_zs False less.prems(1,2) show ?thesis by auto qed qed next assume cycle:"len M' j j (i # xs) < 𝟭" show ?thesis proof (cases "j ∈ set xs") case False then show ?thesis proof (cases "i ∈ set xs") case False with ‹j ∉ set xs› show ?thesis using less.prems(3,6) by auto next case True then obtain ys zs where ys_zs: "xs = ys @ i # zs" by (meson split_list) with len_decomp[of "i # xs" "i # ys" i zs M' j j] have len: "len M' j j (i # xs) = M' j i + len M' i i ys + len M' i j zs" by auto show ?thesis proof (cases "len M' i i ys ≥ 𝟭") case True have "len M' j j (i # zs) = M' j i + len M' i j zs" by simp also from len True have "M' j i + len M' i j zs ≤ len M' j j (i # xs)" by (metis add_le_impl add_lt_neutral comm not_le) finally have cycle': "len M' j j (i # zs) < 𝟭" using cycle by auto from ys_zs less.prems(5) have "x > length zs" by auto from cycle' less.prems ys_zs less.hyps(1)[OF this less.hyps(2) , of zs] show ?thesis by auto next case False with less.prems M'_diag have "ys ≠ []" by (auto simp: neutral) from neg_cycle_IH[OF this] ys_zs False less.prems(1,2) show ?thesis by auto qed qed next case True then obtain ys zs where ys_zs: "xs = ys @ j # zs" by (meson split_list) with len_decomp[of "i # xs" "i # ys" j zs M' j j] have len: "len M' j j (i # xs) = M' j i + len M' i j ys + len M' j j zs" by auto show ?thesis proof (cases "len M' j j zs ≥ 𝟭") case True have "len M' j j (i # ys) = M' j i + len M' i j ys" by simp also from len True have "M' j i + len M' i j ys ≤ len M' j j (i # xs)" by (metis add_lt_neutral comm not_le) finally have cycle': "len M' j j (i # ys) < 𝟭" using cycle by auto from ys_zs less.prems(5) have "x > length ys" by auto from cycle' less.prems ys_zs less.hyps(1)[OF this less.hyps(2) , of ys] show ?thesis by auto next case False with less.prems(2,7) M'_diag have "zs ≠ []" by (auto simp: neutral) from neg_cycle_IH[OF this] ys_zs False less.prems(1,2) show ?thesis by auto qed qed qed qed lemma new_negative_cycle_aux: fixes M :: "('a :: time) DBM" fixes i d defines "M' ≡ λ i' j'. if (i' = i ∧ j' = 0) then Le d else if (i' = 0 ∧ j' = i) then Le (-d) else M i' j'" assumes "i ≤ n" "set xs ⊆ {0..n}" "cycle_free M n" "length xs = m" assumes "len M' 0 0 (i # xs) < 𝟭 ∨ len M' i i (0 # xs) < 𝟭" assumes "i ≠ 0" shows "∃xs. set xs ⊆ {0..n} ∧ 0 ∉ set xs ∧ i ∉ set xs ∧ (len M' 0 0 (i # xs) < 𝟭 ∨ len M' i i (0 # xs) < 𝟭)" using assms proof (induction _ m arbitrary: xs rule: less_induct) case (less x) { fix b a xs assume A: "(0, i) ∉ set (arcs b a xs)" "(i, 0) ∉ set (arcs b a xs)" then have "len M' b a xs = len M b a xs" unfolding M'_def by (induction xs arbitrary: b) auto } note * = this { fix a xs assume A:"(0, i) ∉ set (arcs a a xs)" "(i, 0) ∉ set (arcs a a xs)" assume a: "a ≤ n" and xs: "set xs ⊆ {0..n}" and cycle: "¬ len M' a a xs ≥ 𝟭" from *[OF A] have "len M' a a xs = len M a a xs" . with ‹cycle_free M n› ‹i ≤ n› cycle xs a have False unfolding cycle_free_def by auto } note ** = this { fix a :: nat fix ys :: "nat list" assume A: "ys ≠ []" "length ys ≤ length xs" "set ys ⊆ set xs" "a ≤ n" assume cycle: "len M' a a ys < 𝟭" assume arcs: "(0, i) ∈ set (arcs a a ys) ∨ (i, 0) ∈ set (arcs a a ys)" from arcs have ?thesis proof assume "(0, i) ∈ set (arcs a a ys)" from cycle_rotate_2[OF ‹ys ≠ []› this, of M'] obtain ws where ws: "len M' a a ys = len M' 0 0 (i # ws)" "set ws ⊆ set (a # ys)" "length ws < length ys" by auto with cycle less.hyps(1)[OF _ less.hyps(2) , of "length ws" ws] less.prems A show ?thesis by fastforce next assume "(i, 0) ∈ set (arcs a a ys)" from cycle_rotate_2[OF ‹ys ≠ []› this, of M'] obtain ws where ws: "len M' a a ys = len M' i i (0 # ws)" "set ws ⊆ set (a # ys)" "length ws < length ys" by auto with cycle less.hyps(1)[OF _ less.hyps(2) , of "length ws" ws] less.prems A show ?thesis by fastforce qed } note *** = this { fix a :: nat fix ys :: "nat list" assume A: "ys ≠ []" "length ys ≤ length xs" "set ys ⊆ set xs" "a ≤ n" assume cycle: "¬ len M' a a ys ≥ 𝟭" with A **[of a ys] less.prems(2) have "(0, i) ∈ set (arcs a a ys) ∨ (i, 0) ∈ set (arcs a a ys)" by auto with ***[OF A] cycle have ?thesis by auto } note neg_cycle_IH = this from cycle_free_diag[OF ‹cycle_free M n›] have "∀i. i ≤ n ⟶ Le 0 ≤ M i i" unfolding neutral by auto then have M'_diag: "∀i. i ≤ n ⟶ Le 0 ≤ M' i i" unfolding M'_def using ‹i ≠ 0› by auto from less(7) show ?thesis proof standard assume cycle:"len M' 0 0 (i # xs) < 𝟭" show ?thesis proof (cases "0 ∈ set xs") case False thus ?thesis proof (cases "i ∈ set xs") case False with ‹0 ∉ set xs› show ?thesis using less.prems by auto next case True then obtain ys zs where ys_zs: "xs = ys @ i # zs" by (meson split_list) with len_decomp[of "i # xs" "i # ys" i zs M' 0 0] have len: "len M' 0 0 (i # xs) = M' 0 i + len M' i i ys + len M' i 0 zs" by auto show ?thesis proof (cases "len M' i i ys ≥ 𝟭") case True have "len M' 0 0 (i # zs) = M' 0 i + len M' i 0 zs" by simp also from len True have "M' 0 i + len M' i 0 zs ≤ len M' 0 0 (i # xs)" by (metis add_le_impl add_lt_neutral comm not_le) finally have cycle': "len M' 0 0 (i # zs) < 𝟭" using cycle by auto from ys_zs less.prems(4) have "x > length zs" by auto from cycle' less.prems ys_zs less.hyps(1)[OF this less.hyps(2) , of zs] show ?thesis by auto next case False with less.prems(1,6) M'_diag have "ys ≠ []" by (auto simp: neutral) from neg_cycle_IH[OF this] ys_zs False less.prems(1,2) show ?thesis by auto qed qed next case True then obtain ys zs where ys_zs: "xs = ys @ 0 # zs" by (meson split_list) with len_decomp[of "i # xs" "i # ys" 0 zs M' 0 0] have len: "len M' 0 0 (i # xs) = M' 0 i + len M' i 0 ys + len M' 0 0 zs" by auto show ?thesis proof (cases "len M' 0 0 zs ≥ 𝟭") case True have "len M' 0 0 (i # ys) = M' 0 i + len M' i 0 ys" by simp also from len True have "M' 0 i + len M' i 0 ys ≤ len M' 0 0 (i # xs)" by (metis add_lt_neutral comm not_le) finally have cycle': "len M' 0 0 (i # ys) < 𝟭" using cycle by auto from ys_zs less.prems(4) have "x > length ys" by auto from cycle' less.prems ys_zs less.hyps(1)[OF this less.hyps(2) , of ys] show ?thesis by auto next case False with less.prems(1,6) M'_diag have "zs ≠ []" by (auto simp: neutral) from neg_cycle_IH[OF this] ys_zs False less.prems(1,2) show ?thesis by auto qed qed next assume cycle: "len M' i i (0 # xs) < 𝟭" show ?thesis proof (cases "i ∈ set xs") case False thus ?thesis proof (cases "0 ∈ set xs") case False with ‹i ∉ set xs› show ?thesis using less.prems by auto next case True then obtain ys zs where ys_zs: "xs = ys @ 0 # zs" by (meson split_list) with len_decomp[of "0 # xs" "0 # ys" 0 zs M' i i] have len: "len M' i i (0 # xs) = M' i 0 + len M' 0 0 ys + len M' 0 i zs" by auto show ?thesis proof (cases "len M' 0 0 ys ≥ 𝟭") case True have "len M' i i (0 # zs) = M' i 0 + len M' 0 i zs" by simp also from len True have "M' i 0 + len M' 0 i zs ≤ len M' i i (0 # xs)" by (metis add_le_impl add_lt_neutral comm not_le) finally have cycle': "len M' i i (0 # zs) < 𝟭" using cycle by auto from ys_zs less.prems(4) have "x > length zs" by auto from cycle' less.prems ys_zs less.hyps(1)[OF this less.hyps(2) , of zs] show ?thesis by auto next case False with less.prems(1,6) M'_diag have "ys ≠ []" by (auto simp: neutral) from neg_cycle_IH[OF this] ys_zs False less.prems(1,2) show ?thesis by auto qed qed next case True then obtain ys zs where ys_zs: "xs = ys @ i # zs" by (meson split_list) with len_decomp[of "0 # xs" "0 # ys" i zs M' i i] have len: "len M' i i (0 # xs) = M' i 0 + len M' 0 i ys + len M' i i zs" by auto show ?thesis proof (cases "len M' i i zs ≥ 𝟭") case True have "len M' i i (0 # ys) = M' i 0 + len M' 0 i ys" by simp also from len True have "M' i 0 + len M' 0 i ys ≤ len M' i i (0 # xs)" by (metis add_lt_neutral comm not_le) finally have cycle': "len M' i i (0 # ys) < 𝟭" using cycle by auto from ys_zs less.prems(4) have "x > length ys" by auto from cycle' less.prems ys_zs less.hyps(1)[OF this less.hyps(2) , of ys] show ?thesis by auto next case False with less.prems(1,6) M'_diag have "zs ≠ []" by (auto simp: neutral) from neg_cycle_IH[OF this] ys_zs False less.prems(1,2) show ?thesis by auto qed qed qed qed section ‹The Characteristic Property of Canonical DBMs› theorem fix_index': fixes M :: "(('a :: time) DBMEntry) mat" assumes "Le r ≤ M i j" "Le (-r) ≤ M j i" "cycle_free M n" "canonical M n" "i ≤ n" "j ≤ n" "i ≠ j" defines "M' ≡ λ i' j'. if (i' = i ∧ j' = j) then Le r else if (i' = j ∧ j' = i) then Le (-r) else M i' j'" shows "(∀ u. DBM_val_bounded v u M' n ⟶ DBM_val_bounded v u M n) ∧ cycle_free M' n" proof - note A = assms note r = assms(1,2) from ‹cycle_free M n› have diag_cycles: "∀i xs. i ≤ n ∧ set xs ⊆ {0..n} ⟶ Le 0 ≤ len M i i xs" unfolding cycle_free_def neutral by auto let ?M' = "λ i' j'. if (i' = i ∧ j' = j) then Le r else if (i' = j ∧ j' = i) then Le (-r) else M i' j'" have "?M' i' j' ≤ M i' j'" when "i' ≤ n" "j' ≤ n" for i' j' using assms by auto with DBM_le_subset[folded less_eq, of n ?M' M] have "DBM_val_bounded v u M n" if "DBM_val_bounded v u ?M' n" for u unfolding DBM_zone_repr_def using that by auto then have not_empty:"∀ u. DBM_val_bounded v u ?M' n ⟶ DBM_val_bounded v u M n" by auto { fix a xs assume prems: "a ≤ n" "set xs ⊆ {0..n}" and cycle: "¬ len ?M' a a xs ≥ 𝟭" { fix b assume A: "(i, j) ∉ set (arcs b a xs)" "(j, i) ∉ set (arcs b a xs)" with ‹i ≠ j› have "len ?M' b a xs = len M b a xs" by (induction xs arbitrary: b) auto } note * = this { fix a b xs assume A: "i ∉ set (a # xs)" "j ∉ set (a # xs)" then have "len ?M' a b xs = len M a b xs" by (induction xs arbitrary: a, auto) } note ** = this { assume A:"(i, j) ∉ set (arcs a a xs)" "(j, i) ∉ set (arcs a a xs)" from *[OF this] have "len ?M' a a xs = len M a a xs" . with ‹cycle_free M n› prems cycle have False by (auto simp: cycle_free_def) } then have arcs:"(i, j) ∈ set (arcs a a xs) ∨ (j, i) ∈ set (arcs a a xs)" by auto with ‹i ≠ j› have "xs ≠ []" by auto from arcs obtain xs where xs: "set xs ⊆ {0..n}" "len ?M' i i (j # xs) < 𝟭 ∨ len ?M' j j (i # xs) < 𝟭" proof (standard, goal_cases) case 1 from cycle_rotate_2'[OF ‹xs ≠ []› this(2), of ?M'] prems obtain ys where "len ?M' i i (j # ys) = len ?M' a a xs" "set ys ⊆ {0..n}" by fastforce with 1 cycle show ?thesis by fastforce next case 2 from cycle_rotate_2'[OF ‹xs ≠ []› this(2), of ?M'] prems obtain ys where "len ?M' j j (i # ys) = len ?M' a a xs" "set ys ⊆ {0..n}" by fastforce with 2 cycle show ?thesis by fastforce qed from new_negative_cycle_aux'[OF ‹i ≤ n› ‹j ≤ n› this(1) ‹cycle_free M n› _ this(2) ‹i ≠ j›] obtain xs where xs: "set xs ⊆ {0..n}" "i ∉ set xs" "j ∉ set xs" "len ?M' i i (j # xs) < 𝟭 ∨ len ?M' j j (i # xs) < 𝟭" by auto from this(4) have False proof assume A: "len ?M' j j (i # xs) < 𝟭" show False proof (cases xs) case Nil with ‹i ≠ j› have *:"?M' j i = Le (-r)" "?M' i j = Le r" by simp+ from Nil have "len ?M' j j (i # xs) = ?M' j i + ?M' i j" by simp with * have "len ?M' j j (i # xs) = Le 0" by (simp add: mult) then show False using A by (simp add: neutral) next case (Cons y ys) have *:"M i y + M y j ≥ M i j" using ‹canonical M n› Cons xs ‹i ≤ n› ‹j ≤ n› by (simp add: mult less_eq) have "Le 0 = Le (-r) + Le r" by (simp add: mult) also have "… ≤ Le (-r) + M i j" using r by (simp add: add_mono) also have "… ≤ Le (-r) + M i y + M y j" using * by (simp add: add_mono assoc) also have "… ≤ Le (-r) + ?M' i y + len M y j ys" using canonical_len[OF ‹canonical M n›] xs(1-3) ‹i ≤ n› ‹j ≤ n› Cons by (simp add: add_mono) also have "… = len ?M' j j (i # xs)" using Cons ‹i ≠ j› ** xs(1-3) by (simp add: assoc) also have "… < Le 0" using A by (simp add: neutral) finally show False by simp qed next assume A: "len ?M' i i (j # xs) < 𝟭" show False proof (cases xs) case Nil with ‹i ≠ j› have *:"?M' j i = Le (-r)" "?M' i j = Le r" by simp+ from Nil have "len ?M' i i (j # xs) = ?M' i j + ?M' j i" by simp with * have "len ?M' i i (j # xs) = Le 0" by (simp add: mult) then show False using A by (simp add: neutral) next case (Cons y ys) have *:"M j y + M y i ≥ M j i" using ‹canonical M n› Cons xs ‹i ≤ n› ‹j ≤ n› by (simp add: mult less_eq) have "Le 0 = Le r + Le (-r)" by (simp add: mult) also have "… ≤ Le r + M j i" using r by (simp add: add_mono) also have "… ≤ Le r + M j y + M y i" using * by (simp add: add_mono assoc) also have "… ≤ Le r + ?M' j y + len M y i ys" using canonical_len[OF ‹canonical M n›] xs(1-3) ‹i ≤ n› ‹j ≤ n› Cons by (simp add: add_mono) also have "… = len ?M' i i (j # xs)" using Cons ‹i ≠ j› ** xs(1-3) by (simp add: assoc) also have "… < Le 0" using A by (simp add: neutral) finally show False by simp qed qed } note * = this have "cycle_free ?M' n" using negative_cycle_dest_diag * by fastforce then show ?thesis using not_empty ‹i ≠ j› r unfolding M'_def by auto qed lemma fix_index: fixes M :: "(('a :: time) DBMEntry) mat" assumes "M 0 i + M i 0 > 𝟭" "cycle_free M n" "canonical M n" "i ≤ n" "i ≠ 0" shows "∃ (M' :: ('a DBMEntry) mat). ((∃ u. DBM_val_bounded v u M' n) ⟶ (∃ u. DBM_val_bounded v u M n)) ∧ M' 0 i + M' i 0 = 𝟭 ∧ cycle_free M' n ∧ (∀ j. i ≠ j ∧ M 0 j + M j 0 = 𝟭 ⟶ M' 0 j + M' j 0 = 𝟭) ∧ (∀ j. i ≠ j ∧ M 0 j + M j 0 > 𝟭 ⟶ M' 0 j + M' j 0 > 𝟭)" proof - note A = assms from sum_gt_neutral_dest[OF assms(1)] obtain d where d: "Le d ≤ M i 0" "Le (-d) ≤ M 0 i" by auto have "i ≠ 0" using A by - (rule ccontr; simp) let ?M' = "λi' j'. if i' = i ∧ j' = 0 then Le d else if i' = 0 ∧ j' = i then Le (-d) else M i' j'" from fix_index'[OF d(1,2) A(2,3,4) _ ‹i ≠ 0›] have M': "∀u. DBM_val_bounded v u ?M' n ⟶ DBM_val_bounded v u M n" "cycle_free ?M' n" by auto moreover from ‹i ≠ 0› have "∀ j. i ≠ j ∧ M 0 j + M j 0 = 𝟭 ⟶ ?M' 0 j + ?M' j 0 = 𝟭" by auto moreover from ‹i ≠ 0› have "∀ j. i ≠ j ∧ M 0 j + M j 0 > 𝟭 ⟶ ?M' 0 j + ?M' j 0 > 𝟭" by auto moreover from ‹i ≠ 0› have "?M' 0 i + ?M' i 0 = 𝟭" unfolding neutral mult by auto ultimately show ?thesis by blast qed subsubsection ‹ Putting it together › lemma FW_not_empty: "DBM_val_bounded v u (FW M' n) n ⟹ DBM_val_bounded v u M' n" proof - assume A: "DBM_val_bounded v u (FW M' n) n" have "∀i j. i ≤ n ⟶ j ≤ n ⟶ FW M' n i j ≤ M' i j" using fw_mono by blast from DBM_le_subset[of n "FW M' n" M' _ v, OF this[unfolded less_eq]] show "DBM_val_bounded v u M' n" using A by (auto simp: DBM_zone_repr_def) qed lemma fix_indices: fixes M :: "(('a :: time) DBMEntry) mat" assumes "set xs ⊆ {0..n}" "distinct xs" assumes "cyc_free M n" "canonical M n" shows "∃ (M' :: ('a DBMEntry) mat). ((∃ u. DBM_val_bounded v u M' n) ⟶ (∃ u. DBM_val_bounded v u M n)) ∧ (∀ i ∈ set xs. i ≠ 0 ⟶ M' 0 i + M' i 0 = 𝟭) ∧ cyc_free M' n ∧ (∀ i≤n. i ∉ set xs ∧ M 0 i + M i 0 = 𝟭 ⟶ M' 0 i + M' i 0 = 𝟭)" using assms proof (induction xs arbitrary: M) case Nil then show ?case by auto next case (Cons i xs) show ?case proof (cases "M 0 i + M i 0 ≤ 𝟭 ∨ i = 0") case True note T = this show ?thesis proof (cases "i = 0") case False from Cons.prems have "0 ≤ n" "set [i] ⊆ {0..n}" by auto with Cons.prems(3) False T have "M 0 i + M i 0 = 𝟭" by fastforce with Cons.IH[OF _ _ Cons.prems(3,4)] Cons.prems(1,2) show ?thesis by auto next case True with Cons.IH[OF _ _ Cons.prems(3,4)] Cons.prems(1,2) show ?thesis by auto qed next case False with Cons.prems have "𝟭 < M 0 i + M i 0" "i ≤ n" "i ≠ 0" by auto with fix_index[OF this(1) cycle_free_diag_intro[OF Cons.prems(3)] Cons.prems(4) this(2,3), of v] obtain M' :: "('a DBMEntry) mat" where M': "((∃u. DBM_val_bounded v u M' n) ⟶ (∃u. DBM_val_bounded v u M n))" "(M' 0 i + M' i 0 = 𝟭)" "cyc_free M' n" "∀j≤n. i ≠ j ∧ M 0 j + M j 0 > 𝟭 ⟶ M' 0 j + M' j 0 > 𝟭" "∀j. i ≠ j ∧ M 0 j + M j 0 = 𝟭 ⟶ M' 0 j + M' j 0 = 𝟭" using cycle_free_diag_equiv by blast let ?M' = "FW M' n" from fw_canonical[of M' n] cycle_free_diag_equiv ‹cyc_free M' n› have "canonical ?M' n" by auto from FW_cyc_free_preservation[OF ‹cyc_free M' n›] have "cyc_free ?M' n" by auto from FW_fixed_preservation[OF ‹i ≤ n› M'(2) ‹canonical ?M' n› ‹cyc_free ?M' n›] have fixed:"?M' 0 i + ?M' i 0 = 𝟭" by (auto simp: add_mono) from Cons.IH[OF _ _ ‹cyc_free ?M' n› ‹canonical ?M' n›] Cons.prems(1,2,3) obtain M'' :: "('a DBMEntry) mat" where M'': "((∃u. DBM_val_bounded v u M'' n) ⟶ (∃u. DBM_val_bounded v u ?M' n))" "(∀i∈set xs. i ≠ 0 ⟶ M'' 0 i + M'' i 0 = 𝟭)" "cyc_free M'' n" "(∀i≤n. i ∉ set xs ∧ ?M' 0 i + ?M' i 0 = 𝟭 ⟶ M'' 0 i + M'' i 0 = 𝟭)" by auto from FW_fixed_preservation[OF _ _ ‹canonical ?M' n› ‹cyc_free ?M' n›] M'(5) have "∀j≤n. i ≠ j ∧ M 0 j + M j 0 = 𝟭 ⟶ ?M' 0 j + ?M' j 0 = 𝟭" by auto with M''(4) have "∀j≤n. j ∉ set (i # xs) ∧ M 0 j + M j 0 = 𝟭 ⟶ M'' 0 j + M'' j 0 = 𝟭" by auto moreover from M''(2) M''(4) fixed Cons.prems(2) ‹i ≤ n› have "(∀i∈set (i#xs). i ≠ 0 ⟶ M'' 0 i + M'' i 0 = 𝟭)" by auto moreover from M''(1) M'(1) FW_not_empty[of v _ M' n] have "(∃u. DBM_val_bounded v u M'' n) ⟶ (∃u. DBM_val_bounded v u M n)" by auto ultimately show ?thesis using ‹cyc_free M'' n› M''(4) by auto qed qed lemma cyc_free_obtains_valuation: "cyc_free M n ⟹ ∀ c. v c ≤ n ⟶ v c > 0 ⟹ ∃ u. DBM_val_bounded v u M n" proof - assume A: "cyc_free M n" "∀ c. v c ≤ n ⟶ v c > 0" let ?M = "FW M n" from fw_canonical[of M n] cycle_free_diag_equiv A have "canonical ?M n" by auto from FW_cyc_free_preservation[OF A(1) ] have "cyc_free ?M n" . have "set [0..<n+1] ⊆ {0..n}" "distinct [0..<n+1]" by auto from fix_indices[OF this ‹cyc_free ?M n› ‹canonical ?M n›] obtain M' :: "('a DBMEntry) mat" where M': "(∃u. DBM_val_bounded v u M' n) ⟶ (∃u. DBM_val_bounded v u (FW M n) n)" "∀i∈set [0..<n + 1]. i ≠ 0 ⟶ M' 0 i + M' i 0 = 𝟭" "cyc_free M' n" by blast let ?M' = "FW M' n" have "⋀ i. i ≤ n ⟹ i ∈ set [0..<n + 1]" by auto with M'(2) have M'_fixed: "∀i≤n. i ≠ 0 ⟶ M' 0 i + M' i 0 = 𝟭" by fastforce from fw_canonical[of M' n] cycle_free_diag_equiv M'(3) have "canonical ?M' n" by blast from FW_fixed_preservation[OF _ _ this FW_cyc_free_preservation[OF M'(3)]] M'_fixed have fixed: "∀i≤n. i ≠ 0 ⟶ ?M' 0 i + ?M' i 0 = 𝟭" by auto have *: "⋀i. i ≤ n ⟹ i ≠ 0 ⟹ ∃ d. ?M' 0 i = Le (-d) ∧ ?M' i 0 = Le d" proof - fix i assume i: "i ≤ n" "i ≠ 0" from i fixed have *:"dbm_add (?M' 0 i) (?M' i 0) = Le 0" by (auto simp add: mult neutral) moreover { fix a b :: 'a assume "a + b = 0" then have "a = -b" by (simp add: eq_neg_iff_add_eq_0) } ultimately show "∃d. ?M' 0 i = Le (-d) ∧ ?M' i 0 = Le d" by (cases "?M' 0 i"; cases "?M' i 0"; simp) qed then obtain f where f: "∀ i≤n. i ≠ 0 ⟶ Le (f i) = ?M' i 0 ∧ Le (- f i) = ?M' 0 i" by metis let ?u = "λ c. f (v c)" have "DBM_val_bounded v ?u ?M' n" proof (auto simp add: DBM_val_bounded_def, goal_cases) case 1 from cyc_free_diag_dest'[OF FW_cyc_free_preservation[OF M'(3)]] show ?case unfolding neutral less_eq by fast next case (2 c) with A(2) have **: "v c > 0" by auto with *[OF 2] obtain d where d: "Le (-d) = ?M' 0 (v c)" by auto with f 2 ** have "Le (- f (v c)) = Le (- d)" by simp then have "- f (v c) ≤ - d" by auto from dbm_entry_val.intros(2)[of ?u , OF this] d show ?case by auto next case (3 c) with A(2) have **: "v c > 0" by auto with *[OF 3] obtain d where d: "Le d = ?M' (v c) 0" by auto with f 3 ** have "Le (f (v c)) = Le d" by simp then have "f (v c) ≤ d" by auto from dbm_entry_val.intros(1)[of ?u, OF this] d show ?case by auto next case (4 c1 c2) with A(2) have **: "v c1 > 0" "v c2 > 0" by auto with *[OF 4(1)] obtain d1 where d1: "Le d1 = ?M' (v c1) 0" by auto with f 4 ** have "Le (f (v c1)) = Le d1" by simp then have d1': "f (v c1) = d1" by auto from *[OF 4(2)] ** obtain d2 where d2: "Le d2 = ?M' (v c2) 0" by auto with f 4 ** have "Le (f (v c2)) = Le d2" by simp then have d2': "f (v c2) = d2" by auto have "Le d1 ≤ ?M' (v c1) (v c2) + Le d2" using ‹canonical ?M' n› 4 d1 d2 by (auto simp add: less_eq mult) then show ?case proof (cases "?M' (v c1) (v c2)", auto, goal_cases) case (1 d) from this(1) have "d1 ≤ d + d2" by (auto simp: mult less_eq le_dbm_le) then have "d1 - d2 ≤ d" by (simp add: diff_le_eq) then show ?case using d1' d2' by auto next case (2 d) from this(1) have "d1 < d + d2" by (auto simp: mult less_eq dbm_le_def elim: dbm_lt.cases) then have "d1 - d2 < d" using diff_less_eq by blast then show ?case using d1' d2' by auto qed qed from M'(1) FW_not_empty[OF this] obtain u where "DBM_val_bounded v u ?M n" by auto from FW_not_empty[OF this] show ?thesis by auto qed subsection ‹Floyd-Warshall and Empty DBMs› theorem FW_detects_empty_zone: "∀k≤n. 0 < k ⟶ (∃c. v c = k) ⟹ ∀ c. v c ≤ n ⟶ v c > 0 ⟹ [FW M n]⇘v,n⇙ = {} ⟷ (∃ i≤n. (FW M n) i i < Le 0)" proof assume surj_on:"∀k≤n. 0 < k ⟶ (∃c. v c = k)" and "∃i≤n. (FW M n) i i < Le 0" then obtain i where *: "len (FW M n) i i [] < 𝟭" "i ≤n" by (auto simp add: neutral) show "[FW M n]⇘v,n⇙ = {}" proof (rule ccontr, goal_cases) case 1 then obtain u where "DBM_val_bounded v u (FW M n) n" unfolding DBM_zone_repr_def by auto from DBM_val_bounded_neg_cycle[OF this *(2) _ *(1) surj_on] show ?case by auto qed next assume surj_on: "∀k≤n. 0 < k ⟶ (∃c. v c = k)" and empty: "[FW M n]⇘v,n⇙ = {}" and cn: "∀ c. v c ≤ n ⟶ v c > 0" show "∃ i≤n. (FW M n) i i < Le 0" proof (rule ccontr, goal_cases) case 1 then have *:"∀i≤n. FW M n i i ≥ 𝟭" by (auto simp add: neutral) have "cyc_free M n" proof (rule ccontr) assume "¬ cyc_free M n" then have A: "¬ cycle_free M n" using cycle_free_diag_equiv by auto from FW_neg_cycle_detect[OF A] * show False by auto qed from FW_cyc_free_preservation[OF this] have "cyc_free (FW M n) n" . from cyc_free_obtains_valuation[OF ‹cyc_free (FW M n) n› cn] empty obtain u where "DBM_val_bounded v u (FW M n) n" by blast with empty show ?case by (auto simp add: DBM_zone_repr_def) qed qed (* This definition is "internal" to the theorems for the correctness of the Floyd-Warshall algorithm and we want to reuse this as a variable name, so we hide it away *) hide_const D subsection ‹Mixed Corollaries› lemma cyc_free_not_empty: assumes "cyc_free M n" "∀c. v c ≤ n ⟶ 0 < v c" shows "[(M :: ('a :: time) DBM)]⇘v,n⇙ ≠ {}" using cyc_free_obtains_valuation[OF assms(1,2)] unfolding DBM_zone_repr_def by auto lemma empty_not_cyc_free: assumes "∀c. v c ≤ n ⟶ 0 < v c" "[(M :: ('a :: time) DBM)]⇘v,n⇙ = {}" shows "¬ cyc_free M n" using assms by (meson cyc_free_not_empty) lemma not_empty_cyc_free: assumes "∀k≤n. 0 < k ⟶ (∃ c. v c = k)" "[(M :: ('a :: time) DBM)]⇘v,n⇙ ≠ {}" shows "cyc_free M n" using DBM_val_bounded_neg_cycle[OF _ _ _ _ assms(1)] assms(2) unfolding DBM_zone_repr_def by fastforce lemma neg_cycle_empty: assumes "∀k≤n. 0 < k ⟶ (∃ c. v c = k)" "set xs ⊆ {0..n}" "i ≤ n" "len M i i xs < 𝟭" shows "[(M :: ('a :: time) DBM)]⇘v,n⇙ = {}" using assms by (metis leD not_empty_cyc_free) abbreviation clock_numbering' :: "('c ⇒ nat) ⇒ nat ⇒ bool" where "clock_numbering' v n ≡ ∀ c. v c > 0 ∧ (∀x. ∀y. v x ≤ n ∧ v y ≤ n ∧ v x = v y ⟶ x = y)" lemma non_empty_dbm_diag_set: "clock_numbering' v n ⟹ [M]⇘v,n⇙ ≠ {} ⟹ [M]⇘v,n⇙ = [(λ i j. if i = j then 𝟭 else M i j)]⇘v,n⇙" proof (auto simp: DBM_zone_repr_def