Theory Timed_Automata.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"
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')
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,n⇙ M; 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,n⇙ M; 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
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
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" "∀c∈collect_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" "∀c∈collect_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) ∧ (∀k≤n. 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,r⇖ l'"
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,r⇖ l'"
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