theory Sepref_Additional imports Sepref_Basic begin lemma hoare_alt: "<P> c <λr. Q r > = (∀h as n. pHeap h as n ⊨ P ⟶ (∃h' t r. execute c h = Some (r, h', t) ∧ (pHeap h' (new_addrs h as h') (n - t) ⊨ Q r ∧ t ≤ n ∧ relH {a. a < heap.lim h ∧ a ∉ as} h h' ∧ heap.lim h ≤ heap.lim h')))" (is "?L = (∀h as n. ?H h as n ⟶ (∃h' t r. _ ∧ ?P h as h' n t r))") proof - have "?L = (∀h as n. pHeap h as n ⊨ P ⟶ (∀ σ t r. run c (Some h) σ r t ⟶ σ ≠ None ∧ (?P h as (the σ) n t r)))" unfolding hoare_triple_def by auto also have "… = (∀h as n. pHeap h as n ⊨ P ⟶ (∃h' t r. execute c h = Some (r, h', t) ∧ ?P h as h' n t r))" apply(subst run_and_execute) by simp finally show ?thesis . qed lemma extract_cost_otherway: assumes "Γ * timeCredit_assn Cost_lb ⟹⇩A G * F" "<G> c <λr. Q r >" "⋀r. Q r * F ⟹⇩A Γ' * (∃⇩Ara. R ra r * ↑(ra ∈ dom M)) * true" "(⋀c. c∈ran M ⟹ Cost_lb ≤ c)" shows "hn_refine Γ c Γ' R (REST M)" proof - note pre_rule[OF assms(1) frame_rule[OF assms(2)]] then have TR: "⋀h as n. pHeap h as n ⊨ Γ * timeCredit_assn Cost_lb ⟹ (∃h' t r. execute c h = Some (r, h', t) ∧ pHeap h' (new_addrs h as h') (n - t) ⊨ Q r * F ∧ t ≤ n ∧ relH {a. a < heap.lim h ∧ a ∉ as} h h' ∧ heap.lim h ≤ heap.lim h')" unfolding hoare_alt by simp show ?thesis unfolding hn_refine_def apply auto proof - fix h as n assume "pHeap h as n ⊨ Γ" then have "pHeap h as (n+Cost_lb) ⊨ Γ * timeCredit_assn Cost_lb" by (simp add: mod_timeCredit_dest) from TR[OF this] obtain h' t r where "execute c h = Some (r, h', t)" and h: "pHeap h' (new_addrs h as h') (n + Cost_lb - t) ⊨ Q r * F" and 3: "t ≤ n + Cost_lb" "relH {a. a < heap.lim h ∧ a ∉ as} h h'" "heap.lim h ≤ heap.lim h'" by blast from h assms(3) have h': "pHeap h' (new_addrs h as h') (n + Cost_lb - t) ⊨ Γ' * (∃⇩Ara. R ra r * ↑ (ra ∈ dom M)) * true" by (simp add: entails_def) then have "∃ra. pHeap h' (new_addrs h as h') (n + Cost_lb - t) ⊨ Γ' * R ra r * ↑ (ra ∈ dom M) * true" by simp then obtain ra where h'': "pHeap h' (new_addrs h as h') (n + Cost_lb - t) ⊨ Γ' * R ra r * ↑ (ra ∈ dom M) * true" by blast have "pHeap h' (new_addrs h as h') (n + Cost_lb - t) ⊨ (Γ' * R ra r * true) * ↑ (ra ∈ dom M)" apply(rule entailsD[OF _ h'']) by (simp add: entails_triv move_back_pure') then have h'': "pHeap h' (new_addrs h as h') (n + Cost_lb - t) ⊨ Γ' * R ra r * true" and radom: "ra ∈ dom M" using mod_pure_star_dist by auto show "∃h' t r. execute c h = Some (r, h', t) ∧ (∃ra Ca. Some (enat Ca) ≤ M ra ∧ t ≤ n + Ca ∧ pHeap h' (new_addrs h as h') (n + Ca - t) ⊨ Γ' * R ra r * true) ∧ relH {a. a < heap.lim h ∧ a ∉ as} h h' ∧ heap.lim h ≤ heap.lim h'" apply(rule exI[where x=h']) apply(rule exI[where x=t]) apply(rule exI[where x=r]) apply safe apply fact apply(rule exI[where x=ra]) apply(rule exI[where x=Cost_lb]) apply safe subgoal using assms(4) radom using ranI by force subgoal by fact subgoal using h'' mod_star_trueI by blast apply fact apply fact done qed qed lemma extract_cost_otherway': fixes R assumes "Γ * timeCredit_assn Cost_lb ⟹⇩A G * F" "⋀h. h⊨Γ ⟹ <G> c <λr. Q r >" "⋀r h. h⊨Γ ⟹ Q r * F ⟹⇩A Γ' * (∃⇩Ara. R ra r * ↑(ra ∈ dom M)) * true" "(⋀c h. h⊨Γ ⟹ c∈ran M ⟹ Cost_lb ≤ c)" shows "hn_refine Γ c Γ' R (REST M)" apply(rule hn_refine_preI) apply(rule extract_cost_otherway) using assms by auto subsection "how to extract a hoare triple from hn_refine" lemma extract_cost_ub: assumes "hn_refine Γ c Γ' R (REST M)" "(⋀c. c∈ran M ⟹ c ≤ Cost_ub)" shows "<Γ * timeCredit_assn Cost_ub> c <λr. Γ' * (∃⇩Ara. R ra r * ↑(ra ∈ dom M)) >⇩t" using assms(1) unfolding hn_refine_def unfolding hoare_triple_def apply clarify proof (goal_cases) case (1 h as σ r n t) from 1(2) have 2: "pHeap h as (n-Cost_ub) ⊨ Γ" and nf: "n≥Cost_ub" using mod_timeCredit_dest by auto from 1(1) have 3: "⋀h as n Ma. pHeap h as n ⊨ Γ ⟹ SPECT M = SPECT Ma ⟹ (∃h' t r. execute c h = Some (r, h', t) ∧ (∃ra Ca. Ma ra ≥ Some (enat Ca) ∧ t ≤ n + Ca ∧ pHeap h' (new_addrs h as h') ((n + Ca) - t) ⊨ Γ' * R ra r * true) ∧ relH {a. a < heap.lim h ∧ a ∉ as} h h' ∧ heap.lim h ≤ heap.lim h')" by auto thm effect_deterministic from 3[OF 2 ] obtain h' t' r' where E: "execute c h = Some (r', h', t') " and R: "(∃ra Ca. M ra ≥ Some (enat Ca) ∧ pHeap h' (new_addrs h as h') (n - Cost_ub + Ca - t') ⊨ Γ' * R ra r' * true ∧ t' ≤ n - Cost_ub + Ca) ∧ relH {a. a < heap.lim h ∧ a ∉ as} h h' ∧ heap.lim h ≤ heap.lim h'" by blast have F: "σ = Some h'" and prime: "r' = r" "t' = t" using E 1(3) run.cases apply force using E 1(3) run.cases apply force using E 1(3) run.cases by force then have sig: "the σ = h'" by auto from R have B: "(∃ra Ca. M ra ≥ Some (enat Ca) ∧ pHeap (the σ) (new_addrs h as (the σ)) (n - Cost_ub + Ca - t) ⊨ Γ' * R ra r * true ∧ t ≤ n - Cost_ub + Ca )" and C: "relH {a. a < heap.lim h ∧ a ∉ as} h (the σ)" "heap.lim h ≤ heap.lim (the σ) " unfolding prime sig by auto from B obtain ra Ca where i: "pHeap (the σ) (new_addrs h as (the σ)) (n - Cost_ub + Ca - t) ⊨ Γ' * R ra r * true" and ii: "t ≤ n - Cost_ub + Ca" and ineq: "M ra ≥ Some (enat Ca)" using B by auto from ineq have radom: "ra ∈ dom M" using domIff by fastforce then obtain Mra where Mra: "M ra = Some Mra" by blast with assms(2) have "Mra ≤ enat Cost_ub" by (meson ranI) with Mra ineq have "Some (enat Ca) ≤ Some (enat Cost_ub)" using dual_order.trans by fastforce then have ie: "Ca ≤ Cost_ub" by auto have pr: "(n - Cost_ub + Ca - t) = (n - t) - (Cost_ub - Ca)" using ie ii nf by auto have pl: "(n - (t + (Cost_ub - Ca)) + (Cost_ub - Ca)) = n-t" using ii nf by auto have "pHeap (the σ) (new_addrs h as (the σ) ∪ {}) ((n - t) - (Cost_ub - Ca) + (Cost_ub - Ca)) ⊨ Γ' * R ra r * true * true" apply(rule mod_star_convI) apply simp apply(rule i[unfolded pr]) by (simp add: top_assn_rule) then have H: "pHeap (the σ) (new_addrs h as (the σ)) (n - t) ⊨ Γ' * R ra r * true * true" by (simp add: pl) have "pHeap (the σ) (new_addrs h as (the σ)) (n - t) ⊨ Γ' * R ra r * ↑ (ra ∈ dom M) * true" apply(rule entailsD[OF _ H]) using radom by auto2 then have "∃ra. pHeap (the σ) (new_addrs h as (the σ)) (n - t) ⊨ Γ' * R ra r * ↑ (ra ∈ dom M) * true" by blast then have H': "pHeap (the σ) (new_addrs h as (the σ)) (n - t) ⊨ (∃⇩Ara. Γ' * R ra r * ↑ (ra ∈ dom M) * true)" using mod_ex_dist by blast have H: "pHeap (the σ) (new_addrs h as (the σ)) (n - t) ⊨ Γ' * (∃⇩Ara. R ra r * ↑ (ra ∈ dom M)) * true" apply(rule entailsD[OF _ H']) by auto2 from ii ie nf have T: "t ≤ n " by auto show ?case apply safe subgoal using F by auto subgoal using H by simp subgoal by fact apply fact apply fact done qed lemma r: "ran (λv. if M v then Some (t v) else None) = {t v |v. M v}" by (auto simp: ran_is_image domIff split: if_splits) lemma d: "ra ∈ dom (λv. if M v then Some (t v) else None) ⟷ M ra" unfolding domIff by (auto) lemma extract_cost_ub_SPEC: "hn_refine Γ c Γ' R (SPEC M t) ⟹ (⋀c. M c ⟹ t c ≤ enat Cost_ub) ⟹ <Γ * timeCredit_assn Cost_ub> c <λr. Γ' * (∃⇩Ara. R ra r * ↑ (M ra))>⇩t" unfolding SPEC_def apply(drule extract_cost_ub[where Cost_ub=Cost_ub]) by (auto simp: r d) lemma hnr_hoare_triple_SPEC_conv: "hn_refine Γ c Γ' R (SPEC P (λ_. t)) = <Γ * timeCredit_assn t> c <λr. Γ' * (∃⇩Ara. R ra r * ↑ (P ra))>⇩t" apply(rule) subgoal apply(rule extract_cost_ub_SPEC) by auto subgoal unfolding SPEC_def apply(rule extract_cost_otherway[where Cost_lb="t" and F="emp"]) defer apply assumption apply (auto split: if_splits simp: domIff)[] apply solve_entails apply (auto split: if_splits simp: domIff)[] by(auto split: if_splits simp: ran_def) done lemma post_rulet: "<P> f <Q>⇩t ⟹ ∀x. Q x ⟹⇩A R x * true ⟹ <P> f <R>⇩t" apply(rule post_rule[where Q="λx. Q x * true"]) apply auto apply(rule ent_true_drop(1)) by simp lemma ht_cons_rule: assumes CPRE: "P ⟹⇩A P'" assumes CPOST: "⋀x. Q x ⟹⇩A Q' x" assumes R: "<P'> c <Q>" shows "<P> c <Q'>" apply(rule cons_post_rule[OF _ CPOST]) by(rule pre_rule[OF CPRE R]) lemma extract_cost_ub': assumes "hn_refine Γ c Γ' R (REST M)" "(⋀c. c∈ran M ⟹ c ≤ Cost_ub)" and pre: "P ⟹⇩A Γ * timeCredit_assn Cost_ub" and post: "∀r. Γ' * (∃⇩Ara. R ra r * ↑(ra ∈ dom M)) ⟹⇩A Q r * true" shows "<P> c <Q>⇩t" apply(rule pre_rule[OF pre]) apply(rule post_rulet[OF _ post]) apply(rule extract_cost_ub) by fact+ lemma hn_refineI: shows "tt = enat ttt ==> <Γ * timeCredit_assn ttt> C <λr. Γ' * RR ra r>⇩t ⟹ hn_refine Γ C Γ' RR (SPECT [ra ↦ tt])" apply(rule extract_cost_otherway[where F=emp and Cost_lb=ttt and G=" Γ * timeCredit_assn ttt"]) apply solve_entails apply simp apply simp apply solve_entails by simp lemma RETURNT_SPECT_conv: "RETURNT r = SPECT [r ↦ 0]" unfolding RETURNT_def by auto lemma hn_refineI0: shows "<Γ> C <λr. Γ' * RR ra r>⇩t ⟹ hn_refine Γ C Γ' RR (RETURNT ra)" unfolding RETURNT_SPECT_conv apply(rule extract_cost_otherway[where F=emp and Cost_lb=0 and G=" Γ * timeCredit_assn 0"]) apply solve_entails apply (simp add: zero_time) apply simp apply solve_entails by (simp add: zero_enat_def) end