Theory Refine_Monadic.Refine_Pfun

section ‹Partial Function Package Setup›
theory Refine_Pfun
imports Refine_Basic Refine_Det
begin

text ‹
  In this theory, we set up the partial function package to be used 
  with our refinement framework.
›

subsection ‹Nondeterministic Result Monad›

interpretation nrec:
  partial_function_definitions "(≤)" "Sup::'a nres set  'a nres"
  by unfold_locales (auto simp add: Sup_upper Sup_least)

lemma nrec_admissible: "nrec.admissible (λ(f::'a  'b nres).
  (x0. f x0  SPEC (P x0)))"
  apply (rule ccpo.admissibleI)
  apply (unfold fun_lub_def)
  apply (intro allI impI)
  apply (rule Sup_least)
  apply auto
  done

(*thm fixp_induct_option

lemma fixp_induct_nrec:
  fixes F :: "'c ⇒ 'c" and
    U :: "'c ⇒ 'b ⇒ 'a nres" and
    C :: "('b ⇒ 'a nres) ⇒ 'c" and
    P :: "'b ⇒ 'a ⇒ bool"
  assumes mono: "⋀x. nrec.mono_body (λf. U (F (C f)) x)"                       
  assumes eq: "f ≡ C (nrec.fixp_fun (λf. U (F (C f))))"
  assumes inverse2: "⋀f. U (C f) = f"
  assumes step: "⋀f x z. (⋀x. U f x = U f x; Q x z) ⟹ Q (U (F (C f))) z"
 (* assumes defined: "RETURN y ≤ U (C f) x"*)
  assumes Q: "⋀x z. Q x z ⟷ z = U f x ∧ U f x ≤ SPEC (P x)"
  shows "Q x z" oops
  (*using step defined
    nrec.fixp_induct_uc[of U F C, OF mono eq inverse2 nrec_admissible]
  unfolding Q oops (*
  by blast*)*)

lemma fixp_induct_nrec':
  fixes F :: "'c ⇒ 'c" and
    U :: "'c ⇒ 'b ⇒ 'a nres" and
    C :: "('b ⇒ 'a nres) ⇒ 'c" and
    P :: "'b ⇒ 'a ⇒ bool"
  assumes mono: "⋀x. nrec_mono (λf. U (F (C f)) x)"
  assumes eq: "f ≡ C (nrec_ffix (λf. U (F (C f))))"
  assumes inverse2: "⋀f. U (C f) = f"
  assumes step: "⋀f x0. (⋀x0. U f x0 ≤ SPEC (P x0)) 
    ⟹ U (F f) x0 ≤ SPEC (P x0)"
  assumes defined: "RETURN y ≤ U f x"
  shows "P x y"
proof -
  note defined
  also have "∀x0. U f x0 ≤ SPEC (P x0)"
    apply (rule nrec.fixp_induct_uc[of U F C, OF mono eq inverse2 
      nrec_admissible])
    using step by blast
  hence "U f x ≤ SPEC (P x)" by simp
  finally show "P x y" by auto
qed
*)    
(* TODO/FIXME: Induction rule seems not to work here ! 
    Function package expects induction rule where conclusion is a binary 
    predicate as free variable.
*)

declaration Partial_Function.init "nrec" @{term nrec.fixp_fun}
  @{term nrec.mono_body} @{thm nrec.fixp_rule_uc} @{thm nrec.fixp_induct_uc}
  (*SOME @{thm fixp_induct_nrec}*) (NONE)

lemma bind_mono_pfun[partial_function_mono]:
  fixes C :: "'a  ('b  'c nres)  ('d nres)"
  shows
  " monotone (fun_ord (≤)) (≤) B; 
    y. monotone (fun_ord (≤)) (≤) (λf. C y f)   
     monotone (fun_ord (≤)) (≤) (λf. bind (B f) (λy. C y f))"
  apply rule
  apply (rule Refine_Basic.bind_mono)
  apply (blast dest: monotoneD)+
  done


subsection ‹Deterministic Result Monad›

interpretation drec:
  partial_function_definitions "(≤)" "Sup::'a dres set  'a dres"
  by unfold_locales (auto simp add: Sup_upper Sup_least)

lemma drec_admissible: "drec.admissible (λ(f::'a  'b dres).
  (x. P x  
    (f x  dFAIL  
    (r. f x = dRETURN r  Q x r))))"
proof -
  have [simp]: "fun_ord ((≤) ::'b dres  _  _) = (≤)"
    apply (intro ext)
    unfolding fun_ord_def le_fun_def
    by (rule refl)

  have [simp]: "A x. {y. fA. y = f x} = (λf. f x)`A" by auto

  show ?thesis
    apply (rule ccpo.admissibleI)
    apply (unfold fun_lub_def)
    apply clarsimp
    apply (drule_tac x=x in point_chainI)
    apply (erule dres_Sup_chain_cases)
    apply auto
    apply (metis (poly_guards_query) SUP_bot_conv(1))
    apply (metis (poly_guards_query) SUP_bot_conv(1))
    apply metis
    done
qed

declaration Partial_Function.init "drec" @{term drec.fixp_fun}
  @{term drec.mono_body} @{thm drec.fixp_rule_uc} @{thm drec.fixp_induct_uc} 
  NONE

lemma drec_bind_mono_pfun[partial_function_mono]:
  fixes C :: "'a  ('b  'c dres)  ('d dres)"
  shows
  " monotone (fun_ord (≤)) (≤) B; 
    y. monotone (fun_ord (≤)) (≤) (λf. C y f)   
     monotone (fun_ord (≤)) (≤) (λf. dbind (B f) (λy. C y f))"
  apply rule
  apply (rule dbind_mono)
  apply (blast dest: monotoneD)+
  done

end