```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 (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
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)
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)
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}"

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

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

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}"

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

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

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