src/HOL/Tools/Nitpick/nitpick_hol.ML

bump up Nitpick's axiom/definition unfolding limits, because some real-world problems (e.g. from Boogie) ran into the previous limits;
the limits are there to prevent infinite recursion; they can be set arbitrarily high without much harm

(*  Title:      HOL/Nitpick/Tools/nitpick_hol.ML
    Author:     Jasmin Blanchette, TU Muenchen
    Copyright   2008, 2009

Auxiliary HOL-related functions used by Nitpick.
*)

signature NITPICK_HOL =
sig
  type styp = Nitpick_Util.styp
  type const_table = term list Symtab.table
  type special_fun = (styp * int list * term list) * styp
  type unrolled = styp * styp
  type wf_cache = (styp * (bool * bool)) list

  type extended_context = {
    thy: theory,
    ctxt: Proof.context,
    max_bisim_depth: int,
    boxes: (typ option * bool option) list,
    wfs: (styp option * bool option) list,
    user_axioms: bool option,
    debug: bool,
    destroy_constrs: bool,
    specialize: bool,
    skolemize: bool,
    star_linear_preds: bool,
    uncurry: bool,
    fast_descrs: bool,
    tac_timeout: Time.time option,
    evals: term list,
    case_names: (string * int) list,
    def_table: const_table,
    nondef_table: const_table,
    user_nondefs: term list,
    simp_table: const_table Unsynchronized.ref,
    psimp_table: const_table,
    intro_table: const_table,
    ground_thm_table: term list Inttab.table,
    ersatz_table: (string * string) list,
    skolems: (string * string list) list Unsynchronized.ref,
    special_funs: special_fun list Unsynchronized.ref,
    unrolled_preds: unrolled list Unsynchronized.ref,
    wf_cache: wf_cache Unsynchronized.ref,
    constr_cache: (typ * styp list) list Unsynchronized.ref}

  val name_sep : string
  val numeral_prefix : string
  val skolem_prefix : string
  val eval_prefix : string
  val original_name : string -> string
  val unbox_type : typ -> typ
  val string_for_type : Proof.context -> typ -> string
  val prefix_name : string -> string -> string
  val short_name : string -> string
  val short_const_name : string -> string
  val shorten_const_names_in_term : term -> term
  val type_match : theory -> typ * typ -> bool
  val const_match : theory -> styp * styp -> bool
  val term_match : theory -> term * term -> bool
  val is_TFree : typ -> bool
  val is_higher_order_type : typ -> bool
  val is_fun_type : typ -> bool
  val is_set_type : typ -> bool
  val is_pair_type : typ -> bool
  val is_lfp_iterator_type : typ -> bool
  val is_gfp_iterator_type : typ -> bool
  val is_fp_iterator_type : typ -> bool
  val is_boolean_type : typ -> bool
  val is_integer_type : typ -> bool
  val is_record_type : typ -> bool
  val is_number_type : theory -> typ -> bool
  val const_for_iterator_type : typ -> styp
  val nth_range_type : int -> typ -> typ
  val num_factors_in_type : typ -> int
  val num_binder_types : typ -> int
  val curried_binder_types : typ -> typ list
  val mk_flat_tuple : typ -> term list -> term
  val dest_n_tuple : int -> term -> term list
  val instantiate_type : theory -> typ -> typ -> typ -> typ
  val is_codatatype : theory -> typ -> bool
  val is_pure_typedef : theory -> typ -> bool
  val is_univ_typedef : theory -> typ -> bool
  val is_datatype : theory -> typ -> bool
  val is_record_constr : styp -> bool
  val is_record_get : theory -> styp -> bool
  val is_record_update : theory -> styp -> bool
  val is_abs_fun : theory -> styp -> bool
  val is_rep_fun : theory -> styp -> bool
  val is_constr : theory -> styp -> bool
  val is_stale_constr : theory -> styp -> bool
  val is_sel : string -> bool
  val discr_for_constr : styp -> styp
  val num_sels_for_constr_type : typ -> int
  val nth_sel_name_for_constr_name : string -> int -> string
  val nth_sel_for_constr : styp -> int -> styp
  val boxed_nth_sel_for_constr : extended_context -> styp -> int -> styp
  val sel_no_from_name : string -> int
  val eta_expand : typ list -> term -> int -> term
  val extensionalize : term -> term
  val distinctness_formula : typ -> term list -> term
  val register_frac_type : string -> (string * string) list -> theory -> theory
  val unregister_frac_type : string -> theory -> theory
  val register_codatatype : typ -> string -> styp list -> theory -> theory
  val unregister_codatatype : typ -> theory -> theory
  val datatype_constrs : extended_context -> typ -> styp list
  val boxed_datatype_constrs : extended_context -> typ -> styp list
  val num_datatype_constrs : extended_context -> typ -> int
  val constr_name_for_sel_like : string -> string
  val boxed_constr_for_sel : extended_context -> styp -> styp
  val card_of_type : (typ * int) list -> typ -> int
  val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
  val bounded_precise_card_of_type :
    extended_context -> int -> int -> (typ * int) list -> typ -> int
  val is_finite_type : extended_context -> typ -> bool
  val all_axioms_of : theory -> term list * term list * term list
  val arity_of_built_in_const : bool -> styp -> int option
  val is_built_in_const : bool -> styp -> bool
  val case_const_names : theory -> (string * int) list
  val const_def_table : Proof.context -> term list -> const_table
  val const_nondef_table : term list -> const_table
  val const_simp_table : Proof.context -> const_table
  val const_psimp_table : Proof.context -> const_table
  val inductive_intro_table : Proof.context -> const_table -> const_table
  val ground_theorem_table : theory -> term list Inttab.table
  val ersatz_table : theory -> (string * string) list
  val def_of_const : theory -> const_table -> styp -> term option
  val is_inductive_pred : extended_context -> styp -> bool
  val is_constr_pattern_lhs : theory -> term -> bool
  val is_constr_pattern_formula : theory -> term -> bool
  val merge_type_vars_in_terms : term list -> term list
  val ground_types_in_type : extended_context -> typ -> typ list
  val ground_types_in_terms : extended_context -> term list -> typ list
  val format_type : int list -> int list -> typ -> typ
  val format_term_type :
    theory -> const_table -> (term option * int list) list -> term -> typ
  val user_friendly_const :
   extended_context -> string * string -> (term option * int list) list
   -> styp -> term * typ
  val assign_operator_for_const : styp -> string
  val preprocess_term :
    extended_context -> term -> ((term list * term list) * (bool * bool)) * term
end;

structure Nitpick_HOL : NITPICK_HOL =
struct

open Nitpick_Util

type const_table = term list Symtab.table
type special_fun = (styp * int list * term list) * styp
type unrolled = styp * styp
type wf_cache = (styp * (bool * bool)) list

type extended_context = {
  thy: theory,
  ctxt: Proof.context,
  max_bisim_depth: int,
  boxes: (typ option * bool option) list,
  wfs: (styp option * bool option) list,
  user_axioms: bool option,
  debug: bool,
  destroy_constrs: bool,
  specialize: bool,
  skolemize: bool,
  star_linear_preds: bool,
  uncurry: bool,
  fast_descrs: bool,
  tac_timeout: Time.time option,
  evals: term list,
  case_names: (string * int) list,
  def_table: const_table,
  nondef_table: const_table,
  user_nondefs: term list,
  simp_table: const_table Unsynchronized.ref,
  psimp_table: const_table,
  intro_table: const_table,
  ground_thm_table: term list Inttab.table,
  ersatz_table: (string * string) list,
  skolems: (string * string list) list Unsynchronized.ref,
  special_funs: special_fun list Unsynchronized.ref,
  unrolled_preds: unrolled list Unsynchronized.ref,
  wf_cache: wf_cache Unsynchronized.ref,
  constr_cache: (typ * styp list) list Unsynchronized.ref}

structure Data = Theory_Data(
  type T = {frac_types: (string * (string * string) list) list,
            codatatypes: (string * (string * styp list)) list}
  val empty = {frac_types = [], codatatypes = []}
  val extend = I
  fun merge ({frac_types = fs1, codatatypes = cs1},
               {frac_types = fs2, codatatypes = cs2}) : T =
    {frac_types = AList.merge (op =) (K true) (fs1, fs2),
     codatatypes = AList.merge (op =) (K true) (cs1, cs2)})

(* term * term -> term *)
fun s_conj (t1, @{const True}) = t1
  | s_conj (@{const True}, t2) = t2
  | s_conj (t1, t2) = if @{const False} mem [t1, t2] then @{const False}
                      else HOLogic.mk_conj (t1, t2)
fun s_disj (t1, @{const False}) = t1
  | s_disj (@{const False}, t2) = t2
  | s_disj (t1, t2) = if @{const True} mem [t1, t2] then @{const True}
                      else HOLogic.mk_disj (t1, t2)
(* term -> term -> term *)
fun mk_exists v t =
  HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)

(* term -> term -> term list *)
fun strip_connective conn_t (t as (t0 $ t1 $ t2)) =
    if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t]
  | strip_connective _ t = [t]
(* term -> term list * term *)
fun strip_any_connective (t as (t0 $ t1 $ t2)) =
    if t0 mem [@{const "op &"}, @{const "op |"}] then
      (strip_connective t0 t, t0)
    else
      ([t], @{const Not})
  | strip_any_connective t = ([t], @{const Not})
(* term -> term list *)
val conjuncts = strip_connective @{const "op &"}
val disjuncts = strip_connective @{const "op |"}

val name_sep = "$"
val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep
val sel_prefix = nitpick_prefix ^ "sel"
val discr_prefix = nitpick_prefix ^ "is" ^ name_sep
val set_prefix = nitpick_prefix ^ "set" ^ name_sep
val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep
val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep
val nwf_prefix = nitpick_prefix ^ "nwf" ^ name_sep
val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep
val base_prefix = nitpick_prefix ^ "base" ^ name_sep
val step_prefix = nitpick_prefix ^ "step" ^ name_sep
val ubfp_prefix = nitpick_prefix ^ "ubfp" ^ name_sep
val lbfp_prefix = nitpick_prefix ^ "lbfp" ^ name_sep
val skolem_prefix = nitpick_prefix ^ "sk"
val special_prefix = nitpick_prefix ^ "sp"
val uncurry_prefix = nitpick_prefix ^ "unc"
val eval_prefix = nitpick_prefix ^ "eval"
val bound_var_prefix = "b"
val cong_var_prefix = "c"
val iter_var_prefix = "i"
val val_var_prefix = nitpick_prefix ^ "v"
val arg_var_prefix = "x"

(* int -> string *)
fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep
fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep
(* int -> int -> string *)
fun skolem_prefix_for k j =
  skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
fun uncurry_prefix_for k j =
  uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep

(* string -> string * string *)
val strip_first_name_sep =
  Substring.full #> Substring.position name_sep ##> Substring.triml 1
  #> pairself Substring.string
(* string -> string *)
fun original_name s =
  if String.isPrefix nitpick_prefix s then
    case strip_first_name_sep s of (s1, "") => s1 | (_, s2) => original_name s2
  else
    s
val after_name_sep = snd o strip_first_name_sep

(* When you add constants to these lists, make sure to handle them in
   "Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
   well. *)
val built_in_consts =
  [(@{const_name all}, 1),
   (@{const_name "=="}, 2),
   (@{const_name "==>"}, 2),
   (@{const_name Pure.conjunction}, 2),
   (@{const_name Trueprop}, 1),
   (@{const_name Not}, 1),
   (@{const_name False}, 0),
   (@{const_name True}, 0),
   (@{const_name All}, 1),
   (@{const_name Ex}, 1),
   (@{const_name "op ="}, 2),
   (@{const_name "op &"}, 2),
   (@{const_name "op |"}, 2),
   (@{const_name "op -->"}, 2),
   (@{const_name If}, 3),
   (@{const_name Let}, 2),
   (@{const_name Unity}, 0),
   (@{const_name Pair}, 2),
   (@{const_name fst}, 1),
   (@{const_name snd}, 1),
   (@{const_name Id}, 0),
   (@{const_name insert}, 2),
   (@{const_name converse}, 1),
   (@{const_name trancl}, 1),
   (@{const_name rel_comp}, 2),
   (@{const_name image}, 2),
   (@{const_name Suc}, 0),
   (@{const_name finite}, 1),
   (@{const_name nat}, 0),
   (@{const_name zero_nat_inst.zero_nat}, 0),
   (@{const_name one_nat_inst.one_nat}, 0),
   (@{const_name plus_nat_inst.plus_nat}, 0),
   (@{const_name minus_nat_inst.minus_nat}, 0),
   (@{const_name times_nat_inst.times_nat}, 0),
   (@{const_name div_nat_inst.div_nat}, 0),
   (@{const_name div_nat_inst.mod_nat}, 0),
   (@{const_name ord_nat_inst.less_nat}, 2),
   (@{const_name ord_nat_inst.less_eq_nat}, 2),
   (@{const_name nat_gcd}, 0),
   (@{const_name nat_lcm}, 0),
   (@{const_name zero_int_inst.zero_int}, 0),
   (@{const_name one_int_inst.one_int}, 0),
   (@{const_name plus_int_inst.plus_int}, 0),
   (@{const_name minus_int_inst.minus_int}, 0),
   (@{const_name times_int_inst.times_int}, 0),
   (@{const_name div_int_inst.div_int}, 0),
   (@{const_name div_int_inst.mod_int}, 0),
   (@{const_name uminus_int_inst.uminus_int}, 0),
   (@{const_name ord_int_inst.less_int}, 2),
   (@{const_name ord_int_inst.less_eq_int}, 2),
   (@{const_name Tha}, 1),
   (@{const_name Frac}, 0),
   (@{const_name norm_frac}, 0)]
val built_in_descr_consts =
  [(@{const_name The}, 1),
   (@{const_name Eps}, 1)]
val built_in_typed_consts =
  [((@{const_name of_nat}, nat_T --> int_T), 0)]
val built_in_set_consts =
  [(@{const_name lower_semilattice_fun_inst.inf_fun}, 2),
   (@{const_name upper_semilattice_fun_inst.sup_fun}, 2),
   (@{const_name minus_fun_inst.minus_fun}, 2),
   (@{const_name ord_fun_inst.less_eq_fun}, 2)]

(* typ -> typ *)
fun unbox_type (Type (@{type_name fun_box}, Ts)) =
    Type ("fun", map unbox_type Ts)
  | unbox_type (Type (@{type_name pair_box}, Ts)) =
    Type ("*", map unbox_type Ts)
  | unbox_type (Type (s, Ts)) = Type (s, map unbox_type Ts)
  | unbox_type T = T
(* Proof.context -> typ -> string *)
fun string_for_type ctxt = Syntax.string_of_typ ctxt o unbox_type

(* string -> string -> string *)
val prefix_name = Long_Name.qualify o Long_Name.base_name
(* string -> string *)
fun short_name s = List.last (space_explode "." s) handle List.Empty => ""
(* string -> term -> term *)
val prefix_abs_vars = Term.map_abs_vars o prefix_name
(* term -> term *)
val shorten_abs_vars = Term.map_abs_vars short_name
(* string -> string *)
fun short_const_name s =
  case space_explode name_sep s of
    [_] => s |> String.isPrefix nitpick_prefix s ? unprefix nitpick_prefix
  | ss => map short_name ss |> space_implode "_"
(* term -> term *)
val shorten_const_names_in_term =
  map_aterms (fn Const (s, T) => Const (short_const_name s, T) | t => t)

(* theory -> typ * typ -> bool *)
fun type_match thy (T1, T2) =
  (Sign.typ_match thy (T2, T1) Vartab.empty; true)
  handle Type.TYPE_MATCH => false
(* theory -> styp * styp -> bool *)
fun const_match thy ((s1, T1), (s2, T2)) =
  s1 = s2 andalso type_match thy (T1, T2)
(* theory -> term * term -> bool *)
fun term_match thy (Const x1, Const x2) = const_match thy (x1, x2)
  | term_match thy (Free (s1, T1), Free (s2, T2)) =
    const_match thy ((short_name s1, T1), (short_name s2, T2))
  | term_match thy (t1, t2) = t1 aconv t2

(* typ -> bool *)
fun is_TFree (TFree _) = true
  | is_TFree _ = false
fun is_higher_order_type (Type ("fun", _)) = true
  | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
  | is_higher_order_type _ = false
fun is_fun_type (Type ("fun", _)) = true
  | is_fun_type _ = false
fun is_set_type (Type ("fun", [_, @{typ bool}])) = true
  | is_set_type _ = false
fun is_pair_type (Type ("*", _)) = true
  | is_pair_type _ = false
fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s
  | is_lfp_iterator_type _ = false
fun is_gfp_iterator_type (Type (s, _)) = String.isPrefix gfp_iterator_prefix s
  | is_gfp_iterator_type _ = false
val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type
val is_boolean_type = equal prop_T orf equal bool_T
val is_integer_type =
  member (op =) [nat_T, int_T, @{typ bisim_iterator}] orf is_fp_iterator_type
val is_record_type = not o null o Record.dest_recTs
(* theory -> typ -> bool *)
fun is_frac_type thy (Type (s, [])) =
    not (null (these (AList.lookup (op =) (#frac_types (Data.get thy)) s)))
  | is_frac_type _ _ = false
fun is_number_type thy = is_integer_type orf is_frac_type thy

(* bool -> styp -> typ *)
fun iterator_type_for_const gfp (s, T) =
  Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s,
        binder_types T)
(* typ -> styp *)
fun const_for_iterator_type (Type (s, Ts)) = (after_name_sep s, Ts ---> bool_T)
  | const_for_iterator_type T =
    raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], [])

(* int -> typ -> typ * typ *)
fun strip_n_binders 0 T = ([], T)
  | strip_n_binders n (Type ("fun", [T1, T2])) =
    strip_n_binders (n - 1) T2 |>> cons T1
  | strip_n_binders n (Type (@{type_name fun_box}, Ts)) =
    strip_n_binders n (Type ("fun", Ts))
  | strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], [])
(* typ -> typ *)
val nth_range_type = snd oo strip_n_binders

(* typ -> int *)
fun num_factors_in_type (Type ("*", [T1, T2])) =
    fold (Integer.add o num_factors_in_type) [T1, T2] 0
  | num_factors_in_type _ = 1
fun num_binder_types (Type ("fun", [_, T2])) = 1 + num_binder_types T2
  | num_binder_types _ = 0
(* typ -> typ list *)
val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types
fun maybe_curried_binder_types T =
  (if is_pair_type (body_type T) then binder_types else curried_binder_types) T

(* typ -> term list -> term *)
fun mk_flat_tuple _ [t] = t
  | mk_flat_tuple (Type ("*", [T1, T2])) (t :: ts) =
    HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts)
  | mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts)
(* int -> term -> term list *)
fun dest_n_tuple 1 t = [t]
  | dest_n_tuple n t = HOLogic.dest_prod t ||> dest_n_tuple (n - 1) |> op ::

(* int -> typ -> typ list *)
fun dest_n_tuple_type 1 T = [T]
  | dest_n_tuple_type n (Type (_, [T1, T2])) =
    T1 :: dest_n_tuple_type (n - 1) T2
  | dest_n_tuple_type _ T =
    raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], [])

(* (typ * typ) list -> typ -> typ *)
fun typ_subst [] T = T
  | typ_subst ps T =
    let
      (* typ -> typ *)
      fun subst T =
        case AList.lookup (op =) ps T of
          SOME T' => T'
        | NONE => case T of Type (s, Ts) => Type (s, map subst Ts) | _ => T
    in subst T end

(* theory -> typ -> typ -> typ -> typ *)
fun instantiate_type thy T1 T1' T2 =
  Same.commit (Envir.subst_type_same
                   (Sign.typ_match thy (Logic.varifyT T1, T1') Vartab.empty))
              (Logic.varifyT T2)
  handle Type.TYPE_MATCH =>
         raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], [])

(* theory -> typ -> typ -> styp *)
fun repair_constr_type thy body_T' T =
  instantiate_type thy (body_type T) body_T' T

(* string -> (string * string) list -> theory -> theory *)
fun register_frac_type frac_s ersaetze thy =
  let
    val {frac_types, codatatypes} = Data.get thy
    val frac_types = AList.update (op =) (frac_s, ersaetze) frac_types
  in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
(* string -> theory -> theory *)
fun unregister_frac_type frac_s = register_frac_type frac_s []

(* typ -> string -> styp list -> theory -> theory *)
fun register_codatatype co_T case_name constr_xs thy =
  let
    val {frac_types, codatatypes} = Data.get thy
    val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs
    val (co_s, co_Ts) = dest_Type co_T
    val _ =
      if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) then ()
      else raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], [])
    val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs))
                                   codatatypes
  in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
(* typ -> theory -> theory *)
fun unregister_codatatype co_T = register_codatatype co_T "" []

type typedef_info =
  {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
   set_def: thm option, prop_of_Rep: thm, set_name: string,
   Rep_inverse: thm option}

(* theory -> string -> typedef_info *)
fun typedef_info thy s =
  if is_frac_type thy (Type (s, [])) then
    SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
          Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
          set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
                          |> Logic.varify,
          set_name = @{const_name Frac}, Rep_inverse = NONE}
  else case Typedef.get_info thy s of
    SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Rep_inverse,
          ...} =>
    SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
          Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
          set_name = set_prefix ^ s, Rep_inverse = SOME Rep_inverse}
  | NONE => NONE

(* string -> bool *)
fun is_basic_datatype s =
    s mem [@{type_name "*"}, @{type_name bool}, @{type_name unit},
           @{type_name nat}, @{type_name int}]
(* theory -> string -> bool *)
val is_typedef = is_some oo typedef_info
val is_real_datatype = is_some oo Datatype.get_info
(* theory -> typ -> bool *)
fun is_codatatype thy (T as Type (s, _)) =
    not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
               |> Option.map snd |> these))
  | is_codatatype _ _ = false
fun is_pure_typedef thy (T as Type (s, _)) =
    is_typedef thy s andalso
    not (is_real_datatype thy s orelse is_codatatype thy T
         orelse is_record_type T orelse is_integer_type T)
  | is_pure_typedef _ _ = false
fun is_univ_typedef thy (Type (s, _)) =
    (case typedef_info thy s of
       SOME {set_def, prop_of_Rep, ...} =>
       (case set_def of
          SOME thm =>
          try (fst o dest_Const o snd o Logic.dest_equals o prop_of) thm
        | NONE =>
          try (fst o dest_Const o snd o HOLogic.dest_mem
               o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name UNIV}
     | NONE => false)
  | is_univ_typedef _ _ = false
fun is_datatype thy (T as Type (s, _)) =
    (is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind})
    andalso not (is_basic_datatype s)
  | is_datatype _ _ = false

(* theory -> typ -> (string * typ) list * (string * typ) *)
fun all_record_fields thy T =
  let val (recs, more) = Record.get_extT_fields thy T in
    recs @ more :: all_record_fields thy (snd more)
  end
  handle TYPE _ => []
(* styp -> bool *)
fun is_record_constr (x as (s, T)) =
  String.isSuffix Record.extN s andalso
  let val dataT = body_type T in
    is_record_type dataT andalso
    s = unsuffix Record.ext_typeN (fst (dest_Type dataT)) ^ Record.extN
  end
(* theory -> typ -> int *)
val num_record_fields = Integer.add 1 o length o fst oo Record.get_extT_fields
(* theory -> string -> typ -> int *)
fun no_of_record_field thy s T1 =
  find_index (equal s o fst) (Record.get_extT_fields thy T1 ||> single |> op @)
(* theory -> styp -> bool *)
fun is_record_get thy (s, Type ("fun", [T1, _])) =
    exists (equal s o fst) (all_record_fields thy T1)
  | is_record_get _ _ = false
fun is_record_update thy (s, T) =
  String.isSuffix Record.updateN s andalso
  exists (equal (unsuffix Record.updateN s) o fst)
         (all_record_fields thy (body_type T))
  handle TYPE _ => false
fun is_abs_fun thy (s, Type ("fun", [_, Type (s', _)])) =
    (case typedef_info thy s' of
       SOME {Abs_name, ...} => s = Abs_name
     | NONE => false)
  | is_abs_fun _ _ = false
fun is_rep_fun thy (s, Type ("fun", [Type (s', _), _])) =
    (case typedef_info thy s' of
       SOME {Rep_name, ...} => s = Rep_name
     | NONE => false)
  | is_rep_fun _ _ = false

(* theory -> styp -> styp *)
fun mate_of_rep_fun thy (x as (_, Type ("fun", [T1 as Type (s', _), T2]))) =
    (case typedef_info thy s' of
       SOME {Abs_name, ...} => (Abs_name, Type ("fun", [T2, T1]))
     | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
  | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])

(* theory -> styp -> bool *)
fun is_coconstr thy (s, T) =
  let
    val {codatatypes, ...} = Data.get thy
    val co_T = body_type T
    val co_s = dest_Type co_T |> fst
  in
    exists (fn (s', T') => s = s' andalso repair_constr_type thy co_T T' = T)
           (AList.lookup (op =) codatatypes co_s |> Option.map snd |> these)
  end
  handle TYPE ("dest_Type", _, _) => false
fun is_constr_like thy (s, T) =
  s mem [@{const_name FunBox}, @{const_name PairBox}] orelse
  let val (x as (s, T)) = (s, unbox_type T) in
    Refute.is_IDT_constructor thy x orelse is_record_constr x
    orelse (is_abs_fun thy x andalso is_pure_typedef thy (range_type T))
    orelse s mem [@{const_name Zero_Rep}, @{const_name Suc_Rep}]
    orelse x = (@{const_name zero_nat_inst.zero_nat}, nat_T)
    orelse is_coconstr thy x
  end
fun is_stale_constr thy (x as (_, T)) =
  is_codatatype thy (body_type T) andalso is_constr_like thy x
  andalso not (is_coconstr thy x)
fun is_constr thy (x as (_, T)) =
  is_constr_like thy x
  andalso not (is_basic_datatype (fst (dest_Type (body_type T))))
  andalso not (is_stale_constr thy x)
(* string -> bool *)
val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
val is_sel_like_and_no_discr =
  String.isPrefix sel_prefix
  orf (member (op =) [@{const_name fst}, @{const_name snd}])

datatype boxability =
  InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2

(* boxability -> boxability *)
fun in_fun_lhs_for InConstr = InSel
  | in_fun_lhs_for _ = InFunLHS
fun in_fun_rhs_for InConstr = InConstr
  | in_fun_rhs_for InSel = InSel
  | in_fun_rhs_for InFunRHS1 = InFunRHS2
  | in_fun_rhs_for _ = InFunRHS1

(* extended_context -> boxability -> typ -> bool *)
fun is_boxing_worth_it (ext_ctxt : extended_context) boxy T =
  case T of
    Type ("fun", _) =>
    boxy mem [InPair, InFunLHS] andalso not (is_boolean_type (body_type T))
  | Type ("*", Ts) =>
    boxy mem [InPair, InFunRHS1, InFunRHS2]
    orelse (boxy mem [InExpr, InFunLHS]
            andalso exists (is_boxing_worth_it ext_ctxt InPair)
                           (map (box_type ext_ctxt InPair) Ts))
  | _ => false
(* extended_context -> boxability -> string * typ list -> string *)
and should_box_type (ext_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) =
  case triple_lookup (type_match thy) boxes (Type z) of
    SOME (SOME box_me) => box_me
  | _ => is_boxing_worth_it ext_ctxt boxy (Type z)
(* extended_context -> boxability -> typ -> typ *)
and box_type ext_ctxt boxy T =
  case T of
    Type (z as ("fun", [T1, T2])) =>
    if not (boxy mem [InConstr, InSel])
       andalso should_box_type ext_ctxt boxy z then
      Type (@{type_name fun_box},
            [box_type ext_ctxt InFunLHS T1, box_type ext_ctxt InFunRHS1 T2])
    else
      box_type ext_ctxt (in_fun_lhs_for boxy) T1
      --> box_type ext_ctxt (in_fun_rhs_for boxy) T2
  | Type (z as ("*", Ts)) =>
    if should_box_type ext_ctxt boxy z then
      Type (@{type_name pair_box}, map (box_type ext_ctxt InSel) Ts)
    else
      Type ("*", map (box_type ext_ctxt
                               (if boxy mem [InConstr, InSel] then boxy
                                else InPair)) Ts)
  | _ => T

(* styp -> styp *)
fun discr_for_constr (s, T) = (discr_prefix ^ s, body_type T --> bool_T)

(* typ -> int *)
fun num_sels_for_constr_type T = length (maybe_curried_binder_types T)
(* string -> int -> string *)
fun nth_sel_name_for_constr_name s n =
  if s = @{const_name Pair} then
    if n = 0 then @{const_name fst} else @{const_name snd}
  else
    sel_prefix_for n ^ s
(* styp -> int -> styp *)
fun nth_sel_for_constr x ~1 = discr_for_constr x
  | nth_sel_for_constr (s, T) n =
    (nth_sel_name_for_constr_name s n,
     body_type T --> nth (maybe_curried_binder_types T) n)
(* extended_context -> styp -> int -> styp *)
fun boxed_nth_sel_for_constr ext_ctxt =
  apsnd (box_type ext_ctxt InSel) oo nth_sel_for_constr

(* string -> int *)
fun sel_no_from_name s =
  if String.isPrefix discr_prefix s then
    ~1
  else if String.isPrefix sel_prefix s then
    s |> unprefix sel_prefix |> Int.fromString |> the
  else if s = @{const_name snd} then
    1
  else
    0

(* typ list -> term -> int -> term *)
fun eta_expand _ t 0 = t
  | eta_expand Ts (Abs (s, T, t')) n =
    Abs (s, T, eta_expand (T :: Ts) t' (n - 1))
  | eta_expand Ts t n =
    fold_rev (curry3 Abs ("x\<^isub>\<eta>" ^ nat_subscript n))
             (List.take (binder_types (fastype_of1 (Ts, t)), n))
             (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))

(* term -> term *)
fun extensionalize t =
  case t of
    (t0 as @{const Trueprop}) $ t1 => t0 $ extensionalize t1
  | Const (@{const_name "op ="}, _) $ t1 $ Abs (s, T, t2) =>
    let val v = Var ((s, maxidx_of_term t + 1), T) in
      extensionalize (HOLogic.mk_eq (t1 $ v, subst_bound (v, t2)))
    end
  | _ => t

(* typ -> term list -> term *)
fun distinctness_formula T =
  all_distinct_unordered_pairs_of
  #> map (fn (t1, t2) => @{const Not} $ (HOLogic.eq_const T $ t1 $ t2))
  #> List.foldr (s_conj o swap) @{const True}

(* typ -> term *)
fun zero_const T = Const (@{const_name zero_nat_inst.zero_nat}, T)
fun suc_const T = Const (@{const_name Suc}, T --> T)

(* theory -> typ -> styp list *)
fun uncached_datatype_constrs thy (T as Type (s, Ts)) =
    (case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
       SOME (_, xs' as (_ :: _)) =>
       map (apsnd (repair_constr_type thy T)) xs'
     | _ =>
       if is_datatype thy T then
         case Datatype.get_info thy s of
           SOME {index, descr, ...} =>
           let
             val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the
           in
             map (fn (s', Us) =>
                     (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us
                          ---> T)) constrs
           end
         | NONE =>
           if is_record_type T then
             let
               val s' = unsuffix Record.ext_typeN s ^ Record.extN
               val T' = (Record.get_extT_fields thy T
                        |> apsnd single |> uncurry append |> map snd) ---> T
             in [(s', T')] end
           else case typedef_info thy s of
             SOME {abs_type, rep_type, Abs_name, ...} =>
             [(Abs_name, instantiate_type thy abs_type T rep_type --> T)]
           | NONE =>
             if T = @{typ ind} then
               [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]
             else
               []
       else
         [])
  | uncached_datatype_constrs _ _ = []
(* extended_context -> typ -> styp list *)
fun datatype_constrs (ext_ctxt as {thy, constr_cache, ...} : extended_context)
                     T =
  case AList.lookup (op =) (!constr_cache) T of
    SOME xs => xs
  | NONE =>
    let val xs = uncached_datatype_constrs thy T in
      (Unsynchronized.change constr_cache (cons (T, xs)); xs)
    end
fun boxed_datatype_constrs ext_ctxt =
  map (apsnd (box_type ext_ctxt InConstr)) o datatype_constrs ext_ctxt
(* extended_context -> typ -> int *)
val num_datatype_constrs = length oo datatype_constrs

(* string -> string *)
fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair}
  | constr_name_for_sel_like @{const_name snd} = @{const_name Pair}
  | constr_name_for_sel_like s' = original_name s'
(* extended_context -> styp -> styp *)
fun boxed_constr_for_sel ext_ctxt (s', T') =
  let val s = constr_name_for_sel_like s' in
    AList.lookup (op =) (boxed_datatype_constrs ext_ctxt (domain_type T')) s
    |> the |> pair s
  end
(* extended_context -> styp -> term *)
fun discr_term_for_constr ext_ctxt (x as (s, T)) =
  let val dataT = body_type T in
    if s = @{const_name Suc} then
      Abs (Name.uu, dataT,
           @{const Not} $ HOLogic.mk_eq (zero_const dataT, Bound 0))
    else if num_datatype_constrs ext_ctxt dataT >= 2 then
      Const (discr_for_constr x)
    else
      Abs (Name.uu, dataT, @{const True})
  end

(* extended_context -> styp -> term -> term *)
fun discriminate_value (ext_ctxt as {thy, ...}) (x as (_, T)) t =
  case strip_comb t of
    (Const x', args) =>
    if x = x' then @{const True}
    else if is_constr_like thy x' then @{const False}
    else betapply (discr_term_for_constr ext_ctxt x, t)
  | _ => betapply (discr_term_for_constr ext_ctxt x, t)

(* styp -> term -> term *)
fun nth_arg_sel_term_for_constr (x as (s, T)) n =
  let val (arg_Ts, dataT) = strip_type T in
    if dataT = nat_T then
      @{term "%n::nat. minus_nat_inst.minus_nat n one_nat_inst.one_nat"}
    else if is_pair_type dataT then
      Const (nth_sel_for_constr x n)
    else
      let
        (* int -> typ -> int * term *)
        fun aux m (Type ("*", [T1, T2])) =
            let
              val (m, t1) = aux m T1
              val (m, t2) = aux m T2
            in (m, HOLogic.mk_prod (t1, t2)) end
          | aux m T =
            (m + 1, Const (nth_sel_name_for_constr_name s m, dataT --> T)
                    $ Bound 0)
        val m = fold (Integer.add o num_factors_in_type)
                     (List.take (arg_Ts, n)) 0
      in Abs ("x", dataT, aux m (nth arg_Ts n) |> snd) end
  end
(* theory -> styp -> term -> int -> typ -> term *)
fun select_nth_constr_arg thy x t n res_T =
  case strip_comb t of
    (Const x', args) =>
    if x = x' then nth args n
    else if is_constr_like thy x' then Const (@{const_name unknown}, res_T)
    else betapply (nth_arg_sel_term_for_constr x n, t)
  | _ => betapply (nth_arg_sel_term_for_constr x n, t)

(* theory -> styp -> term list -> term *)
fun construct_value _ x [] = Const x
  | construct_value thy (x as (s, _)) args =
    let val args = map Envir.eta_contract args in
      case hd args of
        Const (x' as (s', _)) $ t =>
        if is_sel_like_and_no_discr s' andalso constr_name_for_sel_like s' = s
           andalso forall (fn (n, t') =>
                              select_nth_constr_arg thy x t n dummyT = t')
                          (index_seq 0 (length args) ~~ args) then
          t
        else
          list_comb (Const x, args)
      | _ => list_comb (Const x, args)
    end

(* extended_context -> typ -> term -> term *)
fun constr_expand (ext_ctxt as {thy, ...}) T t =
  (case head_of t of
     Const x => if is_constr_like thy x then t else raise SAME ()
   | _ => raise SAME ())
  handle SAME () =>
         let
           val x' as (_, T') =
             if is_pair_type T then
               let val (T1, T2) = HOLogic.dest_prodT T in
                 (@{const_name Pair}, [T1, T2] ---> T)
               end
             else
               datatype_constrs ext_ctxt T |> the_single
           val arg_Ts = binder_types T'
         in
           list_comb (Const x', map2 (select_nth_constr_arg thy x' t)
                                     (index_seq 0 (length arg_Ts)) arg_Ts)
         end

(* (typ * int) list -> typ -> int *)
fun card_of_type asgns (Type ("fun", [T1, T2])) =
    reasonable_power (card_of_type asgns T2) (card_of_type asgns T1)
  | card_of_type asgns (Type ("*", [T1, T2])) =
    card_of_type asgns T1 * card_of_type asgns T2
  | card_of_type _ (Type (@{type_name itself}, _)) = 1
  | card_of_type _ @{typ prop} = 2
  | card_of_type _ @{typ bool} = 2
  | card_of_type _ @{typ unit} = 1
  | card_of_type asgns T =
    case AList.lookup (op =) asgns T of
      SOME k => k
    | NONE => if T = @{typ bisim_iterator} then 0
              else raise TYPE ("Nitpick_HOL.card_of_type", [T], [])
(* int -> (typ * int) list -> typ -> int *)
fun bounded_card_of_type max default_card asgns (Type ("fun", [T1, T2])) =
    let
      val k1 = bounded_card_of_type max default_card asgns T1
      val k2 = bounded_card_of_type max default_card asgns T2
    in
      if k1 = max orelse k2 = max then max
      else Int.min (max, reasonable_power k2 k1)
    end
  | bounded_card_of_type max default_card asgns (Type ("*", [T1, T2])) =
    let
      val k1 = bounded_card_of_type max default_card asgns T1
      val k2 = bounded_card_of_type max default_card asgns T2
    in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end
  | bounded_card_of_type max default_card asgns T =
    Int.min (max, if default_card = ~1 then
                    card_of_type asgns T
                  else
                    card_of_type asgns T
                    handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
                           default_card)
(* extended_context -> int -> (typ * int) list -> typ -> int *)
fun bounded_precise_card_of_type ext_ctxt max default_card asgns T =
  let
    (* typ list -> typ -> int *)
    fun aux avoid T =
      (if T mem avoid then
         0
       else case T of
         Type ("fun", [T1, T2]) =>
         let
           val k1 = aux avoid T1
           val k2 = aux avoid T2
         in
           if k1 = 0 orelse k2 = 0 then 0
           else if k1 >= max orelse k2 >= max then max
           else Int.min (max, reasonable_power k2 k1)
         end
       | Type ("*", [T1, T2]) =>
         let
           val k1 = aux avoid T1
           val k2 = aux avoid T2
         in
           if k1 = 0 orelse k2 = 0 then 0
           else if k1 >= max orelse k2 >= max then max
           else Int.min (max, k1 * k2)
         end
       | Type (@{type_name itself}, _) => 1
       | @{typ prop} => 2
       | @{typ bool} => 2
       | @{typ unit} => 1
       | Type _ =>
         (case datatype_constrs ext_ctxt T of
            [] => if is_integer_type T then 0 else raise SAME ()
          | constrs =>
            let
              val constr_cards =
                datatype_constrs ext_ctxt T
                |> map (Integer.prod o map (aux (T :: avoid)) o binder_types
                        o snd)
            in
              if exists (equal 0) constr_cards then 0
              else Integer.sum constr_cards
            end)
       | _ => raise SAME ())
      handle SAME () => AList.lookup (op =) asgns T |> the_default default_card
  in Int.min (max, aux [] T) end

(* extended_context -> typ -> bool *)
fun is_finite_type ext_ctxt =
  not_equal 0 o bounded_precise_card_of_type ext_ctxt 1 2 []

(* term -> bool *)
fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
  | is_ground_term (Const _) = true
  | is_ground_term _ = false

(* term -> word -> word *)
fun hashw_term (t1 $ t2) = Polyhash.hashw (hashw_term t1, hashw_term t2)
  | hashw_term (Const (s, _)) = Polyhash.hashw_string (s, 0w0)
  | hashw_term _ = 0w0
(* term -> int *)
val hash_term = Word.toInt o hashw_term

(* term list -> (indexname * typ) list *)
fun special_bounds ts =
  fold Term.add_vars ts [] |> sort (TermOrd.fast_indexname_ord o pairself fst)

(* indexname * typ -> term -> term *)
fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))

(* theory -> string -> bool *)
fun is_funky_typedef_name thy s =
  s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
         @{type_name int}]
  orelse is_frac_type thy (Type (s, []))
(* theory -> term -> bool *)
fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
  | is_funky_typedef _ _ = false
(* term -> bool *)
fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _)
                         $ Const (@{const_name TYPE}, _)) = true
  | is_arity_type_axiom _ = false
(* theory -> bool -> term -> bool *)
fun is_typedef_axiom thy boring (@{const "==>"} $ _ $ t2) =
    is_typedef_axiom thy boring t2
  | is_typedef_axiom thy boring
        (@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
         $ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) =
    boring <> is_funky_typedef_name thy s andalso is_typedef thy s
  | is_typedef_axiom _ _ _ = false

(* Distinguishes between (1) constant definition axioms, (2) type arity and
   typedef axioms, and (3) other axioms, and returns the pair ((1), (3)).
   Typedef axioms are uninteresting to Nitpick, because it can retrieve them
   using "typedef_info". *)
(* theory -> (string * term) list -> string list -> term list * term list *)
fun partition_axioms_by_definitionality thy axioms def_names =
  let
    val axioms = sort (fast_string_ord o pairself fst) axioms
    val defs = OrdList.inter (fast_string_ord o apsnd fst) def_names axioms
    val nondefs =
      OrdList.subtract (fast_string_ord o apsnd fst) def_names axioms
      |> filter_out ((is_arity_type_axiom orf is_typedef_axiom thy true) o snd)
  in pairself (map snd) (defs, nondefs) end

(* Ideally we would check against "Complex_Main", not "Refute", but any theory
   will do as long as it contains all the "axioms" and "axiomatization"
   commands. *)
(* theory -> bool *)
fun is_built_in_theory thy = Theory.subthy (thy, @{theory Refute})

(* term -> bool *)
val is_plain_definition =
  let
    (* term -> bool *)
    fun do_lhs t1 =
      case strip_comb t1 of
        (Const _, args) => forall is_Var args
                           andalso not (has_duplicates (op =) args)
      | _ => false
    fun do_eq (Const (@{const_name "=="}, _) $ t1 $ _) = do_lhs t1
      | do_eq (@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)) =
        do_lhs t1
      | do_eq _ = false
  in do_eq end

(* theory -> term list * term list * term list *)
fun all_axioms_of thy =
  let
    (* theory list -> term list *)
    val axioms_of_thys = maps Thm.axioms_of #> map (apsnd prop_of)
    val specs = Defs.all_specifications_of (Theory.defs_of thy)
    val def_names = specs |> maps snd |> map_filter #def
                    |> OrdList.make fast_string_ord
    val thys = thy :: Theory.ancestors_of thy
    val (built_in_thys, user_thys) = List.partition is_built_in_theory thys
    val built_in_axioms = axioms_of_thys built_in_thys
    val user_axioms = axioms_of_thys user_thys
    val (built_in_defs, built_in_nondefs) =
      partition_axioms_by_definitionality thy built_in_axioms def_names
      ||> filter (is_typedef_axiom thy false)
    val (user_defs, user_nondefs) =
      partition_axioms_by_definitionality thy user_axioms def_names
    val (built_in_nondefs, user_nondefs) =
      List.partition (is_typedef_axiom thy false) user_nondefs
      |>> append built_in_nondefs
    val defs = (thy |> PureThy.all_thms_of
                    |> filter (equal Thm.definitionK o Thm.get_kind o snd)
                    |> map (prop_of o snd) |> filter is_plain_definition) @
               user_defs @ built_in_defs
  in (defs, built_in_nondefs, user_nondefs) end

(* bool -> styp -> int option *)
fun arity_of_built_in_const fast_descrs (s, T) =
  if s = @{const_name If} then
    if nth_range_type 3 T = @{typ bool} then NONE else SOME 3
  else case AList.lookup (op =)
                (built_in_consts
                 |> fast_descrs ? append built_in_descr_consts) s of
    SOME n => SOME n
  | NONE =>
    case AList.lookup (op =) built_in_typed_consts (s, T) of
      SOME n => SOME n
    | NONE =>
      if is_fun_type T andalso is_set_type (domain_type T) then
        AList.lookup (op =) built_in_set_consts s
      else
        NONE
(* bool -> styp -> bool *)
val is_built_in_const = is_some oo arity_of_built_in_const

(* This function is designed to work for both real definition axioms and
   simplification rules (equational specifications). *)
(* term -> term *)
fun term_under_def t =
  case t of
    @{const "==>"} $ _ $ t2 => term_under_def t2
  | Const (@{const_name "=="}, _) $ t1 $ _ => term_under_def t1
  | @{const Trueprop} $ t1 => term_under_def t1
  | Const (@{const_name "op ="}, _) $ t1 $ _ => term_under_def t1
  | Abs (_, _, t') => term_under_def t'
  | t1 $ _ => term_under_def t1
  | _ => t

(* Here we crucially rely on "Refute.specialize_type" performing a preorder
   traversal of the term, without which the wrong occurrence of a constant could
   be matched in the face of overloading. *)
(* theory -> bool -> const_table -> styp -> term list *)
fun def_props_for_const thy fast_descrs table (x as (s, _)) =
  if is_built_in_const fast_descrs x then
    []
  else
    these (Symtab.lookup table s)
    |> map_filter (try (Refute.specialize_type thy x))
    |> filter (equal (Const x) o term_under_def)

(* theory -> term -> term option *)
fun normalized_rhs_of thy t =
  let
    (* term option -> term option *)
    fun aux (v as Var _) (SOME t) = SOME (lambda v t)
      | aux (c as Const (@{const_name TYPE}, T)) (SOME t) = SOME (lambda c t)
      | aux _ _ = NONE
    val (lhs, rhs) =
      case t of
        Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2)
      | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ t2) =>
        (t1, t2)
      | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
    val args = strip_comb lhs |> snd
  in fold_rev aux args (SOME rhs) end

(* theory -> const_table -> styp -> term option *)
fun def_of_const thy table (x as (s, _)) =
  if is_built_in_const false x orelse original_name s <> s then
    NONE
  else
    x |> def_props_for_const thy false table |> List.last
      |> normalized_rhs_of thy |> Option.map (prefix_abs_vars s)
    handle List.Empty => NONE

datatype fixpoint_kind = Lfp | Gfp | NoFp

(* term -> fixpoint_kind *)
fun fixpoint_kind_of_rhs (Abs (_, _, t)) = fixpoint_kind_of_rhs t
  | fixpoint_kind_of_rhs (Const (@{const_name lfp}, _) $ Abs _) = Lfp
  | fixpoint_kind_of_rhs (Const (@{const_name gfp}, _) $ Abs _) = Gfp
  | fixpoint_kind_of_rhs _ = NoFp

(* theory -> const_table -> term -> bool *)
fun is_mutually_inductive_pred_def thy table t =
  let
    (* term -> bool *)
    fun is_good_arg (Bound _) = true
      | is_good_arg (Const (s, _)) =
        s mem [@{const_name True}, @{const_name False}, @{const_name undefined}]
      | is_good_arg _ = false
  in
    case t |> strip_abs_body |> strip_comb of
      (Const x, ts as (_ :: _)) =>
      (case def_of_const thy table x of
         SOME t' => fixpoint_kind_of_rhs t' <> NoFp andalso forall is_good_arg ts
       | NONE => false)
    | _ => false
  end
(* theory -> const_table -> term -> term *)
fun unfold_mutually_inductive_preds thy table =
  map_aterms (fn t as Const x =>
                 (case def_of_const thy table x of
                    SOME t' =>
                    let val t' = Envir.eta_contract t' in
                      if is_mutually_inductive_pred_def thy table t' then t'
                      else t
                    end
                 | NONE => t)
               | t => t)

(* term -> string * term *)
fun pair_for_prop t =
  case term_under_def t of
    Const (s, _) => (s, t)
  | Free _ => raise NOT_SUPPORTED "local definitions"
  | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t'])

(* (Proof.context -> term list) -> Proof.context -> const_table *)
fun table_for get ctxt =
  get ctxt |> map pair_for_prop |> AList.group (op =) |> Symtab.make

(* theory -> (string * int) list *)
fun case_const_names thy =
  Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) =>
                  if is_basic_datatype dtype_s then
                    I
                  else
                    cons (case_name, AList.lookup (op =) descr index
                                     |> the |> #3 |> length))
              (Datatype.get_all thy) [] @
  map (apsnd length o snd) (#codatatypes (Data.get thy))

(* Proof.context -> term list -> const_table *)
fun const_def_table ctxt ts =
  table_for (map prop_of o Nitpick_Defs.get) ctxt
  |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
          (map pair_for_prop ts)
(* term list -> const_table *)
fun const_nondef_table ts =
  fold (fn t => append (map (fn s => (s, t)) (Term.add_const_names t []))) ts []
  |> AList.group (op =) |> Symtab.make
(* Proof.context -> const_table *)
val const_simp_table = table_for (map prop_of o Nitpick_Simps.get)
val const_psimp_table = table_for (map prop_of o Nitpick_Psimps.get)
(* Proof.context -> const_table -> const_table *)
fun inductive_intro_table ctxt def_table =
  table_for (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt)
                                                  def_table o prop_of)
             o Nitpick_Intros.get) ctxt
(* theory -> term list Inttab.table *)
fun ground_theorem_table thy =
  fold ((fn @{const Trueprop} $ t1 =>
            is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)
          | _ => I) o prop_of o snd) (PureThy.all_thms_of thy) Inttab.empty

val basic_ersatz_table =
  [(@{const_name prod_case}, @{const_name split}),
   (@{const_name card}, @{const_name card'}),
   (@{const_name setsum}, @{const_name setsum'}),
   (@{const_name fold_graph}, @{const_name fold_graph'}),
   (@{const_name wf}, @{const_name wf'}),
   (@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
   (@{const_name wfrec}, @{const_name wfrec'})]

(* theory -> (string * string) list *)
fun ersatz_table thy =
  fold (append o snd) (#frac_types (Data.get thy)) basic_ersatz_table

(* const_table Unsynchronized.ref -> string -> term list -> unit *)
fun add_simps simp_table s eqs =
  Unsynchronized.change simp_table
      (Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s)))

(* Similar to "Refute.specialize_type" but returns all matches rather than only
   the first (preorder) match. *)
(* theory -> styp -> term -> term list *)
fun multi_specialize_type thy slack (x as (s, T)) t =
  let
    (* term -> (typ * term) list -> (typ * term) list *)
    fun aux (Const (s', T')) ys =
        if s = s' then
          ys |> (if AList.defined (op =) ys T' then
                   I
                 else
                  cons (T', Refute.monomorphic_term
                                (Sign.typ_match thy (T', T) Vartab.empty) t)
                  handle Type.TYPE_MATCH => I
                       | Refute.REFUTE _ =>
                         if slack then
                           I
                         else
                           raise NOT_SUPPORTED ("too much polymorphism in \
                                                \axiom involving " ^ quote s))
        else
          ys
      | aux _ ys = ys
  in map snd (fold_aterms aux t []) end

(* theory -> bool -> const_table -> styp -> term list *)
fun nondef_props_for_const thy slack table (x as (s, _)) =
  these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)

(* theory -> styp list -> term list *)
fun optimized_typedef_axioms thy (abs_s, abs_Ts) =
  let val abs_T = Type (abs_s, abs_Ts) in
    if is_univ_typedef thy abs_T then
      []
    else case typedef_info thy abs_s of
      SOME {abs_type, rep_type, Abs_name, Rep_name, prop_of_Rep, set_name,
            ...} =>
      let
        val rep_T = instantiate_type thy abs_type abs_T rep_type
        val rep_t = Const (Rep_name, abs_T --> rep_T)
        val set_t = Const (set_name, rep_T --> bool_T)
        val set_t' =
          prop_of_Rep |> HOLogic.dest_Trueprop
                      |> Refute.specialize_type thy (dest_Const rep_t)
                      |> HOLogic.dest_mem |> snd
      in
        [HOLogic.all_const abs_T
         $ Abs (Name.uu, abs_T, set_t $ (rep_t $ Bound 0))]
        |> set_t <> set_t' ? cons (HOLogic.mk_eq (set_t, set_t'))
        |> map HOLogic.mk_Trueprop
      end
    | NONE => []
  end
(* theory -> styp -> term *)
fun inverse_axiom_for_rep_fun thy (x as (_, T)) =
  typedef_info thy (fst (dest_Type (domain_type T)))
  |> the |> #Rep_inverse |> the |> prop_of |> Refute.specialize_type thy x

(* theory -> int * styp -> term *)
fun constr_case_body thy (j, (x as (_, T))) =
  let val arg_Ts = binder_types T in
    list_comb (Bound j, map2 (select_nth_constr_arg thy x (Bound 0))
                             (index_seq 0 (length arg_Ts)) arg_Ts)
  end
(* extended_context -> typ -> int * styp -> term -> term *)
fun add_constr_case (ext_ctxt as {thy, ...}) res_T (j, x) res_t =
  Const (@{const_name If}, [bool_T, res_T, res_T] ---> res_T)
  $ discriminate_value ext_ctxt x (Bound 0) $ constr_case_body thy (j, x)
  $ res_t
(* extended_context -> typ -> typ -> term *)
fun optimized_case_def (ext_ctxt as {thy, ...}) dataT res_T =
  let
    val xs = datatype_constrs ext_ctxt dataT
    val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
    val (xs', x) = split_last xs
  in
    constr_case_body thy (1, x)
    |> fold_rev (add_constr_case ext_ctxt res_T) (length xs downto 2 ~~ xs')
    |> fold_rev (curry absdummy) (func_Ts @ [dataT])
  end

(* extended_context -> string -> typ -> typ -> term -> term *)
fun optimized_record_get (ext_ctxt as {thy, ...}) s rec_T res_T t =
  let val constr_x = the_single (datatype_constrs ext_ctxt rec_T) in
    case no_of_record_field thy s rec_T of
      ~1 => (case rec_T of
               Type (_, Ts as _ :: _) =>
               let
                 val rec_T' = List.last Ts
                 val j = num_record_fields thy rec_T - 1
               in
                 select_nth_constr_arg thy constr_x t j res_T
                 |> optimized_record_get ext_ctxt s rec_T' res_T
               end
             | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
                                []))
    | j => select_nth_constr_arg thy constr_x t j res_T
  end
(* extended_context -> string -> typ -> term -> term -> term *)
fun optimized_record_update (ext_ctxt as {thy, ...}) s rec_T fun_t rec_t =
  let
    val constr_x as (_, constr_T) = the_single (datatype_constrs ext_ctxt rec_T)
    val Ts = binder_types constr_T
    val n = length Ts
    val special_j = no_of_record_field thy s rec_T
    val ts = map2 (fn j => fn T =>
                      let
                        val t = select_nth_constr_arg thy constr_x rec_t j T
                      in
                        if j = special_j then
                          betapply (fun_t, t)
                        else if j = n - 1 andalso special_j = ~1 then
                          optimized_record_update ext_ctxt s
                              (rec_T |> dest_Type |> snd |> List.last) fun_t t
                        else
                          t
                      end) (index_seq 0 n) Ts
  in list_comb (Const constr_x, ts) end

(* Constants "c" whose definition is of the form "c == c'", where "c'" is also a
   constant, are said to be trivial. For those, we ignore the simplification
   rules and use the definition instead, to ensure that built-in symbols like
   "ord_nat_inst.less_eq_nat" are picked up correctly. *)
(* theory -> const_table -> styp -> bool *)
fun has_trivial_definition thy table x =
  case def_of_const thy table x of SOME (Const _) => true | _ => false

(* theory -> const_table -> string * typ -> fixpoint_kind *)
fun fixpoint_kind_of_const thy table x =