Theory Partial_Function_Command

section ‹ Partial Function Command ›

theory Partial_Function_Command
  imports Function_Toolkit
  keywords "zfun" :: "thy_decl_block" and "precondition" "postcondition"
begin

definition pfun_spec :: "('a ⇒ bool) ⇒ ('a ⇒ 'b ⇒ bool) ⇒ 'a ⇸ 'b" where
"pfun_spec P Q = (λ x | P x ∧ (∃ y. Q x y) ∙ SOME y. Q x y)"

lemma pfun_spec_app_eqI [intro]: "⟦ P x; ⋀ y. Q x y ⟷ y = f x ⟧ ⟹ (pfun_spec P Q)(x)⇩p = f x"
  by (simp add: pfun_spec_def, subst pabs_apply, auto)

ML_file ‹Partial_Function_Command.ML›

ML ‹
val _ =
  Outer_Syntax.command @{command_keyword zfun} "define Z-like partial functions" 
    (Zfun_Command.zfun_parser >> (Toplevel.theory o Zfun_Command.compile_zfun));
›

end