Theory 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}›).›
definition 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_is_extra:
  "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}^+›).›
definition extra_lup ::
  "('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 extrapolations_diag_preservation:
  "extra_lu M L U n i i = M i i" "extra_lup M L U n i i = M i i" "norm M k n i i = M i i"
  unfolding extra_lu_def extra_lup_def norm_def Let_def by auto›

lemma
  assumes "∀i ≤ n. i > 0 ⟶ M 0 i ≤ 0" "∀i ≤ n. U i ≥ 0"
  shows
    extra_lu_lower_bounds:  "∀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
    extra_lup_lower_bounds: "∀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 extra_lu_le_extra_lup:
  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 extra_lu_subs_extra_lup:
  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 extra_lu_mono:
  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 extra_lu_default_preservation:
  "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 extra_lu_finite:
  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