Theory TA_DBM_Operations

section ‹From Clock Constraints to DBMs›

theory TA_DBM_Operations
  imports Timed_Automata Difference_Bound_Matrices.DBM_Operations
begin

fun abstra ::
  "('c, 't::{linordered_cancel_ab_monoid_add,uminus}) acconstraint  't DBM  ('c  nat)  't DBM"
where
  "abstra (EQ c d) M v =
    (λ i j . if i = 0  j = v c then min (M i j) (Le (-d)) else if i = v c  j = 0 then min (M i j) (Le d) else M i j)" |
  "abstra (LT c d) M v =
    (λ i j . if i = v c  j = 0 then min (M i j) (Lt d) else M i j)" |
  "abstra (LE c d) M v =
    (λ i j . if i = v c  j = 0 then min (M i j) (Le d) else M i j)" |
  "abstra (GT c d) M v =
    (λ i j. if i = 0  j = v c then min (M i j) (Lt (- d)) else M i j)" |
  "abstra (GE c d) M v =
    (λ i j. if i = 0  j = v c then min (M i j) (Le (- d)) else M i j)"

fun abstr ::"('c, 't::{linordered_cancel_ab_monoid_add,uminus}) cconstraint  't DBM  ('c  nat)  't DBM"
where
  "abstr cc M v = fold (λ ac M. abstra ac M v) cc M"

(* XXX Move *)
lemma collect_clks_Cons[simp]:
  "collect_clks (ac # cc) = insert (constraint_clk ac) (collect_clks cc)"
unfolding collect_clks_def by auto

lemma abstr_id1:
  "c  collect_clks cc  clock_numbering' v n   c  collect_clks cc. v c  n
     abstr cc M v 0 (v c) = M 0 (v c)"
apply (induction cc arbitrary: M c)
apply (simp; fail)
 subgoal for a
  apply simp
  apply (cases a)
 by auto
done

lemma abstr_id2:
  "c  collect_clks cc  clock_numbering' v n   c  collect_clks cc. v c  n
     abstr cc M v (v c) 0 = M (v c) 0"
apply (induction cc arbitrary: M c)
apply (simp; fail)
 subgoal for a
  apply simp
  apply (cases a)
 by auto
done

text ‹
  This lemma is trivial because we constrained our theory to difference constraints.
›

lemma abstra_id3:
  assumes "clock_numbering v"
  shows "abstra ac M v (v c1) (v c2) = M (v c1) (v c2)"
proof -
  have "c. v c = 0  False"
  proof -
    fix c assume "v c = 0"
    moreover from assms have "v c > 0" by auto
    ultimately show False by linarith
  qed
  then show ?thesis by (cases ac) auto
qed

lemma abstr_id3:
  "clock_numbering v  abstr cc M v (v c1) (v c2) = M (v c1) (v c2)"
by (induction cc arbitrary: M) (auto simp add: abstra_id3)

lemma abstra_id3':
  assumes "c. 0 < v c"
  shows "abstra ac M v 0 0 = M 0 0"
proof -
  have "c. v c = 0  False"
  proof -
    fix c assume "v c = 0"
    moreover from assms have "v c > 0" by auto
    ultimately show False by linarith
  qed
  then show ?thesis by (cases ac) auto
qed

lemma abstr_id3':
  "clock_numbering v  abstr cc M v 0 0 = M 0 0"
by (induction cc arbitrary: M) (auto simp add: abstra_id3')

(* XXX Move *)
lemma clock_numberingD:
  assumes "clock_numbering v" "v c = 0"
  shows "A"
proof-
  from assms(1) have "v c > 0" by auto
  with v c = 0 show ?thesis by linarith
qed

lemma dbm_abstra_soundness:
  "u a ac; u ⊢⇘v,nM; clock_numbering' v n; v (constraint_clk ac)  n
     DBM_val_bounded v u (abstra ac M v) n"
proof (unfold DBM_val_bounded_def, auto, goal_cases)
  case prems: 1
  from abstra_id3'[OF this(4)] have "abstra ac M v 0 0 = M 0 0" .
  with prems show ?case unfolding dbm_le_def by auto
next
  case prems: (2 c)
  then have "clock_numbering' v n" by auto
  note A = prems(1) this prems(6,3)
  let ?c = "constraint_clk ac"
  show ?case
  proof (cases "c = ?c")
    case True
    then show ?thesis using prems by (cases ac) (auto split: split_min intro: clock_numberingD)
  next
    case False
    then show ?thesis using A(3) prems by (cases ac) auto
  qed
next
  case prems: (3 c)
  then have "clock_numbering' v n" by auto
  then have gt0: "v c > 0" by auto
  let ?c = "constraint_clk ac"
  show ?case
  proof (cases "c = ?c")
    case True
    then show ?thesis using prems gt0 by (cases ac) (auto split: split_min intro: clock_numberingD)
  next
    case False
    then show ?thesis using clock_numbering' v n prems by (cases ac) auto
  qed
next
  text ‹Trivial because of missing difference constraints›
  case prems: (4 c1 c2)
  from abstra_id3[OF this(4)] have "abstra ac M v (v c1) (v c2) = M (v c1) (v c2)" by auto
  with prems show ?case by auto
qed

lemma dbm_abstr_soundness':
  "u  cc; u ⊢⇘v,nM; clock_numbering' v n;  c  collect_clks cc. v c  n
     DBM_val_bounded v u (abstr cc M v) n"
  by (induction cc arbitrary: M) (auto simp: clock_val_def dest: dbm_abstra_soundness)

lemmas dbm_abstr_soundness = dbm_abstr_soundness'[OF _ DBM_triv]

lemma dbm_abstra_completeness:
  "DBM_val_bounded v u (abstra ac M v) n; c. v c > 0; v (constraint_clk ac)  n
     u a ac"
proof (cases ac, goal_cases)
  case prems: (1 c d)
  then have "v c  n" by auto
  with prems(1,4) have "dbm_entry_val u (Some c) None ((abstra (LT c d) M v) (v c) 0)"
  by (auto simp: DBM_val_bounded_def)
  moreover from prems(2) have "v c > 0" by auto
  ultimately show ?case using prems(4) by (auto dest: dbm_entry_dbm_min3)
next
  case prems: (2 c d)
  from this have "v c  n" by auto
  with prems(1,4) have "dbm_entry_val u (Some c) None ((abstra (LE c d) M v) (v c) 0)"
  by (auto simp: DBM_val_bounded_def)
  moreover from prems(2) have "v c > 0" by auto
  ultimately show ?case using prems(4) by (auto dest: dbm_entry_dbm_min3)
next
  case prems: (3 c d)
  from this have c: "v c > 0" "v c  n" by auto
  with prems(1,4) have B:
    "dbm_entry_val u (Some c) None ((abstra (EQ c d) M v) (v c) 0)"
    "dbm_entry_val u None (Some c) ((abstra (EQ c d) M v) 0 (v c))"
  by (auto simp: DBM_val_bounded_def)
  from c B have "u c  d" "- u c  -d" by (auto dest: dbm_entry_dbm_min2 dbm_entry_dbm_min3)
  with prems(4) show ?case by auto
next
  case prems: (4 c d)
  from this have "v c  n" by auto
  with prems(1,4) have "dbm_entry_val u None (Some c) ((abstra (GT c d) M v) 0 (v c))"
  by (auto simp: DBM_val_bounded_def)
  moreover from prems(2) have "v c > 0" by auto
  ultimately show ?case using prems(4) by (auto dest!: dbm_entry_dbm_min2)
next
  case prems: (5 c d)
  from this have "v c  n" by auto
  with prems(1,4) have "dbm_entry_val u None (Some c) ((abstra (GE c d) M v) 0 (v c))"
  by (auto simp: DBM_val_bounded_def)
  moreover from prems(2) have "v c > 0" by auto
  ultimately show ?case using prems(4) by (auto dest!: dbm_entry_dbm_min2)
qed

lemma abstra_mono:
  "abstra ac M v i j  M i j"
by (cases ac) auto

lemma abstra_subset:
  "[abstra ac M v]⇘v,n [M]⇘v,n⇙"
using abstra_mono
 apply (simp add: less_eq)
 apply safe
by (rule DBM_le_subset; force)

lemma abstr_subset:
  "[abstr cc M v]⇘v,n [M]⇘v,n⇙"
apply (induction cc arbitrary: M)
 apply (simp; fail)
using abstra_subset by fastforce

(* Move to DBM operations *)
lemma dbm_abstra_zone_eq:
  assumes "clock_numbering' v n" "v (constraint_clk ac)  n"
  shows "[abstra ac M v]⇘v,n= {u. u a ac}  [M]⇘v,n⇙"
  apply safe
  subgoal
    unfolding DBM_zone_repr_def using assms by (auto intro: dbm_abstra_completeness)
  subgoal
    using abstra_subset by blast
  subgoal
    unfolding DBM_zone_repr_def using assms by (auto intro: dbm_abstra_soundness)
  done

(* XXX Move *)
lemma [simp]:
  "u  []"
  by (force simp: clock_val_def)

lemma clock_val_Cons:
  assumes "u a ac" "u  cc"
  shows "u  (ac # cc)"
  using assms by (induction cc) (auto simp: clock_val_def)

lemma abstra_commute:
  "abstra ac1 (abstra ac2 M v) v = abstra ac2 (abstra ac1 M v) v"
  by (cases ac1; cases ac2; fastforce simp: min.commute min.left_commute clock_val_def)

lemma dbm_abstr_completeness_aux:
  "DBM_val_bounded v u (abstr cc (abstra ac M v) v) n; c. v c > 0; v (constraint_clk ac)  n
     u a ac"
apply (induction cc arbitrary: M)
 apply (auto intro: dbm_abstra_completeness; fail)
apply simp
apply (subst (asm) abstra_commute)
by auto

lemma dbm_abstr_completeness:
  "DBM_val_bounded v u (abstr cc M v) n; c. v c > 0;  c  collect_clks cc. v c  n
     u  cc"
apply (induction cc arbitrary: M)
 apply (simp; fail)
apply (rule clock_val_Cons)
apply (rule dbm_abstr_completeness_aux)
by auto

lemma dbm_abstr_zone_eq:
  assumes "clock_numbering' v n" "ccollect_clks cc. v c  n"
  shows "[abstr cc (λi j. ) v]⇘v,n= {u. u  cc}"
using dbm_abstr_soundness dbm_abstr_completeness assms unfolding DBM_zone_repr_def by metis

lemma dbm_abstr_zone_eq2:
  assumes "clock_numbering' v n" "ccollect_clks cc. v c  n"
  shows "[abstr cc M v]⇘v,n= [M]⇘v,n {u. u  cc}"
apply standard
 apply (rule Int_greatest)
  apply (rule abstr_subset)
 unfolding DBM_zone_repr_def
 apply safe
 apply (rule dbm_abstr_completeness)
   using assms apply auto[3]
apply (rule dbm_abstr_soundness')
using assms by auto


abbreviation global_clock_numbering ::
  "('a, 'c, 't, 's) ta  ('c  nat)  nat  bool"
where
  "global_clock_numbering A v n 
    clock_numbering' v n  ( c  clk_set A. v c  n)  (kn. k > 0  (c. v c = k))"

lemma dbm_int_all_abstra:
  assumes "dbm_int_all M" "snd (constraint_pair ac)  "
  shows "dbm_int_all (abstra ac M v)"
using assms by (cases ac) (auto split: split_min)

lemma dbm_int_all_abstr:
  assumes "dbm_int_all M" " (x, m)  collect_clock_pairs g. m  "
  shows "dbm_int_all (abstr g M v)"
using assms
proof (induction g arbitrary: M)
  case Nil
  then show ?case by auto
next
  case (Cons ac cc)
  from Cons.IH[OF dbm_int_all_abstra, OF Cons.prems(1)] Cons.prems(2-) have
    "dbm_int_all (abstr cc (abstra ac M v) v)"
  unfolding collect_clock_pairs_def by force
  then show ?case by auto
qed

lemma dbm_int_all_abstr':
  assumes " (x, m)  collect_clock_pairs g. m  "
  shows "dbm_int_all (abstr g (λi j. ) v)"
 apply (rule dbm_int_all_abstr)
using assms by auto

lemma dbm_int_all_inv_abstr:
  assumes "(x,m)  clkp_set A. m  "
  shows "dbm_int_all (abstr (inv_of A l) (λi j. ) v)"
proof -
  from assms have " (x, m)  collect_clock_pairs (inv_of A l). m  "
  unfolding clkp_set_def collect_clki_def inv_of_def using Nats_subset_Ints by auto
  from dbm_int_all_abstr'[OF this] show ?thesis .
qed

lemma dbm_int_all_guard_abstr:
  assumes " (x, m)  clkp_set A. m  " "A  l ⟶⇗g,a,rl'"
  shows "dbm_int_all (abstr g (λi j. ) v)"
proof -
  from assms have " (x, m)  collect_clock_pairs g. m  "
  unfolding clkp_set_def collect_clkt_def using assms(2) Nats_subset_Ints by fastforce
  from dbm_int_all_abstr'[OF this] show ?thesis .
qed

lemma dbm_int_abstra:
  assumes "dbm_int M n" "snd (constraint_pair ac)  "
  shows "dbm_int (abstra ac M v) n"
using assms by (cases ac) (auto split: split_min)

lemma dbm_int_abstr:
  assumes "dbm_int M n" " (x, m)  collect_clock_pairs g. m  "
  shows "dbm_int (abstr g M v) n"
using assms
proof (induction g arbitrary: M)
  case Nil
  then show ?case by auto
next
  case (Cons ac cc)
  from Cons.IH[OF dbm_int_abstra, OF Cons.prems(1)] Cons.prems(2-) have
    "dbm_int (abstr cc (abstra ac M v) v) n"
  unfolding collect_clock_pairs_def by force
  then show ?case by auto
qed

lemma dbm_int_abstr':
  assumes " (x, m)  collect_clock_pairs g. m  "
  shows "dbm_int (abstr g (λi j. ) v) n"
 apply (rule dbm_int_abstr)
using assms by auto

lemma int_zone_dbm:
  assumes "clock_numbering' v n"
    " (_,d)  collect_clock_pairs cc. d  " " c  collect_clks cc. v c  n"
  obtains M where "{u. u  cc} = [M]⇘v,n⇙"
            and   " i  n.  j  n. M i j    get_const (M i j)  "
proof -
  let ?M = "abstr cc (λi j. ) v"
  from assms(2) have " i  n.  j  n. ?M i j    get_const (?M i j)  "
  by (rule dbm_int_abstr')
  with dbm_abstr_zone_eq[OF assms(1) assms(3)] show ?thesis by (auto intro: that)
qed

lemma dbm_int_inv_abstr:
  assumes "(x,m)  clkp_set A. m  "
  shows "dbm_int (abstr (inv_of A l) (λi j. ) v) n"
proof -
  from assms have " (x, m)  collect_clock_pairs (inv_of A l). m  "
  unfolding clkp_set_def collect_clki_def inv_of_def using Nats_subset_Ints by auto
  from dbm_int_abstr'[OF this] show ?thesis .
qed

lemma dbm_int_guard_abstr:
  assumes " (x, m)  clkp_set A. m  " "A  l ⟶⇗g,a,rl'"
  shows "dbm_int (abstr g (λi j. ) v) n"
proof -
  from assms have " (x, m)  collect_clock_pairs g. m  "
  unfolding clkp_set_def collect_clkt_def using assms(2) Nats_subset_Ints by fastforce
  from dbm_int_abstr'[OF this] show ?thesis .
qed

lemma collect_clks_id: "collect_clks cc = fst ` collect_clock_pairs cc"
proof -
  have "constraint_clk ac = fst (constraint_pair ac)" for ac by (cases ac) auto
  then show ?thesis unfolding collect_clks_def collect_clock_pairs_def by auto
qed

end