```theory Refine_Mono_Prover
imports Main Automatic_Refinement.Refine_Lib
begin
ML_file ‹refine_mono_prover.ML›

setup Refine_Mono_Prover.setup
declaration Refine_Mono_Prover.decl_setup

method_setup refine_mono =
‹Scan.succeed (fn ctxt => SIMPLE_METHOD' (
Refine_Mono_Prover.untriggered_mono_tac ctxt
))›
"Refinement framework: Monotonicity prover"

locale mono_setup_loc =
― ‹Locale to set up monotonicity prover for given ordering operator›
fixes le :: "'a ⇒ 'a ⇒ bool"
assumes refl: "le x x"
begin
lemma monoI: "(⋀f g x. (⋀x. le (f x) (g x)) ⟹ le (B f x) (B g x))
⟹ monotone (fun_ord le) (fun_ord le) B"
unfolding monotone_def fun_ord_def by blast

lemma mono_if: "⟦le t t'; le e e'⟧ ⟹ le (If b t e) (If b t' e')" by auto
lemma mono_let: "(⋀x. le (f x) (f' x)) ⟹ le (Let x f) (Let x f')" by auto

lemmas mono_thms[refine_mono] = monoI mono_if mono_let refl

declaration ‹Refine_Mono_Prover.declare_mono_triggers @{thms monoI}›

end

interpretation order_mono_setup: mono_setup_loc "(≤) :: 'a::preorder ⇒ _"
by standard auto

declaration ‹Refine_Mono_Prover.declare_mono_triggers @{thms monoI}›

lemmas [refine_mono] =
lfp_mono[OF le_funI, THEN le_funD]
gfp_mono[OF le_funI, THEN le_funD]

end

```