Theory ICF_Refine_Monadic

section ‹\isaheader{Refine-Monadci setup for ICF}›
theory ICF_Refine_Monadic
imports ICF_Impl
begin
text ‹
  This theory sets up some lemmas that automate refinement proofs using
  the Isabelle Collection Framework (ICF).
›

subsection ‹General Setup›

lemma (in set) drh[refine_dref_RELATES]: 
  "RELATES (build_rel α invar)" by (simp add: RELATES_def)
lemma (in map) drh[refine_dref_RELATES]: 
  "RELATES (build_rel α invar)" by (simp add: RELATES_def)

lemma (in uprio) drh[refine_dref_RELATES]: "RELATES (build_rel α invar)" 
  by (simp add: RELATES_def)
lemma (in prio) drh[refine_dref_RELATES]: "RELATES (build_rel α invar)" 
  by (simp add: RELATES_def)


lemmas (in StdSet) [refine_hsimp] = correct
lemmas (in StdMap) [refine_hsimp] = correct

lemma (in set_sel') pick_ref[refine_hsimp]:
  "⟦ invar s; α s ≠ {}⟧ ⟹ the (sel' s (λ_. True)) ∈ α s"
  by (auto elim!: sel'E)

(*text {* Wrapper to prevent higher-order unification problems *}
definition [simp, code_unfold]: "IT_tag x ≡ x"

lemma (in set_iteratei) it_is_iterator[refine_transfer]:
  "invar s ⟹ set_iterator (IT_tag iteratei s) (α s)"
  unfolding IT_tag_def by (rule iteratei_rule)

lemma (in map_iteratei) it_is_iterator[refine_transfer]:
  "invar m ⟹ set_iterator (IT_tag iteratei m) (map_to_set (α m))"
  unfolding IT_tag_def by (rule iteratei_rule)
*)

text ‹
  This definition is handy to be used on the abstract level.
›
definition "prio_pop_min q ≡ do {
    ASSERT (dom q ≠ {});
    SPEC (λ(e,w,q'). 
      q'=q(e:=None) ∧ 
      q e = Some w ∧ 
      (∀ e' w'. q e' = Some w' ⟶ w≤w')
    )
  }"

lemma (in uprio_pop) prio_pop_min_refine[refine]:
  "(q,q')∈build_rel α invar ⟹ RETURN (pop q) 
    ≤ ⇓ (⟨Id,⟨Id,br α invar⟩prod_rel⟩prod_rel) (prio_pop_min q')"
  unfolding prio_pop_min_def
  apply refine_rcg
  apply (clarsimp simp: prod_rel_def br_def)
  apply (erule (1) popE)
  apply (rule pw_leI)
  apply (auto simp: refine_pw_simps intro: ranI)
  done


subsection "Iterators"
lemmas (in poly_map_iteratei) [refine_transfer] = iteratei_correct
lemmas (in poly_map_iterateoi) [refine_transfer] = iterateoi_correct
lemmas (in map_no_invar) [refine_transfer] = invar

lemmas (in poly_set_iteratei) [refine_transfer] = iteratei_correct
lemmas (in poly_set_iterateoi) [refine_transfer] = iterateoi_correct
lemmas (in set_no_invar) [refine_transfer] = invar

lemma (in poly_set_iteratei) dres_ne_bot_iterate[refine_transfer]:
  assumes A: "⋀x s. f x s ≠ dSUCCEED"
  shows "iteratei r c (λx s. dbind s (f x)) (dRETURN s) ≠ dSUCCEED"
  unfolding iteratei_def it_to_list_def it_to_it_def
  apply (rule dres_foldli_ne_bot)
  by (simp_all add: A)
lemma (in poly_set_iterateoi) dres_ne_bot_iterateo[refine_transfer]:
  assumes A: "⋀x s. f x s ≠ dSUCCEED"
  shows "iterateoi r c (λx s. dbind s (f x)) (dRETURN s) ≠ dSUCCEED"
  unfolding iterateoi_def it_to_list_def it_to_it_def
  apply (rule dres_foldli_ne_bot)
  by (simp_all add: A)

lemma (in poly_map_iteratei) dres_ne_bot_map_iterate[refine_transfer]:
  assumes A: "⋀x s. f x s ≠ dSUCCEED"
  shows "iteratei r c (λx s. dbind s (f x)) (dRETURN s) ≠ dSUCCEED"
  unfolding iteratei_def it_to_list_def it_to_it_def
  apply (rule dres_foldli_ne_bot)
  by (simp_all add: A)
lemma (in poly_set_iterateoi) dres_ne_bot_map_iterateo[refine_transfer]:
  assumes A: "⋀x s. f x s ≠ dSUCCEED"
  shows "iterateoi r c (λx s. dbind s (f x)) (dRETURN s) ≠ dSUCCEED"
  unfolding iterateoi_def it_to_list_def it_to_it_def
  apply (rule dres_foldli_ne_bot)
  by (simp_all add: A)





subsection "Alternative FOREACH-transfer"
text ‹Required for manual refinements›
lemma transfer_FOREACHoci_plain[refine_transfer]:
  assumes A: "set_iterator_genord iterate s ordR"
  assumes R: "⋀x σ. RETURN (fi x σ) ≤ f x σ"
  shows "RETURN (iterate c fi σ) ≤ FOREACHoci ordR I s c f σ"
proof -
  from A obtain l where [simp]:
    "distinct l" 
    "s = set l" 
    "sorted_wrt ordR l"
    "iterate = foldli l" 
    unfolding set_iterator_genord_def by blast
  
  have "RETURN (foldli l c fi σ) ≤ nfoldli l c f σ"
    by (rule nfoldli_transfer_plain[OF R])
  also have "… = do { l ← RETURN l; nfoldli l c f σ }" by simp
  also have "… ≤ FOREACHoci ordR I s c f σ"
    apply (rule refine_IdD)
    unfolding FOREACHoci_def
    apply refine_rcg
    apply simp
    apply simp
    apply (rule nfoldli_while)
    done
  finally show ?thesis by simp
qed

lemma transfer_FOREACHoi_plain[refine_transfer]:
  assumes A: "set_iterator_genord iterate s ordR"
  assumes R: "⋀x σ. RETURN (fi x σ) ≤ f x σ"
  shows "RETURN (iterate (λ_. True) fi σ) ≤ FOREACHoi ordR I s f σ"
  using assms unfolding FOREACHoi_def by (rule transfer_FOREACHoci_plain)

lemma transfer_FOREACHci_plain[refine_transfer]:
  assumes A: "set_iterator iterate s"
  assumes R: "⋀x σ. RETURN (fi x σ) ≤ f x σ"
  shows "RETURN (iterate c fi σ) ≤ FOREACHci I s c f σ"
  using assms unfolding FOREACHci_def set_iterator_def
  by (rule transfer_FOREACHoci_plain)

lemma transfer_FOREACHi_plain[refine_transfer]:
  assumes A: "set_iterator iterate s"
  assumes R: "⋀x σ. RETURN (fi x σ) ≤ f x σ"
  shows "RETURN (iterate (λ_. True) fi σ) ≤ FOREACHi I s f σ"
  using assms unfolding FOREACHi_def
  by (rule transfer_FOREACHci_plain)

lemma transfer_FOREACHc_plain[refine_transfer]:
  assumes A: "set_iterator iterate s"
  assumes R: "⋀x σ. RETURN (fi x σ) ≤ f x σ"
  shows "RETURN (iterate c fi σ) ≤ FOREACHc s c f σ"
  using assms unfolding FOREACHc_def
  by (rule transfer_FOREACHci_plain)

lemma transfer_FOREACH_plain[refine_transfer]:
  assumes A: "set_iterator iterate s"
  assumes R: "⋀x σ. RETURN (fi x σ) ≤ f x σ"
  shows "RETURN (iterate (λ_. True) fi σ) ≤ FOREACH s f σ"
  using assms unfolding FOREACH_def
  by (rule transfer_FOREACHc_plain)

abbreviation "dres_it iterate c (fi::'a ⇒ 'b ⇒ 'b dres) σ ≡ 
  iterate (case_dres False False c) (λx s. s⤜fi x) (dRETURN σ)"

lemma transfer_FOREACHoci_nres[refine_transfer]:
  assumes A: "set_iterator_genord iterate s ordR"
  assumes R: "⋀x σ. nres_of (fi x σ) ≤ f x σ"
  shows "nres_of (dres_it iterate c fi σ) ≤ FOREACHoci ordR I s c f σ"
proof -
  from A obtain l where [simp]:
    "distinct l" 
    "s = set l" 
    "sorted_wrt ordR l"
    "iterate = foldli l" 
    unfolding set_iterator_genord_def by blast
  
  have "nres_of (dres_it (foldli l) c fi σ) ≤ nfoldli l c f σ"
    by (rule nfoldli_transfer_dres[OF R])
  also have "… = do { l ← RETURN l; nfoldli l c f σ }" by simp
  also have "… ≤ FOREACHoci ordR I s c f σ"
    apply (rule refine_IdD)
    unfolding FOREACHoci_def
    apply refine_rcg
    apply simp
    apply simp
    apply (rule nfoldli_while)
    done
  finally show ?thesis by simp
qed

lemma transfer_FOREACHoi_nres[refine_transfer]:
  assumes A: "set_iterator_genord iterate s ordR"
  assumes R: "⋀x σ. nres_of (fi x σ) ≤ f x σ"
  shows "nres_of (dres_it iterate (λ_. True) fi σ) ≤ FOREACHoi ordR I s f σ"
  using assms unfolding FOREACHoi_def by (rule transfer_FOREACHoci_nres)

lemma transfer_FOREACHci_nres[refine_transfer]:
  assumes A: "set_iterator iterate s"
  assumes R: "⋀x σ. nres_of (fi x σ) ≤ f x σ"
  shows "nres_of (dres_it iterate c fi σ) ≤ FOREACHci I s c f σ"
  using assms unfolding FOREACHci_def set_iterator_def
  by (rule transfer_FOREACHoci_nres)

lemma transfer_FOREACHi_nres[refine_transfer]:
  assumes A: "set_iterator iterate s"
  assumes R: "⋀x σ. nres_of (fi x σ) ≤ f x σ"
  shows "nres_of (dres_it iterate (λ_. True) fi σ) ≤ FOREACHi I s f σ"
  using assms unfolding FOREACHi_def
  by (rule transfer_FOREACHci_nres)

lemma transfer_FOREACHc_nres[refine_transfer]:
  assumes A: "set_iterator iterate s"
  assumes R: "⋀x σ. nres_of (fi x σ) ≤ f x σ"
  shows "nres_of (dres_it iterate c fi σ) ≤ FOREACHc s c f σ"
  using assms unfolding FOREACHc_def
  by (rule transfer_FOREACHci_nres)

lemma transfer_FOREACH_nres[refine_transfer]:
  assumes A: "set_iterator iterate s"
  assumes R: "⋀x σ. nres_of (fi x σ) ≤ f x σ"
  shows "nres_of (dres_it iterate (λ_. True) fi σ) ≤ FOREACH s f σ"
  using assms unfolding FOREACH_def
  by (rule transfer_FOREACHc_nres)


(*
lemma dres_ne_bot_iterate[refine_transfer]:
  assumes B: "set_iterator (IT_tag it r) S"
  assumes A: "⋀x s. f x s ≠ dSUCCEED"
  shows "IT_tag it r c (λx s. dbind s (f x)) (dRETURN s) ≠ dSUCCEED"
  apply (rule_tac I="λ_ s. s≠dSUCCEED" in set_iterator_rule_P[OF B])
  apply (rule dres_ne_bot_basic A | assumption)+
  done
*)

(*
subsubsection {* Monotonicity for Iterators *}

lemma it_mono_aux:
  assumes COND: "⋀σ σ'. σ≤σ' ⟹ c σ ≠ c σ' ⟹ σ=bot ∨ σ'=top "
  assumes STRICT: "⋀x. f x bot = bot" "⋀x. f' x top = top"
  assumes B: "σ≤σ'"
  assumes A: "⋀a x x'. x≤x' ⟹ f a x ≤ f' a x'"
  shows "foldli l c f σ ≤ foldli l c f' σ'"
proof -
  { fix l 
    have "foldli l c f bot = bot" by (induct l) (auto simp: STRICT)
  } note [simp] = this
  { fix l 
    have "foldli l c f' top = top" by (induct l) (auto simp: STRICT)
  } note [simp] = this

  show ?thesis
    using B
    apply (induct l arbitrary: σ σ')
    apply simp_all
    apply (metis assms foldli_not_cond)
    done
qed


lemma it_mono_aux_dres':
  assumes STRICT: "⋀x. f x bot = bot" "⋀x. f' x top = top"
  assumes A: "⋀a x x'. x≤x' ⟹ f a x ≤ f' a x'"
  shows "foldli l (case_dres True True c) f σ 
    ≤ foldli l (case_dres True True c) f' σ"
  apply (rule it_mono_aux)
  apply (simp_all split: dres.split_asm add: STRICT A)
  done

lemma it_mono_aux_dres:
  assumes A: "⋀a x. f a x ≤ f' a x"
  shows "foldli l (case_dres True True c) (λx s. dbind s (f x)) σ 
    ≤ foldli l (case_dres True True c) (λx s. dbind s (f' x)) σ"
  apply (rule it_mono_aux_dres')
  apply (simp_all)
  apply (rule dbind_mono)
  apply (simp_all add: A)
  done
  
lemma iteratei_mono':
  assumes L: "set_iteratei α invar it"
  assumes STRICT: "⋀x. f x bot = bot" "⋀x. f' x top = top"
  assumes A: "⋀a x x'. x≤x' ⟹ f a x ≤ f' a x'"
  assumes I: "invar s"
  shows "IT_tag it s (case_dres True True c) f σ 
    ≤ IT_tag it s (case_dres True True c) f' σ"
  proof -
    from set_iteratei.iteratei_rule[OF L, OF I, unfolded set_iterator_foldli_conv]
    obtain l0 where l0_props: "distinct l0" "α s = set l0" "it s = foldli l0" by blast
 
    from it_mono_aux_dres' [of f f' l0 c σ]
    show ?thesis
      unfolding IT_tag_def l0_props(3)
      by (simp add: STRICT A)
  qed

lemma iteratei_mono:
  assumes L: "set_iteratei α invar it"
  assumes A: "⋀a x. f a x ≤ f' a x"
  assumes I: "invar s"
  shows "IT_tag it s (case_dres True True c) (λx s. dbind s (f x)) σ 
    ≤ IT_tag it s (case_dres True True c) (λx s. dbind s (f' x)) σ"
 proof -
    from set_iteratei.iteratei_rule[OF L, OF I, unfolded set_iterator_foldli_conv]
    obtain l0 where l0_props: "distinct l0" "α s = set l0" "it s = foldli l0" by blast
 
    from it_mono_aux_dres [of f f' l0 c σ]
    show ?thesis
      unfolding IT_tag_def l0_props(3)
      by (simp add: A)
  qed

lemmas [refine_mono] = iteratei_mono[OF ls_iteratei_impl]
lemmas [refine_mono] = iteratei_mono[OF lsi_iteratei_impl]
lemmas [refine_mono] = iteratei_mono[OF rs_iteratei_impl]
lemmas [refine_mono] = iteratei_mono[OF ahs_iteratei_impl]
lemmas [refine_mono] = iteratei_mono[OF ias_iteratei_impl]
lemmas [refine_mono] = iteratei_mono[OF ts_iteratei_impl]
*)
(* Do not require the invariant for lsi_iteratei. 

This is kind of a hack -- the real fix comes with the new Collection/Refinement-Framework. *)
(*
lemma dres_ne_bot_iterate_lsi[refine_transfer]:
  fixes s :: "'a"
  assumes A: "⋀x s. f x s ≠ dSUCCEED"
  shows "IT_tag lsi_iteratei r c (λx s. dbind s (f x)) (dRETURN s) ≠ dSUCCEED"
proof -
  {
    fix l and s :: "'a dres"
    assume "s≠dSUCCEED" 
    hence "foldli l c (λx s. s⤜f x) s ≠ dSUCCEED"
      apply (induct l arbitrary: s)
      using A
      apply simp_all
      apply (intro impI)
      apply (metis dres_ne_bot_basic)
      done
  } note R=this
  with A show ?thesis
    unfolding lsi_iteratei_def
    by simp
qed


lemma iteratei_mono_lsi[refine_mono]:
  assumes A: "⋀a x. f a x ≤ f' a x"
  shows "IT_tag lsi_iteratei s (case_dres True True c) (λx s. dbind s (f x)) σ 
    ≤ IT_tag lsi_iteratei s (case_dres True True c) (λx s. dbind s (f' x)) σ"
 proof -
    from it_mono_aux_dres [of f f' s c σ]
    show ?thesis
      unfolding IT_tag_def lsi_iteratei_def
      by (simp add: A)
 qed
*)
end