File ‹tactic_util.ML›

(*  Title:      ML_Utils/tactic_util.ML
    Author:     Kevin Kappelmann

Tactic utilities.
*)
signature TACTIC_UTIL =
sig
  include HAS_LOGGER
  (* tactic combinators *)
  val HEADGOAL : (int -> 'a) -> 'a

  val THEN : ('a -> 'b Seq.seq) * ('b -> 'c Seq.seq) -> 'a -> 'c Seq.seq
  val THEN' : ('a -> 'b -> 'c Seq.seq) * ('a -> 'c -> 'd Seq.seq) -> 'a -> 'b -> 'd Seq.seq

  val APPEND : ('a -> 'b Seq.seq) * ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq
  val APPEND' : ('a -> 'b -> 'c Seq.seq) * ('a -> 'b -> 'c Seq.seq) -> 'a -> 'b -> 'c Seq.seq

  val ORELSE : ('a -> 'b Seq.seq) * ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq
  val ORELSE' : ('a -> 'b -> 'c Seq.seq) * ('a -> 'b -> 'c Seq.seq) -> 'a -> 'b -> 'c Seq.seq

  val TRY : ('a -> 'a Seq.seq) -> 'a -> 'a Seq.seq
  val TRY' : ('a -> 'b -> 'b Seq.seq) -> 'a -> 'b -> 'b Seq.seq

  val FIRST : ('a -> 'b Seq.seq) list -> 'a -> 'b Seq.seq
  val FIRST' : ('a -> 'b -> 'c Seq.seq) list -> 'a -> 'b -> 'c Seq.seq

  val EVERY_ARG : ('a -> tactic) -> 'a list -> tactic
  val EVERY_ARG' : ('a -> 'b -> tactic) -> 'a list -> 'b -> tactic
  val CONCAT : ('a -> 'b Seq.seq) list -> 'a -> 'b Seq.seq
  val CONCAT' : ('a -> 'b -> 'c Seq.seq) list -> 'a -> 'b -> 'c Seq.seq

  (* like RANGE but applies tactics in increasing subgoal order *)
  val RANGE_UP : (int -> tactic) list -> int -> tactic

  (*filters duplicate results*)
  val unique_thmsq : (thm * thm -> bool) -> thm Seq.seq -> thm Seq.seq
  val UNIQUE : (thm * thm -> bool) -> tactic -> tactic
  val UNIQUE' : (thm * thm -> bool) -> ('a -> tactic) -> 'a -> tactic

  val FOCUS_PARAMS' : (Subgoal.focus -> int -> tactic) -> Proof.context -> int -> tactic
  val FOCUS_PARAMS_CTXT : (Proof.context -> tactic) -> Proof.context -> int -> tactic
  val FOCUS_PARAMS_CTXT' : (Proof.context -> int -> tactic) -> Proof.context -> int -> tactic
  val FOCUS_PARAMS_FIXED' : (Subgoal.focus -> int -> tactic) -> Proof.context -> int -> tactic
  val FOCUS_PREMS' : (Subgoal.focus -> int -> tactic) -> Proof.context -> int -> tactic
  val FOCUS' : (Subgoal.focus -> int -> tactic) -> Proof.context -> int -> tactic
  val SUBPROOF' : (Subgoal.focus -> int -> tactic) -> Proof.context -> int -> tactic

  val CSUBGOAL : (cterm -> int -> thm -> 'a Seq.seq) -> int -> thm -> 'a  Seq.seq
  val SUBGOAL : (term -> int -> thm -> 'a Seq.seq) -> int -> thm -> 'a  Seq.seq
  val CSUBGOAL_DATA : (cterm -> 'a) -> ('a -> int -> thm -> 'b Seq.seq) -> int -> thm -> 'b Seq.seq
  val CSUBGOAL_STRIPPED : (cterm Binders.binders * (cterm list * cterm) -> 'a) ->
    ('a -> int -> thm -> 'b Seq.seq) -> int -> thm -> 'b Seq.seq
  val SUBGOAL_DATA : (term -> 'a) -> ('a -> int -> thm -> 'b Seq.seq) -> int -> thm -> 'b Seq.seq
  val SUBGOAL_STRIPPED : (Term_Util.subgoal -> 'a) -> ('a -> int -> thm -> 'b Seq.seq) ->
    int -> thm -> 'b Seq.seq

  (* tactics *)
  val insert_tac : thm list -> Proof.context -> int -> tactic
  (*thin_tac n i deletes nth premise of the ith subgoal*)
  val thin_tac : int -> int -> tactic
  val thin_tacs : int list -> int -> tactic

  val set_kernel_ho_unif_bound : int -> Proof.context -> Proof.context
  val silence_kernel_ho_bound_exceeded : Proof.context -> Proof.context
  val FLEX_PAIRS_UNCHANGED : tactic -> tactic

  (*nth_eq_assume_tac n i solves ith subgoal by assumption, without unification,
    preferring premise n*)
  val nth_eq_assume_tac : int -> int -> tactic

  (*resolution without lifting of premises and parameters*)
  val no_lift_biresolve_tac : bool -> thm -> int -> Proof.context -> int -> tactic
  val no_lift_resolve_tac : thm -> int -> Proof.context -> int -> tactic
  val no_lift_eresolve_tac : thm -> int -> Proof.context -> int -> tactic

  (*rewrite subgoal according to the given equality theorem "lhs ≡ subgoal"*)
  val rewrite_subgoal_tac : thm -> int -> tactic

  (*protect premises starting from (and excluding) the given index in the specified subgoal*)
  val protect_tac : int -> Proof.context -> int -> tactic
  (*unprotect the subgoal*)
  val unprotect_tac : Proof.context -> int -> tactic
  (*protect, then apply tactic, then unprotect*)
  val protected_tac : int -> (int -> tactic) -> Proof.context -> int -> tactic

  (*focus on the specified subgoal, introducing only the specified list of premises
    as theorems in the focus*)
  val focus_prems_tac : int list -> (Subgoal.focus -> int -> tactic) ->
    Proof.context -> int -> tactic
  (*focus_prems_tac and then deletes all focused premises*)
  val focus_delete_prems_tac : int list -> (Subgoal.focus -> int -> tactic) ->
    Proof.context -> int -> tactic

  (*apply tactic to the specified subgoal, where the state is given as a cterm*)
  val apply_tac : (int -> tactic) -> int -> cterm -> thm Seq.seq

end

structure Tactic_Util : TACTIC_UTIL =
struct

val logger = Logger.setup_new_logger Logger.root "Tactic_Util"

(* tactic combinators *)
fun HEADGOAL f = f 1

fun (tac1 THEN tac2) = Seq.THEN (tac1, tac2)
fun (tac1 THEN' tac2) x = tac1 x THEN tac2 x

(* note: this ORELSE is lazy while the default ORELSE in tactical.ML is not! *)
fun (tac1 ORELSE tac2) st = Seq.make (fn _ => case Seq.pull (tac1 st) of
    NONE => Seq.pull (tac2 st)
  | some => some)
fun (tac1 ORELSE' tac2) x = tac1 x ORELSE tac2 x

fun TRY tac = tac ORELSE Seq.succeed
fun TRY' tac = tac ORELSE' K Seq.succeed

fun FIRST tacs = fold_rev (curry (op ORELSE)) tacs Seq.fail
fun FIRST' tacs = fold_rev (curry (op ORELSE')) tacs (K Seq.fail)

fun EVERY_ARG tac = EVERY o map tac
fun EVERY_ARG' tac = EVERY' o map tac

fun (tac1 APPEND tac2) st = Seq.append (tac1 st) (Seq.make (fn _ => Seq.pull (tac2 st)))
fun (tac1 APPEND' tac2) x = tac1 x APPEND tac2 x

fun CONCAT tacs = fold_rev (curry (op APPEND)) tacs (K Seq.empty)
fun CONCAT' tacs = fold_rev (curry (op APPEND')) tacs (K (K Seq.empty))

fun RANGE_UP [] _ = Seq.succeed
  | RANGE_UP [tac] i = tac i
  | RANGE_UP (tac :: tacs) i = fn st => (tac i
      THEN (fn st' => RANGE_UP tacs (i + Thm.nprems_of st' - Thm.nprems_of st + 1) st')) st

local structure TI = Net
in
fun unique_thmsq eq_thm thmsq =
  let fun go ti = Seq.pull #> Option.mapPartial (fn (thm, thmsq) =>
    let val key = Thm.full_prop_of thm
      |> Same.commit Term_Normalisation.beta_eta_short |> TI.key_of_term
    in
      TI.insert eq_thm (key, thm) ti |> (fn ti => SOME (thm, Seq.make (fn _ => go ti thmsq)))
      handle TI.INSERT => go ti thmsq
    end)
  in Seq.make (fn _ => go TI.empty thmsq) end
fun UNIQUE eq_thm tac = unique_thmsq eq_thm o tac
fun UNIQUE' eq_thm tac = UNIQUE eq_thm o tac
end

fun FOCUS_PARAMS' tac = Subgoal.FOCUS_PARAMS (HEADGOAL o tac)
fun FOCUS_PARAMS_FIXED' tac = Subgoal.FOCUS_PARAMS_FIXED (HEADGOAL o tac)
fun FOCUS_PREMS' tac = Subgoal.FOCUS_PREMS (HEADGOAL o tac)
fun FOCUS' tac = Subgoal.FOCUS (HEADGOAL o tac)
fun SUBPROOF' tac = Subgoal.SUBPROOF (HEADGOAL o tac)

fun FOCUS_PARAMS_CTXT tac = Subgoal.FOCUS_PARAMS (#context #> tac)
fun FOCUS_PARAMS_CTXT' tac = FOCUS_PARAMS' (#context #> tac)

fun CSUBGOAL goalfun i st = case SOME (Thm.cprem_of st i) handle THM _ => NONE of
    SOME goal => goalfun goal i st
  | NONE => Seq.empty
fun SUBGOAL goalfun = CSUBGOAL (Thm.term_of #> goalfun)

fun CSUBGOAL_DATA f tac = CSUBGOAL (tac o f)
fun CSUBGOAL_STRIPPED f = CSUBGOAL_DATA (f o Term_Util.strip_csubgoal)
fun SUBGOAL_DATA f tac = SUBGOAL (tac o f)
fun SUBGOAL_STRIPPED f = SUBGOAL_DATA (f o Term_Util.strip_subgoal)

(* tactics *)
fun insert_tac thms ctxt = Method.insert_tac ctxt thms

fun thin_tac n = if n < 1 then K no_tac
  else rotate_tac (n - 1) THEN' (DETERM o eresolve0_tac [thin_rl]) THEN' rotate_tac (~n + 1)
val thin_tacs = sort int_ord
  #> map_index ((op -) o swap)
  #> EVERY_ARG' thin_tac

val set_kernel_ho_unif_bound = Config.put Unify.search_bound
val silence_kernel_ho_bound_exceeded = Context_Position.set_visible false

fun FLEX_PAIRS_UNCHANGED tac state =
  let val eq_flexps = Thm.tpairs_of #> pair (Thm.tpairs_of state)
    #> eq_list (eq_pair (op aconv) (op aconv))
  in tac state |> Seq.filter eq_flexps end

fun nth_eq_assume_tac n = if n < 1 then K no_tac
  else rotate_tac (n - 1) THEN' eq_assume_tac

(*resolution*)
fun no_lift_biresolve_tac eres brule nsubgoals ctxt =
  Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true}
  (eres, brule, nsubgoals)
  #> PRIMSEQ

val no_lift_resolve_tac = no_lift_biresolve_tac false
val no_lift_eresolve_tac = no_lift_biresolve_tac true

fun rewrite_subgoal_tac eq_thm = CONVERSION (K (Thm.symmetric eq_thm))

fun protect_tac n ctxt =
  let fun protect cbinders (cprems, cconcl) i =
    let val nprems = length cprems
    in
      if nprems < n then
        (@{log Logger.WARN} ctxt (fn _ => Pretty.block [
          Pretty.str "Not enough premises to protect. Given number: ",
          Pretty.str (string_of_int n),
          Pretty.str ". But there are only ",
          Pretty.str (string_of_int nprems),
          Pretty.str " premise(s) in subgoal ",
          Pretty.str (string_of_int i),
          Pretty.str ": ",
          Logic.close_prop (map (apfst fst o apsnd Thm.term_of) cbinders) (map Thm.term_of cprems)
            (Thm.term_of cconcl) |> Syntax.pretty_term ctxt
        ] |> Pretty.string_of);
        no_tac)
      else
        let
          val (cprems_unprotected, cconcl_protected) = chop n cprems
            ||> Drule.list_implies o rpair cconcl
        in
          @{thm Pure.prop_def}
          |> Thm.instantiate' [] [SOME cconcl_protected]
          |> Thm_Util.eq_subgoal_from_eq_concl cbinders cprems_unprotected ctxt
          |> Option.map (fn protected_eq_thm => rewrite_subgoal_tac protected_eq_thm i)
          |> the_default no_tac
        end
    end
  in if n < 0 then K no_tac else CSUBGOAL_STRIPPED I (uncurry protect) end

fun unprotect_tac ctxt = match_tac ctxt [Drule.protectI]

fun protected_tac n tac ctxt =
  protect_tac n ctxt
  THEN' tac
  THEN_ALL_NEW (unprotect_tac ctxt)

fun focus_prems_tac is tac ctxt =
  CONVERSION (Conversion_Util.move_prems_to_front_conv is)
  THEN' protect_tac (length is) ctxt
  THEN' FOCUS_PREMS' (fn {context=ctxt, params=params, prems=prems,
    asms=asms, schematics=schematics, concl=concl} => unprotect_tac ctxt
      THEN' tac {context=ctxt, params=params, prems=prems, asms=asms, schematics=schematics,
        concl=Term_Util.unprotect concl}
  ) ctxt

fun focus_delete_prems_tac is tac ctxt =
  focus_prems_tac is tac ctxt
  THEN' thin_tacs (1 upto length is)

fun apply_tac tac i = Seq.single #> Seq.map Goal.init #> Seq.maps (tac i) #> Seq.map Goal.conclude

end