Theory Normalized_Zone_Semantics

chapter ‹Forward Analysis with DBMs and Widening›

theory Normalized_Zone_Semantics
  imports DBM_Zone_Semantics Approx_Beta
begin

section ‹DBM-based Semantics with Normalization›

subsection ‹Single Step›

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

inductive steps_z_norm ::
  "('a, 'c, t, 's) ta ⇒ 's ⇒ t DBM ⇒ (nat ⇒ nat) ⇒ ('c ⇒ nat) ⇒ nat ⇒ 's ⇒ t DBM ⇒ bool"
("_ ⊢ ⟨_, _⟩ ↝⇘_,_,_⇙* ⟨_, _⟩" [61,61,61,61,61] 61)
where
  refl: "A ⊢ ⟨l, Z⟩  ↝⇘k,v,n⇙* ⟨l, Z⟩" |
  step: "A ⊢ ⟨l, Z⟩  ↝⇘k,v,n⇙* ⟨l', Z'⟩ ⟹ A ⊢ ⟨l', Z'⟩ ↝⇘k,v,n⇙ ⟨l'', Z''⟩
        ⟹ A ⊢ ⟨l, Z⟩ ↝⇘k,v,n⇙* ⟨l'', Z''⟩"

context Regions
begin

abbreviation "v' ≡ beta_interp.v'"

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

abbreviation steps_z_norm' ("_ ⊢ ⟨_, _⟩ ↝⇩𝒩* ⟨_, _⟩" [61,61,61] 61)
where
  "A ⊢ ⟨l, D⟩ ↝⇩𝒩* ⟨l', D'⟩ ≡ A ⊢ ⟨l, D⟩ ↝⇘(k o v'),v,n⇙* ⟨l', D'⟩"

inductive_cases[elim!]: "A ⊢ ⟨l, u⟩ ↝⇩𝒩 ⟨l',u'⟩"

declare step_z_norm.intros[intro]

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

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]

lemma step_z_valid_dbm:
  assumes "A ⊢ ⟨l, D⟩ ↝⇘v,n⇙ ⟨l', D'⟩"
    and "global_clock_numbering A v n" "valid_abstraction A X k" "valid_dbm D"
  shows "valid_dbm D'"
proof -
  from alpha_interp.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⇙⟩ ↝ ⟨l', [D']⇘v,n⇙⟩"
  by fastforce+
  with alpha_interp.step_z_V[OF this(2)] assms(4) show ?thesis by auto
qed

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 cn_weak: "∀k≤n. 0 < k ⟶ (∃c. v c = k)" using clock_numbering(2) by blast

lemma valid_dbm_non_empty_diag:
  assumes "valid_dbm M" "[M]⇘v,n⇙ ≠ {}"
  shows "∀ k ≤ n. M k k ≥ 𝟭"
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(2)] show "𝟭 ≤ M k k" by (simp add: cyc_free_diag_dest')
qed

lemma non_empty_cycle_free:
  assumes "[M]⇘v,n⇙ ≠ {}"
  shows "cycle_free M n"
by (meson assms clock_numbering(2) neg_cycle_empty negative_cycle_dest_diag)

lemma norm_empty_diag_preservation:
  assumes "i ≤ n"
  assumes "M i i < Le 0"
  shows "norm M (k o v') n i i < Le 0"
proof -
  have "¬ Le (k (v' i)) ≺ Le 0" by auto
  with assms show ?thesis unfolding norm_def by (auto simp: Let_def less)
qed

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) cycle_free_diag_equiv have "¬ cycle_free M n"
  by metis
  from FW_neg_cycle_detect[OF this] obtain i where i: "i ≤ n" "FW M n i i < 𝟭" by auto
  with norm_empty_diag_preservation[folded neutral] have "?M i i < 𝟭" .
  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_cycle_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]
      valid_dbm_non_empty_diag[OF assms(1,2)] assms(1)
 show "Approx⇩β ([M]⇘v,n⇙) = [norm (FW M n) (k o v') n]⇘v,n⇙" by auto
 
qed

print_statement step_z_norm.inducts

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

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

text ‹Obsolete›
lemma norm_diag_preservation:
  assumes "∀l≤n. M1 l l ≤ 𝟭"
  shows "∀l≤n. (norm M1 (k o v') n) l l ≤ 𝟭" (is "∀ l ≤ n. ?M l l ≤ 𝟭")
proof safe
  fix j assume j: "j ≤ n"
  show "?M j j ≤ 𝟭"
  proof (cases "j = 0")
    case True
    with j assms show ?thesis unfolding norm_def neutral less_eq dbm_le_def by auto
  next
    case False
    have *: "real ((k ∘ v') j) ≥ 0" by auto
    from j assms have **: "M1 j j ≤ Le 0" unfolding neutral by auto
    have "norm_upper (M1 j j) (real ((k ∘ v') j)) = M1 j j"
    using * ** apply (cases "M1 j j") apply auto by fastforce+
    with assms(1) j False have
      "?M j j = norm_lower (M1 j j) (- real ((k ∘ v') j))"
    unfolding norm_def by auto
    with ** show ?thesis unfolding neutral by auto
  qed
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_cycle_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_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_beta_sound:
  assumes "A ⊢ ⟨l,D⟩ ↝⇩𝒩 ⟨l',D'⟩" "global_clock_numbering A v n" "valid_abstraction A X k"
  and     "valid_dbm D"
  shows   "A ⊢ ⟨l,[D]⇘v,n⇙⟩ ↝⇩β ⟨l',[D']⇘v,n⇙⟩" using assms(2-)
proof (induction A l D l' D' rule: step_z_norm_induct, intro assms(1))
  case (step_z_norm A l D l' D')
  from step_z_dbm_sound[OF step_z_norm(1,2)] have "A ⊢ ⟨l, [D]⇘v,n⇙⟩ ↝ ⟨l',[D']⇘v,n⇙⟩" by blast
  then have *: "A ⊢ ⟨l, [D]⇘v,n⇙⟩ ↝⇩β ⟨l',Approx⇩β ([D']⇘v,n⇙)⟩" by force
  show ?case
  proof (cases "[D']⇘v,n⇙ = {}")
    case False
    from apx_norm_eq_spec[OF step_z_valid_dbm[OF step_z_norm] False] *
    show ?thesis by auto
  next
    case True
    with norm_FW_empty[OF step_z_valid_dbm[OF step_z_norm] this] beta_interp.apx_empty *
    show ?thesis by auto
  qed
qed

lemma step_z_norm_valid_dbm:
  assumes "A ⊢ ⟨l, D⟩ ↝⇩𝒩 ⟨l',D'⟩" "global_clock_numbering A v n" "valid_abstraction A X k" "valid_dbm D"
  shows "valid_dbm D'" using assms(2-)
proof (induction A l D l' D' rule: step_z_norm_induct, intro assms(1))
  case (step_z_norm A l D l' D')
  with norm_FW_valid_preservation[OF step_z_valid_dbm[OF step_z_norm]] show ?case by fast
qed

lemma norm_beta_complete:
  assumes "A ⊢ ⟨l,[D]⇘v,n⇙⟩ ↝⇩β ⟨l',Z⟩" "global_clock_numbering A v n" "valid_abstraction A X k"
  and     "valid_dbm D"
  obtains D' where "A ⊢ ⟨l,D⟩ ↝⇩𝒩 ⟨l',D'⟩" "[D']⇘v,n⇙ = Z" "valid_dbm D'"
proof -
  from assms(1) obtain Z' where Z': "A ⊢ ⟨l,[D]⇘v,n⇙⟩ ↝ ⟨l',Z'⟩" "Z = Approx⇩β 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,3)] obtain D' where
    D': "A ⊢ ⟨l, D⟩ ↝⇘v,n⇙ ⟨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 ∘ v') n" by auto
  show ?thesis
  proof (cases "Z' = {}")
    case False
    with D' have *: "[D']⇘v,n⇙ ≠ {}" by auto
    from apx_norm_eq_spec[OF valid_D' this] D'' D'(2) Z'(2) assms(4) have "Z = [D'']⇘v,n⇙" by auto
    with norm_FW_valid_preservation[OF valid_D'] D' D'' * that[of D''] assms(4)
    show thesis by blast
  next
    case True
    with norm_FW_empty[OF valid_D'[OF assms(4)]] D'' D' Z'(2)
         norm_FW_valid_preservation[OF valid_D'[OF assms(4)]] beta_interp.apx_empty
    show thesis
    apply -
    apply (rule that[of D''])
      apply blast
    by fastforce+
  qed
qed

subsection ‹Multi step›

declare steps_z_norm.intros[intro]

lemma steps_z_norm_induct[case_names _ refl step]:
  assumes "x1 ⊢ ⟨x2, x3⟩ ↝⇘(k o v'),v,n⇙* ⟨x7,x8⟩"
    and "⋀A l Z. P A l Z l Z"
    and
    "⋀A l Z l' Z' l'' Z''.
        A ⊢ ⟨l, Z⟩ ↝⇘(k o v'),v,n⇙* ⟨l',Z'⟩ ⟹
        P A l Z l' Z' ⟹
        A ⊢ ⟨l', Z'⟩ ↝⇘(k o v'),v,n⇙ ⟨l'',Z''⟩ ⟹ P A l Z l'' Z''"
  shows "P x1 x2 x3 x7 x8"
using assms by (induction rule: steps_z_norm.induct) auto

lemma norm_beta_sound_multi:
  assumes "A ⊢ ⟨l,D⟩ ↝⇩𝒩* ⟨l',D'⟩" "global_clock_numbering A v n" "valid_abstraction A X k" "valid_dbm D"
  shows "A ⊢ ⟨l,[D]⇘v,n⇙⟩ ↝⇩β* ⟨l',[D']⇘v,n⇙⟩ ∧ valid_dbm D'" using assms(2-)
proof (induction A l D l' D' rule: steps_z_norm_induct, intro assms(1))
  case refl then show ?case by fast
next
  case (step A l Z l' Z' l'' Z'')
  then have "A ⊢ ⟨l, [Z]⇘v,n⇙⟩ ↝⇩β* ⟨l',[Z']⇘v,n⇙⟩" "valid_dbm Z'" by fast+
  with norm_beta_sound[OF step(2,4,5)] step_z_norm_valid_dbm[OF step(2,4,5)] show ?case by force
qed

lemma norm_beta_complete_multi:
  assumes "A ⊢ ⟨l,[D]⇘v,n⇙⟩ ↝⇩β* ⟨l',Z⟩" "global_clock_numbering A v n" "valid_abstraction A X k"
  and     "valid_dbm D"
  obtains D' where "A ⊢ ⟨l,D⟩ ↝⇩𝒩* ⟨l',D'⟩" "[D']⇘v,n⇙ = Z" "valid_dbm D'"
using assms
proof (induction A l "[D]⇘v,n⇙" l' Z arbitrary: thesis rule: steps_z_beta.induct)
  case refl
  from this(1)[OF steps_z_norm.refl] this(4) show thesis by fast
next
  case (step A l l' Z' l'' Z'')
  from step(2)[OF _ step(5,6,7)] obtain D' where D':
    "A ⊢ ⟨l, D⟩ ↝⇩𝒩* ⟨l',D'⟩" "[D']⇘v,n⇙ = Z'" "valid_dbm D'"
  .
  with norm_beta_complete[OF _ step(5,6), of l' D' l'' Z''] step(3) obtain D'' where D'':
    "A ⊢ ⟨l', D'⟩ ↝⇩𝒩 ⟨l'',D''⟩" "[D'']⇘v,n⇙ = Z''" "valid_dbm D''"
  by auto
  with D'(1) step(4)[of D''] show thesis by blast
qed

lemma norm_beta_equiv_multi:
  assumes "global_clock_numbering A v n" "valid_abstraction A X k"
  and     "valid_dbm D"
  shows "(∃ D'. A ⊢ ⟨l,D⟩ ↝⇩𝒩* ⟨l',D'⟩ ∧ Z = [D']⇘v,n⇙) ⟷ A ⊢ ⟨l,[D]⇘v,n⇙⟩ ↝⇩β* ⟨l',Z⟩"
using norm_beta_complete_multi[OF _ assms] norm_beta_sound_multi[OF _ assms] by metis


subsection ‹Connecting with Correctness Results for Approximating Semantics›

lemma steps_z_norm_complete':
  assumes "A ⊢ ⟨l,[D]⇘v,n⇙⟩ ↝* ⟨l',Z⟩" "global_clock_numbering A v n" "valid_abstraction A X k"
  and "valid_dbm D"
  shows "∃ D'. A ⊢ ⟨l, D⟩ ↝⇩𝒩* ⟨l',D'⟩ ∧  Z ⊆ [D']⇘v,n⇙"
proof -
  from steps_z_beta_complete[OF assms(1,3)] assms(4) obtain Z'' where Z'':
    "A ⊢ ⟨l, [D]⇘v,n⇙⟩ ↝⇩β* ⟨l',Z''⟩" "Z ⊆ Z''"
  by auto
  from this(2) norm_beta_complete_multi[OF this(1) assms(2,3,4)] show ?thesis by metis
qed

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

lemma steps_z_norm_sound':
  assumes "A ⊢ ⟨l,D⟩ ↝⇩𝒩* ⟨l',D'⟩"
    and "global_clock_numbering A v n"
    and "valid_abstraction A X k"
    and "valid_dbm D"
    and "[D']⇘v,n⇙ ≠ {}"
  shows "∃Z. A ⊢ ⟨l,[D]⇘v,n⇙⟩ ↝* ⟨l',Z⟩ ∧ Z ≠ {}"
proof -
  from norm_beta_sound_multi[OF assms(1-4)] have "A ⊢ ⟨l, [D]⇘v,n⇙⟩ ↝⇩β* ⟨l',[D']⇘v,n⇙⟩" by fast
  from steps_z_beta_sound[OF this _ assms(3) valid_dbm_V'] assms(2,4,5) show ?thesis by blast
qed


section ‹The Final Result About Language Emptiness›

lemma steps_z_norm_complete:
  assumes "A ⊢ ⟨l, u⟩ →* ⟨l', u'⟩" "u ∈ [D]⇘v,n⇙"
    and   "global_clock_numbering A v n" "valid_abstraction A X k" "valid_dbm D"
  shows "∃ D'. A ⊢ ⟨l, D⟩ ↝⇩𝒩* ⟨l',D'⟩ ∧ u' ∈ [D']⇘v,n⇙"
using steps_z_norm_complete'[OF _ assms(3-)] steps_z_complete[OF assms(1,2)] by fast

lemma steps_z_norm_sound:
  assumes "A ⊢ ⟨l,D⟩ ↝⇩𝒩* ⟨l',D'⟩"
    and   "global_clock_numbering A v n" "valid_abstraction A X k" "valid_dbm D"
    and   "[D']⇘v,n⇙ ≠ {}"
  shows "∃ u ∈ [D]⇘v,n⇙. ∃ u'. A ⊢ ⟨l, u⟩ →* ⟨l', u'⟩"
using steps_z_norm_sound'[OF assms] steps_z_sound by fast

theorem steps_z_norm_decides_emptiness:
  assumes "global_clock_numbering A v n" "valid_abstraction A X k" "valid_dbm D"
  shows "(∃ D'. A ⊢ ⟨l, D⟩ ↝⇩𝒩* ⟨l',D'⟩ ∧ [D']⇘v,n⇙ ≠ {})
     ⟷ (∃ u ∈ [D]⇘v,n⇙. ∃ u'. A ⊢ ⟨l, u⟩ →* ⟨l', u'⟩)"
using steps_z_norm_sound[OF _ assms] steps_z_norm_complete[OF _ _ assms] by fast


section ‹Finiteness of the Search Space›

abbreviation "dbm_default M ≡ (∀ i > n. ∀ j. M i j = 𝟭) ∧ (∀ j > n. ∀ i. M i j = 𝟭)"

lemma "a ∈ ℤ ⟹ ∃ b. a = real_of_int b" using Ints_cases by auto

lemma norm_default_preservation:
  "dbm_default M ⟹ dbm_default (norm M (k o v') n)"
by (simp add: norm_def)

lemma normalized_integral_dbms_finite:
  "finite {norm M (k o v') n | M. dbm_int M n ∧ dbm_default M}"
proof -
  let ?u = "Max {(k o v') i | i. i ≤ n}" let ?l = "- ?u"
  let ?S = "(Le ` {d :: int. ?l ≤ d ∧ d ≤ ?u}) ∪ (Lt ` {d :: int. ?l ≤ d ∧ d ≤ ?u}) ∪ {∞}"
  from finite_set_of_finite_funs2[of "{0..n}" "{0..n}" ?S] have fin:
    "finite {f. ∀x y. (x ∈ {0..n} ∧ y ∈ {0..n} ⟶ f x y ∈ ?S)
                ∧ (x ∉ {0..n} ⟶ f x y = 𝟭) ∧ (y ∉ {0..n} ⟶ f x y = 𝟭)}" (is "finite ?R")
  by auto
  { fix M :: "t DBM" assume A: "dbm_int M n" "dbm_default M"
    let ?M = "norm M (k o v') n"
    from beta_interp.norm_int_preservation[OF A(1)] norm_default_preservation[OF A(2)] have
      A: "dbm_int ?M n" "dbm_default ?M"
    by blast+
    { fix i j assume "i ∈ {0..n}" "j ∈ {0..n}"
      then have B: "i ≤ n" "j ≤ n" by auto
      have "?M i j ∈ ?S"
      proof (cases "?M i j = ∞")
        case True then show ?thesis by auto
      next
        case False
        note not_inf = this
        with B A(1) have "get_const (?M i j) ∈ ℤ" by auto
        moreover have "?l ≤ get_const (?M i j) ∧ get_const (?M i j) ≤ ?u"
        proof (cases "i = 0")
          case True
          show ?thesis
          proof (cases "j = 0")
            case True
            with ‹i = 0› A(1) B have
              "?M i j = norm_lower (norm_upper (M 0 0) 0) 0"
            unfolding norm_def by auto
            also have "… ≠ ∞ ⟶ get_const … = 0" by (cases "M 0 0"; fastforce)
            finally show ?thesis using not_inf by auto
          next
            case False
            with ‹i = 0› B not_inf have "?M i j ≤ Le 0" "Lt (-real (k (v' j))) ≤ ?M i j"
            by (unfold norm_def, auto simp: Let_def, unfold less[symmetric], auto)
            with not_inf have "get_const (?M i j) ≤ 0" "-k (v' j) ≤ get_const (?M i j)"
            by (cases "?M i j"; auto)+
            moreover from ‹j ≤ n› have "- (k o v') j ≥ ?l" by (auto intro: Max_ge)
            ultimately show ?thesis by auto
          qed
        next
          case False
          then have "i > 0" by simp
          show ?thesis
          proof (cases "j = 0")
            case True
            with ‹i > 0› A(1) B not_inf have "Lt 0 ≤ ?M i j" "?M i j ≤ Le (real ((k ∘ v') i))"
            by (unfold norm_def, auto simp: Let_def, unfold less[symmetric], auto)
            with not_inf have "0 ≤ get_const (?M i j)" "get_const (?M i j) ≤ k (v' i)"
            by (cases "?M i j"; auto)+
            moreover from ‹i ≤ n› have "(k o v') i ≤ ?u" by (auto intro: Max_ge)
            ultimately show ?thesis by auto
          next
            case False
            with ‹i > 0› A(1) B not_inf have
              "Lt (-real ((k ∘ v') j)) ≤ ?M i j" "?M i j ≤ Le (real ((k ∘ v') i))"
            by (unfold norm_def, auto simp: Let_def, unfold less[symmetric], auto)
            with not_inf have "- k (v' j) ≤ get_const (?M i j)" "get_const (?M i j) ≤ k (v' i)"
            by (cases "?M i j"; auto)+
            moreover from ‹i ≤ n› ‹j ≤ n› have "(k o v') i ≤ ?u" "(k o v') j ≤ ?u" by (auto intro: Max_ge)
            ultimately show ?thesis by auto
          qed
        qed
        ultimately show ?thesis by (cases "?M i j"; auto elim: Ints_cases)
      qed
    } moreover
    { fix i j assume "i ∉ {0..n}"
      with A(2) have "?M i j = 𝟭" by auto
    } moreover
    { fix i j assume "j ∉ {0..n}"
      with A(2) have "?M i j = 𝟭" by auto
    } moreover note the = calculation
  } then have "{norm M (k o v') n | M. dbm_int M n ∧ dbm_default M} ⊆ ?R" by blast
  with fin show ?thesis by (blast intro: finite_subset)
qed

end


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
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 (clkp_set A)" "finite (collect_clkvt (trans_of A))" "∀(_,m::real) ∈ clkp_set A. m ∈ ℕ"
  obtains k :: "'c ⇒ nat" where "valid_abstraction A (clk_set A) k"
proof -
  from assms have 1: "finite (clk_set A)" by auto
  have 2: "collect_clkvt (trans_of A) ⊆ clk_set A" by auto
  from assms obtain L where L: "distinct L" "set L = clkp_set A" by (meson finite_distinct_list)
  let ?M = "λ c. {m . (c, m) ∈ 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) ∈ clkp_set A"
    from assms(1) have "finite (snd ` clkp_set A)" by auto
    moreover have "?M c ⊆ (snd ` clkp_set A)" by force
    ultimately have fin: "finite (?M c)" by (blast intro: finite_subset)
    then have "Max (?M c) ∈ {m . (c, m) ∈ 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)
    with A have *: "?k c = Max (?M c) + 1"
    proof auto
      fix n :: int and x :: real
      assume "Max {m. (c, m) ∈ clkp_set A} = real_of_int n"
      then have "real_of_int (n + 1) ∈ ℕ"
        using ‹Max {m. (c, m) ∈ clkp_set A} ∈ ℕ› by auto
      then show "real (nat (n + 1)) = real_of_int n + 1"
        by (metis Nats_cases ceiling_of_int nat_int of_int_1 of_int_add of_int_of_nat_eq)
    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)∈clkp_set A. m ≤ ?k x ∧ x ∈ clk_set A ∧ m ∈ ℕ" by blast
  with 1 2 have "valid_abstraction A ?X ?k" by - (standard, assumption+)
  then show thesis ..
qed

definition
  "finite_ta A ≡ finite (clkp_set A) ∧ finite (collect_clkvt (trans_of A))
                 ∧ (∀(_,m::real) ∈ 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:
  assumes "finite_ta A"
  obtains k :: "'b ⇒ nat" and v n x where
    "Regions' (clk_set A) v n x" "valid_abstraction A (clk_set A) k" "global_clock_numbering A v n"
proof -
  from standard_abstraction assms obtain k :: "'b ⇒ nat" where k:
    "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 ≤ 𝟭)"

lemma dbm_positive:
  assumes "M 0 (v c) ≤ 𝟭" "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

text ‹
  An example of obtaining concrete models from our formalizations.
›
lemma steps_z_norm_sound_spec:
  assumes "finite_ta A"
  obtains k v n where
  "A ⊢ ⟨l,D⟩ ↝⇘k,v,n⇙* ⟨l',D'⟩ ∧ valid_dbm D n ∧ [D']⇘v,n⇙ ≠ {}
  ⟶ (∃Z. A ⊢ ⟨l, [D]⇘v,n⇙⟩ ↝* ⟨l',Z⟩ ∧ Z ≠ {})"
proof -
  from finite_ta_RegionsD[OF assms(1)] obtain k :: "'b ⇒ nat" and v n x where *:
    "Regions' (clk_set A) v n x" "valid_abstraction A (clk_set A) k" "global_clock_numbering A v n"
  .
  from this(1) interpret interp: Regions' "clk_set A" k v n x .
  define v' where "v' i = (if i ≤ n then (THE c. c ∈ clk_set A ∧ v c = i) else x)" for i
  { fix l D l' D'
    assume step: "A ⊢ ⟨l,D⟩ ↝⇘(k o v'),v,n⇙* ⟨l',D'⟩"
    and valid: "valid_dbm D n" and non_empty: "[D']⇘v,n⇙ ≠ {}"
    from valid_dbm_pos[OF valid] interp.V_alt_def have "[D]⇘v,n⇙ ⊆ interp.V" by blast
    with valid have valid: "interp.valid_dbm D" unfolding valid_dbm_def by auto
    from step have "interp.steps_z_norm' A l D l' D'" unfolding v'_def interp.beta_interp.v'_def .
    note this = interp.steps_z_norm_sound'[OF this *(3,2) valid non_empty]
  }
  then show thesis by (blast intro: that)
qed

end