Theory Timed_Automata.DBM_Normalization
section ‹Normalization of DBMs›
theory DBM_Normalization
imports DBM_Basics
begin
text ‹This is the implementation of the common approximation operation.›
fun norm_upper :: "('t::time) DBMEntry ⇒ 't ⇒ ('t::time) DBMEntry"
where
"norm_upper e t = (if Le t ≺ e then ∞ else e)"
fun norm_lower :: "('t::time) DBMEntry ⇒ 't ⇒ ('t::time) DBMEntry"
where
"norm_lower e t = (if e ≺ Lt t then Lt t else e)"
text ‹
Note that literature pretends that ‹𝟬› would have some (presumably infinite bound) 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::time) 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 norm_lower (norm_upper (M i j) ub) lb else M i j
"
section ‹Normalization is a Widening Operator›
lemma norm_mono:
assumes "∀c. v c > 0" "u ∈ [M]⇘v,n⇙"
shows "u ∈ [norm M k 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
proof (unfold DBM_zone_repr_def DBM_val_bounded_def, auto)
show "Le 0 ≼ ?M2 0 0"
using A unfolding norm_def DBM_zone_repr_def DBM_val_bounded_def dbm_le_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) (- k (v c))"
unfolding norm_def by auto
show "dbm_entry_val u None (Some c) (?M2 0 (v c))"
proof (cases "M 0 (v c) ≺ Lt (- k (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 (- k (v c))" by auto
moreover from True dbm_entry_val_mono_2[OF M1] have
"dbm_entry_val u None (Some c) (Lt (- k (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) (k (v c))) 0"
unfolding norm_def by auto
show "dbm_entry_val u (Some c) None (?M2 (v c) 0)"
proof (cases "Le (k (v c)) ≺ M (v c) 0")
case True
with A(1,2) ‹v c ≤ n› have "?M2 (v c) 0 = ∞" unfolding norm_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_mono_3[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
then show "dbm_entry_val u (Some c1) (Some c2) (?M2 (v c1) (v c2))"
proof (cases "Le (k (v c1)) ≺ M (v c1) (v c2)")
case True
with A(1,2) ‹v c1 ≤ n› ‹v c2 ≤ n› have "?M2 (v c1) (v c2) = ∞" unfolding norm_def by auto
then show ?thesis by auto
next
case False
with A(1,2) ‹v c1 ≤ n› ‹v c2 ≤ n› have
*: "?M2 (v c1) (v c2) = norm_lower (M (v c1) (v c2)) (- k (v c2))"
unfolding norm_def by auto
show ?thesis
proof (cases "M (v c1) (v c2) ≺ Lt (- k (v c2))")
case True
with dbm_entry_val_mono_1[OF M1] have
"dbm_entry_val u (Some c1) (Some c2) (Lt (- k (v c2)))"
by auto
then have "u c1 - u c2 < - k (v c2)" by auto
with * True show ?thesis by auto
next
case False with M1 * show ?thesis by auto
qed
qed
qed
qed
end