Theory Refine_Monadic.Refine_Mono_Prover

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