Theory Pf_Mono_Prover

header {* Hack: The monotonicity prover of the partial function package *}
theory Pf_Mono_Prover
imports "../Separation_Logic_Imperative_HOL/Sep_Main"
begin
  (* TODO: Make this visible in the partial_function package! *)

text ‹
  The partial function package comes with a monotonicity prover.
  However, it does not export it. This has the unfortunate effect that
  it cannot be used from external packages, e.g., the automatic refinement tool.

  This theory duplicates the monotonicity prover,
›  

ML {*
  structure Pf_Mono_Prover = struct
    structure Mono_Rules = Named_Thms
    (
      val name = @{binding partial_function_mono};
      val description = "monotonicity rules for partial function definitions";
    );
    
(*** Automated monotonicity proofs ***)

fun strip_cases ctac = ctac #> Seq.map snd;

(*rewrite conclusion with k-th assumtion*)
fun rewrite_with_asm_tac ctxt k =
  Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
    Local_Defs.unfold_tac ctxt' [nth prems k]) ctxt;

fun dest_case thy t =
  case strip_comb t of
    (Const (case_comb, _), args) =>
      (case Datatype.info_of_case thy case_comb of
         NONE => NONE
       | SOME {case_rewrites, ...} =>
           let
             val lhs = prop_of (hd case_rewrites)
               |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst;
             val arity = length (snd (strip_comb lhs));
             val conv = funpow (length args - arity) Conv.fun_conv
               (Conv.rewrs_conv (map mk_meta_eq case_rewrites));
           in
             SOME (nth args (arity - 1), conv)
           end)
  | _ => NONE;

(*split on case expressions*)
val split_cases_tac = Subgoal.FOCUS_PARAMS (fn {context=ctxt, ...} =>
  SUBGOAL (fn (t, i) => case t of
    _ $ (_ $ Abs (_, _, body)) =>
      (case dest_case (Proof_Context.theory_of ctxt) body of
         NONE => no_tac
       | SOME (arg, conv) =>
           let open Conv in
              if Term.is_open arg then no_tac
              else ((DETERM o strip_cases o Induct.cases_tac ctxt false [[SOME arg]] NONE [])
                THEN_ALL_NEW (rewrite_with_asm_tac ctxt 0)
                THEN_ALL_NEW etac @{thm thin_rl}
                THEN_ALL_NEW (CONVERSION
                  (params_conv ~1 (fn ctxt' =>
                    arg_conv (arg_conv (abs_conv (K conv) ctxt'))) ctxt))) i
           end)
  | _ => no_tac) 1);

(*monotonicity proof: apply rules + split case expressions*)
fun mono_tac ctxt =
  K (Local_Defs.unfold_tac ctxt [@{thm curry_def}])
  THEN' (TRY o REPEAT_ALL_NEW
   (resolve_tac (Mono_Rules.get ctxt)
     ORELSE' split_cases_tac ctxt));

  end
  *}


setup {* Pf_Mono_Prover.Mono_Rules.setup *}
declare Partial_Function.partial_function_mono[partial_function_mono]

end