Theory TA_Simulation

section ‹Simulations on Timed Automata›
theory TA_Simulation
  imports
    Timed_Automata.Timed_Automata
    Timed_Automata.Normalized_Zone_Semantics
    Timed_Automata.Simulation_Graphs_TA
    "HOL-Eisbach.Eisbach"
    Simulation_Graphs2
    Munta_Base.Normalized_Zone_Semantics_Impl_Semantic_Refinement
"HOL-ex.Sketch_and_Explore"
begin

text ‹
This theory essentially formalizes the concepts from Guangyuan Li's FORMATS 2009 paper
``Checking Timed Büchi Automata Emptiness Using LU-Abstractions'' cite‹"Li:FORMATS:2009"›.
›

no_notation dbm_le ("_ ≼ _" [51, 51] 50)

subsection ‹Preliminaries›

lemma
  step_z_state_setI1: "l ∈ state_set A" and
  step_z_state_setI2: "l' ∈ state_set A" if "A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩"
  using that unfolding step_z'_def by (force simp: state_set_def trans_of_def)+

lemma step_trans_z'_sound:
  "A ⊢' ⟨l, Z⟩ ↝⇗t⇖ ⟨l', Z'⟩ ⟹ ∀u' ∈ Z'. ∃u ∈ Z. ∃d.  A ⊢' ⟨l, u⟩ →⇗t⇖ ⟨l',u'⟩"
  by (fastforce dest!: step_trans_a_z_sound step_trans_t_z_sound elim!: step_trans_z'.cases)

lemma step_trans_z'_exact_strong:
  assumes "A ⊢' ⟨l, Z⟩ ↝⇗t⇖ ⟨l', Z'⟩"
  shows "Z' = {u'. ∃u ∈ Z. A ⊢' ⟨l, u⟩ →⇗t⇖ ⟨l', u'⟩}"
  using step_trans_z'_sound assms by (auto dest: step_trans_z'_exact step_trans_z'_sound)

lemma step_a_step_trans_iff:
  "A ⊢ ⟨l, u⟩ →⇘a⇙ ⟨l', u'⟩ ⟷ (∃g r. A ⊢t ⟨l, u⟩ →⇘(g,a,r)⇙ ⟨l', u'⟩)"
  unfolding step_a.simps step_trans.simps by fast

lemma step_trans'_step_trans_iff:
  "(∃t. A ⊢' ⟨l, u⟩ →⇗t⇖ ⟨l', u'⟩) ⟷ A ⊢' ⟨l, u⟩ → ⟨l', u'⟩"
  unfolding step_trans'.simps step'.simps step_a_step_trans_iff by fast

subsection ‹Time-Abstract Simulation›

locale Time_Abstract_Simulation =
  fixes A :: "('a, 'c, 't :: time, 'l) ta"
  fixes sim :: "'l × ('c ⇒ 't :: time) ⇒ 'l × ('c ⇒ 't) ⇒ bool" (infix "≼" 60)
  assumes sim:
  "⋀l l' l1 u u' u1 t. (l, u) ≼ (l', u') ⟹ A ⊢' ⟨l, u⟩ →⇗t⇖ ⟨l1, u1⟩
    ⟹ ∃u1'. A ⊢' ⟨l', u'⟩ →⇗t⇖ ⟨l1, u1'⟩ ∧ (l1, u1) ≼ (l1, u1')"
  assumes refl: "⋀u. u ≼ u" and trans: "⋀u v w. u ≼ v ⟹ v ≼ w ⟹ u ≼ w"
begin

lemma simE:
  assumes "(l, u) ≼ (l', u')" "A ⊢' ⟨l, u⟩ →⇗t⇖ ⟨l1, u1⟩"
  obtains u1' where "A ⊢' ⟨l', u'⟩ →⇗t⇖ ⟨l1, u1'⟩" "(l1, u1) ≼ (l1, u1')"
  using assms sim by blast

definition abs :: "'l ⇒ ('c, 't) zone ⇒ ('c, 't) zone" ("α _ _" [71,71] 71) where
  "α l W = {v. ∃v' ∈ W. (l, v) ≼ (l, v')}"

lemma simulation_mono:
  assumes "α l Z ⊆ α l Z'" "A ⊢' ⟨l, Z⟩ ↝⇗t⇖ ⟨l1, Z1⟩" "A ⊢' ⟨l, Z'⟩ ↝⇗t⇖ ⟨l1, Z1'⟩"
  shows "α l1 Z1 ⊆ α l1 Z1'"
proof -
  have
    "Z1 = {u'. ∃u ∈ Z. A ⊢' ⟨l, u⟩ →⇗t⇖ ⟨l1, u'⟩}" "Z1' = {u'. ∃u ∈ Z'. A ⊢' ⟨l, u⟩ →⇗t⇖ ⟨l1, u'⟩}"
    by (intro step_trans_z'_exact_strong assms(2,3))+
  show ?thesis
    unfolding abs_def
  proof safe
    fix u v
    assume "v ∈ Z1" "(l1, u) ≼ (l1, v)"
    with ‹Z1 = _› obtain u0 where "u0 ∈ Z" and step: "A ⊢' ⟨l, u0⟩ →⇗t⇖ ⟨l1, v⟩"
      by auto
    from ‹u0 ∈ Z› ‹α l Z ⊆ _› obtain v0 where "v0 ∈ Z'" "(l, u0) ≼ (l, v0)"
      unfolding abs_def using refl[of "(l, u0)"] by auto
    from simE[OF ‹(l, u0) ≼ (l, v0)› step] obtain v' where
      "A ⊢' ⟨l, v0⟩ →⇗t⇖ ⟨l1, v'⟩" "(l1, v) ≼ (l1, v')" .
    with ‹v0 ∈ Z'› ‹Z1' = _› have "v' ∈ Z1'"
      by auto
    moreover from ‹_ ≼ (l1, v)› ‹(l1, v) ≼ _› have "(l1, u) ≼ (l1, v')"
      by (rule trans)
    ultimately show "∃x∈Z1'. (l1, u) ≼ (l1, x)"
      by fast
  qed
qed

lemma simulation:
  assumes "α l Z = α l Z'" "A ⊢' ⟨l, Z⟩ ↝⇗t⇖ ⟨l', Z1⟩" "A ⊢' ⟨l, Z'⟩ ↝⇗t⇖ ⟨l', Z1'⟩"
  shows "α l' Z1 = α l' Z1'"
  using simulation_mono assms by blast

lemma simulation':
  assumes "α l Z = α l Z'" "A ⊢' ⟨l, Z⟩ ↝⇗t⇖ ⟨l', Z1⟩"
  shows "∃Z1'. A ⊢' ⟨l, Z'⟩ ↝⇗t⇖ ⟨l', Z1'⟩ ∧ α l' Z1 = α l' Z1'"
proof -
  from ‹A ⊢' ⟨l, Z⟩ ↝⇗t⇖ ⟨l', Z1⟩› obtain Z1' where "A ⊢' ⟨l, Z'⟩ ↝⇗t⇖ ⟨l', Z1'⟩"
    by (auto elim!: step_trans_z'.cases step_trans_z.cases)
  with simulation assms show ?thesis
    by blast
qed

lemma abs_involutive:
  "α l (α l Z) = α l Z"
  unfolding abs_def by (auto intro: refl trans)

lemma abs_widens:
  "Z ⊆ α l Z"
  unfolding abs_def by (auto intro: refl)

text ‹
  This is Lemma 4 from the paper
  ``Better Abstractions for Timed Automata'' (🌐‹https://arxiv.org/abs/1110.3705›)
›
corollary transition_compatibility:
  assumes "A ⊢' ⟨l, α l Z⟩ ↝⇗t⇖ ⟨l', W⟩" "A ⊢' ⟨l, Z⟩ ↝⇗t⇖ ⟨l', Z'⟩"
  shows "α l' W = α l' Z'"
  by (rule simulation[OF _ assms(1,2)], rule abs_involutive)

inductive step_abs ::
  "('a, 'c, 't, 'l) ta ⇒ 'l ⇒ ('c, 't) zone ⇒ 'a ⇒ 'l ⇒ ('c, 't) zone ⇒ bool"
("_ ⊢ ⟨_, _⟩ ↝⇘α(_)⇙ ⟨_, _⟩" [61,61,61] 61)
where
  step_alpha:
    "A ⊢ ⟨l, Z⟩ ↝⇘τ⇙ ⟨l', Z'⟩ ⟹ A ⊢ ⟨l', Z'⟩ ↝⇘↿a⇙ ⟨l'', Z''⟩
  ⟹ A ⊢ ⟨l, α l Z⟩ ↝⇘α(a)⇙ ⟨l'', α l'' Z''⟩"

interpretation sim1: Simulation where
  A = "λ(l, u) (l', u'). A ⊢' ⟨l, u⟩ → ⟨l', u'⟩" and
  B = "λ(l, Z) (l', Z'). ∃a. A ⊢ ⟨l, Z⟩ ↝⇘α(a)⇙ ⟨l', Z'⟩" and
  sim = "λ(l, u) (l', Z). l' = l ∧ u ∈ Z ∧ α l Z = Z"
  apply standard
  unfolding step'.simps step_abs.simps
  apply clarsimp
  subgoal premises prems for l v l'' v'' Z d l' v' a
  proof -
    from ‹v ∈ Z› ‹A ⊢ ⟨l, v⟩ →⇗d⇖ ⟨l', v'⟩› obtain Z' where
      "A ⊢ ⟨l, Z⟩ ↝⇘τ⇙ ⟨l', Z'⟩" "v' ∈ Z'"
      by (auto dest: step_t_z_complete)
    moreover obtain Z'' where
      "A ⊢ ⟨l', Z'⟩ ↝⇘↿a⇙ ⟨l'', Z''⟩" "v'' ∈ Z''"
      using prems ‹v' ∈ Z'› by (auto dest: step_a_z_complete)
    ultimately show ?thesis
      using ‹α l Z = Z› abs_involutive abs_widens by blast
  qed
  done

interpretation sim2: Simulation where
  A = "λ(l, u) (l', u'). A ⊢' ⟨l, u⟩ → ⟨l', u'⟩" and
  B = "λ(l, Z) (l', Z'). ∃a. A ⊢ ⟨l, α l Z⟩ ↝⇘α(a)⇙ ⟨l', α l' Z'⟩" and
  sim = "λ(l, u) (l', Z). l' = l ∧ u ∈ Z"
  apply standard
  unfolding step'.simps step_abs.simps
  apply clarsimp
  subgoal premises prems for l v l'' v'' Z d l' v' a
  proof -
    from ‹v ∈ Z› ‹A ⊢ ⟨l, v⟩ →⇗d⇖ ⟨l', v'⟩› obtain Z' where
      "A ⊢ ⟨l, Z⟩ ↝⇘τ⇙ ⟨l', Z'⟩" "v' ∈ Z'"
      by (auto dest: step_t_z_complete)
    moreover obtain Z'' where
      "A ⊢ ⟨l', Z'⟩ ↝⇘↿a⇙ ⟨l'', Z''⟩" "v'' ∈ Z''"
      using prems ‹v' ∈ Z'› by (auto dest: step_a_z_complete)
    ultimately show ?thesis
      by fastforce
  qed
  done

sublocale self_simulation: Self_Simulation where
  E = "λ(l, u) (l', u'). A ⊢' ⟨l, u⟩ → ⟨l', u'⟩" and P = "λ_. True"
  apply standard
  apply (force dest: sim simp: step_trans'_step_trans_iff[symmetric])
  using refl trans unfolding reflp_def transp_def by blast+

end


context Regions_TA
begin

definition sim_regions (infix "≡M" 60) where
  "sim_regions ≡ λ(l, u) (l', u').
    (l' = l ∧ l ∈ state_set A ∧ (∃R ∈ ℛ l. u ∈ R ∧ u' ∈ R))
  ∨ (l ∉ state_set A ∨ u ∉ V) ∧ (l' ∉ state_set A ∨ u' ∉ V)"

abbreviation
  "valid ≡ λ(l, u). l ∈ state_set A ∧ u ∈ V"

lemma ℛ_I:
  assumes "l ∈ state_set A" "u ∈ V"
  shows "∃R ∈ ℛ l. u ∈ R"
  using assms regions_partition[where ℛ = ‹ℛ l› and X = X and k = "k l" and u = u] ℛ_def[of l]
  unfolding V_def by blast

lemma regions_finite:
  "finite (ℛ l)"
  using finite_ℛ[OF finite] unfolding ℛ_def .

lemma valid_iff:
  "valid (l, u) ⟷ valid (l', u')" if "(l, u) ≡M (l', u')"
  using that unfolding sim_regions_def by (auto dest: ℛ_V)

lemma refl:
  "(l, u) ≡M (l, u)"
  unfolding sim_regions_def by (cases "valid (l, u)"; simp add: ℛ_I)

lemma sym:
  "(l, u) ≡M (l', u') ⟷ (l', u') ≡M (l, u)"
  unfolding sim_regions_def by auto

lemma trans:
  "(l, u) ≡M (l'', u'')" if "(l, u) ≡M (l', u')" "(l', u') ≡M (l'', u'')"
proof (cases "valid (l, u)")
  case True
  with that have "valid (l, u)" "valid (l', u')" "valid (l'', u'')"
    using valid_iff by metis+
  then show ?thesis
    using that unfolding sim_regions_def by (auto dest: ℛ_regions_distinct[rotated 2])
next
  case False
  with that have "¬ valid (l, u)" "¬ valid (l', u')" "¬ valid (l'', u'')"
    using valid_iff by metis+
  then show ?thesis
    unfolding sim_regions_def by simp
qed

lemma equiv:
  "equivp (≡M)"
  using refl sym trans by - (rule equivpI; unfold equivp_def reflp_def symp_def transp_def; fast)

lemma same_loc:
  "l' = l" if "(l, u) ≡M (l', u')" "valid (l, u)"
  using that unfolding sim_regions_def by auto

lemma regions_simI:
  "(l, u) ≡M (l, u')" if "l ∈ state_set A" "R ∈ ℛ l" "u ∈ R" "u' ∈ R"
  using that unfolding sim_regions_def by auto

lemma regions_simD:
  "u' ∈ R" if "l ∈ state_set A" "R ∈ ℛ l" "u ∈ R" "(l, u) ≡M (l', u')"
  using that unfolding sim_regions_def by (auto dest: ℛ_V ℛ_regions_distinct)

lemma finite_quotient:
  "finite (UNIV // {(x, y). x ≡M y})"
proof -
  let ?S = "state_set A × (⋃l ∈ state_set A. ℛ l)" and ?f = "λ(l, R). from_R l R"
  let ?invalid = "{(l, u). ¬valid (l, u)}"
  have "Collect ((≡M) (l, u)) ∈ ?f ` ?S"
    if "valid (l, u)" for l u
  proof -
    from that refl[of l u] obtain R where *: "l ∈ state_set A" "R ∈ ℛ l" "u ∈ R"
      unfolding sim_regions_def by auto
    with ‹valid _› have "Collect ((≡M) (l, u)) = from_R l R"
      unfolding from_R_def by (auto simp: same_loc intro: regions_simI regions_simD)
    with * show ?thesis
      by auto
  qed
  moreover have "Collect ((≡M) (l, u)) = ?invalid" if "¬ valid (l, u)" for l u
    using that unfolding sim_regions_def by (auto simp: ℛ_V)
  ultimately have "UNIV // {(x, y). x ≡M y} ⊆ (?f ` ?S) ∪ {?invalid}"
    apply -
    apply (rule subsetI)
    apply (erule quotientE)
    apply clarsimp
    by blast
  also have "finite …"
     by (blast intro: finite_state_set regions_finite)+
   finally show ?thesis .
 qed

sublocale region_self_simulation: Self_Simulation where
  E = "λ(l, u) (l', u'). A ⊢' ⟨l, u⟩ → ⟨l', u'⟩" and sim = "(≡M)" and P = valid
  apply (standard; clarsimp?)
  subgoal simulation premises prems for l u l1 u1 l' u'
  proof -
    from ‹u ∈ V› ‹A ⊢' ⟨l, u⟩ → ⟨l1, u1⟩›[THEN step_r'_complete_spec] obtain a R1 where
      "u1 ∈ R1" "A,ℛ ⊢ ⟨l, [u]⇩l⟩ ↝⇩a ⟨l1, R1⟩"
      by blast
    moreover from prems have "u' ∈ [u]⇩l"
      unfolding V_def by (auto elim: regions_simD dest: region_cover')
    ultimately obtain u1' where "u1' ∈ R1" "A ⊢' ⟨l, u'⟩ → ⟨l1, u1'⟩"
      by (auto 4 3 dest: step_r'_sound)
    moreover from ‹u1 ∈ R1› ‹u1' ∈ R1› ‹A,ℛ ⊢ ⟨l, [u]⇩l⟩ ↝⇩a ⟨l1, R1⟩› have "(l1, u1) ≡M (l1, u1')"
      by (meson regions_simI step_r'_ℛ step_r'_state_set)
    moreover from prems have "valid (l', u')"
      using valid_iff by auto
    moreover from prems have "l' = l"
      by - (erule same_loc, simp)
    ultimately show ?thesis
      using ‹(l, u) ≡M (l', u')› by blast
  qed
  subgoal invariant
    by (meson ℛ_V step_r'_ℛ step_r'_complete_spec step_r'_state_set)
  using refl trans unfolding reflp_def transp_def by fast+

end


subsection ‹LU-Simulation›

definition
  "constraints_of A l = ⋃ (set ` insert (inv_of A l) {g. ∃a r l'. (l, g, a, r, l') ∈ trans_of A})"

definition
  "is_lower A L ≡
  ∀l. ∀ac ∈ constraints_of A l. case ac of
    GT c x ⇒ L l c ≥ x |
    GE c x ⇒ L l c ≥ x |
    EQ c x ⇒ L l c ≥ x |
    _ ⇒ True"

definition
  "is_upper A U ≡
  ∀l. ∀ac ∈ constraints_of A l. case ac of
    LT c x ⇒ U l c ≥ x |
    LE c x ⇒ U l c ≥ x |
    EQ c x ⇒ U l c ≥ x |
    _ ⇒ True"

definition
  "is_locally_consistent A k ≡
  ∀(l, g, a, r, l') ∈ trans_of A. ∀x ∈ clk_set A - set r. k l x ≥ k l' x"

lemma is_locally_consistentD:
  assumes "is_locally_consistent A k" "A ⊢ l ⟶⇗g,a,r⇖ l1"
  shows "∀x ∈ clk_set A - set r. k l x ≥ k l1 x"
  using assms unfolding is_locally_consistent_def by fast

locale TA_LU =
  fixes A :: "('a, 'c, 't :: time, 'l) ta"
  fixes L :: "'l ⇒ 'c ⇒ 't" and U :: "'l ⇒ 'c ⇒ 't"
  assumes is_lower: "is_lower A L" and is_upper: "is_upper A U"
      and locally_consistent: "is_locally_consistent A L" "is_locally_consistent A U"
begin

definition sim :: "'l × ('c ⇒ 't :: time) ⇒ 'l × ('c ⇒ 't) ⇒ bool" (infix "≼" 60) where
  "sim ≡ λ(l, v) (l', v').
    l' = l ∧ (∀x ∈ clk_set A. (v' x < v x ⟶ v' x > L l x) ∧ (v' x > v x ⟶ v x > U l x))"

lemma simE:
  assumes "(l, v) ≼ (l', v')" "x ∈ clk_set A"
  obtains "l' = l" "v x = v' x"
  | "l' = l" "v x > v' x" "v' x > L l x"
  | "l' = l" "v x < v' x" "v x > U l x"
  using assms unfolding sim_def by force

lemma sim_locD:
  "l' = l" if "(l, v) ≼ (l', v')"
  using that unfolding sim_def by auto

lemma sim_nonneg:
  "u x ≥ 0" if "(l, u) ≼ (l', u')" "u' x ≥ 0" "x ∈ clk_set A" "U l x ≥ 0"
  using that by (auto elim: simE)

lemma sim_time_shift:
  "(l, v ⊕ d) ≼ (l', v' ⊕ d)" if "(l, v) ≼ (l', v')" "d ≥ 0"
  using that unfolding cval_add_def sim_def by simp (metis add.commute add_strict_increasing2)

lemma constraints_of_clk_set:
  assumes "g ∈ constraints_of A l"
  shows
    "g = LT c x ⟹ c ∈ clk_set A"
    "g = LE c x ⟹ c ∈ clk_set A"
    "g = EQ c x ⟹ c ∈ clk_set A"
    "g = GE c x ⟹ c ∈ clk_set A"
    "g = GT c x ⟹ c ∈ clk_set A"
  using assms
  unfolding constraints_of_def
  unfolding collect_clkvt_def clkp_set_def
  unfolding
    Timed_Automata.clkp_set_def Timed_Automata.collect_clki_def Timed_Automata.collect_clkt_def
  unfolding collect_clock_pairs_def
  by auto (smt UnCI Union_iff constraint_pair.simps fst_conv image_eqI mem_Collect_eq)+

lemma constraint_simulation:
  assumes "g ∈ constraints_of A l" "(l, v) ≼ (l', v')" "v ⊢a g"
  shows "v' ⊢a g"
  using assms(3,1,2) is_lower is_upper unfolding is_lower_def is_upper_def
  by cases(all ‹frule (1) constraints_of_clk_set; erule (1) simE; fastforce simp: clock_val_a.simps›)

lemma inv_simulation:
  assumes "v ⊢ inv_of A l" "(l, v) ≼ (l', v')"
  shows "v' ⊢ inv_of A l"
proof -
  from assms(1) have "∀ac ∈ set (inv_of A l). v ⊢a ac"
    unfolding clock_val_def list_all_iff by auto
  moreover have "∀ac ∈ set (inv_of A l). ac ∈ constraints_of A l"
    unfolding constraints_of_def by auto
  ultimately show ?thesis
    using ‹_ ≼ _› unfolding clock_val_def list_all_iff by (auto intro: constraint_simulation)
qed

lemma guard_simulation:
  assumes "A ⊢ l ⟶⇗g,a,r⇖ l1" "v ⊢ g" "(l, v) ≼ (l', v')"
  shows "v' ⊢ g"
proof -
  from assms(2) have "∀ac ∈ set g. v ⊢a ac"
    unfolding clock_val_def list_all_iff by auto
  moreover from assms(1) have "∀ac ∈ set g. ac ∈ constraints_of A l"
    unfolding constraints_of_def by auto
  ultimately show ?thesis
    using ‹_ ≼ _› unfolding clock_val_def list_all_iff by (auto intro: constraint_simulation)
qed

lemma sim_delay:
  assumes "(l, v) ≼ (l', v')" "d ≥ 0"
  shows "(l, v ⊕ d) ≼ (l', v' ⊕ d)"
  using assms unfolding cval_add_def sim_def by (auto simp: add_strict_increasing2 gt_swap)

lemma clock_set_iff:
  "([r→0]v) c = (if c ∈ set r then 0 else v c)"
  by auto

lemma sim_reset:
  assumes "A ⊢ l ⟶⇗g,a,r⇖ l1" "v ⊢ g" "(l, v) ≼ (l', v')"
  shows "(l1, [r→0]v) ≼ (l1, [r→0]v')"
proof -
  from assms(1) have
    "∀x ∈ clk_set A - set r. L l x ≥ L l1 x" "∀x ∈ clk_set A - set r. U l x ≥ U l1 x"
    using locally_consistent by - (intro is_locally_consistentD; assumption)+
  then show ?thesis
    using assms(2,3) unfolding sim_def by (auto simp: clock_set_iff) force+
qed

lemma step_t_simulation:
  "(l, u) ≼ (l', u') ⟹ A ⊢ ⟨l, u⟩ →⇗d⇖ ⟨l1, u1⟩
  ⟹ ∃u1'. A ⊢ ⟨l1, u'⟩ →⇗d⇖ ⟨l1, u1'⟩ ∧ (l1, u1) ≼ (l, u1')"
  unfolding step_t.simps by (auto dest: sim_delay inv_simulation sim_locD)

lemma step_a_simulation:
  "(l, u) ≼ (l', u') ⟹ A ⊢ ⟨l, u⟩ →⇘a⇙ ⟨l1, u1⟩
  ⟹ ∃u1'. A ⊢ ⟨l, u'⟩ →⇘a⇙ ⟨l1, u1'⟩ ∧ (l1, u1) ≼ (l1, u1')"
  unfolding step_a.simps
  apply clarsimp
  apply (frule (2) guard_simulation)
  apply (drule (2) sim_reset[rotated -1])
  apply (frule (1) inv_simulation)
  apply auto
  done

lemma step_trans_simulation:
  "(l, u) ≼ (l', u') ⟹ A ⊢t ⟨l, u⟩ →⇘t⇙ ⟨l1, u1⟩
  ⟹ ∃u1'. A ⊢t ⟨l, u'⟩ →⇘t⇙ ⟨l1, u1'⟩ ∧ (l1, u1) ≼ (l1, u1')"
  unfolding step_trans.simps
  apply clarsimp
  apply (frule (2) guard_simulation)
  apply (drule (2) sim_reset[rotated -1])
  apply (frule (1) inv_simulation)
  apply auto
  done

sublocale Time_Abstract_Simulation A sim
  apply standard
  subgoal
    unfolding step_trans'.simps using step_t_simulation step_trans_simulation
    by simp (metis sim_locD)
  subgoal
    unfolding sim_def by auto
  subgoal premises prems for u v w
  proof -
    define clks where "clks = clk_set A"
    from prems show ?thesis
      unfolding sim_def clks_def[symmetric] by fastforce+
  qed
  done

end



subsection ‹Simulation on Reachability Invariants›

locale Invariant_Simulation =
  fixes L :: "'l set" and M :: "'l ⇒ 's set"
    and SE E SE' E' sim :: "('l × 's) ⇒ ('l × 's) ⇒ bool"
  assumes SE_SE':
    "⋀l l' x y x'. sim (l, x) (l, x') ⟹ SE (l, x) (l', y)
    ⟹ ∃y'. SE' (l, x') (l', y') ∧ sim (l', y) (l', y')"
  assumes SE'_SE:
    "⋀l l' x y x' y'. sim (l, x) (l, x') ⟹ sim (l', y) (l', y') ⟹ SE' (l, x') (l', y')
    ⟹ SE (l, x) (l', y)"
  and E'_E:
    "⋀l l' a a' b'. sim (l, a) (l, a') ⟹ E' (l, a') (l', b')
    ⟹ (∃b. E (l, a) (l', b) ∧ sim (l', b) (l', b'))"
begin

definition
  "M' ≡ λl. {x'. ∃x ∈ M l. sim (l, x) (l, x')}"

lemma invariant_simulation:
  assumes
    "∀l ∈ L. ∀s ∈ M l. ∀l' s'. E (l, s) (l', s') ⟶ l' ∈ L ∧ (∃s'' ∈ M l'. SE (l', s') (l', s''))"
  shows
    "∀l ∈ L. ∀s ∈ M' l. ∀l' s'. E' (l, s) (l', s') ⟶ l' ∈ L ∧ (∃s'' ∈ M' l'. SE' (l', s') (l', s''))"
  apply safe
  subgoal
    using assms unfolding M'_def by (auto dest: E'_E)
  subgoal premises prems
  proof -
    have "∃s''. (∃x∈M l'. sim (l', x) (l', s'')) ∧ SE' (l', s') (l', s'')"
      if "l ∈ L" "E' (l, s) (l', s')" "x ∈ M l" "sim (l, x) (l, s)"
      for l :: 'l and s :: 's and l' :: 'l and s' :: 's and x :: 's
    proof -
      from that E'_E obtain x' where "sim (l', x') (l', s')" "E (l, x) (l', x')"
        by force
      with ‹l ∈ L› ‹x ∈ M l› assms obtain x'' where "x'' ∈ M l'" "SE (l', x') (l', x'')"
        by force
      from this(2) ‹sim (l', x') _› obtain s'' where
        "SE' (l', s') (l', s'')" "sim (l', x'') (l', s'')"
        by atomize_elim (rule SE_SE')
      with ‹x'' ∈ _› show "∃s''. (∃x∈M l'. sim (l', x) (l', s'')) ∧ SE' (l', s') (l', s'')"
        by auto
    qed
    with prems show ?thesis
      unfolding M'_def by auto
  qed
  done

interpretation Simulation where
  A = E' and
  B = E and
  sim = "λ(l, s) (l', s'). l' = l ∧ sim (l, s') (l', s)"
  by standard (auto dest: E'_E)

context
  fixes f :: "'l × 's ⇒ nat"
begin

definition
  "f' ≡ λ(l, s). Max ({f (l, s') | s'. sim (l, s') (l, s) ∧ s' ∈ M l})"

context
  assumes finite: "finite L" "∀ l ∈ L. finite (M l)"
  assumes f_topo: "⋀l s l1 s1 l2 s2.
    l ∈ L ⟹ s ∈ M l ⟹ l2 ∈ L ⟹ s2 ∈ M l2 ⟹ E (l, s) (l1, s1) ⟹ SE (l1, s1) (l2, s2) ⟹
    f (l, s) ≤ f (l2, s2)"
begin

lemma topo_simulation: "⋀l s l1 s1 l2 s2.
  l ∈ L ⟹ s ∈ M' l ⟹ l2 ∈ L ⟹ s2 ∈ M' l2 ⟹ E' (l, s) (l1, s1) ⟹ SE' (l1, s1) (l2, s2) ⟹
  f' (l, s) ≤ f' (l2, s2)"
  subgoal premises prems for l s l1 s1 l2 s2
  proof -
    have "f' (l, s) ≤ f' (l'', s'')"
      if "l ∈ L"
        and "l'' ∈ L"
        and "E' (l, s) (l', s')"
        and "SE' (l', s') (l'', s'')"
        and "x ∈ M l"
        and "sim (l, x) (l, s)"
        and "x'' ∈ M l''"
        and "sim (l'', x'') (l'', s'')"
      for l s l' s' l'' s'' x x''
    proof -
      let ?S = "λ l'' s''. {f (l'', s') |s'. sim (l'', s') (l'', s'') ∧ s' ∈ M l''}"
      have finiteI: "finite (?S l s)" if "l ∈ L" for l s
        using finite that using [[simproc add: finite_Collect]] by simp
      have "Max (?S l s) ∈ ?S l s"
        using ‹l ∈ L› ‹sim (l, x) _› ‹x ∈ _› by (intro Max_in) (auto intro: finiteI)
      then obtain y where "f' (l, s) = f (l, y)" "sim (l, y) (l, s)" "y ∈ M l"
        unfolding f'_def by auto
      with E'_E ‹E' (l,s) _› ‹sim (l, x) _› obtain x' where
        "E (l, y) (l', x')" "sim (l', x') (l', s')"
        by metis
      moreover from ‹SE' (l',s') _› ‹sim (l', x') _› ‹sim (l'', x'') _› have "SE (l', x') (l'', x'')"
        using SE'_SE by metis
      ultimately have "f (l, y) ≤ f (l'', x'')"
        using that f_topo[of l y l'' x'' l' x'] ‹y ∈ M l› by auto
      with ‹_ = f (l, y)› have "f' (l, s) ≤ f (l'', x'')"
        by simp
      also from ‹x'' ∈ _› ‹l'' ∈ _› ‹sim (l'', x'') _› have "… ≤ f' (l'', s'')"
        unfolding f'_def by (auto intro: finiteI Max_ge)
      finally show ?thesis .
    qed
    then show ?thesis
      using prems unfolding M'_def by auto
  qed
  done

end

end

end



subsection ‹Abstraction-Simulation on Reachability Invariants›

locale Abstraction_Simulation =
  fixes L :: "'l set" and M :: "'l ⇒ 's set"
    and SE E SE' :: "('l × 's) ⇒ ('l × 's) ⇒ bool"
    and α :: "'l ⇒ 's ⇒ 's"
  assumes SE_SE': "⋀l l' x y. SE (l, x) (l', α l' y) ⟹ SE' (l, α l x) (l', α l' y)"
  assumes SE'_SE: "⋀l l' x y. SE' (l, α l x) (l', α l' y) ⟹ SE (l, x) (l', α l' y)"
    and simulation:
      "⋀l l' a a' b.
        α l a = α l a' ⟹ E (l, a) (l', b) ⟹ (∃b'. E (l, a') (l', b') ∧ α l' b = α l' b')"
begin

definition
  "M' ≡ λl. α l ` M l"

inductive E' where
  "E (l, s) (l', s') ⟹ E' (l, α l s) (l', α l' s')"

sublocale sim: Invariant_Simulation where
  sim = "λ(l, x) (l', y). l' = l ∧ y = α l x" and
  SE = "λ(l, x) (l', y). SE (l, x) (l', α l' y)" and
  SE' = "λ(l, x) (l', y). SE' (l, x) (l', y)" and
  E = E and
  E' = E'
  apply standard
  subgoal for l l' x y x'
    apply clarsimp
    by (rule SE_SE')
  subgoal for l l' x y x' y'
    apply clarsimp
    by (rule SE'_SE)
  subgoal for l l' a a' b'
    using simulation by (auto elim!: E'.cases)
  done

interpretation sim2: Simulation where
  sim = "λ(l, x) (l', y). l' = l ∧ y = α l x" and
  A = E and
  B = E'
  by standard (force simp: E'.simps)

interpretation bisim: Bisimulation where
  sim = "λ(l, x) (l', y). l' = l ∧ y = α l x" and
  A = E and
  B = E'
  apply standard
  subgoal
    using sim2.A_B_step .
  subgoal for a a' b'
    by (cases b') (auto dest: sim.E'_E[rotated])
  done

lemma simulationE:
  assumes "α l a = α l a'" "E (l, a) (l', b)"
  obtains b' where "E (l, a') (l', b')" "α l' b = α l' b'"
  using assms simulation by blast

lemma M'_eq:
  "sim.M' = M'"
  unfolding sim.M'_def M'_def by auto


lemma invariant_simulation:
  assumes
    "∀l∈L. ∀s∈M l. ∀l' s'. E (l, s) (l', s') ⟶ l' ∈ L ∧ (∃s''∈M l'. SE (l', s') (l', α l' s''))"
  shows
    "∀l∈L. ∀s∈M' l. ∀l' s'. E' (l, s) (l', s') ⟶ l' ∈ L ∧ (∃s''∈M' l'. SE' (l', s') (l', s''))"
  using sim.invariant_simulation assms unfolding M'_eq by fast

lemma ― ‹Alternative proof of: @{thm invariant_simulation}›
  assumes
    "∀l∈L. ∀s∈M l. ∀l' s'. E (l, s) (l', s') ⟶ l' ∈ L ∧ (∃s''∈M l'. SE (l', s') (l', α l' s''))"
  shows
    "∀l∈L. ∀s∈M' l. ∀l' s'. E' (l, s) (l', s') ⟶ l' ∈ L ∧ (∃s''∈M' l'. SE' (l', s') (l', s''))"
proof -
  { fix x  l s l' s'
    assume "l ∈ L" "x ∈ M l" "(l, s) → (l', s')" "α l x = α l s"
    then have "l' ∈ L"
      using assms simulation by metis
  }
  moreover
  { fix l l' :: 'l and s s' x :: 's
    assume "l ∈ L" "E (l, s) (l', s')" "α l x = α l s" "x ∈ M l"
    with simulation obtain x' where "α l' s' = α l' x'" "E (l, x) (l', x')"
      by metis
    with ‹l ∈ L› ‹x ∈ M l› assms obtain x'' where "x'' ∈ M l'" "SE (l', x') (l', α l' x'')"
      by force
    from this(2) have "SE' (l', α l' x') (l', α l' x'')"
      by (rule SE_SE')
    with ‹x'' ∈ _› ‹α l' s' = _› have "∃s''∈M l'. SE' (l', α l' s') (l', α l' s'')"
      by auto
  }
  ultimately show ?thesis
    unfolding M'_def by - (safe; (erule E'.cases; clarsimp))
qed


context
  fixes f :: "'l × 's ⇒ nat"
  assumes finite: "finite L" "∀ l ∈ L. finite (M l)"
  assumes f_topo: "⋀l s l1 s1 l2 s2.
    l ∈ L ⟹ s ∈ M l ⟹ l2 ∈ L ⟹ s2 ∈ M l2 ⟹ E (l, s) (l1, s1) ⟹ SE (l1, s1) (l2, α l2 s2)
    ⟹ f (l, s) ≤ f (l2, s2)"
begin

definition
  "f' ≡ λ(l, s). Max ({f (l, s') | s'. α l s' = s ∧ s' ∈ M l})"

lemma f'_eq:
  "sim.f' f = f'"
  unfolding sim.f'_def f'_def by (rule ext; clarsimp; metis)

lemma topo_simulation: "⋀l s l1 s1 l2 s2.
  l ∈ L ⟹ s ∈ M' l ⟹ l2 ∈ L ⟹ s2 ∈ M' l2 ⟹ E' (l, s) (l1, s1) ⟹ SE' (l1, s1) (l2, s2) ⟹
  f' (l, s) ≤ f' (l2, s2)"
  by (rule sim.topo_simulation[where f = f, OF finite, unfolded M'_eq f'_eq])
     ((rule f_topo; simp; fail), simp+)

end

end


subsection ‹Instantiation for Abstractions based on Time-Abstraction Simulations›
context Time_Abstract_Simulation
begin

context
  fixes SE :: "('l × ('c, 't) zone) ⇒ ('l × ('c, 't) zone) ⇒ bool"
  assumes SE_subsumption: "⋀l l' Z Z'. SE (l, Z) (l', Z') ⟹ l' = l ∧ Z ⊆ α l' Z'"
      and SE_determ:
      "⋀l l' Z Z' W. SE (l, Z) (l', Z') ⟹ α l Z = α l W ⟹ SE (l, W) (l', Z')"
begin

lemma step_z'_step_trans_z'_iff:
  "A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z''⟩ ⟷ (∃t. A ⊢' ⟨l, Z⟩ ↝⇗t⇖ ⟨l', Z''⟩)"
  using step_trans_z'_step_z' step_z'_step_trans_z' by metis

interpretation Abstraction_Simulation where
  SE = "λ(l, Z) (l', Z'). ∃W. Z' = α l W ∧ SE (l, Z) (l', W)" and
  E = "λ(l, Z) (l', Z'). A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩" and
  SE' = "λ(l, Z) (l', Z'). ∃W W'. Z = α l W ∧ Z' = α l' W' ∧ SE (l, W) (l', W')" and
  α = abs
  apply (standard; clarsimp)
  subgoal
    using SE_subsumption by metis
  subgoal for l l' x y W W'
    using SE_subsumption SE_determ by metis
  subgoal
    unfolding step_z'_step_trans_z'_iff using simulation' by metis
  done

interpretation inv: Invariant_Simulation where
  SE = "λ(l, Z) (l', Z'). ∃W. l' = l ∧ α l Z' = α l W ∧ SE (l, Z) (l', W)" and
  E = "λ(l, Z) (l', Z'). A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩" and E' = E' and
  SE' = "λ(l, Z) (l', Z'). ∃W W'. l' = l ∧ Z = α l W ∧ Z' = α l' W' ∧ SE (l, W) (l', W')" and
  sim = "λ(l, Z) (l', Z'). l' = l ∧ Z' = α l Z"
  apply (standard; clarsimp simp: abs_involutive)
  subgoal for l Z' W
    by blast
  subgoal for l Z W Z' W'
    using SE_determ by auto
  subgoal for l l' Z Z'
    using sim.E'_E by auto
  done

end

end


subsection ‹``Sandwiches'' of Abstraction-Simulations›

locale Time_Abstract_Simulation_Sandwich =
  Regions_TA where A = A +
  Time_Abstract_Simulation where A = A for A :: "('a, 'c, real, 'l) ta" +
  assumes sim_V: "(l, u) ≼ (l', u') ⟹ u' ∈ V ⟹ u ∈ V"

  fixes I β
  assumes I_invariant: "I Z ⟹ A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩ ⟹ I Z'"
  assumes β_α:      "I Z ⟹ Z ⊆ V ⟹ l ∈ state_set A ⟹ β l Z ⊆ α l Z"
      and β_widens: "I Z ⟹ Z ⊆ V ⟹ l ∈ state_set A ⟹ Z ⊆ β l Z"
      and β_I:      "I Z ⟹ Z ⊆ V ⟹ l ∈ state_set A ⟹ I (β l Z)"
  and finite_abstraction: "finite {β l Z | l Z. I Z ∧ Z ⊆ V ∧ l ∈ state_set A}"

  fixes l0 :: 'l and Z0 :: "('c, real) zone"
  assumes l0_state_set: "l0 ∈ state_set A" and Z0_V: "Z0 ⊆ V" and Z0_I: "I Z0"
begin

inductive step_beta ::
  "('a, 'c, real, 'l) ta ⇒ 'l ⇒ ('c, real) zone ⇒ 'a ⇒ 'l ⇒ ('c, real) zone ⇒ bool"
("_ ⊢ ⟨_, _⟩ ↝⇘β(_)⇙ ⟨_, _⟩" [61,61,61] 61)
where
  step_beta:
    "A ⊢ ⟨l, Z⟩ ↝⇘τ⇙ ⟨l', Z'⟩ ⟹ A ⊢ ⟨l', Z'⟩ ↝⇘↿a⇙ ⟨l'', Z''⟩
  ⟹ A ⊢ ⟨l, Z⟩ ↝⇘β(a)⇙ ⟨l'', β l'' Z''⟩"

no_notation step_z_beta  ("_ ⊢ ⟨_, _⟩ ↝⇘β(_)⇙ ⟨_, _⟩" [61,61,61,61] 61)

no_notation step_z_alpha ("_ ⊢ ⟨_, _⟩ ↝⇘α(_)⇙ ⟨_, _⟩" [61,61,61] 61)

lemma step_beta_alt_def:
  "(∃a. A ⊢ ⟨l, Z⟩ ↝⇘β(a)⇙ ⟨l', W⟩) ⟷ (∃Z'. A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩ ∧ W = β l' Z')"
  unfolding step_beta.simps step_z'_def by auto

lemma step_betaE:
  assumes "A ⊢ ⟨l, Z⟩ ↝⇘β(a)⇙ ⟨l', W⟩"
  obtains Z' where "A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩" "W = β l' Z'"
  using step_beta_alt_def assms by metis

definition
  "loc_is l s ≡ ∀(l', _) ∈ s. l' = l"

lemma α_V:
  "α l Z ⊆ V" if "Z ⊆ V"
  using that sim_V unfolding V_def abs_def by auto

lemma β_V:
  "β l Z ⊆ V" if "Z ⊆ V" "I Z" "l ∈ state_set A"
  using β_α α_V that by blast

(* XXX Move *)
lemma step_z'_V:
  "Z' ⊆ V" if "A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩" "Z ⊆ V"
  by (meson step_z_V step_z'_def that)

text ‹Corresponds to lemma 6 of cite‹"Li:FORMATS:2009"›.›
lemma backward_simulation:
  assumes
    "b ∈ S'" "loc_is l S" "loc_is l' S'" "A ⊢ ⟨l, R_of S⟩ ↝⇘β(a)⇙ ⟨l', R_of S'⟩"
    "I (R_of S)" "R_of S ⊆ V"
  shows "∃a∈S. ∃b'. (case a of (l, u) ⇒ λ(l', u'). A ⊢' ⟨l, u⟩ → ⟨l', u'⟩) b' ∧ b ≼ b'"
proof -
  let ?Z = "R_of S" and ?Z' = "R_of S'"
  obtain u1 where "b = (l', u1)"
    using assms(1,3) unfolding loc_is_def by (cases b) auto
  then have "u1 ∈ ?Z'"
    using assms(1) by blast
  from assms(4) obtain Z' where "A ⊢ ⟨l, ?Z⟩ ↝ ⟨l', Z'⟩" "?Z' = β l' Z'"
    by (erule step_betaE)
  then have "β l' Z' ⊆ α l' Z'"
    using assms(5,6) by (intro β_α) (auto dest: I_invariant step_z'_V step_z_state_setI2)
  with ‹u1 ∈ ?Z'› ‹?Z' = _› obtain u1' where "u1' ∈ Z'" "(l', u1) ≼ (l', u1')"
    unfolding abs_def by auto
  with ‹A ⊢ ⟨l, ?Z⟩ ↝ ⟨l', Z'⟩› obtain u where "A ⊢' ⟨l, u⟩ → ⟨l', u1'⟩" "u ∈ ?Z"
    by (meson step_z_sound')
  with ‹_ ≼ _› show ?thesis
    using assms(2) unfolding R_of_def loc_is_def ‹b = _› by fastforce
qed

lemma step'_step_beta:
  assumes
    "(l, u) ∈ a'" "A ⊢' ⟨l, u⟩ → ⟨l', u'⟩" "loc_is l1 a'" "R_of a' ⊆ V" "I (R_of a')"
  shows
    "∃b'. (∃a l l'. loc_is l a' ∧ loc_is l' b' ∧ a' ≠ {} ∧ b' ≠ {} ∧
            A ⊢ ⟨l, R_of a'⟩ ↝⇘βa⇙ ⟨l', R_of b'⟩) ∧ (l', u') ∈ b'"
proof -
  let ?Z = "R_of a'"
  from ‹(l, u) ∈ _› ‹loc_is _ _› have [simp]: "l1 = l"
    unfolding loc_is_def by auto
  from assms(1) have "u ∈ ?Z"
    unfolding R_of_def by force
  with assms(2) obtain Z' where step: "A ⊢ ⟨l, ?Z⟩ ↝ ⟨l', Z'⟩" "u' ∈ Z'"
    by (metis step_z_complete')
  then obtain a where "A ⊢ ⟨l, R_of a'⟩ ↝⇘βa⇙ ⟨l', β l' Z'⟩"
    by atomize_elim (unfold step_beta_alt_def, fast)
  moreover from β_widens have "u' ∈ β l' Z'"
    using step ‹_ ⊆ V› ‹I ?Z› by (blast dest: step_z'_V I_invariant step_z_state_setI2)
  ultimately show ?thesis
    using ‹loc_is _ _› ‹(l, u) ∈ _›
    by (inst_existentials "from_R l' (β l' Z')" a l l')
       (auto simp: from_R_def loc_is_def R_of_def image_def)
qed

definition beta_step where
  "beta_step ≡ λs s'. ∃a l l'. loc_is l s ∧ loc_is l' s' ∧ s ≠ {} ∧ s' ≠ {} ∧
     A ⊢ ⟨l, R_of s⟩ ↝⇘β(a)⇙ ⟨l', R_of s'⟩"

lemma beta_step_inv:
  assumes "beta_step a b" "∃l∈state_set A. loc_is l a ∧ R_of a ⊆ V ∧ I (R_of a)"
  shows "∃l∈state_set A. loc_is l b ∧ R_of b ⊆ V ∧ I (R_of b)"
  using assms unfolding beta_step_def
  using β_V step_z'_V step_z_state_setI2 β_I I_invariant step_betaE by metis

lemma from_R_R_of:
  assumes "loc_is l S"
  shows "from_R l (R_of S) = S"
  using assms from_R_R_of unfolding loc_is_def by force

interpretation backward_simulation: Backward_Double_Simulation_Complete where
  E = "λ(l, u) (l', u'). A ⊢' ⟨l, u⟩ → ⟨l', u'⟩" and
  G = beta_step and
  sim' = "(≡M)" and
  P = valid and
  Q = "λs. ∃l ∈ state_set A. loc_is l s ∧ R_of s ⊆ V ∧ I (R_of s)" and
  a0 = "from_R l0 Z0"
proof (standard, goal_cases)
  case (1 a b a')
  then show ?case
    by (intro self_simulation.A_B_step TrueI)
next
  case (2 b B A)
  then show ?case
    unfolding beta_step_def by clarify (rule backward_simulation)
next
  case (3 a)
  then show ?case
    by (rule refl)
next
  case 4
  then show ?case
    by (rule self_simulation.trans)
next
  case 5
  then show ?case
    by (rule equiv)
next
  case 6
  then show ?case
    by (rule finite_quotient)
next
  case (7 a b a')
  then show ?case
    unfolding beta_step_def by clarify (rule step'_step_beta)
next
  case (8 a b)
  then show ?case
    by (rule region_self_simulation.PA_invariant.invariant)
next
  case (9 a b)
  then show ?case
    by (rule beta_step_inv[rotated])
next
  case 10
  let ?S = "{from_R l (β l Z) | l Z. l ∈ state_set A ∧ Z ⊆ V ∧ I Z}"
  have "{x. beta_step** (from_R l0 Z0) x} ⊆ ?S ∪ {from_R l0 Z0}"
    apply (rule subsetI)
    apply simp
    subgoal
    proof (induction "from_R l0 Z0" _ rule: rtranclp.induct)
      case rtrancl_refl
      then show ?case
        by simp
    next
      case (rtrancl_into_rtrancl b c)
      let ?Z = "R_of b" and ?Z' = "R_of c"
      from ‹beta_step b c› obtain a l l' where step:
        "loc_is l b" "loc_is l' c" "b ≠ {}" "c ≠ {}"
        "A ⊢ ⟨l, R_of b⟩ ↝⇘βa⇙ ⟨l', R_of c⟩"
        unfolding beta_step_def by blast
      with rtrancl_into_rtrancl(2) ‹loc_is l b› have "l ∈ state_set A" "?Z ⊆ V" "I ?Z"
        apply -
        subgoal
          by (metis step_betaE step_z_state_setI1)
        subgoal
          using Z0_V β_V by (metis R_of_from_R)
        subgoal
          using Z0_I β_I by (metis R_of_from_R)
        done
      with step(1,2,5) show ?case
        using from_R_R_of step_z_state_setI2 step_z'_V step_betaE I_invariant by metis
    qed
    done
  moreover have "finite (?S ∪ {from_R l0 Z0})"
  proof -
    let ?T = "(λ(l, Z). from_R l Z) ` (state_set A × {β l Z |l Z. I Z ∧ Z ⊆ V ∧ l ∈ state_set A})"
    have "?S ⊆ ?T"
      by auto
    also from finite_state_set finite_abstraction have "finite ?T"
      by auto
    finally show ?thesis
      by fast
  qed
  ultimately show ?case
    by (rule finite_subset)
next
  case (11 a)
  then show ?case
    unfolding loc_is_def by auto
next
  case 12
  then show ?case
    using l0_state_set Z0_V Z0_I by (auto simp: V_def loc_is_def from_R_def R_of_def image_def)
qed

end


subsection ‹Invariants on DBM-based Model Checking›

context Regions
begin

inductive step_z_dbm' ::
  "('a, 'c, 't, 's) ta ⇒ 's ⇒ 't :: {linordered_cancel_ab_monoid_add,uminus} DBM
    ⇒ 'a ⇒ 's ⇒ 't DBM ⇒ bool"
("_ ⊢'' ⟨_, _⟩ ↝⇘_⇙ ⟨_, _⟩" [61,61,61] 61) for A l D a l'' D''
where
  "A ⊢' ⟨l,D⟩ ↝⇘a⇙ ⟨l'',D''⟩" if "A ⊢ ⟨l,D⟩ ↝⇘v,n,τ⇙ ⟨l',D'⟩" "A ⊢ ⟨l',D'⟩ ↝⇘v,n,↿a⇙ ⟨l'',D''⟩"

lemmas step_z_dbm'_def = step_z_dbm'.simps

inductive step_impl' ::
  "('a, nat, 't :: linordered_ab_group_add, 's) ta ⇒ 's ⇒ 't DBM'
    ⇒ 'a ⇒ 's ⇒ 't DBM' ⇒ bool"
("_ ⊢I'' ⟨_, _⟩ ↝⇘_⇙ ⟨_, _⟩" [61,61,61] 61) for A l D a l'' D''
where
  "A ⊢I' ⟨l,D⟩ ↝⇘a⇙ ⟨l'',D''⟩" if "A ⊢I ⟨l, D⟩ ↝⇘n,τ⇙ ⟨l',D'⟩" "A ⊢I ⟨l',D'⟩ ↝⇘n,↿a⇙ ⟨l'',D''⟩"

lemmas step_impl'_def = step_impl'.simps

end


definition
  "dbm_nonneg n M ≡ ∀i ≤ n. i > 0 ⟶ M 0 i ≤ 0"

named_theorems dbm_nonneg

lemma dbm_nonneg_And[dbm_nonneg]:
  assumes "dbm_nonneg n M" "dbm_nonneg n M'"
  shows "dbm_nonneg n (And M M')"
  using assms by (auto simp: dbm_nonneg_def min_def)

lemma dbm_nonneg_abstra[dbm_nonneg]:
  assumes "dbm_nonneg n M"
  shows "dbm_nonneg n (abstra ac M v)"
  using assms by (cases ac) (auto simp: dbm_nonneg_def min_def)

lemma dbm_nonneg_abstr[dbm_nonneg]:
  assumes "dbm_nonneg n M"
  shows "dbm_nonneg n (abstr g M v)"
  using assms(1) unfolding abstr.simps
  by (rule fold_acc_preserv'[where P = "dbm_nonneg n", rotated]) (rule dbm_nonneg_abstra)

lemma dbm_nonneg_up[dbm_nonneg]:
  "dbm_nonneg n (up M)" if "dbm_nonneg n M"
  using that unfolding dbm_nonneg_def up_def by auto

lemma dbm_nonneg_reset[dbm_nonneg]:
  fixes M :: "'t :: time DBM"
  assumes "dbm_nonneg n M" "x > 0"
  shows "dbm_nonneg n (reset M n x 0)"
  using assms unfolding reset_def dbm_nonneg_def by (auto simp: neutral min_def)

lemma dbm_nonneg_reset'[dbm_nonneg]:
  fixes M :: "'t :: time DBM"
  assumes "dbm_nonneg n M" "∀c ∈ set r. v c > 0"
  shows "dbm_nonneg n (reset' M n r v 0)"
  using assms by (induction r) (auto intro: dbm_nonneg_reset)

lemma dbm_nonneg_fw_upd[dbm_nonneg]:
  "dbm_nonneg n (fw_upd M k' i j)" if "dbm_nonneg n M"
  using that unfolding dbm_nonneg_def fw_upd_def upd_def min_def by auto

lemma dbm_nonneg_fwi[dbm_nonneg]:
  "dbm_nonneg n (fwi M n k' i j)" if "dbm_nonneg n M"
  using that by (induction M _ _ _ _ rule: fwi.induct) (auto intro!: dbm_nonneg_fw_upd)

lemma dbm_nonneg_fw[dbm_nonneg]:
  "dbm_nonneg n (fw M n k)" if "dbm_nonneg n M"
  using that by (induction k) (auto intro!: dbm_nonneg_fwi)

lemma dbm_nonneg_FW[dbm_nonneg]:
  "dbm_nonneg n (FW M n)" if "dbm_nonneg n M"
  using that by (rule dbm_nonneg_fw)

definition
  "empty_dbm ≡ λ_ _. Lt 0"

lemma neg_diag_zero_empty_dbmI:
  assumes "M 0 0 < 0"
  shows "[M]⇘v,n⇙ = {}"
  using assms
  unfolding DBM_zone_repr_def DBM_val_bounded_def DBM.neutral DBM.less_eq[symmetric] by auto

lemma empty_dbm_empty_zone:
  "[empty_dbm]⇘v,n⇙ = {}"
  unfolding empty_dbm_def by (rule neg_diag_zero_empty_dbmI) (simp add: DBM.neutral)

lemma canonical_empty_dbm:
  "canonical empty_dbm n"
  unfolding empty_dbm_def by (auto simp: DBM.add)

lemma dbm_int_empty_dbm:
  "dbm_int empty_dbm n"
  unfolding empty_dbm_def by auto

lemma dbm_nonneg_empty_dbm:
  "dbm_nonneg n empty_dbm"
  unfolding dbm_nonneg_def empty_dbm_def DBM.neutral by simp

lemmas [simp] = any_le_inf

lemma DBM_val_boundedD1:
  assumes "u ⊢⇘v,n⇙ M" "v c ≤ n"
  shows "Le (- u c) ≤ M 0 (v c)"
  using assms unfolding dbm_entry_val.simps DBM_val_bounded_def by auto

lemma DBM_val_boundedD2:
  assumes "u ⊢⇘v,n⇙ M" "v c ≤ n"
  shows "Le (u c) ≤ M (v c) 0"
  using assms unfolding dbm_entry_val.simps DBM_val_bounded_def by auto

lemma DBM_val_boundedD3:
  assumes "u ⊢⇘v,n⇙ M" "v c1 ≤ n" "v c2 ≤ n"
  shows "Le (u c1 - u c2) ≤ M (v c1) (v c2)"
  using assms unfolding dbm_entry_val.simps DBM_val_bounded_def by force

lemma dbm_default_And:
  assumes "dbm_default M n" "dbm_default M' n"
  shows "dbm_default (And M M') n"
  using assms by auto

lemma dbm_default_abstra:
  assumes "dbm_default M n" "constraint_pair ac = (x, m)" "v x ≤ n"
  shows "dbm_default (abstra ac M v) n"
  using assms by (cases ac) auto

lemma dbm_default_abstr:
  assumes "dbm_default M n" "∀(x, m)∈collect_clock_pairs g. v x ≤ n"
  shows "dbm_default (abstr g M v) n"
  using assms(1) unfolding abstr.simps
proof (rule fold_acc_preserv'[where P = "λM. dbm_default M n", rotated], goal_cases)
  case (1 ac acc)
  then obtain x m where "constraint_pair ac = (x, m)"
    by force
  with assms(2) 1 show ?case
    by (intro dbm_default_abstra) (auto simp: collect_clock_pairs_def)
qed

lemma dbm_entry_dense:
  fixes a b :: "'t :: time DBMEntry"
  assumes "a + b ≥ 0" "b > 0"
  obtains x where "x > 0" "b ≥ Le x" "Le (-x) ≤ a"
proof -
  consider "a = ∞" | "a ≠ ∞" "a + b = 0" | "a ≠ ∞" "a + b > 0"
    using assms(1) by force
  then show ?thesis
  proof cases
    case 1
    with assms show ?thesis
    proof (cases b)
      case (Le x)
      with assms(2) 1 show ?thesis
        by (intro that[of x]) (auto simp: DBM.neutral DBM.add)
    next
      case (Lt x2)
      with assms(2) 1 show ?thesis
        using that time_class.dense by (auto simp: DBM.neutral DBM.add)
    next
      case INF
      with 1 assms(2) that show ?thesis
        by (metis add_inf(2) any_le_inf dbm_less_eq_simps(2) neg_less_iff_less sum_gt_neutral_dest)
    qed
  next
    case 2
    then obtain x where "a = Le (-x)" "b = Le x"
      unfolding neutral by (cases a; cases b; simp add: DBM.add eq_neg_iff_add_eq_0)
    with ‹b > 0› show ?thesis
      by (intro that[of x]; simp add: neutral)
  next
    case 3
    note intro = that
    have 1: "0 < x + y ⟹ - y ≤ x" for x y :: 't
      by (metis ab_semigroup_add_class.add.commute add.right_inverse add_le_cancel_left less_imp_le)
    have 2: thesis if "0 < x + y" "0 < y" "a = Le x" "b = Lt y" for x y :: 't
    proof (cases "x > 0")
      case True
      then have "- x ≤ 0"
        by auto
      from ‹y > 0› dense obtain z where "0 < z" "z < y"
        by auto
      with that ‹- x ≤ 0› show ?thesis
        using dual_order.trans by (intro intro[of z]; fastforce)
    next
      case False
      from that have "-x < y"
        using 1 minus_less_iff by fastforce
      with dense obtain z where "- x < z" "z < y"
        by auto
      with False that show ?thesis
        by (intro intro[of z]; simp add: less_imp_le minus_less_iff)
          (meson leI less_le_trans neg_less_0_iff_less)
    qed
    include no_library_syntax
    have 3: thesis if "a = Le x" "b = ∞" for x :: 't
      by (smt 3(2) Le_le_LtI Lt_le_LeI add.inverse_inverse any_le_inf intro neg_0_less_iff_less
          non_trivial_neg not_less order_trans sum_gt_neutral_dest that(2))
    have 4: thesis if "a = Lt x" "b = ∞" for x :: 't
      by (metis that ‹0 < a + b› add.inverse_inverse dbm_less_eq_simps(2) dbm_less_simps(2) intro leI
          less_imp_le less_le_trans neg_0_less_iff_less sum_gt_neutral_dest)
    have 5: thesis if "0 < x + y" "0 < y" "a = Lt x" "b = Le y" for x y
      by (metis that Le_le_LtI antisym_conv1 diff_0_right diff_less_eq intro less_irrefl minus_diff_eq)
    have 6: thesis if "0 < y" "a = Lt x" "b = Lt y" for x y
      using that ‹a + b > 0›
      apply -
      apply (drule sum_gt_neutral_dest)
      apply safe
      subgoal for d
        by (cases "d ≥ 0", cases "d = 0")
           (smt intro Le_le_LtI Lt_le_LeI
             add.inverse_inverse not_less neg_less_0_iff_less dense order_trans)+
      done
    have 7: thesis if "0 < x + y" "0 < y" "a = Le x" "b = Le y" for x y
      using that by (intro intro[of y]) (auto simp: DBM.add intro: 1)
    from ‹a + b > 0› ‹b > 0› ‹a ≠ ∞› show thesis
      by (cases a; cases b) (auto simp: DBM.add neutral intro: 2 3 4 5 6 7)
  qed
qed

lemma canonical_diag:
  fixes M :: "'t :: time DBM"
  assumes "canonical M n" "i ≤ n"
  shows "M i i ≥ Lt 0"
proof (rule ccontr)
  assume "¬ M i i ≥ Lt 0"
  then have "M i i < Lt 0"
    by auto
  then have "M i i + M i i < M i i"
    by (cases "M i i") (auto simp: DBM.add)
  with assms show False
    by force
qed

lemma canonical_diag_nonnegI:
  fixes M :: "'t :: time DBM"
  assumes "canonical M n" "∀i ≤ n. M i i ≠ Lt 0"
  shows "∀i ≤ n. M i i ≥ 0"
proof clarify
  fix i assume "i ≤ n"
  then show "M i i ≥ 0"
    using canonical_diag[OF assms(1) ‹i ≤ n›] assms(2) by (cases "M i i"; auto simp: DBM.neutral)
qed

context Regions_common
begin

lemma canonical_non_emptyI:
  assumes "[M]⇘v,n⇙ ≠ {}"
  shows "canonical (FW M n) n"
  by (simp add: assms fw_shortest non_empty_cyc_free)

definition
  "canonical_dbm M ≡ canonical M n ∧ dbm_nonneg n M ∧ dbm_int M n"

abbreviation
  "vabstr' (Z :: ('c, t) zone) M ≡ Z = [M]⇘v,n⇙ ∧ canonical_dbm M"

lemma V_structuralI:
  assumes "dbm_nonneg n M"
  shows "[M]⇘v,n⇙ ⊆ V"
  using clock_numbering(3) assms unfolding V_def DBM_zone_repr_def
  by (clarsimp simp: neutral) (meson assms clock_numbering(1) dbm_positive dbm_nonneg_def)

lemma canonical_dbm_valid:
  "valid_dbm M" if "canonical_dbm M"
  using that unfolding canonical_dbm_def by (auto dest: V_structuralI)

lemma dbm_nonnegI:
  assumes "canonical M n" "[M]⇘v,n⇙ ⊆ V" "∀i ≤ n. M i i ≠ Lt 0"
  shows "dbm_nonneg n M"
proof (rule ccontr)
  assume A: "¬ dbm_nonneg n M"
  from assms(1,3) have diag_nonneg: "∀i ≤ n. M i i ≥ 0"
    by (rule canonical_diag_nonnegI)
  from A obtain i where "i > 0" "i ≤ n" "M 0 i > 0"
    unfolding dbm_nonneg_def by auto
  moreover have "M i 0 + M 0 i ≥ 0"
  proof -
    from assms(1) ‹i ≤ n› have "M i i ≥ Lt 0"
      by (rule canonical_diag)
    with ‹i ≤ n› assms(3) have "M i i ≥ 0"
      by (cases "M i i"; auto simp: neutral)
    also from ‹canonical M n› ‹i ≤ n› have "M i 0 + M 0 i ≥ M i i"
      by auto
    finally show ?thesis .
  qed
  ultimately obtain x where "x > 0" "M 0 i ≥ Le x" "Le (-x) ≤ M i 0"
    by - (rule dbm_entry_dense)
  moreover from ‹i > 0› ‹i ≤ n› obtain c where "c ∈ X" "v c ≤ n" "i = v c"
    using clock_numbering by auto
  moreover from clock_numbering(1) cn_weak assms(1) have "cycle_free M n"
    by (intro non_empty_cycle_free canonical_nonneg_diag_non_empty diag_nonneg) auto
  ultimately obtain u where "u ∈ [M]⇘v,n⇙" "u c < 0"
    using assms(1)
    by (auto simp: clock_numbering(1) intro: canonical_saturated_1[where M = M and v = v])
  with assms(2) ‹c ∈ X› show False
    unfolding V_def DBM_zone_repr_def by force
qed

lemma vabstr'_V:
  obtains M where "vabstr' V M"
proof -
  interpret beta_regions: Beta_Regions'
  where k = "k l"
    apply -
    apply unfold_locales
         apply (rule finite)
        apply (simp add: non_empty)
     apply (rule clock_numbering cn_weak not_in_X)+
  done
  have V_eq: "beta_regions.V = V"
    unfolding beta_regions.V_def V_def ..
  let ?M = "beta_regions.V_dbm"
  from beta_regions.V_dbm_eq_V beta_regions.V_dbm_int beta_regions.normalized_V_dbm have *:
    "[?M]⇘v,n⇙ = V" "dbm_int ?M n" "beta_regions.normalized ?M"
    unfolding V_eq by auto
  moreover have "dbm_nonneg n ?M"
    unfolding beta_regions.V_dbm_def dbm_nonneg_def DBM.neutral by simp
  ultimately show ?thesis
    apply -
    apply (rule that[of "FW ?M n"])
    apply (rule conjI)
    subgoal
      using FW_zone_equiv_spec by blast
    unfolding canonical_dbm_def
    apply (intro conjI dbm_nonneg_FW FW_int_preservation canonical_non_emptyI)
      apply (auto simp: V_def)
    done
qed

lemma canonical_dbm_empty_dbm:
  "canonical_dbm empty_dbm"
  unfolding canonical_dbm_def
  by (intro conjI canonical_empty_dbm dbm_int_empty_dbm dbm_nonneg_empty_dbm)

lemma vabstr'_empty_dbm:
  "vabstr' {} empty_dbm"
  by (intro conjI empty_dbm_empty_zone[symmetric] canonical_dbm_empty_dbm)

lemma vabstr'I:
  assumes "dbm_int M' n" "Z' ⊆ V" "Z' = [M']⇘v,n⇙"
  obtains M' where "vabstr' Z' M'"
proof (cases "Z' = {}")
  case True
  then show ?thesis
    by (intro that[of empty_dbm], simp only: vabstr'_empty_dbm)
next
  case False
  with assms obtain M' where *: "Z' = [M']⇘v,n⇙" "dbm_int M' n" "canonical M' n"
    by (metis FW_canonical' FW_valid_preservation FW_zone_equiv_spec
        dbm_non_empty_diag valid_dbm.simps)
  with assms(2) have "dbm_nonneg n M'"
    by - (rule dbm_nonnegI; smt ‹Z' ≠ {}› dbm_less_eq_simps(2) dbm_non_empty_diag neutral)
  let ?M = "FW M' n"
  from * ‹dbm_nonneg n M'› show ?thesis
    apply (intro that[of ?M] conjI)
     apply (simp add: FW_zone_equiv_spec[symmetric])
    unfolding canonical_dbm_def
    unfolding dbm_nonneg_def[symmetric]
    apply (intro conjI FW_canonical' dbm_nonneg_FW FW_int_preservation; assumption?)
    subgoal diag_nonneg
      using FW_zone_equiv_spec False dbm_non_empty_diag by blast
    done
qed

end

context Regions_TA
begin

text ‹The following does not hold:›
lemma
  fixes M :: "real DBM"
  assumes "canonical M n"
      and "∀i ≤ n. M 0 i ≤ 0"
    shows "∀i ≤ n. 0 ≤ M i i"
  oops

lemma global_clock_numbering:
  "global_clock_numbering A v n"
  using clock_numbering(1) clock_numbering_le cn_weak valid_abstraction by blast

sublocale step_z'_bisim_step_z_dbm': Bisimulation
  "λ(l, Z) (l', Z'). A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩"
  "λ(l, M) (l', M'). ∃a. A ⊢' ⟨l,M⟩ ↝⇘a⇙ ⟨l',M'⟩"
  "λ(l, Z) (l', M). l' = l ∧ Z = [M]⇘v,n⇙"
  apply (standard; clarsimp simp: step_z_dbm'_def step_z'_def)
  subgoal
    using global_clock_numbering by (auto elim!: step_z_dbm_DBM)
  subgoal
    by (blast dest: step_z_dbm_sound[OF _ global_clock_numbering])
  done

lemma step_z_dbm_preserves_int:
  "dbm_int M' n" if "A ⊢ ⟨l,M⟩ ↝⇘v,n,a⇙ ⟨l',M'⟩" "dbm_int M n"
  apply (rule step_z_dbm_preserves_int; (rule that global_clock_numbering)?)
  using valid_abstraction valid_abstraction_pairsD by fastforce

lemma step_z_dbm'_preserves_int:
  "dbm_int M' n" if "A ⊢' ⟨l,M⟩ ↝⇘a⇙ ⟨l',M'⟩" "dbm_int M n"
  using that by cases (erule step_z_dbm_preserves_int)+

lemma step_z'_vabstr':
  "∃M. vabstr' Z' M" if "∃M. vabstr' Z M" "A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩"
proof -
  from that obtain M where "vabstr' Z M"
    by auto
  with step_z'_bisim_step_z_dbm'.A_B_step[of "(l, Z)" _ "(l, M)"] that(2) obtain a M' where *:
    "A ⊢' ⟨l, M⟩ ↝⇘a⇙ ⟨l', M'⟩" "Z' = [M']⇘v,n⇙"
    by force
  with ‹vabstr' Z M› have "dbm_int M' n"
    by - (rule step_z_dbm'_preserves_int, auto simp: canonical_dbm_def)
  moreover from *(1) ‹vabstr' Z M› have "Z' ⊆ V"
    by (metis canonical_dbm_valid step_z'_def step_z_V that(2) valid_dbm.simps)
  ultimately obtain M' where "vabstr' Z' M'"
    using ‹Z' = _› by - (rule vabstr'I)
  then show ?thesis
    by (intro exI)
qed

end


subsection ‹Instantiating the ``Sandwich'' for Extrapolations on DBMs›

locale TA_Extrapolation =
  Regions_TA where A = A +
  Time_Abstract_Simulation where A = A for A :: "('a, 'c, real, 'l) ta" +
  assumes simulation_nonneg: "u' ∈ V ⟹ (l, u) ≼ (l', u') ⟹ u ∈ V"
  fixes extra :: "'l ⇒ real DBM ⇒ real DBM" and l0 and M0
  assumes extra_widens: "vabstr' Z M ⟹ Z ⊆ [extra l M]⇘v,n⇙"
      and extra_α: "vabstr' Z M ⟹ [extra l M]⇘v,n⇙ ⊆ α l Z"
      and extra_finite: "finite {extra l M | M. canonical_dbm M}"
      and extra_int: "dbm_int M n ⟹ dbm_int (extra l M) n"
  assumes l0_state_set: "l0 ∈ state_set A" and M0_V: "[M0]⇘v,n⇙ ⊆ V" and M0_int: "dbm_int M0 n"
begin

definition apx where
  "apx l Z ≡ let M = (SOME M. canonical_dbm M ∧ Z = [M]⇘v,n⇙) in [extra l M]⇘v,n⇙"

lemma apx_widens:
  "[M]⇘v,n⇙ ⊆ apx l ([M]⇘v,n⇙)" if "canonical_dbm M"
  by (smt apx_def extra_widens someI_ex that)

lemma apx_abs:
  "apx l ([M]⇘v,n⇙) ⊆ α l ([M]⇘v,n⇙)" if "canonical_dbm M"
  by (smt apx_def extra_α someI_ex that)

lemma α_V:
  "α l Z ⊆ V" if "Z ⊆ V"
  using that simulation_nonneg unfolding V_def abs_def by auto

lemma apx_V:
  "apx l ([M]⇘v,n⇙) ⊆ V" if "canonical_dbm M"
proof -
  from that have "apx l ([M]⇘v,n⇙) ⊆ α l ([M]⇘v,n⇙)"
    by (rule apx_abs)
  moreover from that have "… ⊆ V"
    unfolding canonical_dbm_def by (intro α_V V_structuralI, elim conjE)
  finally show ?thesis .
qed

lemma apx_empty:
  "apx l {} = {}"
proof -
  have "vabstr' {} empty_dbm"
    by (rule vabstr'_empty_dbm)
  from canonical_dbm_empty_dbm have "apx l {} ⊆ α l {}"
    by (subst empty_dbm_empty_zone[symmetric])+ (rule apx_abs)
  also have "… = {}"
    unfolding abs_def by auto
  finally show ?thesis
    by simp
qed

lemma apx_ex:
  assumes "canonical_dbm M"
  shows "∃M'. apx l ([M]⇘v,n⇙) = [extra l M']⇘v,n⇙ ∧ canonical_dbm M'"
  using assms unfolding apx_def by (smt someI_ex)

lemma vabstr'_apx:
  assumes "vabstr' Z M" "Z ⊆ V"
  obtains M where "vabstr' (apx l Z) M"
proof (cases "Z = {}")
  case False
  from apx_ex assms obtain M' where *:
    "apx l Z = [extra l M']⇘v,n⇙" "canonical_dbm M'"
    using apx_ex by blast
  with FW_zone_equiv_spec have "apx l Z = [FW (extra l M') n]⇘v,n⇙"
    by auto
  moreover from ‹canonical_dbm M'› have "canonical_dbm (FW (extra l M') n)"
  proof -
    from assms have "Z ⊆ apx l Z"
      by (auto intro!: apx_widens)
    with ‹Z ≠ {}› have "apx l Z ≠ {}"
      by auto
    then have "canonical (FW (extra l M') n) n"
      unfolding * by (rule canonical_non_emptyI)
    moreover have "dbm_nonneg n (FW (extra l M') n)"
      using ‹apx l Z = [FW (extra l M') n]⇘v,n⇙› ‹apx l Z ≠ {}› ‹canonical (FW _ _) _›
      apply (intro dbm_nonnegI)
      apply assumption
      subgoal
        using apx_V assms(1) by blast
      subgoal
        by (metis DBMEntry.distinct(1) Le_less_Lt  antisym_conv dbm_non_empty_diag leI neutral)
      done
    moreover have "dbm_int (FW (extra l M') n) n"
      using *(2) unfolding canonical_dbm_def by (intro FW_int_preservation extra_int, elim conjE)
    ultimately show ?thesis
      unfolding canonical_dbm_def by (intro conjI)
  qed
  ultimately show ?thesis
    by (auto intro: that)
next
  case True
  then show ?thesis
    by (intro that[of empty_dbm])(auto simp: empty_dbm_empty_zone apx_empty canonical_dbm_empty_dbm)
qed

lemma apx_finite:
  "finite {apx l Z |l Z. ∃M. vabstr' Z M ∧ l ∈ state_set A}" (is "finite ?S")
proof -
  { fix l assume "l ∈ state_set A"
    from extra_finite have "finite {[extra l M]⇘v,n⇙ | M. canonical_dbm M}"
    proof -
      have "{[extra l M]⇘v,n⇙ | M. canonical_dbm M}
        = (λM. [M]⇘v,n⇙) ` {extra l M | M. canonical_dbm M}"
        by auto
      with extra_finite show ?thesis
        by simp
    qed
    also from apx_ex have "{apx l Z |Z. ∃M. vabstr' Z M} ⊆ …"
      by auto
    finally (finite_subset[rotated]) have "finite {apx l Z |Z. ∃M. vabstr' Z M}" .
  } note * = this
  have "?S = (⋃ l ∈ state_set A. {apx l Z |Z. ∃M. vabstr' Z M})"
    by auto
  also have "finite …"
    using * finite_state_set by auto
  finally show ?thesis .
qed

sublocale Time_Abstract_Simulation_Sandwich
  where β = apx and I = "λZ. ∃M. vabstr' Z M" and Z0 = "[M0]⇘v,n⇙"
proof standard
  show "u ∈ V" if "(l, u) ≼ (l', u')" "u' ∈ V" for l l' :: 'l and u u' :: "'c ⇒ real"
    using that by (rule simulation_nonneg[rotated])
  show "∃M. vabstr' Z' M"
    if "∃M. vabstr' Z M" and "A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩" for Z Z' :: "('c ⇒ real) set" and l l' :: 'l
    using that by (rule step_z'_vabstr')
  show "apx l Z ⊆ α l Z"
    if "∃M. vabstr' Z M" "Z ⊆ V" for Z :: "('c ⇒ real) set" and l :: 'l
    using that apx_abs by auto
  show "Z ⊆ apx l Z" if "∃M. vabstr' Z M" "Z ⊆ V" for Z :: "('c ⇒ real) set" and l :: 'l
    using that apx_widens by auto
  show "∃M. vabstr' (apx l Z) M"
    if "∃M. vabstr' Z M" "Z ⊆ V" for Z :: "('c ⇒ real) set" and l :: 'l
    using that by (elim exE) (rule vabstr'_apx, auto)
  show "finite {apx l Z |l Z. (∃M. vabstr' Z M) ∧ Z ⊆ V ∧ l ∈ state_set A}"
    using apx_finite by (rule finite_subset[rotated]) auto
  show "l0 ∈ state_set A"
    by (rule l0_state_set)
  show "[M0]⇘v,n⇙ ⊆ V"
    by (rule M0_V)
  show "∃M. vabstr' ([M0]⇘v,n⇙) M"
    by (rule vabstr'I; (rule M0_int M0_V)?) auto
qed

end

end