Theory Refine_Pfun

header {* \isaheader{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 "op ≤" "Sup::'a nres set => 'a nres"
  by unfold_locales (auto simp add: Sup_upper Sup_least)
print_theorems

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" sorry
  (*using step defined
    nrec.fixp_induct_uc[of U F C, OF mono eq inverse2 nrec_admissible]
  unfolding Q sorry (*
  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 op ≤) op ≤ B; 
    !!y. monotone (fun_ord op ≤) op ≤ (λf. C y f) |] ==> 
     monotone (fun_ord op ≤) op ≤ (λ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 "op ≤" "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 (op ≤::'b dres => _ => _) = op ≤"
    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 (simp only: SUP_def)
    apply simp
    apply (simp only: SUP_def)
    apply auto []
    apply (simp only: SUP_def)
    apply force
    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 op ≤) op ≤ B; 
    !!y. monotone (fun_ord op ≤) op ≤ (λf. C y f) |] ==> 
     monotone (fun_ord op ≤) op ≤ (λf. dbind (B f) (λy. C y f))"
  apply rule
  apply (rule dbind_mono)
  apply (blast dest: monotoneD)+
  done

end