Quelle  util.ML

(*
  File: util.ML
  Author: Bohua Zhan

  Utility functions.
*)

signature BASIC_UTIL =
sig
  (* Exceptions *)
  val assert: bool -> string -> unit

  (* Types *)
  val propT: typ

  (* Lists *)
  val the_pair: 'a list -> 'a * 'a
  val the_triple: 'a list -> 'a * 'a * 'a
  val filter_split: ('a -> bool) -> 'a list -> 'a list * 'a list

  (* Managing matching environments. *)
  val fo_init: Type.tyenv * Envir.tenv
  val lookup_instn: Type.tyenv * Envir.tenv -> string * int -> term
  val lookup_inst: Type.tyenv * Envir.tenv -> string -> term

  (* Tracing functions. *)
  val trace_t: Proof.context -> string -> term -> unit
  val trace_tlist: Proof.context -> string -> term list -> unit
  val trace_thm: Proof.context -> string -> thm -> unit
  val trace_fullthm: Proof.context -> string -> thm -> unit
  val trace_thm_global: string -> thm -> unit
  val trace_fullthm_global: string -> thm -> unit

  (* Terms *)
  val dest_arg: term -> term
  val dest_arg1: term -> term

  (* Theorems *)
  val apply_to_thm: conv -> thm -> thm
  val meta_sym: thm -> thm
  val apply_to_lhs: conv -> thm -> thm
  val apply_to_rhs: conv -> thm -> thm
end;

signature UTIL =
sig
  include BASIC_UTIL

  (* Lists *)
  val max: ('a * 'a -> order) -> 'a list -> 'a
  val max_partial: ('a -> 'a -> bool) -> 'a list -> 'a list
  val subsets: 'a list -> 'a list list
  val all_permutes: 'a list -> 'a list list
  val all_pairs: 'a list * 'b list -> ('a * 'b) list
  val remove_dup_lists: ('a * 'a -> order) -> 'a list * 'a list -> 'a list * 'a list
  val is_subseq: ('a * 'a -> bool) -> 'a list * 'a list -> bool

  (* Strings. *)
  val is_prefix_str: string -> string -> bool
  val is_just_internal: string -> bool

  (* Managing matching environments. *)
  val defined_instn: Type.tyenv * Envir.tenv -> string * int -> bool
  val lookup_tyinst: Type.tyenv * Envir.tenv -> string -> typ
  val update_env: indexname * term -> Type.tyenv * Envir.tenv ->
                  Type.tyenv * Envir.tenv
  val eq_env: (Type.tyenv * Envir.tenv) * (Type.tyenv * Envir.tenv) -> bool

  (* Matching. *)
  val first_order_match_list:
      theory -> (term * term) list -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv

  (* Printing functions, mostly from Isabelle Cookbook. *)
  val string_of_terms: Proof.context -> term list -> string
  val string_of_terms_global: theory -> term list -> string
  val string_of_tyenv: Proof.context -> Type.tyenv -> string
  val string_of_env: Proof.context -> Envir.tenv -> string
  val string_of_list: ('a -> string) -> 'a list -> string
  val string_of_list': ('a -> string) -> 'a list -> string
  val string_of_bool: bool -> string

  (* Managing context. *)
  val declare_free_term: term -> Proof.context -> Proof.context

  (* Terms. *)
  val is_abs: term -> bool
  val is_implies: term -> bool
  val dest_binop: term -> term * (term * term)
  val dest_binop_head: term -> term
  val dest_binop_args: term -> term * term
  val dest_args: term -> term list
  val dest_argn: int -> term -> term
  val get_head_name: term -> string
  val is_meta_eq: term -> bool
  val occurs_frees: term list -> term -> bool
  val occurs_free: term -> term -> bool
  val has_vars: term -> bool
  val is_subterm: term -> term -> bool
  val has_subterm: term list -> term -> bool
  val is_head: term -> term -> bool
  val lambda_abstract: term -> term -> term
  val is_pattern_list: term list -> bool
  val is_pattern: term -> bool

  val normalize_meta_all_imp: Proof.context -> conv
  val swap_meta_imp_alls: Proof.context -> conv
  val normalize_meta_horn: Proof.context -> conv
  val strip_meta_horn: term -> term list * (term list * term)
  val list_meta_horn: term list * (term list * term) -> term
  val to_internal_vars: Proof.context -> term list * term -> term list * term
  val rename_abs_term: term list -> term -> term
  val print_term_detail: Proof.context -> term -> string

  (* cterms. *)
  val dest_cargs: cterm -> cterm list
  val dest_binop_cargs: cterm -> cterm * cterm

  (* Theorems. *)
  val arg_backn_conv: int -> conv -> conv
  val argn_conv: int -> conv -> conv
  val comb_equiv: cterm * thm list -> thm
  val name_of_thm: thm -> string
  val update_name_of_thm: thm -> string -> thm -> thm
  val lhs_of: thm -> term
  val rhs_of: thm -> term
  val assume_meta_eq: theory -> term * term -> thm
  val assume_thm: Proof.context -> term -> thm
  val subst_thm_thy: theory -> Type.tyenv * Envir.tenv -> thm -> thm
  val subst_thm: Proof.context -> Type.tyenv * Envir.tenv -> thm -> thm
  val send_first_to_hyps: thm -> thm
  val send_all_to_hyps: thm -> thm
  val subst_thm_atomic: (cterm * cterm) list -> thm -> thm
  val subst_term_norm: Type.tyenv * Envir.tenv -> term -> term
  val concl_conv_n: int -> conv -> conv
  val concl_conv: conv -> conv
  val transitive_list: thm list -> thm
  val skip_n_conv: int -> conv -> conv
  val pattern_rewr_conv: term -> (term * thm) list -> conv
  val eq_cong_th: int -> term -> term -> Proof.context -> thm
  val forall_elim_sch: thm -> thm

  (* Conversions *)
  val reverse_eta_conv: Proof.context -> conv
  val repeat_n_conv: int -> conv -> conv

  (* Miscellaneous. *)
  val test_conv: Proof.context -> conv -> string -> string * string -> unit
  val term_pat_setup: theory -> theory
  val cterm_pat_setup: theory -> theory
  val type_pat_setup: theory -> theory
  val timer: string * (unit -> 'a) -> 'a
end;

structure Util : UTIL =
struct

fun assert b exn_str = if b then () else raise Fail exn_str

val propT = @{typ prop}

fun max comp lst =
    let
      fun max2 t1 t2 = if comp (t1, t2) = LESS then t2 else t1
    in
      case lst of
          [] => raise Fail "max: empty list"
        | l :: ls => fold max2 ls l
    end

(* Given a function comp, remove y for each pair (x, y) such that comp
   x y = true (if x dominates y).
 *)
fun max_partial comp lst =
    let
      fun helper taken remains =
          case remains of
              [] => taken
            | x :: xs =>
              if exists (fn y => comp y x) taken then
                helper taken xs
              else
                helper (x :: filter_out (fn y => comp x y) taken) xs
    in
      helper [] lst
    end

(* Return all subsets of lst. *)
fun subsets [] = [[]]
  | subsets (l::ls) =
    let val prev = subsets ls in prev @ map (cons l) prev end

(* List of all permutations of xs *)
fun all_permutes xs =
    case xs of
        [] => [[]]
      | [x] => [[x]]
      | [x, y] => [[x, y], [y, x]]
      | _ =>
        maps (fn i => map (cons (nth xs i)) (all_permutes (nth_drop i xs)))
             (0 upto (length xs - 1))

(* Convert list to pair. List must consist of exactly two items. *)
fun the_pair lst =
    case lst of [i1, i2] => (i1, i2)
              | _ => raise Fail "the_pair"

(* Convert list to triple. List must consist of exactly three items. *)
fun the_triple lst =
    case lst of [i1, i2, i3] => (i1, i2, i3)
              | _ => raise Fail "the_triple"

(* Split list into (ins, outs), where ins satisfy f, and outs don't. *)
fun filter_split _ [] = ([], [])
  | filter_split f (x :: xs) =
    let
      val (ins, outs) = filter_split f xs
    in
      if f x then (x :: ins, outs) else (ins, x :: outs)
    end

(* Form the Cartesian product of two lists. *)
fun all_pairs (l1, l2) =
    maps (fn y => (map (fn x => (x, y)) l1)) l2

(* Given two sorted lists, remove all pairs of terms that appear in
   both lists, counting multiplicity.
 *)
fun remove_dup_lists ord (xs, ys) =
    case xs of
        [] => ([], ys)
     | x :: xs' =>
       case ys of
           [] => (xs, [])
         | y :: ys' =>
           case ord (x, y) of
               LESS => apfst (cons x) (remove_dup_lists ord (xs', ys))
             | EQUAL => remove_dup_lists ord (xs', ys')
             | GREATER => apsnd (cons y) (remove_dup_lists ord (xs, ys'))

(* Whether l1 is a subsequence of l2. *)
fun is_subseq eq (l1, l2) =
    case l1 of
        [] => true
      | x :: l1' =>
        case l2 of
            [] => false
          | y :: l2' => if eq (x, y) then is_subseq eq (l1', l2')
                        else is_subseq eq (l1, l2')

(* Whether pre is a prefix of str. *)
fun is_prefix_str pre str =
    is_prefix (op =) (String.explode pre) (String.explode str)

(* Test whether x is followed by exactly one _. *)
fun is_just_internal x =
    Name.is_internal x andalso not (Name.is_skolem x)

val fo_init = (Vartab.empty, Vartab.empty)

(* Lookup a Vartab inst with string and integer specifying indexname. *)
fun defined_instn (_, inst) (str, n) = Vartab.defined inst (str, n)
fun lookup_instn (_, inst) (str, n) =
    case Vartab.lookup inst (str, n) of
        NONE => raise Fail ("lookup_inst: not found " ^ str ^
                            (if n = 0 then "" else string_of_int n))
      | SOME (_, u) => u
fun lookup_inst (tyinst, inst) str = lookup_instn (tyinst, inst) (str, 0)
fun lookup_tyinst (tyinst, _) str =
    case Vartab.lookup tyinst (str, 0) of
        NONE => raise Fail ("lookup_tyinst: not found " ^ str)
      | SOME (_, T) => T

fun update_env (idx, t) (tyenv, tenv) =
    (tyenv, tenv |> Vartab.update_new (idx, (type_of t, t)))

(* A rough comparison, simply compare the corresponding terms. *)
fun eq_env ((_, inst1), (_, inst2)) =
    let
      val data1 = Vartab.dest inst1
      val data2 = Vartab.dest inst2
      fun compare_data (((x, i), (ty, t)), ((x', i'), (ty', t'))) =
          x = x' andalso i = i' andalso ty = ty' andalso t aconv t'
    in
      eq_set compare_data (data1, data2)
    end

fun first_order_match_list thy pairs inst =
    case pairs of
        [] => inst
      | (t, u) :: rest =>
        let
          val inst' = Pattern.first_order_match thy (t, u) inst
        in
          first_order_match_list thy rest inst'
        end

fun string_of_terms ctxt ts =
    ts |> map (Syntax.pretty_term ctxt)
       |> Pretty.commas |> Pretty.block |> Pretty.string_of
fun string_of_terms_global thy ts =
    ts |> map (Syntax.pretty_term_global thy)
       |> Pretty.commas |> Pretty.block |> Pretty.string_of

fun pretty_helper aux env =
    env |> Vartab.dest
        |> map aux
        |> map (fn (s1, s2) => Pretty.block [s1, Pretty.str " := ", s2])
        |> Pretty.enum "," "[" "]"
        |> Pretty.string_of

fun string_of_tyenv ctxt tyenv =
    let
      fun get_typs (v, (s, T)) = (TVar (v, s), T)
      val print = apply2 (Syntax.pretty_typ ctxt)
    in
      pretty_helper (print o get_typs) tyenv
    end

fun string_of_env ctxt env =
    let
      fun get_ts (v, (T, t)) = (Var (v, T), t)
      val print = apply2 (Syntax.pretty_term ctxt)
    in
      pretty_helper (print o get_ts) env
    end

fun string_of_list func lst =
    Pretty.str_list "[" "]" (map func lst) |> Pretty.string_of
fun string_of_list' func lst =
    if length lst = 1 then func (the_single lst) else string_of_list func lst
fun string_of_bool b = if b then "true" else "false"

fun trace_t ctxt s t =
    tracing (s ^ " " ^ (Syntax.string_of_term ctxt t))
fun trace_tlist ctxt s ts =
    tracing (s ^ " " ^ (string_of_terms ctxt ts))
fun trace_thm ctxt s th =
    tracing (s ^ " " ^ (th |> Thm.prop_of |> Syntax.string_of_term ctxt))
fun trace_fullthm ctxt s th =
    tracing (s ^ " [" ^ (Thm.hyps_of th |> string_of_terms ctxt) ^
             "] ==> " ^ (Thm.prop_of th |> Syntax.string_of_term ctxt))
fun trace_thm_global s th =
    let
      val thy = Thm.theory_of_thm th
    in
      tracing (s ^ " " ^ (th |> Thm.prop_of |> Syntax.string_of_term_global thy))
    end

fun trace_fullthm_global s th =
    let
      val thy = Thm.theory_of_thm th
    in
      tracing (s ^ " [" ^ (Thm.hyps_of th |> string_of_terms_global thy) ^
               "] ==> " ^ (Thm.prop_of th |> Syntax.string_of_term_global thy))
    end

fun declare_free_term t ctxt =
    if not (is_Free t) then raise Fail "declare_free_term: t not free."
    else ctxt |> Variable.add_fixes_direct [t |> Term.dest_Free |> fst]
              |> Variable.declare_term t

fun is_abs t =
    case t of Abs _ => true | _ => false

(* Whether a given term is of the form A ==> B. *)
fun is_implies t =
    let val _ = assert (fastype_of t = propT) "is_implies: wrong type"
    in case t of @{const Pure.imp} $ _ $ _ => true
               | _ => false
    end

(* Extract the last two arguments on t, collecting the rest into f. *)
fun dest_binop t =
    case t of
        f $ a $ b => (f, (a, b))
      | _ => raise Fail "dest_binop"

fun dest_binop_head t = fst (dest_binop t)
fun dest_binop_args t = snd (dest_binop t)

(* Return the argument of t. If t is f applied to multiple arguments,
   return the last argument.
 *)
fun dest_arg t =
    case t of _ $ arg => arg | _ => raise Fail "dest_arg"

(* Return the first of two arguments of t. *)
fun dest_arg1 t =
    case t of _ $ arg1 $ _ => arg1 | _ => raise Fail "dest_arg1"

(* Return the list of all arguments of t. *)
fun dest_args t = t |> Term.strip_comb |> snd

(* Return the nth argument of t, counting from left and starting at zero. *)
fun dest_argn n t = nth (dest_args t) n

(* Return the name of the head function. *)
fun get_head_name t =
    case Term.head_of t of
        Const (nm, _) => nm
      | _ => raise Fail "get_head_name"

(* Whether the term is of the form A == B. *)
fun is_meta_eq t =
    let val _ = assert (fastype_of t = propT) "is_meta_eq_term: wrong type"
    in case t of Const (@{const_name Pure.eq}, _) $ _ $ _ => true
               | _ => false
    end

(* Given free variable freevar (or a list of free variables freevars),
   determine whether any of the inputs appears in t.
 *)
fun occurs_frees freevars t =
    inter (op aconv) (map Free (Term.add_frees t [])) freevars <> []
fun occurs_free freevar t = occurs_frees [freevar] t

(* Whether the given term contains schematic variables. *)
fun has_vars t = length (Term.add_vars t []) > 0

(* Whether subt is a subterm of t. *)
fun is_subterm subt t = exists_subterm (fn t' => t' aconv subt) t

(* Whether any of subts is a subterm of t. *)
fun has_subterm subts t = exists_subterm (fn t' => member (op aconv) subts t') t

(* Whether s is a head term of t. *)
fun is_head s t =
    let
      val (sf, sargs) = Term.strip_comb s
      val (tf, targs) = Term.strip_comb t
    in
      sf aconv tf andalso is_prefix (op aconv) sargs targs
    end

(* If stmt is P(t), return %t. P(t). *)
fun lambda_abstract t stmt = Term.lambda t (Term.abstract_over (t, stmt))

(* A more general criterion for patterns. In combinations, any
   argument that is a pattern (in the more general sense) frees up
   checking for any functional schematic variables in that argument.
 *)
fun is_pattern_list ts =
    let
      fun is_funT T = case T of Type ("fun", _) => true | _ => false
      fun get_fun_vars t = (Term.add_vars t [])
                               |> filter (is_funT o snd) |> map Var

      fun test_list exclude_vars ts =
          case ts of
              [] => true
            | [t] => test_term exclude_vars t
            | t :: ts' =>
              if test_term exclude_vars t then
                test_list (merge (op aconv) (exclude_vars, get_fun_vars t)) ts'
              else if test_list exclude_vars ts' then
                test_term (distinct (op aconv)
                                    (exclude_vars @ maps get_fun_vars ts')) t
              else false

      and test_term exclude_vars t =
          case t of
              Abs (_, _, t') => test_term exclude_vars t'
            | _ => let val (head, args) = strip_comb t in
                     if is_Var head then
                       if member (op aconv) exclude_vars head then
                         test_list exclude_vars args
                       else
                         forall is_Bound args andalso
                         not (has_duplicates (op aconv) args)
                     else
                       test_list exclude_vars args
                   end
    in
      test_list [] ts
    end

fun is_pattern t = is_pattern_list [t]

(* Push !!x to the right as much as possible. *)
fun normalize_meta_all_imp_once ct =
    Conv.try_conv (
      Conv.every_conv [Conv.rewr_conv (Thm.symmetric @{thm Pure.norm_hhf_eq}),
                       Conv.arg_conv normalize_meta_all_imp_once]) ct

fun normalize_meta_all_imp ctxt ct =
    let
      val t = Thm.term_of ct
    in
      if Logic.is_all t then
        Conv.every_conv [Conv.binder_conv (normalize_meta_all_imp o snd) ctxt,
                         normalize_meta_all_imp_once] ct
      else if is_implies t then
        Conv.arg_conv (normalize_meta_all_imp ctxt) ct
      else
        Conv.all_conv ct
    end

(* Rewrite A ==> !!v_i. B to !!v_i. A ==> B. *)
fun swap_meta_imp_alls ctxt ct =
    let
      val t = Thm.term_of ct
    in
      if is_implies t andalso Logic.is_all (dest_arg t) then
        Conv.every_conv [Conv.rewr_conv @{thm Pure.norm_hhf_eq},
                         Conv.binder_conv (swap_meta_imp_alls o snd) ctxt] ct
      else
        Conv.all_conv ct
    end

(* Normalize a horn clause into standard form !!v_i. A_i ==> B. *)
fun normalize_meta_horn ctxt ct =
    let
      val t = Thm.term_of ct
    in
      if Logic.is_all t then
        Conv.binder_conv (normalize_meta_horn o snd) ctxt ct
      else if is_implies t then
        Conv.every_conv [Conv.arg_conv (normalize_meta_horn ctxt),
                         swap_meta_imp_alls ctxt] ct
      else
        Conv.all_conv ct
    end

(* Deconstruct a horn clause !!v_i. A_i ==> B into (v_i, (A_i, B)). *)
fun strip_meta_horn t =
    case t of
        Const (@{const_name Pure.all}, _) $ (u as Abs _) =>
        let
          val (v, body) = Term.dest_abs_global u
          val (vars, (assums, concl)) = strip_meta_horn body
        in
          (Free v :: vars, (assums, concl))
        end
      | @{const Pure.imp} $ P $ Q =>
        let
          val (vars, (assums, concl)) = strip_meta_horn Q
        in
          (vars, (P :: assums, concl))
        end
      | _ => ([], ([], t))

fun list_meta_horn (vars, (As, B)) =
    (Logic.list_implies (As, B)) |> fold Logic.all (rev vars)

fun to_internal_vars ctxt (vars, body) =
    let
      val vars' = vars |> map Term.dest_Free
                       |> Variable.variant_names ctxt
                       |> map (apfst Name.internal)
                       |> map Free
      val subst = vars ~~ vars'
    in
      (vars', subst_atomic subst body)
    end

fun rename_abs_term vars t =
    case vars of
        [] => t
      | var :: rest =>
        let
          val (x, _) = Term.dest_Free var
        in
          case t of A $ Abs (_, T1, body) =>
                    A $ Abs (x, T1, rename_abs_term rest body)
                  | _ => error "rename_abs_term"
        end

fun print_term_detail ctxt t =
    case t of
        Const (s, ty) => "Const (" ^ s ^ ", " ^ (Syntax.string_of_typ ctxt ty)
      | Free (s, ty) => "Free (" ^ s ^ ", " ^ (Syntax.string_of_typ ctxt ty) ^ ")"
      | Var ((x, i), ty) => "Var ((" ^ x ^ ", " ^ (string_of_int i) ^ "), " ^
                             (Syntax.string_of_typ ctxt ty) ^ ")"
      | Bound n => "Bound " ^ (string_of_int n)
      | Abs (s, ty, b) => "Abs (" ^ s ^ ", " ^ (Syntax.string_of_typ ctxt ty) ^
                          ", " ^ (print_term_detail ctxt b) ^ ")"
      | u $ v => "(" ^ print_term_detail ctxt u ^ ") $ (" ^
                 print_term_detail ctxt v ^ ")"

(* Version for ct. *)
fun dest_cargs ct = ct |> Drule.strip_comb |> snd
fun dest_binop_cargs ct = (Thm.dest_arg1 ct, Thm.dest_arg ct)

(* Apply cv to nth argument of t, counting from right and starting at 0. *)
fun arg_backn_conv n cv ct =
    if n = 0 then Conv.arg_conv cv ct
    else Conv.fun_conv (arg_backn_conv (n-1) cv) ct

(* Apply cv to nth argument of t, counting from left and starting at 0. *)
fun argn_conv n cv ct =
    let
      val args_count = ct |> Thm.term_of |> dest_args |> length
      val _ = assert (n >= 0 andalso n < args_count)
    in
      arg_backn_conv (args_count - n - 1) cv ct
    end

(* Given a head cterm f (function to be applied), and a list of
   equivalence theorems of arguments, produce an equivalent theorem
   for the overall term.
 *)
fun comb_equiv (cf, arg_equivs) =
    Library.foldl (uncurry Thm.combination) (Thm.reflexive cf, arg_equivs)

(* Retrive name of theorem. *)
fun name_of_thm th = if Thm.has_name_hint th then Thm_Name.short (Thm.get_name_hint th)
                     else raise Fail "name_of_thm: not found"

(* Set the name of th to the name of ori_th, followed by suffix. *)
fun update_name_of_thm ori_th suffix th =
    if Thm.has_name_hint ori_th then
      th |> Thm.put_name_hint (Thm_Name.short (Thm.get_name_hint ori_th) ^ suffix, 0)
    else th

val lhs_of = Thm.term_of o Thm.lhs_of
val rhs_of = Thm.term_of o Thm.rhs_of

fun assume_meta_eq thy (t1, t2) =
    Thm.assume (Thm.global_cterm_of thy (Logic.mk_equals (t1, t2)))
fun assume_thm ctxt t =
    if type_of t <> propT then
      raise Fail "assume_thm: t is not of type prop"
    else Thm.assume (Thm.cterm_of ctxt t)

(* Similar to Envir.subst_term. Apply an instantiation to a theorem. *)
fun subst_thm_thy thy (tyinsts, insts) th =
    let
      fun process_tyenv (v, (S, T)) =
          ((v, S), Thm.global_ctyp_of thy T)
      val tys = map process_tyenv (Vartab.dest tyinsts)
      fun process_tenv (v, (T, u)) =
          ((v, Envir.subst_type tyinsts T), Thm.global_cterm_of thy u)
      val ts = map process_tenv (Vartab.dest insts)
    in
      th |> Drule.instantiate_normalize (TVars.make tys, Vars.make ts)
    end

fun subst_thm ctxt (tyinsts, insts) th =
    subst_thm_thy (Proof_Context.theory_of ctxt) (tyinsts, insts) th

fun send_first_to_hyps th =
    let
      val cprem = Thm.cprem_of th 1
    in
      Thm.implies_elim th (Thm.assume cprem)
    end

fun send_all_to_hyps th =
    let
      val _ = assert (forall (not o has_vars) (Thm.prems_of th))
                     "send_all_to_hyps: schematic variables in hyps."
    in
      funpow (Thm.nprems_of th) send_first_to_hyps th
    end

(* Replace using subst the internal variables in th. This proceeds in
   several steps: first, pull any hypotheses of the theorem involving
   the replaced variables into statement of the theorem, perform the
   replacement (using forall_intr then forall_elim), finally return
   the hypotheses to their original place.
 *)
fun subst_thm_atomic subst th =
    let
      val old_cts = map fst subst
      val old_ts = map Thm.term_of old_cts
      val new_cts = map snd subst
      val chyps = filter (fn ct => has_subterm old_ts (Thm.term_of ct))
                         (Thm.chyps_of th)
    in
      th |> fold Thm.implies_intr chyps
         |> fold Thm.forall_intr old_cts
         |> fold Thm.forall_elim (rev new_cts)
         |> funpow (length chyps) send_first_to_hyps
    end

(* Substitution into terms used in auto2. Substitute types first and
   instantiate the types in the table of term instantiations. Also
   perform beta_norm at the end.
 *)
fun subst_term_norm (tyinsts, insts) t =
    let
      fun inst_tenv tenv =
          tenv |> Vartab.dest
               |> map (fn (ixn, (T, v)) =>
                          (ixn, (Envir.subst_type tyinsts T, v)))
               |> Vartab.make
    in
      t |> Envir.subst_term_types tyinsts
        |> Envir.subst_term (tyinsts, inst_tenv insts)
        |> Envir.beta_norm
    end

(* Apply the conversion cv to the statement of th, yielding the
   equivalent theorem.
 *)
fun apply_to_thm cv th =
    let val eq = cv (Thm.cprop_of th)
    in if Thm.is_reflexive eq then th else Thm.equal_elim eq th end

(* Given th of form A == B, get th' of form B == A. *)
val meta_sym = Thm.symmetric

(* Apply conv to rewrite the left hand side of th. *)
fun apply_to_lhs cv th =
    let val eq = cv (Thm.lhs_of th)
    in if Thm.is_reflexive eq then th else Thm.transitive (meta_sym eq) th end

(* Apply conv to rewrite the right hand side of th. *)
fun apply_to_rhs cv th =
    let val eq = cv (Thm.rhs_of th)
    in if Thm.is_reflexive eq then th else Thm.transitive th eq end

(* Using cv, rewrite the part of ct after stripping i premises. *)
fun concl_conv_n i cv ct =
    if i = 0 then cv ct
    else (Conv.arg_conv (concl_conv_n (i-1) cv)) ct

(* Rewrite part of ct after stripping all premises. *)
fun concl_conv cv ct =
    case Thm.term_of ct of
        @{const Pure.imp} $ _ $ _ => Conv.arg_conv (concl_conv cv) ct
      | _ => cv ct

(* Given a list of theorems A = B, B = C, etc., apply
   Thm.transitive to get equality between start and end.
 *)
fun transitive_list ths =
    let
      fun rev_transitive btoc atob =
          let
            val (b, c) = btoc |> Thm.cprop_of |> Thm.dest_equals
            val (a, b') = atob |> Thm.cprop_of |> Thm.dest_equals
          in
            if b aconvc b' then
              if a aconvc b then btoc
              else if b aconvc c then atob
              else Thm.transitive atob btoc
            else
              let
                val _ = map (trace_thm_global "ths:") ths
              in
                raise Fail "transitive_list: intermediate does not agree"
              end
          end
    in
      fold rev_transitive (tl ths) (hd ths)
    end

(* Skip to argument n times. For example, if applied to rewrite a
   proposition in implication form (==> or -->), it will skip the
   first n assumptions.
 *)
fun skip_n_conv n cv =
    if n <= 0 then cv else Conv.arg_conv (skip_n_conv (n-1) cv)

(* Given a term t, and pairs (a_i, eq_i), where a_i's are atomic
   subterms of t. Suppose the input is obtained by replacing each a_i
   by the left side of eq_i in t, obtain equality from t to the term
   obtained by replacing each a_i by the right side of eq_i in t.
 *)
fun pattern_rewr_conv t eq_ths ct =
    case t of
        Bound _ => raise Fail "pattern_rewr_conv: bound variable."
      | Abs _ => raise Fail "pattern_rewr_conv: abs not supported."
      | _ $ _ =>
        let
          val (f, arg) = Term.strip_comb t
          val (f', arg') = Drule.strip_comb ct
          val _ = assert (f aconv Thm.term_of f')
                         "pattern_rewr_conv: input does not match pattern."
          val ths = map (fn (t, ct) => pattern_rewr_conv t eq_ths ct)
                        (arg ~~ arg')
        in
          comb_equiv (f', ths)
        end
      | Const _ =>
        let
          val _ = assert (t aconv Thm.term_of ct)
                         "pattern_rewr_conv: input does not match pattern."
        in
          Conv.all_conv ct
        end
      | _ =>  (* Free and Var cases *)
        (case AList.lookup (op aconv) eq_ths t of
             NONE => Conv.all_conv ct
           | SOME eq_th =>
             let
               val _ = assert (lhs_of eq_th aconv (Thm.term_of ct))
                              "pattern_rewr_conv: wrong substitution."
             in
               eq_th
             end)

(* Given integer i, term b_i, and a term A = f(a_1, ..., a_n), produce
   the theorem a_i = b_i ==> A = f(a_1, ..., b_i, ..., a_n).
 *)
fun eq_cong_th i bi A ctxt =
    let
      val thy = Proof_Context.theory_of ctxt
      val (cf, cargs) = Drule.strip_comb (Thm.cterm_of ctxt A)
      val _ = assert (i < length cargs) "eq_cong_th: i out of bounds."
      val ai = Thm.term_of (nth cargs i)
      val eq_i = assume_meta_eq thy (ai, bi)
      val eqs = map Thm.reflexive (take i cargs) @ [eq_i] @
                map Thm.reflexive (drop (i + 1) cargs)
      val eq_A = comb_equiv (cf, eqs)
    in
      Thm.implies_intr (Thm.cprop_of eq_i) eq_A
    end

(* Convert theorems of form !!x y. P x y into P ?x ?y (arbitrary
   number of quantifiers).
 *)
fun forall_elim_sch th =
    case Thm.prop_of th of
        Const (@{const_name Pure.all}, _) $ Abs (x, T, _) =>
        let
          val var_xs = map fst (Term.add_var_names (Thm.prop_of th) [])
          val x' = if member (op =) var_xs x then
                     singleton (Name.variant_list var_xs) x
                   else x
          val thy = Thm.theory_of_thm th
        in
          th |> Thm.forall_elim (Thm.global_cterm_of thy (Var ((x', 0), T)))
             |> forall_elim_sch
        end
      | _ => th

(* Given P of function type, produce P == %x. P x. *)
fun reverse_eta_conv ctxt ct =
    let
      val t = Thm.term_of ct
      val argT = Term.domain_type (fastype_of t)
                 handle Match => raise CTERM ("reverse_eta_conv", [ct])
      val rhs = Abs ("x", argT, t $ Bound 0)
      val eq_th = Thm.eta_conversion (Thm.cterm_of ctxt rhs)
    in
      meta_sym eq_th
    end

(* Repeat cv exactly n times. *)
fun repeat_n_conv n cv t =
    if n = 0 then Conv.all_conv t
    else (cv then_conv (repeat_n_conv (n-1) cv)) t

(* Generic function for testing a conv. *)
fun test_conv ctxt cv err_str (str1, str2) =
    let
      val (t1, t2) = (Proof_Context.read_term_pattern ctxt str1,
                      Proof_Context.read_term_pattern ctxt str2)
      val th = cv (Thm.cterm_of ctxt t1)
    in
      if t1 aconv (lhs_of th) andalso t2 aconv (rhs_of th) then ()
      else let
        val _ = trace_t ctxt "Input:" t1
        val _ = trace_t ctxt "Expected:" t2
        val _ = trace_t ctxt "Actual:" (Thm.prop_of th)
      in
        raise Fail err_str
      end
    end

(* term_pat and typ_pat, from Isabelle Cookbook. *)
val term_pat_setup =
    let
      val parser = Args.context -- Scan.lift Parse.embedded_inner_syntax
      fun term_pat (ctxt, str) =
          str |> Proof_Context.read_term_pattern ctxt
              |> ML_Syntax.print_term
              |> ML_Syntax.atomic
    in
      ML_Antiquotation.inline @{binding "term_pat"} (parser >> term_pat)
    end

val cterm_pat_setup =
    let
      val parser = Args.context -- Scan.lift Parse.embedded_inner_syntax
      fun cterm_pat (ctxt, str) =
          str |> Proof_Context.read_term_pattern ctxt
              |> ML_Syntax.print_term
              |> ML_Syntax.atomic
              |> prefix "Thm.cterm_of ML_context"
    in
      ML_Antiquotation.value @{binding "cterm_pat"} (parser >> cterm_pat)
    end

val type_pat_setup =
    let
      val parser = Args.context -- Scan.lift Parse.embedded_inner_syntax
      fun typ_pat (ctxt, str) =
          let
            val ctxt' = Proof_Context.set_mode Proof_Context.mode_schematic ctxt
          in
            str |> Syntax.read_typ ctxt'
                |> ML_Syntax.print_typ
                |> ML_Syntax.atomic
          end
    in
      ML_Antiquotation.inline @{binding "typ_pat"} (parser >> typ_pat)
    end

(* Time the given function f : unit -> 'a. *)
fun timer (msg, f) =
    let
      val t_start = Timing.start ()
      val res = f ()
      val t_end = Timing.result t_start
    in
      (writeln (msg ^ (Timing.message t_end)); res)
    end

end  (* structure Util. *)

structure Basic_Util: BASIC_UTIL = Util
open Basic_Util

val _ = Theory.setup (Util.term_pat_setup)
val _ = Theory.setup (Util.cterm_pat_setup)
val _ = Theory.setup (Util.type_pat_setup)