subsection ‹Semantics Based on DBMs› theory DBM_Zone_Semantics imports DBM_Operations begin subsection ‹Single Step› inductive step_z_dbm :: "('a, 'c, 't, 's) ta ⇒ 's ⇒ ('t::time) DBM ⇒ ('c ⇒ nat) ⇒ nat ⇒ 's ⇒ ('t::time) DBM ⇒ bool" ("_ ⊢ ⟨_, _⟩ ↝⇘_,_⇙ ⟨_, _⟩" [61,61,61] 61) where step_t_z_dbm: "D_inv = abstr (inv_of A l) (λi j. ∞) v ⟹ A ⊢ ⟨l,D⟩ ↝⇘v,n⇙ ⟨l,And (up (And D D_inv)) D_inv⟩" | step_a_z_dbm: "A ⊢ l ⟶⇗g,a,r⇖ l' ⟹ A ⊢ ⟨l,D⟩ ↝⇘v,n⇙ ⟨l',And (reset' (And D (abstr g (λi j. ∞) v)) n r v 0) (abstr (inv_of A l') (λi j. ∞) v)⟩" inductive_cases step_z_cases: "A ⊢ ⟨l, D⟩ ↝⇘v,n⇙ ⟨l', D'⟩" declare step_z_dbm.intros[intro] lemma step_z_dbm_preserves_int: assumes "A ⊢ ⟨l,D⟩ ↝⇘v,n⇙ ⟨l',D'⟩" "global_clock_numbering A v n" "valid_abstraction A X k" "dbm_int D n" shows "dbm_int D' n" using assms proof (cases, goal_cases) case (1 D'') hence "clock_numbering' v n" "∀c∈clk_set A. v c ≤ n" by blast+ from 1(2) have "∀ (x, m) ∈ clkp_set A. m ∈ ℕ" by (auto elim: valid_abstraction.cases) from dbm_int_inv_abstr[OF this] 1 have D''_int: "dbm_int D'' n" by simp show ?thesis unfolding 1(5) by (intro And_int_preservation up_int_preservation dbm_int_inv_abstr D''_int 1) next case (2 g a r) hence assms: "clock_numbering' v n" "∀c∈clk_set A. v c ≤ n" "∀k≤n. k > 0 ⟶ (∃c. v c = k)" by blast+ from 2(2) have *: "∀ (x, m) ∈ clkp_set A. m ∈ ℕ" by (auto elim: valid_abstraction.cases) from dbm_int_inv_abstr[OF this] have D'_int: "dbm_int (abstr (inv_of A l') (λi j. ∞) v) n" by simp from dbm_int_guard_abstr 2 have D''_int: "dbm_int (abstr g (λi j. ∞) v) n" by simp have "set r ⊆ clk_set A" using 2(5) unfolding trans_of_def collect_clkvt_def by fastforce hence **:"∀c∈set r. v c ≤ n" using assms(2) by fastforce show ?thesis unfolding 2(4) by (intro And_int_preservation DBM_reset'_int_preservation dbm_int_inv_abstr 2 D''_int) (simp_all add: assms(1) * **) qed lemma And_correct: shows "[M1]⇘v,n⇙ ∩ [M2]⇘v,n⇙ = [And M1 M2]⇘v,n⇙" using DBM_and_sound1 DBM_and_sound2 DBM_and_complete unfolding DBM_zone_repr_def by auto lemma up_correct: assumes "clock_numbering' v n" shows "[up M]⇘v,n⇙ = [M]⇘v,n⇙⇧^{↑}" using assms apply safe apply (rule DBM_up_sound') apply assumption+ apply (rule DBM_up_complete') apply auto done lemma step_z_dbm_sound: assumes "A ⊢ ⟨l, D⟩ ↝⇘v,n⇙ ⟨l', D'⟩" "global_clock_numbering A v n" shows "A ⊢ ⟨l, [D]⇘v,n⇙⟩ ↝ ⟨l', [D']⇘v,n⇙⟩" using assms proof (cases, goal_cases) case (1 D'') hence "clock_numbering' v n" "∀c∈clk_set A. v c ≤ n" by blast+ note assms = assms(1) this from assms(3) have *: "∀c∈collect_clks (inv_of A l). v c ≤ n" unfolding clkp_set_def collect_clki_def inv_of_def by (fastforce simp: collect_clks_id) from 1 have D'':"[D'']⇘v,n⇙ = {u. u ⊢ inv_of A l}" using dbm_abstr_zone_eq[OF assms(2) *] by metis with And_correct have A11: "[And D D'']⇘v,n⇙ = ([D]⇘v,n⇙) ∩ ({u. u ⊢ inv_of A l})" by blast with And_correct D'' have "[D']⇘v,n⇙ = ([up (And D D'')]⇘v,n⇙) ∩ ({u. u ⊢ inv_of A l})" unfolding 1(3) by blast with up_correct[OF assms(2)] A11 have "[D']⇘v,n⇙ = (([D]⇘v,n⇙) ∩ {u. u ⊢ inv_of A l})⇧^{↑}∩ {u. u ⊢ inv_of A l}" by metis with 1(2) show ?thesis by auto next case (2 g a r) hence "clock_numbering' v n" "∀c∈clk_set A. v c ≤ n" "∀k≤n. k > 0 ⟶ (∃c. v c = k)" by blast+ note assms = assms(1) this from assms(3) have *: "∀c∈collect_clks (inv_of A l'). v c ≤ n" unfolding clkp_set_def collect_clki_def inv_of_def by (fastforce simp: collect_clks_id) have D': "[abstr (inv_of A l') (λi j. ∞) v]⇘v,n⇙ = {u. u ⊢ inv_of A l'}" using 2 dbm_abstr_zone_eq[OF assms(2) *] by simp from assms(3) 2(3) have *: "∀c∈collect_clks g. v c ≤ n" unfolding clkp_set_def collect_clkt_def inv_of_def by (fastforce simp: collect_clks_id) have D'':"[abstr g (λi j. ∞) v]⇘v,n⇙ = {u. u ⊢ g}" using 2 dbm_abstr_zone_eq[OF assms(2) *] by auto with And_correct have A11: "[And D (abstr g (λi j. ∞) v)]⇘v,n⇙ = ([D]⇘v,n⇙) ∩ ({u. u ⊢ g})" by blast let ?D = "reset' (And D (abstr g (λi j. ∞) v)) n r v 0" have "set r ⊆ clk_set A" using 2(3) unfolding trans_of_def collect_clkvt_def by fastforce hence **:"∀c∈set r. v c ≤ n" using assms(3) by fastforce have D_reset: "[?D]⇘v,n⇙ = zone_set (([D]⇘v,n⇙) ∩ {u. u ⊢ g}) r" proof safe fix u assume u: "u ∈ [?D]⇘v,n⇙" from DBM_reset'_sound[OF assms(4,2) ** this] obtain ts where "set_clocks r ts u ∈ [And D (abstr g (λi j. ∞) v)]⇘v,n⇙" by auto with A11 have *: "set_clocks r ts u ∈ ([D]⇘v,n⇙) ∩ ({u. u ⊢ g})" by blast from DBM_reset'_resets[OF assms(4,2) **] u have "∀c ∈ set r. u c = 0" unfolding DBM_zone_repr_def by auto from reset_set[OF this] have "[r→0]set_clocks r ts u = u" by simp with * show "u ∈ zone_set (([D]⇘v,n⇙) ∩ {u. u ⊢ g}) r" unfolding zone_set_def by force next fix u assume u: "u ∈ zone_set (([D]⇘v,n⇙) ∩ {u. u ⊢ g}) r" from DBM_reset'_complete[OF _ assms(2) **] u A11 show "u ∈ [?D]⇘v,n⇙" unfolding DBM_zone_repr_def zone_set_def by force qed from D' And_correct D_reset have A22: "[And ?D (abstr (inv_of A l') (λi j. ∞) v)]⇘v,n⇙ = ([?D]⇘v,n⇙) ∩ ({u. u ⊢ inv_of A l'})" by blast with D_reset 2(2,3) show ?thesis by auto qed lemma step_z_dbm_DBM: assumes "A ⊢ ⟨l, [D]⇘v,n⇙⟩ ↝ ⟨l', Z⟩" "global_clock_numbering A v n" obtains D' where "A ⊢ ⟨l, D⟩ ↝⇘v,n⇙ ⟨l', D'⟩" "Z = [D']⇘v,n⇙" using assms proof (cases, goal_cases) case 1 hence "clock_numbering' v n" "∀c∈clk_set A. v c ≤ n" by metis+ note assms = assms(1) this from assms(3) have *: "∀c∈collect_clks (inv_of A l). v c ≤ n" unfolding clkp_set_def collect_clki_def inv_of_def by (fastforce simp: collect_clks_id) obtain D'' where D''_def: "D'' = abstr (inv_of A l) (λi j. ∞) v" by auto hence D'':"[D'']⇘v,n⇙ = {u. u ⊢ inv_of A l}" using dbm_abstr_zone_eq[OF assms(2) *] by metis obtain A1 where A1: "A1 = And D D''" by fast with And_correct D'' have A11: "[A1]⇘v,n⇙ = ([D]⇘v,n⇙) ∩ ({u. u ⊢ inv_of A l})" by blast then obtain D_up where D_up': "D_up = up A1" by blast with up_correct assms(2) A11 have D_up: "[D_up]⇘v,n⇙ = (([D]⇘v,n⇙) ∩ ({u. u ⊢ inv_of A l}))⇧^{↑}" by metis obtain A2 where A2: "A2 = And D_up D''" by fast with And_correct D'' have A22: "[A2]⇘v,n⇙ = ([D_up]⇘v,n⇙) ∩ ({u. u ⊢ inv_of A l})" by blast from A2 D_up' D''_def A1 have "A ⊢ ⟨l,D⟩ ↝⇘v,n⇙ ⟨l,A2⟩" by blast moreover from A22 D_up have "[A2]⇘v,n⇙ = (([D]⇘v,n⇙) ∩ {u. u ⊢ inv_of A l})⇧^{↑}∩ {u. u ⊢ inv_of A l}" by auto ultimately show thesis using 1 by (intro that[of A2]) auto next case (2 g a r) hence "clock_numbering' v n" "∀c∈clk_set A. v c ≤ n" "∀k≤n. k > 0 ⟶ (∃c. v c = k)" by metis+ note assms = assms(1) this from assms(3) have *: "∀c∈collect_clks (inv_of A l'). v c ≤ n" unfolding clkp_set_def collect_clki_def inv_of_def by (fastforce simp: collect_clks_id) obtain D' where D'_def: "D' = abstr (inv_of A l') (λi j. ∞) v" by blast hence D':"[D']⇘v,n⇙ = {u. u ⊢ inv_of A l'}" using dbm_abstr_zone_eq[OF assms(2) *] by simp from assms(3) 2(4) have *: "∀c∈collect_clks g. v c ≤ n" unfolding clkp_set_def collect_clkt_def inv_of_def by (fastforce simp: collect_clks_id) obtain D'' where D''_def: "D'' = abstr g (λi j. ∞) v" by blast hence D'':"[D'']⇘v,n⇙ = {u. u ⊢ g}" using dbm_abstr_zone_eq[OF assms(2) *] by auto obtain A1 where A1: "A1 = And D D''" by fast with And_correct D'' have A11: "[A1]⇘v,n⇙ = ([D]⇘v,n⇙) ∩ ({u. u ⊢ g})" by blast let ?D = "reset' A1 n r v 0" have "set r ⊆ clk_set A" using 2(4) unfolding trans_of_def collect_clkvt_def by fastforce hence **:"∀c∈set r. v c ≤ n" using assms(3) by fastforce have D_reset: "[?D]⇘v,n⇙ = zone_set (([D]⇘v,n⇙) ∩ {u. u ⊢ g}) r" proof safe fix u assume u: "u ∈ [?D]⇘v,n⇙" from DBM_reset'_sound[OF assms(4,2) ** this] obtain ts where "set_clocks r ts u ∈ [A1]⇘v,n⇙" by auto with A11 have *: "set_clocks r ts u ∈ ([D]⇘v,n⇙) ∩ ({u. u ⊢ g})" by blast from DBM_reset'_resets[OF assms(4,2) **] u have "∀c ∈ set r. u c = 0" unfolding DBM_zone_repr_def by auto from reset_set[OF this] have "[r→0]set_clocks r ts u = u" by simp with * show "u ∈ zone_set (([D]⇘v,n⇙) ∩ {u. u ⊢ g}) r" unfolding zone_set_def by force next fix u assume u: "u ∈ zone_set (([D]⇘v,n⇙) ∩ {u. u ⊢ g}) r" from DBM_reset'_complete[OF _ assms(2) **] u A11 show "u ∈ [?D]⇘v,n⇙" unfolding DBM_zone_repr_def zone_set_def by force qed obtain A2 where A2: "A2 = And ?D D'" by fast with And_correct D' have A22: "[A2]⇘v,n⇙ = ([?D]⇘v,n⇙) ∩ ({u. u ⊢ inv_of A l'})" by blast from 2(4) A2 D'_def D''_def A1 have "A ⊢ ⟨l,D⟩ ↝⇘v,n⇙ ⟨l',A2⟩" by blast moreover from A22 D_reset have "[A2]⇘v,n⇙ = zone_set (([D]⇘v,n⇙) ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}" by auto ultimately show ?thesis using 2 by (intro that[of A2]) simp+ qed lemma step_z_computable: assumes "A ⊢ ⟨l, [D]⇘v,n⇙⟩ ↝ ⟨l',Z⟩" "global_clock_numbering A v n" obtains D' where "Z = [D']⇘v,n⇙" using step_z_dbm_DBM[OF assms] by blast lemma step_z_dbm_complete: assumes "global_clock_numbering A v n" "A ⊢ ⟨l, u⟩ → ⟨l',u'⟩" and "u ∈ [(D )]⇘v,n⇙" shows "∃ D'. A ⊢ ⟨l, D⟩ ↝⇘v,n⇙ ⟨l',D'⟩ ∧ u' ∈ [D']⇘v,n⇙" proof - note A = assms from step_z_complete[OF A(2,3)] obtain Z' where Z': "A ⊢ ⟨l, [D]⇘v,n⇙⟩ ↝ ⟨l',Z'⟩" "u' ∈ Z'" by auto with step_z_dbm_DBM[OF Z'(1) A(1)] obtain D' where D': "A ⊢ ⟨l, D⟩ ↝⇘v,n⇙ ⟨l',D'⟩" "Z' = [D']⇘v,n⇙" by metis with Z'(2) show ?thesis by auto qed subsection ‹Multi Step› inductive steps_z_dbm :: "('a, 'c, 't, 's) ta ⇒ 's ⇒ ('t::time) DBM ⇒ ('c ⇒ nat) ⇒ nat ⇒ 's ⇒ ('t::time) DBM ⇒ bool" ("_ ⊢ ⟨_, _⟩ ↝*⇘_,_⇙ ⟨_, _⟩" [61,61,61] 61) where refl: "A ⊢ ⟨l,D⟩ ↝*⇘v,n⇙ ⟨l,D⟩" | step: "A ⊢ ⟨l,D⟩ ↝⇘v,n⇙ ⟨l',D'⟩ ⟹ A ⊢ ⟨l',D'⟩ ↝*⇘v,n⇙ ⟨l'',D''⟩ ⟹ A ⊢ ⟨l,D⟩ ↝*⇘v,n⇙ ⟨l'',D''⟩" declare steps_z_dbm.intros[intro] lemma steps_z_dbm_sound: assumes "A ⊢ ⟨l,D⟩ ↝*⇘v,n⇙ ⟨l',D'⟩" and "global_clock_numbering A v n" and "u' ∈ [D']⇘v,n⇙" shows "∃ u ∈ [D]⇘v,n⇙. A ⊢ ⟨l, u⟩ →* ⟨l',u'⟩" using assms proof (induction A l D v n l' D' rule: steps_z_dbm.induct) case refl thus ?case by fast next case (step A l D v n l' D' l'' D'') then obtain u'' where u'': "A ⊢ ⟨l', u''⟩ →* ⟨l'',u'⟩" "u''∈[D']⇘v,n⇙" by blast with step_z_sound[OF step_z_dbm_sound[OF step(1,4)]] obtain u where "u ∈ [D]⇘v,n⇙" "A ⊢ ⟨l, u⟩ → ⟨l',u''⟩" by blast with u'' show ?case by blast qed lemma steps_z_dbm_complete: assumes "A ⊢ ⟨l, u⟩ →* ⟨l',u'⟩" and "global_clock_numbering A v n" and "u ∈ [D]⇘v,n⇙" shows "∃ D'. A ⊢ ⟨l, D⟩ ↝*⇘v,n⇙ ⟨l', D'⟩ ∧ u' ∈ [D']⇘v,n⇙" using assms proof (induction arbitrary: D rule: steps.induct) case refl thus ?case by auto next case (step A l u l' u' l'' u'' D) from step_z_dbm_complete[OF step(4,1,5)] obtain D' where D': "A ⊢ ⟨l,D⟩ ↝⇘v,n⇙ ⟨l',D'⟩" "u' ∈ [D']⇘v,n⇙" by auto with step(3)[OF step(4)] obtain D'' where "A ⊢ ⟨l',D'⟩ ↝*⇘v,n⇙ ⟨l'',D''⟩" "u'' ∈ [D'']⇘v,n⇙" by blast with D' show ?case by blast qed end (*>*)