Theory Difference_Bound_Matrices.Zones

subsection ‹Zones and DBMs›
theory Zones
  imports DBM
begin

type_synonym ('c, 't) zone = "('c, 't) cval set"

type_synonym ('c, 't) cval = "'c ⇒ 't"

definition cval_add :: "('c,'t) cval ⇒ 't::plus ⇒ ('c,'t) cval" (infixr ‹⊕› 64)
where
  "u ⊕ d = (λ x. u x + d)"

definition zone_delay :: "('c, ('t::time)) zone ⇒ ('c, 't) zone"
(‹_⇧↑› [71] 71)
where
  "Z⇧↑ = {u ⊕ d|u d. u ∈ Z ∧ d ≥ (0::'t)}"

fun clock_set :: "'c list ⇒ 't::time ⇒ ('c,'t) cval ⇒ ('c,'t) cval"
where
  "clock_set [] _ u = u" |
  "clock_set (c#cs) t u = (clock_set cs t u)(c:=t)"

abbreviation clock_set_abbrv :: "'c list ⇒ 't::time ⇒ ('c,'t) cval ⇒ ('c,'t) cval"
(‹[_→_]_› [65,65,65] 65)
where
  "[r → t]u ≡ clock_set r t u"

definition zone_set :: "('c, 't::time) zone ⇒ 'c list ⇒ ('c, 't) zone"
(‹_⇘_ → 0⇙› [71] 71)
where
  "zone_set Z r = {[r → (0::'t)]u | u . u ∈ Z}"

lemma clock_set_set[simp]:
  "([r→d]u) c = d" if "c ∈ set r"
  using that by (induction r) auto

lemma clock_set_id[simp]:
  "([r→d]u) c = u c" if "c ∉ set r"
  using that by (induction r) auto

definition DBM_zone_repr :: "('t::time) DBM ⇒ ('c ⇒ nat) ⇒ nat ⇒ ('c, 't :: time) zone"
(‹[_]⇘_,_⇙› [72,72,72] 72)
where
  "[M]⇘v,n⇙ = {u . DBM_val_bounded v u M n}"

lemma dbm_entry_val_mono1:
  "dbm_entry_val u (Some c) (Some c') b ⟹ b ≼ b' ⟹ dbm_entry_val u (Some c) (Some c') b'"
proof (induction b, goal_cases)
  case 1 thus ?case using le_dbm_le le_dbm_lt by - (cases b'; fastforce)
next
  case 2 thus ?case using lt_dbm_le lt_dbm_lt by (cases b'; fastforce)
next
  case 3 thus ?case unfolding dbm_le_def by auto
qed

lemma dbm_entry_val_mono2:
  "dbm_entry_val u None (Some c) b ⟹ b ≼ b' ⟹ dbm_entry_val u None (Some c) b'"
proof (induction b, goal_cases)
  case 1 thus ?case using le_dbm_le le_dbm_lt by - (cases b'; fastforce)
next
  case 2 thus ?case using lt_dbm_le lt_dbm_lt by (cases b'; fastforce)
next
  case 3 thus ?case unfolding dbm_le_def by auto
qed

lemma dbm_entry_val_mono3:
  "dbm_entry_val u (Some c) None b ⟹ b ≼ b' ⟹ dbm_entry_val u (Some c) None b'"
proof (induction b, goal_cases)
  case 1 thus ?case using le_dbm_le le_dbm_lt by - (cases b'; fastforce)
next
  case 2 thus ?case using lt_dbm_le lt_dbm_lt by (cases b'; fastforce)
next
  case 3 thus ?case unfolding dbm_le_def by auto
qed

lemmas dbm_entry_val_mono = dbm_entry_val_mono1 dbm_entry_val_mono2 dbm_entry_val_mono3

lemma DBM_le_subset:
  "∀ i j. i ≤ n ⟶ j ≤ n ⟶ M i j ≼ M' i j ⟹ u ∈ [M]⇘v,n⇙ ⟹ u ∈ [M']⇘v,n⇙"
proof -
  assume A: "∀i j. i ≤ n ⟶ j ≤ n ⟶ M i j ≼ M' i j" "u ∈ [M]⇘v,n⇙"
  hence "DBM_val_bounded v u M n" by (simp add: DBM_zone_repr_def)
  with A(1) have "DBM_val_bounded v u M' n" unfolding DBM_val_bounded_def
  proof (safe, goal_cases)
    case 1 from this(1,2) show ?case unfolding less_eq[symmetric] by fastforce
  next
    case (2 c)
    hence "dbm_entry_val u None (Some c) (M 0 (v c))" "M 0 (v c) ≼ M' 0 (v c)" by auto
    thus ?case using dbm_entry_val_mono2 by fast
  next
    case (3 c)
    hence "dbm_entry_val u (Some c) None (M (v c) 0)" "M (v c) 0 ≼ M' (v c) 0" by auto
    thus ?case using dbm_entry_val_mono3 by fast
  next
    case (4 c1 c2)
    hence "dbm_entry_val u (Some c1) (Some c2) (M (v c1) (v c2))" "M (v c1) (v c2) ≼ M' (v c1) (v c2)"
    by auto
    thus ?case using dbm_entry_val_mono1 by fast
  qed
  thus "u ∈ [M']⇘v,n⇙" by (simp add: DBM_zone_repr_def)
qed

end