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]:
  "([rd]u) c = d" if "c  set r"
  using that by (induction r) auto

lemma clock_set_id[simp]:
  "([rd]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