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