diff --git a/thys/Refine_Imperative_HOL/Sepref_Rules.thy b/thys/Refine_Imperative_HOL/Sepref_Rules.thy --- a/thys/Refine_Imperative_HOL/Sepref_Rules.thy +++ b/thys/Refine_Imperative_HOL/Sepref_Rules.thy @@ -1,1745 +1,1745 @@ section \Refinement Rule Management\ theory Sepref_Rules imports Sepref_Basic Sepref_Constraints begin text \This theory contains tools for managing the refinement rules used by Sepref\ text \The theories are based on uncurried functions, i.e., every function has type @{typ "'a\'b"}, where @{typ 'a} is the tuple of parameters, or unit if there are none. \ subsection \Assertion Interface Binding\ text \Binding of interface types to refinement assertions\ definition intf_of_assn :: "('a \ _ \ assn) \ 'b itself \ bool" where [simp]: "intf_of_assn a b = True" lemma intf_of_assnI: "intf_of_assn R TYPE('a)" by simp named_theorems_rev intf_of_assn \Links between refinement assertions and interface types\ lemma intf_of_assn_fallback: "intf_of_assn (R :: 'a \ _ \ assn) TYPE('a)" by simp subsection \Function Refinement with Precondition\ definition fref :: "('c \ bool) \ ('a \ 'c) set \ ('b \ 'd) set \ (('a \ 'b) \ ('c \ 'd)) set" ("[_]\<^sub>f _ \ _" [0,60,60] 60) where "[P]\<^sub>f R \ S \ {(f,g). \x y. P y \ (x,y)\R \ (f x, g y)\S}" abbreviation freft ("_ \\<^sub>f _" [60,60] 60) where "R \\<^sub>f S \ ([\_. True]\<^sub>f R \ S)" lemma rel2p_fref[rel2p]: "rel2p (fref P R S) = (\f g. (\x y. P y \ rel2p R x y \ rel2p S (f x) (g y)))" by (auto simp: fref_def rel2p_def[abs_def]) lemma fref_cons: assumes "(f,g) \ [P]\<^sub>f R \ S" assumes "\c a. (c,a)\R' \ Q a \ P a" assumes "R' \ R" assumes "S \ S'" shows "(f,g) \ [Q]\<^sub>f R' \ S'" using assms unfolding fref_def by fastforce lemmas fref_cons' = fref_cons[OF _ _ order_refl order_refl] lemma frefI[intro?]: assumes "\x y. \P y; (x,y)\R\ \ (f x, g y)\S" shows "(f,g)\fref P R S" using assms unfolding fref_def by auto lemma fref_ncI: "(f,g)\R\S \ (f,g)\R\\<^sub>fS" apply (rule frefI) apply parametricity done lemma frefD: assumes "(f,g)\fref P R S" shows "\P y; (x,y)\R\ \ (f x, g y)\S" using assms unfolding fref_def by auto lemma fref_ncD: "(f,g)\R\\<^sub>fS \ (f,g)\R\S" apply (rule fun_relI) apply (drule frefD) apply simp apply assumption+ done lemma fref_compI: "fref P R1 R2 O fref Q S1 S2 \ fref (\x. Q x \ (\y. (y,x)\S1 \ P y)) (R1 O S1) (R2 O S2)" unfolding fref_def apply (auto) apply blast done lemma fref_compI': "\ (f,g)\fref P R1 R2; (g,h)\fref Q S1 S2 \ \ (f,h) \ fref (\x. Q x \ (\y. (y,x)\S1 \ P y)) (R1 O S1) (R2 O S2)" using fref_compI[of P R1 R2 Q S1 S2] by auto lemma fref_unit_conv: "(\_. c, \_. a) \ fref P unit_rel S \ (P () \ (c,a)\S)" by (auto simp: fref_def) lemma fref_uncurry_conv: "(uncurry c, uncurry a) \ fref P (R1\\<^sub>rR2) S \ (\x1 y1 x2 y2. P (y1,y2) \ (x1,y1)\R1 \ (x2,y2)\R2 \ (c x1 x2, a y1 y2) \ S)" by (auto simp: fref_def) lemma fref_mono: "\ \x. P' x \ P x; R' \ R; S \ S' \ \ fref P R S \ fref P' R' S'" unfolding fref_def by auto blast lemma fref_composeI: assumes FR1: "(f,g)\fref P R1 R2" assumes FR2: "(g,h)\fref Q S1 S2" assumes C1: "\x. P' x \ Q x" assumes C2: "\x y. \P' x; (y,x)\S1\ \ P y" assumes R1: "R' \ R1 O S1" assumes R2: "R2 O S2 \ S'" assumes FH: "f'=f" "h'=h" shows "(f',h') \ fref P' R' S'" unfolding FH apply (rule subsetD[OF fref_mono fref_compI'[OF FR1 FR2]]) using C1 C2 apply blast using R1 apply blast using R2 apply blast done lemma fref_triv: "A\Id \ (f,f)\[P]\<^sub>f A \ Id" by (auto simp: fref_def) subsection \Heap-Function Refinement\ text \ The following relates a heap-function with a pure function. It contains a precondition, a refinement assertion for the arguments before and after execution, and a refinement relation for the result. \ (* TODO: We only use this with keep/destroy information, so we could model the parameter relations as such (('a\'ai \ assn) \ bool) *) definition hfref :: " ('a \ bool) \ (('a \ 'ai \ assn) \ ('a \ 'ai \ assn)) \ ('b \ 'bi \ assn) \ (('ai \ 'bi Heap) \ ('a\'b nres)) set" ("[_]\<^sub>a _ \ _" [0,60,60] 60) where "[P]\<^sub>a RS \ T \ { (f,g) . \c a. P a \ hn_refine (fst RS a c) (f c) (snd RS a c) T (g a)}" abbreviation hfreft ("_ \\<^sub>a _" [60,60] 60) where "RS \\<^sub>a T \ ([\_. True]\<^sub>a RS \ T)" lemma hfrefI[intro?]: assumes "\c a. P a \ hn_refine (fst RS a c) (f c) (snd RS a c) T (g a)" shows "(f,g)\hfref P RS T" using assms unfolding hfref_def by blast lemma hfrefD: assumes "(f,g)\hfref P RS T" shows "\c a. P a \ hn_refine (fst RS a c) (f c) (snd RS a c) T (g a)" using assms unfolding hfref_def by blast lemma hfref_to_ASSERT_conv: "NO_MATCH (\_. True) P \ (a,b)\[P]\<^sub>a R \ S \ (a,\x. ASSERT (P x) \ b x) \ R \\<^sub>a S" unfolding hfref_def apply (clarsimp; safe; clarsimp?) apply (rule hn_refine_nofailI) apply (simp add: refine_pw_simps) subgoal for xc xa apply (drule spec[of _ xc]) apply (drule spec[of _ xa]) by simp done text \ A pair of argument refinement assertions can be created by the input assertion and the information whether the parameter is kept or destroyed by the function. \ primrec hf_pres :: "('a \ 'b \ assn) \ bool \ ('a \ 'b \ assn)\('a \ 'b \ assn)" where "hf_pres R True = (R,R)" | "hf_pres R False = (R,invalid_assn R)" abbreviation hfkeep :: "('a \ 'b \ assn) \ ('a \ 'b \ assn)\('a \ 'b \ assn)" ("(_\<^sup>k)" [1000] 999) where "R\<^sup>k \ hf_pres R True" abbreviation hfdrop :: "('a \ 'b \ assn) \ ('a \ 'b \ assn)\('a \ 'b \ assn)" ("(_\<^sup>d)" [1000] 999) where "R\<^sup>d \ hf_pres R False" abbreviation "hn_kede R kd \ hn_ctxt (snd (hf_pres R kd))" abbreviation "hn_keep R \ hn_kede R True" abbreviation "hn_dest R \ hn_kede R False" lemma keep_drop_sels[simp]: "fst (R\<^sup>k) = R" "snd (R\<^sup>k) = R" "fst (R\<^sup>d) = R" "snd (R\<^sup>d) = invalid_assn R" by auto lemma hf_pres_fst[simp]: "fst (hf_pres R k) = R" by (cases k) auto text \ The following operator combines multiple argument assertion-pairs to argument assertion-pairs for the product. It is required to state argument assertion-pairs for uncurried functions. \ definition hfprod :: " (('a \ 'b \ assn)\('a \ 'b \ assn)) \ (('c \ 'd \ assn)\('c \ 'd \ assn)) \ ((('a\'c) \ ('b \ 'd) \ assn) \ (('a\'c) \ ('b \ 'd) \ assn))" (infixl "*\<^sub>a" 65) where "RR *\<^sub>a SS \ (prod_assn (fst RR) (fst SS), prod_assn (snd RR) (snd SS))" lemma hfprod_fst_snd[simp]: "fst (A *\<^sub>a B) = prod_assn (fst A) (fst B)" "snd (A *\<^sub>a B) = prod_assn (snd A) (snd B)" unfolding hfprod_def by auto subsubsection \Conversion from fref to hfref\ (* TODO: Variant of import-param! Automate this! *) lemma fref_to_pure_hfref': assumes "(f,g) \ [P]\<^sub>f R\\S\nres_rel" assumes "\x. x\Domain R \ R\``Collect P \ f x = RETURN (f' x)" shows "(return o f', g) \ [P]\<^sub>a (pure R)\<^sup>k\pure S" apply (rule hfrefI) apply (rule hn_refineI) using assms apply ((sep_auto simp: fref_def pure_def pw_le_iff pw_nres_rel_iff refine_pw_simps eintros del: exI)) apply force done subsubsection \Conversion from hfref to hnr\ text \This section contains the lemmas. The ML code is further down. \ lemma hf2hnr: assumes "(f,g) \ [P]\<^sub>a R \ S" shows "\x xi. P x \ hn_refine (emp * hn_ctxt (fst R) x xi) (f$xi) (emp * hn_ctxt (snd R) x xi) S (g$x)" using assms unfolding hfref_def by (auto simp: hn_ctxt_def) (*lemma hf2hnr_new: assumes "(f,g) \ [P]\<^sub>a R \ S" shows "\x xi. (\h. h\fst R x xi \ P x) \ hn_refine (emp * hn_ctxt (fst R) x xi) (f xi) (emp * hn_ctxt (snd R) x xi) S (g$x)" using assms unfolding hfref_def by (auto simp: hn_ctxt_def intro: hn_refine_preI) *) (* Products that stem from currying are tagged by a special refinement relation *) definition [simp]: "to_hnr_prod \ prod_assn" lemma to_hnr_prod_fst_snd: "fst (A *\<^sub>a B) = to_hnr_prod (fst A) (fst B)" "snd (A *\<^sub>a B) = to_hnr_prod (snd A) (snd B)" unfolding hfprod_def by auto (* Warning: This lemma is carefully set up to be applicable as an unfold rule, for more than one level of uncurrying*) lemma hnr_uncurry_unfold: " (\x xi. P x \ hn_refine (\ * hn_ctxt (to_hnr_prod A B) x xi) (fi xi) (\' * hn_ctxt (to_hnr_prod A' B') x xi) R (f x)) \ (\b bi a ai. P (a,b) \ hn_refine (\ * hn_ctxt B b bi * hn_ctxt A a ai) (fi (ai,bi)) (\' * hn_ctxt B' b bi * hn_ctxt A' a ai) R (f (a,b)) )" by (auto simp: hn_ctxt_def prod_assn_def star_aci) lemma hnr_intro_dummy: "\x xi. P x \ hn_refine (\ x xi) (c xi) (\' x xi) R (a x) \ \x xi. P x \ hn_refine (emp*\ x xi) (c xi) (emp*\' x xi) R (a x)" by simp lemma hn_ctxt_ctxt_fix_conv: "hn_ctxt (hn_ctxt R) = hn_ctxt R" by (simp add: hn_ctxt_def[abs_def]) lemma uncurry_APP: "uncurry f$(a,b) = f$a$b" by auto (* TODO: Replace by more general rule. *) lemma norm_RETURN_o: "\f. (RETURN o f)$x = (RETURN$(f$x))" "\f. (RETURN oo f)$x$y = (RETURN$(f$x$y))" "\f. (RETURN ooo f)$x$y$z = (RETURN$(f$x$y$z))" "\f. (\x. RETURN ooo f x)$x$y$z$a = (RETURN$(f$x$y$z$a))" "\f. (\x y. RETURN ooo f x y)$x$y$z$a$b = (RETURN$(f$x$y$z$a$b))" by auto lemma norm_return_o: "\f. (return o f)$x = (return$(f$x))" "\f. (return oo f)$x$y = (return$(f$x$y))" "\f. (return ooo f)$x$y$z = (return$(f$x$y$z))" "\f. (\x. return ooo f x)$x$y$z$a = (return$(f$x$y$z$a))" "\f. (\x y. return ooo f x y)$x$y$z$a$b = (return$(f$x$y$z$a$b))" by auto lemma hn_val_unit_conv_emp[simp]: "hn_val unit_rel x y = emp" by (auto simp: hn_ctxt_def pure_def) subsubsection \Conversion from hnr to hfref\ text \This section contains the lemmas. The ML code is further down. \ abbreviation "id_assn \ pure Id" abbreviation "unit_assn \ id_assn :: unit \ _" lemma pure_unit_rel_eq_empty: "unit_assn x y = emp" by (auto simp: pure_def) lemma uc_hfprod_sel: "fst (A *\<^sub>a B) a c = (case (a,c) of ((a1,a2),(c1,c2)) \ fst A a1 c1 * fst B a2 c2)" "snd (A *\<^sub>a B) a c = (case (a,c) of ((a1,a2),(c1,c2)) \ snd A a1 c1 * snd B a2 c2)" unfolding hfprod_def prod_assn_def[abs_def] by auto subsubsection \Conversion from relation to fref\ text \This section contains the lemmas. The ML code is further down. \ definition "CURRY R \ { (f,g). (uncurry f, uncurry g) \ R }" lemma fref_param1: "R\S = fref (\_. True) R S" by (auto simp: fref_def fun_relD) lemma fref_nest: "fref P1 R1 (fref P2 R2 S) \ CURRY (fref (\(a,b). P1 a \ P2 b) (R1\\<^sub>rR2) S)" apply (rule eq_reflection) by (auto simp: fref_def CURRY_def) lemma in_CURRY_conv: "(f,g) \ CURRY R \ (uncurry f, uncurry g) \ R" unfolding CURRY_def by auto lemma uncurry0_APP[simp]: "uncurry0 c $ x = c" by auto lemma fref_param0I: "(c,a)\R \ (uncurry0 c, uncurry0 a) \ fref (\_. True) unit_rel R" by (auto simp: fref_def) subsubsection \Composition\ definition hr_comp :: "('b \ 'c \ assn) \ ('b \ 'a) set \ 'a \ 'c \ assn" \ \Compose refinement assertion with refinement relation\ where "hr_comp R1 R2 a c \ \\<^sub>Ab. R1 b c * \((b,a)\R2)" definition hrp_comp :: "('d \ 'b \ assn) \ ('d \ 'c \ assn) \ ('d \ 'a) set \ ('a \ 'b \ assn) \ ('a \ 'c \ assn)" \ \Compose argument assertion-pair with refinement relation\ where "hrp_comp RR' S \ (hr_comp (fst RR') S, hr_comp (snd RR') S) " lemma hr_compI: "(b,a)\R2 \ R1 b c \\<^sub>A hr_comp R1 R2 a c" unfolding hr_comp_def by sep_auto lemma hr_comp_Id1[simp]: "hr_comp (pure Id) R = pure R" unfolding hr_comp_def[abs_def] pure_def apply (intro ext ent_iffI) by sep_auto+ lemma hr_comp_Id2[simp]: "hr_comp R Id = R" unfolding hr_comp_def[abs_def] apply (intro ext ent_iffI) by sep_auto+ (*lemma hr_comp_invalid[simp]: "hr_comp (\a c. true) R a c = true * \(\b. (b,a)\R)" unfolding hr_comp_def[abs_def] apply (intro ext ent_iffI) apply sep_auto+ done*) lemma hr_comp_emp[simp]: "hr_comp (\a c. emp) R a c = \(\b. (b,a)\R)" unfolding hr_comp_def[abs_def] apply (intro ext ent_iffI) apply sep_auto+ done lemma hr_comp_prod_conv[simp]: "hr_comp (prod_assn Ra Rb) (Ra' \\<^sub>r Rb') = prod_assn (hr_comp Ra Ra') (hr_comp Rb Rb')" unfolding hr_comp_def[abs_def] prod_assn_def[abs_def] apply (intro ext ent_iffI) apply solve_entails apply clarsimp apply sep_auto apply clarsimp apply (intro ent_ex_preI) apply (rule ent_ex_postI) apply (sep_auto split: prod.splits) done lemma hr_comp_pure: "hr_comp (pure R) S = pure (R O S)" apply (intro ext) apply (rule ent_iffI) unfolding hr_comp_def[abs_def] apply (sep_auto simp: pure_def)+ done lemma hr_comp_is_pure[safe_constraint_rules]: "is_pure A \ is_pure (hr_comp A B)" by (auto simp: hr_comp_pure is_pure_conv) lemma hr_comp_the_pure: "is_pure A \ the_pure (hr_comp A B) = the_pure A O B" unfolding is_pure_conv by (clarsimp simp: hr_comp_pure) lemma rdomp_hrcomp_conv: "rdomp (hr_comp A R) x \ (\y. rdomp A y \ (y,x)\R)" by (auto simp: rdomp_def hr_comp_def) lemma hn_rel_compI: "\nofail a; (b,a)\\R2\nres_rel\ \ hn_rel R1 b c \\<^sub>A hn_rel (hr_comp R1 R2) a c" unfolding hr_comp_def hn_rel_def nres_rel_def apply (clarsimp intro!: ent_ex_preI) apply (drule (1) order_trans) apply (simp add: ret_le_down_conv) by sep_auto lemma hr_comp_precise[constraint_rules]: assumes [safe_constraint_rules]: "precise R" assumes SV: "single_valued S" shows "precise (hr_comp R S)" apply (rule preciseI) unfolding hr_comp_def apply clarsimp by (metis SV assms(1) preciseD single_valuedD) lemma hr_comp_assoc: "hr_comp (hr_comp R S) T = hr_comp R (S O T)" apply (intro ext) unfolding hr_comp_def apply (rule ent_iffI; clarsimp) apply sep_auto apply (rule ent_ex_preI; clarsimp) (* TODO: sep_auto/solve_entails is too eager splitting the subgoal here! *) apply sep_auto done lemma hnr_comp: assumes R: "\b1 c1. P b1 \ hn_refine (R1 b1 c1 * \) (c c1) (R1p b1 c1 * \') R (b b1)" assumes S: "\a1 b1. \Q a1; (b1,a1)\R1'\ \ (b b1,a a1)\\R'\nres_rel" assumes PQ: "\a1 b1. \Q a1; (b1,a1)\R1'\ \ P b1" assumes Q: "Q a1" shows "hn_refine (hr_comp R1 R1' a1 c1 * \) (c c1) (hr_comp R1p R1' a1 c1 * \') (hr_comp R R') (a a1)" unfolding hn_refine_alt proof clarsimp assume NF: "nofail (a a1)" show " > c c1 <\r. hn_rel (hr_comp R R') (a a1) r * (hr_comp R1p R1' a1 c1 * \')>\<^sub>t" apply (subst hr_comp_def) apply (clarsimp intro!: norm_pre_ex_rule) proof - fix b1 assume R1: "(b1, a1) \ R1'" from S R1 Q have R': "(b b1, a a1) \ \R'\nres_rel" by blast with NF have NFB: "nofail (b b1)" by (simp add: nres_rel_def pw_le_iff refine_pw_simps) from PQ R1 Q have P: "P b1" by blast with NFB R have "> c c1 <\r. hn_rel R (b b1) r * (R1p b1 c1 * \')>\<^sub>t" unfolding hn_refine_alt by auto thus "> c c1 <\r. hn_rel (hr_comp R R') (a a1) r * (hr_comp R1p R1' a1 c1 * \')>\<^sub>t" apply (rule cons_post_rule) apply (solve_entails) by (intro ent_star_mono hn_rel_compI[OF NF R'] hr_compI[OF R1] ent_refl) qed qed lemma hnr_comp1_aux: assumes R: "\b1 c1. P b1 \ hn_refine (hn_ctxt R1 b1 c1) (c c1) (hn_ctxt R1p b1 c1) R (b$b1)" assumes S: "\a1 b1. \Q a1; (b1,a1)\R1'\ \ (b$b1,a$a1)\\R'\nres_rel" assumes PQ: "\a1 b1. \Q a1; (b1,a1)\R1'\ \ P b1" assumes Q: "Q a1" shows "hn_refine (hr_comp R1 R1' a1 c1) (c c1) (hr_comp R1p R1' a1 c1) (hr_comp R R') (a a1)" using assms hnr_comp[where \=emp and \'=emp and a=a and b=b and c=c and P=P and Q=Q] unfolding hn_ctxt_def by auto lemma hfcomp: assumes A: "(f,g) \ [P]\<^sub>a RR' \ S" assumes B: "(g,h) \ [Q]\<^sub>f T \ \U\nres_rel" shows "(f,h) \ [\a. Q a \ (\a'. (a',a)\T \ P a')]\<^sub>a hrp_comp RR' T \ hr_comp S U" using assms unfolding fref_def hfref_def hrp_comp_def apply clarsimp apply (rule hnr_comp1_aux[of P "fst RR'" f "snd RR'" S g "\a. Q a \ (\a'. (a',a)\T \ P a')" T h U]) apply (auto simp: hn_ctxt_def) done lemma hfref_weaken_pre_nofail: assumes "(f,g) \ [P]\<^sub>a R \ S" shows "(f,g) \ [\x. nofail (g x) \ P x]\<^sub>a R \ S" using assms unfolding hfref_def hn_refine_def by auto lemma hfref_cons: assumes "(f,g) \ [P]\<^sub>a R \ S" assumes "\x. P' x \ P x" assumes "\x y. fst R' x y \\<^sub>t fst R x y" assumes "\x y. snd R x y \\<^sub>t snd R' x y" assumes "\x y. S x y \\<^sub>t S' x y" shows "(f,g) \ [P']\<^sub>a R' \ S'" unfolding hfref_def apply clarsimp apply (rule hn_refine_cons) apply (rule assms(3)) defer apply (rule entt_trans[OF assms(4)]; sep_auto) apply (rule assms(5)) apply (frule assms(2)) using assms(1) unfolding hfref_def apply auto done subsubsection \Composition Automation\ text \This section contains the lemmas. The ML code is further down. \ lemma prod_hrp_comp: "hrp_comp (A *\<^sub>a B) (C \\<^sub>r D) = hrp_comp A C *\<^sub>a hrp_comp B D" unfolding hrp_comp_def hfprod_def by simp lemma hrp_comp_keep: "hrp_comp (A\<^sup>k) B = (hr_comp A B)\<^sup>k" by (auto simp: hrp_comp_def) lemma hr_comp_invalid: "hr_comp (invalid_assn R1) R2 = invalid_assn (hr_comp R1 R2)" apply (intro ent_iffI entailsI ext) unfolding invalid_assn_def hr_comp_def by auto lemma hrp_comp_dest: "hrp_comp (A\<^sup>d) B = (hr_comp A B)\<^sup>d" by (auto simp: hrp_comp_def hr_comp_invalid) definition "hrp_imp RR RR' \ \a b. (fst RR' a b \\<^sub>t fst RR a b) \ (snd RR a b \\<^sub>t snd RR' a b)" lemma hfref_imp: "hrp_imp RR RR' \ [P]\<^sub>a RR \ S \ [P]\<^sub>a RR' \ S" apply clarsimp apply (erule hfref_cons) apply (simp_all add: hrp_imp_def) done lemma hrp_imp_refl: "hrp_imp RR RR" unfolding hrp_imp_def by auto lemma hrp_imp_reflI: "RR = RR' \ hrp_imp RR RR'" unfolding hrp_imp_def by auto lemma hrp_comp_cong: "hrp_imp A A' \ B=B' \ hrp_imp (hrp_comp A B) (hrp_comp A' B')" by (sep_auto simp: hrp_imp_def hrp_comp_def hr_comp_def entailst_def) lemma hrp_prod_cong: "hrp_imp A A' \ hrp_imp B B' \ hrp_imp (A*\<^sub>aB) (A'*\<^sub>aB')" by (sep_auto simp: hrp_imp_def prod_assn_def intro: entt_star_mono) lemma hrp_imp_trans: "hrp_imp A B \ hrp_imp B C \ hrp_imp A C" unfolding hrp_imp_def by (fastforce intro: entt_trans) lemma fcomp_norm_dflt_init: "x\[P]\<^sub>a R \ T \ hrp_imp R S \ x\[P]\<^sub>a S \ T" apply (erule rev_subsetD) by (rule hfref_imp) definition "comp_PRE R P Q S \ \x. S x \ (P x \ (\y. (y,x)\R \ Q x y))" lemma comp_PRE_cong[cong]: assumes "R\R'" assumes "\x. P x \ P' x" assumes "\x. S x \ S' x" assumes "\x y. \P x; (y,x)\R; y\Domain R; S' x \ \ Q x y \ Q' x y" shows "comp_PRE R P Q S \ comp_PRE R' P' Q' S'" using assms by (fastforce simp: comp_PRE_def intro!: eq_reflection ext) lemma fref_compI_PRE: "\ (f,g)\fref P R1 R2; (g,h)\fref Q S1 S2 \ \ (f,h) \ fref (comp_PRE S1 Q (\_. P) (\_. True)) (R1 O S1) (R2 O S2)" using fref_compI[of P R1 R2 Q S1 S2] unfolding comp_PRE_def by auto lemma PRE_D1: "(Q x \ P x) \ comp_PRE S1 Q (\x _. P x) S x" by (auto simp: comp_PRE_def) lemma PRE_D2: "(Q x \ (\y. (y,x)\S1 \ S x \ P x y)) \ comp_PRE S1 Q P S x" by (auto simp: comp_PRE_def) lemma fref_weaken_pre: assumes "\x. P x \ P' x" assumes "(f,h) \ fref P' R S" shows "(f,h) \ fref P R S" apply (rule rev_subsetD[OF assms(2) fref_mono]) using assms(1) by auto lemma fref_PRE_D1: assumes "(f,h) \ fref (comp_PRE S1 Q (\x _. P x) X) R S" shows "(f,h) \ fref (\x. Q x \ P x) R S" by (rule fref_weaken_pre[OF PRE_D1 assms]) lemma fref_PRE_D2: assumes "(f,h) \ fref (comp_PRE S1 Q P X) R S" shows "(f,h) \ fref (\x. Q x \ (\y. (y,x)\S1 \ X x \ P x y)) R S" by (rule fref_weaken_pre[OF PRE_D2 assms]) lemmas fref_PRE_D = fref_PRE_D1 fref_PRE_D2 lemma hfref_weaken_pre: assumes "\x. P x \ P' x" assumes "(f,h) \ hfref P' R S" shows "(f,h) \ hfref P R S" using assms by (auto simp: hfref_def) lemma hfref_weaken_pre': assumes "\x. \P x; rdomp (fst R) x\ \ P' x" assumes "(f,h) \ hfref P' R S" shows "(f,h) \ hfref P R S" apply (rule hfrefI) apply (rule hn_refine_preI) using assms by (auto simp: hfref_def rdomp_def) lemma hfref_weaken_pre_nofail': assumes "(f,g) \ [P]\<^sub>a R \ S" assumes "\x. \nofail (g x); Q x\ \ P x" shows "(f,g) \ [Q]\<^sub>a R \ S" apply (rule hfref_weaken_pre[OF _ assms(1)[THEN hfref_weaken_pre_nofail]]) using assms(2) by blast lemma hfref_compI_PRE_aux: assumes A: "(f,g) \ [P]\<^sub>a RR' \ S" assumes B: "(g,h) \ [Q]\<^sub>f T \ \U\nres_rel" shows "(f,h) \ [comp_PRE T Q (\_. P) (\_. True)]\<^sub>a hrp_comp RR' T \ hr_comp S U" apply (rule hfref_weaken_pre[OF _ hfcomp[OF A B]]) by (auto simp: comp_PRE_def) lemma hfref_compI_PRE: assumes A: "(f,g) \ [P]\<^sub>a RR' \ S" assumes B: "(g,h) \ [Q]\<^sub>f T \ \U\nres_rel" shows "(f,h) \ [comp_PRE T Q (\x y. P y) (\x. nofail (h x))]\<^sub>a hrp_comp RR' T \ hr_comp S U" using hfref_compI_PRE_aux[OF A B, THEN hfref_weaken_pre_nofail] apply (rule hfref_weaken_pre[rotated]) apply (auto simp: comp_PRE_def) done lemma hfref_PRE_D1: assumes "(f,h) \ hfref (comp_PRE S1 Q (\x _. P x) X) R S" shows "(f,h) \ hfref (\x. Q x \ P x) R S" by (rule hfref_weaken_pre[OF PRE_D1 assms]) lemma hfref_PRE_D2: assumes "(f,h) \ hfref (comp_PRE S1 Q P X) R S" shows "(f,h) \ hfref (\x. Q x \ (\y. (y,x)\S1 \ X x \ P x y)) R S" by (rule hfref_weaken_pre[OF PRE_D2 assms]) lemma hfref_PRE_D3: assumes "(f,h) \ hfref (comp_PRE S1 Q P X) R S" shows "(f,h) \ hfref (comp_PRE S1 Q P X) R S" using assms . lemmas hfref_PRE_D = hfref_PRE_D1 hfref_PRE_D3 subsection \Automation\ text \Purity configuration for constraint solver\ lemmas [safe_constraint_rules] = pure_pure text \Configuration for hfref to hnr conversion\ named_theorems to_hnr_post \to_hnr converter: Postprocessing unfold rules\ lemma uncurry0_add_app_tag: "uncurry0 (RETURN c) = uncurry0 (RETURN$c)" by simp lemmas [to_hnr_post] = norm_RETURN_o norm_return_o uncurry0_add_app_tag uncurry0_apply uncurry0_APP hn_val_unit_conv_emp mult_1[of "x::assn" for x] mult_1_right[of "x::assn" for x] named_theorems to_hfref_post \to_hfref converter: Postprocessing unfold rules\ lemma prod_casesK[to_hfref_post]: "case_prod (\_ _. k) = (\_. k)" by auto lemma uncurry0_hfref_post[to_hfref_post]: "hfref (uncurry0 True) R S = hfref (\_. True) R S" apply (fo_rule arg_cong fun_cong)+ by auto (* Currently not used, we keep it in here anyway. *) text \Configuration for relation normalization after composition\ named_theorems fcomp_norm_unfold \fcomp-normalizer: Unfold theorems\ named_theorems fcomp_norm_simps \fcomp-normalizer: Simplification theorems\ named_theorems fcomp_norm_init "fcomp-normalizer: Initialization rules" named_theorems fcomp_norm_trans "fcomp-normalizer: Transitivity rules" named_theorems fcomp_norm_cong "fcomp-normalizer: Congruence rules" named_theorems fcomp_norm_norm "fcomp-normalizer: Normalization rules" named_theorems fcomp_norm_refl "fcomp-normalizer: Reflexivity rules" text \Default Setup\ lemmas [fcomp_norm_unfold] = prod_rel_comp nres_rel_comp Id_O_R R_O_Id lemmas [fcomp_norm_unfold] = hr_comp_Id1 hr_comp_Id2 lemmas [fcomp_norm_unfold] = hr_comp_prod_conv lemmas [fcomp_norm_unfold] = prod_hrp_comp hrp_comp_keep hrp_comp_dest hr_comp_pure (*lemmas [fcomp_norm_unfold] = prod_casesK uncurry0_hfref_post*) lemma [fcomp_norm_simps]: "CONSTRAINT is_pure P \ pure (the_pure P) = P" by simp lemmas [fcomp_norm_simps] = True_implies_equals lemmas [fcomp_norm_init] = fcomp_norm_dflt_init lemmas [fcomp_norm_trans] = hrp_imp_trans lemmas [fcomp_norm_cong] = hrp_comp_cong hrp_prod_cong (*lemmas [fcomp_norm_norm] = hrp_comp_dest*) lemmas [fcomp_norm_refl] = refl hrp_imp_refl lemma ensure_fref_nresI: "(f,g)\[P]\<^sub>f R\S \ (RETURN o f, RETURN o g)\[P]\<^sub>f R\\S\nres_rel" by (auto intro: nres_relI simp: fref_def) lemma ensure_fref_nres_unfold: "\f. RETURN o (uncurry0 f) = uncurry0 (RETURN f)" "\f. RETURN o (uncurry f) = uncurry (RETURN oo f)" "\f. (RETURN ooo uncurry) f = uncurry (RETURN ooo f)" by auto text \Composed precondition normalizer\ named_theorems fcomp_prenorm_simps \fcomp precondition-normalizer: Simplification theorems\ text \Support for preconditions of the form \_\Domain R\, where \R\ is the relation of the next more abstract level.\ declare DomainI[fcomp_prenorm_simps] lemma auto_weaken_pre_init_hf: assumes "\x. PROTECT P x \ P' x" assumes "(f,h) \ hfref P' R S" shows "(f,h) \ hfref P R S" using assms by (auto simp: hfref_def) lemma auto_weaken_pre_init_f: assumes "\x. PROTECT P x \ P' x" assumes "(f,h) \ fref P' R S" shows "(f,h) \ fref P R S" using assms by (auto simp: fref_def) lemmas auto_weaken_pre_init = auto_weaken_pre_init_hf auto_weaken_pre_init_f lemma auto_weaken_pre_uncurry_step: assumes "PROTECT f a \ f'" shows "PROTECT (\(x,y). f x y) (a,b) \ f' b" using assms by (auto simp: curry_def dest!: meta_eq_to_obj_eq intro!: eq_reflection) lemma auto_weaken_pre_uncurry_finish: "PROTECT f x \ f x" by (auto) lemma auto_weaken_pre_uncurry_start: assumes "P \ P'" assumes "P'\Q" shows "P\Q" using assms by (auto) lemma auto_weaken_pre_comp_PRE_I: assumes "S x \ P x" assumes "\y. \(y,x)\R; P x; S x\ \ Q x y" shows "comp_PRE R P Q S x" using assms by (auto simp: comp_PRE_def) lemma auto_weaken_pre_to_imp_nf: "(A\B\C) = (A\B \ C)" "((A\B)\C) = (A\B\C)" by auto lemma auto_weaken_pre_add_dummy_imp: "P \ True \ P" by simp text \Synthesis for hfref statements\ definition hfsynth_ID_R :: "('a \ _ \ assn) \ 'a \ bool" where [simp]: "hfsynth_ID_R _ _ \ True" lemma hfsynth_ID_R_D: fixes I :: "'a itself" assumes "hfsynth_ID_R R a" assumes "intf_of_assn R I" shows "a ::\<^sub>i I" by simp lemma hfsynth_hnr_from_hfI: assumes "\x xi. P x \ hfsynth_ID_R (fst R) x \ hn_refine (emp * hn_ctxt (fst R) x xi) (f$xi) (emp * hn_ctxt (snd R) x xi) S (g$x)" shows "(f,g) \ [P]\<^sub>a R \ S" using assms unfolding hfref_def by (auto simp: hn_ctxt_def) lemma hfsynth_ID_R_uncurry_unfold: "hfsynth_ID_R (to_hnr_prod R S) (a,b) \ hfsynth_ID_R R a \ hfsynth_ID_R S b" "hfsynth_ID_R (fst (hf_pres R k)) \ hfsynth_ID_R R" by (auto intro!: eq_reflection) ML \ signature SEPREF_RULES = sig (* Analysis of relations, both fref and fun_rel *) (* "R1\...\Rn\_" / "[_]\<^sub>f ((R1\\<^sub>rR2)...\\<^sub>rRn)" \ "[R1,...,Rn]" *) val binder_rels: term -> term list (* "_\...\_\S" / "[_]\<^sub>f _ \ S" \ "S" *) val body_rel: term -> term (* Map \/fref to (precond,args,res). NONE if no/trivial precond. *) val analyze_rel: term -> term option * term list * term (* Make trivial ("\_. True") precond *) val mk_triv_precond: term list -> term (* Make "[P]\<^sub>f ((R1\\<^sub>rR2)...\\<^sub>rRn) \ S". Insert trivial precond if NONE. *) val mk_rel: term option * term list * term -> term (* Map relation to (args,res) *) val strip_rel: term -> term list * term (* Make hfprod (op *\<^sub>a) *) val mk_hfprod : term * term -> term val mk_hfprods : term list -> term (* Determine interface type of refinement assertion, using default fallback if necessary. Use named_thms intf_of_assn for configuration. *) val intf_of_assn : Proof.context -> term -> typ (* Convert a parametricity theorem in higher-order form to uncurried fref-form. For functions without arguments, a unit-argument is added. TODO/FIXME: Currently this only works for higher-order theorems, i.e., theorems of the form (f,g)\R1\\\Rn. First-order theorems are silently treated as refinement theorems for functions with zero arguments, i.e., a unit-argument is added. *) val to_fref : Proof.context -> thm -> thm (* Convert a parametricity or fref theorem to first order form *) val to_foparam : Proof.context -> thm -> thm (* Convert schematic hfref goal to hnr-goal *) val prepare_hfref_synth_tac : Proof.context -> tactic' (* Convert theorem in hfref-form to hnr-form *) val to_hnr : Proof.context -> thm -> thm (* Convert theorem in hnr-form to hfref-form *) val to_hfref: Proof.context -> thm -> thm (* Convert theorem to given form, if not yet in this form *) val ensure_fref : Proof.context -> thm -> thm val ensure_fref_nres : Proof.context -> thm -> thm val ensure_hfref : Proof.context -> thm -> thm val ensure_hnr : Proof.context -> thm -> thm type hnr_analysis = { thm: thm, (* Original theorem, may be normalized *) precond: term, (* Precondition, abstracted over abs-arguments *) prems : term list, (* Premises not depending on arguments *) ahead: term * bool, (* Abstract function, has leading RETURN *) chead: term * bool, (* Concrete function, has leading return *) argrels: (term * bool) list, (* Argument relations, preserved (keep-flag) *) result_rel: term (* Result relation *) } val analyze_hnr: Proof.context -> thm -> hnr_analysis val pretty_hnr_analysis: Proof.context -> hnr_analysis -> Pretty.T val mk_hfref_thm: Proof.context -> hnr_analysis -> thm (* Simplify precondition of fref/hfref-theorem *) val simplify_precond: Proof.context -> thm -> thm (* Normalize hfref-theorem after composition *) val norm_fcomp_rule: Proof.context -> thm -> thm (* Replace "pure ?A" by "?A'" and is_pure constraint, then normalize *) val add_pure_constraints_rule: Proof.context -> thm -> thm (* Compose fref/hfref and fref theorem, to produce hfref theorem. The input theorems may also be in ho-param or hnr form, and are converted accordingly. *) val gen_compose : Proof.context -> thm -> thm -> thm (* FCOMP-attribute *) val fcomp_attrib: attribute context_parser end structure Sepref_Rules: SEPREF_RULES = struct local open Refine_Util Relators in fun binder_rels @{mpat "?F \ ?G"} = F::binder_rels G | binder_rels @{mpat "fref _ ?F _"} = strip_prodrel_left F | binder_rels _ = [] local fun br_aux @{mpat "_ \ ?G"} = br_aux G | br_aux R = R in fun body_rel @{mpat "fref _ _ ?G"} = G | body_rel R = br_aux R end fun strip_rel R = (binder_rels R, body_rel R) fun analyze_rel @{mpat "fref (\_. True) ?R ?S"} = (NONE,strip_prodrel_left R,S) | analyze_rel @{mpat "fref ?P ?R ?S"} = (SOME P,strip_prodrel_left R,S) | analyze_rel R = let val (args,res) = strip_rel R in (NONE,args,res) end fun mk_triv_precond Rs = absdummy (map rel_absT Rs |> list_prodT_left) @{term True} fun mk_rel (P,Rs,S) = let val R = list_prodrel_left Rs val P = case P of SOME P => P | NONE => mk_triv_precond Rs in @{mk_term "fref ?P ?R ?S"} end end fun mk_hfprod (a, b) = @{mk_term "?a*\<^sub>a?b"} local fun mk_hfprods_rev [] = @{mk_term "unit_assn\<^sup>k"} | mk_hfprods_rev [Rk] = Rk | mk_hfprods_rev (Rkn::Rks) = mk_hfprod (mk_hfprods_rev Rks, Rkn) in val mk_hfprods = mk_hfprods_rev o rev end fun intf_of_assn ctxt t = let val orig_ctxt = ctxt val (t,ctxt) = yield_singleton (Variable.import_terms false) t ctxt val v = TVar (("T",0),Proof_Context.default_sort ctxt ("T",0)) |> Logic.mk_type val goal = @{mk_term "Trueprop (intf_of_assn ?t ?v)"} val i_of_assn_rls = Named_Theorems_Rev.get ctxt @{named_theorems_rev intf_of_assn} @ @{thms intf_of_assn_fallback} fun tac ctxt = REPEAT_ALL_NEW (resolve_tac ctxt i_of_assn_rls) val thm = Goal.prove ctxt [] [] goal (fn {context,...} => ALLGOALS (tac context)) val intf = case Thm.concl_of thm of @{mpat "Trueprop (intf_of_assn _ (?v AS\<^sub>p TYPE (_)))"} => v | _ => raise THM("Intf_of_assn: Proved a different theorem?",~1,[thm]) val intf = singleton (Variable.export_terms ctxt orig_ctxt) intf |> Logic.dest_type in intf end datatype rthm_type = RT_HOPARAM (* (_,_) \ _ \ \ \ _ *) | RT_FREF (* (_,_) \ [_]\<^sub>f _ \ _ *) | RT_HNR (* hn_refine _ _ _ _ _ *) | RT_HFREF (* (_,_) \ [_]\<^sub>a _ \ _ *) | RT_OTHER fun rthm_type thm = case Thm.concl_of thm |> HOLogic.dest_Trueprop of @{mpat "(_,_) \ fref _ _ _"} => RT_FREF | @{mpat "(_,_) \ hfref _ _ _"} => RT_HFREF | @{mpat "hn_refine _ _ _ _ _"} => RT_HNR | @{mpat "(_,_) \ _"} => RT_HOPARAM (* TODO: Distinction between ho-param and fo-param *) | _ => RT_OTHER fun to_fref ctxt thm = let open Conv in case Thm.concl_of thm |> HOLogic.dest_Trueprop of @{mpat "(_,_)\_\_"} => Local_Defs.unfold0 ctxt @{thms fref_param1} thm |> fconv_rule (repeat_conv (Refine_Util.ftop_conv (K (rewr_conv @{thm fref_nest})) ctxt)) |> Local_Defs.unfold0 ctxt @{thms in_CURRY_conv} | @{mpat "(_,_)\_"} => thm RS @{thm fref_param0I} | _ => raise THM ("to_fref: Expected theorem of form (_,_)\_",~1,[thm]) end fun to_foparam 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 frefD} OF [thm]) - |> forall_intr_vars + |> 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 to_hnr ctxt thm = (thm RS @{thm hf2hnr}) |> Local_Defs.unfold0 ctxt @{thms to_hnr_prod_fst_snd keep_drop_sels} (* Resolve fst and snd over *\<^sub>a and R\<^sup>k, R\<^sup>d *) |> Local_Defs.unfold0 ctxt @{thms hnr_uncurry_unfold} (* Resolve products for uncurried parameters *) |> Local_Defs.unfold0 ctxt @{thms uncurry_apply uncurry_APP assn_one_left split} (* Remove the uncurry modifiers, the emp-dummy, and unfold product cases *) |> Local_Defs.unfold0 ctxt @{thms hn_ctxt_ctxt_fix_conv} (* Remove duplicate hn_ctxt tagging *) |> Local_Defs.unfold0 ctxt @{thms all_to_meta imp_to_meta HOL.True_implies_equals HOL.implies_True_equals Pure.triv_forall_equality cnv_conj_to_meta} (* Convert to meta-level, remove vacuous condition *) |> Local_Defs.unfold0 ctxt (Named_Theorems.get ctxt @{named_theorems to_hnr_post}) (* Post-Processing *) |> Goal.norm_result ctxt |> Conv.fconv_rule Thm.eta_conversion (* Convert schematic hfref-goal to hn_refine goal *) fun prepare_hfref_synth_tac ctxt = let val i_of_assn_rls = Named_Theorems_Rev.get ctxt @{named_theorems_rev intf_of_assn} @ @{thms intf_of_assn_fallback} val to_hnr_post_rls = Named_Theorems.get ctxt @{named_theorems to_hnr_post} val i_of_assn_tac = ( REPEAT' ( DETERM o dresolve_tac ctxt @{thms hfsynth_ID_R_D} THEN' DETERM o SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt i_of_assn_rls)) ) ) in (* Note: To re-use the to_hnr infrastructure, we first work with $-tags on the abstract function, which are finally removed. *) resolve_tac ctxt @{thms hfsynth_hnr_from_hfI} THEN_ELSE' ( SELECT_GOAL ( unfold_tac ctxt @{thms to_hnr_prod_fst_snd keep_drop_sels hf_pres_fst} (* Distribute fst,snd over product and hf_pres *) THEN unfold_tac ctxt @{thms hnr_uncurry_unfold hfsynth_ID_R_uncurry_unfold} (* Curry parameters *) THEN unfold_tac ctxt @{thms uncurry_apply uncurry_APP assn_one_left split} (* Curry parameters (II) and remove emp assertion *) (*THEN unfold_tac ctxt @{thms hn_ctxt_ctxt_fix_conv} (* Remove duplicate hn_ctxt (Should not be necessary) *)*) THEN unfold_tac ctxt @{thms all_to_meta imp_to_meta HOL.True_implies_equals HOL.implies_True_equals Pure.triv_forall_equality cnv_conj_to_meta} (* Convert precondition to meta-level *) THEN ALLGOALS i_of_assn_tac (* Generate _::\<^sub>i_ premises*) THEN unfold_tac ctxt to_hnr_post_rls (* Postprocessing *) THEN unfold_tac ctxt @{thms APP_def} (* Get rid of $ - tags *) ) , K all_tac ) end (************************************) (* Analyze hnr *) structure Termtab2 = Table( type key = term * term val ord = prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord); type hnr_analysis = { thm: thm, precond: term, prems : term list, ahead: term * bool, chead: term * bool, argrels: (term * bool) list, result_rel: term } fun analyze_hnr (ctxt:Proof.context) thm = let (* Debug information: Stores string*term pairs, which are pretty-printed on error *) val dbg = Unsynchronized.ref [] fun add_dbg msg ts = ( dbg := (msg,ts) :: !dbg; () ) fun pretty_dbg (msg,ts) = Pretty.block [ Pretty.str msg, Pretty.str ":", Pretty.brk 1, Pretty.list "[" "]" (map (Syntax.pretty_term ctxt) ts) ] fun pretty_dbgs l = map pretty_dbg l |> Pretty.fbreaks |> Pretty.block fun trace_dbg msg = Pretty.block [Pretty.str msg, Pretty.fbrk, pretty_dbgs (rev (!dbg))] |> Pretty.string_of |> tracing fun fail msg = (trace_dbg msg; raise THM(msg,~1,[thm])) fun assert cond msg = cond orelse fail msg; (* Heads may have a leading return/RETURN. The following code strips off the leading return, unless it has the form "return x" for an argument x *) fun check_strip_leading args t f = (* Handle the case RETURN x, where x is an argument *) if Termtab.defined args f then (t,false) else (f,true) fun strip_leading_RETURN args (t as @{mpat "RETURN$(?f)"}) = check_strip_leading args t f | strip_leading_RETURN args (t as @{mpat "RETURN ?f"}) = check_strip_leading args t f | strip_leading_RETURN _ t = (t,false) fun strip_leading_return args (t as @{mpat "return$(?f)"}) = check_strip_leading args t f | strip_leading_return args (t as @{mpat "return ?f"}) = check_strip_leading args t f | strip_leading_return _ t = (t,false) (* The following code strips the arguments of the concrete or abstract function. It knows how to handle APP-tags ($), and stops at PR_CONST-tags. Moreover, it only strips actual arguments that occur in the precondition-section of the hn_refine-statement. This ensures that non-arguments, like maxsize, are treated correctly. *) fun strip_fun _ (t as @{mpat "PR_CONST _"}) = (t,[]) | strip_fun s (t as @{mpat "?f$?x"}) = check_arg s t f x | strip_fun s (t as @{mpat "?f ?x"}) = check_arg s t f x | strip_fun _ f = (f,[]) and check_arg s t f x = if Termtab.defined s x then strip_fun s f |> apsnd (curry op :: x) else (t,[]) (* Arguments in the pre/postcondition are wrapped into hn_ctxt tags. This function strips them off. *) fun dest_hn_ctxt @{mpat "hn_ctxt ?R ?a ?c"} = ((a,c),R) | dest_hn_ctxt _ = fail "Invalid hn_ctxt parameter in pre or postcondition" fun dest_hn_refine @{mpat "(hn_refine ?G ?c ?G' ?R ?a)"} = (G,c,G',R,a) | dest_hn_refine _ = fail "Conclusion is not a hn_refine statement" (* Strip separation conjunctions. Special case for "emp", which is ignored. *) fun is_emp @{mpat emp} = true | is_emp _ = false val strip_star' = Sepref_Basic.strip_star #> filter (not o is_emp) (* Compare Termtab2s for equality of keys *) fun pairs_eq pairs1 pairs2 = Termtab2.forall (Termtab2.defined pairs1 o fst) pairs2 andalso Termtab2.forall (Termtab2.defined pairs2 o fst) pairs1 fun atomize_prem @{mpat "Trueprop ?p"} = p | atomize_prem _ = fail "Non-atomic premises" (* Make HOL conjunction list *) fun mk_conjs [] = @{const True} | mk_conjs [p] = p | mk_conjs (p::ps) = HOLogic.mk_binop @{const_name "HOL.conj"} (p,mk_conjs ps) (***********************) (* Start actual analysis *) val _ = add_dbg "thm" [Thm.prop_of thm] val prems = Thm.prems_of thm val concl = Thm.concl_of thm |> HOLogic.dest_Trueprop val (G,c,G',R,a) = dest_hn_refine concl val pre_pairs = G |> strip_star' |> tap (add_dbg "precondition") |> map dest_hn_ctxt |> Termtab2.make val post_pairs = G' |> strip_star' |> tap (add_dbg "postcondition") |> map dest_hn_ctxt |> Termtab2.make val _ = assert (pairs_eq pre_pairs post_pairs) "Parameters in precondition do not match postcondition" val aa_set = pre_pairs |> Termtab2.keys |> map fst |> Termtab.make_set val ca_set = pre_pairs |> Termtab2.keys |> map snd |> Termtab.make_set val (a,leading_RETURN) = strip_leading_RETURN aa_set a val (c,leading_return) = strip_leading_return ca_set c val _ = add_dbg "stripped abstract term" [a] val _ = add_dbg "stripped concrete term" [c] val (ahead,aargs) = strip_fun aa_set a; val (chead,cargs) = strip_fun ca_set c; val _ = add_dbg "abstract head" [ahead] val _ = add_dbg "abstract args" aargs val _ = add_dbg "concrete head" [chead] val _ = add_dbg "concrete args" cargs val _ = assert (length cargs = length aargs) "Different number of abstract and concrete arguments"; val _ = assert (not (has_duplicates op aconv aargs)) "Duplicate abstract arguments" val _ = assert (not (has_duplicates op aconv cargs)) "Duplicate concrete arguments" val argpairs = aargs ~~ cargs val ap_set = Termtab2.make_set argpairs val _ = assert (pairs_eq pre_pairs ap_set) "Arguments from pre/postcondition do not match operation's arguments" val pre_rels = map (the o (Termtab2.lookup pre_pairs)) argpairs val post_rels = map (the o (Termtab2.lookup post_pairs)) argpairs val _ = add_dbg "pre-rels" pre_rels val _ = add_dbg "post-rels" post_rels fun adjust_hf_pres @{mpat "snd (?R\<^sup>k)"} = R | adjust_hf_pres t = t val post_rels = map adjust_hf_pres post_rels fun is_invalid R @{mpat "invalid_assn ?R'"} = R aconv R' | is_invalid _ @{mpat "snd (_\<^sup>d)"} = true | is_invalid _ _ = false fun is_keep (R,R') = if R aconv R' then true else if is_invalid R R' then false else fail "Mismatch between pre and post relation for argument" val keep = map is_keep (pre_rels ~~ post_rels) val argrels = pre_rels ~~ keep val aa_set = Termtab.make_set aargs val ca_set = Termtab.make_set cargs fun is_precond t = (exists_subterm (Termtab.defined ca_set) t andalso fail "Premise contains concrete argument") orelse exists_subterm (Termtab.defined aa_set) t val (preconds, prems) = split is_precond prems val precond = map atomize_prem preconds |> mk_conjs |> fold lambda aargs val _ = add_dbg "precond" [precond] val _ = add_dbg "prems" prems in { thm = thm, precond = precond, prems = prems, ahead = (ahead,leading_RETURN), chead = (chead,leading_return), argrels = argrels, result_rel = R } end fun pretty_hnr_analysis ctxt ({thm,precond,ahead,chead,argrels,result_rel,...}) : Pretty.T = let val _ = thm (* Suppress unused warning for thm *) fun pretty_argrel (R,k) = Pretty.block [ Syntax.pretty_term ctxt R, if k then Pretty.str "\<^sup>k" else Pretty.str "\<^sup>d" ] val pretty_chead = case chead of (t,false) => Syntax.pretty_term ctxt t | (t,true) => Pretty.block [Pretty.str "return ", Syntax.pretty_term ctxt t] val pretty_ahead = case ahead of (t,false) => Syntax.pretty_term ctxt t | (t,true) => Pretty.block [Pretty.str "RETURN ", Syntax.pretty_term ctxt t] in Pretty.fbreaks [ (*Display.pretty_thm ctxt thm,*) Pretty.block [ Pretty.enclose "[" "]" [pretty_chead, pretty_ahead], Pretty.enclose "[" "]" [Syntax.pretty_term ctxt precond], Pretty.brk 1, Pretty.block (Pretty.separate " \" (map pretty_argrel argrels @ [Syntax.pretty_term ctxt result_rel])) ] ] |> Pretty.block end fun mk_hfref_thm ctxt ({thm,precond,prems,ahead,chead,argrels,result_rel}) = let fun mk_keep (R,true) = @{mk_term "?R\<^sup>k"} | mk_keep (R,false) = @{mk_term "?R\<^sup>d"} (* TODO: Move, this is of general use! *) fun mk_uncurry f = @{mk_term "uncurry ?f"} (* Uncurry function for the given number of arguments. For zero arguments, add a unit-parameter. *) fun rpt_uncurry n t = if n=0 then @{mk_term "uncurry0 ?t"} else if n=1 then t else funpow (n-1) mk_uncurry t (* Rewrite uncurried lambda's to \(_,_). _ form. Use top-down rewriting to correctly handle nesting to the left. TODO: Combine with abstraction and uncurry-procedure, and mark the deviation about uncurry as redundant intermediate step to be eliminated. *) fun rew_uncurry_lambda t = let val rr = map (Logic.dest_equals o Thm.prop_of) @{thms uncurry_def uncurry0_def} val thy = Proof_Context.theory_of ctxt in Pattern.rewrite_term_top thy rr [] t end (* Shortcuts for simplification tactics *) fun gsimp_only ctxt sec = let val ss = put_simpset HOL_basic_ss ctxt |> sec in asm_full_simp_tac ss end fun simp_only ctxt thms = gsimp_only ctxt (fn ctxt => ctxt addsimps thms) (********************************) (* Build theorem statement *) (* \prems\ \ (chead,ahead) \ [precond] rels \ R *) (* Uncurry precondition *) val num_args = length argrels val precond = precond |> rpt_uncurry num_args |> rew_uncurry_lambda (* Convert to nicer \((...,_),_) - form*) (* Re-attach leading RETURN/return *) fun mk_RETURN (t,r) = if r then let val T = funpow num_args range_type (fastype_of (fst ahead)) val tRETURN = Const (@{const_name RETURN}, T --> Type(@{type_name nres},[T])) in Refine_Util.mk_compN num_args tRETURN t end else t fun mk_return (t,r) = if r then let val T = funpow num_args range_type (fastype_of (fst chead)) val tRETURN = Const (@{const_name return}, T --> Type(@{type_name Heap},[T])) in Refine_Util.mk_compN num_args tRETURN t end else t (* Hrmpf!: Gone for good from 2015\2016. Inserting ctxt-based substitute here. *) fun certify_inst ctxt (instT, inst) = (map (apsnd (Thm.ctyp_of ctxt)) (Term_Subst.TVars.dest instT), map (apsnd (Thm.cterm_of ctxt)) (Term_Subst.Vars.dest inst)); (* fun mk_RETURN (t,r) = if r then @{mk_term "RETURN o ?t"} else t fun mk_return (t,r) = if r then @{mk_term "return o ?t"} else t *) (* Uncurry abstract and concrete function, append leading return *) val ahead = ahead |> mk_RETURN |> rpt_uncurry num_args val chead = chead |> mk_return |> rpt_uncurry num_args (* Add keep-flags and summarize argument relations to product *) val argrel = map mk_keep argrels |> rev (* TODO: Why this rev? *) |> mk_hfprods (* Produce final result statement *) val result = @{mk_term "Trueprop ((?chead,?ahead) \ [?precond]\<^sub>a ?argrel \ ?result_rel)"} val result = Logic.list_implies (prems,result) (********************************) (* Prove theorem *) (* Create context and import result statement and original theorem *) val orig_ctxt = ctxt (*val thy = Proof_Context.theory_of ctxt*) val (insts, ctxt) = Variable.import_inst true [result] ctxt val insts' = certify_inst ctxt insts val result = Term_Subst.instantiate insts result val thm = Thm.instantiate insts' thm (* Unfold APP tags. This is required as some APP-tags have also been unfolded by analysis *) val thm = Local_Defs.unfold0 ctxt @{thms APP_def} thm (* Tactic to prove the theorem. A first step uses hfrefI to get a hnr-goal. This is then normalized in several consecutive steps, which get rid of uncurrying. Finally, the original theorem is used for resolution, where the pre- and postcondition, and result relation are connected with a consequence rule, to handle unfolded hn_ctxt-tags, re-ordered relations, and introduced unit-parameters (TODO: Mark artificially introduced unit-parameter specially, it may get confused with intentional unit-parameter, e.g., functional empty_set ()!) *) fun tac ctxt = resolve_tac ctxt @{thms hfrefI} THEN' gsimp_only ctxt (fn c => c addsimps @{thms uncurry_def hn_ctxt_def uncurry0_def keep_drop_sels uc_hfprod_sel o_apply APP_def} |> Splitter.add_split @{thm prod.split} ) THEN' TRY o ( REPEAT_ALL_NEW (match_tac ctxt @{thms allI impI}) THEN' simp_only ctxt @{thms Product_Type.split prod.inject}) THEN' TRY o REPEAT_ALL_NEW (ematch_tac ctxt @{thms conjE}) THEN' TRY o hyp_subst_tac ctxt THEN' simp_only ctxt @{thms triv_forall_equality} THEN' ( resolve_tac ctxt @{thms hn_refine_cons[rotated]} THEN' (resolve_tac ctxt [thm] THEN_ALL_NEW assume_tac ctxt)) THEN_ALL_NEW simp_only ctxt @{thms hn_ctxt_def entt_refl pure_unit_rel_eq_empty mult_ac mult_1 mult_1_right keep_drop_sels} (* Prove theorem *) val result = Thm.cterm_of ctxt result val rthm = Goal.prove_internal ctxt [] result (fn _ => ALLGOALS (tac ctxt)) (* Export statement to original context *) val rthm = singleton (Variable.export ctxt orig_ctxt) rthm (* Post-processing *) val rthm = Local_Defs.unfold0 ctxt (Named_Theorems.get ctxt @{named_theorems to_hfref_post}) rthm in rthm end fun to_hfref ctxt = analyze_hnr ctxt #> mk_hfref_thm ctxt (***********************************) (* Composition *) local fun norm_set_of ctxt = { trans_rules = Named_Theorems.get ctxt @{named_theorems fcomp_norm_trans}, cong_rules = Named_Theorems.get ctxt @{named_theorems fcomp_norm_cong}, norm_rules = Named_Theorems.get ctxt @{named_theorems fcomp_norm_norm}, refl_rules = Named_Theorems.get ctxt @{named_theorems fcomp_norm_refl} } fun init_rules_of ctxt = Named_Theorems.get ctxt @{named_theorems fcomp_norm_init} fun unfold_rules_of ctxt = Named_Theorems.get ctxt @{named_theorems fcomp_norm_unfold} fun simp_rules_of ctxt = Named_Theorems.get ctxt @{named_theorems fcomp_norm_simps} in fun norm_fcomp_rule ctxt = let open PO_Normalizer Refine_Util val norm1 = gen_norm_rule (init_rules_of ctxt) (norm_set_of ctxt) ctxt val norm2 = Local_Defs.unfold0 ctxt (unfold_rules_of ctxt) val norm3 = Conv.fconv_rule ( Simplifier.asm_full_rewrite (put_simpset HOL_basic_ss ctxt addsimps simp_rules_of ctxt)) val norm = changed_rule (try_rule norm1 o try_rule norm2 o try_rule norm3) in repeat_rule norm end end fun add_pure_constraints_rule ctxt thm = let val orig_ctxt = ctxt val t = Thm.prop_of thm fun cnv (@{mpat (typs) "pure (mpaq_STRUCT (mpaq_Var ?x _) :: (?'v_c\?'v_a) set)"}) = let val T = a --> c --> @{typ assn} val t = Var (x,T) val t = @{mk_term "(the_pure ?t)"} in [(x,T,t)] end | cnv (t$u) = union op= (cnv t) (cnv u) | cnv (Abs (_,_,t)) = cnv t | cnv _ = [] val pvars = cnv t val _ = (pvars |> map #1 |> has_duplicates op=) andalso raise TERM ("Duplicate indexname with different type",[t]) (* This should not happen *) val substs = map (fn (x,_,t) => (x,t)) pvars val t' = subst_Vars substs t fun mk_asm (x,T,_) = let val t = Var (x,T) val t = @{mk_term "Trueprop (CONSTRAINT is_pure ?t)"} in t end val assms = map mk_asm pvars fun add_prems prems t = let val prems' = Logic.strip_imp_prems t val concl = Logic.strip_imp_concl t in Logic.list_implies (prems@prems', concl) end val t' = add_prems assms t' val (t',ctxt) = yield_singleton (Variable.import_terms true) t' ctxt val thm' = Goal.prove_internal ctxt [] (Thm.cterm_of ctxt t') (fn _ => ALLGOALS (resolve_tac ctxt [thm] THEN_ALL_NEW assume_tac ctxt)) val thm' = norm_fcomp_rule ctxt thm' val thm' = singleton (Variable.export ctxt orig_ctxt) thm' in thm' end val cfg_simp_precond = Attrib.setup_config_bool @{binding fcomp_simp_precond} (K true) local fun mk_simp_thm ctxt t = let val st = t |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt |> Goal.init val ctxt = Context_Position.set_visible false ctxt val ctxt = ctxt addsimps ( refine_pw_simps.get ctxt @ Named_Theorems.get ctxt @{named_theorems fcomp_prenorm_simps} @ @{thms split_tupled_all cnv_conj_to_meta} ) val trace_incomplete_transfer_tac = COND (Thm.prems_of #> exists (strip_all_body #> Logic.strip_imp_concl #> Term.is_open)) (print_tac ctxt "Failed transfer from intermediate level:") all_tac val tac = ALLGOALS (resolve_tac ctxt @{thms auto_weaken_pre_comp_PRE_I} ) THEN ALLGOALS (Simplifier.asm_full_simp_tac ctxt) THEN trace_incomplete_transfer_tac THEN ALLGOALS (TRY o filter_prems_tac ctxt (K false)) THEN Local_Defs.unfold0_tac ctxt [Drule.triv_forall_equality] val st' = tac st |> Seq.take 1 |> Seq.list_of val thm = case st' of [st'] => Goal.conclude st' | _ => raise THM("Simp_Precond: Simp-Tactic failed",~1,[st]) (* Check generated premises for leftover intermediate stuff *) val _ = exists (Logic.is_all) (Thm.prems_of thm) andalso raise THM("Simp_Precond: Transfer from intermediate level failed",~1,[thm]) val thm = thm (*|> map (Simplifier.asm_full_simplify ctxt)*) |> Conv.fconv_rule (Object_Logic.atomize ctxt) |> Local_Defs.unfold0 ctxt @{thms auto_weaken_pre_to_imp_nf} val thm = case Thm.concl_of thm of @{mpat "Trueprop (_ \ _)"} => thm | @{mpat "Trueprop _"} => thm RS @{thm auto_weaken_pre_add_dummy_imp} | _ => raise THM("Simp_Precond: Generated odd theorem, expected form 'P\Q'",~1,[thm]) in thm end in fun simplify_precond ctxt thm = let val orig_ctxt = ctxt val thm = Refine_Util.OF_fst @{thms auto_weaken_pre_init} [asm_rl,thm] val thm = Local_Defs.unfold0 ctxt @{thms split_tupled_all} thm OF @{thms auto_weaken_pre_uncurry_start} fun rec_uncurry thm = case try (fn () => thm OF @{thms auto_weaken_pre_uncurry_step}) () of NONE => thm OF @{thms auto_weaken_pre_uncurry_finish} | SOME thm => rec_uncurry thm val thm = rec_uncurry thm |> Conv.fconv_rule Thm.eta_conversion val t = case Thm.prems_of thm of t::_ => t | _ => raise THM("Simp-Precond: Expected at least one premise",~1,[thm]) val (t,ctxt) = yield_singleton (Variable.import_terms false) t ctxt val ((_,t),ctxt) = Variable.focus NONE t ctxt val t = case t of @{mpat "Trueprop (_ \ ?t)"} => t | _ => raise TERM("Simp_Precond: Expected implication",[t]) val simpthm = mk_simp_thm ctxt t |> singleton (Variable.export ctxt orig_ctxt) val thm = thm OF [simpthm] val thm = Local_Defs.unfold0 ctxt @{thms prod_casesK} thm in thm end fun simplify_precond_if_cfg ctxt = if Config.get ctxt cfg_simp_precond then simplify_precond ctxt else I end (* fref O fref *) fun compose_ff ctxt A B = (@{thm fref_compI_PRE} OF [A,B]) |> norm_fcomp_rule ctxt |> simplify_precond_if_cfg ctxt |> Conv.fconv_rule Thm.eta_conversion (* hfref O fref *) fun compose_hf ctxt A B = (@{thm hfref_compI_PRE} OF [A,B]) |> norm_fcomp_rule ctxt |> simplify_precond_if_cfg ctxt |> Conv.fconv_rule Thm.eta_conversion |> add_pure_constraints_rule ctxt |> Conv.fconv_rule Thm.eta_conversion fun ensure_fref ctxt thm = case rthm_type thm of RT_HOPARAM => to_fref ctxt thm | RT_FREF => thm | _ => raise THM("Expected parametricity or fref theorem",~1,[thm]) fun ensure_fref_nres ctxt thm = let val thm = ensure_fref ctxt thm in case Thm.concl_of thm of @{mpat (typs) "Trueprop (_\fref _ _ (_::(_ nres\_)set))"} => thm | @{mpat "Trueprop ((_,_)\fref _ _ _)"} => (thm RS @{thm ensure_fref_nresI}) |> Local_Defs.unfold0 ctxt @{thms ensure_fref_nres_unfold} | _ => raise THM("Expected fref-theorem",~1,[thm]) end fun ensure_hfref ctxt thm = case rthm_type thm of RT_HNR => to_hfref ctxt thm | RT_HFREF => thm | _ => raise THM("Expected hnr or hfref theorem",~1,[thm]) fun ensure_hnr ctxt thm = case rthm_type thm of RT_HNR => thm | RT_HFREF => to_hnr ctxt thm | _ => raise THM("Expected hnr or hfref theorem",~1,[thm]) fun gen_compose ctxt A B = let val rtA = rthm_type A in if rtA = RT_HOPARAM orelse rtA = RT_FREF then compose_ff ctxt (ensure_fref ctxt A) (ensure_fref ctxt B) else compose_hf ctxt (ensure_hfref ctxt A) ((ensure_fref_nres ctxt B)) end val parse_fcomp_flags = Refine_Util.parse_paren_lists (Refine_Util.parse_bool_config "prenorm" cfg_simp_precond) val fcomp_attrib = parse_fcomp_flags |-- Attrib.thm >> (fn B => Thm.rule_attribute [] (fn context => fn A => let val ctxt = Context.proof_of context in gen_compose ctxt A B end)) end \ attribute_setup to_fref = \ Scan.succeed (Thm.rule_attribute [] (Sepref_Rules.to_fref o Context.proof_of)) \ "Convert parametricity theorem to uncurried fref-form" attribute_setup to_foparam = \ Scan.succeed (Thm.rule_attribute [] (Sepref_Rules.to_foparam o Context.proof_of)) \ \Convert param or fref rule to first order rule\ (* Overloading existing param_fo - attribute from Parametricity.thy *) attribute_setup param_fo = \ Scan.succeed (Thm.rule_attribute [] (Sepref_Rules.to_foparam o Context.proof_of)) \ \Convert param or fref rule to first order rule\ attribute_setup to_hnr = \ Scan.succeed (Thm.rule_attribute [] (Sepref_Rules.to_hnr o Context.proof_of)) \ "Convert hfref-rule to hnr-rule" attribute_setup to_hfref = \Scan.succeed ( Thm.rule_attribute [] (Context.proof_of #> Sepref_Rules.to_hfref) )\ \Convert hnr to hfref theorem\ attribute_setup ensure_fref_nres = \Scan.succeed ( Thm.rule_attribute [] (Context.proof_of #> Sepref_Rules.ensure_fref_nres) )\ attribute_setup sepref_dbg_norm_fcomp_rule = \Scan.succeed ( Thm.rule_attribute [] (Context.proof_of #> Sepref_Rules.norm_fcomp_rule) )\ attribute_setup sepref_simplify_precond = \Scan.succeed ( Thm.rule_attribute [] (Context.proof_of #> Sepref_Rules.simplify_precond) )\ \Simplify precondition of fref/hfref-theorem\ attribute_setup FCOMP = Sepref_Rules.fcomp_attrib "Composition of refinement rules" end diff --git a/thys/Refine_Imperative_HOL/Sepref_Translate.thy b/thys/Refine_Imperative_HOL/Sepref_Translate.thy --- a/thys/Refine_Imperative_HOL/Sepref_Translate.thy +++ b/thys/Refine_Imperative_HOL/Sepref_Translate.thy @@ -1,927 +1,927 @@ section \Translation\ theory Sepref_Translate imports Sepref_Monadify Sepref_Constraints Sepref_Frame "Lib/Pf_Mono_Prover" Sepref_Rules Sepref_Combinator_Setup "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 \sepref_fr_rules\, and the collection \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 \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} \ (*subsection \Basic Translation Tool\ definition COPY -- "Copy operation" where [simp]: "COPY \ RETURN" lemma tagged_nres_monad1: "Refine_Basic.bind$(RETURN$x)$(\\<^sub>2x. f x) = f x" by simp text \The PREPARED-tag is used internally, to flag a refinement goal with the index of the refinement rule to be used\ definition PREPARED_TAG :: "'a => nat => 'a" where [simp]: "PREPARED_TAG x i == x" lemma PREPARED_TAG_I: "hn_refine \ c \' R a \ hn_refine \ c \' R (PREPARED_TAG a i)" by simp lemmas prepare_refine_simps = tagged_nres_monad1 COPY_def PREPARED_TAG_def lemma mono_trigger: "mono_Heap F \ mono_Heap F" . *) 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" (* abbreviation DEP_SIDE_PRECOND -- \Precondition that depends on information from relators, like maximum size. It must be processed after frame inference, when the relator variables have been fixed.\ where "DEP_SIDE_PRECOND \ \ DEFER_tag (PRECOND_tag \)" lemma DEP_SIDE_PRECOND_D: "DEP_SIDE_PRECOND P \ P" by simp *) 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 (\\<^sub>1 * \\<^sub>2) \ vassn_tag \\<^sub>1 \ vassn_tag \\<^sub>2" "vassn_tag (hn_ctxt R a b) \ a\rdom R" unfolding vassn_tag_def rdomp_def[abs_def] by (auto simp: mod_star_conv hn_ctxt_def) lemma entails_preI: assumes "vassn_tag A \ A \\<^sub>A B" shows "A \\<^sub>A B" using assms by (auto simp: entails_def vassn_tag_def) lemma invalid_assn_const: "invalid_assn (\_ _. P) x y = \(vassn_tag P) * true" by (simp_all add: invalid_assn_def vassn_tag_def) lemma vassn_tag_simps[simp]: "vassn_tag emp" "vassn_tag true" by (sep_auto simp: vassn_tag_def mod_emp)+ definition "GEN_ALGO f \ \ \ f" \ \Tag to synthesize @{term f} with property @{term \}.\ lemma is_GEN_ALGO: "GEN_ALGO f \ \ GEN_ALGO f \" . 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 \' \ hn_refine \' c \'' R a" shows "hn_refine (F*\) c (F*\'') R a" apply (rule hn_refine_frame[OF _ entt_refl]) applyF (rule hn_refine_cons_pre) focus using assms(1) unfolding RECOVER_PURE_def apply assumption solved apply1 (rule hn_refine_preI) apply1 (rule assms) applyS (auto simp add: vassn_tag_def) solved done lemma recover_pure_cons: \ \Used for debugging\ assumes "RECOVER_PURE \ \'" assumes "hn_refine \' c \'' R a" shows "hn_refine (\) c (\'') R a" using trans_frame_rule[where F=emp, OF assms] by simp \ \Tag to align structure of refinement assertions for consequence rule\ 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: \ \Consequence rule to be applied if no direct operation rule matches\ assumes "CPR_TAG P P'" assumes "P \\<^sub>t P'" assumes "hn_refine P' c Q R m" shows "hn_refine P c Q R m" using assms(2-) by (rule hn_refine_cons_pre) named_theorems_rev sepref_gen_algo_rules \Sepref: Generic algorithm 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 gen_msg_analyze t ctxt = let val t = Logic.strip_assums_concl t in case t of @{mpat "Trueprop ?t"} => (case t of @{mpat "_ \\<^sub>A _ \\<^sub>t _"} => "t_merge" | @{mpat "_ \\<^sub>t _"} => "t_frame" | @{mpat "INDEP _"} => "t_indep" | @{mpat "CONSTRAINT _ _"} => "t_constraint" | @{mpat "mono_Heap _"} => "t_mono" | @{mpat "PREFER_tag _"} => "t_prefer" | @{mpat "DEFER_tag _"} => "t_defer" | @{mpat "RPREM _"} => "t_rprem" | @{mpat "hn_refine _ _ _ _ ?a"} => Pretty.block [Pretty.str "t_hnr: ",Pretty.brk 1, Syntax.pretty_term ctxt a] |> Pretty.string_of | _ => "Unknown goal type" ) | _ => "Non-Trueprop goal" end fun msg_analyze msg = Sepref_Debugging.msg_from_subgoal msg gen_msg_analyze fun check_side_conds thm = let open Sepref_Basic (* Check that term is no binary operator on assertions *) 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 "?l \\<^sub>A ?r \\<^sub>t ?m"} = ( assert is_atomic_star_list l; assert is_atomic_star_list r; assert is_atomic_star_list m ) | chk (t as @{mpat "_ \\<^sub>A _"}) = raise TERM("Invalid frame side condition (old-style ent)",[t]) | chk @{mpat "?l \\<^sub>t ?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 ) (***** Side Condition Solving *) local open Sepref_Basic in fun side_unfold_tac ctxt = let (*val ctxt = put_simpset HOL_basic_ss ctxt addsimps sepref_prep_side_simps.get ctxt*) in CONVERSION (Id_Op.unprotect_conv ctxt) THEN' SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms bind_ref_tag_def}) (*THEN' asm_full_simp_tac ctxt*) end fun side_fallback_tac ctxt = side_unfold_tac ctxt THEN' TRADE (SELECT_GOAL o auto_tac) ctxt val side_frame_tac = Sepref_Frame.frame_tac side_fallback_tac val side_merge_tac = Sepref_Frame.merge_tac side_fallback_tac fun side_constraint_tac ctxt = Sepref_Constraints.constraint_tac ctxt fun side_mono_tac ctxt = side_unfold_tac ctxt THEN' TRADE Pf_Mono_Prover.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)) (* Solve side condition, or invoke hnr_tac on hn_refine goal. In debug mode, side-condition solvers are allowed to not completely solve the side condition, but must change the goal. *) 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_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_fallback = MK side_fallback_tac in WITH_concl (fn @{mpat "Trueprop ?t"} => (case t of @{mpat "_ \\<^sub>A _ \\<^sub>t _"} => t_merge | @{mpat "_ \\<^sub>t _"} => t_frame | @{mpat "_ \\<^sub>A _"} => Sepref_Debugging.warning_tac' "Old-style frame side condition" ctxt THEN' (K no_tac) | @{mpat "INDEP _"} => t_indep (* TODO: Get rid of this!? *) | @{mpat "CONSTRAINT _ _"} => t_constraint | @{mpat "mono_Heap _"} => 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 "hn_refine _ _ _ _ _"} => hnr_tac | _ => t_fallback ) | _ => K no_tac ) end end (***** Main Translation Tactic *) local open Sepref_Basic STactical (* ATTENTION: Beware of evaluation order, as some initialization operations on context are expensive, and should not be repeated during proof search! *) in (* Translate combinator, yields new translation goals and side conditions which must be processed in order. *) 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 ORELSE' ( Sepref_Frame.norm_goal_pre_tac ctxt THEN' resolve_from_net_tac ctxt comb_rl_net ) ) end (* Translate operator. Only succeeds if it finds an operator rule such that all resulting side conditions can be solved. Takes the first such rule. In debug mode, it returns a sequence of the unsolved side conditions of each applicable rule. *) 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 (* Try direct match *) ORELSE' ( Sepref_Frame.norm_goal_pre_tac ctxt (* Normalize precondition *) THEN' ( resolve_from_net_tac ctxt fr_rl_net ORELSE' ( resolve_tac ctxt @{thms cons_pre_rule} (* Finally, generate a frame condition *) THEN_ALL_NEW_LIST [ SOLVED' (REPEAT_ALL_NEW_FWD (DETERM o resolve_tac ctxt @{thms CPR_TAG_rules})), K all_tac, (* Frame remains unchanged as first goal, even if fr_rl creates side-conditions *) 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 (* Present all possibilities with (partially resolved) side conditions *) fr_rl_tac THEN_ALL_NEW_FWD (TRY o side_tac) else (* Choose first rule that solves all side conditions *) 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 goal *) ("Recover pure",Sepref_Frame.recover_pure_tac, ~1), (* hn-refine goal with stripped precondition *) ("Apply rule",K fr_tac,~1) ] (flag_phases_ctrl dbg) ctxt end (* Translate combinator, operator, or side condition. *) fun gen_trans_step_tac dbg ctxt = side_cond_dispatch_tac dbg (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 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 subsubsection \Basic Setup\ lemma hn_pass[sepref_fr_rules]: shows "hn_refine (hn_ctxt P x x') (return x') (hn_invalid P x x') P (PASS$x)" apply rule apply (sep_auto simp: hn_ctxt_def invalidate_clone') done (*lemma hn_pass_pure[sepref_fr_rules]: shows "hn_refine (hn_val P x x') (return x') (hn_val P x x') (pure P) (PASS$x)" by rule (sep_auto simp: hn_ctxt_def pure_def) *) lemma hn_bind[sepref_comb_rules]: assumes D1: "hn_refine \ m' \1 Rh m" assumes D2: "\x x'. bind_ref_tag x m \ hn_refine (\1 * hn_ctxt Rh x x') (f' x') (\2 x x') R (f x)" assumes IMP: "\x x'. \2 x x' \\<^sub>t \' * hn_ctxt Rx x x'" shows "hn_refine \ (m'\f') \' R (Refine_Basic.bind$m$(\\<^sub>2x. f x))" using assms unfolding APP_def PROTECT2_def bind_ref_tag_def by (rule hnr_bind) lemma hn_RECT'[sepref_comb_rules]: assumes "INDEP Ry" "INDEP Rx" "INDEP Rx'" assumes FR: "P \\<^sub>t 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 (RCALL$af$ax)\ \ hn_refine (hn_ctxt Rx ax px * F) (cB cf px) (F' ax px) Ry (aB af ax)" assumes FR': "\ax px. F' ax px \\<^sub>t hn_ctxt Rx' ax px * F" assumes M: "(\x. mono_Heap (\f. cB f x))" (*assumes PREC[unfolded CONSTRAINT_def]: "CONSTRAINT precise Ry"*) shows "hn_refine (P) (heap.fixp_fun cB px) (hn_ctxt Rx' ax px * F) Ry (RECT$(\\<^sub>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 S[unfolded RCALL_def APP_def]) apply assumption apply fact+ done lemma hn_RCALL[sepref_comb_rules]: assumes "RPREM (hn_refine P' c Q' R (RCALL $ a $ b))" and "P \\<^sub>t F * P'" shows "hn_refine P c (F * Q') R (RCALL $ a $ b)" using assms hn_refine_frame[where m="RCALL$a$b"] by simp definition "monadic_WHILEIT I b f s \ do { RECT (\D s. do { ASSERT (I s); bv \ b s; if bv then do { s \ f s; D s } else do {RETURN s} }) s }" definition "heap_WHILET b f s \ do { heap.fixp_fun (\D s. do { bv \ b s; if bv then do { s \ f s; D s } else do {return s} }) s }" lemma heap_WHILET_unfold[code]: "heap_WHILET b f s = do { bv \ b s; if bv then do { s \ f s; heap_WHILET b f s } else return s }" unfolding heap_WHILET_def apply (subst heap.mono_body_fixp) apply pf_mono apply simp done lemma WHILEIT_to_monadic: "WHILEIT I b f s = monadic_WHILEIT I (\s. RETURN (b s)) f s" unfolding WHILEIT_def monadic_WHILEIT_def unfolding WHILEI_body_def bind_ASSERT_eq_if by (simp cong: if_cong) lemma WHILEIT_pat[def_pat_rules]: "WHILEIT$I \ UNPROTECT (WHILEIT I)" "WHILET \ PR_CONST (WHILEIT (\_. True))" by (simp_all add: WHILET_def) lemma id_WHILEIT[id_rules]: "PR_CONST (WHILEIT I) ::\<^sub>i TYPE(('a \ bool) \ ('a \ 'a nres) \ 'a \ 'a nres)" by simp lemma WHILE_arities[sepref_monadify_arity]: (*"WHILET \ WHILEIT$(\\<^sub>2_. True)"*) "PR_CONST (WHILEIT I) \ \\<^sub>2b f s. SP (PR_CONST (WHILEIT I))$(\\<^sub>2s. b$s)$(\\<^sub>2s. f$s)$s" by (simp_all add: WHILET_def) lemma WHILEIT_comb[sepref_monadify_comb]: "PR_CONST (WHILEIT I)$(\\<^sub>2x. b x)$f$s \ Refine_Basic.bind$(EVAL$s)$(\\<^sub>2s. SP (PR_CONST (monadic_WHILEIT I))$(\\<^sub>2x. (EVAL$(b x)))$f$s )" by (simp_all add: WHILEIT_to_monadic) lemma hn_monadic_WHILE_aux: assumes FR: "P \\<^sub>t \ * hn_ctxt Rs s' s" assumes b_ref: "\s s'. I s' \ hn_refine (\ * hn_ctxt Rs s' s) (b s) (\b s' s) (pure bool_rel) (b' s')" assumes b_fr: "\s' s. \b s' s \\<^sub>t \ * hn_ctxt Rs s' s" assumes f_ref: "\s' s. \I s'\ \ hn_refine (\ * hn_ctxt Rs s' s) (f s) (\f s' s) Rs (f' s')" assumes f_fr: "\s' s. \f s' s \\<^sub>t \ * hn_ctxt (\_ _. true) s' s" (*assumes PREC: "precise Rs"*) shows "hn_refine (P) (heap_WHILET b f s) (\ * hn_invalid Rs s' s) Rs (monadic_WHILEIT I b' f' s')" unfolding monadic_WHILEIT_def heap_WHILET_def apply1 (rule hn_refine_cons_pre[OF FR]) apply weaken_hnr_post focus (rule hn_refine_cons_pre[OF _ hnr_RECT]) applyS (subst mult_ac(2)[of \]; rule entt_refl; fail) apply1 (rule hnr_ASSERT) focus (rule hnr_bind) focus (rule hn_refine_cons[OF _ b_ref b_fr entt_refl]) applyS (simp add: star_aci) applyS assumption solved focus (rule hnr_If) applyS (sep_auto; fail) focus (rule hnr_bind) focus (rule hn_refine_cons[OF _ f_ref f_fr entt_refl]) apply (sep_auto simp: hn_ctxt_def pure_def intro!: enttI; fail) apply assumption solved focus (rule hn_refine_frame) applyS rprems applyS (rule enttI; solve_entails) solved apply (sep_auto intro!: enttI; fail) solved applyF (sep_auto,rule hn_refine_frame) applyS (rule hnr_RETURN_pass) (*apply (tactic {* Sepref_Frame.frame_tac @{context} 1*})*) apply (rule enttI) apply (fr_rot_rhs 1) apply (fr_rot 1, rule fr_refl) apply (rule fr_refl) apply solve_entails solved apply (rule entt_refl) solved apply (rule enttI) applyF (rule ent_disjE) apply1 (sep_auto simp: hn_ctxt_def pure_def) apply1 (rule ent_true_drop) apply1 (rule ent_true_drop) applyS (rule ent_refl) applyS (sep_auto simp: hn_ctxt_def pure_def) solved solved apply pf_mono solved done lemma hn_monadic_WHILE_lin[sepref_comb_rules]: assumes "INDEP Rs" assumes FR: "P \\<^sub>t \ * hn_ctxt Rs s' s" assumes b_ref: "\s s'. I s' \ hn_refine (\ * hn_ctxt Rs s' s) (b s) (\b s' s) (pure bool_rel) (b' s')" assumes b_fr: "\s' s. TERM (monadic_WHILEIT,''cond'') \ \b s' s \\<^sub>t \ * hn_ctxt Rs s' s" assumes f_ref: "\s' s. I s' \ hn_refine (\ * hn_ctxt Rs s' s) (f s) (\f s' s) Rs (f' s')" assumes f_fr: "\s' s. TERM (monadic_WHILEIT,''body'') \ \f s' s \\<^sub>t \ * hn_ctxt (\_ _. true) s' s" shows "hn_refine P (heap_WHILET b f s) (\ * hn_invalid Rs s' s) Rs (PR_CONST (monadic_WHILEIT I)$(\\<^sub>2s'. b' s')$(\\<^sub>2s'. f' s')$(s'))" using assms(2-) unfolding APP_def PROTECT2_def CONSTRAINT_def PR_CONST_def by (rule hn_monadic_WHILE_aux) lemma monadic_WHILEIT_refine[refine]: assumes [refine]: "(s',s) \ R" assumes [refine]: "\s' s. \ (s',s)\R; I s \ \ I' s'" assumes [refine]: "\s' s. \ (s',s)\R; I s; I' s' \ \ b' s' \\bool_rel (b s)" assumes [refine]: "\s' s. \ (s',s)\R; I s; I' s'; nofail (b s); inres (b s) True \ \ f' s' \\R (f s)" shows "monadic_WHILEIT I' b' f' s' \\R (monadic_WHILEIT I b f s)" unfolding monadic_WHILEIT_def by (refine_rcg bind_refine'; assumption?; auto) lemma monadic_WHILEIT_refine_WHILEIT[refine]: assumes [refine]: "(s',s) \ R" assumes [refine]: "\s' s. \ (s',s)\R; I s \ \ I' s'" assumes [THEN order_trans,refine_vcg]: "\s' s. \ (s',s)\R; I s; I' s' \ \ b' s' \ SPEC (\r. r = b s)" assumes [refine]: "\s' s. \ (s',s)\R; I s; I' s'; b s \ \ f' s' \\R (f s)" shows "monadic_WHILEIT I' b' f' s' \\R (WHILEIT I b f s)" unfolding WHILEIT_to_monadic by (refine_vcg; assumption?; auto) lemma monadic_WHILEIT_refine_WHILET[refine]: assumes [refine]: "(s',s) \ R" assumes [THEN order_trans,refine_vcg]: "\s' s. \ (s',s)\R \ \ b' s' \ SPEC (\r. r = b s)" assumes [refine]: "\s' s. \ (s',s)\R; b s \ \ f' s' \\R (f s)" shows "monadic_WHILEIT (\_. True) b' f' s' \\R (WHILET b f s)" unfolding WHILET_def by (refine_vcg; assumption?) lemma monadic_WHILEIT_pat[def_pat_rules]: "monadic_WHILEIT$I \ UNPROTECT (monadic_WHILEIT I)" by auto lemma id_monadic_WHILEIT[id_rules]: "PR_CONST (monadic_WHILEIT I) ::\<^sub>i TYPE(('a \ bool nres) \ ('a \ 'a nres) \ 'a \ 'a nres)" by simp lemma monadic_WHILEIT_arities[sepref_monadify_arity]: "PR_CONST (monadic_WHILEIT I) \ \\<^sub>2b f s. SP (PR_CONST (monadic_WHILEIT I))$(\\<^sub>2s. b$s)$(\\<^sub>2s. f$s)$s" by (simp) lemma monadic_WHILEIT_comb[sepref_monadify_comb]: "PR_CONST (monadic_WHILEIT I)$b$f$s \ Refine_Basic.bind$(EVAL$s)$(\\<^sub>2s. SP (PR_CONST (monadic_WHILEIT I))$b$f$s )" by (simp) 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)$(\\<^sub>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) ::\<^sub>i TYPE('a nres \ 'a nres)" by simp lemma arity_ASSERT_bind[sepref_monadify_arity]: "PR_CONST (op_ASSERT_bind I) \ \\<^sub>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 m" shows "hn_refine \ c \' R (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)$(\\<^sub>2_. m) \ UNPROTECT (op_ASSUME_bind I)$m" by simp lemma id_op_ASSUME_bind[id_rules]: "PR_CONST (op_ASSUME_bind I) ::\<^sub>i TYPE('a nres \ 'a nres)" by simp lemma arity_ASSUME_bind[sepref_monadify_arity]: "PR_CONST (op_ASSUME_bind I) \ \\<^sub>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 m" shows "hn_refine \ c \' R (PR_CONST (op_ASSUME_bind I)$m)" apply (rule hn_refine_preI) using assms apply (cases I) apply (auto simp: vassn_tag_def) done subsection "Import of Parametricity Theorems" lemma pure_hn_refineI: assumes "Q \ (c,a)\R" shows "hn_refine (\Q) (return c) (\Q) (pure R) (RETURN a)" unfolding hn_refine_def using assms by (sep_auto simp: pure_def) lemma pure_hn_refineI_no_asm: assumes "(c,a)\R" shows "hn_refine emp (return c) emp (pure R) (RETURN a)" unfolding hn_refine_def using assms by (sep_auto simp: pure_def) 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) 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" 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 (* TODO: Almost clone of Sepref_Rules.to_foparam*) 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]) - |> forall_intr_vars + |> 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 (* TODO: Hack. Need clean interfaces for fref and param rules. Also add PR_CONST to fref rules! *) | @{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 lemma precise_pure[constraint_rules]: "single_valued R \ precise (pure R)" unfolding precise_def pure_def by (auto dest: single_valuedD) lemma precise_pure_iff_sv: "precise (pure R) \ single_valued R" apply (auto simp: precise_pure) using preciseD[where R="pure R" and F=emp and F'=emp] by (sep_auto simp: mod_and_dist intro: single_valuedI) lemma pure_precise_iff_sv: "\is_pure R\ \ precise R \ single_valued (the_pure R)" by (auto simp: is_pure_conv precise_pure_iff_sv) lemmas [safe_constraint_rules] = single_valued_Id br_sv end