Theory Hnr_Primitives_Experiment
section ‹Arrays and Option Arrays›
theory Hnr_Primitives_Experiment
imports Sepref "../ds/LLVM_DS_Dflt"
begin
hide_const (open) LLVM_DS_Array.array_assn
paragraph ‹Summary›
text ‹This theory introduces monadic operations on lists and lists with explicit ownership.
Then it defines data strucutres for arrays and arrays with explicit ownership.›
abbreviation "raw_array_assn ≡ ↿LLVM_DS_NArray.narray_assn"
lemma satminus_lift_acost: "satminus ta (the_acost (lift_acost t) b) = 0 ⟷ ta ≤ the_acost t b"
unfolding satminus_def lift_acost_def by auto
term lift_acost
lemma hnr_SPECT_D:
fixes Φ :: "_ ⇒ ((_,enat) acost) option"
shows
"do { ASSERT P; consume (RETURNT x) (lift_acost t) } = SPECT Φ
⟹ P ∧ Some (lift_acost t) ≤ Φ x"
apply(simp add: pw_acost_eq_iff)
apply(simp add: refine_pw_simps)
apply(auto simp: satminus_lift_acost)
apply(cases "Φ x")
subgoal
by force
subgoal premises prems for e
apply(rule acost_componentwise_leI[where e=e] )
subgoal using prems by simp
subgoal for b
using prems(2)[rule_format, where x=x and t="the_acost t b" and b=b]
using prems(3)
by (auto simp: lift_acost_def)
done
done
lemma lift_acost_plus_distrib[named_ss fri_prepare_simps]:
"$lift_acost (a + b) = ($lift_acost a ** $lift_acost b)"
unfolding time_credits_assn_def lift_acost_def SND_def EXACT_def
apply (cases a; cases b)
apply (auto simp add: sep_algebra_simps fun_eq_iff sep_conj_def sep_disj_acost_def sep_disj_enat_def)
done
lemma snat_assn_to_basic_layer: "snat_assn = ↿snat.assn"
by (simp add: snat.assn_is_rel snat_rel_def)
lemma DECOMP_HNR[vcg_decomp_rules]: "DECOMP_HTRIPLE (hn_refine Γ c Γ' R a) ⟹ hn_refine Γ c Γ' R a" by (simp add: vcg_tag_defs)
lemma hn_refine_pre_pureI:
assumes "pure_part Γ ⟹ hn_refine Γ c Γ' R a"
shows "hn_refine Γ c Γ' R a"
using assms unfolding hn_refine_def
apply auto
using prep_ext_state pure_part_split_conj by blast
lemma hnr_mop_vcgI[htriple_vcg_intros]:
assumes "⋀F s cr. ⟦Φ; pure_part Γ; llSTATE (Γ**F**$(lift_acost t)) (s,cr+(lift_acost t))⟧ ⟹
EXTRACT (wp c (λri. POSTCOND ll_α (Γ' ** R r ri ** F ** GC)) (s,cr+lift_acost t))"
shows "hn_refine Γ c Γ' R (do {ASSERT Φ; consume (RETURNT r) (lift_acost t)})"
apply (rule hn_refine_pre_pureI)
apply (rule hnr_vcgI)
apply(drule hnr_SPECT_D, clarify)
apply (rule exI[where x="r"])
apply (rule exI[where x="t"])
using assms by blast
lemmas hnr_mop_vcgI_nopre[htriple_vcg_intros] = hnr_mop_vcgI[where Φ=True, simplified]
subsection ‹List Operations›
subsubsection ‹Monadic List Operations›
context
fixes T :: "(nat × nat) ⇒ (char list, enat) acost"
begin
definition mop_list_get :: "'a list ⇒ nat ⇒ ('a, _) nrest"
where [simp]: "mop_list_get xs i ≡ do { ASSERT (i<length xs); consume (RETURNT (xs!i)) (T (length xs,i)) }"
sepref_register "mop_list_get"
end
lemma param_mop_list_get:
"(mop_list_get T, mop_list_get T) ∈ ⟨the_pure A⟩ list_rel → nat_rel → ⟨the_pure A⟩ nrest_rel"
apply(intro nrest_relI fun_relI)
unfolding mop_list_get_def
apply (auto simp: pw_acost_le_iff refine_pw_simps list_rel_imp_same_length)
apply parametricity
by simp
context
fixes T :: "(nat × unit × unit) ⇒ (char list, enat) acost"
begin
definition [simp]: "mop_list_set xs i x ≡ do { ASSERT (i<length xs); consume (RETURNT (xs[i:=x])) (T (length xs,(),())) }"
sepref_register "mop_list_set"
print_theorems
end
lemma param_mop_list_set:
"(mop_list_set T, mop_list_set T) ∈ ⟨the_pure A⟩ list_rel → nat_rel → (the_pure A) → ⟨⟨the_pure A⟩ list_rel⟩ nrest_rel"
apply(intro nrest_relI fun_relI)
unfolding mop_list_set_def
apply (auto simp: pw_acost_le_iff refine_pw_simps list_rel_imp_same_length)
apply parametricity
by simp
context
fixes T :: "(nat × unit) ⇒ (char list, enat) acost"
begin
definition [simp]: "mop_list_replicate n x ≡ do { ASSERT (PROTECT True); consume (RETURNT (replicate n x)) (T (n,())) }"
sepref_register "mop_list_replicate"
end
lemma param_mop_list_replicate:
"(mop_list_replicate T, mop_list_replicate T) ∈ nat_rel → (A) → ⟨⟨A⟩ list_rel⟩ nrest_rel"
apply(intro nrest_relI fun_relI)
unfolding mop_list_replicate_def
apply (auto simp: pw_acost_le_iff refine_pw_simps list_rel_imp_same_length)
apply parametricity
by simp
context
fixes T :: "(nat) ⇒ (char list, enat) acost"
begin
definition [simp]: "mop_list_init x n ≡ do { ASSERT (PROTECT True); consume (RETURNT (replicate n x)) (T n) }"
definition [simp]: "mop_list_init_raw n ≡ do { ASSERT (PROTECT True); consume (RETURNT (replicate n init)) (T n) }"
context fixes x begin sepref_register "mop_list_init x" end
sepref_register "mop_list_init_raw"
end
find_theorems is_init
lemma refine_mop_list_init_raw:
assumes "GEN_ALGO x (is_init A)"
shows "(mop_list_init_raw T, PR_CONST (mop_list_init T x)) ∈ nat_rel → ⟨⟨the_pure A⟩ list_rel⟩ nrest_rel"
using assms
apply(intro nrest_relI fun_relI)
unfolding mop_list_init_def mop_list_init_raw_def
unfolding GEN_ALGO_def is_init_def
apply (auto simp: pw_acost_le_iff refine_pw_simps list_rel_imp_same_length)
apply parametricity
by simp
subsubsection ‹Monadic Option List Operations›
context
fixes T :: "(nat × unit) ⇒ (char list, enat) acost"
begin
definition mop_eo_extract :: "'a option list ⇒ nat ⇒ (_, _) nrest"
where [simp]: "mop_eo_extract xs i ≡ do { ASSERT (i<length xs ∧ xs!i≠None); consume (RETURNT (the (xs!i), xs[i:=None])) (T (length xs,())) }"
sepref_register "mop_eo_extract"
end
context
fixes T :: "(nat × unit × unit) ⇒ (char list, enat) acost"
begin
definition [simp]: "mop_eo_set xs i x ≡ do { ASSERT (i<length xs ∧ xs!i=None); consume (RETURNT (xs[i:=Some x])) (T (length xs,(),())) }"
sepref_register "mop_eo_set"
print_theorems
end
context
fixes T :: "(nat) ⇒ (char list, enat) acost"
begin
definition [simp]: "mop_olist_new n ≡ do { ASSERT (PROTECT True); consume (RETURNT (replicate n None)) (T n) }"
sepref_register "mop_olist_new"
end
lemma param_mop_olist_new:
"(mop_olist_new T, mop_olist_new T) ∈ nat_rel → ⟨⟨⟨the_pure A⟩ option_rel⟩ list_rel⟩ nrest_rel"
apply(intro nrest_relI fun_relI)
unfolding mop_olist_new_def
apply (auto simp: pw_acost_le_iff refine_pw_simps list_rel_imp_same_length)
apply parametricity
by simp
subsubsection ‹Array Operation costs›
abbreviation "mop_array_nth_cost ≡ (cost ''load'' (Suc 0)+cost ''ofs_ptr'' (Suc 0))"
abbreviation "mop_array_upd_cost ≡ (cost ''store'' (Suc 0)+cost ''ofs_ptr'' (Suc 0))"
abbreviation "cost'_narray_new n ≡ cost ''malloc'' n + cost ''free'' 1 + cost ''if'' 1 + cost ''if'' 1 + cost ''icmp_eq'' 1 + cost ''ptrcmp_eq'' 1"
subsection ‹Option Array›
text ‹Assertion that adds constraint on concrete value. Used to carry through concrete equalities.›
definition "cnc_assn φ A a c ≡ ↑(φ c) ** A a c"
lemma cnc_assn_prod_conv[named_ss sepref_frame_normrel]:
shows "⋀A B φ. A ×⇩a cnc_assn φ B = cnc_assn (φ o snd) (A×⇩aB)"
and "⋀A B φ. cnc_assn φ A ×⇩a B = cnc_assn (φ o fst) (A×⇩aB)"
unfolding cnc_assn_def
by (auto simp: sep_algebra_simps fun_eq_iff)
lemma norm_ceq_assn[named_ss sepref_frame_normrel]: "hn_ctxt (cnc_assn φ A) a c = (↑(φ c) ** hn_ctxt A a c)"
unfolding hn_ctxt_def cnc_assn_def by simp
definition "mop_oarray_extract ≡ mop_eo_extract (λ_. lift_acost mop_array_nth_cost)"
lemma "mop_oarray_extract xs i = doN { ASSERT (i<length xs ∧ xs!i≠None); consume (RETURNT (the (xs!i), xs[i:=None])) (lift_acost mop_array_nth_cost) }"
by(auto simp: mop_oarray_extract_def)
definition "mop_oarray_upd ≡ mop_eo_set (λ_. lift_acost mop_array_upd_cost)"
lemma "mop_oarray_upd xs i x = do { ASSERT (i<length xs ∧ xs!i=None); consume (RETURNT (xs[i:=Some x])) (lift_acost mop_array_upd_cost) }"
by(auto simp: mop_oarray_upd_def)
definition "mop_oarray_new ≡ mop_olist_new (λn. lift_acost (cost'_narray_new n))"
lemma "mop_oarray_new n = consume (RETURNT (replicate n None)) (lift_acost (cost'_narray_new n))"
by(auto simp: mop_oarray_new_def)
sepref_register mop_oarray_extract
definition "eoarray_assn A ≡ ↿(nao_assn (mk_assn A))"
definition [llvm_inline]: "eoarray_nth_impl xsi ii ≡ doM {
r ← array_nth xsi ii;
return (r,xsi)
}"
lemma hnr_eoarray_nth: "hn_refine
(hn_ctxt (eoarray_assn A) xs xsi ** hn_ctxt snat_assn i ii)
(eoarray_nth_impl xsi ii)
(hn_invalid (eoarray_assn A) xs xsi ** hn_ctxt snat_assn i ii)
(cnc_assn (λ(_,xsi'). xsi'=xsi) (A ×⇩a eoarray_assn A))
(mop_oarray_extract $ xs $ i)"
unfolding snat_assn_to_basic_layer
unfolding hn_ctxt_def pure_def invalid_assn_def cnc_assn_def eoarray_assn_def mop_oarray_extract_def eoarray_nth_impl_def
by vcg
lemma hnr_eoarray_nth'[sepref_fr_rules]: "(uncurry eoarray_nth_impl, uncurry mop_oarray_extract)
∈ (eoarray_assn A)⇧d *⇩a snat_assn⇧k →⇩a⇩d (λx (ai, _). A ×⇩a cnc_assn (λx. x = ai) (eoarray_assn A))"
unfolding snat_assn_to_basic_layer
apply(rule hfrefI)
unfolding to_hnr_prod_fst_snd keep_drop_sels hf_pres_fst mop_oarray_extract_def hn_ctxt_def
pure_def invalid_assn_def cnc_assn_def eoarray_assn_def eoarray_nth_impl_def
by vcg
lemma hnr_eoarray_upd: "hn_refine
(hn_ctxt (eoarray_assn A) xs xsi ** hn_ctxt snat_assn i ii ** hn_ctxt A x xi)
(array_upd xsi ii xi)
(hn_invalid (eoarray_assn A) xs xsi ** hn_ctxt snat_assn i ii ** hn_invalid A x xi)
(cnc_assn (λri. ri=xsi) (eoarray_assn A))
(mop_oarray_upd $ xs $ i $ x)"
unfolding snat_assn_to_basic_layer
unfolding hn_ctxt_def pure_def invalid_assn_def cnc_assn_def eoarray_assn_def mop_oarray_upd_def
by vcg
lemma hnr_eoarray_upd'[sepref_fr_rules]: "(uncurry2 array_upd, uncurry2 mop_oarray_upd)
∈ (eoarray_assn A)⇧d *⇩a snat_assn⇧k *⇩a A⇧d →⇩a⇩d (λx ((ai, _), _). cnc_assn (λx. x = ai) (eoarray_assn A))"
unfolding snat_assn_to_basic_layer
apply(rule hfrefI)
unfolding to_hnr_prod_fst_snd keep_drop_sels hf_pres_fst mop_oarray_upd_def hn_ctxt_def pure_def
invalid_assn_def cnc_assn_def eoarray_assn_def eoarray_nth_impl_def
by vcg
lemma hnr_eoarray_new: "hn_refine
(hn_ctxt snat_assn i ii)
(narrayo_new TYPE('a::llvm_rep) ii)
(hn_ctxt snat_assn i ii)
(eoarray_assn A)
(mop_oarray_new i)"
unfolding snat_assn_to_basic_layer
unfolding hn_ctxt_def pure_def invalid_assn_def eoarray_assn_def mop_oarray_new_def
by vcg
lemma hnr_eoarray_new'[sepref_fr_rules]: "( (narrayo_new TYPE('a::llvm_rep)), mop_oarray_new )
∈ snat_assn⇧k →⇩a (eoarray_assn A)"
unfolding snat_assn_to_basic_layer
apply(rule hfrefI)
unfolding to_hnr_prod_fst_snd keep_drop_sels hf_pres_fst hn_ctxt_def pure_def invalid_assn_def mop_oarray_new_def cnc_assn_def eoarray_assn_def eoarray_nth_impl_def
by vcg
definition "mop_oarray_free xs ≡ do { ASSERT (set xs ⊆ {None}); consume (RETURNT ()) (lift_acost 0) }"
lemma hnr_eoarray_free[sepref_fr_rules]: "hn_refine
(hn_ctxt (eoarray_assn A) xs xsi)
(narray_free xsi)
(hn_invalid (eoarray_assn A) xs xsi)
(id_assn)
(mop_oarray_free $ xs)"
unfolding hn_ctxt_def pure_def invalid_assn_def eoarray_assn_def mop_oarray_free_def
apply vcg_step
apply vcg_step
by vcg
definition "mop_to_eo_conv xs ≡ do { consume (RETURNT (map Some xs)) (lift_acost 0) }"
definition "mop_to_wo_conv xs ≡ do { ASSERT (None∉set xs); consume (RETURNT (map the xs)) (lift_acost 0) }"
sepref_register mop_to_eo_conv
lemma mop_to_eo_conv_alt: "mop_to_eo_conv xs ≡ (RETURNT (map Some xs)) "
unfolding mop_to_eo_conv_def lift_acost_zero consume_0 .
lemma mop_to_eo_conv_refine: "wfR'' R ⟹ (xs,xs')∈Id ⟹ mop_to_eo_conv xs ≤ ⇓ Id (timerefine R (mop_to_eo_conv xs'))"
unfolding mop_to_eo_conv_def
apply(intro refine0)
by (auto simp: lift_acost_zero simp del: conc_Id )
lemma mop_to_wo_conv_refines: "wfR'' R ⟹ (a,a')∈Id ⟹ mop_to_wo_conv a ≤ ⇓ Id (timerefine R (mop_to_wo_conv a'))"
unfolding mop_to_wo_conv_def
apply(intro refine0 bindT_refine_easy SPECc2_refine')
by (auto simp: lift_acost_zero)
definition "some_rel ≡ br the (Not o is_None)"
definition "array_assn A ≡ hr_comp (eoarray_assn A) (⟨some_rel⟩list_rel)"
lemma map_the_some_rel_list_rel_iff: "(xs, map the xs) ∈ ⟨some_rel⟩list_rel ⟷ None ∉ set xs"
unfolding some_rel_def
apply (auto simp: map_in_list_rel_conv split: option.splits)
by (metis option.exhaust)
lemma map_in_list_rel_br_iff: "(map f xs, xs) ∈ ⟨br α I⟩list_rel ⟷ (∀x∈set xs. I (f x) ∧ α (f x) = x)"
apply (induction xs)
apply (auto simp: in_br_conv)
done
lemma in_br_list_rel_conv: "(xs,ys) ∈ ⟨br α I⟩list_rel ⟷ (∀x∈set xs. I x) ∧ ys = map α xs"
apply (rule)
subgoal premises prems
using prems
apply (induction rule: list_rel_induct)
by (auto simp: in_br_conv)
subgoal by (auto simp: map_in_list_rel_conv)
done
lemma in_some_rel_list_rel_conv: "(x,xi) ∈⟨some_rel⟩list_rel ⟷ x = map Some xi"
unfolding some_rel_def
by (auto simp: in_br_list_rel_conv map_idI split: option.splits)
lemma hnr_to_wo_conv[sepref_fr_rules]: "hn_refine
(hn_ctxt (eoarray_assn A) xs xsi)
(return xsi)
(hn_invalid (eoarray_assn A) xs xsi)
(array_assn A)
(mop_to_wo_conv $ xs)"
unfolding mop_to_wo_conv_def
unfolding hn_ctxt_def pure_def invalid_assn_def eoarray_assn_def
array_assn_def hr_comp_def
apply Basic_VCG.vcg'
apply (simp add: map_the_some_rel_list_rel_iff)
done
lemma mop_to_wo_conv_hnr_dep: "(return,mop_to_wo_conv)∈(eoarray_assn A)⇧d →⇩a⇩d (λ_ xi. cnc_assn (λx. x=xi) (array_assn A))"
unfolding mop_to_wo_conv_def cnc_assn_def
apply(rule hfrefI) apply simp
unfolding hn_ctxt_def pure_def invalid_assn_def eoarray_assn_def
array_assn_def hr_comp_def
apply Basic_VCG.vcg'
apply (simp add: map_the_some_rel_list_rel_iff)
done
lemma hnr_to_eo_conv[sepref_fr_rules]: "hn_refine
(hn_ctxt (array_assn A) xs xsi)
(return xsi)
(hn_invalid (array_assn A) xs xsi)
(eoarray_assn A)
(mop_to_eo_conv $ xs)"
unfolding hn_ctxt_def pure_def invalid_assn_def eoarray_assn_def mop_to_eo_conv_def
array_assn_def hr_comp_def
supply [simp] = in_some_rel_list_rel_conv
by vcg
lemma mop_to_eo_conv_hnr_dep: "(return,mop_to_eo_conv)∈(array_assn A)⇧d →⇩a⇩d (λ_ xi. cnc_assn (λx. x=xi) (eoarray_assn A))"
unfolding mop_to_eo_conv_def cnc_assn_def
apply(rule hfrefI) apply simp
unfolding mop_to_eo_conv_def cnc_assn_def
unfolding hn_ctxt_def pure_def invalid_assn_def eoarray_assn_def
array_assn_def hr_comp_def
supply [simp] = in_some_rel_list_rel_conv
by vcg
lemma the_pure_pure_part_conv: "is_pure A ⟹ the_pure A = {(c,a). pure_part (A a c)}"
apply safe
subgoal by (metis Sepref_Basic.pure_part_pure pure_the_pure)
subgoal by (metis Sepref_Basic.pure_part_pure pure_the_pure)
done
lemma is_pure_assn_pred_lift: "is_pure A ⟹ A a c = ↑((c,a)∈the_pure A)"
by (metis Sepref_Basic.pure_def pure_the_pure)
lemma pure_list_assn_list_rel_conv: "is_pure A ⟹ ↿(list_assn (mk_assn A)) xs xsi = ↑((xsi,xs)∈⟨the_pure A⟩list_rel)"
proof (induction xs arbitrary: xsi)
case Nil
then show ?case by simp
next
case (Cons a xs)
then show ?case
apply (cases xsi; simp)
by (auto simp add: sep_algebra_simps pred_lift_extract_simps fun_eq_iff is_pure_assn_pred_lift)
qed
definition [to_relAPP]: "oelem_rel A ≡ {(c,a) . case a of None ⇒ True | Some b ⇒ (c,b)∈A}"
lemma oelem_pure_assn_conv: "oelem_assn (mk_assn (pure A)) = mk_assn (pure (⟨A⟩oelem_rel))"
unfolding oelem_assn_def sel_mk_assn oelem_rel_def
apply (rule arg_cong[where f=mk_assn])
by (auto simp: fun_eq_iff pure_def sep_algebra_simps split: option.split )
lemma map_some_oelem_list_rel_conv: "(xs, map Some ys) ∈ ⟨⟨R⟩oelem_rel⟩list_rel ⟷ (xs,ys) ∈ ⟨R⟩list_rel"
proof (induction xs arbitrary: ys)
case Nil
then show ?case by auto
next
case (Cons a xs)
then show ?case
apply (cases ys)
by (auto simp: oelem_rel_def)
qed
definition "unborrow src dst ≡ doN {ASSERT (src=dst); RETURN ()}"
sepref_register unborrow
lemma unborrow_rule[sepref_comb_rules]:
assumes FRAME: "Γ ⊢ hn_ctxt R src srci ** hn_invalid R dst dsti ** F"
assumes [simp]: "vassn_tag Γ ⟹ srci = dsti"
shows "hn_refine Γ (return ():: _ llM) (hn_invalid R src srci ** hn_ctxt R dst dsti ** F) unit_assn (unborrow$src$dst)"
apply (rule hn_refine_vassn_tagI)
apply (rule hn_refine_cons_pre[rotated,OF FRAME])
unfolding unborrow_def APP_def
apply (rule hn_refineI'')
apply (simp add: refine_pw_simps)
unfolding hn_ctxt_def invalid_assn_def pure_def
by vcg'
subsection ‹Array›
definition "mop_array_nth ≡ mop_list_get (λ_. lift_acost mop_array_nth_cost) "
definition "mop_array_upd ≡ mop_list_set (λ_. lift_acost mop_array_upd_cost)"
definition mop_array_new :: "('a ⇒ 'c ⇒ assn) ⇒ 'a ⇒ nat ⇒ ('a list, ecost) nrest"
where "mop_array_new A ≡ mop_list_init (λn. lift_acost (cost'_narray_new n))"
context fixes A :: "'a ⇒ 'c ⇒ assn" and x :: 'a begin
sepref_register "mop_array_new A x"
end
subsubsection ‹Raw hnr rules›
thm vcg_rules
lemma hnr_raw_array_nth: "hn_refine
(hn_ctxt raw_array_assn xs xsi ** hn_ctxt snat_assn i ii)
(array_nth xsi ii)
(hn_ctxt raw_array_assn xs xsi ** hn_ctxt snat_assn i ii)
id_assn
(mop_array_nth xs i)"
unfolding snat_assn_to_basic_layer
unfolding hn_ctxt_def pure_def mop_array_nth_def
apply vcg_step
apply vcg_step
by vcg
lemma hnr_raw_array_upd: "((uncurry2 array_upd, uncurry2 mop_array_upd)
∈ [λ((a, b), x). True]⇩a raw_array_assn⇧d *⇩a snat_assn⇧k *⇩a id_assn⇧k → raw_array_assn)"
unfolding snat_assn_to_basic_layer
apply(intro hfrefI)
unfolding to_hnr_prod_fst_snd keep_drop_sels hf_pres_fst hn_ctxt_def pure_def invalid_assn_def mop_array_upd_def
by vcg
lemma hnr_raw_array_new:
"(narray_new TYPE('a::llvm_rep), mop_list_init_raw (λn. lift_acost (cost'_narray_new n))) : snat_assn⇧k →⇩a raw_array_assn"
unfolding snat_assn_to_basic_layer
apply (rule hfrefI)
unfolding hn_ctxt_def pure_def invalid_assn_def mop_array_new_def mop_list_init_raw_def
by vcg
lemma FREE_raw_array_assn: "MK_FREE raw_array_assn narray_free"
apply rule
by vcg
subsubsection ‹hnr rules›
lemma pure_array_assn_alt:
assumes "is_pure A"
shows "array_assn A = hr_comp raw_array_assn (⟨the_pure A⟩list_rel)"
apply (rewrite pure_the_pure[of A, symmetric, OF assms])
unfolding array_assn_def eoarray_assn_def nao_assn_def hr_comp_def
apply (auto
simp: fun_eq_iff sep_algebra_simps pred_lift_extract_simps oelem_pure_assn_conv
simp: pure_list_assn_list_rel_conv in_some_rel_list_rel_conv map_some_oelem_list_rel_conv
)
done
lemma norm_array_assn[fcomp_norm_simps]:
assumes "CONSTRAINT is_pure A"
shows "hr_comp raw_array_assn (⟨the_pure A⟩list_rel) = array_assn A"
using pure_array_assn_alt[OF assms[THEN CONSTRAINT_D]] by simp
lemma one_time_bind_ASSERT: "(Φ ⟹ one_time m) ⟹ one_time (do {_ ← ASSERT Φ; m })"
apply(cases Φ) by (auto simp: OT_fail)
context
fixes A :: "'a ⇒ 'b:: llvm_rep ⇒ assn"
assumes [fcomp_norm_simps]: "CONSTRAINT is_pure A"
begin
lemma hnr_array_upd[sepref_fr_rules]: "(uncurry2 array_upd, uncurry2 mop_array_upd) ∈ (array_assn A)⇧d *⇩a snat_assn⇧k *⇩a A⇧k →⇩a array_assn A"
apply(rule hnr_raw_array_upd[unfolded mop_array_upd_def, FCOMP param_mop_list_set[of _ A], folded mop_array_upd_def])
unfolding SC_attains_sup_def mop_array_upd_def
apply safe
apply(rule one_time_attains_sup)
apply simp
by(intro OT_consume OT_return one_time_bind_ASSERT)
lemma hnr_array_nth[sepref_fr_rules]: "(uncurry array_nth, uncurry mop_array_nth) ∈ (array_assn A)⇧k *⇩a snat_assn⇧k →⇩a A"
apply(rule hnr_raw_array_nth[unfolded mop_array_nth_def, FCOMP param_mop_list_get[of _ A], folded mop_array_nth_def])
unfolding SC_attains_sup_def mop_array_nth_def
apply safe
apply(rule one_time_attains_sup)
apply simp
by(intro OT_consume OT_return one_time_bind_ASSERT)
end
thm OT_intros
context
fixes A :: "'a ⇒ 'c:: llvm_rep ⇒ assn"
and x :: 'a
assumes INIT: "GEN_ALGO x (is_init A)"
begin
private lemma PURE: "CONSTRAINT is_pure A"
using INIT unfolding GEN_ALGO_def CONSTRAINT_def is_init_def by simp
context
notes PURE[fcomp_norm_simps]
begin
lemma cheat[OT_intros]: "SC_attains_sup (∀a1 b1. attains_sup (mop_list_init_raw (λn. lift_acost (cost'_narray_new n)) b1) (PR_CONST (mop_array_new A x) a1) (⟨the_pure A⟩list_rel))"
apply(intro allI SC_attains_supI)
apply (rule one_time_attains_sup)
unfolding PR_CONST_def mop_array_new_def mop_list_init_def apply simp
apply(intro OT_intros) done
lemmas hnr_array_new[sepref_fr_rules]
= hnr_raw_array_new[FCOMP refine_mop_list_init_raw[OF INIT], folded mop_array_new_def[of A], OF cheat]
end
end
lemma FREE_hrcompI:
assumes "MK_FREE (A) f"
shows "MK_FREE (hr_comp A R) f"
supply [vcg_rules] = MK_FREED[OF assms]
apply (rule)
unfolding hr_comp_def
by vcg
lemma FREE_array_assn[sepref_frame_free_rules]:
assumes PURE: "is_pure A"
shows "MK_FREE (array_assn A) narray_free"
apply (rewrite pure_array_assn_alt[OF PURE])
apply (rule FREE_hrcompI)
apply (rule FREE_raw_array_assn)
done
end