Theory 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