Theory Refine_Monadic.Refine_Monadic

section ‹Refinement Framework›
theory Refine_Monadic
imports 
  Refine_Chapter
  Refine_Basic 
  Refine_Leof
  Refine_Heuristics 
  Refine_More_Comb
  Refine_While 
  Refine_Foreach 
  Refine_Transfer
  Refine_Pfun
  Refine_Automation
  Autoref_Monadic
begin
  text ‹
    This theory summarizes all default theories of the refinement framework.
›

  subsection ‹Convenience Constructs›

  definition "REC_annot pre post body x  
    REC (λD x. do {ASSERT (pre x); rbody D x; ASSERT (post x r); RETURN r}) x"
  
  theorem REC_annot_rule[refine_vcg]:
    assumes M: "trimono body"
    and P: "pre x"
    and S: "f x. x. pre x  f x  SPEC (post x); pre x 
             body f x  SPEC (post x)"
    and C: "r. post x r  Φ r"
    shows "REC_annot pre post body x  SPEC Φ"
  proof -
    from trimono body have [refine_mono]:
      "f g x xa. (x. flat_ge (f x) (g x))  flat_ge (body f x) (body g x)"
      "f g x xa. (x. f x  g x)  body f x  body g x"
      apply -
      unfolding trimono_def monotone_def fun_ord_def mono_def le_fun_def
      apply (auto)
      done
  
    show ?thesis
      unfolding REC_annot_def
      apply (rule order_trans[where y="SPEC (post x)"])
      apply (refine_rcg 
        refine_vcg 
        REC_rule[where pre=pre and M="λx. SPEC (post x)"]
        order_trans[OF S]
      )
      apply fact
      apply simp
      using C apply (auto) []
      done
  qed
  
  subsection ‹Syntax Sugar›
  locale Refine_Monadic_Syntax begin
  
    notation SPEC (binder "spec " 10)
    notation ASSERT ("assert")
    notation RETURN ("return")
    notation FOREACH ("foreach")
    notation WHILE ("while")
    notation WHILET ("whileT")
    notation WHILEI ("while⇗_")
    notation WHILET ("whileT")
    notation WHILEIT ("whileT_")

    notation RECT (binder "recT " 10)
    notation REC (binder "rec " 10)

    notation SELECT (binder "select " 10)
      
  end
    
end