Theory Difference_Bound_Matrices.DBM_Normalization
section ‹Extrapolation of DBMs›
theory DBM_Normalization
imports
DBM_Basics
DBM_Misc
"HOL-Eisbach.Eisbach"
begin
text ‹NB: The journal paper on extrapolations based on lower and upper bounds
\<^cite>‹BehrmannBLP06› provides slightly incorrect definitions that would always set
(lower) bounds of the form ‹M 0 i› to ‹∞›.
To fix this, we use two invariants that can also be found in TChecker's DBM library, for instance:
▸ Lower bounds are always nonnegative, i.e.\ ‹∀i ≤ n. M 0 i ≤ 0›
(see ‹extra_lup_lower_bounds›).
▸ Entries to the diagonal is always normalized to ‹Le 0›, ‹Lt 0› or ‹∞›. This makes it again
obvious that the set of normalized DBMs is finite.
›
lemmas dbm_less_simps[simp] = dbm_lt_code_simps[folded DBM.less]
lemma dbm_less_eq_simps[simp]:
"Le a ≤ Le b ⟷ a ≤ b"
"Le a ≤ Lt b ⟷ a < b"
"Lt a ≤ Le b ⟷ a ≤ b"
"Lt a ≤ Lt b ⟷ a ≤ b"
unfolding less_eq dbm_le_def by auto
lemma Le_less_Lt[simp]: "Le x < Lt x ⟷ False"
using leD by blast
subsection ‹Classical extrapolation›
text ‹This is the implementation of the classical extrapolation operator (‹Extra⇩M›).›
fun norm_upper :: "('t::linorder) DBMEntry ⇒ 't ⇒ 't DBMEntry"
where
"norm_upper e t = (if Le t ≺ e then ∞ else e)"
fun norm_lower :: "('t::linorder) DBMEntry ⇒ 't ⇒ 't DBMEntry"
where
"norm_lower e t = (if e ≺ Lt t then Lt t else e)"
definition
"norm_diag e = (if e ≺ Le 0 then Lt 0 else if e = Le 0 then e else ∞)"
text ‹
Note that literature pretends that ‹𝟬› would have a bound of negative infinity in ‹k›
and thus defines normalization uniformly. The easiest way to get around this seems to explicate
this in the definition as below.
›
definition norm :: "('t :: linordered_ab_group_add) DBM ⇒ (nat ⇒ 't) ⇒ nat ⇒ 't DBM"
where
"norm M k n ≡ λi j.
let ub = if i > 0 then k i else 0 in
let lb = if j > 0 then - k j else 0 in
if i ≤ n ∧ j ≤ n then
if i ≠ j then norm_lower (norm_upper (M i j) ub) lb else norm_diag (M i j)
else M i j
"
subsection ‹Extrapolations based on lower and upper bounds›
text ‹This is the implementation of the LU-bounds based extrapolation operation (‹Extra_{LU}›).›
::
"('t :: linordered_ab_group_add) DBM ⇒ (nat ⇒ 't) ⇒ (nat ⇒ 't) ⇒ nat ⇒ 't DBM"
where
"extra_lu M l u n ≡ λi j.
let ub = if i > 0 then l i else 0 in
let lb = if j > 0 then - u j else 0 in
if i ≤ n ∧ j ≤ n then
if i ≠ j then norm_lower (norm_upper (M i j) ub) lb else norm_diag (M i j)
else M i j
"
lemma :
"norm M k n = extra_lu M k k n"
unfolding norm_def extra_lu_def ..
text ‹This is the implementation of the LU-bounds based extrapolation operation (‹Extra_{LU}^+›).›
::
"('t :: linordered_ab_group_add) DBM ⇒ (nat ⇒ 't) ⇒ (nat ⇒ 't) ⇒ nat ⇒ 't DBM"
where
"extra_lup M l u n ≡ λi j.
let ub = if i > 0 then Lt (l i) else Le 0;
lb = if j > 0 then Lt (- u j) else Lt 0
in
if i ≤ n ∧ j ≤ n then
if i ≠ j then
if ub ≺ M i j then ∞
else if i > 0 ∧ M 0 i ≺ Lt (- l i) then ∞
else if i > 0 ∧ M 0 j ≺ lb then ∞
else if i = 0 ∧ M 0 j ≺ lb then Lt (- u j)
else M i j
else norm_diag (M i j)
else M i j
"
method csimp = (clarsimp simp: extra_lup_def Let_def DBM.less[symmetric] not_less any_le_inf neutral)
method solve = csimp?; safe?; (csimp | meson Lt_le_LeI le_less le_less_trans less_asym'); fail
lemma
assumes "∀i ≤ n. i > 0 ⟶ M 0 i ≤ 0" "∀i ≤ n. U i ≥ 0"
shows
: "∀i ≤ n. i > 0 ⟶ extra_lu M L U n 0 i ≤ 0" and
norm_lower_bounds: "∀i ≤ n. i > 0 ⟶ norm M U n 0 i ≤ 0" and
: "∀i ≤ n. i > 0 ⟶ extra_lup M L U n 0 i ≤ 0"
using assms unfolding extra_lu_def norm_def by - (csimp; force)+
lemma :
assumes canonical: "canonical M n"
and canonical_lower_bounds: "∀i ≤ n. i > 0 ⟶ M 0 i ≤ 0"
shows "extra_lu M l u n i j ≤ extra_lup M l u n i j"
proof -
have "M 0 j ≤ M i j" if "i ≤ n" "j ≤ n" "i > 0"
proof -
have "M 0 i ≤ 0"
using canonical_lower_bounds ‹i ≤ n› ‹i > 0› by simp
then have "M 0 i + M i j ≤ M i j"
by (simp add: add_decreasing)
also have "M 0 j ≤ M 0 i + M i j"
using canonical that by auto
finally (xtrans) show ?thesis .
qed
then show ?thesis
unfolding extra_lu_def Let_def by (cases "i ≤ n"; cases "j ≤ n") (simp; safe?; solve)+
qed
lemma :
assumes canonical: "canonical M n" and canonical_lower_bounds: "∀i ≤ n. i > 0 ⟶ M 0 i ≤ 0"
shows "[extra_lu M L U n]⇘v,n⇙ ⊆ [extra_lup M L U n]⇘v,n⇙"
using assms
by (auto intro: extra_lu_le_extra_lup simp: DBM.less_eq[symmetric] elim!: DBM_le_subset[rotated])
subsection ‹Extrapolations are widening operators›
lemma :
assumes "∀c. v c > 0" "u ∈ [M]⇘v,n⇙"
shows "u ∈ [extra_lu M L U n]⇘v,n⇙" (is "u ∈ [?M2]⇘v,n⇙")
proof -
note A = assms
note M1 = A(2)[unfolded DBM_zone_repr_def DBM_val_bounded_def]
show ?thesis
unfolding DBM_zone_repr_def DBM_val_bounded_def
proof safe
show "Le 0 ≼ ?M2 0 0"
using A unfolding extra_lu_def DBM_zone_repr_def DBM_val_bounded_def dbm_le_def norm_diag_def
by auto
next
fix c assume "v c ≤ n"
with M1 have M1: "dbm_entry_val u None (Some c) (M 0 (v c))" by auto
from ‹v c ≤ n› A have *:
"?M2 0 (v c) = norm_lower (norm_upper (M 0 (v c)) 0) (- U (v c))"
unfolding extra_lu_def by auto
show "dbm_entry_val u None (Some c) (?M2 0 (v c))"
proof (cases "M 0 (v c) ≺ Lt (- U (v c))")
case True
show ?thesis
proof (cases "Le 0 ≺ M 0 (v c)")
case True with * show ?thesis by auto
next
case False
with * True have "?M2 0 (v c) = Lt (- U (v c))" by auto
moreover from True dbm_entry_val_mono2[OF M1] have
"dbm_entry_val u None (Some c) (Lt (- U (v c)))"
by auto
ultimately show ?thesis by auto
qed
next
case False
show ?thesis
proof (cases "Le 0 ≺ M 0 (v c)")
case True with * show ?thesis by auto
next
case F: False
with M1 * False show ?thesis by auto
qed
qed
next
fix c assume "v c ≤ n"
with M1 have M1: "dbm_entry_val u (Some c) None (M (v c) 0)" by auto
from ‹v c ≤ n› A have *:
"?M2 (v c) 0 = norm_lower (norm_upper (M (v c) 0) (L (v c))) 0"
unfolding extra_lu_def by auto
show "dbm_entry_val u (Some c) None (?M2 (v c) 0)"
proof (cases "Le (L (v c)) ≺ M (v c) 0")
case True
with A(1,2) ‹v c ≤ n› have "?M2 (v c) 0 = ∞" unfolding extra_lu_def by auto
then show ?thesis by auto
next
case False
show ?thesis
proof (cases "M (v c) 0 ≺ Lt 0")
case True with False * dbm_entry_val_mono3[OF M1] show ?thesis by auto
next
case F: False
with M1 * False show ?thesis by auto
qed
qed
next
fix c1 c2 assume "v c1 ≤ n" "v c2 ≤ n"
with M1 have M1: "dbm_entry_val u (Some c1) (Some c2) (M (v c1) (v c2))" by auto
show "dbm_entry_val u (Some c1) (Some c2) (?M2 (v c1) (v c2))"
proof (cases "v c1 = v c2")
case True
with M1 show ?thesis
by (auto simp: extra_lu_def norm_diag_def dbm_entry_val.simps dbm_lt.simps)
(meson diff_less_0_iff_less le_less_trans less_le_trans)+
next
case False
show ?thesis
proof (cases "Le (L (v c1)) ≺ M (v c1) (v c2)")
case True
with A(1,2) ‹v c1 ≤ n› ‹v c2 ≤ n› ‹v c1 ≠ v c2› have "?M2 (v c1) (v c2) = ∞"
unfolding extra_lu_def by auto
then show ?thesis by auto
next
case False
with A(1,2) ‹v c1 ≤ n› ‹v c2 ≤ n› ‹v c1 ≠ v c2› have *:
"?M2 (v c1) (v c2) = norm_lower (M (v c1) (v c2)) (- U (v c2))"
unfolding extra_lu_def by auto
show ?thesis
proof (cases "M (v c1) (v c2) ≺ Lt (- U (v c2))")
case True
with dbm_entry_val_mono1[OF M1] have
"dbm_entry_val u (Some c1) (Some c2) (Lt (- U (v c2)))"
by auto
then have "u c1 - u c2 < - U (v c2)" by auto
with * True show ?thesis by auto
next
case False with M1 * show ?thesis by auto
qed
qed
qed
qed
qed
lemma norm_mono:
assumes "∀c. v c > 0" "u ∈ [M]⇘v,n⇙"
shows "u ∈ [norm M k n]⇘v,n⇙"
using assms unfolding norm_is_extra by (rule extra_lu_mono)
subsection ‹Finiteness of extrapolations›
abbreviation "dbm_default M n ≡ (∀ i > n. ∀ j. M i j = 0) ∧ (∀ j > n. ∀ i. M i j = 0)"
lemma norm_default_preservation:
"dbm_default M n ⟹ dbm_default (norm M k n) n"
by (simp add: norm_def norm_diag_def DBM.neutral dbm_lt.simps)
lemma :
"dbm_default M n ⟹ dbm_default (extra_lu M L U n) n"
by (simp add: extra_lu_def norm_diag_def DBM.neutral dbm_lt.simps)
instance int :: linordered_cancel_ab_monoid_add by (standard; simp)
lemmas finite_subset_rev[intro?] = finite_subset[rotated]
lemmas [intro?] = finite_subset
lemma :
fixes L U :: "nat ⇒ nat"
shows "finite {extra_lu M L U n | M. dbm_default M n}"
proof -
let ?u = "Max {L i | i. i ≤ n}" let ?l = "- Max {U i | i. i ≤ n}"
let ?S = "(Le ` {d :: int. ?l ≤ d ∧ d ≤ ?u}) ∪ (Lt ` {d :: int. ?l ≤ d ∧ d ≤ ?u}) ∪ {Le 0, Lt 0, ∞}"
from finite_set_of_finite_funs2[of "{0..n}" "{0..n}" ?S] have fin:
"finite {f. ∀x y. (x ∈ {0..n} ∧ y ∈ {0..n} ⟶ f x y ∈ ?S)
∧ (x ∉ {0..n} ⟶ f x y = 0) ∧ (y ∉ {0..n} ⟶ f x y = 0)}" (is "finite ?R")
by auto
{ fix M :: "int DBM" assume A: "dbm_default M n"
let ?M = "extra_lu M L U n"
from extra_lu_default_preservation[OF A] have A: "dbm_default ?M n" .
{ fix i j assume "i ∈ {0..n}" "j ∈ {0..n}"
then have B: "i ≤ n" "j ≤ n"
by auto
have "?M i j ∈ ?S"
proof (cases "?M i j ∈ {Le 0, Lt 0, ∞}")
case True then show ?thesis
by auto
next
case F: False
note not_inf = this
have "?l ≤ get_const (?M i j) ∧ get_const (?M i j) ≤ ?u"
proof (cases "i = 0")
case True
show ?thesis
proof (cases "j = 0")
case True
with ‹i = 0› A F show ?thesis
unfolding extra_lu_def by (auto simp: neutral norm_diag_def)
next
case False
with ‹i = 0› B not_inf have "?M i j ≤ Le 0" "Lt (-int (U j)) ≤ ?M i j"
unfolding extra_lu_def by (auto simp: Let_def less[symmetric] intro: any_le_inf)
with not_inf have "get_const (?M i j) ≤ 0" "-U j ≤ get_const (?M i j)"
by (cases "?M i j"; auto)+
moreover from ‹j ≤ n› have "- U j ≥ ?l"
by (auto intro: Max_ge)
ultimately show ?thesis
by auto
qed
next
case False
then have "i > 0" by simp
show ?thesis
proof (cases "j = 0")
case True
with ‹i > 0› A(1) B not_inf have "Lt 0 ≤ ?M i j" "?M i j ≤ Le (int (L i))"
unfolding extra_lu_def by (auto simp: Let_def less[symmetric] intro: any_le_inf)
with not_inf have "0 ≤ get_const (?M i j)" "get_const (?M i j) ≤ L i"
by (cases "?M i j"; auto)+
moreover from ‹i ≤ n› have "L i ≤ ?u"
by (auto intro: Max_ge)
ultimately show ?thesis
by auto
next
case False
with ‹i > 0› A(1) B not_inf F have
"Lt (-int (U j)) ≤ ?M i j" "?M i j ≤ Le (int (L i))"
unfolding extra_lu_def
by (auto simp: Let_def less[symmetric] neutral norm_diag_def
intro: any_le_inf split: if_split_asm)
with not_inf have "- U j ≤ get_const (?M i j)" "get_const (?M i j) ≤ L i"
by (cases "?M i j"; auto)+
moreover from ‹i ≤ n› ‹j ≤ n› have "?l ≤ - U j" "L i ≤ ?u"
by (auto intro: Max_ge)
ultimately show ?thesis
by auto
qed
qed
then show ?thesis by (cases "?M i j"; auto elim: Ints_cases)
qed
} moreover
{ fix i j assume "i ∉ {0..n}"
with A have "?M i j = 0" by auto
} moreover
{ fix i j assume "j ∉ {0..n}"
with A have "?M i j = 0" by auto
} moreover note the = calculation
} then have "{extra_lu M L U n | M. dbm_default M n} ⊆ ?R"
by blast
with fin show ?thesis ..
qed
lemma normalized_integral_dbms_finite:
"finite {norm M (k :: nat ⇒ nat) n | M. dbm_default M n}"
unfolding norm_is_extra by (rule extra_lu_finite)
end