theory Closure imports Regions begin section ‹Correct Approximation of Zones with ‹α›-regions› locale AlphaClosure = fixes X k ℛ and V :: "('c, t) cval set" defines "ℛ ≡ {region X I r | I r. valid_region X k I r}" defines "V ≡ {v . ∀ x ∈ X. v x ≥ 0}" assumes finite: "finite X" begin lemmas set_of_regions_spec = set_of_regions[OF _ _ _ finite, of _ k, folded ℛ_def] lemmas region_cover_spec = region_cover[of X _ k, folded ℛ_def] lemmas region_unique_spec = region_unique[of ℛ X k, folded ℛ_def, simplified] lemmas regions_closed'_spec = regions_closed'[of ℛ X k, folded ℛ_def, simplified] lemma valid_regions_distinct_spec: "R ∈ ℛ ⟹ R' ∈ ℛ ⟹ v ∈ R ⟹ v ∈ R' ⟹ R = R'" unfolding ℛ_def using valid_regions_distinct by auto (drule valid_regions_distinct, assumption+, simp)+ definition cla ("Closure⇩_{α}_" [71] 71) where "cla Z = ⋃ {R ∈ ℛ. R ∩ Z ≠ {}}" subsubsection ‹The nice and easy properties proved by Bouyer› lemma closure_constraint_id: "∀(x, m)∈collect_clock_pairs g. m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ ⟹ Closure⇩_{α}⦃g⦄ = ⦃g⦄ ∩ V" proof goal_cases case 1 show ?case proof auto fix v assume v: "v ∈ Closure⇩_{α}⦃g⦄" then obtain R where R: "v ∈ R" "R ∈ ℛ" "R ∩ ⦃g⦄ ≠ {}" unfolding cla_def by auto with ccompatible[OF 1, folded ℛ_def] show "v ∈ ⦃g⦄" unfolding ccompatible_def by auto from R show "v ∈ V" unfolding V_def ℛ_def by auto next fix v assume v: "v ∈ ⦃g⦄" "v ∈ V" with region_cover[of X v k, folded ℛ_def] obtain R where "R ∈ ℛ" "v ∈ R" unfolding V_def by auto then show "v ∈ Closure⇩_{α}⦃g⦄" unfolding cla_def using v by auto qed qed lemma closure_id': "Z ≠ {} ⟹ Z ⊆ R ⟹ R ∈ ℛ ⟹ Closure⇩_{α}Z = R" proof goal_cases case 1 note A = this then have "R ⊆ Closure⇩_{α}Z" unfolding cla_def by auto moreover { fix R' assume R': "Z ∩ R' ≠ {}" "R' ∈ ℛ" "R ≠ R'" with A obtain v where "v ∈ R" "v ∈ R'" by auto with ℛ_regions_distinct[OF _ A(3) this(1) R'(2-)] ℛ_def have False by auto } ultimately show ?thesis unfolding cla_def by auto qed lemma closure_id: "Closure⇩_{α}Z ≠ {} ⟹ Z ⊆ R ⟹ R ∈ ℛ ⟹ Closure⇩_{α}Z = R" proof goal_cases case 1 then have "Z ≠ {}" unfolding cla_def by auto with 1 closure_id' show ?case by blast qed lemma closure_update_mono: "Z ⊆ V ⟹ set r ⊆ X ⟹ zone_set (Closure⇩_{α}Z) r ⊆ Closure⇩_{α}(zone_set Z r)" proof - assume A: "Z ⊆ V" "set r ⊆ X" let ?U = "{R ∈ ℛ. Z ∩ R ≠ {}}" from A(1) region_cover_spec have "∀ v ∈ Z. ∃ R. R ∈ ℛ ∧ v ∈ R" unfolding V_def by auto then have "Z = ⋃ {Z ∩ R | R. R ∈ ?U}" proof (auto, goal_cases) case (1 v) then obtain R where "R ∈ ℛ" "v ∈ R" by auto moreover with 1 have "Z ∩ R ≠ {}" "v ∈ Z ∩ R" by auto ultimately show ?case by auto qed then obtain U where U: "Z = ⋃ {Z ∩ R | R. R ∈ U}" "∀ R ∈ U. R ∈ ℛ" by blast { fix R assume R: "R ∈ U" { fix v' assume v': "v' ∈ zone_set (Closure⇩_{α}(Z ∩ R)) r - Closure⇩_{α}(zone_set (Z ∩ R) r)" then obtain v where *: "v ∈ Closure⇩_{α}(Z ∩ R)" "v' = [r → 0]v" unfolding zone_set_def by auto with closure_id[of "Z ∩ R" R] R U(2) have **: "Closure⇩_{α}(Z ∩ R) = R" "Closure⇩_{α}(Z ∩ R) ∈ ℛ" by fastforce+ with region_set'_id[OF _ *(1) finite _ _ A(2), of k 0, folded ℛ_def, OF this(2)] have ***: "zone_set R r ∈ ℛ" "[r→0]v ∈ zone_set R r" unfolding zone_set_def region_set'_def by auto from * have "Z ∩ R ≠ {}" unfolding cla_def by auto then have "zone_set (Z ∩ R) r ≠ {}" unfolding zone_set_def by auto from closure_id'[OF this _ ***(1)] have "Closure⇩_{α}zone_set (Z ∩ R) r = zone_set R r" unfolding zone_set_def by auto with v' **(1) have False by auto } then have "zone_set (Closure⇩_{α}(Z ∩ R)) r ⊆ Closure⇩_{α}(zone_set (Z ∩ R) r)" by auto } note Z_i = this from U(1) have "Closure⇩_{α}Z = ⋃ {Closure⇩_{α}(Z ∩ R) | R. R ∈ U}" unfolding cla_def by auto then have "zone_set (Closure⇩_{α}Z) r = ⋃ {zone_set (Closure⇩_{α}(Z ∩ R)) r | R. R ∈ U}" unfolding zone_set_def by auto also have "… ⊆ ⋃ {Closure⇩_{α}(zone_set (Z ∩ R) r) | R. R ∈ U}" using Z_i by auto also have "… = Closure⇩_{α}⋃ {(zone_set (Z ∩ R) r) | R. R ∈ U}" unfolding cla_def by auto also have "… = Closure⇩_{α}zone_set (⋃ {Z ∩ R| R. R ∈ U}) r" proof goal_cases case 1 have "zone_set (⋃ {Z ∩ R| R. R ∈ U}) r = ⋃ {(zone_set (Z ∩ R) r) | R. R ∈ U}" unfolding zone_set_def by auto then show ?case by auto qed finally show "zone_set (Closure⇩_{α}Z) r ⊆ Closure⇩_{α}(zone_set Z r)" using U by simp qed lemma SuccI3: "R ∈ ℛ ⟹ v ∈ R ⟹ t ≥ 0 ⟹ (v ⊕ t) ∈ R' ⟹ R' ∈ ℛ ⟹ R' ∈ Succ ℛ R" apply (intro SuccI2[of ℛ X k, folded ℛ_def, simplified]) apply assumption+ apply (intro region_unique[of ℛ X k, folded ℛ_def, simplified, symmetric]) by assumption+ lemma closure_delay_mono: "Z ⊆ V ⟹ (Closure⇩_{α}Z)⇧^{↑}⊆ Closure⇩_{α}(Z⇧^{↑})" proof fix v assume v: "v ∈ (Closure⇩_{α}Z)⇧^{↑}" and Z: "Z ⊆ V" then obtain u u' t R where A: "u ∈ Closure⇩_{α}Z" "v = (u ⊕ t)" "u ∈ R" "u' ∈ R" "R ∈ ℛ" "u' ∈ Z" "t ≥ 0" unfolding cla_def zone_delay_def by blast from A(3,5) have "∀ x ∈ X. u x ≥ 0" unfolding ℛ_def by fastforce with region_cover_spec[of v] A(2,7) obtain R' where R': "R' ∈ ℛ" "v ∈ R'" unfolding cval_add_def by auto with set_of_regions_spec[OF A(5,4), OF SuccI3, of u] A obtain t where t: "t ≥ 0" "[u' ⊕ t]⇩ℛ = R'" by auto with A have "(u' ⊕ t) ∈ Z⇧^{↑}" unfolding zone_delay_def by auto moreover from regions_closed'_spec[OF A(5,4)] t have "(u' ⊕ t) ∈ R'" by auto ultimately have "R' ∩ (Z⇧^{↑}) ≠ {}" by auto with R' show "v ∈ Closure⇩_{α}(Z⇧^{↑})" unfolding cla_def by auto qed lemma region_V: "R ∈ ℛ ⟹ R ⊆ V" using V_def ℛ_def region.cases by auto lemma closure_V: "Closure⇩_{α}Z ⊆ V" unfolding cla_def using region_V by auto lemma closure_V_int: "Closure⇩_{α}Z = Closure⇩_{α}(Z ∩ V)" unfolding cla_def using region_V by auto lemma closure_constraint_mono: "Closure⇩_{α}g = g ⟹ g ∩ (Closure⇩_{α}Z) ⊆ Closure⇩_{α}(g ∩ Z)" unfolding cla_def by auto lemma closure_constraint_mono': assumes "Closure⇩_{α}g = g ∩ V" shows "g ∩ (Closure⇩_{α}Z) ⊆ Closure⇩_{α}(g ∩ Z)" proof - from assms closure_V_int have "Closure⇩_{α}(g ∩ V) = g ∩ V" by auto from closure_constraint_mono[OF this, of Z] have "g ∩ (V ∩ Closure⇩_{α}Z) ⊆ Closure⇩_{α}(g ∩ Z ∩ V)" by (metis Int_assoc Int_commute) with closure_V[of Z] closure_V_int[of "g ∩ Z"] show ?thesis by auto qed lemma cla_empty_iff: "Z ⊆ V ⟹ Z = {} ⟷ Closure⇩_{α}Z = {}" unfolding cla_def V_def using region_cover_spec by fast lemma closure_involutive_aux: "U ⊆ ℛ ⟹ Closure⇩_{α}⋃ U = ⋃ U" unfolding cla_def using valid_regions_distinct_spec by blast lemma closure_involutive_aux': "∃ U. U ⊆ ℛ ∧ Closure⇩_{α}Z = ⋃ U" unfolding cla_def by (rule exI[where x = "{R ∈ ℛ. R ∩ Z ≠ {}}"]) auto lemma closure_involutive: "Closure⇩_{α}Closure⇩_{α}Z = Closure⇩_{α}Z" using closure_involutive_aux closure_involutive_aux' by metis lemma closure_involutive': "Z ⊆ Closure⇩_{α}W ⟹ Closure⇩_{α}Z ⊆ Closure⇩_{α}W" unfolding cla_def using valid_regions_distinct_spec by fast lemma closure_subs: "Z ⊆ V ⟹ Z ⊆ Closure⇩_{α}Z" unfolding cla_def V_def using region_cover_spec by fast lemma cla_mono': "Z' ⊆ V ⟹ Z ⊆ Z' ⟹ Closure⇩_{α}Z ⊆ Closure⇩_{α}Z'" by (meson closure_involutive' closure_subs subset_trans) lemma cla_mono: "Z ⊆ Z' ⟹ Closure⇩_{α}Z ⊆ Closure⇩_{α}Z'" using closure_V_int cla_mono'[of "Z' ∩ V" "Z ∩ V"] by auto section ‹A New Zone Semantics Abstracting with ‹Closure⇩_{α}›› subsection ‹Single step› inductive step_z_alpha :: "('a, 'c, t, 's) ta ⇒ 's ⇒ ('c, t) zone ⇒ 's ⇒ ('c, t) zone ⇒ bool" ("_ ⊢ ⟨_, _⟩ ↝⇩_{α}⟨_, _⟩" [61,61,61] 61) where step_alpha: "A ⊢ ⟨l, Z⟩ ↝ ⟨l', Z'⟩ ⟹ A ⊢ ⟨l, Z⟩ ↝⇩_{α}⟨l', Closure⇩_{α}Z'⟩" inductive_cases[elim!]: "A ⊢ ⟨l, u⟩ ↝⇩_{α}⟨l',u'⟩" declare step_z_alpha.intros[intro] lemma up_V: "Z ⊆ V ⟹ Z⇧^{↑}⊆ V" unfolding V_def zone_delay_def cval_add_def by auto lemma reset_V: "Z ⊆ V ⟹ (zone_set Z r) ⊆ V" unfolding V_def unfolding zone_set_def by (induction r, auto) lemma step_z_V: "A ⊢ ⟨l, Z⟩ ↝ ⟨l',Z'⟩ ⟹ Z ⊆ V ⟹ Z' ⊆ V" apply (induction rule: step_z.induct) apply (rule le_infI1) apply (rule up_V) apply blast apply (rule le_infI1) apply (rule reset_V) by blast text ‹Single-step soundness and completeness follows trivially from ‹cla_empty_iff›.› lemma step_z_alpha_sound: "A ⊢ ⟨l, Z⟩ ↝⇩_{α}⟨l',Z'⟩ ⟹ Z ⊆ V ⟹ Z' ≠ {} ⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝ ⟨l',Z''⟩ ∧ Z'' ≠ {}" apply (induction rule: step_z_alpha.induct) apply (frule step_z_V) apply assumption apply (rotate_tac 3) apply (drule cla_empty_iff) by auto lemma step_z_alpha_complete: "A ⊢ ⟨l, Z⟩ ↝ ⟨l',Z'⟩ ⟹ Z ⊆ V ⟹ Z' ≠ {} ⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝⇩_{α}⟨l',Z''⟩ ∧ Z'' ≠ {}" apply (frule step_z_V) apply assumption apply (rotate_tac 3) apply (drule cla_empty_iff) by auto lemma zone_set_mono: "A ⊆ B ⟹ zone_set A r ⊆ zone_set B r" unfolding zone_set_def by auto lemma zone_delay_mono: "A ⊆ B ⟹ A⇧^{↑}⊆ B⇧^{↑}" unfolding zone_delay_def by auto subsection ‹Multi step› inductive steps_z_alpha :: "('a, 'c, t, 's) ta ⇒ 's ⇒ ('c, t) zone ⇒ 's ⇒ ('c, t) zone ⇒ bool" ("_ ⊢ ⟨_, _⟩ ↝⇩_{α}* ⟨_, _⟩" [61,61,61] 61) where refl: "A ⊢ ⟨l, Z⟩ ↝⇩_{α}* ⟨l, Z⟩" | step: "A ⊢ ⟨l, Z⟩ ↝⇩_{α}* ⟨l', Z'⟩ ⟹ A ⊢ ⟨l', Z'⟩ ↝⇩_{α}⟨l'', Z''⟩ ⟹ A ⊢ ⟨l, Z⟩ ↝⇩_{α}* ⟨l'', Z''⟩" declare steps_z_alpha.intros[intro] lemma subset_int_mono: "A ⊆ B ⟹ A ∩ C ⊆ B ∩ C" by blast text ‹P. Bouyer's calculation for @{term "Post(Closure⇩_{α}Z, e) ⊆ Closure⇩_{α}(Post (Z, e))"}› text ‹This is now obsolete as we argue solely with monotonicty of ‹steps_z› w.r.t ‹Closure⇩_{α}›› lemma calc: "valid_abstraction A X k ⟹ Z ⊆ V ⟹ A ⊢ ⟨l, Closure⇩_{α}Z⟩ ↝ ⟨l', Z'⟩ ⟹ ∃Z''. A ⊢ ⟨l, Z⟩ ↝⇩_{α}⟨l', Z''⟩ ∧ Z' ⊆ Z''" proof (cases rule: step_z.cases, assumption, goal_cases) case 1 note A = this from A(1) have "∀(x, m)∈clkp_set A. m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ" by (fastforce elim: valid_abstraction.cases) then have "∀(x, m)∈collect_clock_pairs (inv_of A l). m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ" unfolding clkp_set_def collect_clki_def inv_of_def by auto from closure_constraint_id[OF this] have *: "Closure⇩_{α}⦃inv_of A l⦄ = ⦃inv_of A l⦄ ∩ V" . from closure_constraint_mono'[OF *, of Z] have "(Closure⇩_{α}Z) ∩ {u. u ⊢ inv_of A l} ⊆ Closure⇩_{α}(Z ∩ {u. u ⊢ inv_of A l})" unfolding ccval_def by (subst Int_commute) (subst (asm) (2) Int_commute, assumption) moreover have "…⇧^{↑}⊆ Closure⇩_{α}((Z ∩ {u. u ⊢ inv_of A l})⇧^{↑})" using A(2) by (blast intro!: closure_delay_mono) ultimately have "Z' ⊆ Closure⇩_{α}((Z ∩ {u. u ⊢ inv_of A l})⇧^{↑}∩ {u. u ⊢ inv_of A l})" using closure_constraint_mono'[OF *, of "(Z ∩ {u. u ⊢ inv_of A l})⇧^{↑}"] unfolding ccval_def apply (subst A(5)) apply (subst (asm) (5 7) Int_commute) apply (rule subset_trans) defer apply assumption apply (subst subset_int_mono) defer apply rule apply (rule subset_trans) defer apply assumption apply (rule zone_delay_mono) apply assumption done with A(4,3) show ?thesis by auto next case (2 g a r) note A = this from A(1) have *: "∀(x, m)∈clkp_set A. m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ" "collect_clkvt (trans_of A) ⊆ X" "finite X" by (auto elim: valid_abstraction.cases) from *(1) A(5) have "∀(x, m)∈collect_clock_pairs (inv_of A l'). m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ" unfolding clkp_set_def collect_clki_def inv_of_def by fastforce from closure_constraint_id[OF this] have **: "Closure⇩_{α}⦃inv_of A l'⦄ = ⦃inv_of A l'⦄ ∩ V" . from *(1) A(5) have "∀(x, m)∈collect_clock_pairs g. m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ" unfolding clkp_set_def collect_clkt_def by fastforce from closure_constraint_id[OF this] have ***: "Closure⇩_{α}⦃g⦄ = ⦃g⦄ ∩ V" . from *(2) A(5) have ****: "set r ⊆ X" unfolding collect_clkvt_def by fastforce from closure_constraint_mono'[OF ***, of Z] have "(Closure⇩_{α}Z) ∩ {u. u ⊢ g} ⊆ Closure⇩_{α}(Z ∩ {u. u ⊢ g})" unfolding ccval_def by (subst Int_commute) (subst (asm) (2) Int_commute, assumption) moreover have "zone_set … r ⊆ Closure⇩_{α}(zone_set (Z ∩ {u. u ⊢ g}) r)" using **** A(2) by (intro closure_update_mono, auto) ultimately have "Z' ⊆ Closure⇩_{α}(zone_set (Z ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'})" using closure_constraint_mono'[OF **, of "zone_set (Z ∩ {u. u ⊢ g}) r"] unfolding ccval_def apply (subst A(4)) apply (subst (asm) (5 7) Int_commute) apply (rule subset_trans) defer apply assumption apply (subst subset_int_mono) defer apply rule apply (rule subset_trans) defer apply assumption apply (rule zone_set_mono) apply assumption done with A(5) show ?thesis by auto qed text ‹ Turning P. Bouyers argument for multiple steps into an inductive proof is not direct. With this initial argument we can get to a point where the induction hypothesis is applicable. This breaks the "information hiding" induced by the different variants of steps. › lemma steps_z_alpha_closure_involutive'_aux: "A ⊢ ⟨l, Z⟩ ↝ ⟨l',Z'⟩ ⟹ Closure⇩_{α}Z ⊆ Closure⇩_{α}W ⟹ valid_abstraction A X k ⟹ Z ⊆ V ⟹ ∃ W'. A ⊢ ⟨l, W⟩ ↝ ⟨l',W'⟩ ∧ Closure⇩_{α}Z' ⊆ Closure⇩_{α}W'" proof (induction rule: step_z.induct) case A: (step_t_z A l Z) let ?Z' = "(Z ∩ {u. u ⊢ inv_of A l})⇧^{↑}∩ {u. u ⊢ inv_of A l}" let ?W' = "(W ∩ {u. u ⊢ inv_of A l})⇧^{↑}∩ {u. u ⊢ inv_of A l}" from ℛ_def have ℛ_def': "ℛ = {region X I r |I r. valid_region X k I r}" by simp have step_z: "A ⊢ ⟨l, W⟩ ↝ ⟨l,?W'⟩" by auto moreover have "Closure⇩_{α}?Z' ⊆ Closure⇩_{α}?W'" proof fix v assume v: "v ∈ Closure⇩_{α}?Z'" then obtain R' v' where 1: "R' ∈ ℛ" "v ∈ R'" "v' ∈ R'" "v' ∈ ?Z'" unfolding cla_def by auto then obtain u d where "u ∈ Z" and v': "v' = u ⊕ d" "u ⊢ inv_of A l" "u ⊕ d ⊢ inv_of A l" "0 ≤ d" unfolding zone_delay_def by blast with closure_subs[OF A(3)] A(1) obtain u' R where u': "u' ∈ W" "u ∈ R" "u' ∈ R" "R ∈ ℛ" unfolding cla_def by blast then have "∀x∈X. 0 ≤ u x" unfolding ℛ_def by fastforce from region_cover'[OF ℛ_def' this] have R: "[u]⇩ℛ ∈ ℛ" "u ∈ [u]⇩ℛ" by auto from SuccI2[OF ℛ_def' this(2,1) v'(4), of "[v']⇩ℛ"] v'(1) have v'1: "[v']⇩ℛ ∈ Succ ℛ ([u]⇩ℛ)" "[v']⇩ℛ ∈ ℛ" by auto from regions_closed'_spec[OF R(1,2) v'(4)] v'(1) have v'2: "v' ∈ [v']⇩ℛ" by simp from A(2) have *: "∀(x, m)∈clkp_set A. m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ" "collect_clkvt (trans_of A) ⊆ X" "finite X" by (auto elim: valid_abstraction.cases) from *(1) u'(2) have "∀(x, m)∈collect_clock_pairs (inv_of A l). m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ" unfolding clkp_set_def collect_clki_def inv_of_def by fastforce from ccompatible[OF this, folded ℛ_def'] v'1(2) v'2 v'(1,2,3) R have 3: "[v']⇩ℛ ⊆ ⦃inv_of A l⦄" "([u]⇩ℛ) ⊆ ⦃inv_of A l⦄" unfolding ccompatible_def ccval_def by auto with A v'1 R(1) ℛ_def' have "A,ℛ ⊢ ⟨l, ([u]⇩ℛ)⟩ ↝ ⟨l,([v']⇩ℛ)⟩" by auto with valid_regions_distinct_spec[OF v'1(2) 1(1) v'2 1(3)] region_unique_spec[OF u'(2,4)] have step_r: "A,ℛ ⊢ ⟨l, R⟩ ↝ ⟨l, R'⟩" and 2: "[v']⇩ℛ = R'" "[u]⇩ℛ = R" by auto from set_of_regions_spec[OF u'(4,3)] v'1(1) 2 obtain t where t: "t ≥ 0" "[u' ⊕ t]⇩ℛ = R'" by auto with regions_closed'_spec[OF u'(4,3) this(1)] step_t_r(1) have *: "u' ⊕ t ∈ R'" by auto with t(1) 3 2 u'(1,3) have "A ⊢ ⟨l, u'⟩ → ⟨l, u' ⊕ t⟩" "u' ⊕ t ∈ ?W'" unfolding zone_delay_def ccval_def by auto with * 1(1) have "R' ⊆ Closure⇩_{α}?W'" unfolding cla_def by auto with 1(2) show "v ∈ Closure⇩_{α}?W'" .. qed ultimately show ?case by auto next case A: (step_a_z A l g a r l' Z) let ?Z' = "zone_set (Z ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}" let ?W' = "zone_set (W ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}" from ℛ_def have ℛ_def': "ℛ = {region X I r |I r. valid_region X k I r}" by simp from A(1) have step_z: "A ⊢ ⟨l, W⟩ ↝ ⟨l',?W'⟩" by auto moreover have "Closure⇩_{α}?Z' ⊆ Closure⇩_{α}?W'" proof fix v assume v: "v ∈ Closure⇩_{α}?Z'" then obtain R' v' where 1: "R' ∈ ℛ" "v ∈ R'" "v' ∈ R'" "v' ∈ ?Z'" unfolding cla_def by auto then obtain u where "u ∈ Z" and v': "v' = [r→0]u" "u ⊢ g" "v' ⊢ inv_of A l'" unfolding zone_set_def by blast let ?R'= "region_set' (([u]⇩ℛ) ∩ {u. u ⊢ g}) r 0 ∩ {u. u ⊢ inv_of A l'}" from ‹u ∈ Z› closure_subs[OF A(4)] A(2) obtain u' R where u': "u' ∈ W" "u ∈ R" "u' ∈ R" "R ∈ ℛ" unfolding cla_def by blast then have "∀x∈X. 0 ≤ u x" unfolding ℛ_def by fastforce from region_cover'[OF ℛ_def' this] have R: "[u]⇩ℛ ∈ ℛ" "u ∈ [u]⇩ℛ" by auto from step_r_complete_aux[OF ℛ_def' A(3) this(2,1) A(1) v'(2)] v' have *: "[u]⇩ℛ = ([u]⇩ℛ) ∩ {u. u ⊢ g}" "?R' = region_set' ([u]⇩ℛ) r 0" "?R' ∈ ℛ" by auto from ℛ_def' A(3) have "collect_clkvt (trans_of A) ⊆ X" "finite X" by (auto elim: valid_abstraction.cases) with A(1) have r: "set r ⊆ X" unfolding collect_clkvt_def by fastforce from * v'(1) R(2) have "v' ∈ ?R'" unfolding region_set'_def by auto moreover have "A,ℛ ⊢ ⟨l,([u]⇩ℛ)⟩ ↝ ⟨l',?R'⟩" using R(1) ℛ_def' A(1,3) v'(2) by auto thm valid_regions_distinct_spec with valid_regions_distinct_spec[OF *(3) 1(1) ‹v' ∈ ?R'› 1(3)] region_unique_spec[OF u'(2,4)] have 2: "?R' = R'" "[u]⇩ℛ = R" by auto with * u' have *: "[r→0]u' ∈ ?R'" "u' ⊢ g" "[r→0]u' ⊢ inv_of A l'" unfolding region_set'_def by auto with A(1) have "A ⊢ ⟨l, u'⟩ → ⟨l',[r→0]u'⟩" apply (intro step.intros(1)) apply rule by auto moreover from * u'(1) have "[r→0]u' ∈ ?W'" unfolding zone_set_def by auto ultimately have "R' ⊆ Closure⇩_{α}?W'" using *(1) 1(1) 2(1) unfolding cla_def by auto with 1(2) show "v ∈ Closure⇩_{α}?W'" .. qed ultimately show ?case by meson qed lemma steps_z_alpha_closure_involutive'_aux': "A ⊢ ⟨l, Z⟩ ↝ ⟨l',Z'⟩ ⟹ Closure⇩_{α}Z ⊆ Closure⇩_{α}W ⟹ valid_abstraction A X k ⟹ Z ⊆ V ⟹ W ⊆ Z ⟹ ∃ W'. A ⊢ ⟨l, W⟩ ↝ ⟨l',W'⟩ ∧ Closure⇩_{α}Z' ⊆ Closure⇩_{α}W' ∧ W' ⊆ Z'" proof (induction rule: step_z.induct) case A: (step_t_z A l Z) let ?Z' = "(Z ∩ {u. u ⊢ inv_of A l})⇧^{↑}∩ {u. u ⊢ inv_of A l}" let ?W' = "(W ∩ {u. u ⊢ inv_of A l})⇧^{↑}∩ {u. u ⊢ inv_of A l}" from ℛ_def have ℛ_def': "ℛ = {region X I r |I r. valid_region X k I r}" by simp have step_z: "A ⊢ ⟨l, W⟩ ↝ ⟨l,?W'⟩" by auto moreover have "Closure⇩_{α}?Z' ⊆ Closure⇩_{α}?W'" proof fix v assume v: "v ∈ Closure⇩_{α}?Z'" then obtain R' v' where 1: "R' ∈ ℛ" "v ∈ R'" "v' ∈ R'" "v' ∈ ?Z'" unfolding cla_def by auto then obtain u d where "u ∈ Z" and v': "v' = u ⊕ d" "u ⊢ inv_of A l" "u ⊕ d ⊢ inv_of A l" "0 ≤ d" unfolding zone_delay_def by blast with closure_subs[OF A(3)] A(1) obtain u' R where u': "u' ∈ W" "u ∈ R" "u' ∈ R" "R ∈ ℛ" unfolding cla_def by blast then have "∀x∈X. 0 ≤ u x" unfolding ℛ_def by fastforce from region_cover'[OF ℛ_def' this] have R: "[u]⇩ℛ ∈ ℛ" "u ∈ [u]⇩ℛ" by auto from SuccI2[OF ℛ_def' this(2,1) v'(4), of "[v']⇩ℛ"] v'(1) have v'1: "[v']⇩ℛ ∈ Succ ℛ ([u]⇩ℛ)" "[v']⇩ℛ ∈ ℛ" by auto from regions_closed'_spec[OF R(1,2) v'(4)] v'(1) have v'2: "v' ∈ [v']⇩ℛ" by simp from A(2) have *: "∀(x, m)∈clkp_set A. m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ" "collect_clkvt (trans_of A) ⊆ X" "finite X" by (auto elim: valid_abstraction.cases) from *(1) u'(2) have "∀(x, m)∈collect_clock_pairs (inv_of A l). m ≤ real (k x) ∧ x ∈ X ∧ m ∈ ℕ" unfolding clkp_set_def collect_clki_def inv_of_def by fastforce from ccompatible[OF this, folded ℛ_def'] v'1(2) v'2 v'(1,2,3) R have 3: "[v']⇩ℛ ⊆ ⦃inv_of A l⦄" "([u]⇩ℛ) ⊆ ⦃inv_of A l⦄" unfolding ccompatible_def ccval_def by auto with A v'1 R(1) ℛ_def' have "A,ℛ ⊢ ⟨l, ([u]⇩ℛ)⟩ ↝ ⟨l,([v']⇩ℛ)⟩" by auto with valid_regions_distinct_spec[OF v'1(2) 1(1) v'2 1(3)] region_unique_spec[OF u'(2,4)] have step_r: "A,ℛ ⊢ ⟨l, R⟩ ↝ ⟨l, R'⟩" and 2: "[v']⇩ℛ = R'" "[u]⇩ℛ = R" by auto from set_of_regions_spec[OF u'(4,3)] v'1(1) 2 obtain t where t: "t ≥ 0" "[u' ⊕ t]⇩ℛ = R'" by auto with regions_closed'_spec[OF u'(4,3) this(1)] step_t_r(1) have *: "u' ⊕ t ∈ R'" by auto with t(1) 3 2 u'(1,3) have "A ⊢ ⟨l, u'⟩ → ⟨l, u' ⊕ t⟩" "u' ⊕ t ∈ ?W'" unfolding zone_delay_def ccval_def by auto with * 1(1) have "R' ⊆ Closure⇩_{α}?W'" unfolding cla_def by auto with 1(2) show "v ∈ Closure⇩_{α}?W'" .. qed moreover have "?W' ⊆ ?Z'" using ‹W ⊆ Z› unfolding zone_delay_def by auto ultimately show ?case by auto next case A: (step_a_z A l g a r l' Z) let ?Z' = "zone_set (Z ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}" let ?W' = "zone_set (W ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}" from ℛ_def have ℛ_def': "ℛ = {region X I r |I r. valid_region X k I r}" by simp from A(1) have step_z: "A ⊢ ⟨l, W⟩ ↝ ⟨l',?W'⟩" by auto moreover have "Closure⇩_{α}?Z' ⊆ Closure⇩_{α}?W'" proof fix v assume v: "v ∈ Closure⇩_{α}?Z'" then obtain R' v' where 1: "R' ∈ ℛ" "v ∈ R'" "v' ∈ R'" "v' ∈ ?Z'" unfolding cla_def by auto then obtain u where "u ∈ Z" and v': "v' = [r→0]u" "u ⊢ g" "v' ⊢ inv_of A l'" unfolding zone_set_def by blast let ?R'= "region_set' (([u]⇩ℛ) ∩ {u. u ⊢ g}) r 0 ∩ {u. u ⊢ inv_of A l'}" from ‹u ∈ Z› closure_subs[OF A(4)] A(2) obtain u' R where u': "u' ∈ W" "u ∈ R" "u' ∈ R" "R ∈ ℛ" unfolding cla_def by blast then have "∀x∈X. 0 ≤ u x" unfolding ℛ_def by fastforce from region_cover'[OF ℛ_def' this] have R: "[u]⇩ℛ ∈ ℛ" "u ∈ [u]⇩ℛ" by auto from step_r_complete_aux[OF ℛ_def' A(3) this(2,1) A(1) v'(2)] v' have *: "[u]⇩ℛ = ([u]⇩ℛ) ∩ {u. u ⊢ g}" "?R' = region_set' ([u]⇩ℛ) r 0" "?R' ∈ ℛ" by auto from ℛ_def' A(3) have "collect_clkvt (trans_of A) ⊆ X" "finite X" by (auto elim: valid_abstraction.cases) with A(1) have r: "set r ⊆ X" unfolding collect_clkvt_def by fastforce from * v'(1) R(2) have "v' ∈ ?R'" unfolding region_set'_def by auto moreover have "A,ℛ ⊢ ⟨l,([u]⇩ℛ)⟩ ↝ ⟨l',?R'⟩" using R(1) ℛ_def' A(1,3) v'(2) by auto thm valid_regions_distinct_spec with valid_regions_distinct_spec[OF *(3) 1(1) ‹v' ∈ ?R'› 1(3)] region_unique_spec[OF u'(2,4)] have 2: "?R' = R'" "[u]⇩ℛ = R" by auto with * u' have *: "[r→0]u' ∈ ?R'" "u' ⊢ g" "[r→0]u' ⊢ inv_of A l'" unfolding region_set'_def by auto with A(1) have "A ⊢ ⟨l, u'⟩ → ⟨l',[r→0]u'⟩" apply (intro step.intros(1)) apply rule by auto moreover from * u'(1) have "[r→0]u' ∈ ?W'" unfolding zone_set_def by auto ultimately have "R' ⊆ Closure⇩_{α}?W'" using *(1) 1(1) 2(1) unfolding cla_def by auto with 1(2) show "v ∈ Closure⇩_{α}?W'" .. qed moreover have "?W' ⊆ ?Z'" using ‹W ⊆ Z› unfolding zone_set_def by auto ultimately show ?case by meson qed lemma steps_z_alt: "A ⊢ ⟨l, Z⟩ ↝* ⟨l',Z'⟩ ⟹ A ⊢ ⟨l', Z'⟩ ↝ ⟨l'',Z''⟩ ⟹ A ⊢ ⟨l, Z⟩ ↝* ⟨l'',Z''⟩" by (induction rule: steps_z.induct) auto lemma steps_z_alpha_V: "A ⊢ ⟨l, Z⟩ ↝⇩_{α}* ⟨l',Z'⟩ ⟹ Z ⊆ V ⟹ Z' ⊆ V" apply (induction rule: steps_z_alpha.induct) using closure_V by auto lemma steps_z_alpha_closure_involutive': "A ⊢ ⟨l, Z⟩ ↝⇩_{α}* ⟨l',Z'⟩ ⟹ A ⊢ ⟨l', Z'⟩ ↝ ⟨l'',Z''⟩ ⟹ valid_abstraction A X k ⟹ Z ⊆ V ⟹ ∃ Z'''. A ⊢ ⟨l, Z⟩ ↝* ⟨l'',Z'''⟩ ∧ Closure⇩_{α}Z'' ⊆ Closure⇩_{α}Z''' ∧ Z''' ⊆ Z''" proof (induction A l Z l' Z' arbitrary: Z'' l'' rule: steps_z_alpha.induct, goal_cases) case refl from this(1) show ?case by blast next case A: (2 A l Z l' Z' l'' Z'' Z''a l''a) from A(3) obtain 𝒵 where Z'': "Z'' = Closure⇩_{α}𝒵" "A ⊢ ⟨l', Z'⟩ ↝ ⟨l'',𝒵⟩" by auto from A(2)[OF Z''(2) A(5,6)] obtain Z''' where Z''': "A ⊢ ⟨l, Z⟩ ↝* ⟨l'',Z'''⟩" "Closure⇩_{α}𝒵 ⊆ Closure⇩_{α}Z'''" "Z''' ⊆ 𝒵" by auto from closure_subs have *: "Z''' ⊆ Closure⇩_{α}𝒵" by (metis A(1,6) Z'''(3) Z''(2) step_z_V steps_z_alpha_V subset_trans) from A(4) Z'' have "A ⊢ ⟨l'', Closure⇩_{α}𝒵⟩ ↝ ⟨l''a,Z''a⟩" by auto from steps_z_alpha_closure_involutive'_aux'[OF this(1) _ A(5) closure_V *] Z'''(2,3) obtain W' where ***: "A ⊢ ⟨l'', Z'''⟩ ↝ ⟨l''a,W'⟩" "Closure⇩_{α}Z''a ⊆ Closure⇩_{α}W'" "W' ⊆ Z''a" by (auto simp: closure_involutive) with Z'''(1) have "A ⊢ ⟨l, Z⟩ ↝* ⟨l''a,W'⟩" by (blast intro: steps_z_alt) with ***(2,3) show ?case by blast qed text ‹Old proof using Bouyer's calculation› lemma steps_z_alpha_closure_involutive'': "A ⊢ ⟨l, Z⟩ ↝⇩_{α}* ⟨l',Z'⟩ ⟹ A ⊢ ⟨l', Z'⟩ ↝ ⟨l'',Z''⟩ ⟹ valid_abstraction A X k ⟹ Z ⊆ V ⟹ ∃ Z'''. A ⊢ ⟨l, Z⟩ ↝* ⟨l'',Z'''⟩ ∧ Closure⇩_{α}Z'' ⊆ Closure⇩_{α}Z'''" proof (induction A l Z l' Z' arbitrary: Z'' l'' rule: steps_z_alpha.induct, goal_cases) case refl from this(1) show ?case by blast next case A: (2 A l Z l' Z' l'' Z'' Z''a l''a) from A(3) obtain 𝒵 where Z'': "Z'' = Closure⇩_{α}𝒵" "A ⊢ ⟨l', Z'⟩ ↝ ⟨l'',𝒵⟩" by auto from A(2)[OF Z''(2) A(5,6)] obtain Z''' where Z''': "A ⊢ ⟨l, Z⟩ ↝* ⟨l'',Z'''⟩" "Closure⇩_{α}𝒵 ⊆ Closure⇩_{α}Z'''" by auto from steps_z_alpha_V[OF A(1,6)] step_z_V[OF Z''(2)] have *: "𝒵 ⊆ V" by blast from A Z'' have "A ⊢ ⟨l'', Closure⇩_{α}𝒵⟩ ↝ ⟨l''a,Z''a⟩" by auto from calc[OF A(5) * this] obtain 𝒵' where **: "A ⊢ ⟨l'', 𝒵⟩ ↝ ⟨l''a,𝒵'⟩" "Z''a ⊆ Closure⇩_{α}𝒵'" by auto from steps_z_alpha_closure_involutive'_aux[OF this(1) Z'''(2) A(5) *] obtain W' where ***: "A ⊢ ⟨l'', Z'''⟩ ↝ ⟨l''a,W'⟩" "Closure⇩_{α}𝒵' ⊆ Closure⇩_{α}W'" by auto with Z'''(1) have "A ⊢ ⟨l, Z⟩ ↝* ⟨l''a,W'⟩" by (blast intro: steps_z_alt) with closure_involutive'[OF **(2)] ***(2) show ?case by blast qed lemma steps_z_alpha_closure_involutive: "A ⊢ ⟨l, Z⟩ ↝⇩_{α}* ⟨l',Z'⟩ ⟹ valid_abstraction A X k ⟹ Z ⊆ V ⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝* ⟨l',Z''⟩ ∧ Closure⇩_{α}Z' ⊆ Closure⇩_{α}Z'' ∧ Z'' ⊆ Z'" proof (induction A l Z l' Z' rule: steps_z_alpha.induct) case refl show ?case by blast next case 2: (step A l Z l' Z' l'' Z'') then obtain Z''a where *: "A ⊢ ⟨l', Z'⟩ ↝ ⟨l'',Z''a⟩" "Z'' = Closure⇩_{α}Z''a" by auto from steps_z_alpha_closure_involutive'[OF 2(1) this(1) 2(4,5)] obtain Z''' where Z''': "A ⊢ ⟨l, Z⟩ ↝* ⟨l'',Z'''⟩" "Closure⇩_{α}Z''a ⊆ Closure⇩_{α}Z'''" "Z''' ⊆ Z''a" by blast have "Z''' ⊆ Z''" by (metis *(1,2) 2(1,5) Z'''(3) closure_subs step_z_V steps_z_alpha_V subset_trans) with * closure_involutive Z''' show ?case by auto qed lemma steps_z_V: "A ⊢ ⟨l, Z⟩ ↝* ⟨l',Z'⟩ ⟹ Z ⊆ V ⟹ Z' ⊆ V" apply (induction rule: steps_z.induct) apply blast using step_z_V by metis lemma steps_z_alpha_sound: "A ⊢ ⟨l, Z⟩ ↝⇩_{α}* ⟨l',Z'⟩ ⟹ valid_abstraction A X k ⟹ Z ⊆ V ⟹ Z' ≠ {} ⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝* ⟨l',Z''⟩ ∧ Z'' ≠ {} ∧ Z'' ⊆ Z'" proof goal_cases case 1 from steps_z_alpha_closure_involutive[OF 1(1-3)] obtain Z'' where Z'': "A ⊢ ⟨l, Z⟩ ↝* ⟨l',Z''⟩" "Closure⇩_{α}Z' ⊆ Closure⇩_{α}Z''" "Z'' ⊆ Z'" by blast with 1(4) cla_empty_iff[OF steps_z_alpha_V[OF 1(1)], OF 1(3)] cla_empty_iff[OF steps_z_V, OF this(1) 1(3)] have "Z'' ≠ {}" by auto with Z'' show ?case by auto qed lemma step_z_mono: "A ⊢ ⟨l, Z⟩ ↝ ⟨l',Z'⟩ ⟹ Z ⊆ W ⟹ ∃ W'. A ⊢ ⟨l, W⟩ ↝ ⟨l',W'⟩ ∧ Z' ⊆ W'" proof (cases rule: step_z.cases, assumption, goal_cases) case A: 1 let ?W' = "(W ∩ {u. u ⊢ inv_of A l})⇧^{↑}∩ {u. u ⊢ inv_of A l}" from A have "A ⊢ ⟨l, W⟩ ↝ ⟨l',?W'⟩" by auto moreover have "Z' ⊆ ?W'" apply (subst A(4)) apply (rule subset_int_mono) apply (rule zone_delay_mono) apply (rule subset_int_mono) apply (rule A(2)) done ultimately show ?thesis by auto next case A: (2 g a r) let ?W' = "zone_set (W ∩ {u. u ⊢ g}) r ∩ {u. u ⊢ inv_of A l'}" from A have "A ⊢ ⟨l, W⟩ ↝ ⟨l',?W'⟩" by auto moreover have "Z' ⊆ ?W'" apply (subst A(3)) apply (rule subset_int_mono) apply (rule zone_set_mono) apply (rule subset_int_mono) apply (rule A(2)) done ultimately show ?thesis by auto qed lemma step_z_alpha_mono: "A ⊢ ⟨l, Z⟩ ↝⇩_{α}⟨l',Z'⟩ ⟹ Z ⊆ W ⟹ W ⊆ V ⟹ ∃ W'. A ⊢ ⟨l, W⟩ ↝⇩_{α}⟨l',W'⟩ ∧ Z' ⊆ W'" proof goal_cases case 1 then obtain Z'' where *: "A ⊢ ⟨l, Z⟩ ↝ ⟨l',Z''⟩" "Z' = Closure⇩_{α}Z''" by auto from step_z_mono[OF this(1) 1(2)] obtain W' where "A ⊢ ⟨l, W⟩ ↝ ⟨l',W'⟩" "Z'' ⊆ W'" by auto moreover with *(2) have "Z' ⊆ Closure⇩_{α}W'" unfolding cla_def by auto ultimately show ?case by blast qed lemma steps_z_alpha_mono: "A ⊢ ⟨l, Z⟩ ↝⇩_{α}* ⟨l',Z'⟩ ⟹ Z ⊆ W ⟹ W ⊆ V ⟹ ∃ W'. A ⊢ ⟨l, W⟩ ↝⇩_{α}* ⟨l',W'⟩ ∧ Z' ⊆ W'" proof (induction rule: steps_z_alpha.induct, goal_cases) case refl then show ?case by auto next case (2 A l Z l' Z' l'' Z'') then obtain W' where "A ⊢ ⟨l, W⟩ ↝⇩_{α}* ⟨l',W'⟩" "Z' ⊆ W'" by auto with step_z_alpha_mono[OF 2(3) this(2) steps_z_alpha_V[OF this(1) 2(5)]] show ?case by blast qed lemma steps_z_alpha_alt: "A ⊢ ⟨l, Z⟩ ↝⇩_{α}⟨l', Z'⟩ ⟹ A ⊢ ⟨l', Z'⟩ ↝⇩_{α}* ⟨l'', Z''⟩ ⟹ A ⊢ ⟨l, Z⟩ ↝⇩_{α}* ⟨l'', Z''⟩" by (rotate_tac, induction rule: steps_z_alpha.induct) blast+ lemma steps_z_alpha_complete: "A ⊢ ⟨l, Z⟩ ↝* ⟨l',Z'⟩ ⟹ valid_abstraction A X k ⟹ Z ⊆ V ⟹ Z' ≠ {} ⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝⇩_{α}* ⟨l',Z''⟩ ∧ Z' ⊆ Z''" proof (induction rule: steps_z.induct, goal_cases) case refl with cla_empty_iff show ?case by blast next case (2 A l Z l' Z' l'' Z'') with step_z_V[OF this(1,5)] obtain Z''' where "A ⊢ ⟨l', Z'⟩ ↝⇩_{α}* ⟨l'',Z'''⟩" "Z'' ⊆ Z'''" by blast with steps_z_alpha_mono[OF this(1) closure_subs[OF step_z_V[OF 2(1,5)]] closure_V] obtain W' where W': "A ⊢ ⟨l', Closure⇩_{α}Z'⟩ ↝⇩_{α}* ⟨l'',W'⟩" " Z'' ⊆ W'" by auto with 2(1) have "A ⊢ ⟨l, Z⟩ ↝⇩_{α}* ⟨l'',W'⟩" by (auto intro: steps_z_alpha_alt) with W' show ?case by auto qed lemma steps_z_alpha_complete': "A ⊢ ⟨l, Z⟩ ↝* ⟨l',Z'⟩ ⟹ valid_abstraction A X k ⟹ Z ⊆ V ⟹ Z' ≠ {} ⟹ ∃ Z''. A ⊢ ⟨l, Z⟩ ↝⇩_{α}* ⟨l',Z''⟩ ∧ Z'' ≠ {}" using steps_z_alpha_complete by fast end end