Theory Refine_Imperative_HOL.Sepref_Improper

section ‹Ad-Hoc Solutions›
theory Sepref_Improper
imports
  Sepref_Tool
  Sepref_HOL_Bindings
  (*Sepref_IICF_Bindings*)
  Sepref_Foreach
  Sepref_Intf_Util
begin
  text ‹This theory provides some ad-hoc solutions to practical problems, 
    that, however, still need a more robust/clean solution›

  subsection ‹Pure Higher-Order Functions›
  text ‹Ad-Hoc way to support pure higher-order arguments›
  
  (* TODO: Cleaner way for pure higher-order functions! 
    Alternative: Work in context with fixed tgt
  *)
  definition pho_apply :: "('a ⇒ 'b) ⇒ 'a ⇒ 'b" where [code_unfold,simp]: "pho_apply f x = f x"
  sepref_register pho_apply
  
  lemmas fold_pho_apply = pho_apply_def[symmetric]

  lemma pure_fun_refine[sepref_fr_rules]: "hn_refine 
    (hn_val (A→B) f fi * hn_val A x xi) 
    (return (pho_apply$fi$xi)) 
    (hn_val (A→B) f fi * hn_val A x xi)
    (pure B)
    (RETURN$(pho_apply$f$x))"
    by (sep_auto intro!: hn_refineI simp: pure_def hn_ctxt_def dest: fun_relD)







end