```section ‹Refinement Framework›
imports
Refine_Chapter
Refine_Basic
Refine_Leof
Refine_Heuristics
Refine_More_Comb
Refine_While
Refine_Foreach
Refine_Transfer
Refine_Pfun
Refine_Automation
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›

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
```