Theory 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. ∃f∈A. 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