# Theory Refine_Parallel

```theory
Refine_Parallel
imports
"HOL-Library.Parallel"
Ordinary_Differential_Equations.ODE_Auxiliarities
"../Refinement/Autoref_Misc"
"../Refinement/Weak_Set"
begin

context includes autoref_syntax begin

lemma dres_of_dress_impl:
"nres_of (rec_list (dRETURN []) (λx xs r. do { fx ← x; r ← r; dRETURN (fx # r)}) (Parallel.map f x)) ≤
nres_of_nress_impl (Parallel.map f' x)"
if [refine_transfer]: "⋀x. nres_of (f x) ≤ f' x"
unfolding Parallel.map_def nres_of_nress_impl_map
apply (induction x)
apply auto
apply refine_transfer
done
concrete_definition dres_of_dress_impl uses dres_of_dress_impl
lemmas [refine_transfer] = dres_of_dress_impl.refine

definition PAR_IMAGE::"('a ⇒ 'c ⇒ bool) ⇒ ('a ⇒ 'c nres) ⇒ 'a set ⇒ ('a × 'c) set nres" where
"PAR_IMAGE P f X = do {
xs ← list_spec X;
fxs ←nres_of_nress (λ(x, y). P x y) (Parallel.map (λx. do { y ← f x; RETURN (x, y)}) xs);
RETURN (set fxs)
}"

lemma [autoref_op_pat_def]: "PAR_IMAGE P ≡ OP (PAR_IMAGE P)" by auto
lemma [autoref_rules]: "(Parallel.map, Parallel.map) ∈ (A → B) → ⟨A⟩list_rel → ⟨B⟩list_rel"
unfolding Parallel.map_def
by parametricity
schematic_goal PAR_IMAGE_nres:
"(?r, PAR_IMAGE P \$ f \$ X) ∈ ⟨⟨A×⇩rB⟩list_wset_rel⟩nres_rel"
if [autoref_rules]: "(fi, f) ∈ A → ⟨B⟩nres_rel" "(Xi, X) ∈ ⟨A⟩list_wset_rel"
and [THEN PREFER_sv_D, relator_props]:
"PREFER single_valued A"  "PREFER single_valued B"
unfolding PAR_IMAGE_def
including art
by autoref
concrete_definition PAR_IMAGE_nres uses PAR_IMAGE_nres
lemma PAR_IMAGE_nres_impl_refine[autoref_rules]:
"PREFER single_valued A ⟹
PREFER single_valued B ⟹
(λfi Xi. PAR_IMAGE_nres fi Xi, PAR_IMAGE P)
∈ (A → ⟨B⟩nres_rel) → ⟨A⟩list_wset_rel → ⟨⟨A×⇩rB⟩list_wset_rel⟩nres_rel"
using PAR_IMAGE_nres.refine by force
schematic_goal PAR_IMAGE_dres:
assumes [refine_transfer]: "⋀x. nres_of (f x) ≤ f' x"
shows "nres_of (?f) ≤ PAR_IMAGE_nres f' X'"
unfolding PAR_IMAGE_nres_def
by refine_transfer
concrete_definition PAR_IMAGE_dres for f X' uses PAR_IMAGE_dres
lemmas [refine_transfer] = PAR_IMAGE_dres.refine

lemma nres_of_nress_Parallel_map_SPEC[le, refine_vcg]:
assumes "⋀x. x ∈ set xs ⟹ f x ≤ SPEC (I x)"
shows
"nres_of_nress (λ(x, y). I x y) (Parallel.map (λx. f x ⤜ (λy. RETURN (x, y))) xs) ≤
SPEC (λxrs. map fst xrs = xs ∧ (∀(x, r) ∈ set xrs. I x r))"
using assms
apply (induction xs)
subgoal by simp
apply clarsimp
apply (rule refine_vcg)
subgoal for x xs
apply (rule order_trans[of _ "SPEC (I x)"]) apply force
apply (rule refine_vcg)
apply (rule refine_vcg)
apply (rule order_trans, assumption)
apply refine_vcg
done
done

lemma PAR_IMAGE_SPEC[le, refine_vcg]:
"PAR_IMAGE I f X ≤ SPEC (λR. X = fst ` R ∧ (∀(x,r) ∈ R. I x r))"
if [le, refine_vcg]: "⋀x. x ∈ X ⟹ f x ≤ SPEC (I x)"
unfolding PAR_IMAGE_def
by refine_vcg

end

end```