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