Theory Sepref_Basic
section ‹Basic Definitions›
theory Sepref_Basic
imports
"../ds/LLVM_DS_NArray"
"HOL-Eisbach.Eisbach"
"Lib/Sepref_Misc"
"Lib/Structured_Apply"
"../nrest/NREST_Main"
Sepref_Id_Op
"../lib/More_Refine_Util"
begin
paragraph ‹Summary›
text ‹This theory introduces the synthesishn predicate and basic rules for it.›
paragraph ‹Main Theorems/Definitions›
text ‹
▪ hn_refine: the synthesise predicate hnr
▪ hnr_bind: the hnr rule for @{term bindT}
▪ ht_from_hnr: with this rule one can extract a Hoare Triple from a hnr with special form: the
running time may not depend on the result but only on the input parameters.
›
no_notation i_ANNOT (infixr ":::⇩i" 10)
no_notation CONST_INTF (infixr "::⇩i" 10)
no_notation pred_K ("⟨_⟩")
type_synonym assn = ll_assn
translations
(type) "assn" ↽ (type) "llvm_amemory × (char list, enat) acost ⇒ bool"
abbreviation (input) "RETURN ≡ RETURNT"
text ‹
In this theory, we define the basic concept of refinement
from a nondeterministic program specified in the
Isabelle Refinement Framework to an imperative deterministic one
specified in Imperative/HOL.
›
subsection {* Values on Heap *}
text ‹We tag every refinement assertion with the tag @{text hn_ctxt}, to
avoid higher-order unification problems when the refinement assertion
is schematic.›
definition hn_ctxt :: "('a⇒'c⇒assn) ⇒ 'a ⇒ 'c ⇒ assn"
where
"hn_ctxt P a c ≡ P a c"
definition pure :: "('b × 'a) set ⇒ 'a ⇒ 'b ⇒ assn"
where "pure R ≡ (λa c. ↑((c,a)∈R))"
lemma pure_app_eq: "pure R a c = ↑((c,a)∈R)" by (auto simp: pure_def)
lemma pure_eq_conv[simp]: "pure R = pure R' ⟷ R=R'"
unfolding pure_def
apply (rule iffI)
apply safe
apply (meson pure_assn_eq_conv)
apply (meson pure_assn_eq_conv)
done
lemma pure_rel_eq_false_iff: "pure R x y = sep_false ⟷ (y,x)∉R"
by (auto simp: pure_def sep_algebra_simps)
lemma pure_part_pure[simp]: "pure_part (pure R a c) ⟷ (c,a)∈R"
by (simp add: pure_app_eq)
definition is_pure :: "(_ ⇒ _ ⇒ assn) ⇒ bool" where "is_pure P ≡ ∃P'. ∀x x'. P x x'=↑(P' x x')"
lemma is_pureI[intro?]:
assumes "⋀x x'. P x x' = ↑(P' x x')"
shows "is_pure P"
using assms unfolding is_pure_def by blast
lemma is_pureE:
assumes "is_pure P"
obtains P' where "⋀x x'. P x x' = ↑(P' x x')"
using assms unfolding is_pure_def by blast
lemma pure_pure[simp]: "is_pure (pure P)"
unfolding pure_def by rule blast
lemma pure_hn_ctxt[intro!]: "is_pure P ⟹ is_pure (hn_ctxt P)"
unfolding hn_ctxt_def[abs_def] .
definition the_pure :: "('b ⇒ 'a ⇒ assn) ⇒ ('a × 'b) set"
where "the_pure P ≡ THE P'. ∀x x'. P x x'=↑((x',x)∈P')"
lemma the_pure_pure[simp]: "the_pure (pure R) = R"
unfolding pure_def the_pure_def
by (rule theI2[where a=R]) auto
lemma is_pure_alt_def: "is_pure R ⟷ (∃Ri. ∀x y. R x y = ↑((y,x)∈Ri))"
unfolding is_pure_def
apply auto
apply (rename_tac P')
apply (rule_tac x="{(x,y). P' y x}" in exI)
apply auto
done
lemma pure_the_pure[simp]: "is_pure R ⟹ pure (the_pure R) = R"
unfolding is_pure_alt_def pure_def the_pure_def
apply (intro ext)
apply clarsimp
apply (rename_tac a c Ri)
apply (rule_tac a=Ri in theI2)
apply auto
done
lemma is_pure_conv: "is_pure R ⟷ (∃R'. R = pure R')"
unfolding pure_def is_pure_alt_def by force
lemma is_pure_the_pure_id_eq[simp]: "is_pure R ⟹ the_pure R = Id ⟷ R=pure Id"
by (auto simp: is_pure_conv)
lemma is_pure_iff_pure_assn: "is_pure P = (∀x x'. sep_is_pure_assn (P x x'))"
unfolding is_pure_def
apply (rule iffI)
apply auto []
apply (rule exI[where x="λa c. pure_part (P a c)"])
apply auto
done
abbreviation "hn_val R ≡ hn_ctxt (pure R)"
lemma hn_val_unfold: "hn_val R a b = ↑((b,a)∈R)"
by (simp add: hn_ctxt_def pure_def)
definition "invalid_assn R x y ≡ ↑(pure_part (R x y))"
abbreviation "hn_invalid R ≡ hn_ctxt (invalid_assn R)"
lemma invalidate_clone: "R x y = (invalid_assn R x y ** R x y)"
unfolding invalid_assn_def
by (metis (mono_tags, lifting) pure_partI pure_part_pure_eq pure_part_split_conj pure_true_conv sep.add.right_neutral sep_conj_commute sep_is_pure_assn_def)
lemma invalidate_clone': "hn_ctxt R x y = (hn_invalid R x y ** hn_ctxt R x y)"
unfolding hn_ctxt_def using invalidate_clone .
lemma invalid_pure_recover: "invalid_assn (pure R) x y = pure R x y"
unfolding invalid_assn_def pure_def by auto
lemma hn_invalidI: "hn_ctxt P x y s ⟹ hn_invalid P x y = □"
by (auto simp: invalid_assn_def hn_ctxt_def pure_partI pure_true_conv)
lemma invalid_assn_cong[cong]:
assumes "x≡x'"
assumes "y≡y'"
assumes "R x' y' ≡ R' x' y'"
shows "invalid_assn R x y = invalid_assn R' x' y'"
using assms unfolding invalid_assn_def
by simp
subsection ‹Constraints in Refinement Relations›
definition rdomp :: "('a ⇒ 'c ⇒ assn) ⇒ 'a ⇒ bool" where
"rdomp R a ≡ ∃h c. R a c h"
lemma rdomp_ctxt[simp]: "rdomp (hn_ctxt R) = rdomp R"
by (simp add: hn_ctxt_def[abs_def])
lemma rdomp_pure[simp]: "rdomp (pure R) a ⟷ a∈Range R"
unfolding rdomp_def pure_def by (auto simp: pred_lift_extract_simps)
lemma rdomp_invalid_simp[simp]: "rdomp (invalid_assn P) x = rdomp P x"
by (auto simp: invalid_assn_def rdomp_def pure_part_def pred_lift_extract_simps)
lemma Range_of_constraint_conv[simp]: "Range (A∩UNIV×C) = Range A ∩ C"
by auto
subsection ‹Heap-Nres Refinement Calculus›
subsubsection ‹Definition of hnr›
text {* Predicate that expresses refinement. Given a heap
@{text "Γ"}, program @{text "c"} produces a heap @{text "Γ'"} and
a concrete result that is related with predicate @{text "R"} to some
abstract result from @{text "m"}*}
definition "hn_refine Γ c Γ' R m ≡
nofailT m ⟶
(∀F s cr M. m = REST M ⟶
llSTATE (Γ ∧* F) (s,cr) ⟶
(∃ra Ca. M ra ≥ Some Ca
∧ wp c (λr. llSTATE (Γ' ∧* R ra r ∧* F ∧* GC)) (s, cr+Ca)
)
)"
lemma STATE_alt: "STATE α P = (λs. P (α s))"
by(auto simp: STATE_def)
lemma "hn_refine Γ c Γ' R m = (
nofailT m ⟶
(∀F s cr M. m = REST M ⟶
(Γ ∧* F) (llvm_α s,cr) ⟶
(∃ra Ca. M ra ≥ Some Ca
∧ wp c (λr (s',cr'). (Γ' ∧* R ra r ∧* F ∧* GC) (llvm_α s',cr')) (s, cr+Ca)
)
))"
unfolding hn_refine_def STATE_alt lift_α_cost_def ll_α_def
apply (simp split: prod.splits)
by (smt case_prodD case_prodI2 wp_monoI)
subsubsection ‹Hnr Rules›
lemma hn_refine_extract_pre_val:
"hn_refine (hn_val S xa xc ** Γ) c Γ' R m ⟷ ((xc,xa)∈S ⟶ hn_refine Γ c Γ' R m)"
unfolding hn_refine_def hn_ctxt_def pure_def
by (auto simp: STATE_def sep_algebra_simps pred_lift_extract_simps htriple_extract_pre_pure)
lemma hn_refineI_SPECT:
assumes "llvm_htriple ($t ** Γ) c (λr. Γ' ** R x r)"
shows "hn_refine Γ c Γ' R (SPECT [x↦t])"
apply (auto simp add: hn_refine_def STATE_alt)
apply(rule exI[where x="t"]) apply simp
proof (goal_cases)
fix F s cr
assume "(Γ ** F) (ll_α (s, cr))"
then have "((Γ ** F) ** $(t)) (ll_α (s, cr + t))"
unfolding lift_α_cost_def ll_α_def
apply(rule sep_conjI[where y="(0,t)"])
subgoal by(simp add: time_credits_assn_def sep_algebra_simps)
subgoal by(simp add: sep_disj_enat_def sep_disj_acost_def sep_algebra_simps)
subgoal by(simp add: sep_disj_enat_def sep_disj_acost_def sep_algebra_simps)
done
then have "(($t ∧* Γ) ∧* F) (ll_α (s, cr + t))"
by (simp add: sep_conj_c)
from assms[unfolded htriple_def, rule_format, OF this]
show "wp c (λr s. (Γ' ∧* R x r ∧* F ∧* GC) (ll_α s)) (s, cr + t)"
by (simp add: sep_algebra_simps sep_conj_c)
qed
lemma hn_refineI':
assumes "llvm_htriple Γ c (λr. Γ' ** R x r)"
shows "hn_refine Γ c Γ' R (RETURNT x)"
apply (auto simp add: hn_refine_def STATE_alt)
apply(rule exI[where x=0]) apply simp
using assms unfolding htriple_def
by (simp add: sep_conj_c)
lemma hn_refineI'':
assumes "Φ ⟹ llvm_htriple Γ c (λr. Γ' ** R x r)"
shows "hn_refine Γ c Γ' R (doN { _ ← ASSERT Φ; RETURNT x })"
apply (auto simp add: hn_refine_def STATE_alt ASSERT_def iASSERT_def)
apply(rule exI[where x=0]) apply simp
using assms unfolding htriple_def
by (simp add: sep_conj_c)
lemma hn_refineI[intro]:
assumes "⋀F s cr M. ⟦ m = REST M; (Γ**F) (ll_α(s,cr)) ⟧
⟹ (∃ra Ca. M ra ≥ Some Ca ∧
(wp c (λr s. (Γ' ** R ra r ** F ** GC) (ll_α s)) (s,cr+Ca)))"
shows "hn_refine Γ c Γ' R m"
apply (auto simp add: hn_refine_def STATE_alt)
apply(rule assms) by auto
lemma hnr_vcgI_aux:
assumes "⋀F s cr M. ⟦ m = REST M; llSTATE (Γ**F) (s,cr) ⟧
⟹ (∃ra Ca. M ra ≥ Some Ca ∧
EXTRACT (wp c (λr. POSTCOND ll_α (Γ' ** R ra r ** F ** GC)) (s,cr+Ca)))"
shows "hn_refine Γ c Γ' R m"
using assms by (simp add: hn_refine_def vcg_tag_defs)
lemma hnr_vcg_aux1:
"P (s, cr) ⟹ (P ∧* $Ca) (s, cr + Ca)"
apply(rule sep_conjI[where y="(0,Ca)"])
apply (simp_all add: time_credits_assn_def sep_disj_prod_def sep_algebra_simps)
by (auto simp add: sep_disj_acost_def sep_disj_enat_def sep_algebra_simps)
lemma hnr_vcg_aux2:
"(P ∧* $(lift_acost Ca)) (s, cr + (lift_acost Ca)) ⟹ P (s, cr)"
apply(drule sep_conjD) apply (auto simp: lift_acost_def time_credits_assn_def sep_algebra_simps)
by (metis add.commute cost_ecost_add_minus_cancel lift_acost_def)
lemma hnr_vcgI:
assumes "⋀F s cr M. ⟦ m = REST M ⟧
⟹ (∃ra Ca. (llSTATE (Γ**F**$(lift_acost Ca)) (s,cr+(lift_acost Ca)) ⟶ (M ra ≥ Some (lift_acost Ca) ∧
EXTRACT (wp c (λr. POSTCOND ll_α (Γ' ** R ra r ** F ** GC)) (s,cr+lift_acost Ca)))))"
shows "hn_refine Γ c Γ' R m"
apply(rule hnr_vcgI_aux)
subgoal premises prems for F s cr M
using assms[OF prems(1), where F=F and s=s and cr=cr] apply -
apply(elim exE)
subgoal for ra Ca apply(rule exI[where x=ra])
apply(rule exI[where x="lift_acost Ca"])
apply(erule mp)
using prems(2)
unfolding STATE_def ll_α_def lift_α_cost_def apply simp
apply(rule hnr_vcg_aux1[of "(Γ ∧* F)", simplified]) .
done
done
lemma hn_refine_consume_return:
"hn_refine Γ c Γ' R m =
nofailT m ⟶
(∀F s cr .
llSTATE (Γ ∧* F) (s,cr) ⟶
(∃ra Ca. consume (RETURNT ra) Ca ≤ m
∧ wp c (λr. llSTATE (Γ' ∧* R ra r ∧* F ∧* GC)) (s, cr+Ca)
)
)"
unfolding hn_refine_def
apply auto
apply(cases m)
apply auto
subgoal premises p for F x cr x2
using p(2)[rule_format, OF p(1)]
apply safe
subgoal for ra Ca
apply(rule exI[where x=ra])
apply(rule exI[where x=Ca])
unfolding consume_def RETURNT_def apply simp
by (auto simp: le_fun_def)
done
done
lemma hn_refineD:
assumes "hn_refine Γ c Γ' R m"
assumes "m = REST M" "(Γ ∧* F) (ll_α (s,cr))"
shows "(∃ra Ca. M ra ≥ Some Ca
∧ wp c (λr s. (Γ' ∧* R ra r ∧* F ∧* GC) (ll_α s)) (s, cr+Ca)
)"
using assms by(auto simp: hn_refine_def STATE_alt nofailT_def)
lemma hn_refine_preI:
assumes "⋀h. Γ h ⟹ hn_refine Γ c Γ' R a"
shows "hn_refine Γ c Γ' R a"
apply(rule hn_refineI)
using sep_conjD assms hn_refineD by blast
lemma hn_refine_nofailI:
assumes "nofailT a ⟹ hn_refine Γ c Γ' R a"
shows "hn_refine Γ c Γ' R a"
using assms by (auto simp: hn_refine_def)
lemma hn_refine_false[simp]: "hn_refine sep_false c Γ' R m"
by rule auto
lemma hnr_FAIL[simp, intro!]: "hn_refine Γ c Γ' R FAILT"
by rule auto
thm sep_conj_impl1 wp_monoI frame_rule
lemma STATE_rev_mp: "STATE α P s ⟹ P⊢P' ⟹ STATE α P' s"
unfolding STATE_def entails_def by blast
lemma wp_post_cons: "wp m (λr. STATE α (Q r)) s ⟹ (⋀r. Q r ⊢ Q' r) ⟹ wp m (λr. STATE α (Q' r)) s"
by (simp add: STATE_rev_mp wp_monoI)
lemma hn_refine_cons_complete:
assumes R: "hn_refine P' c Q R m"
assumes I: "P⊢P'"
assumes I': "Q⊢Q'"
assumes R': "⋀x y. R x y ⊢ R' x y"
assumes LE: "m≤m'"
shows "hn_refine P c Q' R' m'"
unfolding hn_refine_def
apply clarify
using LE apply (cases m; simp)
apply (drule STATE_rev_mp)
apply (sep_drule I; rule entails_refl)
apply (frule (1) R[unfolded hn_refine_def, rule_format, rotated])
apply simp
apply (elim exE conjE)
apply (intro exI conjI)
apply (rule order_trans, assumption, erule le_funD)
apply (erule wp_post_cons)
apply (sep_drule I')
apply (sep_drule R')
apply (rule ENTAILSD)
apply fri
done
lemmas hn_refine_cons = hn_refine_cons_complete[OF _ _ _ _ order_refl]
lemmas hn_refine_cons_pre = hn_refine_cons_complete[OF _ _ entails_refl entails_refl order_refl]
lemmas hn_refine_cons_post = hn_refine_cons_complete[OF _ entails_refl _ entails_refl order_refl]
lemmas hn_refine_cons_res = hn_refine_cons_complete[OF _ entails_refl entails_refl _ order_refl]
lemmas hn_refine_ref = hn_refine_cons_complete[OF _ entails_refl entails_refl entails_refl]
lemma zz: "(P ∧* Q) s ⟹ P ⊢ P' ** F ⟹ (P' ** Q ** F) s"
unfolding entails_def
apply(subst (2) sep_conj_commute)
apply(subst sep_conj_assoc[symmetric])
apply (drule sep_conjD)
apply safe
apply(rule sep_conjI)
by(auto simp add: sep_algebra_simps )
thm frame_rule
lemma hn_refine_frame:
assumes hnr: "hn_refine P' c Q' R m"
assumes ent: "P ⊢ P' ** F"
shows "hn_refine P c (Q' ** F) R m"
apply (rule hn_refineI)
subgoal for Fa s cr M
apply(drule zz[OF _ ent])
apply(drule hnr[THEN hn_refineD, where F="Fa**F"])
apply simp
apply(auto simp add: sep_conj_aci sep_algebra_simps pred_lift_extract_simps)
done
done
lemma hn_refine_frame': "hn_refine Γ c Γ' R m ⟹ hn_refine (Γ**F) c (Γ'**F) R m"
by (simp add: hn_refine_frame)
lemma hn_refine_frame'': "hn_refine Γ c Γ' R m ⟹ hn_refine (F**Γ) c (F**Γ') R m"
using hn_refine_frame' sep_conj_c by smt
lemma hn_refine_augment_res:
assumes A: "hn_refine Γ f Γ' R g"
assumes B: "g ≤⇩n SPEC Φ t"
shows "hn_refine Γ f Γ' (λa c. R a c ** ↑(Φ a)) g"
apply (rule hn_refineI)
proof -
fix F s cr M
assume g: "g = SPECT M" and h:"(Γ ∧* F) (ll_α (s, cr))"
from A[THEN hn_refineD, OF this] obtain ra Ca
where s: "Some Ca ≤ M ra"
and w: "wp f (λr s. (Γ' ∧* R ra r ∧* F ∧* GC) (ll_α s)) (s, cr + Ca)"
by blast
from B g have "⋀x. M x ≤ (if Φ x then Some (t x) else None)"
by(auto simp: le_or_fail_def SPEC_def le_fun_def)
from this[of ra] have *: "Φ ra"
using s apply(auto split: if_splits simp: less_eq_option_None_is_None )
using less_eq_option_Some_None order.trans by blast
show "∃ra Ca.
Some Ca ≤ M ra ∧
wp f (λr s. (Γ' ∧* (R ra r ∧* ↑Φ ra) ∧* F ∧* GC) (ll_α s))
(s, cr + Ca)"
apply(rule exI[where x=ra])
apply(rule exI[where x=Ca])
apply safe
apply fact
apply(simp add: pure_def pred_lift_def * sep_algebra_simps)
by fact
qed
subsection ‹Product Types›
text ‹Some notion for product types is already defined here, as it is used
for currying and uncurrying, which is fundamental for the sepref tool›
definition prod_assn :: "('a1⇒'c1⇒assn) ⇒ ('a2⇒'c2⇒assn)
⇒ 'a1*'a2 ⇒ 'c1*'c2 ⇒ assn" where
"prod_assn P1 P2 a c ≡ case (a,c) of ((a1,a2),(c1,c2)) ⇒
P1 a1 c1 ** P2 a2 c2"
notation prod_assn (infixr "×⇩a" 70)
lemma prod_assn_pure_conv[simp]: "prod_assn (pure R1) (pure R2) = pure (R1 ×⇩r R2)"
by (auto simp: pure_def prod_assn_def pred_lift_extract_simps intro!: ext)
lemma prod_assn_pair_conv[simp]:
"prod_assn A B (a1,b1) (a2,b2) = (A a1 a2 ** B b1 b2)"
unfolding prod_assn_def by auto
lemma prod_assn_true[simp]: "prod_assn (λ_ _. sep_true) (λ_ _. sep_true) = (λ_ _. sep_true)"
by (auto intro!: ext simp: hn_ctxt_def prod_assn_def)
subsection "Convenience Lemmas"
lemma hn_refine_guessI:
assumes "hn_refine P f P' R f'"
assumes "f=f_conc"
shows "hn_refine P f_conc P' R f'"
using assms by simp
lemma imp_correctI:
assumes R: "hn_refine Γ c Γ' R a"
assumes C: "a ≤ SPECT (emb Φ T)"
shows "llvm_htriple (Γ ** $T) c (λr'. EXS r. Γ' ** R r r' ** ↑(Φ r))" oops
lemma hnr_pre_ex_conv:
shows "hn_refine (EXS x. Γ x) c Γ' R a ⟷ (∀x. hn_refine (Γ x) c Γ' R a)"
proof -
have *: "⋀x Γ F s cr. llSTATE (Γ x ∧* F) (s, cr) ⟹ llSTATE ((λs. ∃x. Γ x s) ∧* F) (s, cr)"
by (metis (no_types, lifting) STATE_def sep_conj_impl1)
have **: "⋀x Γ F s cr. llSTATE ((λs. ∃x. Γ x s) ∧* F) (s, cr) ⟹ ∃x. llSTATE (Γ x ∧* F) (s, cr)"
by (smt STATE_def sep_conjE sep_conjI)
show ?thesis
unfolding hn_refine_def
apply (safe; clarsimp?)
subgoal premises prems for x F s cr
using prems(1)[rule_format] *[of Γ, OF prems(3)] by blast
subgoal premises prems for x F s cr
using prems(1)[rule_format] **[of Γ, OF prems(3)] by blast
done
qed
lemma hnr_pre_pure_conv:
shows "hn_refine (↑P ** Γ) c Γ' R a ⟷ (P ⟶ hn_refine Γ c Γ' R a)"
unfolding hn_refine_def
apply (auto simp: sep_algebra_simps htriple_extract_pre_pure STATE_def)
using pred_lift_extract_simps(2) by blast
lemma hn_refine_split_post:
assumes "hn_refine Γ c Γ' R a"
shows "hn_refine Γ c (Γ' or Γ'') R a"
apply (rule hn_refine_cons_post[OF assms])
apply (auto simp: entails_def)
done
lemma hn_refine_post_other:
assumes "hn_refine Γ c Γ'' R a"
shows "hn_refine Γ c (Γ' or Γ'') R a"
apply (rule hn_refine_cons_post[OF assms])
apply (auto simp: entails_def)
done
subsubsection ‹Return›
lemma hnr_RETURN_pass:
"hn_refine (hn_ctxt R x p) (return p) (hn_invalid R x p) R (RETURNT x)"
apply (subst invalidate_clone')
unfolding hn_ctxt_def
apply(rule hnr_vcgI_aux)
apply(simp add: ecost_le_zero)
apply vcg
done
lemma hnr_RETURN_pure:
assumes "(c,a)∈R"
shows "hn_refine emp (return c) emp (pure R) (RETURNT a)"
apply(rule hnr_vcgI_aux) using assms
apply(simp add: ecost_le_zero)
supply [simp] = pure_def
by vcg
subsubsection ‹Assertion›
lemma hnr_ASSERT:
assumes "Φ ⟹ hn_refine Γ c Γ' R c'"
shows "hn_refine Γ c Γ' R (do { ASSERT Φ; c'})"
using assms
apply (cases Φ)
by auto
subsubsection ‹Bind›
lemma bind_det_aux:
fixes m :: "(_,(_,enat)acost) nrest"
shows "⟦ RETURN x ≤ m; RETURN y ≤ f x ⟧ ⟹ RETURN y ≤ m ⤜ f"
apply (rule order_trans[rotated])
apply (rule bindT_acost_mono')
apply assumption
apply (rule order_refl)
apply simp
done
definition "MK_FREE R f ≡ ∀a c. llvm_htriple (R a c) (f c) (λ_::unit. □)"
lemma MK_FREEI[intro?]: "⟦⋀a c. llvm_htriple (R a c) (f c) (λ_. □)⟧ ⟹ MK_FREE R f"
by (auto simp: MK_FREE_def)
lemma MK_FREED: "MK_FREE R f ⟹ llvm_htriple (R a c) (f c) (λ_. □)"
by (auto simp: MK_FREE_def)
lemma mk_free_pure: "MK_FREE (pure R) (λ_. return ())"
apply rule unfolding pure_def
by vcg
lemma mk_free_is_pure: "is_pure A ⟹ MK_FREE A (λ_. return ())"
apply rule unfolding pure_def is_pure_def
by vcg
lemma mk_free_invalid: "MK_FREE (invalid_assn R) (λ_. return ())"
apply rule unfolding invalid_assn_def
by vcg
lemma mk_free_pair:
assumes "MK_FREE R⇩1 f⇩1"
assumes "MK_FREE R⇩2 f⇩2"
shows "MK_FREE (R⇩1×⇩aR⇩2) (λ(c⇩1,c⇩2). doM {f⇩1 c⇩1; f⇩2 c⇩2})"
supply [vcg_rules] = assms[THEN MK_FREED]
apply (rule)
by vcg
lemma acost_plus_assoc: "a + (b + c) = (a + b) + (c::(char list, enat) acost)"
apply(cases a; cases b; cases c) by auto
lemma "le_cost_ecost c (cr + Ca) ⟹ le_cost_ecost c (cr + (Ca + Ca'))"
apply(simp add: acost_plus_assoc) apply(rule cost_ecost_add_increasing2) .
lemma hnr_bind:
assumes D1: "hn_refine Γ m' Γ1 Rh m"
assumes D2:
"⋀x x'. RETURNT x ≤ m ⟹ hn_refine (hn_ctxt Rh x x' ** Γ1) (f' x') (Γ2 x x') R (f x)"
assumes IMP: "⋀x x'. Γ2 x x' ⊢ hn_ctxt Rx x x' ** Γ'"
assumes MKF: "MK_FREE Rx fr"
shows "hn_refine Γ (doM {x←m'; r ← f' x; fr x; return r}) Γ' R (m⤜f)"
apply rule
supply [vcg_rules] = D1[THEN hn_refineD]
supply [simp] = pw_bindT_nofailT
proof goal_cases
case C: (1 F s cr M)
hence "nofailT (m ⤜ f)" by auto
hence nfm: "nofailT m" and nff: "⋀x t b. inresT (project_acost b m) x t ⟹ nofailT (f x)"
by (auto simp: g_pw_bindT_nofailT)
from nfm obtain Mm where M: "m = SPECT Mm" by fastforce
from D1[THEN hn_refineD, OF M C(2)] obtain ra Ca where Mra: "Some Ca ≤ Mm ra"
and wp1: "wp m' (λr s. (Γ1 ∧* Rh ra r ∧* F ∧* GC) (ll_α s)) (s, cr + Ca)"
by blast
term "(run m' s)"
from wp1[unfolded wp_def mwp_def] obtain s' r c
where mH: "(Γ1 ∧* Rh ra r ∧* F ∧* GC) (ll_α (s', minus_ecost_cost (cr + Ca) c))"
and mle: "le_cost_ecost c (cr + Ca)"
and r1: "run m' s = SUCC r c s'"
by (auto split: mres.splits)
from M Mra have ram: "RETURNT ra ≤ m" apply(auto simp: le_fun_def RETURNT_def)
by (simp add: dual_order.trans needname_nonneg)
have noff: "nofailT (f ra)" apply(rule nff[where t=0]) using Mra M unfolding inresT_def
by (metis RETURNT_alt ‹RETURNT ra ≤ m› project_acost_RETURNT pw_acost_le_project zero_enat_def)
then obtain fM where fMra: "f ra = SPECT fM" by fastforce
from mH have mH': "((Rh ra r ∧* Γ1) ∧* F ∧* GC) (ll_α (s', minus_ecost_cost (cr + Ca) c))"
by (simp add: sep_conj_c)
from D2[OF ram, THEN hn_refineD, OF fMra, of r, unfolded hn_ctxt_def, OF mH'] obtain ra' Ca'
where fMra': "Some Ca' ≤ fM ra'"
and wp2: "wp (f' r) (λrb s. (Γ2 ra r ∧* R ra' rb ∧* (F ∧* GC) ∧* GC) (ll_α s))
(s', minus_ecost_cost (cr + Ca) c + Ca')"
by blast
from wp2[unfolded wp_def mwp_def] obtain s'' r' c'
where mH2: "(Γ2 ra r ∧* R ra' r' ∧* F ∧* GC) (ll_α (s'', minus_ecost_cost (minus_ecost_cost (cr + Ca) c + Ca') c'))"
and mle2: "le_cost_ecost c' (minus_ecost_cost (cr + Ca) c + Ca')"
and r2: "run (f' r) s' = SUCC r' c' s''"
by (auto split: mres.splits)
from mH2 IMP have mH2': "(Rx ra r ∧* (Γ' ∧* R ra' r' ∧* F ∧* GC))
(ll_α (s'', minus_ecost_cost (minus_ecost_cost (cr + Ca) c + Ca') c'))"
by (smt entails_def hn_ctxt_def sep.mult_assoc sep_conj_impl1)
note wp3 = MKF[unfolded MK_FREE_def htriple_def, rule_format, OF mH2']
from wp3[unfolded wp_def mwp_def] obtain s''' r'' c''
where mH3: "(GC ∧* Γ' ∧* R ra' r' ∧* F ∧* GC) (ll_α (s''', minus_ecost_cost (minus_ecost_cost (minus_ecost_cost (cr + Ca) c + Ca') c') c''))"
and mle3: "le_cost_ecost c'' (minus_ecost_cost (minus_ecost_cost (cr + Ca) c + Ca') c')"
and r3: "run (fr r) s'' = SUCC r'' c'' s'''"
by (auto split: mres.splits)
from mH3 have mH3': "(Γ' ∧* R ra' r' ∧* F ∧* GC) (ll_α (s''', minus_ecost_cost (minus_ecost_cost (minus_ecost_cost (cr + Ca) c + Ca') c') c''))"
by (metis (no_types, lifting) GC_move_left(3) sep_conj_left_commute)
from Mra fMra' obtain Car Car' where PF: "Mm ra = Some Car" "fM ra' = Some Car'" by fastforce+
have "Some (Ca+Ca') ≤ Some (Car+Car')"
using PF Mra fMra' add_mono by fastforce
also
from C(1) fMra M have
"Some ((Car+Car')) ≤ M ra' "
unfolding bindT_def apply simp apply(drule nrest_Sup_SPECT_D[where x=ra'])
apply simp apply(rule Sup_upper) apply auto
apply(rule exI[where x="(map_option ((+) (Car)) ∘ fM)"])
using PF
apply simp apply(rule exI[where x=ra]) apply(rule exI[where x="Car"])
by auto
finally have "Some (Ca+Ca') ≤ M ra' " .
have **: "minus_ecost_cost (cr + Ca) c + Ca'
= minus_ecost_cost (cr + (Ca + Ca')) c"
using mle
by (simp add: acost_plus_assoc cost_ecost_minus_add_assoc2)
show ?case
apply(rule exI[where x=ra'])
apply(rule exI[where x="Ca+Ca'"])
apply safe
subgoal apply fact done
apply(simp add: wp_bind)
apply(subst wp_def) apply(subst mwp_def)
apply (simp add: r1)
apply(simp add: wp_bind)
apply(subst wp_def) apply(subst mwp_def)
apply (simp add: r2)
apply(simp add: wp_bind)
apply(subst wp_def) apply(subst mwp_def)
apply (simp add: r3)
apply(simp add: wp_return)
apply safe
subgoal using mH3' unfolding ** .
subgoal using mle3 unfolding ** .
subgoal using mle2 unfolding ** .
subgoal using mle apply(simp add: acost_plus_assoc) apply(rule cost_ecost_add_increasing2) .
done
qed
text ‹Version fro manual synthesis, if freeing of bound variable has been inserted manually›
lemma hnr_bind_manual_free:
fixes m' :: "_ llM"
assumes D1: "hn_refine Γ m' Γ1 Rh m"
assumes D2:
"⋀x x'. RETURN x ≤ m ⟹ hn_refine (hn_ctxt Rh x x' ** Γ1) (f' x') (Γ') R (f x)"
shows "hn_refine Γ (m'⤜f') Γ' R (m⤜f)"
apply(rule hnr_bind[OF D1 _ entails_refl, of f' "λx x'. hn_invalid Rh x x'" Γ' R f "λ_. return ()", simplified])
subgoal for x x' apply(subst invalidate_clone')
apply(drule D2[THEN hn_refine_frame'', where F=" (hn_invalid Rh) x x'", of _ x']) unfolding hn_ctxt_def using sep_conj_ac by smt
subgoal unfolding MK_FREE_def invalid_assn_def hn_ctxt_def by vcg
done
subsubsection ‹Recursion›
term "Monad.REC "
find_theorems "Monad.REC"
lemma hnr_RECT:
assumes S: "⋀cf af ax px. ⟦
⋀ax px. hn_refine (hn_ctxt Rx ax px ** F) (cf px) (F' ax px) Ry (af ax)⟧
⟹ hn_refine (hn_ctxt Rx ax px ** F) (cB cf px) (F' ax px) Ry (aB af ax)"
assumes M: "(⋀x. M.mono_body (λf. cB f x))"
shows "hn_refine
(hn_ctxt Rx ax px ** F) (Monad.REC cB px) (F' ax px) Ry (RECT aB ax)"
unfolding RECT_flat_gfp_def Monad.REC_def
proof (simp, intro conjI impI)
assume "mono2 aB"
hence "flatf_mono_ge aB" by (simp add: trimonoD_flatf_ge)
have "∀ax px.
hn_refine (hn_ctxt Rx ax px ** F) (M.fixp_fun cB px) (F' ax px) Ry
(flatf_gfp aB ax)"
apply (rule flatf_ord.fixp_induct[OF _ ‹flatf_mono_ge aB›])
apply (rule flatf_admissible_pointwise)
apply simp
apply (auto simp: hn_refine_def) []
apply clarsimp
apply (subst M.mono_body_fixp[of cB, OF M])
apply (rule S)
apply blast
done
thus "hn_refine (hn_ctxt Rx ax px ** F) (M.fixp_fun cB px) (F' ax px) Ry (flatf_gfp aB ax)"
by simp
qed
subsubsection ‹Merging›
definition "MERGE Γ1 f1 Γ2 f2 Γ' ≡ llvm_htriple Γ1 f1 (λ_. Γ') ∧ llvm_htriple Γ2 f2 (λ_. Γ')"
lemma MERGED:
assumes "MERGE Γ1 f1 Γ2 f2 Γ'"
shows "llvm_htriple Γ1 f1 (λ_. Γ')" "llvm_htriple Γ2 f2 (λ_. Γ')"
using assms by (auto simp: MERGE_def)
lemma MERGEI[intro?]:
assumes "llvm_htriple Γ1 f1 (λ_. Γ')" "llvm_htriple Γ2 f2 (λ_. Γ')"
shows "MERGE Γ1 f1 Γ2 f2 Γ'"
using assms by (auto simp: MERGE_def)
definition "MERGE1 R1 f1 R2 f2 R' ≡ ∀ a c. MERGE (R1 a c) (f1 c) (R2 a c) (f2 c) (R' a c)"
lemma MERGE1I[intro?]:
assumes "⋀a c. llvm_htriple (R1 a c) (f1 c) (λ_. R' a c)"
and "⋀a c. llvm_htriple (R2 a c) (f2 c) (λ_. R' a c)"
shows "MERGE1 R1 f1 R2 f2 R'"
using assms by (auto simp: MERGE1_def MERGE_def)
lemma MERGE1D:
assumes "MERGE1 R1 f1 R2 f2 R'"
shows "⋀a c. llvm_htriple (R1 a c) (f1 c) (λ_. R' a c)"
and "⋀a c. llvm_htriple (R2 a c) (f2 c) (λ_. R' a c)"
using assms by (auto simp: MERGE1_def MERGE_def)
lemma MERGE_STAR:
assumes "MERGE1 R1 f1 R2 f2 R'" "MERGE Γ1 fs1 Γ2 fs2 Γ'"
shows "MERGE (hn_ctxt R1 a c ** Γ1) (doM {f1 c;fs1}) (hn_ctxt R2 a c ** Γ2) (doM {f2 c;fs2}) (hn_ctxt R' a c ** Γ')"
proof -
note [vcg_rules] = MERGE1D[OF assms(1)] MERGED[OF assms(2)]
show ?thesis unfolding hn_ctxt_def by rule vcg
qed
lemma MERGE_triv: "MERGE Γ (return ()) Γ (return ()) Γ"
apply (rule) unfolding FRI_END_def by vcg
lemma MERGE_END: "MERGE FRI_END (return ()) FRI_END (return ()) □"
apply (rule) unfolding FRI_END_def by vcg
lemma MERGE1_eq: "MERGE1 P (λ_. return ()) P (λ_. return ()) P"
by rule vcg
lemma MERGE1_invalids:
assumes "MK_FREE R f"
shows "MERGE1 (invalid_assn R) (λ_. return ()) R f (invalid_assn R)" (is ?left)
and "MERGE1 R f (invalid_assn R) (λ_. return ()) (invalid_assn R)" (is ?right)
proof -
note [vcg_rules] = MK_FREED[OF assms]
show ?left
apply rule
apply vcg []
apply (subst invalidate_clone[of R])
unfolding invalid_assn_def
by vcg
show ?right
apply rule
apply (subst invalidate_clone[of R])
unfolding invalid_assn_def
by vcg
qed
subsubsection ‹Extracting a Hoare Triple from a HNR rule›
lemma ht_from_hnr:
assumes "hn_refine Γ c Γ' R (timerefine E (do {_ ← ASSERT Φ; SPECT (emb Q T) }))"
and "Φ"
shows " llvm_htriple ($(timerefineA E T) ** Γ) c (λr. (EXS ra. ↑(Q ra) ** R ra r) ** Γ')"
proof -
from assms(1)[unfolded hn_refine_def]
have *: "⋀F s cr. llSTATE (Γ ∧* F) (s, cr) ⟹ (∃ra Ca. Some Ca ≤ (emb Q (timerefineA E T)) ra ∧ wp c (λr. llSTATE (Γ' ∧* R ra r ∧* F ∧* GC)) (s, cr + Ca))"
using assms(2) apply (simp add: nofailT_timerefine)
unfolding SPEC_REST_emb'_conv[symmetric]
apply (simp add: SPEC_timerefine_conv)
unfolding SPEC_REST_emb'_conv by auto
show ?thesis
unfolding htriple_def
apply safe
proof -
fix F a b
assume "(($timerefineA E T ∧* Γ) ∧* F) (ll_α (a, b))"
then have G:"($timerefineA E T ** (Γ ** F)) (ll_α (a, b))"
by(simp add: sep_conj_aci)
obtain b' where G':"(Γ ** F) (ll_α (a, b'))" and b: "b= b'+ (timerefineA E T)"
using G[THEN sep_conjD] apply (simp add: dollar_aux_conv )
unfolding ll_α_def lift_α_cost_def
apply auto
using c_simps(5) by blast
from *[unfolded STATE_def,OF G'] obtain ra Ca where
i: "Some Ca ≤ emb Q (timerefineA E T) ra"
and wp: "wp c (λr s. (Γ' ∧* R ra r ∧* F ∧* GC) (ll_α s)) (a, b' + Ca)"
by auto
from i have Q: "Q ra" unfolding emb'_def by (auto split: if_splits)
from i have "∃delta. (timerefineA E T) = delta + Ca"
apply(intro get_delta) by(auto simp: emb'_def split: if_splits)
then obtain delta where tet: "(timerefineA E T) = delta + Ca" by blast
have b_alt: "b = (b' + Ca) + delta"
unfolding b tet
by (simp add: add.commute c_simps(6))
show "wp c (λr s'. ((((λs. ∃x. (↑Q x ∧* R x r) s) ∧* Γ') ∧* GC) ∧* F) (ll_α s')) (a, b)"
unfolding b_alt
apply(rule wp_monoI)
apply(rule wp_time_mono)
apply(rule wp)
apply safe
apply auto
unfolding ll_α_def lift_α_cost_def
apply simp
proof -
fix r a cc'
assume l: "(Γ' ∧* R ra r ∧* F ∧* GC) (llvm_α a, cc') "
have "((Γ' ∧* R ra r ∧* F ∧* GC)∧* GC) ((llvm_α a, cc')+(0,delta))"
apply(rule sep_conjI[where y="(0,delta)"])
apply (rule l)
subgoal unfolding GC_def SND_def by auto
subgoal apply (auto simp: sep_disj_prod_def )
using sep_disj_acost_def sep_disj_enat_def by blast
apply simp
done
then have k: "((Γ' ∧* R ra r ∧* F ∧* GC)∧* GC) ((llvm_α a, cc'+delta))"
by(simp)
then have k': "(R ra r ** (Γ' ∧* GC ∧* F)) ((llvm_α a, cc'+delta))"
apply simp
by(simp add: sep_conj_aci)
have R: "R ra r ⊢ (λs. ∃x. (↑Q x ∧* R x r) s)"
using Q
by (smt entails_def pure_true_conv sep.add.right_neutral sep_conj_commute)
show "((λs. ∃x. (↑Q x ∧* R x r) s) ∧* (Γ' ∧* GC ∧* F)) (llvm_α a, cc' + delta)"
apply(rule entailsD[rotated])
apply(rule k')
apply(rule conj_entails_mono[OF R])
apply simp
done
qed
qed
qed
lemma llvm_htriple_more_time: "a≤b ⟹ llvm_htriple ($a ** F) c Q ⟹ llvm_htriple ($b ** F) c Q"
proof -
assume ll: "llvm_htriple ($a ** F) c Q"
assume p: "a≤b"
obtain c where "b=c+a"
using get_delta[OF p] by blast
then have *: "$b = ($a ** $c)"
by (simp add: add.commute time_credits_add)
show ?thesis
unfolding *
unfolding htriple_def
apply safe
subgoal for F h1 h2
apply(rule wp_monoI)
apply(rule ll[unfolded htriple_def, rule_format, where F="$c ** F"])
apply(simp add: sep_conj_aci )
apply simp
subgoal premises p for r x
apply(rule entailsD[rotated])
apply(rule p(2))
apply(rule conj_entails_mono)
apply simp
apply(simp only: sep_conj_assoc[symmetric])
apply(rule conj_entails_mono)
subgoal
by (metis consume_credits_fri_end_rule entails_eq_iff sep.add_ac(2))
subgoal by simp
done
done
done
qed
subsubsection ‹Payday: move Time Credits between Heap and Monadic Costs›
text ‹In the following we prove two rules that allow to move time credits in an hnr rule between
the pre-heap and the advertised costs in the abstract algorithm. ›
lemma hn_refine_pay_aux: "NREST.consume m t = SPECT M
⟹ ∃M'. m = SPECT M' ∧ M = (map_option ((+) t) ∘ M')"
unfolding consume_def apply(cases m) by auto
lemma hnr_vcg_aux4:
"P (s, cr) ⟹ ($Ca ∧* P) (s, cr + Ca)"
apply(rule sep_conjI[where x="(0,Ca)"])
apply (simp_all add: time_credits_assn_def sep_disj_prod_def sep_algebra_simps)
by (auto simp add: sep_disj_acost_def sep_disj_enat_def sep_algebra_simps)
lemma hnr_vcg_aux3:
"($Ca ∧* P) (s, cr) ⟹ ∃cr'. P (s, cr') ∧ cr=cr'+Ca"
apply(erule sep_conjE)
by (auto simp: time_credits_assn_def SND_def add.commute)
lemma hn_refine_payday_aux2:
fixes t:: ecost
shows "Some Ca ≤ m ⟹ Some (Ca + t) ≤ map_option ((+) t) m"
apply(cases m)
by( auto simp add: add.commute add_mono)
lemma hn_refine_payday_aux3:
fixes t:: ecost
shows "Some Ca ≤ map_option ((+) t) m ⟹ Ca ≥ t ∧ Some (Ca - t) ≤ m "
apply(cases m) apply auto
oops
text ‹Time Credits can always be pushed from the Heap to the advertised costs.›
lemma hn_refine_payday:
fixes m :: " ('d, (char list, enat) acost) nrest"
shows "hn_refine ($t ∧* Γ) c Γ' R m ⟹ hn_refine Γ c Γ' R (consume m t)"
unfolding hn_refine_def
apply auto
subgoal apply(cases m) by auto
subgoal premises p for F s cr M
using p(1)[THEN hn_refine_pay_aux]
apply safe
subgoal premises p2 for M'
using p(3)[rule_format, where s=s and cr="cr+t" and M=M', OF p2(1), unfolded ll_α_def lift_α_cost_def STATE_def,
simplified, OF p(2)[ unfolded ll_α_def lift_α_cost_def STATE_def, simplified, THEN hnr_vcg_aux4[where P="(Γ ∧* F)"]]]
apply safe
subgoal for ra Ca
apply(rule exI[where x="ra"])
apply(rule exI[where x="Ca+t"])
unfolding STATE_def ll_α_def lift_α_cost_def
by (simp add: hn_refine_payday_aux2 add.assoc add.commute add.left_commute)
done
done
done
lemma
fixes t:: nat
shows "Some Ca ≤ map_option ((+) t) m
⟹ Some (Ca - t) ≤ m"
by(cases m, auto)
lemma hn_refine_payday_reverse_aux1:
"Ca ≤ (lift_acost t) + (Ca - (lift_acost t))"
apply(cases t; cases Ca)
unfolding lift_acost_def minus_acost_alt less_eq_acost_def
apply auto
by (metis add.commute add_diff_assoc_enat linear needname_cancle)
lemma hn_refine_payday_reverse_aux2:
shows "Some Ca ≤ map_option ((+) (lift_acost t)) m
⟹ Some (Ca - (lift_acost t)) ≤ m"
apply(cases m, auto)
unfolding less_eq_acost_def lift_acost_def
apply(cases Ca; cases t) apply simp
by (metis (mono_tags, lifting) acost.sel add_diff_cancel_enat comp_apply drm_class.diff_right_mono enat.distinct(2) the_acost_propagate)
text ‹Time credits can be pulled from the advertised costs to the Heap if it is finite.›
lemma hn_refine_payday_reverse:
fixes m :: " ('d, (char list, enat) acost) nrest"
shows "hn_refine Γ c Γ' R (consume m (lift_acost t)) ⟹ hn_refine ($(lift_acost t) ∧* Γ) c Γ' R m"
unfolding hn_refine_def
apply auto
subgoal apply(cases m) by (auto simp: nofailT_consume)
subgoal premises p for F s cr M
using p(2)[unfolded ll_α_def lift_α_cost_def STATE_def, simplified, THEN hnr_vcg_aux3]
apply safe
subgoal premises p2 for cr'
using p(3)[rule_format, where s=s and cr="cr'" and M="(map_option ((+) (lift_acost t)) ∘ M)", unfolded ll_α_def lift_α_cost_def STATE_def,
simplified, OF _ p2(1)]
apply (simp add: consume_def)
apply safe
subgoal for ra Ca
apply(rule exI[where x="ra"])
apply(rule exI[where x="Ca-(lift_acost t)"])
apply(frule hn_refine_payday_reverse_aux2)
apply simp
using p2(2)
unfolding STATE_def ll_α_def lift_α_cost_def
apply (auto simp add: hn_refine_payday_aux2 add.assoc add.commute add.left_commute)
using get_delta[OF hn_refine_payday_reverse_aux1, of t Ca]
apply safe
subgoal premises p for delta
using p(2)[THEN wp_time_mono, where d=delta]
apply(subst p(5))
apply(rule wp_monoI)
apply (simp add: add.assoc add.commute add.left_commute)
apply auto
subgoal premises p2 for r a cc'
apply (rule entailsD)
defer
apply(rule p2(2)[THEN hnr_vcg_aux4[where P="(Γ' ∧* R ra r ∧* F ∧* GC)" and Ca=delta and s="llvm_α a" and cr=cc']])
apply(rule entails_trans)
apply(rule conj_entails_mono)
apply(rule entails_GC)
apply(rule entails_refl)
apply (rule ENTAILSD)
apply fri
done
done
done
done
done
done
subsection ‹ML-Level Utilities›
ML ‹
signature SEPREF_BASIC = sig
val dest_lambda_rc: Proof.context -> term -> ((term * (term -> term)) * Proof.context)
val apply_under_lambda: (Proof.context -> term -> term) -> Proof.context -> term -> term
val is_nresT: typ -> bool
val mk_nresT: typ -> typ
val dest_nresT: typ -> typ
val mk_cequals: cterm * cterm -> cterm
val mk_entails: term * term -> term
val constrain_type_pre: typ -> term -> term
val mk_pair_in_pre: term -> term -> term -> term
val mk_compN_pre: int -> term -> term -> term
val mk_curry0_pre: term -> term
val mk_curry_pre: term -> term
val mk_curryN_pre: int -> term -> term
val mk_uncurry0_pre: term -> term
val mk_uncurry_pre: term -> term
val mk_uncurryN_pre: int -> term -> term
val hn_refine_conv: conv -> conv -> conv -> conv -> conv -> conv
val hn_refine_conv_a: conv -> conv
val hn_refine_concl_conv_a: (Proof.context -> conv) -> Proof.context -> conv
val dest_hn_refine: term -> term * term * term * term * term
val mk_hn_refine: term * term * term * term * term -> term
val is_hn_refine_concl: term -> bool
val dest_hnr_absfun: term -> bool * (term * term list)
val star_permute_tac: Proof.context -> tactic
val mk_star: term * term -> term
val list_star: term list -> term
val strip_star: term -> term list
val is_true: term -> bool
val is_hn_ctxt: term -> bool
val dest_hn_ctxt: term -> term * term * term
val dest_hn_ctxt_opt: term -> (term * term * term) option
type phases_ctrl = {
trace: bool,
trace_goals: bool,
int_res: bool,
start: string option,
stop: string option
}
val dflt_phases_ctrl: phases_ctrl
val dbg_phases_ctrl: phases_ctrl
val full_dbg_phases_ctrl: phases_ctrl
val cfg_trace_phase_goals: bool Config.T
val flag_phases_ctrl: Proof.context -> bool -> phases_ctrl
type phase = string * (Proof.context -> tactic') * int
val PHASES': phase list -> phases_ctrl -> Proof.context -> tactic'
end
structure Sepref_Basic: SEPREF_BASIC = struct
fun is_nresT (Type (@{type_name nrest},[_,_])) = true | is_nresT _ = false
fun mk_nresT T = Type(@{type_name nrest},[T,@{typ ecost}])
fun dest_nresT (Type (@{type_name nrest},[T,_])) = T | dest_nresT T = raise TYPE("dest_nresT",[T],[])
fun dest_lambda_rc ctxt (Abs (x,T,t)) = let
val (u,ctxt) = yield_singleton Variable.variant_fixes x ctxt
val u = Free (u,T)
val t = subst_bound (u,t)
val reconstruct = Term.lambda_name (x,u)
in
((t,reconstruct),ctxt)
end
| dest_lambda_rc _ t = raise TERM("dest_lambda_rc",[t])
fun apply_under_lambda f ctxt t = let
val ((t,rc),ctxt) = dest_lambda_rc ctxt t
val t = f ctxt t
in
rc t
end
fun mk_pair_in_pre x y r = Const (@{const_name Set.member}, dummyT) $
(Const (@{const_name Product_Type.Pair}, dummyT) $ x $ y) $ r
fun mk_uncurry_pre t = Const(@{const_name uncurry}, dummyT)$t
fun mk_uncurry0_pre t = Const(@{const_name uncurry0}, dummyT)$t
fun mk_uncurryN_pre 0 = mk_uncurry0_pre
| mk_uncurryN_pre 1 = I
| mk_uncurryN_pre n = mk_uncurry_pre o mk_uncurryN_pre (n-1)
fun mk_curry_pre t = Const(@{const_name curry}, dummyT)$t
fun mk_curry0_pre t = Const(@{const_name curry0}, dummyT)$t
fun mk_curryN_pre 0 = mk_curry0_pre
| mk_curryN_pre 1 = I
| mk_curryN_pre n = mk_curry_pre o mk_curryN_pre (n-1)
fun mk_compN_pre 0 f g = f $ g
| mk_compN_pre n f g = let
val g = fold (fn i => fn t => t$Bound i) (n-2 downto 0) g
val t = Const(@{const_name "Fun.comp"},dummyT) $ f $ g
val t = fold (fn i => fn t => Abs ("x"^string_of_int i,dummyT,t)) (n-1 downto 1) t
in
t
end
fun constrain_type_pre T t = Const(@{syntax_const "_type_constraint_"},T-->T) $ t
local open Conv in
fun hn_refine_conv c1 c2 c3 c4 c5 ct = case Thm.term_of ct of
@{mpat "hn_refine _ _ _ _ _"} => let
val cc = combination_conv
in
cc (cc (cc (cc (cc all_conv c1) c2) c3) c4) c5 ct
end
| _ => raise CTERM ("hn_refine_conv",[ct])
val hn_refine_conv_a = hn_refine_conv all_conv all_conv all_conv all_conv
fun hn_refine_concl_conv_a conv ctxt = Refine_Util.HOL_concl_conv
(fn ctxt => hn_refine_conv_a (conv ctxt)) ctxt
end
val mk_cequals = uncurry SMT_Util.mk_cequals
val mk_entails = HOLogic.mk_binrel @{const_name "entails"}
val mk_star = HOLogic.mk_binop @{const_name "sep_conj"}
fun list_star [] = @{term "□::assn"}
| list_star [a] = a
| list_star (a::l) = mk_star (a,list_star l)
fun strip_star @{mpat "?a**?b"} = strip_star a @ strip_star b
| strip_star @{mpat "□"} = []
| strip_star t = [t]
fun is_true @{mpat "sep_true"} = true | is_true _ = false
fun is_hn_ctxt @{mpat "hn_ctxt _ _ _"} = true | is_hn_ctxt _ = false
fun dest_hn_ctxt @{mpat "hn_ctxt ?R ?a ?p"} = (R,a,p)
| dest_hn_ctxt t = raise TERM("dest_hn_ctxt",[t])
fun dest_hn_ctxt_opt @{mpat "hn_ctxt ?R ?a ?p"} = SOME (R,a,p)
| dest_hn_ctxt_opt _ = NONE
fun strip_abs_args (t as @{mpat "PR_CONST _"}) = (t,[])
| strip_abs_args @{mpat "?f$?a"} = (case strip_abs_args f of (f,args) => (f,args@[a]))
| strip_abs_args t = (t,[])
fun dest_hnr_absfun @{mpat "RETURN$?a"} = (true, strip_abs_args a)
| dest_hnr_absfun f = (false, strip_abs_args f)
fun dest_hn_refine @{mpat "hn_refine ?P ?c ?Q ?R ?a"} = (P,c,Q,R,a)
| dest_hn_refine t = raise TERM("dest_hn_refine",[t])
fun mk_hn_refine (P,c,Q,R,a) = @{mk_term "hn_refine ?P ?c ?Q ?R ?a"}
val is_hn_refine_concl = can (HOLogic.dest_Trueprop #> dest_hn_refine)
fun star_permute_tac ctxt = ALLGOALS (
VCG_Lib.simp_only_tac @{thms sep_conj_empty sep_conj_empty' sep_conj_ac} ctxt)
type phases_ctrl = {
trace: bool,
trace_goals: bool,
int_res: bool,
start: string option,
stop: string option
}
val dflt_phases_ctrl = {trace=false,trace_goals=false,int_res=false,start=NONE,stop=NONE}
val dbg_phases_ctrl = {trace=true,trace_goals=false,int_res=true,start=NONE,stop=NONE}
val full_dbg_phases_ctrl = {trace=true,trace_goals=true,int_res=true,start=NONE,stop=NONE}
val cfg_trace_phase_goals = Attrib.setup_config_bool @{binding sepref_trace_phase_goals} (K false)
fun flag_phases_ctrl ctxt dbg =
case (Config.get ctxt cfg_trace_phase_goals, dbg) of
(_, false) => dflt_phases_ctrl
| (false, true) => dbg_phases_ctrl
| (true,true) => full_dbg_phases_ctrl
type phase = string * (Proof.context -> tactic') * int
local
fun ph_range phases start stop = let
fun find_phase name = let
val i = find_index (fn (n,_,_) => n=name) phases
val _ = if i<0 then error ("No such phase: " ^ name) else ()
in
i
end
val i = case start of NONE => 0 | SOME n => find_phase n
val j = case stop of NONE => length phases - 1 | SOME n => find_phase n
val phases = take (j+1) phases |> drop i
val _ = case phases of [] => error "No phases selected, range is empty" | _ => ()
in
phases
end
in
fun PHASES' phases ctrl ctxt = let
val phases = ph_range phases (#start ctrl) (#stop ctrl)
val phases = map (fn (n,tac,d) => (n,tac ctxt,d)) phases
fun r [] _ st = Seq.single st
| r ((name,tac,d)::tacs) i st = let
val n = Thm.nprems_of st
val bailout_tac = if #int_res ctrl then all_tac else no_tac
fun trace_tac msg st = (if #trace ctrl then tracing msg else (); Seq.single st)
val trace_goal_tac = if #trace_goals ctrl then print_tac ctxt "Proof state" else all_tac
val trace_start_tac = trace_tac ("Phase " ^ name)
in
K trace_goal_tac THEN' K trace_start_tac THEN' IF_EXGOAL (tac)
THEN_ELSE' (
fn i => fn st =>
if Thm.nprems_of st = n+d then
((trace_tac " Done" THEN r tacs i) st)
else
(trace_tac "*** Wrong number of produced goals" THEN bailout_tac) st
,
K (trace_tac "*** Phase tactic failed" THEN bailout_tac))
end i st
in
r phases
end
end
end
signature SEPREF_DEBUGGING = sig
val cfg_debug_all: bool Config.T
val is_debug: bool Config.T -> Proof.context -> bool
val is_debug': Proof.context -> bool
val DBG_CONVERSION: bool Config.T -> Proof.context -> conv -> tactic'
val DBG_CONVERSION': Proof.context -> conv -> tactic'
val tracing_tac': string -> Proof.context -> tactic'
val warning_tac': string -> Proof.context -> tactic'
val error_tac': string -> Proof.context -> tactic'
val dbg_trace_msg: bool Config.T -> Proof.context -> string -> unit
val dbg_trace_msg': Proof.context -> string -> unit
val dbg_trace: bool Config.T -> Proof.context -> (Proof.context -> string) -> unit
val dbg_trace': Proof.context -> (Proof.context -> string) -> unit
val dbg_msg_tac: bool Config.T -> (Proof.context -> int -> thm -> string) -> Proof.context -> tactic'
val dbg_msg_tac': (Proof.context -> int -> thm -> string) -> Proof.context -> tactic'
val msg_text: string -> Proof.context -> int -> thm -> string
val msg_subgoal: string -> Proof.context -> int -> thm -> string
val msg_from_subgoal: string -> (term -> Proof.context -> string) -> Proof.context -> int -> thm -> string
val msg_allgoals: string -> Proof.context -> int -> thm -> string
end
structure Sepref_Debugging: SEPREF_DEBUGGING = struct
val cfg_debug_all =
Attrib.setup_config_bool @{binding sepref_debug_all} (K false)
fun is_debug cfg ctxt = Config.get ctxt cfg orelse Config.get ctxt cfg_debug_all
fun is_debug' ctxt = Config.get ctxt cfg_debug_all
fun dbg_trace cfg ctxt obj =
if is_debug cfg ctxt then
tracing ((obj ctxt))
else ()
fun dbg_trace' ctxt obj =
if is_debug' ctxt then
tracing ((obj ctxt))
else ()
fun dbg_trace_msg cfg ctxt msg =
if is_debug cfg ctxt then
tracing msg
else ()
fun dbg_trace_msg' ctxt msg =
if is_debug' ctxt then
tracing msg
else ()
fun DBG_CONVERSION cfg ctxt cv i st =
Seq.single (Conv.gconv_rule cv i st)
handle e as THM _ => (dbg_trace cfg ctxt (K (@{make_string} e)); Seq.empty)
| e as CTERM _ => (dbg_trace cfg ctxt (K (@{make_string} e)); Seq.empty)
| e as TERM _ => (dbg_trace cfg ctxt (K (@{make_string} e)); Seq.empty)
| e as TYPE _ => (dbg_trace cfg ctxt (K (@{make_string} e)); Seq.empty);
fun DBG_CONVERSION' ctxt cv i st =
Seq.single (Conv.gconv_rule cv i st)
handle e as THM _ => (dbg_trace' ctxt (K (@{make_string} e)); Seq.empty)
| e as CTERM _ => (dbg_trace' ctxt (K (@{make_string} e)); Seq.empty)
| e as TERM _ => (dbg_trace' ctxt (K (@{make_string} e)); Seq.empty)
| e as TYPE _ => (dbg_trace' ctxt (K (@{make_string} e)); Seq.empty);
local
fun gen_subgoal_msg_tac do_msg msg ctxt = IF_EXGOAL (fn i => fn st => let
val t = nth (Thm.prems_of st) (i-1)
val _ = Pretty.block [Pretty.str msg, Pretty.fbrk, Syntax.pretty_term ctxt t]
|> Pretty.string_of |> do_msg
in
Seq.single st
end)
in
val tracing_tac' = gen_subgoal_msg_tac tracing
val warning_tac' = gen_subgoal_msg_tac warning
val error_tac' = gen_subgoal_msg_tac error
end
fun dbg_msg_tac cfg msg ctxt =
if is_debug cfg ctxt then (fn i => fn st => (tracing (msg ctxt i st); Seq.single st))
else K all_tac
fun dbg_msg_tac' msg ctxt =
if is_debug' ctxt then (fn i => fn st => (tracing (msg ctxt i st); Seq.single st))
else K all_tac
fun msg_text msg _ _ _ = msg
fun msg_from_subgoal msg sgmsg ctxt i st =
case try (nth (Thm.prems_of st)) (i-1) of
NONE => msg ^ "\n" ^ "Subgoal out of range"
| SOME t => msg ^ "\n" ^ sgmsg t ctxt
fun msg_subgoal msg = msg_from_subgoal msg (fn t => fn ctxt =>
Syntax.pretty_term ctxt t |> Pretty.string_of
)
fun msg_allgoals msg ctxt _ st =
msg ^ "\n" ^ Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals ctxt st))
end
›
ML ‹
infix 1 THEN_NEXT THEN_ALL_NEW_LIST THEN_ALL_NEW_LIST'
signature STACTICAL = sig
val THEN_NEXT: tactic' * tactic' -> tactic'
val APPLY_LIST: tactic' list -> tactic'
val THEN_ALL_NEW_LIST: tactic' * tactic' list -> tactic'
val THEN_ALL_NEW_LIST': tactic' * (tactic' list * tactic') -> tactic'
end
structure STactical : STACTICAL = struct
infix 1 THEN_WITH_GOALDIFF
fun (tac1 THEN_WITH_GOALDIFF tac2) st = let
val n1 = Thm.nprems_of st
in
st |> (tac1 THEN (fn st => tac2 (Thm.nprems_of st - n1) st ))
end
fun (tac1 THEN_NEXT tac2) i =
tac1 i THEN_WITH_GOALDIFF (fn d => (
if d < ~1 then
(error "THEN_NEXT: Tactic solved more than one goal"; no_tac)
else
tac2 (i+1+d)
))
fun APPLY_LIST [] = K all_tac
| APPLY_LIST (tac::tacs) = tac THEN_NEXT APPLY_LIST tacs
fun (tac1 THEN_ALL_NEW_LIST tacs) i =
tac1 i
THEN_WITH_GOALDIFF (fn d =>
if d+1 <> length tacs then (
error "THEN_ALL_NEW_LIST: Tactic produced wrong number of goals"; no_tac
) else APPLY_LIST tacs i
)
fun (tac1 THEN_ALL_NEW_LIST' (tacs,rtac)) i =
tac1 i
THEN_WITH_GOALDIFF (fn d => let
val _ = if d+1 < length tacs then error "THEN_ALL_NEW_LIST': Tactic produced too few goals" else ();
val tacs' = tacs @ replicate (d + 1 - length tacs) rtac
in
APPLY_LIST tacs' i
end)
end
open STactical
›
end