Theory 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); r←body 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 ("while⇩T")
    notation WHILEI ("while⇗_⇖")
    notation WHILET ("while⇩T")
    notation WHILEIT ("while⇩T⇗_⇖")

    notation RECT (binder "rec⇩T " 10)
    notation REC (binder "rec " 10)

    notation SELECT (binder "select " 10)
      
  end
    
end