Theory Refine_Monadic.Refine_Transfer

section ‹Transfer Setup›
theory Refine_Transfer
imports
  Refine_Basic
  Refine_While
  Refine_Det 
  "Generic/RefineG_Transfer"
begin

subsection ‹Transfer to Deterministic Result Lattice›
text ‹
  TODO: Once lattice and ccpo are connected, also transfer to option monad, that
  is a ccpo, but no complete lattice!
›
subsubsection ‹Connecting Deterministic and Non-Deterministic Result Lattices›
definition "nres_of r ≡ case r of
  dSUCCEEDi ⇒ SUCCEED
| dFAILi ⇒ FAIL
| dRETURN x ⇒ RETURN x"

lemma nres_of_simps[simp]:
  "nres_of dSUCCEED = SUCCEED"
  "nres_of dFAIL = FAIL"
  "nres_of (dRETURN x) = RETURN x"
  apply -
  unfolding nres_of_def bot_dres_def top_dres_def
  by (auto simp del: dres_internal_simps)

lemma nres_of_mono: "mono nres_of"
  apply (rule)
  apply (case_tac x, simp_all, case_tac y, simp_all)
  done

lemma nres_transfer:
  "nres_of dSUCCEED = SUCCEED"
  "nres_of dFAIL = FAIL"
  "nres_of a ≤ nres_of b ⟷ a≤b"
  "nres_of a < nres_of b ⟷ a<b"
  "is_chain A ⟹ nres_of (Sup A) = Sup (nres_of`A)"
  "is_chain A ⟹ nres_of (Inf A) = Inf (nres_of`A)"
  apply simp_all
  apply (case_tac a, simp_all, case_tac [!] b, simp_all) [1]

  apply (simp add: less_le)
  apply (case_tac a, simp_all, case_tac [!] b, simp_all) [1]

  apply (erule dres_Sup_chain_cases)
    apply (cases "A={}")
    apply auto []
    apply (subgoal_tac "A={dSUCCEED}", auto) []

    apply (case_tac "A={dRETURN r}")
    apply auto []
    apply (subgoal_tac "A={dSUCCEED,dRETURN r}", auto) []

    apply (drule imageI[where f=nres_of])
    apply auto []

  apply (erule dres_Inf_chain_cases)
    apply (cases "A={}")
    apply auto []
    apply (subgoal_tac "A={dFAIL}", auto) []

    apply (case_tac "A={dRETURN r}")
    apply auto []
    apply (subgoal_tac "A={dFAIL,dRETURN r}", auto) []

    apply (drule imageI[where f=nres_of])
    apply (auto intro: bot_Inf [symmetric]) []
  done

lemma nres_correctD:
  assumes "nres_of S ≤ SPEC Φ"
  shows 
  "S=dRETURN x ⟹ Φ x"
  "S≠dFAIL"
  using assms apply -
  apply (cases S, simp_all)+
  done

subsubsection ‹Transfer Theorems Setup›
interpretation dres: dist_transfer nres_of 
  apply unfold_locales
  apply (simp add: nres_transfer)
  done

lemma nres_of_transfer[refine_transfer]: "nres_of x ≤ nres_of x" by simp

lemma det_FAIL[refine_transfer]: "nres_of (dFAIL) ≤ FAIL" by auto
lemma det_SUCCEED[refine_transfer]: "nres_of (dSUCCEED) ≤ SUCCEED" by auto
lemma det_SPEC: "Φ x ⟹ nres_of (dRETURN x) ≤ SPEC Φ" by simp
lemma det_RETURN[refine_transfer]: 
  "nres_of (dRETURN x) ≤ RETURN x" by simp
lemma det_bind[refine_transfer]:
  assumes "nres_of m ≤ M"
  assumes "⋀x. nres_of (f x) ≤ F x"
  shows "nres_of (dbind m f) ≤ bind M F"
  using assms 
  apply (cases m) 
  apply (auto simp: pw_le_iff refine_pw_simps)
  done

interpretation det_assert: transfer_generic_Assert_remove 
  bind RETURN ASSERT ASSUME
  nres_of
  by unfold_locales

interpretation det_while: transfer_WHILE
  dbind dRETURN dWHILEIT dWHILEI dWHILET dWHILE 
  bind RETURN WHILEIT WHILEI WHILET WHILE nres_of
  apply unfold_locales
  apply (auto intro: det_bind)
  done

(*
interpretation det_foreach: 
  transfer_FOREACH nres_of dRETURN dbind "case_dres True True"
  apply unfold_locales
  apply (blast intro: det_bind)
  apply simp
  apply (case_tac m)
  apply simp_all
  done
*)

(* Done generally in RefineG_Transfer
lemma det_rec_list[refine_transfer]:
  assumes FN: "⋀s. RETURN (fn s) ≤ (fn' s)"
  assumes FC: "⋀x l rec rec' s. ⟦ ⋀s. RETURN (rec s) ≤ (rec' s) ⟧ 
    ⟹ RETURN (fc x l rec s) ≤ fc' x l rec' s"
  shows "RETURN (rec_list fn fc l s) ≤ rec_list fn' fc' l s"
  apply (induct l arbitrary: s)
  apply (simp add: FN)
  apply (simp add: FC)
  done

lemma det_rec_nat[refine_transfer]:
  assumes FN: "⋀s. RETURN (fn s) ≤ (fn' s)"
  assumes FC: "⋀n rec rec' s. ⟦ ⋀s. RETURN (rec s) ≤ (rec' s) ⟧ 
    ⟹ RETURN (fc x l rec s) ≤ fc' x l rec' s"
  shows "RETURN (rec_list fn fc l s) ≤ rec_list fn' fc' l s"
  apply (induct l arbitrary: s)
  apply (simp add: FN)
  apply (simp add: FC)
  done
*)

subsection ‹Transfer to Plain Function›

interpretation plain: transfer RETURN .

lemma plain_RETURN[refine_transfer]: "RETURN a ≤ RETURN a" by simp
lemma plain_bind[refine_transfer]: 
  "⟦RETURN x ≤ M; ⋀x. RETURN (f x) ≤ F x⟧ ⟹ RETURN (Let x f) ≤ bind M F"
  apply (erule order_trans[rotated,OF bind_mono(1)])
  apply assumption
  apply simp
  done

interpretation plain_assert: transfer_generic_Assert_remove 
  bind RETURN ASSERT ASSUME
  RETURN
  by unfold_locales

(*
interpretation plain: transfer_FOREACH RETURN "(λx. x)" Let "(λx. x)"
  apply (unfold_locales)
  apply (erule plain_bind, assumption)
  apply simp
  apply simp
  done
*)

subsection ‹Total correctness in deterministic monad›
text ‹
  Sometimes one cannot extract total correct programs to executable plain 
  Isabelle functions, for example, if the total correctness only holds for
  certain preconditions. In those cases, one can still show
  ‹RETURN (the_res S) ≤ S'›. Here, ‹the_res› extracts
  the result from a deterministic monad. As ‹the_res› is executable,
  the above shows that ‹(the_res S)› is always a correct result.
›

fun the_res where "the_res (dRETURN x) = x"

text ‹The following lemma converts a proof-obligation
  with result extraction to a transfer proof obligation,
  and a proof obligation that the program yields not bottom.

  Note that this rule has to be applied manually, as, otherwise,
  it would interfere with the default setup, that tries to generate a
  plain function.
›
lemma the_resI:
  assumes "nres_of S ≤ S'"
  assumes "S ≠ dSUCCEED"
  shows "RETURN (the_res S) ≤ S'"
  using assms
  by (cases S, simp_all)


text ‹The following rule sets up a refinement goal, a transfer goal, and a 
  final optimization goal.›
definition "detTAG x ≡ x"
lemma detTAGI: "x = detTAG x" unfolding detTAG_def by simp
lemma autoref_detI:
  assumes "(b,a)∈⟨R⟩nres_rel"
  assumes "RETURN c ≤ b"
  assumes "c = detTAG d"
  shows "(RETURN d, a)∈⟨R⟩nres_rel"
  using assms
  unfolding nres_rel_def detTAG_def
  by simp


subsection ‹Relator-Based Transfer›

definition dres_nres_rel_internal_def: 
  "dres_nres_rel R ≡ {(c,a). nres_of c ≤ ⇓ R a}"

lemma dres_nres_rel_def: "⟨R⟩dres_nres_rel ≡ {(c,a). nres_of c ≤ ⇓ R a}"
  by (simp add: dres_nres_rel_internal_def relAPP_def)

lemma dres_nres_relI[intro?]: "nres_of c ≤ ⇓ R a ⟹ (c,a)∈⟨R⟩dres_nres_rel"
  by (simp add: dres_nres_rel_def)

lemma dres_nres_relD: "(c,a)∈⟨R⟩dres_nres_rel ⟹ nres_of c ≤ ⇓ R a"
  by (simp add: dres_nres_rel_def)

lemma dres_nres_rel_as_br_conv: 
  "⟨R⟩dres_nres_rel = br nres_of (λ_. True) O ⟨R⟩nres_rel"
  unfolding dres_nres_rel_def br_def nres_rel_def by auto


definition plain_nres_rel_internal_def: 
  "plain_nres_rel R ≡ {(c,a). RETURN c ≤ ⇓ R a}"

lemma plain_nres_rel_def: "⟨R⟩plain_nres_rel ≡ {(c,a). RETURN c ≤ ⇓ R a}"
  by (simp add: plain_nres_rel_internal_def relAPP_def)

lemma plain_nres_relI[intro?]: "RETURN c ≤ ⇓ R a ⟹ (c,a)∈⟨R⟩plain_nres_rel"
  by (simp add: plain_nres_rel_def)

lemma plain_nres_relD: "(c,a)∈⟨R⟩plain_nres_rel ⟹ RETURN c ≤ ⇓ R a"
  by (simp add: plain_nres_rel_def)

lemma plain_nres_rel_as_br_conv: 
  "⟨R⟩plain_nres_rel = br RETURN (λ_. True) O ⟨R⟩nres_rel"
  unfolding plain_nres_rel_def br_def nres_rel_def by auto

(* TODO: Refine_Transfer could be expressed also just as a 
    parametricity based transfer, and based on the same infrastructure
    as autoref *)

subsection ‹Post-Simplification Setup›
lemma dres_unit_simps[refine_transfer_post_simp]:
  "dbind (dRETURN (u::unit)) f = f ()"
  by auto

lemma Let_dRETURN_simp[refine_transfer_post_simp]:
  "Let m dRETURN = dRETURN m" by auto

lemmas [refine_transfer_post_simp] = dres_monad_laws


end