# Theory Timed_Automata.DBM

theory DBM
imports Floyd_Warshall Timed_Automata
begin

chapter ‹Difference Bound Matrices›

section ‹Definitions›

text ‹
Difference Bound Matrices (DBMs) constrain differences of clocks
(or more precisely, the difference of values assigned to individual clocks by a valuation).
The possible constraints are given by the following datatype:
›

datatype ('t::time) DBMEntry = Le 't | Lt 't | INF ("∞")

text ‹\noindent This yields a simple definition of DBMs:›

type_synonym 't DBM = "nat ⇒ nat ⇒ 't DBMEntry"

text ‹\noindent
To relate clocks with rows and columns of
a DBM, we use a clock numbering ‹v› of type @{typ "'c ⇒ nat"} to map clocks to indices.
DBMs will regularly be  accompanied by a natural number $n$,
which designates the number of clocks constrained by the matrix.
To be able to represent the full set of clock constraints with DBMs, we add an imaginary
clock ‹𝟬›, which shall be assigned to 0 in every valuation.
In the following predicate we explicitly keep track of ‹𝟬›.
›

inductive dbm_entry_val :: "('c, 't) cval ⇒ 'c option ⇒ 'c option ⇒ ('t::time) DBMEntry ⇒ bool"
where
"u r ≤ d ⟹ dbm_entry_val u (Some r) None (Le d)" |
"-u c ≤ d ⟹ dbm_entry_val u None (Some c) (Le d)" |
"u r < d ⟹ dbm_entry_val u (Some r) None (Lt d)" |
"-u c < d ⟹ dbm_entry_val u None (Some c) (Lt d)" |
"u r - u c ≤ d ⟹ dbm_entry_val u (Some r) (Some c) (Le d)" |
"u r - u c < d ⟹ dbm_entry_val u (Some r) (Some c) (Lt d)" |
"dbm_entry_val _ _ _ ∞"

declare dbm_entry_val.intros[intro]
inductive_cases[elim!]: "dbm_entry_val u None (Some c) (Le d)"
inductive_cases[elim!]: "dbm_entry_val u (Some c) None (Le d)"
inductive_cases[elim!]: "dbm_entry_val u None (Some c) (Lt d)"
inductive_cases[elim!]: "dbm_entry_val u (Some c) None (Lt d)"
inductive_cases[elim!]: "dbm_entry_val u (Some r) (Some c) (Le d)"
inductive_cases[elim!]: "dbm_entry_val u (Some r) (Some c) (Lt d)"

fun dbm_entry_bound :: "('t::time) DBMEntry ⇒ 't"
where
"dbm_entry_bound (Le t) = t" |
"dbm_entry_bound (Lt t) = t" |
"dbm_entry_bound ∞ = 0"

inductive dbm_lt :: "('t::time) DBMEntry ⇒ 't DBMEntry ⇒ bool"
("_ ≺ _" [51, 51] 50)
where
"dbm_lt (Lt _) ∞" |
"dbm_lt (Le _) ∞" |
"a < b  ⟹ dbm_lt (Le a) (Le b)" |
"a < b  ⟹ dbm_lt (Le a) (Lt b)" |
"a ≤ b  ⟹ dbm_lt (Lt a) (Le b)" |
"a < b  ⟹ dbm_lt (Lt a) (Lt b)"

declare dbm_lt.intros[intro]

definition dbm_le :: "('t::time) DBMEntry ⇒ 't DBMEntry ⇒ bool"
("_ ≼ _" [51, 51] 50)
where
"dbm_le a b ≡ (a ≺ b) ∨ a = b"

text ‹
Now a valuation is contained in the zone represented by a DBM if it fulfills all individual
constraints:
›

definition DBM_val_bounded :: "('c ⇒ nat) ⇒ ('c, 't) cval ⇒ ('t::time) DBM ⇒ nat ⇒ bool"
where
"DBM_val_bounded v u m n ≡ Le 0 ≼ m 0 0 ∧
(∀ c. v c ≤ n ⟶ (dbm_entry_val u None (Some c) (m 0 (v c))
∧ dbm_entry_val u (Some c) None (m (v c) 0)))
∧ (∀ c1 c2. v c1 ≤ n ∧ v c2 ≤ n ⟶ dbm_entry_val u (Some c1) (Some c2) (m (v c1) (v c2)))"

abbreviation DBM_val_bounded_abbrev ::
"('c, 't) cval ⇒ ('c ⇒ nat) ⇒ nat ⇒ ('t::time) DBM ⇒ bool"
("_ ⊢⇘_,_⇙ _")
where
"u ⊢⇘v,n⇙ M ≡ DBM_val_bounded v u M n"

abbreviation
"dmin a b ≡ if a ≺ b then a else b"

lemma dbm_le_dbm_min:
"a ≼ b ⟹ a = dmin a b" unfolding dbm_le_def
by auto

lemma dbm_lt_asym:
assumes "e ≺ f"
shows "~ f ≺ e"
using assms
proof (safe, cases e f rule: dbm_lt.cases, goal_cases)
case 1 from this(2) show ?case using 1(3-) by (cases f e rule: dbm_lt.cases) auto
next
case 2 from this(2) show ?case using 2(3-) by (cases f e rule: dbm_lt.cases) auto
next
case 3 from this(2) show ?case using 3(3-) by (cases f e rule: dbm_lt.cases) auto
next
case 4 from this(2) show ?case using 4(3-) by (cases f e rule: dbm_lt.cases) auto
next
case 5 from this(2) show ?case using 5(3-) by (cases f e rule: dbm_lt.cases) auto
next
case 6 from this(2) show ?case using 6(3-) by (cases f e rule: dbm_lt.cases) auto
qed

lemma dbm_le_dbm_min2:
"a ≼ b ⟹ a = dmin b a"
using dbm_lt_asym by (auto simp: dbm_le_def)

lemma dmb_le_dbm_entry_bound_inf:
"a ≼ b ⟹ a = ∞ ⟹ b = ∞"
apply (auto simp: dbm_le_def)
apply (cases rule: dbm_lt.cases)
by auto

lemma dbm_not_lt_eq: "¬ a ≺ b ⟹ ¬ b ≺ a ⟹ a = b"
apply (cases a)
apply (cases b, fastforce+)+
done

lemma dbm_not_lt_impl: "¬ a ≺ b ⟹ b ≺ a ∨ a = b" using dbm_not_lt_eq by auto

lemma "dmin a b = dmin b a"
proof (cases "a ≺ b")
case True thus ?thesis by (simp add: dbm_lt_asym)
next
case False thus ?thesis by (simp add: dbm_not_lt_eq)
qed

lemma dbm_lt_trans: "a ≺ b ⟹ b ≺ c ⟹ a ≺ c"
proof (cases a b rule: dbm_lt.cases, goal_cases)
case 1 thus ?case by simp
next
case 2 from this(2-) show ?case by (cases rule: dbm_lt.cases) simp+
next
case 3 from this(2-) show ?case by (cases rule: dbm_lt.cases) simp+
next
case 4 from this(2-) show ?case by (cases rule: dbm_lt.cases) auto
next
case 5 from this(2-) show ?case by (cases rule: dbm_lt.cases) auto
next
case 6 from this(2-) show ?case by (cases rule: dbm_lt.cases) auto
next
case 7 from this(2-) show ?case by (cases rule: dbm_lt.cases) auto
qed

lemma aux_3: "¬ a ≺ b ⟹ ¬ b ≺ c ⟹ a ≺ c ⟹ c = a"
proof goal_cases
case 1 thus ?case
proof (cases "c ≺ b")
case True
with ‹a ≺ c› have "a ≺ b" by (rule dbm_lt_trans)
thus ?thesis using 1 by auto
next
case False thus ?thesis using dbm_not_lt_eq 1 by auto
qed
qed

inductive_cases[elim!]: "∞ ≺ x"

lemma dbm_lt_asymmetric[simp]: "x ≺ y ⟹ y ≺ x ⟹ False"
by (cases x y rule: dbm_lt.cases) (auto elim: dbm_lt.cases)

lemma le_dbm_le: "Le a ≼ Le b ⟹ a ≤ b" unfolding dbm_le_def by (auto elim: dbm_lt.cases)

lemma le_dbm_lt: "Le a ≼ Lt b ⟹ a < b" unfolding dbm_le_def by (auto elim: dbm_lt.cases)

lemma lt_dbm_le: "Lt a ≼ Le b ⟹ a ≤ b" unfolding dbm_le_def by (auto elim: dbm_lt.cases)

lemma lt_dbm_lt: "Lt a ≼ Lt b ⟹ a ≤ b" unfolding dbm_le_def by (auto elim: dbm_lt.cases)

lemma not_dbm_le_le_impl: "¬ Le a ≺ Le b ⟹ a ≥ b" by (metis dbm_lt.intros(3) not_less)

lemma not_dbm_lt_le_impl: "¬ Lt a ≺ Le b ⟹ a > b" by (metis dbm_lt.intros(5) not_less)

lemma not_dbm_lt_lt_impl: "¬ Lt a ≺ Lt b ⟹ a ≥ b" by (metis dbm_lt.intros(6) not_less)

lemma not_dbm_le_lt_impl: "¬ Le a ≺ Lt b ⟹ a ≥ b" by (metis dbm_lt.intros(4) not_less)

(*>*)

(*<*)

fun dbm_add :: "('t::time) DBMEntry ⇒ 't DBMEntry ⇒ 't DBMEntry" (infixl "⊗" 70)
where
"dbm_add ∞     _      = ∞" |
"dbm_add _      ∞     = ∞" |
"dbm_add (Le a) (Le b) = (Le (a+b))" |
"dbm_add (Le a) (Lt b) = (Lt (a+b))" |
"dbm_add (Lt a) (Le b) = (Lt (a+b))" |
"dbm_add (Lt a) (Lt b) = (Lt (a+b))"

by (cases x y rule: dbm_lt.cases) ((cases z), auto)+

proof -
assume lt: "dbm_add x z ≺ dbm_add y z" "¬ x ≺ y"
hence "x = y ∨ y ≺ x" by (auto simp: dbm_not_lt_eq)
thus ?thesis
proof
assume "x = y" thus ?thesis by simp
next
assume "y ≺ x"
thus ?thesis
proof (cases y x rule: dbm_lt.cases, goal_cases)
case 1 thus ?case using lt by auto
next
case 2 thus ?case using lt by auto
next
case 3 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+
next
case 4 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+
next
case 5 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+
next
case 6 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+
qed
qed
qed

by (cases x y rule: dbm_lt.cases) ((cases z), auto)+

proof -
assume lt: "dbm_add z x ≺ dbm_add z y" "¬ x ≺ y"
hence "x = y ∨ y ≺ x" by (auto simp: dbm_not_lt_eq)
thus ?thesis
proof
assume "x = y" thus ?thesis by simp
next
assume "y ≺ x"
thus ?thesis
proof (cases y x rule: dbm_lt.cases, goal_cases)
case 1 thus ?case using lt by (cases z) fastforce+
next
case 2 thus ?case using lt by (cases z) fastforce+
next
case 3 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+
next
case 4 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+
next
case 5 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+
next
case 6 thus ?case using dbm_lt_asymmetric lt(1) by (cases z) fastforce+
qed
qed
qed

"a ≠ ∞ ⟹ b ≠ ∞ ⟹ dbm_add a b ≠ ∞"
by (cases a, auto, cases b, auto, cases b, auto)

lemma dbm_le_not_inf:
"a ≼ b ⟹ b ≠ ∞ ⟹ a ≠ ∞"
by (cases "a = b") (auto simp: dbm_le_def)

section ‹DBM Entries Form a Linearly Ordered Abelian Monoid›

instantiation DBMEntry :: (time) linorder
begin
definition less_eq: "(≤) ≡ dbm_le"
definition less: "(<) = dbm_lt"
instance
proof ((standard; unfold less less_eq), goal_cases)
case 1 thus ?case unfolding dbm_le_def using dbm_lt_asymmetric by auto
next
case 2 thus ?case by (simp add: dbm_le_def)
next
case 3 thus ?case unfolding dbm_le_def using dbm_lt_trans by auto
next
case 4 thus ?case unfolding dbm_le_def using dbm_lt_asymmetric by auto
next
case 5 thus ?case unfolding dbm_le_def using dbm_not_lt_eq by auto
qed
end

begin
definition neutral: "neutral = Le 0"
instance proof ((standard; unfold mult neutral less less_eq), goal_cases)
case (1 a b c) thus ?case by (cases a; cases b; cases c; auto)
next
case (2 a b) thus ?case by (cases a; cases b) auto
next
case (3 a b c)
thus ?case unfolding dbm_le_def
apply safe
apply (rule dbm_lt.cases)
apply assumption
by (cases c; fastforce)+
next
case (4 x) thus ?case by (cases x) auto
next
case (5 x) thus ?case by (cases x) auto
qed
end

apply (standard, fold neutral mult less_eq less)

lemma Le_Le_dbm_lt_D[dest]: "Le a ≺ Lt b ⟹ a < b" by (cases rule: dbm_lt.cases) auto
lemma Le_Lt_dbm_lt_D[dest]: "Le a ≺ Le b ⟹ a < b" by (cases rule: dbm_lt.cases) auto
lemma Lt_Le_dbm_lt_D[dest]: "Lt a ≺ Le b ⟹ a ≤ b" by (cases rule: dbm_lt.cases) auto
lemma Lt_Lt_dbm_lt_D[dest]: "Lt a ≺ Lt b ⟹ a < b" by (cases rule: dbm_lt.cases) auto

lemma Le_le_LeI[intro]: "a ≤ b ⟹ Le a ≤ Le b" unfolding less_eq dbm_le_def by auto
lemma Lt_le_LeI[intro]: "a ≤ b ⟹ Lt a ≤ Le b" unfolding less_eq dbm_le_def by auto
lemma Lt_le_LtI[intro]: "a ≤ b ⟹ Lt a ≤ Lt b" unfolding less_eq dbm_le_def by auto
lemma Le_le_LtI[intro]: "a < b ⟹ Le a ≤ Lt b" unfolding less_eq dbm_le_def by auto
lemma Lt_lt_LeI: "x ≤ y ⟹ Lt x < Le y" unfolding less by auto

lemma Le_le_LeD[dest]: "Le a ≤ Le b ⟹ a ≤ b" unfolding dbm_le_def less_eq by auto
lemma Le_le_LtD[dest]: "Le a ≤ Lt b ⟹ a < b" unfolding dbm_le_def less_eq by auto
lemma Lt_le_LeD[dest]: "Lt a ≤ Le b ⟹ a ≤ b" unfolding less_eq dbm_le_def by auto
lemma Lt_le_LtD[dest]: "Lt a ≤ Lt b ⟹ a ≤ b" unfolding less_eq dbm_le_def by auto

lemma inf_not_le_Le[simp]: "∞ ≤ Le x = False" unfolding less_eq dbm_le_def by auto
lemma inf_not_le_Lt[simp]: "∞ ≤ Lt x = False" unfolding less_eq dbm_le_def by auto
lemma inf_not_lt[simp]: "∞ ≺ x = False" by auto

lemma any_le_inf: "x ≤ ∞" by (metis less_eq dmb_le_dbm_entry_bound_inf le_cases)

section ‹Basic Properties of DBMs›

subsection ‹DBMs and Length of Paths›

lemma dbm_entry_val_add_1: "dbm_entry_val u (Some c) (Some d) a ⟹  dbm_entry_val u (Some d) None b
⟹ dbm_entry_val u (Some c) None (dbm_add a b)"
proof (cases a, goal_cases)
case 1 thus ?thesis
apply (cases b)
apply auto
next
case 2 thus ?thesis
apply (cases b)
apply auto
apply (simp add: dbm_entry_val.intros(3) diff_less_eq less_le_trans)
next
case 3 thus ?thesis by (cases b) auto
qed

lemma dbm_entry_val_add_2: "dbm_entry_val u None (Some c) a ⟹ dbm_entry_val u (Some c) (Some d) b
⟹ dbm_entry_val u None (Some d) (dbm_add a b)"
proof (cases a, goal_cases)
case 1 thus ?thesis
apply (cases b)
apply auto
next
case 2 thus ?thesis
apply (cases b)
apply auto
next
case 3 thus ?thesis by (cases b) auto
qed

"dbm_entry_val u (Some c) (Some d) a ⟹  dbm_entry_val u (Some d) (Some e) b
⟹ dbm_entry_val u (Some c) (Some e) (dbm_add a b)"
proof (cases a, goal_cases)
case 1 thus ?thesis
apply (cases b)
apply auto
next
case 2 thus ?thesis
apply (cases b)
apply auto
next
case 3 thus ?thesis by (cases b) auto
qed

"dbm_entry_val u (Some c) None a ⟹ dbm_entry_val u None (Some d) b
⟹ dbm_entry_val u (Some c) (Some d) (dbm_add a b)"
proof (cases a, goal_cases)
case 1 thus ?thesis
apply (cases b)
apply auto
next
case 2 thus ?thesis
apply (cases b)
apply auto
next
case 3 thus ?thesis by (cases b) auto
qed

lemma DBM_val_bounded_len_1'_aux:
assumes "DBM_val_bounded v u m n" "v c ≤ n" "∀ k ∈ set vs. k > 0 ∧ k ≤ n ∧ (∃ c. v c = k)"
shows "dbm_entry_val u (Some c) None (len m (v c) 0 vs)" using assms
proof (induction vs arbitrary: c)
case Nil then show ?case unfolding DBM_val_bounded_def by auto
next
case (Cons k vs)
then obtain c' where c': "k > 0" "k ≤ n" "v c' = k" by auto
with Cons have "dbm_entry_val u (Some c') None (len m (v c') 0 vs)" by auto
moreover have "dbm_entry_val u (Some c) (Some c') (m (v c) (v c'))" using Cons.prems c'
ultimately have "dbm_entry_val u (Some c) None (m (v c) (v c') + len m (v c') 0 vs)"
using dbm_entry_val_add_1 unfolding mult by fastforce
with c' show ?case unfolding DBM_val_bounded_def by simp
qed

lemma DBM_val_bounded_len_3'_aux:
"DBM_val_bounded v u m n ⟹ v c ≤ n ⟹ v d ≤ n ⟹ ∀ k ∈ set vs. k > 0 ∧ k ≤ n ∧ (∃ c. v c = k)
⟹ dbm_entry_val u (Some c) (Some d) (len m (v c) (v d) vs)"
proof (induction vs arbitrary: c)
case Nil thus ?case unfolding DBM_val_bounded_def by auto
next
case (Cons k vs)
then obtain c' where c': "k > 0" "k ≤ n" "v c' = k" by auto
with Cons have "dbm_entry_val u (Some c') (Some d) (len m (v c') (v d) vs)" by auto
moreover have "dbm_entry_val u (Some c) (Some c') (m (v c) (v c'))" using Cons.prems c'
ultimately have "dbm_entry_val u (Some c) (Some d) (m (v c) (v c') + len m (v c') (v d) vs)"
using dbm_entry_val_add_3 unfolding mult by fastforce
with c' show ?case unfolding DBM_val_bounded_def by simp
qed

lemma DBM_val_bounded_len_2'_aux:
"DBM_val_bounded v u m n ⟹ v c ≤ n ⟹ ∀ k ∈ set vs. k > 0 ∧ k ≤ n ∧ (∃ c. v c = k)
⟹ dbm_entry_val u None (Some c) (len m 0 (v c) vs)"
proof (cases vs, goal_cases)
case 1 then show ?thesis unfolding DBM_val_bounded_def by auto
next
case (2 k vs)
then obtain c' where c': "k > 0" "k ≤ n" "v c' = k" by auto
with 2 have "dbm_entry_val u (Some c') (Some c) (len m (v c') (v c) vs)"
using DBM_val_bounded_len_3'_aux by auto
moreover have "dbm_entry_val u None (Some c') (m 0 (v c'))"
using 2 c' by (auto simp add: DBM_val_bounded_def)
ultimately have "dbm_entry_val u None (Some c) (m 0 (v c') + len m (v c') (v c) vs)"
using dbm_entry_val_add_2 unfolding mult by fastforce
with 2(4) c' show ?case unfolding DBM_val_bounded_def by simp
qed

lemma cnt_0_D:
"cnt x xs = 0 ⟹ x ∉ set xs"
apply (induction xs)
apply simp
apply (rename_tac a xs)
apply (case_tac "x = a")
by simp+

lemma cnt_at_most_1_D:
"cnt x (xs @ x # ys) ≤ 1 ⟹ x ∉ set xs ∧ x ∉ set ys"
apply (induction xs)
apply auto[]
using cnt_0_D apply force
apply (rename_tac a xs)
apply (case_tac "a = x")
apply simp
apply simp
done

lemma nat_list_0 [intro]:
"x ∈ set xs ⟹ 0 ∉ set (xs :: nat list) ⟹ x > 0"
by (induction xs) auto

lemma DBM_val_bounded_len':
fixes v
defines "vo ≡ λ k. if k = 0 then None else Some (SOME c. v c = k)"
assumes "DBM_val_bounded v u m n" "cnt 0 (i # j # vs) ≤ 1"
"∀ k ∈ set (i # j # vs). k > 0 ⟶ k ≤ n ∧ (∃ c. v c = k)"
shows "dbm_entry_val u (vo i) (vo j) (len m i j vs)"
proof -
show ?thesis
proof (cases "∀ k ∈ set vs. k > 0")
case True
with assms have *: "∀ k ∈ set vs. k > 0 ∧ k ≤ n ∧ (∃ c. v c = k)" by auto
show ?thesis
proof (cases "i = 0")
case True
then have i: "vo i = None" by (simp add: vo_def)
show ?thesis
proof (cases "j = 0")
case True with assms ‹i = 0› show ?thesis by auto
next
case False
with assms obtain c2 where c2: "j ≤ n" "v c2 = j" "vo j = Some c2"
unfolding vo_def by (fastforce intro: someI)
with ‹i = 0› i DBM_val_bounded_len_2'_aux[OF assms(2) _ *] show ?thesis by auto
qed
next
case False
with assms(4) obtain c1 where c1: "i ≤ n" "v c1 = i" "vo i = Some c1"
unfolding vo_def by (fastforce intro: someI)
show ?thesis
proof (cases "j = 0")
case True
with DBM_val_bounded_len_1'_aux[OF assms(2) _ *] c1 show ?thesis by (auto simp: vo_def)
next
case False
with assms obtain c2 where c2: "j ≤ n" "v c2 = j" "vo j = Some c2"
unfolding vo_def by (fastforce intro: someI)
with c1 DBM_val_bounded_len_3'_aux[OF assms(2) _ _ *] show ?thesis by auto
qed
qed
next
case False
then have "∃ k ∈ set vs. k = 0" by auto
then obtain us ws where vs: "vs = us @ 0 # ws" by (meson split_list_last)
with cnt_at_most_1_D[of 0 "i # j # us"] assms(3) have
"0 ∉ set us" "0 ∉ set ws" "i ≠ 0" "j ≠ 0"
by auto
with vs have vs: "vs = us @ 0 # ws" "∀ k ∈ set us. k > 0" "∀ k ∈ set ws. k > 0" by auto
with assms(4) have v:
"∀k∈set us. 0 < k ∧ k ≤ n ∧ (∃c. v c = k)" "∀k∈set ws. 0 < k ∧ k ≤ n ∧ (∃c. v c = k)"
by auto
from ‹i ≠ 0› ‹j ≠ 0› assms obtain c1 c2 where
c1: "i ≤ n" "v c1 = i" "vo i = Some c1" and c2: "j ≤ n" "v c2 = j" "vo j = Some c2"
unfolding vo_def by (fastforce intro: someI)
with dbm_entry_val_add_4 [OF DBM_val_bounded_len_1'_aux[OF assms(2) _ v(1)] DBM_val_bounded_len_2'_aux[OF assms(2) _ v(2)]]
have "dbm_entry_val u (Some c1) (Some c2) (dbm_add (len m (v c1) 0 us) (len m 0 (v c2) ws))" by auto
moreover from vs have "len m (v c1) (v c2) vs = dbm_add (len m (v c1) 0 us) (len m 0 (v c2) ws)"
ultimately show ?thesis using c1 c2 by auto
qed
qed

lemma DBM_val_bounded_len'1:
fixes v
assumes "DBM_val_bounded v u m n" "0 ∉ set vs" "v c ≤ n"
"∀ k ∈ set vs. k > 0 ⟶ k ≤ n ∧ (∃ c. v c = k)"
shows "dbm_entry_val u (Some c) None (len m (v c) 0 vs)"
using DBM_val_bounded_len_1'_aux[OF assms(1,3)] assms(2,4) by fastforce

lemma DBM_val_bounded_len'2:
fixes v
assumes "DBM_val_bounded v u m n" "0 ∉ set vs" "v c ≤ n"
"∀ k ∈ set vs. k > 0 ⟶ k ≤ n ∧ (∃ c. v c = k)"
shows "dbm_entry_val u None (Some c) (len m 0 (v c) vs)"
using DBM_val_bounded_len_2'_aux[OF assms(1,3)] assms(2,4) by fastforce

lemma DBM_val_bounded_len'3:
fixes v
assumes "DBM_val_bounded v u m n" "cnt 0 vs ≤ 1" "v c1 ≤ n" "v c2 ≤ n"
"∀ k ∈ set vs. k > 0 ⟶ k ≤ n ∧ (∃ c. v c = k)"
shows "dbm_entry_val u (Some c1) (Some c2) (len m (v c1) (v c2) vs)"
proof -
show ?thesis
proof (cases "∀ k ∈ set vs. k > 0")
case True
with assms have "∀ k ∈ set vs. k > 0 ∧ k ≤ n ∧ (∃ c. v c = k)" by auto
with DBM_val_bounded_len_3'_aux[OF assms(1,3,4)] show ?thesis by auto
next
case False
then have "∃ k ∈ set vs. k = 0" by auto
then obtain us ws where vs: "vs = us @ 0 # ws" by (meson split_list_last)
with cnt_at_most_1_D[of 0 "us"] assms(2) have
"0 ∉ set us" "0 ∉ set ws"
by auto
with vs have vs: "vs = us @ 0 # ws" "∀ k ∈ set us. k > 0" "∀ k ∈ set ws. k > 0" by auto
with assms(5) have v:
"∀k∈set us. 0 < k ∧ k ≤ n ∧ (∃c. v c = k)" "∀k∈set ws. 0 < k ∧ k ≤ n ∧ (∃c. v c = k)"
by auto
with dbm_entry_val_add_4 [OF DBM_val_bounded_len_1'_aux[OF assms(1,3) v(1)] DBM_val_bounded_len_2'_aux[OF assms(1,4) v(2)]]
have "dbm_entry_val u (Some c1) (Some c2) (dbm_add (len m (v c1) 0 us) (len m 0 (v c2) ws))" by auto
moreover from vs have "len m (v c1) (v c2) vs = dbm_add (len m (v c1) 0 us) (len m 0 (v c2) ws)"
ultimately show ?thesis by auto
qed
qed

lemma DBM_val_bounded_len'':
fixes v
defines "vo ≡ λ k. if k = 0 then None else Some (SOME c. v c = k)"
assumes "DBM_val_bounded v u m n" "i ≠ 0 ∨ j ≠ 0"
"∀ k ∈ set (i # j # vs). k > 0 ⟶ k ≤ n ∧ (∃ c. v c = k)"
shows "dbm_entry_val u (vo i) (vo j) (len m i j vs)" using assms
proof (induction "length vs" arbitrary: i vs rule: less_induct)
case less
show ?case
proof (cases "∀ k ∈ set vs. k > 0")
case True
with less.prems have *: "∀ k ∈ set vs. k > 0 ∧ k ≤ n ∧ (∃ c. v c = k)" by auto
show ?thesis
proof (cases "i = 0")
case True
then have i: "vo i = None" by (simp add: vo_def)
show ?thesis
proof (cases "j = 0")
case True with less.prems ‹i = 0› show ?thesis by auto
next
case False
with less.prems obtain c2 where c2: "j ≤ n" "v c2 = j" "vo j = Some c2"
unfolding vo_def by (fastforce intro: someI)
with ‹i = 0› i DBM_val_bounded_len_2'_aux[OF less.prems(1) _ *] show ?thesis by auto
qed
next
case False
with less.prems obtain c1 where c1: "i ≤ n" "v c1 = i" "vo i = Some c1"
unfolding vo_def by (fastforce intro: someI)
show ?thesis
proof (cases "j = 0")
case True
with DBM_val_bounded_len_1'_aux[OF less.prems(1) _ *] c1 show ?thesis by (auto simp: vo_def)
next
case False
with less.prems obtain c2 where c2: "j ≤ n" "v c2 = j" "vo j = Some c2"
unfolding vo_def by (fastforce intro: someI)
with c1 DBM_val_bounded_len_3'_aux[OF less.prems(1) _ _ *] show ?thesis by auto
qed
qed
next
case False
then have "∃ us ws. vs = us @ 0 # ws ∧ (∀ k ∈ set us. k > 0)"
proof (induction vs)
case Nil then show ?case by auto
next
case (Cons x vs)
show ?case
proof (cases "x = 0")
case True then show ?thesis by fastforce
next
case False
with Cons.prems have "¬ (∀a∈set vs. 0 < a)" by auto
from Cons.IH[OF this] obtain us ws where "vs = us @ 0 # ws" "∀a∈set us. 0 < a" by auto
with False have "x # vs = (x # us) @ 0 # ws" "∀a∈set (x # us). 0 < a" by auto
then show ?thesis by blast
qed
qed
then obtain us ws where vs: "vs = us @ 0 # ws" "∀ k ∈ set us. k > 0" by blast
then show ?thesis
oops

lemma DBM_val_bounded_len_1: "DBM_val_bounded v u m n ⟹ v c ≤ n ⟹ ∀ c ∈ set cs. v c ≤ n
⟹ dbm_entry_val u (Some c) None (len m (v c) 0 (map v cs))"
proof (induction cs arbitrary: c)
case Nil thus ?case unfolding DBM_val_bounded_def by auto
next
case (Cons c' cs)
hence "dbm_entry_val u (Some c') None (len m (v c') 0 (map v cs))" by auto
moreover have "dbm_entry_val u (Some c) (Some c') (m (v c) (v c'))" using Cons.prems
ultimately have "dbm_entry_val u (Some c) None (m (v c) (v c') + len m (v c') 0 (map v cs))"
using dbm_entry_val_add_1 unfolding mult by fastforce
thus ?case unfolding DBM_val_bounded_def by simp
qed

lemma DBM_val_bounded_len_3: "DBM_val_bounded v u m n ⟹ v c ≤ n ⟹ v d ≤ n ⟹ ∀ c ∈ set cs. v c ≤ n
⟹ dbm_entry_val u (Some c) (Some d) (len m (v c) (v d) (map v cs))"
proof (induction cs arbitrary: c)
case Nil thus ?case unfolding DBM_val_bounded_def by auto
next
case (Cons c' cs)
hence "dbm_entry_val u (Some c') (Some d) (len m (v c') (v d) (map v cs))" by auto
moreover have "dbm_entry_val u (Some c) (Some c') (m (v c) (v c'))" using Cons.prems
ultimately have "dbm_entry_val u (Some c) (Some d) (m (v c) (v c') + len m (v c') (v d) (map v cs))"
using dbm_entry_val_add_3 unfolding mult by fastforce
thus ?case unfolding DBM_val_bounded_def by simp
qed

lemma DBM_val_bounded_len_2: "DBM_val_bounded v u m n ⟹ v c ≤ n ⟹ ∀ c ∈ set cs. v c ≤ n
⟹ dbm_entry_val u None (Some c) (len m 0 (v c) (map v cs))"
proof (cases cs, goal_cases)
case 1 thus ?thesis unfolding DBM_val_bounded_def by auto
next
case (2 c' cs)
hence "dbm_entry_val u (Some c') (Some c) (len m (v c') (v c) (map v cs))"
using DBM_val_bounded_len_3 by auto
moreover have "dbm_entry_val u None (Some c') (m 0 (v c'))"
using 2 by (simp add: DBM_val_bounded_def)
ultimately have "dbm_entry_val u None (Some c) (m 0 (v c') + len m (v c') (v c) (map v cs))"
using dbm_entry_val_add_2 unfolding mult by fastforce
thus ?case using 2(4) unfolding DBM_val_bounded_def by simp
qed

end