Theory DBM_Basics
theory DBM_Basics
imports
DBM
Paths_Cycles
Zones
begin
subsection ‹Useful definitions›
fun get_const where
"get_const (Le c) = c" |
"get_const (Lt c) = c" |
"get_const (∞ :: _ DBMEntry) = undefined"
subsection ‹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 ‹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)) ≥ 0 ⟹ a + b > 0 ⟹ ∃ d. Le d ≤ a ∧ Le (-d) ≤ b ∧ d ≥ 0"
proof -
assume "a + b > 0" "a ≥ 0"
show ?thesis
proof (cases "b ≥ 0")
case True
with ‹a ≥ 0› show ?thesis by (auto simp: neutral)
next
case False
hence "b < Le 0" by (auto simp: neutral)
note * = this ‹a ≥ 0› ‹a + b > 0›
note [simp] = neutral
show ?thesis
proof (cases a, cases b, goal_cases)
case (1 a' b')
with * have "a' + b' > 0" by (auto elim: dbm_lt.cases simp: less add)
hence "b' > -a'" by (metis add.commute diff_0 diff_less_eq)
with * 1 show ?case
by (auto simp: dbm_le_def less_eq le_dbm_le)
next
case (2 a' b')
with * have "a' + b' > 0" by (auto elim: dbm_lt.cases simp: less add)
hence "b' > -a'" by (metis add.commute diff_0 diff_less_eq)
with * 2 show ?case
by (auto simp: dbm_le_def less_eq le_dbm_le)
next
case (3 a')
with * show ?case
by auto
next
case (4 a')
thus ?case
proof (cases b, 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 add)
then have "-b' < a'" by (metis diff_0 diff_less_eq)
with ‹b' < 0› * 1 show ?case by (auto simp: dbm_le_def less_eq)
next
case (2 b')
with * 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) 2 * 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 add)
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) 2 ** 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
with * show ?case
by auto
qed
next
case 5 thus ?case
proof (cases b, goal_cases)
case (1 b')
with * 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› * 1 show ?case by auto
next
case (2 b')
with * 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+
with * 2 show ?case by auto
next
case 3
with * show ?case
by auto
qed
qed
qed
qed
lemma sum_gt_neutral_dest:
"(a :: (('a :: time) DBMEntry)) + b > 0 ⟹ ∃ d. Le d ≤ a ∧ Le (-d) ≤ b"
proof -
assume A: "a + b > 0"
then have A': "b + a > 0" by (simp add: comm)
show ?thesis
proof (cases "a ≥ 0")
case True
with A sum_gt_neutral_dest' show ?thesis by auto
next
case False
{ assume "b ≤ 0"
with False have "a ≤ 0" "b ≤ 0" by auto
from add_mono[OF this] have "a + b ≤ 0" by auto
with A have False by auto
}
then have "b ≥ 0" 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 < 0" 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
subgoal for a xs
using cnt_0_I by (cases "x = a") fastforce+
done
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 < 0" 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 < 0" "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
paragraph ‹Nicer Path Boundedness Theorems›
lemma DBM_val_bounded_len_1:
fixes v
assumes "DBM_val_bounded v u M n" "v c ≤ n" "set vs ⊆ {0..n}" "∀ k ≤ n. (∃ c. v c = k)"
shows "dbm_entry_val u (Some c) None (len M (v c) 0 vs)" using assms
proof (induction "length vs" arbitrary: vs rule: less_induct)
case A: less
show ?case
proof (cases "0 ∈ set vs")
case False
with DBM_val_bounded_len_1'_aux[OF A(2,3)] A(4,5) show ?thesis by fastforce
next
case True
then obtain xs ys where vs: "vs = xs @ 0 # ys" by (meson split_list)
from len_decomp[OF this] have "len M (v c) 0 vs = len M (v c) 0 xs + len M 0 0 ys" .
moreover have "len M 0 0 ys ≥ 0"
proof (rule ccontr, goal_cases)
case 1
then have "len M 0 0 ys < 0" by simp
with DBM_val_bounded_neg_cycle[OF assms(1), of 0 ys] vs A(4,5) show False by auto
qed
ultimately have *: "len M (v c) 0 vs ≥ len M (v c) 0 xs" by (simp add: add_increasing2)
from vs A have "dbm_entry_val u (Some c) None (len M (v c) 0 xs)" by auto
from dbm_entry_val_mono3[OF this, of "len M (v c) 0 vs"] * show ?thesis unfolding less_eq by auto
qed
qed
lemma DBM_val_bounded_len_2:
fixes v
assumes "DBM_val_bounded v u M n" "v c ≤ n" "set vs ⊆ {0..n}" "∀ k ≤ n. (∃ c. v c = k)"
shows "dbm_entry_val u None (Some c) (len M 0 (v c) vs)" using assms
proof (induction "length vs" arbitrary: vs rule: less_induct)
case A: less
show ?case
proof (cases "0 ∈ set vs")
case False
with DBM_val_bounded_len_2'_aux[OF A(2,3)] A(4,5) show ?thesis by fastforce
next
case True
then obtain xs ys where vs: "vs = xs @ 0 # ys" by (meson split_list)
from len_decomp[OF this] have "len M 0 (v c) vs = len M 0 0 xs + len M 0 (v c) ys" .
moreover have "len M 0 0 xs ≥ 0"
proof (rule ccontr, goal_cases)
case 1
then have "len M 0 0 xs < 0" by simp
with DBM_val_bounded_neg_cycle[OF assms(1), of 0 xs] vs A(4,5) show False by auto
qed
ultimately have *: "len M 0 (v c) vs ≥ len M 0 (v c) ys" by (simp add: add_increasing)
from vs A have "dbm_entry_val u None (Some c) (len M 0 (v c) ys)" by auto
from dbm_entry_val_mono2[OF this] * show ?thesis unfolding less_eq by auto
qed
qed
lemma DBM_val_bounded_len_3:
fixes v
assumes "DBM_val_bounded v u M n" "v c1 ≤ n" "v c2 ≤ n" "set vs ⊆ {0..n}"
"∀ k ≤ n. (∃ c. v c = k)"
shows "dbm_entry_val u (Some c1) (Some c2) (len M (v c1) (v c2) vs)" using assms
proof (cases "0 ∈ set vs")
case False
with DBM_val_bounded_len_3'_aux[OF assms(1-3)] assms(4-) show ?thesis by fastforce
next
case True
then obtain xs ys where vs: "vs = xs @ 0 # ys" by (meson split_list)
from assms(4,5) vs DBM_val_bounded_len_1[OF assms(1,2)] DBM_val_bounded_len_2[OF assms(1,3)]
have
"dbm_entry_val u (Some c1) None (len M (v c1) 0 xs)"
"dbm_entry_val u None (Some c2) (len M 0 (v c2) ys)"
by auto
from dbm_entry_val_add_4[OF this] len_decomp[OF vs, of M] show ?thesis unfolding add by auto
qed
text ‹An equivalent way of handling ‹𝟬››
fun val_0 :: "('c ⇒ ('a :: linordered_ab_group_add)) ⇒ 'c option ⇒ 'a" where
"val_0 u None = 0" |
"val_0 u (Some c) = u c"
notation val_0 ("_⇩𝟬 _" [90,90] 90)
lemma dbm_entry_val_None_None[dest]:
"dbm_entry_val u None None l ⟹ l = ∞"
by (auto elim: dbm_entry_val.cases)
lemma dbm_entry_val_dbm_lt:
assumes "dbm_entry_val u x y l"
shows "Lt (u⇩𝟬 x - u⇩𝟬 y) ≺ l"
using assms by (cases rule: dbm_entry_val.cases, auto)
lemma dbm_lt_dbm_entry_val_1:
assumes "Lt (u x) ≺ l"
shows "dbm_entry_val u (Some x) None l"
using assms by (cases rule: dbm_lt.cases) auto
lemma dbm_lt_dbm_entry_val_2:
assumes "Lt (- u x) ≺ l"
shows "dbm_entry_val u None (Some x) l"
using assms by (cases rule: dbm_lt.cases) auto
lemma dbm_lt_dbm_entry_val_3:
assumes "Lt (u x - u y) ≺ l"
shows "dbm_entry_val u (Some x) (Some y) l"
using assms by (cases rule: dbm_lt.cases) auto
text ‹A more uniform theorem for boundedness by paths›
lemma DBM_val_bounded_len:
fixes v
defines "v' ≡ λ x. if x = None then 0 else v (the x)"
assumes "DBM_val_bounded v u M n" "v' x ≤ n" "v' y ≤ n" "set vs ⊆ {0..n}"
"∀ k ≤ n. (∃ c. v c = k)" "x ≠ None ∨ y ≠ None"
shows "Lt (u⇩𝟬 x - u⇩𝟬 y) ≺ len M (v' x) (v' y) vs" using assms
apply -
apply (rule dbm_entry_val_dbm_lt)
apply (cases x; cases y)
apply simp_all
apply (rule DBM_val_bounded_len_2; auto)
apply (rule DBM_val_bounded_len_1; auto)
apply (rule DBM_val_bounded_len_3; auto)
done
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 i n j M] 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
from cyc_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 (safe, goal_cases)
case 1
from fw_shortest_path[OF cyc_free] 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 ≥ 0" by auto
then show ?case unfolding neutral less_eq by simp
next
case (2 c)
with fw_shortest_path[OF cyc_free] 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 cyc_free] 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 cyc_free]
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› by (auto dest!: distinct_cnt[of _ 0])
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) < 0 ∨ len M' j j (i # xs) < 0"
assumes "i ≠ j"
shows "∃xs. set xs ⊆ {0..n} ∧ j ∉ set xs ∧ i ∉ set xs
∧ (len M' i i (j # xs) < 0 ∨ len M' j j (i # xs) < 0)" 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 ≥ 0"
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 < 0"
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 ≥ 0"
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) < 0"
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 ≥ 0")
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) < 0" 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 ≥ 0")
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) < 0" 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) < 0"
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 ≥ 0")
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) < 0" 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 ≥ 0")
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) < 0" 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) < 0 ∨ len M' i i (0 # xs) < 0"
assumes "i ≠ 0"
shows "∃xs. set xs ⊆ {0..n} ∧ 0 ∉ set xs ∧ i ∉ set xs
∧ (len M' 0 0 (i # xs) < 0 ∨ len M' i i (0 # xs) < 0)" 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 ≥ 0"
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 < 0"
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 ≥ 0"
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) < 0"
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 ≥ 0")
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) < 0" 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 ≥ 0")
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) < 0" 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) < 0"
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 ≥ 0")
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) < 0" 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 ≥ 0")
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) < 0" 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 ≥ 0"
{ 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) < 0 ∨ len ?M' j j (i # xs) < 0"
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) < 0 ∨ len ?M' j j (i # xs) < 0"
by auto
from this(4) have False
proof
assume A: "len ?M' j j (i # xs) < 0"
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: add)
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: add less_eq)
have "Le 0 = Le (-r) + Le r" by (simp add: add)
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 add.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: 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) < 0"
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: add)
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: add less_eq)
have "Le 0 = Le r + Le (-r)" by (simp add: add)
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 add.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: 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" unfolding cycle_free_diag_equiv[symmetric]
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 > 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 = 0 ∧ cycle_free M' n
∧ (∀ j. i ≠ j ∧ M 0 j + M j 0 = 0 ⟶ M' 0 j + M' j 0 = 0)
∧ (∀ j. i ≠ j ∧ M 0 j + M j 0 > 0 ⟶ M' 0 j + M' j 0 > 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 = 0 ⟶ ?M' 0 j + ?M' j 0 = 0" by auto
moreover from ‹i ≠ 0› have "∀ j. i ≠ j ∧ M 0 j + M j 0 > 0 ⟶ ?M' 0 j + ?M' j 0 > 0" by auto
moreover from ‹i ≠ 0› have "?M' 0 i + ?M' i 0 = 0" unfolding neutral add 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 = 0) ∧ cyc_free M' n
∧ (∀ i≤n. i ∉ set xs ∧ M 0 i + M i 0 = 0 ⟶ M' 0 i + M' i 0 = 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 ≤ 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 = 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 "0 < 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 = 0)"
"cyc_free M' n" "∀j≤n. i ≠ j ∧ M 0 j + M j 0 > 0 ⟶ M' 0 j + M' j 0 > 0"
"∀j. i ≠ j ∧ M 0 j + M j 0 = 0 ⟶ M' 0 j + M' j 0 = 0"
using cycle_free_diag_equiv by blast
let ?M' = "FW M' n"
from fw_canonical[of n M'] ‹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 = 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 = 0)" "cyc_free M'' n"
"(∀i≤n. i ∉ set xs ∧ ?M' 0 i + ?M' i 0 = 0 ⟶ M'' 0 i + M'' i 0 = 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 = 0 ⟶ ?M' 0 j + ?M' j 0 = 0" by auto
with M''(4) have "∀j≤n. j ∉ set (i # xs) ∧ M 0 j + M j 0 = 0 ⟶ M'' 0 j + M'' j 0 = 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 = 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 n M] 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 = 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 = 0" by fastforce
from fw_canonical[of n M'] 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 = 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: add 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"
unfolding DBM_val_bounded_def
proof (safe, 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 add)
then show ?case
proof (cases "?M' (v c1) (v c2)", goal_cases)
case (1 d)
then have "d1 ≤ d + d2" by (auto simp: add less_eq le_dbm_le)
then have "d1 - d2 ≤ d" by (simp add: diff_le_eq)
with 1 show ?case using d1' d2' by auto
next
case (2 d)
then have "d1 < d + d2" by (auto simp: add less_eq dbm_le_def elim: dbm_lt.cases)
then have "d1 - d2 < d" using diff_less_eq by blast
with 2 show ?case using d1' d2' by auto
qed auto
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 [] < 0" "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 ≥ 0" by (auto simp add: neutral)
have "cyc_free M n"
proof (rule ccontr)
assume "¬ cyc_free M n"
from FW_neg_cycle_detect[OF this] * 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
hide_const (open) 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 < 0"
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 0 else M i j)]⇘v,n⇙"
unfolding DBM_zone_repr_def
proof (safe, goal_cases)
case 1
{ fix c assume A: "v c = 0"
from 1 have "v c > 0" by auto
with A have False by auto
} note * = this
from 1 have [simp]: "Le 0 ≼ M 0 0" by (auto simp: DBM_val_bounded_def)
note [simp] = neutral
from 1 show ?case
unfolding DBM_val_bounded_def
apply safe
subgoal
using * by simp
subgoal
using * by (metis (full_types))
subgoal
using * by (metis (full_types))
subgoal for c1 c2
by (cases "c1 = c2") auto
done
next
case (2 x xa)
note G = this
{ fix c assume A: "v c = 0"
from 2 have "v c > 0" by auto
with A have False by auto
} note * = this
{ fix c assume A: "v c ≤ n" "M (v c) (v c) < 0"
with 2 have False
by (fastforce simp: neutral DBM_val_bounded_def less elim!: dbm_lt.cases)
} note ** = this
from 2 have [simp]: "Le 0 ≼ M 0 0" by (auto simp: DBM_val_bounded_def)
note [simp] = neutral
from 2 show ?case
unfolding DBM_val_bounded_def
proof (safe, goal_cases)
case 1 with * show ?case by simp presburger
case 2 with * show ?case by presburger
next
case (3 c1 c2)
show ?case
proof (cases "v c1 = v c2")
case True
with 3 have "c1 = c2" by auto
moreover from this **[OF 3(9)] not_less have "M (v c2) (v c2) ≥ 0" by auto
ultimately show "dbm_entry_val xa (Some c1) (Some c2) (M (v c1) (v c2))" unfolding neutral
by (cases "M (v c1) (v c2)") (auto simp add: less_eq dbm_le_def, fastforce+)
next
case False
with 3 show ?thesis by presburger
qed
qed
qed
lemma non_empty_cycle_free:
assumes "[M]⇘v,n⇙ ≠ {}"
and "∀k≤n. 0 < k ⟶ (∃c. v c = k)"
shows "cycle_free M n"
apply (rule ccontr)
apply (drule negative_cycle_dest_diag')
using DBM_val_bounded_neg_cycle assms unfolding DBM_zone_repr_def by blast
lemma neg_diag_empty:
assumes "∀k≤n. 0 < k ⟶ (∃c. v c = k)" "i ≤ n" "M i i < 0"
shows "[M]⇘v,n⇙ = {}"
unfolding DBM_zone_repr_def using DBM_val_bounded_neg_cycle[of v _ M n i "[]"] assms by auto
lemma canonical_empty_zone:
assumes "∀k≤n. 0 < k ⟶ (∃c. v c = k)" "∀c. v c ≤ n ⟶ 0 < v c"
and "canonical M n"
shows "[M]⇘v,n⇙ = {} ⟷ (∃i≤n. M i i < 0)"
using FW_detects_empty_zone[OF assms(1,2), of M] FW_canonical_id[OF assms(3)] unfolding neutral
by simp
section ‹Orderings of DBMs›
lemma canonical_saturated_1:
assumes "Le r ≤ M (v c1) 0"
and "Le (- r) ≤ M 0 (v c1)"
and "cycle_free M n"
and "canonical M n"
and "v c1 ≤ n"
and "v c1 > 0"
and "∀c. v c ≤ n ⟶ 0 < v c"
obtains u where "u ∈ [M]⇘v,n⇙" "u c1 = r"
proof -
let ?M' = "λi' j'. if i'=v c1 ∧ j'=0 then Le r else if i'=0 ∧ j'=v c1 then Le (- r) else M i' j'"
from fix_index'[OF assms(1-5)] assms(6) have M':
"∀u. DBM_val_bounded v u ?M' n ⟶ DBM_val_bounded v u M n"
"cycle_free ?M' n" "?M' (v c1) 0 = Le r" "?M' 0 (v c1) = Le (- r)"
by auto
with cyc_free_obtains_valuation[unfolded cycle_free_diag_equiv, of ?M' n v] assms(7) obtain u where
u: "DBM_val_bounded v u ?M' n"
by fastforce
with assms(5,6) M'(3,4) have "u c1 = r" unfolding DBM_val_bounded_def by fastforce
moreover from u M'(1) have "u ∈ [M]⇘v,n⇙" unfolding DBM_zone_repr_def by auto
ultimately show thesis by (auto intro: that)
qed
lemma canonical_saturated_2:
assumes "Le r ≤ M 0 (v c2)"
and "Le (- r) ≤ M (v c2) 0"
and "cycle_free M n"
and "canonical M n"
and "v c2 ≤ n"
and "v c2 > 0"
and "∀c. v c ≤ n ⟶ 0 < v c"
obtains u where "u ∈ [M]⇘v,n⇙" "u c2 = - r"
proof -
let ?M' = "λi' j'. if i'=0 ∧ j'=v c2 then Le r else if i'=v c2 ∧ j'=0 then Le (-r) else M i' j'"
from fix_index'[OF assms(1-4)] assms(5,6) have M':
"∀u. DBM_val_bounded v u ?M' n ⟶ DBM_val_bounded v u M n"
"cycle_free ?M' n" "?M' 0 (v c2) = Le r" "?M' (v c2) 0 = Le (- r)"
by auto
with cyc_free_obtains_valuation[unfolded cycle_free_diag_equiv, of ?M' n v] assms(7) obtain u where
u: "DBM_val_bounded v u ?M' n"
by fastforce
with assms(5,6) M'(3,4) have "u c2 ≤ -r" "- u c2 ≤ r" unfolding DBM_val_bounded_def by fastforce+
then have "u c2 = -r" by (simp add: le_minus_iff)
moreover from u M'(1) have "u ∈ [M]⇘v,n⇙" unfolding DBM_zone_repr_def by auto
ultimately show thesis by (auto intro: that)
qed
lemma canonical_saturated_3:
assumes "Le r ≤ M (v c1) (v c2)"
and "Le (- r) ≤ M (v c2) (v c1)"
and "cycle_free M n"
and "canonical M n"
and "v c1 ≤ n" "v c2 ≤ n"
and "v c1 ≠ v c2"
and "∀c. v c ≤ n ⟶ 0 < v c"
obtains u where "u ∈ [M]⇘v,n⇙" "u c1 - u c2 = r"
proof -
let ?M'="λi' j'. if i'=v c1 ∧ j'=v c2 then Le r else if i'=v c2 ∧ j'=v c1 then Le (-r) else M i' j'"
from fix_index'[OF assms(1-7), of v] assms(7,8) have M':
"∀u. DBM_val_bounded v u ?M' n ⟶ DBM_val_bounded v u M n"
"cycle_free ?M' n" "?M' (v c1) (v c2) = Le r" "?M' (v c2) (v c1) = Le (- r)"
by auto
with cyc_free_obtains_valuation[unfolded cycle_free_diag_equiv, of ?M' n v] assms obtain u where u:
"DBM_val_bounded v u ?M' n"
by fastforce
with assms(5,6) M'(3,4) have
"u c1 - u c2 ≤ r" "u c2 - u c1 ≤ - r"
unfolding DBM_val_bounded_def by fastforce+
then have "u c1 - u c2 = r" by (simp add: le_minus_iff)
moreover from u M'(1) have "u ∈ [M]⇘v,n⇙" unfolding DBM_zone_repr_def by auto
ultimately show thesis by (auto intro: that)
qed
lemma DBM_canonical_subset_le:
notes any_le_inf[intro]
fixes M :: "real DBM"
assumes "canonical M n" "[M]⇘v,n⇙ ⊆ [M']⇘v,n⇙" "[M]⇘v,n⇙ ≠ {}" "i ≤ n" "j ≤ n" "i ≠ j"
assumes clock_numbering: "clock_numbering' v n"
"∀k≤n. 0 < k ⟶ (∃c. v c = k)"
shows "M i j ≤ M' i j"
proof -
from non_empty_cycle_free[OF assms(3)] clock_numbering(2) have "cycle_free M n" by auto
with assms(1,4,5) have non_neg:
"M i j + M j i ≥ Le 0"
by (metis cycle_free_diag order.trans neutral)
from clock_numbering have cn: "∀c. v c ≤ n ⟶ 0 < v c" by auto
show ?thesis
proof (cases "i = 0")
case True
show ?thesis
proof (cases "j = 0")
case True
with assms ‹i = 0› show ?thesis
unfolding neutral DBM_zone_repr_def DBM_val_bounded_def less_eq by auto
next
case False
then have "j > 0" by auto
with ‹j ≤ n› clock_numbering obtain c2 where c2: "v c2 = j" by auto
note t = canonical_saturated_2[OF _ _ ‹cycle_free M n› assms(1) assms(5)[folded c2] _ cn,unfolded c2]
show ?thesis
proof (rule ccontr, goal_cases)
case 1
{ fix d assume 1: "M 0 j = ∞"
obtain r where r: "Le r ≤ M 0 j" "Le (-r) ≤ M j 0" "d < r"
proof (cases "M j 0")
case (Le d')
obtain r where "r > - d'" using gt_ex by blast
with Le 1 show ?thesis by (intro that[of "max r (d + 1)"]) auto
next
case (Lt d')
obtain r where "r > - d'" using gt_ex by blast
with Lt 1 show ?thesis by (intro that[of "max r (d + 1)"]) auto
next
case INF
with 1 show ?thesis by (intro that[of "d + 1"]) auto
qed
then have "∃ r. Le r ≤ M 0 j ∧ Le (-r) ≤ M j 0 ∧ d < r" by auto
} note inf_case = this
{ fix a b d :: real assume 1: "a < b" assume b: "b + d > 0"
then have *: "b > -d" by auto
obtain r where "r > - d" "r > a" "r < b"
proof (cases "a ≥ - d")
case True
from 1 obtain r where "r > a" "r < b" using dense by auto
with True show ?thesis by (auto intro: that[of r])
next
case False
with * obtain r where "r > -d" "r < b" using dense by auto
with False show ?thesis by (auto intro: that[of r])
qed
then have "∃ r. r > -d ∧ r > a ∧ r < b" by auto
} note gt_case = this
{ fix a r assume r: "Le r ≤ M 0 j" "Le (-r) ≤ M j 0" "a < r" "M' 0 j = Le a ∨ M' 0 j = Lt a"
from t[OF this(1,2) ‹0 < j›] obtain u where u: "u ∈ [M]⇘v,n⇙" "u c2 = - r" .
with ‹j ≤ n› c2 assms(2) have "dbm_entry_val u None (Some c2) (M' 0 j)"
unfolding DBM_zone_repr_def DBM_val_bounded_def by blast
with u(2) r(3,4) have False by auto
} note contr = this
from 1 True have "M' 0 j < M 0 j" by auto
then show False unfolding less
proof (cases rule: dbm_lt.cases)
case (1 d)
with inf_case obtain r where r: "Le r ≤ M 0 j" "Le (-r) ≤ M j 0" "d < r" by auto
from contr[OF this] 1 show False by fast
next
case (2 d)
with inf_case obtain r where r: "Le r ≤ M 0 j" "Le (-r) ≤ M j 0" "d < r" by auto
from contr[OF this] 2 show False by fast
next
case (3 a b)
obtain r where r: "Le r ≤ M 0 j" "Le (-r) ≤ M j 0" "a < r"
proof (cases "M j 0")
case (Le d')
with 3 non_neg ‹i = 0› have "b + d' ≥ 0" unfolding add by auto
then have "b ≥ - d'" by auto
with 3 obtain r where "r ≥ - d'" "r > a" "r ≤ b" by blast
with Le 3 show ?thesis by (intro that[of r]) auto
next
case (Lt d')
with 3 non_neg ‹i = 0› have "b + d' > 0" unfolding add by auto
from gt_case[OF 3(3) this] obtain r where "r > - d'" "r > a" "r ≤ b" by auto
with Lt 3 show ?thesis by (intro that[of r]) auto
next
case INF
with 3 show ?thesis by (intro that[of b]) auto
qed
from contr[OF this] 3 show False by fast
next
case (4 a b)
obtain r where r: "Le r ≤ M 0 j" "Le (-r) ≤ M j 0" "a < r"
proof (cases "M j 0")
case (Le d)
with 4 non_neg ‹i = 0› have "b + d > 0" unfolding add by auto
from gt_case[OF 4(3) this] obtain r where "r > - d" "r > a" "r < b" by auto
with Le 4 show ?thesis by (intro that[of r]) auto
next
case (Lt d)
with 4 non_neg ‹i = 0› have "b + d > 0" unfolding add by auto
from gt_case[OF 4(3) this] obtain r where "r > - d" "r > a" "r < b" by auto
with Lt 4 show ?thesis by (intro that[of r]) auto
next
case INF
from 4 dense obtain r where "r > a" "r < b" by auto
with 4 INF show ?thesis by (intro that[of r]) auto
qed
from contr[OF this] 4 show False by fast
next
case (5 a b)
obtain r where r: "Le r ≤ M 0 j" "Le (-r) ≤ M j 0" "a ≤ r"
proof (cases "M j 0")
case (Le d')
with 5 non_neg ‹i = 0› have "b + d' ≥ 0" unfolding add by auto
then have "b ≥ - d'" by auto
with 5 obtain r where "r ≥ - d'" "r ≥ a" "r ≤ b" by blast
with Le 5 show ?thesis by (intro that[of r]) auto
next
case (Lt d')
with 5 non_neg ‹i = 0› have "b + d' > 0" unfolding add by auto
then have "b > - d'" by auto
with 5 obtain r where "r > - d'" "r ≥ a" "r ≤ b" by blast
with Lt 5 show ?thesis by (intro that[of r]) auto
next
case INF
with 5 show ?thesis by (intro that[of b]) auto
qed
from t[OF this(1,2) ‹j > 0›] obtain u where u: "u ∈ [M]⇘v,n⇙" "u c2 = - r" .
with ‹j ≤ n› c2 assms(2) have "dbm_entry_val u None (Some c2) (M' 0 j)"
unfolding DBM_zone_repr_def DBM_val_bounded_def by blast
with u(2) r(3) 5 show False by auto
next
case (6 a b)
obtain r where r: "Le r ≤ M 0 j" "Le (-r) ≤ M j 0" "a < r"
proof (cases "M j 0")
case (Le d)
with 6 non_neg ‹i = 0› have "b + d > 0" unfolding add by auto
from gt_case[OF 6(3) this] obtain r where "r > - d" "r > a" "r < b" by auto
with Le 6 show ?thesis by (intro that[of r]) auto
next
case (Lt d)
with 6 non_neg ‹i = 0› have "b + d > 0" unfolding add by auto
from gt_case[OF 6(3) this] obtain r where "r > - d" "r > a" "r < b" by auto
with Lt 6 show ?thesis by (intro that[of r]) auto
next
case INF
from 6 dense obtain r where "r > a" "r < b" by auto
with 6 INF show ?thesis by (intro that[of r]) auto
qed
from contr[OF this] 6 show False by fast
qed
qed
qed
next
case False
then have "i > 0" by auto
with ‹i ≤ n› clock_numbering obtain c1 where c1: "v c1 = i" by auto
show ?thesis
proof (cases "j = 0")
case True
note t = canonical_saturated_1[OF _ _ ‹cycle_free M n› assms(1) assms(4)[folded c1] _ cn,
unfolded c1]
show ?thesis
proof (rule ccontr, goal_cases)
case 1
{ fix d assume 1: "M i 0 = ∞"
obtain r where r: "Le r ≤ M i 0" "Le (-r) ≤ M 0 i" "d < r"
proof (cases "M 0 i")
case (Le d')
obtain r where "r > - d'" using gt_ex by blast
with Le 1 show ?thesis by (intro that[of "max r (d + 1)"]) auto
next
case (Lt d')
obtain r where "r > - d'" using gt_ex by blast
with Lt 1 show ?thesis by (intro that[of "max r (d + 1)"]) auto
next
case INF
with 1 show ?thesis by (intro that[of "d + 1"]) auto
qed
then have "∃ r. Le r ≤ M i 0 ∧ Le (-r) ≤ M 0 i ∧ d < r" by auto
} note inf_case = this
{ fix a b d :: real assume 1: "a < b" assume b: "b + d > 0"
then have *: "b > -d" by auto
obtain r where "r > - d" "r > a" "r < b"
proof (cases "a ≥ - d")
case True
from 1 obtain r where "r > a" "r < b" using dense by auto
with True show ?thesis by (auto intro: that[of r])
next
case False
with * obtain r where "r > -d" "r < b" using dense by auto
with False show ?thesis by (auto intro: that[of r])
qed
then have "∃ r. r > -d ∧ r > a ∧ r < b" by auto
} note gt_case = this
{ fix a r assume r: "Le r ≤ M i 0" "Le (-r) ≤ M 0 i" "a < r" "M' i 0 = Le a ∨ M' i 0 = Lt a"
from t[OF this(1,2) ‹i > 0›] obtain u where u: "u ∈ [M]⇘v,n⇙" "u c1 = r" .
with ‹i ≤ n› c1 assms(2) have "dbm_entry_val u (Some c1) None (M' i 0)"
unfolding DBM_zone_repr_def DBM_val_bounded_def by blast
with u(2) r(3,4) have False by auto
} note contr = this
from 1 True have "M' i 0 < M i 0" by auto
then show False unfolding less
proof (cases rule: dbm_lt.cases)
case (1 d)
with inf_case obtain r where r: "Le r ≤ M i 0" "Le (-r) ≤ M 0 i" "d < r" by auto
from contr[OF this] 1 show False by fast
next
case (2 d)
with inf_case obtain r where r: "Le r ≤ M i 0" "Le (-r) ≤ M 0 i" "d < r" by auto
from contr[OF this] 2 show False by fast
next
case (3 a b)
obtain r where r: "Le r ≤ M i 0" "Le (-r) ≤ M 0 i" "a < r"
proof (cases "M 0 i")
case (Le d')
with 3 non_neg ‹j = 0› have "b + d' ≥ 0" unfolding add by auto
then have "b ≥ - d'" by auto
with 3 obtain r where "r ≥ - d'" "r > a" "r ≤ b" by blast
with Le 3 show ?thesis by (intro that[of r]) auto
next
case (Lt d')
with 3 non_neg ‹j = 0› have "b + d' > 0" unfolding add by auto
from gt_case[OF 3(3) this] obtain r where "r > - d'" "r > a" "r ≤ b" by auto
with Lt 3 show ?thesis by (intro that[of r]) auto
next
case INF
with 3 show ?thesis by (intro that[of b]) auto
qed
from contr[OF this] 3 show False by fast
next
case (4 a b)
obtain r where r: "Le r ≤ M i 0" "Le (-r) ≤ M 0 i" "a < r"
proof (cases "M 0 i")
case (Le d)
with 4 non_neg ‹j = 0› have "b + d > 0" unfolding add by auto
from gt_case[OF 4(3) this] obtain r where "r > - d" "r > a" "r < b" by auto
with Le 4 show ?thesis by (intro that[of r]) auto
next
case (Lt d)
with 4 non_neg ‹j = 0› have "b + d > 0" unfolding add by auto
from gt_case[OF 4(3) this] obtain r where "r > - d" "r > a" "r < b" by auto
with Lt 4 show ?thesis by (intro that[of r]) auto
next
case INF
from 4 dense obtain r where "r > a" "r < b" by auto
with 4 INF show ?thesis by (intro that[of r]) auto
qed
from contr[OF this] 4 show False by fast
next
case (5 a b)
obtain r where r: "Le r ≤ M i 0" "Le (-r) ≤ M 0 i" "a ≤ r"
proof (cases "M 0 i")
case (Le d')
with 5 non_neg ‹j = 0› have "b + d' ≥ 0" unfolding add by auto
then have "b ≥ - d'" by auto
with 5 obtain r where "r ≥ - d'" "r ≥ a" "r ≤ b" by blast
with Le 5 show ?thesis by (intro that[of r]) auto
next
case (Lt d')
with 5 non_neg ‹j = 0› have "b + d' > 0" unfolding add by auto
then have "b > - d'" by auto
with 5 obtain r where "r > - d'" "r ≥ a" "r ≤ b" by blast
with Lt 5 show ?thesis by (intro that[of r]) auto
next
case INF
with 5 show ?thesis by (intro that[of b]) auto
qed
from t[OF this(1,2) ‹i > 0›] obtain u where u: "u ∈ [M]⇘v,n⇙" "u c1 = r" .
with ‹i ≤ n› c1 assms(2) have "dbm_entry_val u (Some c1) None (M' i 0)"
unfolding DBM_zone_repr_def DBM_val_bounded_def by blast
with u(2) r(3) 5 show False by auto
next
case (6 a b)
obtain r where r: "Le r ≤ M i 0" "Le (-r) ≤ M 0 i" "a < r"
proof (cases "M 0 i")
case (Le d)
with 6 non_neg ‹j = 0› have "b + d > 0" unfolding add by auto
from gt_case[OF 6(3) this] obtain r where "r > - d" "r > a" "r < b" by auto
with Le 6 show ?thesis by (intro that[of r]) auto
next
case (Lt d)
with 6 non_neg ‹j = 0› have "b + d > 0" unfolding add by auto
from gt_case[OF 6(3) this] obtain r where "r > - d" "r > a" "r < b" by auto
with Lt 6 show ?thesis by (intro that[of r]) auto
next
case INF
from 6 dense obtain r where "r > a" "r < b" by auto
with 6 INF show ?thesis by (intro that[of r]) auto
qed
from contr[OF this] 6 show False by fast
qed
qed
next
case False
then have "j > 0" by auto
with ‹j ≤ n› clock_numbering obtain c2 where c2: "v c2 = j" by auto
note t = canonical_saturated_3[OF _ _ ‹cycle_free M n› assms(1) assms(4)[folded c1]
assms(5)[folded c2] _ cn, unfolded c1 c2]
show ?thesis
proof (rule ccontr, goal_cases)
case 1
{ fix d assume 1: "M i j = ∞"
obtain r where r: "Le r ≤ M i j" "Le (-r) ≤ M j i" "d < r"
proof (cases "M j i")
case (Le d')
obtain r where "r > - d'" using gt_ex by blast
with Le 1 show ?thesis by (intro that[of "max r (d + 1)"]) auto
next
case (Lt d')
obtain r where "r > - d'" using gt_ex by blast
with Lt 1 show ?thesis by (intro that[of "max r (d + 1)"]) auto
next
case INF
with 1 show ?thesis by (intro that[of "d + 1"]) auto
qed
then have "∃ r. Le r ≤ M i j ∧ Le (-r) ≤ M j i ∧ d < r" by auto
} note inf_case = this
{ fix a b d :: real assume 1: "a < b" assume b: "b + d > 0"
then have *: "b > -d" by auto
obtain r where "r > - d" "r > a" "r < b"
proof (cases "a ≥ - d")
case True
from 1 obtain r where "r > a" "r < b" using dense by auto
with True show ?thesis by (auto intro: that[of r])
next
case False
with * obtain r where "r > -d" "r < b" using dense by auto
with False show ?thesis by (auto intro: that[of r])
qed
then have "∃ r. r > -d ∧ r > a ∧ r < b" by auto
} note gt_case = this
{ fix a r assume r: "Le r ≤ M i j" "Le (-r) ≤ M j i" "a < r" "M' i j = Le a ∨ M' i j = Lt a"
from t[OF this(1,2) ‹i ≠ j›] obtain u where u: "u ∈ [M]⇘v,n⇙" "u c1 - u c2 = r" .
with ‹i ≤ n› ‹j ≤ n› c1 c2 assms(2) have "dbm_entry_val u (Some c1) (Some c2) (M' i j)"
unfolding DBM_zone_repr_def DBM_val_bounded_def by blast
with u(2) r(3,4) have False by auto
} note contr = this
from 1 have "M' i j < M i j" by auto
then show False unfolding less
proof (cases rule: dbm_lt.cases)
case (1 d)
with inf_case obtain r where r: "Le r ≤ M i j" "Le (-r) ≤ M j i" "d < r" by auto
from contr[OF this] 1 show False by fast
next
case (2 d)
with inf_case obtain r where r: "Le r ≤ M i j" "Le (-r) ≤ M j i" "d < r" by auto
from contr[OF this] 2 show False by fast
next
case (3 a b)
obtain r where r: "Le r ≤ M i j" "Le (-r) ≤ M j i" "a < r"
proof (cases "M j i")
case (Le d')
with 3 non_neg have "b + d' ≥ 0" unfolding add by auto
then have "b ≥ - d'" by auto
with 3 obtain r where "r ≥ - d'" "r > a" "r ≤ b" by blast
with Le 3 show ?thesis by (intro that[of r]) auto
next
case (Lt d')
with 3 non_neg have "b + d' > 0" unfolding add by auto
from gt_case[OF 3(3) this] obtain r where "r > - d'" "r > a" "r ≤ b" by auto
with Lt 3 show ?thesis by (intro that[of r]) auto
next
case INF
with 3 show ?thesis by (intro that[of b]) auto
qed
from contr[OF this] 3 show False by fast
next
case (4 a b)
obtain r where r: "Le r ≤ M i j" "Le (-r) ≤ M j i" "a < r"
proof (cases "M j i")
case (Le d)
with 4 non_neg have "b + d > 0" unfolding add by auto
from gt_case[OF 4(3) this] obtain r where "r > - d" "r > a" "r < b" by auto
with Le 4 show ?thesis by (intro that[of r]) auto
next
case (Lt d)
with 4 non_neg have "b + d > 0" unfolding add by auto
from gt_case[OF 4(3) this] obtain r where "r > - d" "r > a" "r < b" by auto
with Lt 4 show ?thesis by (intro that[of r]) auto
next
case INF
from 4 dense obtain r where "r > a" "r < b" by auto
with 4 INF show ?thesis by (intro that[of r]) auto
qed
from contr[OF this] 4 show False by fast
next
case (5 a b)
obtain r where r: "Le r ≤ M i j" "Le (-r) ≤ M j i" "a ≤ r"
proof (cases "M j i")
case (Le d')
with 5 non_neg have "b + d' ≥ 0" unfolding add by auto
then have "b ≥ - d'" by auto
with 5 obtain r where "r ≥ - d'" "r ≥ a" "r ≤ b" by blast
with Le 5 show ?thesis by (intro that[of r]) auto
next
case (Lt d')
with 5 non_neg have "b + d' > 0" unfolding add by auto
then have "b > - d'" by auto
with 5 obtain r where "r > - d'" "r ≥ a" "r ≤ b" by blast
with Lt 5 show ?thesis by (intro that[of r]) auto
next
case INF
with 5 show ?thesis by (intro that[of b]) auto
qed
from t[OF this(1,2) ‹i ≠ j›] obtain u where u: "u ∈ [M]⇘v,n⇙" "u c1 - u c2= r" .
with ‹i ≤ n› ‹j ≤ n› c1 c2 assms(2) have "dbm_entry_val u (Some c1) (Some c2) (M' i j)"
unfolding DBM_zone_repr_def DBM_val_bounded_def by blast
with u(2) r(3) 5 show False by auto
next
case (6 a b)
obtain r where r: "Le r ≤ M i j" "Le (-r) ≤ M j i" "a < r"
proof (cases "M j i")
case (Le d)
with 6 non_neg have "b + d > 0" unfolding add by auto
from gt_case[OF 6(3) this] obtain r where "r > - d" "r > a" "r < b" by auto
with Le 6 show ?thesis by (intro that[of r]) auto
next
case (Lt d)
with 6 non_neg have "b + d > 0" unfolding add by auto
from gt_case[OF 6(3) this] obtain r where "r > - d" "r > a" "r < b" by auto
with Lt 6 show ?thesis by (intro that[of r]) auto
next
case INF
from 6 dense obtain r where "r > a" "r < b" by auto
with 6 INF show ?thesis by (intro that[of r]) auto
qed
from contr[OF this] 6 show False by fast
qed
qed
qed
qed
qed
end