Theory Normalized_Zone_Semantics

chapter ‹Forward Analysis with DBMs and Widening›

theory Normalized_Zone_Semantics
  imports DBM_Zone_Semantics Approx_Beta Simulation_Graphs_TA
begin

hide_const (open) D
no_notation infinity (‹∞›)

(* XXX Move *)
lemma rtranclp_backwards_invariant_iff:
  assumes invariant: "⋀ y z. E⇧*⇧* x y ⟹ P z ⟹ E y z ⟹ P y"
    and E': "E' = (λ x y. E x y ∧ P y)"
  shows "E'⇧*⇧* x y ∧ P x ⟷ E⇧*⇧* x y ∧ P y"
  unfolding E'
  by (safe; induction rule: rtranclp_induct; auto dest: invariant intro: rtranclp.intros(2))

(* XXX Move *)
context Bisimulation_Invariant
begin

context
  fixes φ :: "'a ⇒ bool" and ψ :: "'b ⇒ bool"
  assumes compatible: "a ∼ b ⟹ PA a ⟹ PB b ⟹ φ a ⟷ ψ b"
begin

lemma reaches_ex_iff:
  "(∃ b. A.reaches a b ∧ φ b) ⟷ (∃ b. B.reaches a' b ∧ ψ b)" if "a ∼ a'" "PA a" "PB a'"
  using that by (force simp: compatible equiv'_def dest: bisim.A_B_reaches bisim.B_A_reaches)

lemma reaches_all_iff:
  "(∀ b. A.reaches a b ⟶ φ b) ⟷ (∀ b. B.reaches a' b ⟶ ψ b)" if "a ∼ a'" "PA a" "PB a'"
  using that by (force simp: compatible equiv'_def dest: bisim.A_B_reaches bisim.B_A_reaches)

end (* Context for Compatibility *)

end (* Bisimulation Invariant *)

(* XXX Move *)
lemma step_z_dbm_delay_loc:
  "l' = l" if "A ⊢ ⟨l, D⟩ ↝⇘v,n,τ⇙ ⟨l', D'⟩"
  using that by (auto elim!: step_z_dbm.cases)

lemma step_z_dbm_action_state_set1:
  "l ∈ state_set A" if "A ⊢ ⟨l, D⟩ ↝⇘v,n,↿a⇙ ⟨l', D'⟩"
  using that by (auto elim!: step_z_dbm.cases intro: state_setI1)

lemma step_z_dbm_action_state_set2:
  "l' ∈ state_set A" if "A ⊢ ⟨l, D⟩ ↝⇘v,n,↿a⇙ ⟨l', D'⟩"
  using that by (auto elim!: step_z_dbm.cases intro: state_setI2)

lemma step_delay_loc:
  "l' = l" if "A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l', u'⟩"
  using that by (auto elim!: step_t.cases)

lemma step_a_state_set1:
  "l ∈ state_set A" if "A ⊢ ⟨l, u⟩ →⇘a⇙ ⟨l', u'⟩"
  using that by (auto elim!: step_a.cases intro: state_setI1)

lemma step'_state_set1:
  "l ∈ state_set A" if "A ⊢' ⟨l, u⟩ → ⟨l', u'⟩"
  using that by (auto elim!: step'.cases intro: step_a_state_set1 dest: step_delay_loc)

section ‹DBM-based Semantics with Normalization›

subsection ‹Single Step›

inductive step_z_norm ::
  "('a, 'c, t, 's) ta
  ⇒ 's ⇒ t DBM ⇒ ('s ⇒ nat ⇒ nat) ⇒ ('c ⇒ nat) ⇒ nat ⇒ 'a action ⇒ 's ⇒ t DBM ⇒ bool"
(‹_ ⊢ ⟨_, _⟩ ↝⇘_,_,_,_⇙ ⟨_, _⟩› [61,61,61,61,61,61] 61)
where step_z_norm:
  "A ⊢ ⟨l,D⟩ ↝⇘v,n,a⇙ ⟨l', D'⟩ ⟹ A ⊢ ⟨l,D⟩ ↝⇘k,v,n,a⇙ ⟨l', norm (FW D' n) (k l') n⟩"

inductive step_z_norm' ::
  "('a, 'c, t, 's) ta ⇒ 's ⇒ t DBM ⇒ ('s ⇒ nat ⇒ nat) ⇒ ('c ⇒ nat) ⇒ nat ⇒ 's ⇒ t DBM ⇒ bool"
(‹_ ⊢'' ⟨_, _⟩ ↝⇘_,_,_⇙ ⟨_, _⟩› [61,61,61,61,61] 61)
where
  step: "A ⊢ ⟨l', Z'⟩ ↝⇘v,n,τ⇙ ⟨l'', Z''⟩
        ⟹ A ⊢ ⟨l'', Z''⟩ ↝⇘k,v,n,↿(a)⇙ ⟨l''', Z'''⟩
        ⟹ A ⊢' ⟨l', Z'⟩ ↝⇘k,v,n⇙ ⟨l''', Z'''⟩"

abbreviation steps_z_norm ::
  "('a, 'c, t, 's) ta ⇒ 's ⇒ t DBM ⇒ ('s ⇒ nat ⇒ nat) ⇒ ('c ⇒ nat) ⇒ nat ⇒ 's ⇒ t DBM ⇒ bool"
(‹_ ⊢ ⟨_, _⟩ ↝⇘_,_,_⇙* ⟨_, _⟩› [61,61,61,61,61] 61) where
 "A ⊢ ⟨l,D⟩ ↝⇘k,v,n⇙* ⟨l', D'⟩ ≡ (λ (l, Z) (l', Z'). A ⊢' ⟨l, Z⟩ ↝⇘k,v,n⇙ ⟨l', Z'⟩)⇧*⇧* (l, D) (l', D')"

lemma norm_empty_diag_preservation_real:
  fixes k :: "nat ⇒ nat"
  assumes "i ≤ n"
  assumes "M i i < Le 0"
  shows "norm M (real o k) n i i < Le 0"
  using assms unfolding norm_def by (auto simp: Let_def norm_diag_def DBM.less)

context Regions_defs
begin

inductive valid_dbm where
  "[M]⇘v,n⇙ ⊆ V ⟹ dbm_int M n ⟹ valid_dbm M"

inductive_cases valid_dbm_cases[elim]: "valid_dbm M"

declare valid_dbm.intros[intro]

end (* End of context for augmenting definitions for local and global sets of regions *)

locale Regions_common =
  Regions_defs X v n for X :: "'c set" and v n +
  fixes not_in_X
  assumes finite: "finite X"
  assumes clock_numbering: "clock_numbering' v n" "∀k≤n. k > 0 ⟶ (∃c ∈ X. v c = k)"
                           "∀ c ∈ X. v c ≤ n"
  assumes not_in_X: "not_in_X ∉ X"
  assumes non_empty: "X ≠ {}"
begin

lemma FW_zone_equiv_spec:
  shows "[M]⇘v,n⇙ = [FW M n]⇘v,n⇙"
apply (rule FW_zone_equiv) using clock_numbering(2) by auto

lemma dbm_non_empty_diag:
  assumes "[M]⇘v,n⇙ ≠ {}"
  shows "∀ k ≤ n. M k k ≥ 0"
proof safe
  fix k assume k: "k ≤ n"
  have "∀k≤n. 0 < k ⟶ (∃c. v c = k)" using clock_numbering(2) by blast
  from k not_empty_cyc_free[OF this assms(1)] show "0 ≤ M k k" by (simp add: cyc_free_diag_dest')
qed

lemma cn_weak: "∀k≤n. 0 < k ⟶ (∃c. v c = k)" using clock_numbering(2) by blast

lemma negative_diag_empty:
  assumes "∃ k ≤ n. M k k < 0"
  shows "[M]⇘v,n⇙ = {}"
using dbm_non_empty_diag assms by force

lemma non_empty_cyc_free:
  assumes "[M]⇘v,n⇙ ≠ {}"
  shows "cyc_free M n"
  using FW_neg_cycle_detect FW_zone_equiv_spec assms negative_diag_empty by blast

lemma FW_valid_preservation:
  assumes "valid_dbm M"
  shows "valid_dbm (FW M n)"
proof standard
  from FW_int_preservation assms show "dbm_int (FW M n) n" by blast
next
  from FW_zone_equiv_spec[of M, folded neutral] assms show "[FW M n]⇘v,n⇙ ⊆ V" by fastforce
qed

end

context Regions_global
begin

sublocale Regions_common by standard (rule finite clock_numbering not_in_X non_empty)+

abbreviation "v' ≡ beta_interp.v'"

lemma apx_empty_iff'':
  assumes "canonical M1 n" "[M1]⇘v,n⇙ ⊆ V" "dbm_int M1 n"
  shows "[M1]⇘v,n⇙ = {} ⟷ [norm M1 (k o v') n]⇘v,n⇙ = {}"
  using beta_interp.apx_norm_eq[OF assms] apx_empty_iff'[of "[M1]⇘v,n⇙"] assms
  unfolding V'_def by blast

lemma norm_FW_empty:
  assumes "valid_dbm M"
  assumes "[M]⇘v,n⇙ = {}"
  shows "[norm (FW M n) (k o v') n]⇘v,n⇙ = {}" (is "[?M]⇘v,n⇙ = {}")
proof -
  from assms(2) cyc_free_not_empty clock_numbering(1) have "¬ cyc_free M n"
    by metis
  from FW_neg_cycle_detect[OF this] obtain i where i: "i ≤ n" "FW M n i i < 0" by auto
  with norm_empty_diag_preservation_real[folded neutral] have
    "?M i i < 0"
  unfolding comp_def by auto
  with ‹i ≤ n› show ?thesis using beta_interp.neg_diag_empty_spec by auto
qed

lemma apx_norm_eq_spec:
  assumes "valid_dbm M"
    and "[M]⇘v,n⇙ ≠ {}"
  shows "beta_interp.Approx⇩β ([M]⇘v,n⇙) = [norm (FW M n) (k o v') n]⇘v,n⇙"
proof -
  note cyc_free = non_empty_cyc_free[OF assms(2)]
  from assms(1) FW_zone_equiv_spec[of M] have "[M]⇘v,n⇙ = [FW M n]⇘v,n⇙" by (auto simp: neutral)
  with beta_interp.apx_norm_eq[OF fw_canonical[OF cyc_free] _ FW_int_preservation]
      dbm_non_empty_diag[OF assms(2)] assms(1)
 show "Approx⇩β ([M]⇘v,n⇙) = [norm (FW M n) (k o v') n]⇘v,n⇙" by auto
qed

lemma norm_FW_valid_preservation_non_empty:
  assumes "valid_dbm M" "[M]⇘v,n⇙ ≠ {}"
  shows "valid_dbm (norm (FW M n) (k o v') n)" (is "valid_dbm ?M")
proof -
  from FW_valid_preservation[OF assms(1)] have valid: "valid_dbm (FW M n)" .
  show ?thesis
  proof standard
    from valid beta_interp.norm_int_preservation show "dbm_int ?M n" by blast
  next
    from fw_canonical[OF non_empty_cyc_free] assms have "canonical (FW M n) n" by auto
    from beta_interp.norm_V_preservation[OF _ this ] valid show "[?M]⇘v,n⇙ ⊆ V" by fast
  qed
qed

lemma norm_int_all_preservation:
  fixes M :: "real DBM"
  assumes "dbm_int_all M"
  shows "dbm_int_all (norm M (k o v') n)"
using assms unfolding norm_def norm_diag_def by (auto simp: Let_def)

lemma norm_FW_valid_preservation_empty:
  assumes "valid_dbm M" "[M]⇘v,n⇙ = {}"
  shows "valid_dbm (norm (FW M n) (k o v') n)" (is "valid_dbm ?M")
proof -
  from FW_valid_preservation[OF assms(1)] have valid: "valid_dbm (FW M n)" .
  show ?thesis
  proof standard
    from valid beta_interp.norm_int_preservation show "dbm_int ?M n" by blast
  next
    from norm_FW_empty[OF assms(1,2)] show "[?M]⇘v,n⇙ ⊆ V" by fast
  qed
qed

lemma norm_FW_valid_preservation:
  assumes "valid_dbm M"
  shows "valid_dbm (norm (FW M n) (k o v') n)"
using assms norm_FW_valid_preservation_empty norm_FW_valid_preservation_non_empty by metis

lemma norm_FW_equiv:
  assumes valid: "dbm_int D n" "dbm_int M n" "[D]⇘v,n⇙ ⊆ V"
      and equiv: "[D]⇘v,n⇙ = [M]⇘v,n⇙"
  shows "[norm (FW D n) (k o v') n]⇘v,n⇙ = [norm (FW M n) (k o v') n]⇘v,n⇙"
proof (cases "[D]⇘v,n⇙ = {}")
  case False
  with equiv fw_shortest[OF non_empty_cyc_free] FW_zone_equiv_spec have
    "canonical (FW D n) n" "canonical (FW M n) n" "[FW D n]⇘v,n⇙ = [D]⇘v,n⇙" "[FW M n]⇘v,n⇙ = [M]⇘v,n⇙"
  by blast+
  with valid equiv show ?thesis
   apply -
   apply (subst beta_interp.apx_norm_eq[symmetric])
   prefer 4
   apply (subst beta_interp.apx_norm_eq[symmetric])
  by (simp add: FW_int_preservation)+
next
  case True
  show ?thesis
   apply (subst norm_FW_empty)
   prefer 3
   apply (subst norm_FW_empty)
  using valid equiv True by blast+
qed

end (* End of context for global set of regions *)

context Regions
begin

sublocale Regions_common by standard (rule finite clock_numbering not_in_X non_empty)+

definition "v' ≡ λ i. if 0 < i ∧ i ≤ n then (THE c. c ∈ X ∧ v c = i) else not_in_X"
(*abbreviation "v' ≡ beta_interp.v'"*)

abbreviation step_z_norm' (‹_ ⊢ ⟨_, _⟩ ↝⇘𝒩(_)⇙ ⟨_, _⟩› [61,61,61,61] 61)
where
  "A ⊢ ⟨l, D⟩ ↝⇘𝒩(a)⇙ ⟨l', D'⟩ ≡ A ⊢ ⟨l, D⟩ ↝⇘(λ l. k l o v'),v,n,a⇙ ⟨l', D'⟩"

definition step_z_norm'' (‹_ ⊢'' ⟨_, _⟩ ↝⇘𝒩(_)⇙ ⟨_, _⟩› [61,61,61,61] 61)
where
  "A ⊢' ⟨l, D⟩ ↝⇘𝒩(a)⇙ ⟨l'', D''⟩ ≡
  ∃ l' D'. A ⊢ ⟨l, D⟩ ↝⇘v,n,τ⇙ ⟨l', D'⟩ ∧ A ⊢ ⟨l', D'⟩ ↝⇘𝒩(↿a)⇙ ⟨l'', D''⟩"

abbreviation steps_z_norm' (‹_ ⊢ ⟨_, _⟩ ↝⇩𝒩* ⟨_, _⟩› [61,61,61] 61)
where
  "A ⊢ ⟨l, D⟩ ↝⇩𝒩* ⟨l', D'⟩ ≡ (λ (l,D) (l',D'). ∃ a. A ⊢' ⟨l, D⟩ ↝⇘𝒩(a)⇙ ⟨l', D'⟩)⇧*⇧* (l,D) (l',D')"

inductive_cases step_z_norm'_elims[elim!]: "A ⊢ ⟨l, u⟩ ↝⇘𝒩(a)⇙ ⟨l',u'⟩"

declare step_z_norm.intros[intro]

lemma step_z_valid_dbm:
  assumes "A ⊢ ⟨l, D⟩ ↝⇘v,n,a⇙ ⟨l', D'⟩"
    and "global_clock_numbering A v n" "valid_abstraction A X k" "valid_dbm D"
  shows "valid_dbm D'"
proof -
  from step_z_V step_z_dbm_sound[OF assms(1,2)] step_z_dbm_preserves_int[OF assms(1,2)]
       assms(3,4)
  have
    "dbm_int D' n" "A ⊢ ⟨l, [D]⇘v,n⇙⟩ ↝⇘a⇙ ⟨l', [D']⇘v,n⇙⟩"
  by (fastforce dest!: valid_abstraction_pairsD)+
  with step_z_V[OF this(2)] assms(4) show ?thesis by auto
qed

(* Crudely copied from step_z_norm.inducts *)
lemma step_z_norm_induct[case_names _ step_z_norm step_z_refl]:
  assumes "x1 ⊢ ⟨x2, x3⟩ ↝⇘(λ l. k l o v'),v,n,a⇙ ⟨x7,x8⟩"
    and step_z_norm:
    "⋀A l D l' D'.
        A ⊢ ⟨l, D⟩ ↝⇘v,n,a⇙ ⟨l',D'⟩ ⟹
        P A l D l' (norm (FW D' n) (k l' o v') n)"
  shows "P x1 x2 x3 x7 x8"
using assms by (induction rule: step_z_norm.inducts) auto

context
  fixes l' :: 's
begin

interpretation regions: Regions_global _ _ _ "k l'"
  by standard (rule finite clock_numbering not_in_X non_empty)+

lemma regions_v'_eq[simp]:
  "regions.v' = v'"
  unfolding v'_def regions.beta_interp.v'_def by simp

lemma step_z_norm_int_all_preservation:
  assumes
    "A ⊢ ⟨l,D⟩ ↝⇘𝒩(a)⇙ ⟨l',D'⟩" "global_clock_numbering A v n"
    "∀(x, m)∈Timed_Automata.clkp_set A. m ∈ ℕ" "dbm_int_all D"
  shows "dbm_int_all D'"
using assms
 apply cases
 apply simp
 apply (rule regions.norm_int_all_preservation[simplified])
 apply (rule FW_int_all_preservation)
 apply (erule step_z_dbm_preserves_int_all)
by fast+

lemma step_z_norm_valid_dbm_preservation:
  assumes
    "A ⊢ ⟨l,D⟩ ↝⇘𝒩(a)⇙ ⟨l',D'⟩" "global_clock_numbering A v n" "valid_abstraction A X k" "valid_dbm D"
  shows "valid_dbm D'"
  using assms
  by cases (simp; rule regions.norm_FW_valid_preservation[simplified]; erule step_z_valid_dbm; fast)

lemma norm_beta_sound:
  assumes "A ⊢ ⟨l,D⟩ ↝⇘𝒩(a)⇙ ⟨l',D'⟩" "global_clock_numbering A v n" "valid_abstraction A X k"
  and     "valid_dbm D"
shows   "A ⊢ ⟨l,[D]⇘v,n⇙⟩ ↝⇘β(a)⇙ ⟨l',[D']⇘v,n⇙⟩" using assms(2-)
  apply (induction A l D l' ≡ l' D' rule: step_z_norm_induct, (subst assms(1); blast))
proof goal_cases
  case step_z_norm: (1 A l D D')
  from step_z_dbm_sound[OF step_z_norm(1,2)] have "A ⊢ ⟨l, [D]⇘v,n⇙⟩ ↝⇘a⇙ ⟨l',[D']⇘v,n⇙⟩" by blast
  then have *: "A ⊢ ⟨l, [D]⇘v,n⇙⟩ ↝⇘β(a)⇙ ⟨l',Approx⇩β l' ([D']⇘v,n⇙)⟩" by force
  show ?case
  proof (cases "[D']⇘v,n⇙ = {}")
    case False
    from regions.apx_norm_eq_spec[OF step_z_valid_dbm[OF step_z_norm] False] *
    show ?thesis by auto
  next
    case True
    with
      regions.norm_FW_empty[OF step_z_valid_dbm[OF step_z_norm] this] regions.beta_interp.apx_empty *
    show ?thesis by auto
  qed
qed

lemma step_z_norm_valid_dbm:
  assumes
    "A ⊢ ⟨l, D⟩ ↝⇘𝒩(a)⇙ ⟨l',D'⟩" "global_clock_numbering A v n"
    "valid_abstraction A X k" "valid_dbm D"
  shows "valid_dbm D'" using assms(2-)
apply (induction A l D l' ≡ l' D' rule: step_z_norm_induct, (subst assms(1); blast))
proof goal_cases
  case step_z_norm: (1 A l D D')
  with regions.norm_FW_valid_preservation[OF step_z_valid_dbm[OF step_z_norm]] show ?case by auto
qed

lemma norm_beta_complete:
  assumes "A ⊢ ⟨l,[D]⇘v,n⇙⟩ ↝⇘β(a)⇙ ⟨l',Z⟩" "global_clock_numbering A v n" "valid_abstraction A X k"
  and     "valid_dbm D"
  obtains D' where "A ⊢ ⟨l,D⟩ ↝⇘𝒩(a)⇙ ⟨l',D'⟩" "[D']⇘v,n⇙ = Z" "valid_dbm D'"
proof -
  from assms(3) have ta_int: "∀(x, m)∈Timed_Automata.clkp_set A. m ∈ ℕ"
    by (fastforce dest!: valid_abstraction_pairsD)
  from assms(1) obtain Z' where Z': "A ⊢ ⟨l,[D]⇘v,n⇙⟩ ↝⇘a⇙ ⟨l',Z'⟩" "Z = Approx⇩β l' Z'" by auto
  from assms(4) have "dbm_int D n" by auto
  with step_z_dbm_DBM[OF Z'(1) assms(2)] step_z_dbm_preserves_int[OF _ assms(2) ta_int] obtain D'
    where D': "A ⊢ ⟨l, D⟩ ↝⇘v,n,a⇙ ⟨l',D'⟩" "Z' = [D']⇘v,n⇙" "dbm_int D' n"
  by auto
  note valid_D' = step_z_valid_dbm[OF D'(1) assms(2,3)]
  obtain D'' where D'': "D'' = norm (FW D' n) (k l' ∘ v') n" by auto
  show ?thesis
  proof (cases "Z' = {}")
    case False
    with D' have *: "[D']⇘v,n⇙ ≠ {}" by auto
    from regions.apx_norm_eq_spec[OF valid_D' this] D'' D'(2) Z'(2) assms(4) have "Z = [D'']⇘v,n⇙"
      by auto
    with regions.norm_FW_valid_preservation[OF valid_D'] D' D'' *  assms(4)
    show thesis
      apply -
      apply (rule that[of D''])
      by (drule step_z_norm.intros[where k = "λ l. k l o v'"]) simp+
  next
    case True
    with regions.norm_FW_empty[OF valid_D'[OF assms(4)]] D'' D' Z'(2)
         regions.norm_FW_valid_preservation[OF valid_D'[OF assms(4)]] regions.beta_interp.apx_empty
    show thesis
    apply -
    apply (rule that[of D''])
      apply blast
    by fastforce+
  qed
qed

(* XXX Maybe move *)
lemma step_z_norm_mono:
  assumes "A ⊢ ⟨l,D⟩ ↝⇘𝒩(a)⇙ ⟨l',D'⟩" "global_clock_numbering A v n" "valid_abstraction A X k"
  and     "valid_dbm D" "valid_dbm M"
  and "[D]⇘v,n⇙ ⊆ [M]⇘v,n⇙"
  shows "∃ M'. A ⊢ ⟨l, M⟩ ↝⇘𝒩(a)⇙ ⟨l', M'⟩ ∧ [D']⇘v,n⇙ ⊆ [M']⇘v,n⇙"
proof -
  from norm_beta_sound[OF assms(1,2,3,4)] have "A ⊢ ⟨l, [D]⇘v,n⇙⟩ ↝⇘β(a)⇙ ⟨l', [D']⇘v,n⇙⟩" .
  from step_z_beta_mono[OF this assms(6)] assms(5) obtain Z where
    "A ⊢ ⟨l, [M]⇘v,n⇙⟩ ↝⇘β(a)⇙ ⟨l', Z⟩" "[D']⇘v,n⇙ ⊆ Z"
  by auto
  with norm_beta_complete[OF this(1) assms(2,3,5)] show ?thesis by metis
qed

lemma step_z_norm_equiv:
  assumes step: "A ⊢ ⟨l,D⟩ ↝⇘𝒩(a)⇙ ⟨l',D'⟩"
      and prems: "global_clock_numbering A v n" "valid_abstraction A X k"
      and valid: "valid_dbm D" "valid_dbm M"
      and equiv: "[D]⇘v,n⇙ = [M]⇘v,n⇙"
  shows "∃ M'. A ⊢ ⟨l, M⟩ ↝⇘𝒩(a)⇙ ⟨l', M'⟩ ∧ [D']⇘v,n⇙ = [M']⇘v,n⇙"
using step
 apply cases
 apply (frule step_z_dbm_equiv[OF prems(1)])
 apply (rule equiv)
 apply clarify
 apply (drule regions.norm_FW_equiv[rotated 3])
   prefer 4
   apply force
using step_z_valid_dbm[OF _ prems] valid by (simp add: valid_dbm.simps)+

end (* End of context for fixed location *)

subsection ‹Multi Step›

lemma valid_dbm_V':
  assumes "valid_dbm M"
  shows "[M]⇘v,n⇙ ∈ V'"
using assms unfolding V'_def by force

lemma step_z_empty:
  assumes "A ⊢ ⟨l, Z⟩ ↝⇘a⇙ ⟨l', Z'⟩" "Z = {}"
  shows "Z' = {}"
  using assms
  apply cases
  unfolding zone_delay_def zone_set_def
  by auto

subsection ‹Connecting with Correctness Results for Approximating Semantics›

context
  fixes A :: "('a, 'c, real, 's) ta"
    assumes gcn: "global_clock_numbering A v n"
    and va: "valid_abstraction A X k"
begin

context
  notes [intro] = step_z_valid_dbm[OF _ gcn va]
begin

lemma valid_dbm_step_z_norm'':
  "valid_dbm D'" if "A ⊢' ⟨l, D⟩ ↝⇘𝒩(a)⇙ ⟨l', D'⟩" "valid_dbm D"
  using that unfolding step_z_norm''_def by (auto intro: step_z_norm_valid_dbm[OF _ gcn va])

lemma steps_z_norm'_valid_dbm_invariant:
  "valid_dbm D'" if "A ⊢ ⟨l, D⟩ ↝⇩𝒩* ⟨l', D'⟩" "valid_dbm D"
  using that by (induction rule: rtranclp_induct2) (auto intro: valid_dbm_step_z_norm'')

lemma norm_beta_sound'':
  assumes "A ⊢' ⟨l, D⟩ ↝⇘𝒩(a)⇙ ⟨l'', D''⟩"
      and "valid_dbm D"
    shows "A ⊢ ⟨l, [D]⇘v,n⇙⟩ ↝⇩β ⟨l'', [D'']⇘v,n⇙⟩"
proof -
  from assms(1) obtain l' D' where
    "A ⊢ ⟨l, D⟩ ↝⇘v,n,τ⇙ ⟨l', D'⟩" "A ⊢ ⟨l', D'⟩ ↝⇘𝒩(↿a)⇙ ⟨l'', D''⟩"
    by (auto simp: step_z_norm''_def)
  moreover with ‹valid_dbm D› have "valid_dbm D'"
    by auto
  ultimately have "A ⊢ ⟨l', [D']⇘v,n⇙⟩ ↝⇘β↿a⇙ ⟨l'', [D'']⇘v,n⇙⟩"
    by - (rule norm_beta_sound[OF _ gcn va])
  with step_z_dbm_sound[OF ‹A ⊢ ⟨l, D⟩ ↝⇘v,n,τ⇙ ⟨l', D'⟩› gcn] show ?thesis
    unfolding step_z_beta'_def by - (frule step_z.cases[where P = "l' = l"]; force)
qed

lemma norm_beta_complete1:
  assumes "A ⊢ ⟨l,[D]⇘v,n⇙⟩ ↝⇩β ⟨l'',Z''⟩"
  and     "valid_dbm D"
  obtains a D'' where "A ⊢' ⟨l,D⟩ ↝⇘𝒩(a)⇙ ⟨l'',D''⟩" "[D'']⇘v,n⇙ = Z''" "valid_dbm D''"
proof -
  from assms(1) obtain a l' Z' where steps:
    "A ⊢ ⟨l, [D]⇘v,n⇙⟩ ↝⇘τ⇙ ⟨l', Z'⟩" "A ⊢ ⟨l', Z'⟩ ↝⇘β(↿a)⇙ ⟨l'', Z''⟩"
    by (auto simp: step_z_beta'_def)
  from step_z_dbm_DBM[OF this(1) gcn] obtain D' where D':
    "A ⊢ ⟨l, D⟩ ↝⇘v,n,τ⇙ ⟨l', D'⟩" "Z' = [D']⇘v,n⇙"
    by auto
  with ‹valid_dbm D› have "valid_dbm D'"
    by auto
  from steps D' show ?thesis
    by (auto
        intro!: that[unfolded step_z_norm''_def]
        elim!: norm_beta_complete[OF _ gcn va ‹valid_dbm D'›]
        )
qed

lemma bisim:
  "Bisimulation_Invariant
  (λ (l, Z) (l', Z'). A ⊢ ⟨l, Z⟩ ↝⇩β ⟨l', Z'⟩ ∧ Z' ≠ {})
  (λ (l, D) (l', D'). ∃ a. A ⊢' ⟨l, D⟩ ↝⇘𝒩(a)⇙ ⟨l', D'⟩ ∧ [D']⇘v,n⇙ ≠ {})
  (λ (l, Z) (l', D). l = l' ∧ Z = [D]⇘v,n⇙)
  (λ _. True) (λ (l, D). valid_dbm D)"
proof (standard, goal_cases)
  ― ‹‹β ⇒ 𝒩››
  case (1 a b a')
  then show ?case
    by (blast elim: norm_beta_complete1)
next
  ― ‹‹𝒩 ⇒ β››
  case (2 a a' b')
  then show ?case
    by (blast intro: norm_beta_sound'')
next
  ― ‹‹β› invariant›
  case (3 a b)
  then show ?case
    by simp
next
  ― ‹‹𝒩› invariant›
  case (4 a b)
  then show ?case
    unfolding step_z_norm''_def
    by (auto intro: step_z_norm_valid_dbm[OF _ gcn va])
qed

end (* Setup for Automation *)

interpretation Bisimulation_Invariant
  "λ (l, Z) (l', Z'). A ⊢ ⟨l, Z⟩ ↝⇩β ⟨l', Z'⟩ ∧ Z' ≠ {}"
  "λ (l, D) (l', D'). ∃ a. A ⊢' ⟨l, D⟩ ↝⇘𝒩(a)⇙ ⟨l', D'⟩ ∧ [D']⇘v,n⇙ ≠ {}"
  "λ (l, Z) (l', D). l = l' ∧ Z = [D]⇘v,n⇙"
  "λ _. True" "λ (l, D). valid_dbm D"
  by (rule bisim)

lemma step_z_norm''_non_empty:
  "[D]⇘v,n⇙ ≠ {}" if "A ⊢' ⟨l, D⟩ ↝⇘𝒩(a)⇙ ⟨l', D'⟩" "[D']⇘v,n⇙ ≠ {}" "valid_dbm D"
proof -
  from that B_A_step[of "(l, D)" "(l', D')" "(l, [D]⇘v,n⇙)"] have
    "A ⊢ ⟨l, [D]⇘v,n⇙⟩ ↝⇩β ⟨l', [D']⇘v,n⇙⟩"
    by auto
  with ‹_ ≠ {}› show ?thesis
    by (auto 4 3 dest: step_z_beta'_empty)
qed

lemma norm_steps_empty:
  "A ⊢ ⟨l, D⟩ ↝⇩𝒩* ⟨l', D'⟩ ∧ [D']⇘v,n⇙ ≠ {} ⟷ B.reaches (l, D) (l', D') ∧ [D]⇘v,n⇙ ≠ {}"
  if "valid_dbm D"
  apply (subst rtranclp_backwards_invariant_iff[
    of "λ(l, D) (l', D'). ∃ a. A ⊢' ⟨l, D⟩ ↝⇘𝒩(a)⇙ ⟨l', D'⟩" "(l, D)" "λ(l, D). [D]⇘v,n⇙ ≠ {}",
    simplified
    ])
  using ‹valid_dbm D›
  by (auto dest!: step_z_norm''_non_empty intro: steps_z_norm'_valid_dbm_invariant)

context
  fixes P Q :: "'s ⇒ bool" ― ‹The state property we want to check›
begin

interpretation bisim_ψ: Bisimulation_Invariant
  "λ (l, Z) (l', Z'). A ⊢ ⟨l, Z⟩ ↝⇩β ⟨l', Z'⟩ ∧ Z' ≠ {} ∧ Q l'"
  "λ (l, D) (l', D'). ∃ a. A ⊢' ⟨l, D⟩ ↝⇘𝒩(a)⇙ ⟨l', D'⟩ ∧ [D']⇘v,n⇙ ≠ {} ∧ Q l'"
  "λ (l, Z) (l', D). l = l' ∧ Z = [D]⇘v,n⇙"
  "λ _. True" "λ (l, D). valid_dbm D"
  by (rule Bisimulation_Invariant_filter[OF bisim, of "λ (l, _). Q l" "λ (l, _). Q l"]) auto

end (* Context for State Formulae *)

context
  assumes finite_state_set: "finite (state_set A)"
begin

interpretation R: Regions_TA
  by (standard; rule va finite_state_set)

lemma A_reaches_non_empty:
  "Z' ≠ {}" if "A.reaches (l, Z) (l', Z')" "Z ≠ {}"
  using that by cases auto

lemma A_reaches_start_non_empty_iff:
  "(∃Z'. (∃u. u ∈ Z') ∧ A.reaches (l, Z) (l', Z')) ⟷ (∃Z'. A.reaches (l, Z) (l', Z')) ∧ Z ≠ {}"
  apply safe
    apply blast
  subgoal
    by (auto dest: step_z_beta'_empty elim: converse_rtranclpE2)
  by (auto dest: A_reaches_non_empty)

(* XXX Move *)
lemma step_z_norm''_state_set1:
  "l ∈ state_set A" if "A ⊢' ⟨l, D⟩ ↝⇘𝒩a⇙ ⟨l', D'⟩"
  using that unfolding step_z_norm''_def
  by (auto dest: step_z_dbm_delay_loc intro: step_z_dbm_action_state_set1)

lemma step_z_norm''_state_set2:
  "l' ∈ state_set A" if "A ⊢' ⟨l, D⟩ ↝⇘𝒩a⇙ ⟨l', D'⟩"
  using that unfolding step_z_norm''_def by (auto intro: step_z_dbm_action_state_set2)

theorem steps_z_norm_decides_emptiness:
  assumes "valid_dbm D"
  shows "(∃ D'. A ⊢ ⟨l, D⟩ ↝⇩𝒩* ⟨l',D'⟩ ∧ [D']⇘v,n⇙ ≠ {})
     ⟷ (∃ u ∈ [D]⇘v,n⇙. (∃ u'. A ⊢' ⟨l, u⟩ →* ⟨l', u'⟩))"
proof (cases "[D]⇘v,n⇙ = {}")
  case True
  then show ?thesis
    unfolding norm_steps_empty[OF ‹valid_dbm D›] by auto
next
  case F: False
  show ?thesis
  proof (cases "l ∈ state_set A")
    case True
    interpret Regions_TA_Start_State v n not_in_X X k A l "[D]⇘v,n⇙"
      using assms F True by - (standard, auto elim!: valid_dbm_V')
    show ?thesis
      unfolding steps'_iff[symmetric] norm_steps_empty[OF ‹valid_dbm D›]
      using
        reaches_ex_iff[of "λ (l, _). l = l'" "λ (l, _). l = l'" "(l, [D]⇘v,n⇙)" "(l, D)"]
        ‹valid_dbm D› ta_reaches_ex_iff[of "λ (l, _). l = l'"]
      by (auto simp: A_reaches_start_non_empty_iff from_R_def a⇩0_def)
  next
    case False
    have "A ⊢ ⟨l, D⟩ ↝⇩𝒩* ⟨l',D'⟩ ⟷ (D' = D ∧ l' = l)" for D'
      using False by (blast dest: step_z_norm''_state_set1 elim: converse_rtranclpE2)
    moreover have "A ⊢' ⟨l, u⟩ →* ⟨l', u'⟩ ⟷ (u' = u ∧ l' = l)" for u u'
      unfolding steps'_iff[symmetric] using False
      by (blast dest: step'_state_set1 elim: converse_rtranclpE2)
    ultimately show ?thesis
      using F by auto
  qed
qed

end (* Finite State Set *)

end (* Context for Global Clock Numbering *)

context
  fixes A :: "('a, 'c, real, 's) ta"
    assumes gcn: "global_clock_numbering A v n"
    and va: "valid_abstraction A X k"
begin

lemmas
  step_z_norm_valid_dbm' = step_z_norm_valid_dbm[OF _ gcn va]

lemmas
  step_z_valid_dbm' = step_z_valid_dbm[OF _ gcn va]

lemmas norm_beta_sound' = norm_beta_sound[OF _ gcn va]

lemma v_bound:
  "∀ c ∈ clk_set A. v c ≤ n"
  using gcn by blast

lemmas alpha_beta_step'' = alpha_beta_step'[OF _ va v_bound]

lemmas step_z_dbm_sound' = step_z_dbm_sound[OF _ gcn]

lemmas step_z_V'' = step_z_V'[OF _ va v_bound]

end

end

section ‹Additional Useful Properties of the Normalized Semantics›

text ‹Obsolete›

lemma norm_diag_alt_def:
  "norm_diag e = (if e < 0 then Lt 0 else if e = 0 then e else ∞)"
  unfolding norm_diag_def DBM.neutral DBM.less ..

lemma norm_diag_preservation:
  assumes "∀l≤n. M1 l l ≤ 0"
  shows "∀l≤n. (norm M1 (k :: nat ⇒ nat) n) l l ≤ 0"
  using assms unfolding norm_def norm_diag_alt_def by (auto simp: DBM.neutral)


section ‹Appendix: Standard Clock Numberings for Concrete Models›

locale Regions' =
  fixes X and k :: "'c ⇒ nat" and v :: "'c ⇒ nat" and n :: nat and not_in_X
  assumes finite: "finite X"
  assumes clock_numbering': "∀ c ∈ X. v c > 0" "∀ c. c ∉ X ⟶ v c > n"
  assumes bij: "bij_betw v X {1..n}"
  assumes non_empty: "X ≠ {}"
  assumes not_in_X: "not_in_X ∉ X"

begin

lemma inj: "inj_on v X" using bij_betw_imp_inj_on bij by simp

lemma cn_weak: "∀ c. v c > 0" using clock_numbering' by force

lemma in_X: assumes "v x ≤ n" shows "x ∈ X" using assms clock_numbering'(2) by force

end

sublocale Regions' ⊆ Regions_global
proof (unfold_locales, auto simp: finite clock_numbering' non_empty cn_weak not_in_X, goal_cases)
  case (1 x y) with inj in_X show ?case unfolding inj_on_def by auto
next
  case (2 k)
  from bij have "v ` X = {1..n}" unfolding bij_betw_def by auto
  from 2 have "k ∈ {1..n}" by simp
  then obtain x where "x ∈ X" "v x = k" unfolding image_def
  by (metis (no_types, lifting) ‹v ` X = {1..n}› imageE)
  then show ?case by blast
next
  case (3 x) with bij show ?case unfolding bij_betw_def by auto
qed

(* This is for automata carrying real time annotations *)
lemma standard_abstraction:
  assumes
    "finite (Timed_Automata.clkp_set A)" "finite (Timed_Automata.collect_clkvt (trans_of A))"
    "∀(_,m::real) ∈ Timed_Automata.clkp_set A. m ∈ ℕ"
  obtains k :: "'c ⇒ nat" where "Timed_Automata.valid_abstraction A (clk_set A) k"
proof -
  from assms have 1: "finite (clk_set A)" by auto
  have 2: "Timed_Automata.collect_clkvt (trans_of A) ⊆ clk_set A" by auto
  from assms obtain L where L: "distinct L" "set L = Timed_Automata.clkp_set A"
    by (meson finite_distinct_list)
  let ?M = "λ c. {m . (c, m) ∈ Timed_Automata.clkp_set A}"
  let ?X = "clk_set A"
  let ?m = "map_of L"
  let ?k = "λ x. if ?M x = {} then 0 else nat (floor (Max (?M x)) + 1)"
  { fix c m assume A: "(c, m) ∈ Timed_Automata.clkp_set A"
    from assms(1) have "finite (snd ` Timed_Automata.clkp_set A)" by auto
    moreover have "?M c ⊆ (snd ` Timed_Automata.clkp_set A)" by force
    ultimately have fin: "finite (?M c)" by (blast intro: finite_subset)
    then have "Max (?M c) ∈ {m . (c, m) ∈ Timed_Automata.clkp_set A}" using Max_in A by auto
    with assms(3) have "Max (?M c) ∈ ℕ" by auto
    then have "floor (Max (?M c)) = Max (?M c)" by (metis Nats_cases floor_of_nat of_int_of_nat_eq)
    have *: "?k c = Max (?M c) + 1"
    proof -
      have "real (nat (n + 1)) = real_of_int n + 1"
        if "Max {m. (c, m) ∈ Timed_Automata.clkp_set A} = real_of_int n"
        for n :: int and x :: real
      proof -
        from that have "real_of_int (n + 1) ∈ ℕ"
          using ‹Max {m. (c, m) ∈ Timed_Automata.clkp_set A} ∈ ℕ› by auto
        then show ?thesis
          by (metis Nats_cases ceiling_of_int nat_int of_int_1 of_int_add of_int_of_nat_eq)
      qed
      with A ‹floor (Max (?M c)) = Max (?M c)› show ?thesis
        by auto
    qed
    from fin A have "Max (?M c) ≥ m" by auto
    moreover from A assms(3) have "m ∈ ℕ" by auto
    ultimately have "m ≤ ?k c" "m ∈ ℕ" "c ∈ clk_set A" using A * by force+
  }
  then have "∀(x, m) ∈ Timed_Automata.clkp_set A. m ≤ ?k x ∧ x ∈ clk_set A ∧ m ∈ ℕ" by blast
  with 1 2 have "Timed_Automata.valid_abstraction A ?X ?k" by - (standard, assumption+)
  then show thesis ..
qed

definition
  "finite_ta A ≡
    finite (Timed_Automata.clkp_set A) ∧ finite (Timed_Automata.collect_clkvt (trans_of A))
  ∧ (∀(_,m) ∈ Timed_Automata.clkp_set A. m ∈ ℕ) ∧ clk_set A ≠ {} ∧ -clk_set A ≠ {}"

lemma finite_ta_Regions':
  fixes A :: "('a, 'c, real, 's) ta"
  assumes "finite_ta A"
  obtains v n x where "Regions' (clk_set A) v n x"
proof -
  from assms obtain x where x: "x ∉ clk_set A" unfolding finite_ta_def by auto
  from assms(1) have "finite (clk_set A)" unfolding finite_ta_def by auto
  with standard_numbering[of "clk_set A"] assms obtain v and n :: nat where
            "bij_betw v (clk_set A) {1..n}"
            "∀c∈clk_set A. 0 < v c" "∀c. c ∉ clk_set A ⟶ n < v c"
  by auto
  then have "Regions' (clk_set A) v n x" using x assms unfolding finite_ta_def by - (standard, auto)
  then show ?thesis ..
qed

lemma finite_ta_RegionsD:
  fixes A :: "('a, 'c, t, 's) ta"
  assumes "finite_ta A"
  obtains k :: "'c ⇒ nat" and v n x where
    "Regions' (clk_set A) v n x" "Timed_Automata.valid_abstraction A (clk_set A) k"
    "global_clock_numbering A v n"
proof -
  from standard_abstraction assms obtain k :: "'c ⇒ nat" where k:
    "Timed_Automata.valid_abstraction A (clk_set A) k"
  unfolding finite_ta_def by blast
  from finite_ta_Regions'[OF assms] obtain v n x where *: "Regions' (clk_set A) v n x" .
  then interpret interp: Regions' "clk_set A" k v n x .
  from interp.clock_numbering have "global_clock_numbering A v n" by blast
  with * k show ?thesis ..
qed

definition valid_dbm where "valid_dbm M n ≡ dbm_int M n ∧ (∀ i ≤ n. M 0 i ≤ 0)"

lemma dbm_positive:
  assumes "M 0 (v c) ≤ 0" "v c ≤ n" "DBM_val_bounded v u M n"
  shows "u c ≥ 0"
proof -
  from assms have "dbm_entry_val u None (Some c) (M 0 (v c))" unfolding DBM_val_bounded_def by auto
  with assms(1) show ?thesis
  proof (cases "M 0 (v c)", goal_cases)
    case 1
    then show ?case unfolding less_eq neutral using order_trans by (fastforce dest!: le_dbm_le)
  next
    case 2
    then show ?case unfolding less_eq neutral
    by (auto dest!: lt_dbm_le) (meson less_trans neg_0_less_iff_less not_less)
  next
    case 3
    then show ?case unfolding neutral less_eq dbm_le_def by auto
  qed
qed

lemma valid_dbm_pos:
  assumes "valid_dbm M n"
  shows "[M]⇘v,n⇙ ⊆ {u. ∀ c. v c ≤ n ⟶ u c ≥ 0}"
using dbm_positive assms unfolding valid_dbm_def unfolding DBM_zone_repr_def by fast

lemma (in Regions') V_alt_def:
  shows "{u. ∀ c. v c > 0 ∧ v c ≤ n ⟶ u c ≥ 0} = V"
unfolding V_def using clock_numbering by metis

end (* Theory *)