Theory Sepref_Translate
section ‹Translation›
theory Sepref_Translate
imports
Sepref_Monadify
Sepref_Constraints
Sepref_Conc_Post
Sepref_Frame
Sepref_Rules
Sepref_Combinator_Setup
"../lib/More_Eisbach_Tools"
"Lib/User_Smashing"
begin
text ‹
This theory defines the translation phase.
The main functionality of the translation phase is to
apply refinement rules. Thereby, the linearity information is
exploited to create copies of parameters that are still required, but
would be destroyed by a synthesized operation.
These \emph{frame-based} rules are in the named theorem collection
@{text sepref_fr_rules}, and the collection @{text sepref_copy_rules}
contains rules to handle copying of parameters.
Apart from the frame-based rules described above, there is also a set of
rules for combinators, in the collection @{text sepref_comb_rules},
where no automatic copying of parameters is applied.
Moreover, this theory contains
\begin{itemize}
\item A setup for the basic monad combinators and recursion.
\item A tool to import parametricity theorems.
\item Some setup to identify pure refinement relations, i.e., those not
involving the heap.
\item A preprocessor that identifies parameters in refinement goals,
and flags them with a special tag, that allows their correct handling.
\end{itemize}
›
text ‹Tag to keep track of abstract bindings.
Required to recover information for side-condition solving.›
definition "bind_ref_tag x m ≡ RETURN x ≤ m"
text ‹Tag to keep track of preconditions in assertions›
definition "vassn_tag Γ ≡ ∃h. Γ h"
lemma vassn_tagI: "Γ h ⟹ vassn_tag Γ"
unfolding vassn_tag_def ..
lemma vassn_dest[dest!]:
"vassn_tag (Γ⇩1 ** Γ⇩2) ⟹ vassn_tag Γ⇩1 ∧ vassn_tag Γ⇩2"
"vassn_tag (hn_ctxt R a b) ⟹ rdomp R a"
"vassn_tag (↑Φ) ⟹ Φ"
unfolding vassn_tag_def hn_ctxt_def rdomp_def[abs_def]
by (auto simp: sep_conj_def pred_lift_extract_simps)
lemma entails_preI:
assumes "vassn_tag A ⟹ A ⊢ B"
shows "A ⊢ B"
using assms
by (auto simp: entails_def vassn_tag_def)
lemma invalid_assn_const:
"invalid_assn (λ_ _. P) x y = ↑(vassn_tag P)"
by (simp_all add: invalid_assn_def vassn_tag_def pure_part_def)
lemma vassn_tag_simps[simp]:
"vassn_tag □"
"vassn_tag sep_true"
by (auto simp: vassn_tag_def)
lemma hn_refine_vassn_tagI:
"⟦ vassn_tag Γ ⟹ hn_refine Γ c Γ' R CP a ⟧ ⟹ hn_refine Γ c Γ' R CP a"
apply (rule hn_refine_preI)
by (auto simp: vassn_tag_def)
definition "GEN_ALGO f Φ ≡ Φ f"
lemma is_GEN_ALGO: "GEN_ALGO f Φ ⟹ GEN_ALGO f Φ" .
named_theorems_rev sepref_gen_algo_rules ‹Sepref: Generic algorithm rules›
text ‹Tag for side-condition solver to discharge by assumption›
definition RPREM :: "bool ⇒ bool" where [simp]: "RPREM P = P"
lemma RPREMI: "P ⟹ RPREM P" by simp
lemma trans_frame_rule:
assumes "RECOVER_PURE Γ Γ'"
assumes "vassn_tag (Γ'**F) ⟹ hn_refine Γ' c Γ'' R CP a"
shows "hn_refine (Γ**F) c (Γ''**F) R CP a"
apply (rule hn_refine_vassn_tagI)
apply (rule hn_refine_frame[OF _ entails_refl])
applyF (rule hn_refine_cons_pre)
focus using assms(1) unfolding RECOVER_PURE_def apply assumption solved
apply1 (rule assms)
applyS (metis RECOVER_PURE_def assms(1) entails_eq_iff entails_preI frame_thms(2))
solved
done
lemma recover_pure_cons:
assumes "RECOVER_PURE Γ Γ'"
assumes "hn_refine Γ' c Γ'' R CP a"
shows "hn_refine (Γ) c (Γ'') R CP a"
using trans_frame_rule[where F=□, OF assms] by simp
definition CPR_TAG :: "assn ⇒ assn ⇒ bool" where [simp]: "CPR_TAG y x ≡ True"
lemma CPR_TAG_starI:
assumes "CPR_TAG P1 Q1"
assumes "CPR_TAG P2 Q2"
shows "CPR_TAG (P1**P2) (Q1**Q2)"
by simp
lemma CPR_tag_ctxtI: "CPR_TAG (hn_ctxt R x xi) (hn_ctxt R' x xi)" by simp
lemma CPR_tag_fallbackI: "CPR_TAG P Q" by simp
lemmas CPR_TAG_rules = CPR_TAG_starI CPR_tag_ctxtI CPR_tag_fallbackI
lemma cons_pre_rule:
assumes "CPR_TAG P P'"
assumes "P ⊢ P'"
assumes "hn_refine P' c Q R CP m"
shows "hn_refine P c Q R CP m"
using assms(2-) by (rule hn_refine_cons_pre)
named_theorems_rev sepref_bounds_dest ‹Bounds solver drules›
named_theorems_rev sepref_bounds_simps ‹Bounds solver simp rules›
ML ‹
structure Sepref_Translate = struct
val cfg_debug =
Attrib.setup_config_bool @{binding sepref_debug_translate} (K false)
val dbg_msg_tac = Sepref_Debugging.dbg_msg_tac cfg_debug
fun check_side_conds thm = let
open Sepref_Basic
fun is_atomic (Const (_,@{typ "assn⇒assn⇒assn"})$_$_) = false
| is_atomic _ = true
val is_atomic_star_list = ("Expected atoms separated by star",forall is_atomic o strip_star)
val is_trueprop = ("Expected Trueprop conclusion",can HOLogic.dest_Trueprop)
fun assert t' (msg,p) t = if p t then () else raise TERM(msg,[t',t])
fun chk_prem t = let
val assert = assert t
fun chk @{mpat "MERGE ?l _ ?r _ ?m"} = (
assert is_atomic_star_list l;
assert is_atomic_star_list r;
assert is_atomic_star_list m
)
| chk @{mpat "?l ⊢ ?r"} = (
assert is_atomic_star_list l;
assert is_atomic_star_list r
)
| chk _ = ()
val t = Logic.strip_assums_concl t
in
assert is_trueprop t;
chk (HOLogic.dest_Trueprop t)
end
in
map chk_prem (Thm.prems_of thm)
end
structure sepref_comb_rules = Named_Sorted_Thms (
val name = @{binding "sepref_comb_rules"}
val description = "Sepref: Combinator rules"
val sort = K I
fun transform _ thm = let
val _ = check_side_conds thm
in
[thm]
end
)
structure sepref_fr_rules = Named_Sorted_Thms (
val name = @{binding "sepref_fr_rules"}
val description = "Sepref: Frame-based rules"
val sort = K I
fun transform context thm = let
val ctxt = Context.proof_of context
val thm = Sepref_Rules.ensure_hnr ctxt thm
|> Conv.fconv_rule (Sepref_Frame.align_rl_conv ctxt)
val _ = check_side_conds thm
val _ = case try (Sepref_Rules.analyze_hnr ctxt) thm of
NONE =>
(Pretty.block [
Pretty.str "hnr-analysis failed",
Pretty.str ":",
Pretty.brk 1,
Thm.pretty_thm ctxt thm])
|> Pretty.string_of |> error
| SOME ana => let
val _ = Sepref_Combinator_Setup.is_valid_abs_op ctxt (fst (#ahead ana))
orelse Pretty.block [
Pretty.str "Invalid abstract head:",
Pretty.brk 1,
Pretty.enclose "(" ")" [Syntax.pretty_term ctxt (fst (#ahead ana))],
Pretty.brk 1,
Pretty.str "in thm",
Pretty.brk 1,
Thm.pretty_thm ctxt thm
]
|> Pretty.string_of |> error
in () end
in
[thm]
end
)
local
open Sepref_Basic
in
fun side_unfold_tac ctxt = let
in
CONVERSION (Id_Op.unprotect_conv ctxt)
THEN' SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms bind_ref_tag_def})
THEN' TRY o (hyp_subst_tac ctxt)
end
fun linarith_tac ctxt =
Method.insert_tac ctxt (rev (Named_Theorems.get ctxt \<^named_theorems>‹arith›))
THEN' Lin_Arith.tac ctxt
fun bounds_tac ctxt = let
val ctxt = ctxt
addSDs Named_Theorems_Rev.get ctxt @{named_theorems_rev sepref_bounds_dest}
addsimps Named_Theorems_Rev.get ctxt @{named_theorems_rev sepref_bounds_simps}
in
TRADE (fn ctxt =>
SELECT_GOAL (auto_tac ctxt)
THEN_ALL_NEW TRY o linarith_tac ctxt
) ctxt
end
fun side_fallback_tac ctxt =
side_unfold_tac ctxt
THEN' (
TRADE (SELECT_GOAL o auto_tac) ctxt
THEN_ALL_NEW (TRY o SOLVED' (bounds_tac ctxt))
)
val side_frame_tac = Sepref_Frame.frame_tac side_fallback_tac
val side_merge_tac = Sepref_Frame.merge_tac side_fallback_tac
val side_free_tac = Sepref_Frame.free_tac side_fallback_tac
fun side_constraint_tac ctxt = Sepref_Constraints.constraint_tac ctxt
val pf_mono_tac = Subgoal.FOCUS_PREMS (fn {context=ctxt,...} => CHANGED (ALLGOALS (Partial_Function.mono_tac ctxt)))
fun side_mono_tac ctxt = side_unfold_tac ctxt THEN' TRADE pf_mono_tac ctxt
fun side_gen_algo_tac ctxt =
side_unfold_tac ctxt
THEN' resolve_tac ctxt (Named_Theorems_Rev.get ctxt @{named_theorems_rev sepref_gen_algo_rules})
fun side_pref_def_tac ctxt =
side_unfold_tac ctxt THEN'
TRADE (fn ctxt =>
resolve_tac ctxt @{thms PREFER_tagI DEFER_tagI}
THEN' (Sepref_Debugging.warning_tac' "Obsolete PREFER/DEFER side condition" ctxt THEN' Tagged_Solver.solve_tac ctxt)
) ctxt
fun side_rprem_tac ctxt =
resolve_tac ctxt @{thms RPREMI} THEN' Refine_Util.rprems_tac ctxt
THEN' (K (smash_new_rule ctxt))
fun side_cond_dispatch_tac dbg hnr_tac ctxt = let
fun MK tac = if dbg then CHANGED o tac ctxt else SOLVED' (tac ctxt)
val t_merge = MK side_merge_tac
val t_frame = MK side_frame_tac
val t_free = MK side_free_tac
val t_indep = MK Indep_Vars.indep_tac
val t_constraint = MK side_constraint_tac
val t_mono = MK side_mono_tac
val t_pref_def = MK side_pref_def_tac
val t_rprem = MK side_rprem_tac
val t_gen_algo = side_gen_algo_tac ctxt
val t_cp_cond = MK (apply_method_noargs @{method cp_solve_cond})
val t_cp_simplify = MK (apply_method_noargs @{method cp_simplify})
val t_fallback = MK side_fallback_tac
in
WITH_concl
(fn @{mpat "Trueprop ?t"} => (case t of
@{mpat "MERGE _ _ _ _ _"} => t_merge
| @{mpat "MK_FREE _ _"} => t_free
| @{mpat "_ ⊢ _"} => t_frame
| @{mpat "INDEP _"} => t_indep
| @{mpat "CONSTRAINT _ _"} => t_constraint
| @{mpat "monotone _ _ _"} => t_mono
| @{mpat "∀_. monotone _ _ _"} => t_mono
| @{mpat "PREFER_tag _"} => t_pref_def
| @{mpat "DEFER_tag _"} => t_pref_def
| @{mpat "RPREM _"} => t_rprem
| @{mpat "GEN_ALGO _ _"} => t_gen_algo
| @{mpat "CP_cond _"} => t_cp_cond
| @{mpat "CP_simplify _ _"} => t_cp_simplify
| @{mpat "hn_refine _ _ _ _ _ _"} => hnr_tac
| _ => t_fallback
)
| _ => K no_tac
)
end
end
local
open Sepref_Basic STactical
in
fun trans_comb_tac ctxt = let
val comb_rl_net = sepref_comb_rules.get ctxt
|> Tactic.build_net
in
DETERM o (
resolve_from_net_tac ctxt comb_rl_net
)
end
fun gen_trans_op_tac dbg ctxt = let
val fr_rl_net = sepref_fr_rules.get ctxt |> Tactic.build_net
val fr_rl_tac =
resolve_from_net_tac ctxt fr_rl_net
ORELSE' (
Sepref_Frame.norm_goal_pre_tac ctxt
THEN' (
resolve_from_net_tac ctxt fr_rl_net
ORELSE' (
resolve_tac ctxt @{thms cons_pre_rule}
THEN_ALL_NEW_LIST [
SOLVED' (REPEAT_ALL_NEW_FWD (DETERM o resolve_tac ctxt @{thms CPR_TAG_rules})),
K all_tac,
resolve_from_net_tac ctxt fr_rl_net
]
)
)
)
val side_tac = REPEAT_ALL_NEW_FWD (side_cond_dispatch_tac false (K no_tac) ctxt)
val fr_tac =
if dbg then
fr_rl_tac THEN_ALL_NEW_FWD (TRY o side_tac)
else
DETERM o SOLVED' (fr_rl_tac THEN_ALL_NEW_FWD (SOLVED' side_tac))
in
PHASES' [
("Align goal",Sepref_Frame.align_goal_tac, 0),
("Frame rule",fn ctxt => resolve_tac ctxt @{thms trans_frame_rule}, 1),
("Recover pure",Sepref_Frame.recover_pure_tac, ~1),
("Apply rule",K fr_tac,~1)
] (flag_phases_ctrl ctxt dbg) ctxt
end
fun gen_trans_step_tac dbg ctxt = side_cond_dispatch_tac dbg
( Sepref_Frame.norm_goal_pre_tac ctxt
THEN' (trans_comb_tac ctxt ORELSE' gen_trans_op_tac dbg ctxt))
ctxt
val trans_step_tac = gen_trans_step_tac false
val trans_step_keep_tac = gen_trans_step_tac true
fun gen_trans_tac dbg ctxt =
PHASES' [
("Translation steps",REPEAT_DETERM' o trans_step_tac,~1),
("Constraint solving",fn ctxt => fn _ => Sepref_Constraints.process_constraint_slot ctxt, 0)
] (flag_phases_ctrl ctxt dbg) ctxt
val trans_tac = gen_trans_tac false
val trans_keep_tac = gen_trans_tac true
end
val setup = I
#> sepref_fr_rules.setup
#> sepref_comb_rules.setup
end
›
setup Sepref_Translate.setup
method_setup sepref_bounds = ‹SIMPLE_METHOD_NOPARAM' (Sepref_Translate.bounds_tac)›
subsubsection ‹Basic Setup›
lemma hn_pass[sepref_fr_rules]:
shows "hn_refine (hn_ctxt P x x') (Mreturn x') (hn_invalid P x x') P (λr. r=x') (PASS$x)"
apply rule
apply (subst invalidate_clone') unfolding hn_ctxt_def
apply vcg
done
thm hnr_bind
lemma hn_bind[sepref_comb_rules]:
assumes D1: "hn_refine Γ m' Γ1 Rh CP⇩1 m"
assumes D2:
"⋀x x'. bind_ref_tag x m ⟹ CP_assm (CP⇩1 x') ⟹
hn_refine (hn_ctxt Rh x x' ** Γ1) (f' x') (Γ2 x x') R (CP⇩2 x') (f x)"
assumes IMP: "⋀x x'. Γ2 x x' ⊢ hn_ctxt Rx x x' ** Γ'"
assumes "MK_FREE Rx fr"
shows "hn_refine Γ (doM {x←m'; r←f' x; fr x; Mreturn r}) Γ' R (CP_SEQ CP⇩1 CP⇩2) (Refine_Basic.bind$m$(λ⇩2x. f x))"
using assms
unfolding APP_def PROTECT2_def bind_ref_tag_def CP_defs
by (rule hnr_bind)
lemma hn_RECT'[sepref_comb_rules]:
assumes "INDEP Ry" "INDEP Rx" "INDEP Rx'"
assumes FR: "P ⊢ hn_ctxt Rx ax px ** F"
assumes S: "⋀cf af ax px. ⟦
⋀ax px. hn_refine (hn_ctxt Rx ax px ** F) (cf px) (hn_ctxt Rx' ax px ** F) Ry (λ_. True)
(RCALL$af$ax)⟧
⟹ hn_refine (hn_ctxt Rx ax px ** F) (cB cf px) (F' ax px) Ry (CP px)
(aB af ax)"
assumes FR': "⋀ax px. F' ax px ⊢ hn_ctxt Rx' ax px ** F"
assumes M: "M_mono_body cB"
shows "hn_refine
(P) (MMonad.REC cB px) (hn_ctxt Rx' ax px ** F) Ry (CP$px)
(RECT$(λ⇩2D x. aB D x)$ax)"
unfolding APP_def PROTECT2_def
apply (rule hn_refine_cons_pre[OF FR])
apply (rule hnr_RECT)
apply (rule hn_refine_cons_post[OF _ FR'])
apply (rule hn_refine_cons_cp_only)
apply (rule S[unfolded RCALL_def APP_def])
apply (rule hn_refine_cons_cp_only)
apply assumption
apply simp
apply assumption
apply fact
done
lemma hn_RCALL[sepref_comb_rules]:
assumes "RPREM (hn_refine P' c Q' R CP (RCALL $ a $ b))"
and "P ⊢ P' ** F"
shows "hn_refine P c (Q'**F) R CP (RCALL $ a $ b)"
using assms hn_refine_frame[where m="RCALL$a$b"]
by simp
definition RECT_cp_annot :: "('ai ⇒ 'bi ⇒ bool) ⇒ (('a ⇒ 'b nres) ⇒ 'a ⇒ 'b nres) ⇒ 'a ⇒ 'b nres"
where "RECT_cp_annot CP ≡ RECT"
lemma RECT_cp_annot: "RECT = RECT_cp_annot CP" unfolding RECT_cp_annot_def ..
lemma RECT_cp_annot_pat[def_pat_rules]:
"RECT_cp_annot$CP ≡ UNPROTECT (RECT_cp_annot CP)"
by simp
lemma RECT_cp_annot_arity[sepref_monadify_arity]:
"PR_CONST (RECT_cp_annot CP) ≡ λ⇩2B x. SP (PR_CONST (RECT_cp_annot CP))$(λ⇩2D x. B$(λ⇩2x. RCALL$D$x)$x)$x"
by (simp_all)
lemma RECT_cp_annot_comb[sepref_monadify_comb]:
"⋀B x. PR_CONST (RECT_cp_annot CP)$B$x ≡ Refine_Basic.bind$(EVAL$x)$(λ⇩2x. SP (PR_CONST (RECT_cp_annot CP)$B$x))"
by (simp_all)
lemma RECT_cp_annot_id[id_rules]:
"PR_CONST (RECT_cp_annot CP) ::⇩i TYPE((('c ⇒ 'd nres) ⇒ 'c ⇒ 'd nres) ⇒ 'c ⇒ 'd nres)"
by simp
lemma hn_RECT_cp_annot:
assumes "INDEP Ry" "INDEP Rx" "INDEP Rx'"
assumes FR: "P ⊢ hn_ctxt Rx ax px ** F"
assumes S: "⋀cf af ax px. ⟦
⋀ax px. hn_refine (hn_ctxt Rx ax px ** F) (cf px) (hn_ctxt Rx' ax px ** F) Ry (CP px)
(RCALL$af$ax)⟧
⟹ hn_refine (hn_ctxt Rx ax px ** F) (cB cf px) (F' ax px) Ry (CP' px)
(aB af ax)"
assumes CP: "⋀px r. CP_assm (CP' px r) ⟹ CP_cond (CP px r)"
assumes FR': "⋀ax px. F' ax px ⊢ hn_ctxt Rx' ax px ** F"
assumes M: "M_mono_body cB"
shows "hn_refine
(P) (MMonad.REC cB px) (hn_ctxt Rx' ax px ** F) Ry (CP$px)
(PR_CONST (RECT_cp_annot CP)$(λ⇩2D x. aB D x)$ax)"
unfolding APP_def PROTECT2_def RECT_cp_annot_def PR_CONST_def
apply (rule hn_refine_cons_pre[OF FR])
thm hnr_RECT
apply (rule hnr_RECT)
apply (rule hn_refine_cons_post[OF _ FR'])
apply (rule hn_refine_cons_cp_only)
apply (rule S[unfolded RCALL_def APP_def])
apply (rule hn_refine_cons_cp_only)
applyS assumption
applyS simp
subgoal using CP by (simp add: CP_defs)
applyS fact
done
lemma hn_RECT_cp_annot_noframe:
assumes "INDEP Ry" "INDEP Rx" "INDEP Rx'"
assumes FR: "P ⊢ hn_ctxt Rx ax px ** F"
assumes S: "⋀cf af ax px. ⟦
⋀ax px. hn_refine (hn_ctxt Rx ax px) (cf px) (hn_ctxt Rx' ax px) Ry (CP px)
(RCALL$af$ax)⟧
⟹ hn_refine (hn_ctxt Rx ax px) (cB cf px) (F' ax px) Ry (CP' px)
(aB af ax)"
assumes CP: "⋀px r. CP_assm (CP' px r) ⟹ CP_cond (CP px r)"
assumes FR': "⋀ax px. F' ax px ⊢ hn_ctxt Rx' ax px"
assumes M: "M_mono_body cB"
shows "hn_refine
(P) (MMonad.REC cB px) (hn_ctxt Rx' ax px ** F) Ry (CP$px)
(PR_CONST (RECT_cp_annot CP)$(λ⇩2D x. aB D x)$ax)"
apply (rule hn_refine_cons_post)
apply (rule hn_refine_frame[where F=F])
apply (rule hn_RECT_cp_annot[where F=□, OF assms(1,2,3)])
applyS (rule entails_refl)
focus apply simp apply (rule S) apply simp solved
applyS fact
focus apply simp apply fact solved
applyS fact
focus using FR apply (simp add: algebra_simps) solved
applyS (simp add: algebra_simps)
done
lemma hn_RECT'_cp[sepref_comb_rules]:
assumes "INDEP Ry" "INDEP Rx" "INDEP Rx'"
assumes FR: "P ⊢ hn_ctxt Rx ax px ** F"
assumes S: "⋀cf af ax px. ⟦
⋀ax px. hn_refine (hn_ctxt Rx ax px ** F) (cf px) (hn_ctxt Rx' ax px ** F) Ry (CP px)
(RCALL$af$ax)⟧
⟹ hn_refine (hn_ctxt Rx ax px ** F) (cB cf px) (F' ax px) Ry (CP' px)
(aB af ax)"
assumes CP: "⋀px r. CP_assm (CP' px r) ⟹ CP_cond (CP px r)"
assumes FR': "⋀ax px. F' ax px ⊢ hn_ctxt Rx' ax px ** F"
assumes M: "M_mono_body cB"
shows "hn_refine
(P) (MMonad.REC cB px) (hn_ctxt Rx' ax px ** F) Ry (CP$px)
(PR_CONST (RECT_cp_annot CP)$(λ⇩2D x. aB D x)$ax)"
unfolding APP_def PROTECT2_def RECT_cp_annot_def PR_CONST_def
apply (rule hn_refine_cons_pre[OF FR])
apply (rule hnr_RECT)
apply (rule hn_refine_cons_post[OF _ FR'])
apply (rule hn_refine_cons_cp_only)
apply (rule S[unfolded RCALL_def APP_def])
apply (rule hn_refine_cons_cp_only)
apply assumption
apply simp
subgoal using CP by (simp add: CP_defs)
apply fact
done
lemma hn_refine_synthI:
assumes "hn_refine Γ c Γ' R' CP m"
assumes "c = c'"
assumes "R' = R''"
assumes "Γ' ⊢ Γ''"
shows "hn_refine Γ c' Γ'' R'' CP m"
using assms by (blast intro: hn_refine_cons_post)
lemma :
"hn_refine (hn_val S xa xc ** Γ) c Γ' R CP m ⟷ ((xc,xa)∈S ⟶ hn_refine Γ c Γ' R CP m)"
unfolding hn_refine_def hn_ctxt_def pure_def
apply (cases "(xc,xa)∈S")
by (auto simp: sep_algebra_simps)
lemma hnr_freeI:
assumes "MK_FREE R fr"
assumes "hn_refine Γ c Γ' R' CP m"
shows "hn_refine (hn_ctxt R x y ** Γ) (doM { fr y; c}) Γ' R' CP m"
proof (rule hn_refine_nofailI)
assume "nofail m"
note [vcg_rules] = MK_FREED[OF assms(1)] hn_refineD[OF assms(2) ‹nofail m›]
show ?thesis unfolding hn_ctxt_def
by rule vcg
qed
lemma drop_hn_val: "hn_val R x y ⊢ □" by (auto simp: hn_ctxt_def pure_def entails_def pred_lift_extract_simps)
lemma drop_hn_invalid: "hn_invalid R x y ⊢ □" by (auto simp: hn_ctxt_def invalid_assn_def entails_def pred_lift_extract_simps)
definition [simp]: "op_ASSERT_bind I m ≡ Refine_Basic.bind (ASSERT I) (λ_. m)"
lemma pat_ASSERT_bind[def_pat_rules]:
"Refine_Basic.bind$(ASSERT$I)$(λ⇩2_. m) ≡ UNPROTECT (op_ASSERT_bind I)$m"
by simp
term "PR_CONST (op_ASSERT_bind I)"
lemma id_op_ASSERT_bind[id_rules]:
"PR_CONST (op_ASSERT_bind I) ::⇩i TYPE('a nres ⇒ 'a nres)"
by simp
lemma arity_ASSERT_bind[sepref_monadify_arity]:
"PR_CONST (op_ASSERT_bind I) ≡ λ⇩2m. SP (PR_CONST (op_ASSERT_bind I))$m"
apply (rule eq_reflection)
by auto
lemma hn_ASSERT_bind[sepref_comb_rules]:
assumes "I ⟹ hn_refine Γ c Γ' R CP m"
shows "hn_refine Γ c Γ' R CP (PR_CONST (op_ASSERT_bind I)$m)"
using assms
apply (cases I)
apply auto
done
definition [simp]: "op_ASSUME_bind I m ≡ Refine_Basic.bind (ASSUME I) (λ_. m)"
lemma pat_ASSUME_bind[def_pat_rules]:
"Refine_Basic.bind$(ASSUME$I)$(λ⇩2_. m) ≡ UNPROTECT (op_ASSUME_bind I)$m"
by simp
lemma id_op_ASSUME_bind[id_rules]:
"PR_CONST (op_ASSUME_bind I) ::⇩i TYPE('a nres ⇒ 'a nres)"
by simp
lemma arity_ASSUME_bind[sepref_monadify_arity]:
"PR_CONST (op_ASSUME_bind I) ≡ λ⇩2m. SP (PR_CONST (op_ASSUME_bind I))$m"
apply (rule eq_reflection)
by auto
lemma hn_ASSUME_bind[sepref_comb_rules]:
assumes "vassn_tag Γ ⟹ I"
assumes "I ⟹ hn_refine Γ c Γ' R CP m"
shows "hn_refine Γ c Γ' R CP (PR_CONST (op_ASSUME_bind I)$m)"
apply (rule hn_refine_preI)
using assms
apply (cases I)
apply (auto simp: vassn_tag_def)
done
text ‹Manual deallocation. Frees data before its variable goes out of scope›
definition "mop_free x ≡ RETURN ()"
sepref_register mop_free
lemma mop_free_hnr[sepref_fr_rules]:
assumes "MK_FREE R f"
shows "(f,mop_free)∈R⇧d→⇩a⇩d(λ_. unit_assn)"
unfolding mop_free_def
apply (rule hfrefI)
apply (rule hn_refineI)
apply (rule htriple_pure_preI)
apply (clarsimp
simp: hn_ctxt_def pure_def sep_algebra_simps invalid_assn_def)
supply [vcg_rules] = MK_FREED[OF assms]
by vcg
subsection "Import of Parametricity Theorems"
lemma pure_hn_refineI:
assumes "Q ⟶ (c,a)∈R"
shows "hn_refine (↑Q) (Mreturn c) (↑Q) (pure R) (λ_. True) (RETURN a)"
unfolding hn_refine_def pure_def using assms by vcg
lemma pure_hn_refineI_no_asm:
assumes "(c,a)∈R"
shows "hn_refine □ (Mreturn c) □ (pure R) (λ_. True) (RETURN a)"
unfolding hn_refine_def pure_def using assms by vcg
lemma import_param_0:
"(P⟹Q) ≡ Trueprop (PROTECT P ⟶ Q)"
apply (rule, simp+)+
done
lemma import_param_1:
"(P⟹Q) ≡ Trueprop (P⟶Q)"
"(P⟶Q⟶R) ⟷ (P∧Q ⟶ R)"
"PROTECT (P ∧ Q) ≡ PROTECT P ∧ PROTECT Q"
"(P ∧ Q) ∧ R ≡ P ∧ Q ∧ R"
"(a,c)∈Rel ∧ PROTECT P ⟷ PROTECT P ∧ (a,c)∈Rel"
apply (rule, simp+)+
done
lemma import_param_2:
"Trueprop (PROTECT P ∧ Q ⟶ R) ≡ (P ⟹ Q⟶R)"
apply (rule, simp+)+
done
lemma import_param_3:
"↑(P ∧ Q) = (↑P**↑Q)"
"↑((c,a)∈R) = hn_val R a c"
by (simp_all add: hn_ctxt_def pure_def sep_algebra_simps)
named_theorems_rev sepref_import_rewrite ‹Rewrite rules on importing parametricity theorems›
lemma to_import_frefD:
assumes "(f,g)∈fref P R S"
shows "⟦PROTECT (P y); (x,y)∈R⟧ ⟹ (f x, g y)∈S y"
using assms
unfolding fref_def
by auto
lemma add_PR_CONST: "(c,a)∈R ⟹ (c,PR_CONST a)∈R" by simp
ML ‹
structure Sepref_Import_Param = struct
fun to_import_fo ctxt thm = let
val unf_thms = @{thms
split_tupled_all prod_rel_simp uncurry_apply cnv_conj_to_meta Product_Type.split}
in
case Thm.concl_of thm of
@{mpat "Trueprop ((_,_) ∈ fref _ _ _)"} =>
(@{thm to_import_frefD} OF [thm])
|> Thm.forall_intr_vars
|> Local_Defs.unfold0 ctxt unf_thms
|> Variable.gen_all ctxt
| @{mpat "Trueprop ((_,_) ∈ _)"} =>
Parametricity.fo_rule thm
| _ => raise THM("Expected parametricity or fref theorem",~1,[thm])
end
fun add_PR_CONST thm = case Thm.concl_of thm of
@{mpat "Trueprop ((_,_) ∈ fref _ _ _)"} => thm
| @{mpat "Trueprop ((_,PR_CONST _) ∈ _)"} => thm
| @{mpat "Trueprop ((_,?a) ∈ _)"} => if is_Const a orelse is_Free a orelse is_Var a then
thm
else
thm RS @{thm add_PR_CONST}
| _ => thm
fun import ctxt thm = let
open Sepref_Basic
val thm = thm
|> Conv.fconv_rule Thm.eta_conversion
|> add_PR_CONST
|> Local_Defs.unfold0 ctxt @{thms import_param_0}
|> Local_Defs.unfold0 ctxt @{thms imp_to_meta}
|> to_import_fo ctxt
|> Local_Defs.unfold0 ctxt @{thms import_param_1}
|> Local_Defs.unfold0 ctxt @{thms import_param_2}
val thm = case Thm.concl_of thm of
@{mpat "Trueprop (_⟶_)"} => thm RS @{thm pure_hn_refineI}
| _ => thm RS @{thm pure_hn_refineI_no_asm}
val thm = Local_Defs.unfold0 ctxt @{thms import_param_3} thm
|> Conv.fconv_rule (hn_refine_concl_conv_a (K (Id_Op.protect_conv ctxt)) ctxt)
val thm = Local_Defs.unfold0 ctxt (Named_Theorems_Rev.get ctxt @{named_theorems_rev sepref_import_rewrite}) thm
val thm = Sepref_Rules.add_pure_constraints_rule ctxt thm
in
thm
end
val import_attr = Scan.succeed (Thm.mixed_attribute (fn (context,thm) =>
let
val thm = import (Context.proof_of context) thm
val context = Sepref_Translate.sepref_fr_rules.add_thm thm context
in (context,thm) end
))
val import_attr_rl = Scan.succeed (Thm.rule_attribute [] (fn context =>
import (Context.proof_of context) #> Sepref_Rules.ensure_hfref (Context.proof_of context)
))
val setup = I
#> Attrib.setup @{binding sepref_import_param} import_attr
"Sepref: Import parametricity rule"
#> Attrib.setup @{binding sepref_param} import_attr_rl
"Sepref: Transform parametricity rule to sepref rule"
#> Attrib.setup @{binding sepref_dbg_import_rl_only}
(Scan.succeed (Thm.rule_attribute [] (import o Context.proof_of)))
"Sepref: Parametricity to hnr-rule, no conversion to hfref"
end
›
setup Sepref_Import_Param.setup
subsection "Purity"
definition "import_rel1 R ≡ λA c ci. ↑(is_pure A ∧ (ci,c)∈⟨the_pure A⟩R)"
definition "import_rel2 R ≡ λA B c ci. ↑(is_pure A ∧ is_pure B ∧ (ci,c)∈⟨the_pure A, the_pure B⟩R)"
lemma import_rel1_pure_conv: "import_rel1 R (pure A) = pure (⟨A⟩R)"
unfolding import_rel1_def
apply simp
apply (simp add: pure_def)
done
lemma import_rel2_pure_conv: "import_rel2 R (pure A) (pure B) = pure (⟨A,B⟩R)"
unfolding import_rel2_def
apply simp
apply (simp add: pure_def)
done
lemmas [safe_constraint_rules] = single_valued_Id br_sv
end