src/HOL/Tools/Nitpick/nitpick_hol.ML
author blanchet
Mon Feb 28 17:53:10 2011 +0100 (2011-02-28)
changeset 41859 c3a5912d0922
parent 41803 ef13e3b7cbaf
child 41860 49d0fc8c418c
permissions -rw-r--r--
made "fixed_is_special_eligible_arg" smarter w.r.t. pairs, and fixed previous unintended behavior because "andalso" ties more tightly than "orelse"
     1 (*  Title:      HOL/Tools/Nitpick/nitpick_hol.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2008, 2009, 2010
     4 
     5 Auxiliary HOL-related functions used by Nitpick.
     6 *)
     7 
     8 signature NITPICK_HOL =
     9 sig
    10   type styp = Nitpick_Util.styp
    11   type const_table = term list Symtab.table
    12   type special_fun = (styp * int list * term list) * styp
    13   type unrolled = styp * styp
    14   type wf_cache = (styp * (bool * bool)) list
    15 
    16   type hol_context =
    17     {thy: theory,
    18      ctxt: Proof.context,
    19      max_bisim_depth: int,
    20      boxes: (typ option * bool option) list,
    21      stds: (typ option * bool) list,
    22      wfs: (styp option * bool option) list,
    23      user_axioms: bool option,
    24      debug: bool,
    25      whacks: term list,
    26      binary_ints: bool option,
    27      destroy_constrs: bool,
    28      specialize: bool,
    29      star_linear_preds: bool,
    30      preconstrs: (term option * bool option) list,
    31      tac_timeout: Time.time option,
    32      evals: term list,
    33      case_names: (string * int) list,
    34      def_tables: const_table * const_table,
    35      nondef_table: const_table,
    36      user_nondefs: term list,
    37      simp_table: const_table Unsynchronized.ref,
    38      psimp_table: const_table,
    39      choice_spec_table: const_table,
    40      intro_table: const_table,
    41      ground_thm_table: term list Inttab.table,
    42      ersatz_table: (string * string) list,
    43      skolems: (string * string list) list Unsynchronized.ref,
    44      special_funs: special_fun list Unsynchronized.ref,
    45      unrolled_preds: unrolled list Unsynchronized.ref,
    46      wf_cache: wf_cache Unsynchronized.ref,
    47      constr_cache: (typ * styp list) list Unsynchronized.ref}
    48 
    49   datatype fixpoint_kind = Lfp | Gfp | NoFp
    50   datatype boxability =
    51     InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
    52 
    53   val name_sep : string
    54   val numeral_prefix : string
    55   val base_prefix : string
    56   val step_prefix : string
    57   val unrolled_prefix : string
    58   val ubfp_prefix : string
    59   val lbfp_prefix : string
    60   val quot_normal_prefix : string
    61   val skolem_prefix : string
    62   val special_prefix : string
    63   val uncurry_prefix : string
    64   val eval_prefix : string
    65   val iter_var_prefix : string
    66   val strip_first_name_sep : string -> string * string
    67   val original_name : string -> string
    68   val abs_var : indexname * typ -> term -> term
    69   val is_higher_order_type : typ -> bool
    70   val is_special_eligible_arg : bool -> typ list -> term -> bool
    71   val s_let :
    72     typ list -> string -> int -> typ -> typ -> (term -> term) -> term -> term
    73   val s_betapply : typ list -> term * term -> term
    74   val s_betapplys : typ list -> term * term list -> term
    75   val s_conj : term * term -> term
    76   val s_disj : term * term -> term
    77   val strip_any_connective : term -> term list * term
    78   val conjuncts_of : term -> term list
    79   val disjuncts_of : term -> term list
    80   val unarize_unbox_etc_type : typ -> typ
    81   val uniterize_unarize_unbox_etc_type : typ -> typ
    82   val string_for_type : Proof.context -> typ -> string
    83   val pretty_for_type : Proof.context -> typ -> Pretty.T
    84   val prefix_name : string -> string -> string
    85   val shortest_name : string -> string
    86   val short_name : string -> string
    87   val shorten_names_in_term : term -> term
    88   val strict_type_match : theory -> typ * typ -> bool
    89   val type_match : theory -> typ * typ -> bool
    90   val const_match : theory -> styp * styp -> bool
    91   val term_match : theory -> term * term -> bool
    92   val frac_from_term_pair : typ -> term -> term -> term
    93   val is_TFree : typ -> bool
    94   val is_fun_type : typ -> bool
    95   val is_set_type : typ -> bool
    96   val is_pair_type : typ -> bool
    97   val is_lfp_iterator_type : typ -> bool
    98   val is_gfp_iterator_type : typ -> bool
    99   val is_fp_iterator_type : typ -> bool
   100   val is_iterator_type : typ -> bool
   101   val is_boolean_type : typ -> bool
   102   val is_integer_type : typ -> bool
   103   val is_bit_type : typ -> bool
   104   val is_word_type : typ -> bool
   105   val is_integer_like_type : typ -> bool
   106   val is_record_type : typ -> bool
   107   val is_number_type : Proof.context -> typ -> bool
   108   val const_for_iterator_type : typ -> styp
   109   val strip_n_binders : int -> typ -> typ list * typ
   110   val nth_range_type : int -> typ -> typ
   111   val num_factors_in_type : typ -> int
   112   val num_binder_types : typ -> int
   113   val curried_binder_types : typ -> typ list
   114   val mk_flat_tuple : typ -> term list -> term
   115   val dest_n_tuple : int -> term -> term list
   116   val is_real_datatype : theory -> string -> bool
   117   val is_standard_datatype : theory -> (typ option * bool) list -> typ -> bool
   118   val is_codatatype : Proof.context -> typ -> bool
   119   val is_quot_type : Proof.context -> typ -> bool
   120   val is_pure_typedef : Proof.context -> typ -> bool
   121   val is_univ_typedef : Proof.context -> typ -> bool
   122   val is_datatype : Proof.context -> (typ option * bool) list -> typ -> bool
   123   val is_record_constr : styp -> bool
   124   val is_record_get : theory -> styp -> bool
   125   val is_record_update : theory -> styp -> bool
   126   val is_abs_fun : Proof.context -> styp -> bool
   127   val is_rep_fun : Proof.context -> styp -> bool
   128   val is_quot_abs_fun : Proof.context -> styp -> bool
   129   val is_quot_rep_fun : Proof.context -> styp -> bool
   130   val mate_of_rep_fun : Proof.context -> styp -> styp
   131   val is_constr_like : Proof.context -> styp -> bool
   132   val is_constr : Proof.context -> (typ option * bool) list -> styp -> bool
   133   val is_sel : string -> bool
   134   val is_sel_like_and_no_discr : string -> bool
   135   val box_type : hol_context -> boxability -> typ -> typ
   136   val binarize_nat_and_int_in_type : typ -> typ
   137   val binarize_nat_and_int_in_term : term -> term
   138   val discr_for_constr : styp -> styp
   139   val num_sels_for_constr_type : typ -> int
   140   val nth_sel_name_for_constr_name : string -> int -> string
   141   val nth_sel_for_constr : styp -> int -> styp
   142   val binarized_and_boxed_nth_sel_for_constr :
   143     hol_context -> bool -> styp -> int -> styp
   144   val sel_no_from_name : string -> int
   145   val close_form : term -> term
   146   val distinctness_formula : typ -> term list -> term
   147   val register_frac_type :
   148     string -> (string * string) list -> morphism -> Context.generic
   149     -> Context.generic
   150   val register_frac_type_global :
   151     string -> (string * string) list -> theory -> theory
   152   val unregister_frac_type :
   153     string -> morphism -> Context.generic -> Context.generic
   154   val unregister_frac_type_global : string -> theory -> theory
   155   val register_codatatype :
   156     typ -> string -> styp list -> morphism -> Context.generic -> Context.generic
   157   val register_codatatype_global :
   158     typ -> string -> styp list -> theory -> theory
   159   val unregister_codatatype :
   160     typ -> morphism -> Context.generic -> Context.generic
   161   val unregister_codatatype_global : typ -> theory -> theory
   162   val datatype_constrs : hol_context -> typ -> styp list
   163   val binarized_and_boxed_datatype_constrs :
   164     hol_context -> bool -> typ -> styp list
   165   val num_datatype_constrs : hol_context -> typ -> int
   166   val constr_name_for_sel_like : string -> string
   167   val binarized_and_boxed_constr_for_sel : hol_context -> bool -> styp -> styp
   168   val discriminate_value : hol_context -> styp -> term -> term
   169   val select_nth_constr_arg :
   170     Proof.context -> (typ option * bool) list -> styp -> term -> int -> typ
   171     -> term
   172   val construct_value :
   173     Proof.context -> (typ option * bool) list -> styp -> term list -> term
   174   val coerce_term : hol_context -> typ list -> typ -> typ -> term -> term
   175   val card_of_type : (typ * int) list -> typ -> int
   176   val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
   177   val bounded_exact_card_of_type :
   178     hol_context -> typ list -> int -> int -> (typ * int) list -> typ -> int
   179   val is_finite_type : hol_context -> typ -> bool
   180   val is_small_finite_type : hol_context -> typ -> bool
   181   val special_bounds : term list -> (indexname * typ) list
   182   val is_funky_typedef : Proof.context -> typ -> bool
   183   val all_axioms_of :
   184     Proof.context -> (term * term) list -> term list * term list * term list
   185   val arity_of_built_in_const :
   186     theory -> (typ option * bool) list -> styp -> int option
   187   val is_built_in_const :
   188     theory -> (typ option * bool) list -> styp -> bool
   189   val term_under_def : term -> term
   190   val case_const_names :
   191     Proof.context -> (typ option * bool) list -> (string * int) list
   192   val unfold_defs_in_term : hol_context -> term -> term
   193   val const_def_tables :
   194     Proof.context -> (term * term) list -> term list
   195     -> const_table * const_table
   196   val const_nondef_table : term list -> const_table
   197   val const_simp_table : Proof.context -> (term * term) list -> const_table
   198   val const_psimp_table : Proof.context -> (term * term) list -> const_table
   199   val const_choice_spec_table :
   200     Proof.context -> (term * term) list -> const_table
   201   val inductive_intro_table :
   202     Proof.context -> (term * term) list -> const_table * const_table
   203     -> const_table
   204   val ground_theorem_table : theory -> term list Inttab.table
   205   val ersatz_table : Proof.context -> (string * string) list
   206   val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit
   207   val inverse_axioms_for_rep_fun : Proof.context -> styp -> term list
   208   val optimized_typedef_axioms : Proof.context -> string * typ list -> term list
   209   val optimized_quot_type_axioms :
   210     Proof.context -> (typ option * bool) list -> string * typ list -> term list
   211   val def_of_const : theory -> const_table * const_table -> styp -> term option
   212   val fixpoint_kind_of_rhs : term -> fixpoint_kind
   213   val fixpoint_kind_of_const :
   214     theory -> const_table * const_table -> string * typ -> fixpoint_kind
   215   val is_real_inductive_pred : hol_context -> styp -> bool
   216   val is_constr_pattern_lhs : Proof.context -> term -> bool
   217   val is_constr_pattern_formula : Proof.context -> term -> bool
   218   val nondef_props_for_const :
   219     theory -> bool -> const_table -> styp -> term list
   220   val is_choice_spec_fun : hol_context -> styp -> bool
   221   val is_choice_spec_axiom : theory -> const_table -> term -> bool
   222   val is_real_equational_fun : hol_context -> styp -> bool
   223   val is_equational_fun_but_no_plain_def : hol_context -> styp -> bool
   224   val codatatype_bisim_axioms : hol_context -> typ -> term list
   225   val is_well_founded_inductive_pred : hol_context -> styp -> bool
   226   val unrolled_inductive_pred_const : hol_context -> bool -> styp -> term
   227   val equational_fun_axioms : hol_context -> styp -> term list
   228   val is_equational_fun_surely_complete : hol_context -> styp -> bool
   229   val merged_type_var_table_for_terms :
   230     theory -> term list -> (sort * string) list
   231   val merge_type_vars_in_term :
   232     theory -> bool -> (sort * string) list -> term -> term
   233   val ground_types_in_type : hol_context -> bool -> typ -> typ list
   234   val ground_types_in_terms : hol_context -> bool -> term list -> typ list
   235 end;
   236 
   237 structure Nitpick_HOL : NITPICK_HOL =
   238 struct
   239 
   240 open Nitpick_Util
   241 
   242 type const_table = term list Symtab.table
   243 type special_fun = (styp * int list * term list) * styp
   244 type unrolled = styp * styp
   245 type wf_cache = (styp * (bool * bool)) list
   246 
   247 type hol_context =
   248   {thy: theory,
   249    ctxt: Proof.context,
   250    max_bisim_depth: int,
   251    boxes: (typ option * bool option) list,
   252    stds: (typ option * bool) list,
   253    wfs: (styp option * bool option) list,
   254    user_axioms: bool option,
   255    debug: bool,
   256    whacks: term list,
   257    binary_ints: bool option,
   258    destroy_constrs: bool,
   259    specialize: bool,
   260    star_linear_preds: bool,
   261    preconstrs: (term option * bool option) list,
   262    tac_timeout: Time.time option,
   263    evals: term list,
   264    case_names: (string * int) list,
   265    def_tables: const_table * const_table,
   266    nondef_table: const_table,
   267    user_nondefs: term list,
   268    simp_table: const_table Unsynchronized.ref,
   269    psimp_table: const_table,
   270    choice_spec_table: const_table,
   271    intro_table: const_table,
   272    ground_thm_table: term list Inttab.table,
   273    ersatz_table: (string * string) list,
   274    skolems: (string * string list) list Unsynchronized.ref,
   275    special_funs: special_fun list Unsynchronized.ref,
   276    unrolled_preds: unrolled list Unsynchronized.ref,
   277    wf_cache: wf_cache Unsynchronized.ref,
   278    constr_cache: (typ * styp list) list Unsynchronized.ref}
   279 
   280 datatype fixpoint_kind = Lfp | Gfp | NoFp
   281 datatype boxability =
   282   InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
   283 
   284 structure Data = Generic_Data
   285 (
   286   type T = {frac_types: (string * (string * string) list) list,
   287             codatatypes: (string * (string * styp list)) list}
   288   val empty = {frac_types = [], codatatypes = []}
   289   val extend = I
   290   fun merge ({frac_types = fs1, codatatypes = cs1},
   291              {frac_types = fs2, codatatypes = cs2}) : T =
   292     {frac_types = AList.merge (op =) (K true) (fs1, fs2),
   293      codatatypes = AList.merge (op =) (K true) (cs1, cs2)}
   294 )
   295 
   296 val name_sep = "$"
   297 val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep
   298 val sel_prefix = nitpick_prefix ^ "sel"
   299 val discr_prefix = nitpick_prefix ^ "is" ^ name_sep
   300 val set_prefix = nitpick_prefix ^ "set" ^ name_sep
   301 val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep
   302 val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep
   303 val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep
   304 val base_prefix = nitpick_prefix ^ "base" ^ name_sep
   305 val step_prefix = nitpick_prefix ^ "step" ^ name_sep
   306 val ubfp_prefix = nitpick_prefix ^ "ubfp" ^ name_sep
   307 val lbfp_prefix = nitpick_prefix ^ "lbfp" ^ name_sep
   308 val quot_normal_prefix = nitpick_prefix ^ "qn" ^ name_sep
   309 val skolem_prefix = nitpick_prefix ^ "sk"
   310 val special_prefix = nitpick_prefix ^ "sp"
   311 val uncurry_prefix = nitpick_prefix ^ "unc"
   312 val eval_prefix = nitpick_prefix ^ "eval"
   313 val iter_var_prefix = "i"
   314 
   315 (** Constant/type information and term/type manipulation **)
   316 
   317 fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep
   318 fun quot_normal_name_for_type ctxt T =
   319   quot_normal_prefix ^ unyxml (Syntax.string_of_typ ctxt T)
   320 
   321 val strip_first_name_sep =
   322   Substring.full #> Substring.position name_sep ##> Substring.triml 1
   323   #> pairself Substring.string
   324 fun original_name s =
   325   if String.isPrefix nitpick_prefix s then
   326     case strip_first_name_sep s of (s1, "") => s1 | (_, s2) => original_name s2
   327   else
   328     s
   329 
   330 val evil_nix = 0
   331 val evil_prod = 1
   332 val evil_fun = 2
   333 
   334 (* Returns an approximation of how evil a type is (i.e., how much are we willing
   335    to try to specialize the argument even if it contains bound variables). *)
   336 fun type_evil (Type (@{type_name fun}, _)) = evil_fun
   337   | type_evil (Type (s, Ts)) =
   338     (if s = @{type_name prod} then evil_prod else evil_nix)
   339     |> fold (Integer.max o type_evil) Ts
   340   | type_evil _ = evil_nix
   341 
   342 fun is_higher_order_type T = (type_evil T = evil_fun)
   343 
   344 fun is_special_eligible_arg strict Ts t =
   345   case map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) of
   346     [] => true
   347   | bad_Ts =>
   348     case type_evil (fastype_of1 (Ts, t)) of
   349       0 => false
   350     | T_evil =>
   351       let val bad_Ts_evil = fold (Integer.max o type_evil) bad_Ts evil_nix in
   352         (bad_Ts_evil, T_evil) |> (if strict then op < else op <=)
   353       end
   354 
   355 fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
   356 
   357 fun let_var s = (nitpick_prefix ^ s, 999)
   358 val let_inline_threshold = 20
   359 
   360 fun s_let Ts s n abs_T body_T f t =
   361   if (n - 1) * (size_of_term t - 1) <= let_inline_threshold orelse
   362      is_special_eligible_arg false Ts t then
   363     f t
   364   else
   365     let val z = (let_var s, abs_T) in
   366       Const (@{const_name Let}, abs_T --> (abs_T --> body_T) --> body_T)
   367       $ t $ abs_var z (incr_boundvars 1 (f (Var z)))
   368     end
   369 
   370 fun loose_bvar1_count (Bound i, k) = if i = k then 1 else 0
   371   | loose_bvar1_count (t1 $ t2, k) =
   372     loose_bvar1_count (t1, k) + loose_bvar1_count (t2, k)
   373   | loose_bvar1_count (Abs (_, _, t), k) = loose_bvar1_count (t, k + 1)
   374   | loose_bvar1_count _ = 0
   375 
   376 fun s_betapply _ (Const (@{const_name If}, _) $ @{const True} $ t1', _) = t1'
   377   | s_betapply _ (Const (@{const_name If}, _) $ @{const False} $ _, t2) = t2
   378   | s_betapply Ts (Const (@{const_name Let},
   379                           Type (_, [bound_T, Type (_, [_, body_T])]))
   380                    $ t12 $ Abs (s, T, t13'), t2) =
   381     let val body_T' = range_type body_T in
   382       Const (@{const_name Let}, bound_T --> (bound_T --> body_T') --> body_T')
   383       $ t12 $ Abs (s, T, s_betapply (T :: Ts) (t13', incr_boundvars 1 t2))
   384     end
   385   | s_betapply Ts (t1 as Abs (s1, T1, t1'), t2) =
   386     (s_let Ts s1 (loose_bvar1_count (t1', 0)) T1 (fastype_of1 (T1 :: Ts, t1'))
   387               (curry betapply t1) t2
   388      handle TERM _ => betapply (t1, t2)) (* FIXME: fix all uses *)
   389   | s_betapply _ (t1, t2) = t1 $ t2
   390 fun s_betapplys Ts = Library.foldl (s_betapply Ts)
   391 
   392 fun s_beta_norm Ts t =
   393   let
   394     fun aux _ (Var _) = raise Same.SAME
   395       | aux Ts (Abs (s, T, t')) = Abs (s, T, aux (T :: Ts) t')
   396       | aux Ts ((t1 as Abs _) $ t2) =
   397         Same.commit (aux Ts) (s_betapply Ts (t1, t2))
   398       | aux Ts (t1 $ t2) =
   399         ((case aux Ts t1 of
   400            t1 as Abs _ => Same.commit (aux Ts) (s_betapply Ts (t1, t2))
   401          | t1 => t1 $ Same.commit (aux Ts) t2)
   402         handle Same.SAME => t1 $ aux Ts t2)
   403       | aux _ _ = raise Same.SAME
   404   in aux Ts t handle Same.SAME => t end
   405 
   406 fun s_conj (t1, @{const True}) = t1
   407   | s_conj (@{const True}, t2) = t2
   408   | s_conj (t1, t2) =
   409     if t1 = @{const False} orelse t2 = @{const False} then @{const False}
   410     else HOLogic.mk_conj (t1, t2)
   411 fun s_disj (t1, @{const False}) = t1
   412   | s_disj (@{const False}, t2) = t2
   413   | s_disj (t1, t2) =
   414     if t1 = @{const True} orelse t2 = @{const True} then @{const True}
   415     else HOLogic.mk_disj (t1, t2)
   416 
   417 fun strip_connective conn_t (t as (t0 $ t1 $ t2)) =
   418     if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t]
   419   | strip_connective _ t = [t]
   420 fun strip_any_connective (t as (t0 $ _ $ _)) =
   421     if t0 = @{const HOL.conj} orelse t0 = @{const HOL.disj} then
   422       (strip_connective t0 t, t0)
   423     else
   424       ([t], @{const Not})
   425   | strip_any_connective t = ([t], @{const Not})
   426 val conjuncts_of = strip_connective @{const HOL.conj}
   427 val disjuncts_of = strip_connective @{const HOL.disj}
   428 
   429 (* When you add constants to these lists, make sure to handle them in
   430    "Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
   431    well. *)
   432 val built_in_consts =
   433   [(@{const_name all}, 1),
   434    (@{const_name "=="}, 2),
   435    (@{const_name "==>"}, 2),
   436    (@{const_name Pure.conjunction}, 2),
   437    (@{const_name Trueprop}, 1),
   438    (@{const_name Not}, 1),
   439    (@{const_name False}, 0),
   440    (@{const_name True}, 0),
   441    (@{const_name All}, 1),
   442    (@{const_name Ex}, 1),
   443    (@{const_name HOL.eq}, 1),
   444    (@{const_name HOL.conj}, 2),
   445    (@{const_name HOL.disj}, 2),
   446    (@{const_name HOL.implies}, 2),
   447    (@{const_name If}, 3),
   448    (@{const_name Let}, 2),
   449    (@{const_name Pair}, 2),
   450    (@{const_name fst}, 1),
   451    (@{const_name snd}, 1),
   452    (@{const_name Id}, 0),
   453    (@{const_name converse}, 1),
   454    (@{const_name trancl}, 1),
   455    (@{const_name rel_comp}, 2),
   456    (@{const_name finite}, 1),
   457    (@{const_name unknown}, 0),
   458    (@{const_name is_unknown}, 1),
   459    (@{const_name safe_The}, 1),
   460    (@{const_name Frac}, 0),
   461    (@{const_name norm_frac}, 0)]
   462 val built_in_nat_consts =
   463   [(@{const_name Suc}, 0),
   464    (@{const_name nat}, 0),
   465    (@{const_name nat_gcd}, 0),
   466    (@{const_name nat_lcm}, 0)]
   467 val built_in_typed_consts =
   468   [((@{const_name zero_class.zero}, int_T), 0),
   469    ((@{const_name one_class.one}, int_T), 0),
   470    ((@{const_name plus_class.plus}, int_T --> int_T --> int_T), 0),
   471    ((@{const_name minus_class.minus}, int_T --> int_T --> int_T), 0),
   472    ((@{const_name times_class.times}, int_T --> int_T --> int_T), 0),
   473    ((@{const_name div_class.div}, int_T --> int_T --> int_T), 0),
   474    ((@{const_name uminus_class.uminus}, int_T --> int_T), 0),
   475    ((@{const_name ord_class.less}, int_T --> int_T --> bool_T), 2),
   476    ((@{const_name ord_class.less_eq}, int_T --> int_T --> bool_T), 2)]
   477 val built_in_typed_nat_consts =
   478   [((@{const_name zero_class.zero}, nat_T), 0),
   479    ((@{const_name one_class.one}, nat_T), 0),
   480    ((@{const_name plus_class.plus}, nat_T --> nat_T --> nat_T), 0),
   481    ((@{const_name minus_class.minus}, nat_T --> nat_T --> nat_T), 0),
   482    ((@{const_name times_class.times}, nat_T --> nat_T --> nat_T), 0),
   483    ((@{const_name div_class.div}, nat_T --> nat_T --> nat_T), 0),
   484    ((@{const_name ord_class.less}, nat_T --> nat_T --> bool_T), 2),
   485    ((@{const_name ord_class.less_eq}, nat_T --> nat_T --> bool_T), 2),
   486    ((@{const_name of_nat}, nat_T --> int_T), 0)]
   487 val built_in_set_consts =
   488   [(@{const_name ord_class.less_eq}, 2)]
   489 
   490 fun unarize_type @{typ "unsigned_bit word"} = nat_T
   491   | unarize_type @{typ "signed_bit word"} = int_T
   492   | unarize_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_type Ts)
   493   | unarize_type T = T
   494 fun unarize_unbox_etc_type (Type (@{type_name fun_box}, Ts)) =
   495     unarize_unbox_etc_type (Type (@{type_name fun}, Ts))
   496   | unarize_unbox_etc_type (Type (@{type_name pair_box}, Ts)) =
   497     Type (@{type_name prod}, map unarize_unbox_etc_type Ts)
   498   | unarize_unbox_etc_type @{typ "unsigned_bit word"} = nat_T
   499   | unarize_unbox_etc_type @{typ "signed_bit word"} = int_T
   500   | unarize_unbox_etc_type (Type (s, Ts as _ :: _)) =
   501     Type (s, map unarize_unbox_etc_type Ts)
   502   | unarize_unbox_etc_type T = T
   503 fun uniterize_type (Type (s, Ts as _ :: _)) = Type (s, map uniterize_type Ts)
   504   | uniterize_type @{typ bisim_iterator} = nat_T
   505   | uniterize_type T = T
   506 val uniterize_unarize_unbox_etc_type = uniterize_type o unarize_unbox_etc_type
   507 
   508 fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_unbox_etc_type
   509 fun pretty_for_type ctxt = Syntax.pretty_typ ctxt o unarize_unbox_etc_type
   510 
   511 val prefix_name = Long_Name.qualify o Long_Name.base_name
   512 fun shortest_name s = List.last (space_explode "." s) handle List.Empty => ""
   513 val prefix_abs_vars = Term.map_abs_vars o prefix_name
   514 fun short_name s =
   515   case space_explode name_sep s of
   516     [_] => s |> String.isPrefix nitpick_prefix s ? unprefix nitpick_prefix
   517   | ss => map shortest_name ss |> space_implode "_"
   518 fun shorten_names_in_type (Type (s, Ts)) =
   519     Type (short_name s, map shorten_names_in_type Ts)
   520   | shorten_names_in_type T = T
   521 val shorten_names_in_term =
   522   map_aterms (fn Const (s, T) => Const (short_name s, T) | t => t)
   523   #> map_types shorten_names_in_type
   524 
   525 fun strict_type_match thy (T1, T2) =
   526   (Sign.typ_match thy (T2, T1) Vartab.empty; true)
   527   handle Type.TYPE_MATCH => false
   528 fun type_match thy = strict_type_match thy o pairself unarize_unbox_etc_type
   529 fun const_match thy ((s1, T1), (s2, T2)) =
   530   s1 = s2 andalso type_match thy (T1, T2)
   531 fun term_match thy (Const x1, Const x2) = const_match thy (x1, x2)
   532   | term_match thy (Free (s1, T1), Free (s2, T2)) =
   533     const_match thy ((shortest_name s1, T1), (shortest_name s2, T2))
   534   | term_match _ (t1, t2) = t1 aconv t2
   535 
   536 fun frac_from_term_pair T t1 t2 =
   537   case snd (HOLogic.dest_number t1) of
   538     0 => HOLogic.mk_number T 0
   539   | n1 => case snd (HOLogic.dest_number t2) of
   540             1 => HOLogic.mk_number T n1
   541           | n2 => Const (@{const_name divide}, T --> T --> T)
   542                   $ HOLogic.mk_number T n1 $ HOLogic.mk_number T n2
   543 
   544 fun is_TFree (TFree _) = true
   545   | is_TFree _ = false
   546 fun is_fun_type (Type (@{type_name fun}, _)) = true
   547   | is_fun_type _ = false
   548 fun is_set_type (Type (@{type_name fun}, [_, @{typ bool}])) = true
   549   | is_set_type _ = false
   550 fun is_pair_type (Type (@{type_name prod}, _)) = true
   551   | is_pair_type _ = false
   552 fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s
   553   | is_lfp_iterator_type _ = false
   554 fun is_gfp_iterator_type (Type (s, _)) = String.isPrefix gfp_iterator_prefix s
   555   | is_gfp_iterator_type _ = false
   556 val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type
   557 fun is_iterator_type T =
   558   (T = @{typ bisim_iterator} orelse is_fp_iterator_type T)
   559 fun is_boolean_type T = (T = prop_T orelse T = bool_T)
   560 fun is_integer_type T = (T = nat_T orelse T = int_T)
   561 fun is_bit_type T = (T = @{typ unsigned_bit} orelse T = @{typ signed_bit})
   562 fun is_word_type (Type (@{type_name word}, _)) = true
   563   | is_word_type _ = false
   564 val is_integer_like_type = is_iterator_type orf is_integer_type orf is_word_type
   565 val is_record_type = not o null o Record.dest_recTs
   566 fun is_frac_type ctxt (Type (s, [])) =
   567     s |> AList.lookup (op =) (#frac_types (Data.get (Context.Proof ctxt)))
   568       |> these |> null |> not
   569   | is_frac_type _ _ = false
   570 fun is_number_type ctxt = is_integer_like_type orf is_frac_type ctxt
   571 
   572 fun iterator_type_for_const gfp (s, T) =
   573   Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s,
   574         binder_types T)
   575 fun const_for_iterator_type (Type (s, Ts)) =
   576     (strip_first_name_sep s |> snd, Ts ---> bool_T)
   577   | const_for_iterator_type T =
   578     raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], [])
   579 
   580 fun strip_n_binders 0 T = ([], T)
   581   | strip_n_binders n (Type (@{type_name fun}, [T1, T2])) =
   582     strip_n_binders (n - 1) T2 |>> cons T1
   583   | strip_n_binders n (Type (@{type_name fun_box}, Ts)) =
   584     strip_n_binders n (Type (@{type_name fun}, Ts))
   585   | strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], [])
   586 val nth_range_type = snd oo strip_n_binders
   587 
   588 fun num_factors_in_type (Type (@{type_name prod}, [T1, T2])) =
   589     fold (Integer.add o num_factors_in_type) [T1, T2] 0
   590   | num_factors_in_type _ = 1
   591 fun num_binder_types (Type (@{type_name fun}, [_, T2])) =
   592     1 + num_binder_types T2
   593   | num_binder_types _ = 0
   594 val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types
   595 fun maybe_curried_binder_types T =
   596   (if is_pair_type (body_type T) then binder_types else curried_binder_types) T
   597 
   598 fun mk_flat_tuple _ [t] = t
   599   | mk_flat_tuple (Type (@{type_name prod}, [T1, T2])) (t :: ts) =
   600     HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts)
   601   | mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts)
   602 fun dest_n_tuple 1 t = [t]
   603   | dest_n_tuple n t = HOLogic.dest_prod t ||> dest_n_tuple (n - 1) |> op ::
   604 
   605 type typedef_info =
   606   {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
   607    set_def: thm option, prop_of_Rep: thm, set_name: string,
   608    Abs_inverse: thm option, Rep_inverse: thm option}
   609 
   610 fun typedef_info ctxt s =
   611   if is_frac_type ctxt (Type (s, [])) then
   612     SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
   613           Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
   614           set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
   615                           |> Logic.varify_global,
   616           set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
   617   else case Typedef.get_info ctxt s of
   618     (* When several entries are returned, it shouldn't matter much which one
   619        we take (according to Florian Haftmann). *)
   620     (* The "Logic.varifyT_global" calls are a temporary hack because these
   621        types's type variables sometimes clash with locally fixed type variables.
   622        Remove these calls once "Typedef" is fully localized. *)
   623     ({abs_type, rep_type, Abs_name, Rep_name, ...},
   624      {set_def, Rep, Abs_inverse, Rep_inverse, ...}) :: _ =>
   625     SOME {abs_type = Logic.varifyT_global abs_type,
   626           rep_type = Logic.varifyT_global rep_type, Abs_name = Abs_name,
   627           Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
   628           set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
   629           Rep_inverse = SOME Rep_inverse}
   630   | _ => NONE
   631 
   632 val is_typedef = is_some oo typedef_info
   633 val is_real_datatype = is_some oo Datatype.get_info
   634 fun is_standard_datatype thy = the oo triple_lookup (type_match thy)
   635 
   636 (* FIXME: Use antiquotation for "code_numeral" below or detect "rep_datatype",
   637    e.g., by adding a field to "Datatype_Aux.info". *)
   638 fun is_basic_datatype thy stds s =
   639   member (op =) [@{type_name prod}, @{type_name bool}, @{type_name int},
   640                  "Code_Numeral.code_numeral"] s orelse
   641   (s = @{type_name nat} andalso is_standard_datatype thy stds nat_T)
   642 
   643 (* TODO: use "Term_Subst.instantiateT" instead? *)
   644 fun instantiate_type thy T1 T1' T2 =
   645   Same.commit (Envir.subst_type_same
   646                    (Sign.typ_match thy (T1, T1') Vartab.empty)) T2
   647   handle Type.TYPE_MATCH =>
   648          raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], [])
   649 fun varify_and_instantiate_type ctxt T1 T1' T2 =
   650   let val thy = ProofContext.theory_of ctxt in
   651     instantiate_type thy (varify_type ctxt T1) T1' (varify_type ctxt T2)
   652   end
   653 
   654 fun repair_constr_type ctxt body_T' T =
   655   varify_and_instantiate_type ctxt (body_type T) body_T' T
   656 
   657 fun register_frac_type_generic frac_s ersaetze generic =
   658   let
   659     val {frac_types, codatatypes} = Data.get generic
   660     val frac_types = AList.update (op =) (frac_s, ersaetze) frac_types
   661   in Data.put {frac_types = frac_types, codatatypes = codatatypes} generic end
   662 (* TODO: Consider morphism. *)
   663 fun register_frac_type frac_s ersaetze (_ : morphism) =
   664   register_frac_type_generic frac_s ersaetze
   665 val register_frac_type_global = Context.theory_map oo register_frac_type_generic
   666 
   667 fun unregister_frac_type_generic frac_s = register_frac_type_generic frac_s []
   668 (* TODO: Consider morphism. *)
   669 fun unregister_frac_type frac_s (_ : morphism) =
   670   unregister_frac_type_generic frac_s
   671 val unregister_frac_type_global =
   672   Context.theory_map o unregister_frac_type_generic
   673 
   674 fun register_codatatype_generic co_T case_name constr_xs generic =
   675   let
   676     val ctxt = Context.proof_of generic
   677     val thy = Context.theory_of generic
   678     val {frac_types, codatatypes} = Data.get generic
   679     val constr_xs = map (apsnd (repair_constr_type ctxt co_T)) constr_xs
   680     val (co_s, co_Ts) = dest_Type co_T
   681     val _ =
   682       if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) andalso
   683          co_s <> @{type_name fun} andalso
   684          not (is_basic_datatype thy [(NONE, true)] co_s) then
   685         ()
   686       else
   687         raise TYPE ("Nitpick_HOL.register_codatatype_generic", [co_T], [])
   688     val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs))
   689                                    codatatypes
   690   in Data.put {frac_types = frac_types, codatatypes = codatatypes} generic end
   691 (* TODO: Consider morphism. *)
   692 fun register_codatatype co_T case_name constr_xs (_ : morphism) =
   693   register_codatatype_generic co_T case_name constr_xs
   694 val register_codatatype_global =
   695   Context.theory_map ooo register_codatatype_generic
   696 
   697 fun unregister_codatatype_generic co_T = register_codatatype_generic co_T "" []
   698 (* TODO: Consider morphism. *)
   699 fun unregister_codatatype co_T (_ : morphism) =
   700   unregister_codatatype_generic co_T
   701 val unregister_codatatype_global =
   702   Context.theory_map o unregister_codatatype_generic
   703 
   704 fun is_codatatype ctxt (Type (s, _)) =
   705     s |> AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt)))
   706       |> Option.map snd |> these |> null |> not
   707   | is_codatatype _ _ = false
   708 fun is_real_quot_type thy (Type (s, _)) =
   709     is_some (Quotient_Info.quotdata_lookup_raw thy s)
   710   | is_real_quot_type _ _ = false
   711 fun is_quot_type ctxt T =
   712   let val thy = ProofContext.theory_of ctxt in
   713     is_real_quot_type thy T andalso not (is_codatatype ctxt T)
   714   end
   715 fun is_pure_typedef ctxt (T as Type (s, _)) =
   716     let val thy = ProofContext.theory_of ctxt in
   717       is_typedef ctxt s andalso
   718       not (is_real_datatype thy s orelse is_real_quot_type thy T orelse
   719            is_codatatype ctxt T orelse is_record_type T orelse
   720            is_integer_like_type T)
   721     end
   722   | is_pure_typedef _ _ = false
   723 fun is_univ_typedef ctxt (Type (s, _)) =
   724     (case typedef_info ctxt s of
   725        SOME {set_def, prop_of_Rep, ...} =>
   726        let
   727          val t_opt =
   728            case set_def of
   729              SOME thm => try (snd o Logic.dest_equals o prop_of) thm
   730            | NONE => try (snd o HOLogic.dest_mem o HOLogic.dest_Trueprop)
   731                          prop_of_Rep
   732        in
   733          case t_opt of
   734            SOME (Const (@{const_name top}, _)) => true
   735            (* "Multiset.multiset" *)
   736          | SOME (Const (@{const_name Collect}, _)
   737                  $ Abs (_, _, Const (@{const_name finite}, _) $ _)) => true
   738            (* "FinFun.finfun" *)
   739          | SOME (Const (@{const_name Collect}, _) $ Abs (_, _,
   740                      Const (@{const_name Ex}, _) $ Abs (_, _,
   741                          Const (@{const_name finite}, _) $ _))) => true
   742          | _ => false
   743        end
   744      | NONE => false)
   745   | is_univ_typedef _ _ = false
   746 fun is_datatype ctxt stds (T as Type (s, _)) =
   747     let val thy = ProofContext.theory_of ctxt in
   748       (is_typedef ctxt s orelse is_codatatype ctxt T orelse
   749        T = @{typ ind} orelse is_real_quot_type thy T) andalso
   750       not (is_basic_datatype thy stds s)
   751     end
   752   | is_datatype _ _ _ = false
   753 
   754 fun all_record_fields thy T =
   755   let val (recs, more) = Record.get_extT_fields thy T in
   756     recs @ more :: all_record_fields thy (snd more)
   757   end
   758   handle TYPE _ => []
   759 fun is_record_constr (s, T) =
   760   String.isSuffix Record.extN s andalso
   761   let val dataT = body_type T in
   762     is_record_type dataT andalso
   763     s = unsuffix Record.ext_typeN (fst (dest_Type dataT)) ^ Record.extN
   764   end
   765 val num_record_fields = Integer.add 1 o length o fst oo Record.get_extT_fields
   766 fun no_of_record_field thy s T1 =
   767   find_index (curry (op =) s o fst)
   768              (Record.get_extT_fields thy T1 ||> single |> op @)
   769 fun is_record_get thy (s, Type (@{type_name fun}, [T1, _])) =
   770     exists (curry (op =) s o fst) (all_record_fields thy T1)
   771   | is_record_get _ _ = false
   772 fun is_record_update thy (s, T) =
   773   String.isSuffix Record.updateN s andalso
   774   exists (curry (op =) (unsuffix Record.updateN s) o fst)
   775          (all_record_fields thy (body_type T))
   776   handle TYPE _ => false
   777 fun is_abs_fun ctxt (s, Type (@{type_name fun}, [_, Type (s', _)])) =
   778     (case typedef_info ctxt s' of
   779        SOME {Abs_name, ...} => s = Abs_name
   780      | NONE => false)
   781   | is_abs_fun _ _ = false
   782 fun is_rep_fun ctxt (s, Type (@{type_name fun}, [Type (s', _), _])) =
   783     (case typedef_info ctxt s' of
   784        SOME {Rep_name, ...} => s = Rep_name
   785      | NONE => false)
   786   | is_rep_fun _ _ = false
   787 fun is_quot_abs_fun ctxt (x as (_, Type (@{type_name fun},
   788                                          [_, abs_T as Type (s', _)]))) =
   789     try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s'
   790     = SOME (Const x) andalso not (is_codatatype ctxt abs_T)
   791   | is_quot_abs_fun _ _ = false
   792 fun is_quot_rep_fun ctxt (x as (_, Type (@{type_name fun},
   793                                          [abs_T as Type (s', _), _]))) =
   794     try (Quotient_Term.absrep_const_chk Quotient_Term.RepF ctxt) s'
   795     = SOME (Const x) andalso not (is_codatatype ctxt abs_T)
   796   | is_quot_rep_fun _ _ = false
   797 
   798 fun mate_of_rep_fun ctxt (x as (_, Type (@{type_name fun},
   799                                          [T1 as Type (s', _), T2]))) =
   800     (case typedef_info ctxt s' of
   801        SOME {Abs_name, ...} => (Abs_name, Type (@{type_name fun}, [T2, T1]))
   802      | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
   803   | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
   804 fun rep_type_for_quot_type thy (T as Type (s, _)) =
   805     let val {qtyp, rtyp, ...} = Quotient_Info.quotdata_lookup thy s in
   806       instantiate_type thy qtyp T rtyp
   807     end
   808   | rep_type_for_quot_type _ T =
   809     raise TYPE ("Nitpick_HOL.rep_type_for_quot_type", [T], [])
   810 fun equiv_relation_for_quot_type thy (Type (s, Ts)) =
   811     let
   812       val {qtyp, equiv_rel, equiv_thm, ...} =
   813         Quotient_Info.quotdata_lookup thy s
   814       val partial =
   815         case prop_of equiv_thm of
   816           @{const Trueprop} $ (Const (@{const_name equivp}, _) $ _) => false
   817         | @{const Trueprop} $ (Const (@{const_name part_equivp}, _) $ _) => true
   818         | _ => raise NOT_SUPPORTED "Ill-formed quotient type equivalence \
   819                                    \relation theorem"
   820       val Ts' = qtyp |> dest_Type |> snd
   821     in (subst_atomic_types (Ts' ~~ Ts) equiv_rel, partial) end
   822   | equiv_relation_for_quot_type _ T =
   823     raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], [])
   824 
   825 fun is_coconstr ctxt (s, T) =
   826   case body_type T of
   827     co_T as Type (co_s, _) =>
   828     let val {codatatypes, ...} = Data.get (Context.Proof ctxt) in
   829       exists (fn (s', T') => s = s' andalso repair_constr_type ctxt co_T T' = T)
   830              (AList.lookup (op =) codatatypes co_s |> Option.map snd |> these)
   831     end
   832   | _ => false
   833 fun is_constr_like ctxt (s, T) =
   834   member (op =) [@{const_name FunBox}, @{const_name PairBox},
   835                  @{const_name Quot}, @{const_name Zero_Rep},
   836                  @{const_name Suc_Rep}] s orelse
   837   let
   838     val thy = ProofContext.theory_of ctxt
   839     val (x as (_, T)) = (s, unarize_unbox_etc_type T)
   840   in
   841     is_real_constr thy x orelse is_record_constr x orelse
   842     (is_abs_fun ctxt x andalso is_pure_typedef ctxt (range_type T)) orelse
   843     is_coconstr ctxt x
   844   end
   845 fun is_stale_constr ctxt (x as (_, T)) =
   846   is_codatatype ctxt (body_type T) andalso is_constr_like ctxt x andalso
   847   not (is_coconstr ctxt x)
   848 fun is_constr ctxt stds (x as (_, T)) =
   849   let val thy = ProofContext.theory_of ctxt in
   850     is_constr_like ctxt x andalso
   851     not (is_basic_datatype thy stds
   852                          (fst (dest_Type (unarize_type (body_type T))))) andalso
   853     not (is_stale_constr ctxt x)
   854   end
   855 val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
   856 val is_sel_like_and_no_discr =
   857   String.isPrefix sel_prefix orf
   858   (member (op =) [@{const_name fst}, @{const_name snd}])
   859 
   860 fun in_fun_lhs_for InConstr = InSel
   861   | in_fun_lhs_for _ = InFunLHS
   862 fun in_fun_rhs_for InConstr = InConstr
   863   | in_fun_rhs_for InSel = InSel
   864   | in_fun_rhs_for InFunRHS1 = InFunRHS2
   865   | in_fun_rhs_for _ = InFunRHS1
   866 
   867 fun is_boxing_worth_it (hol_ctxt : hol_context) boxy T =
   868   case T of
   869     Type (@{type_name fun}, _) =>
   870     (boxy = InPair orelse boxy = InFunLHS) andalso
   871     not (is_boolean_type (body_type T))
   872   | Type (@{type_name prod}, Ts) =>
   873     boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse
   874     ((boxy = InExpr orelse boxy = InFunLHS) andalso
   875      exists (is_boxing_worth_it hol_ctxt InPair)
   876             (map (box_type hol_ctxt InPair) Ts))
   877   | _ => false
   878 and should_box_type (hol_ctxt as {thy, boxes, ...}) boxy z =
   879   case triple_lookup (type_match thy) boxes (Type z) of
   880     SOME (SOME box_me) => box_me
   881   | _ => is_boxing_worth_it hol_ctxt boxy (Type z)
   882 and box_type hol_ctxt boxy T =
   883   case T of
   884     Type (z as (@{type_name fun}, [T1, T2])) =>
   885     if boxy <> InConstr andalso boxy <> InSel andalso
   886        should_box_type hol_ctxt boxy z then
   887       Type (@{type_name fun_box},
   888             [box_type hol_ctxt InFunLHS T1, box_type hol_ctxt InFunRHS1 T2])
   889     else
   890       box_type hol_ctxt (in_fun_lhs_for boxy) T1
   891       --> box_type hol_ctxt (in_fun_rhs_for boxy) T2
   892   | Type (z as (@{type_name prod}, Ts)) =>
   893     if boxy <> InConstr andalso boxy <> InSel
   894        andalso should_box_type hol_ctxt boxy z then
   895       Type (@{type_name pair_box}, map (box_type hol_ctxt InSel) Ts)
   896     else
   897       Type (@{type_name prod},
   898             map (box_type hol_ctxt
   899                           (if boxy = InConstr orelse boxy = InSel then boxy
   900                            else InPair)) Ts)
   901   | _ => T
   902 
   903 fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}
   904   | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}
   905   | binarize_nat_and_int_in_type (Type (s, Ts)) =
   906     Type (s, map binarize_nat_and_int_in_type Ts)
   907   | binarize_nat_and_int_in_type T = T
   908 val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type
   909 
   910 fun discr_for_constr (s, T) = (discr_prefix ^ s, body_type T --> bool_T)
   911 
   912 fun num_sels_for_constr_type T = length (maybe_curried_binder_types T)
   913 fun nth_sel_name_for_constr_name s n =
   914   if s = @{const_name Pair} then
   915     if n = 0 then @{const_name fst} else @{const_name snd}
   916   else
   917     sel_prefix_for n ^ s
   918 fun nth_sel_for_constr x ~1 = discr_for_constr x
   919   | nth_sel_for_constr (s, T) n =
   920     (nth_sel_name_for_constr_name s n,
   921      body_type T --> nth (maybe_curried_binder_types T) n)
   922 fun binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize =
   923   apsnd ((binarize ? binarize_nat_and_int_in_type) o box_type hol_ctxt InSel)
   924   oo nth_sel_for_constr
   925 
   926 fun sel_no_from_name s =
   927   if String.isPrefix discr_prefix s then
   928     ~1
   929   else if String.isPrefix sel_prefix s then
   930     s |> unprefix sel_prefix |> Int.fromString |> the
   931   else if s = @{const_name snd} then
   932     1
   933   else
   934     0
   935 
   936 val close_form =
   937   let
   938     fun close_up zs zs' =
   939       fold (fn (z as ((s, _), T)) => fn t' =>
   940                Term.all T $ Abs (s, T, abstract_over (Var z, t')))
   941            (take (length zs' - length zs) zs')
   942     fun aux zs (@{const "==>"} $ t1 $ t2) =
   943         let val zs' = Term.add_vars t1 zs in
   944           close_up zs zs' (Logic.mk_implies (t1, aux zs' t2))
   945         end
   946       | aux zs t = close_up zs (Term.add_vars t zs) t
   947   in aux [] end
   948 
   949 fun distinctness_formula T =
   950   all_distinct_unordered_pairs_of
   951   #> map (fn (t1, t2) => @{const Not} $ (HOLogic.eq_const T $ t1 $ t2))
   952   #> List.foldr (s_conj o swap) @{const True}
   953 
   954 fun zero_const T = Const (@{const_name zero_class.zero}, T)
   955 fun suc_const T = Const (@{const_name Suc}, T --> T)
   956 
   957 fun uncached_datatype_constrs ({thy, ctxt, stds, ...} : hol_context)
   958                               (T as Type (s, Ts)) =
   959     (case AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt)))
   960                        s of
   961        SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type ctxt T)) xs'
   962      | _ =>
   963        if is_datatype ctxt stds T then
   964          case Datatype.get_info thy s of
   965            SOME {index, descr, ...} =>
   966            let
   967              val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the
   968            in
   969              map (apsnd (fn Us =>
   970                             map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T))
   971                  constrs
   972            end
   973          | NONE =>
   974            if is_record_type T then
   975              let
   976                val s' = unsuffix Record.ext_typeN s ^ Record.extN
   977                val T' = (Record.get_extT_fields thy T
   978                         |> apsnd single |> uncurry append |> map snd) ---> T
   979              in [(s', T')] end
   980            else if is_real_quot_type thy T then
   981              [(@{const_name Quot}, rep_type_for_quot_type thy T --> T)]
   982            else case typedef_info ctxt s of
   983              SOME {abs_type, rep_type, Abs_name, ...} =>
   984              [(Abs_name,
   985                varify_and_instantiate_type ctxt abs_type T rep_type --> T)]
   986            | NONE =>
   987              if T = @{typ ind} then
   988                [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]
   989              else
   990                []
   991        else
   992          [])
   993   | uncached_datatype_constrs _ _ = []
   994 fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T =
   995   case AList.lookup (op =) (!constr_cache) T of
   996     SOME xs => xs
   997   | NONE =>
   998     let val xs = uncached_datatype_constrs hol_ctxt T in
   999       (Unsynchronized.change constr_cache (cons (T, xs)); xs)
  1000     end
  1001 fun binarized_and_boxed_datatype_constrs hol_ctxt binarize =
  1002   map (apsnd ((binarize ? binarize_nat_and_int_in_type)
  1003               o box_type hol_ctxt InConstr)) o datatype_constrs hol_ctxt
  1004 val num_datatype_constrs = length oo datatype_constrs
  1005 
  1006 fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair}
  1007   | constr_name_for_sel_like @{const_name snd} = @{const_name Pair}
  1008   | constr_name_for_sel_like s' = original_name s'
  1009 fun binarized_and_boxed_constr_for_sel hol_ctxt binarize (s', T') =
  1010   let val s = constr_name_for_sel_like s' in
  1011     AList.lookup (op =)
  1012         (binarized_and_boxed_datatype_constrs hol_ctxt binarize (domain_type T'))
  1013         s
  1014     |> the |> pair s
  1015   end
  1016 
  1017 fun discr_term_for_constr hol_ctxt (x as (s, T)) =
  1018   let val dataT = body_type T in
  1019     if s = @{const_name Suc} then
  1020       Abs (Name.uu, dataT,
  1021            @{const Not} $ HOLogic.mk_eq (zero_const dataT, Bound 0))
  1022     else if num_datatype_constrs hol_ctxt dataT >= 2 then
  1023       Const (discr_for_constr x)
  1024     else
  1025       Abs (Name.uu, dataT, @{const True})
  1026   end
  1027 fun discriminate_value (hol_ctxt as {ctxt, ...}) x t =
  1028   case head_of t of
  1029     Const x' =>
  1030     if x = x' then @{const True}
  1031     else if is_constr_like ctxt x' then @{const False}
  1032     else s_betapply [] (discr_term_for_constr hol_ctxt x, t)
  1033   | _ => s_betapply [] (discr_term_for_constr hol_ctxt x, t)
  1034 
  1035 fun nth_arg_sel_term_for_constr thy stds (x as (s, T)) n =
  1036   let val (arg_Ts, dataT) = strip_type T in
  1037     if dataT = nat_T andalso is_standard_datatype thy stds nat_T then
  1038       @{term "%n::nat. n - 1"}
  1039     else if is_pair_type dataT then
  1040       Const (nth_sel_for_constr x n)
  1041     else
  1042       let
  1043         fun aux m (Type (@{type_name prod}, [T1, T2])) =
  1044             let
  1045               val (m, t1) = aux m T1
  1046               val (m, t2) = aux m T2
  1047             in (m, HOLogic.mk_prod (t1, t2)) end
  1048           | aux m T =
  1049             (m + 1, Const (nth_sel_name_for_constr_name s m, dataT --> T)
  1050                     $ Bound 0)
  1051         val m = fold (Integer.add o num_factors_in_type)
  1052                      (List.take (arg_Ts, n)) 0
  1053       in Abs ("x", dataT, aux m (nth arg_Ts n) |> snd) end
  1054   end
  1055 fun select_nth_constr_arg ctxt stds x t n res_T =
  1056   let val thy = ProofContext.theory_of ctxt in
  1057     (case strip_comb t of
  1058        (Const x', args) =>
  1059        if x = x' then nth args n
  1060        else if is_constr_like ctxt x' then Const (@{const_name unknown}, res_T)
  1061        else raise SAME ()
  1062      | _ => raise SAME())
  1063     handle SAME () =>
  1064            s_betapply [] (nth_arg_sel_term_for_constr thy stds x n, t)
  1065   end
  1066 
  1067 fun construct_value _ _ x [] = Const x
  1068   | construct_value ctxt stds (x as (s, _)) args =
  1069     let val args = map Envir.eta_contract args in
  1070       case hd args of
  1071         Const (s', _) $ t =>
  1072         if is_sel_like_and_no_discr s' andalso
  1073            constr_name_for_sel_like s' = s andalso
  1074            forall (fn (n, t') =>
  1075                       select_nth_constr_arg ctxt stds x t n dummyT = t')
  1076                   (index_seq 0 (length args) ~~ args) then
  1077           t
  1078         else
  1079           list_comb (Const x, args)
  1080       | _ => list_comb (Const x, args)
  1081     end
  1082 
  1083 fun constr_expand (hol_ctxt as {ctxt, stds, ...}) T t =
  1084   (case head_of t of
  1085      Const x => if is_constr_like ctxt x then t else raise SAME ()
  1086    | _ => raise SAME ())
  1087   handle SAME () =>
  1088          let
  1089            val x' as (_, T') =
  1090              if is_pair_type T then
  1091                let val (T1, T2) = HOLogic.dest_prodT T in
  1092                  (@{const_name Pair}, T1 --> T2 --> T)
  1093                end
  1094              else
  1095                datatype_constrs hol_ctxt T |> hd
  1096            val arg_Ts = binder_types T'
  1097          in
  1098            list_comb (Const x', map2 (select_nth_constr_arg ctxt stds x' t)
  1099                                      (index_seq 0 (length arg_Ts)) arg_Ts)
  1100          end
  1101 
  1102 fun coerce_bound_no f j t =
  1103   case t of
  1104     t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
  1105   | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
  1106   | Bound j' => if j' = j then f t else t
  1107   | _ => t
  1108 fun coerce_bound_0_in_term hol_ctxt new_T old_T =
  1109   old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0
  1110 and coerce_term (hol_ctxt as {ctxt, stds, ...}) Ts new_T old_T t =
  1111   if old_T = new_T then
  1112     t
  1113   else
  1114     case (new_T, old_T) of
  1115       (Type (new_s, new_Ts as [new_T1, new_T2]),
  1116        Type (@{type_name fun}, [old_T1, old_T2])) =>
  1117       (case eta_expand Ts t 1 of
  1118          Abs (s, _, t') =>
  1119          Abs (s, new_T1,
  1120               t' |> coerce_bound_0_in_term hol_ctxt new_T1 old_T1
  1121                  |> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2)
  1122          |> Envir.eta_contract
  1123          |> new_s <> @{type_name fun}
  1124             ? construct_value ctxt stds
  1125                   (@{const_name FunBox},
  1126                    Type (@{type_name fun}, new_Ts) --> new_T)
  1127               o single
  1128        | t' => raise TERM ("Nitpick_HOL.coerce_term", [t']))
  1129     | (Type (new_s, new_Ts as [new_T1, new_T2]),
  1130        Type (old_s, old_Ts as [old_T1, old_T2])) =>
  1131       if old_s = @{type_name fun_box} orelse
  1132          old_s = @{type_name pair_box} orelse old_s = @{type_name prod} then
  1133         case constr_expand hol_ctxt old_T t of
  1134           Const (old_s, _) $ t1 =>
  1135           if new_s = @{type_name fun} then
  1136             coerce_term hol_ctxt Ts new_T (Type (@{type_name fun}, old_Ts)) t1
  1137           else
  1138             construct_value ctxt stds
  1139                 (old_s, Type (@{type_name fun}, new_Ts) --> new_T)
  1140                 [coerce_term hol_ctxt Ts (Type (@{type_name fun}, new_Ts))
  1141                              (Type (@{type_name fun}, old_Ts)) t1]
  1142         | Const _ $ t1 $ t2 =>
  1143           construct_value ctxt stds
  1144               (if new_s = @{type_name prod} then @{const_name Pair}
  1145                else @{const_name PairBox}, new_Ts ---> new_T)
  1146               (map3 (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2]
  1147                     [t1, t2])
  1148         | t' => raise TERM ("Nitpick_HOL.coerce_term", [t'])
  1149       else
  1150         raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t])
  1151     | _ => raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t])
  1152 
  1153 fun card_of_type assigns (Type (@{type_name fun}, [T1, T2])) =
  1154     reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
  1155   | card_of_type assigns (Type (@{type_name prod}, [T1, T2])) =
  1156     card_of_type assigns T1 * card_of_type assigns T2
  1157   | card_of_type _ (Type (@{type_name itself}, _)) = 1
  1158   | card_of_type _ @{typ prop} = 2
  1159   | card_of_type _ @{typ bool} = 2
  1160   | card_of_type assigns T =
  1161     case AList.lookup (op =) assigns T of
  1162       SOME k => k
  1163     | NONE => if T = @{typ bisim_iterator} then 0
  1164               else raise TYPE ("Nitpick_HOL.card_of_type", [T], [])
  1165 fun bounded_card_of_type max default_card assigns
  1166                          (Type (@{type_name fun}, [T1, T2])) =
  1167     let
  1168       val k1 = bounded_card_of_type max default_card assigns T1
  1169       val k2 = bounded_card_of_type max default_card assigns T2
  1170     in
  1171       if k1 = max orelse k2 = max then max
  1172       else Int.min (max, reasonable_power k2 k1)
  1173     end
  1174   | bounded_card_of_type max default_card assigns
  1175                          (Type (@{type_name prod}, [T1, T2])) =
  1176     let
  1177       val k1 = bounded_card_of_type max default_card assigns T1
  1178       val k2 = bounded_card_of_type max default_card assigns T2
  1179     in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end
  1180   | bounded_card_of_type max default_card assigns T =
  1181     Int.min (max, if default_card = ~1 then
  1182                     card_of_type assigns T
  1183                   else
  1184                     card_of_type assigns T
  1185                     handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
  1186                            default_card)
  1187 fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card
  1188                                assigns T =
  1189   let
  1190     fun aux avoid T =
  1191       (if member (op =) avoid T then
  1192          0
  1193        else if member (op =) finitizable_dataTs T then
  1194          raise SAME ()
  1195        else case T of
  1196          Type (@{type_name fun}, [T1, T2]) =>
  1197          let
  1198            val k1 = aux avoid T1
  1199            val k2 = aux avoid T2
  1200          in
  1201            if k1 = 0 orelse k2 = 0 then 0
  1202            else if k1 >= max orelse k2 >= max then max
  1203            else Int.min (max, reasonable_power k2 k1)
  1204          end
  1205        | Type (@{type_name prod}, [T1, T2]) =>
  1206          let
  1207            val k1 = aux avoid T1
  1208            val k2 = aux avoid T2
  1209          in
  1210            if k1 = 0 orelse k2 = 0 then 0
  1211            else if k1 >= max orelse k2 >= max then max
  1212            else Int.min (max, k1 * k2)
  1213          end
  1214        | Type (@{type_name itself}, _) => 1
  1215        | @{typ prop} => 2
  1216        | @{typ bool} => 2
  1217        | Type _ =>
  1218          (case datatype_constrs hol_ctxt T of
  1219             [] => if is_integer_type T orelse is_bit_type T then 0
  1220                   else raise SAME ()
  1221           | constrs =>
  1222             let
  1223               val constr_cards =
  1224                 map (Integer.prod o map (aux (T :: avoid)) o binder_types o snd)
  1225                     constrs
  1226             in
  1227               if exists (curry (op =) 0) constr_cards then 0
  1228               else Integer.sum constr_cards
  1229             end)
  1230        | _ => raise SAME ())
  1231       handle SAME () =>
  1232              AList.lookup (op =) assigns T |> the_default default_card
  1233   in Int.min (max, aux [] T) end
  1234 
  1235 val small_type_max_card = 5
  1236 
  1237 fun is_finite_type hol_ctxt T =
  1238   bounded_exact_card_of_type hol_ctxt [] 1 2 [] T > 0
  1239 fun is_small_finite_type hol_ctxt T =
  1240   let val n = bounded_exact_card_of_type hol_ctxt [] 1 2 [] T in
  1241     n > 0 andalso n <= small_type_max_card
  1242   end
  1243 
  1244 fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
  1245   | is_ground_term (Const _) = true
  1246   | is_ground_term _ = false
  1247 
  1248 fun hashw_term (t1 $ t2) = hashw (hashw_term t1, hashw_term t2)
  1249   | hashw_term (Const (s, _)) = hashw_string (s, 0w0)
  1250   | hashw_term _ = 0w0
  1251 val hash_term = Word.toInt o hashw_term
  1252 
  1253 fun special_bounds ts =
  1254   fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst)
  1255 
  1256 (* FIXME: detect "rep_datatype"? *)
  1257 fun is_funky_typedef_name ctxt s =
  1258   member (op =) [@{type_name unit}, @{type_name prod},
  1259                  @{type_name Sum_Type.sum}, @{type_name int}] s orelse
  1260   is_frac_type ctxt (Type (s, []))
  1261 fun is_funky_typedef ctxt (Type (s, _)) = is_funky_typedef_name ctxt s
  1262   | is_funky_typedef _ _ = false
  1263 fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _)
  1264                          $ Const (@{const_name TYPE}, _)) = true
  1265   | is_arity_type_axiom _ = false
  1266 fun is_typedef_axiom ctxt boring (@{const "==>"} $ _ $ t2) =
  1267     is_typedef_axiom ctxt boring t2
  1268   | is_typedef_axiom ctxt boring
  1269         (@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
  1270          $ Const (_, Type (@{type_name fun}, [Type (s, _), _]))
  1271          $ Const _ $ _)) =
  1272     boring <> is_funky_typedef_name ctxt s andalso is_typedef ctxt s
  1273   | is_typedef_axiom _ _ _ = false
  1274 val is_class_axiom =
  1275   Logic.strip_horn #> swap #> op :: #> forall (can Logic.dest_of_class)
  1276 
  1277 (* Distinguishes between (1) constant definition axioms, (2) type arity and
  1278    typedef axioms, and (3) other axioms, and returns the pair ((1), (3)).
  1279    Typedef axioms are uninteresting to Nitpick, because it can retrieve them
  1280    using "typedef_info". *)
  1281 fun partition_axioms_by_definitionality ctxt axioms def_names =
  1282   let
  1283     val axioms = sort (fast_string_ord o pairself fst) axioms
  1284     val defs = Ord_List.inter (fast_string_ord o apsnd fst) def_names axioms
  1285     val nondefs =
  1286       Ord_List.subtract (fast_string_ord o apsnd fst) def_names axioms
  1287       |> filter_out ((is_arity_type_axiom orf is_typedef_axiom ctxt true) o snd)
  1288   in pairself (map snd) (defs, nondefs) end
  1289 
  1290 (* Ideally we would check against "Complex_Main", not "Refute", but any theory
  1291    will do as long as it contains all the "axioms" and "axiomatization"
  1292    commands. *)
  1293 fun is_built_in_theory thy = Theory.subthy (thy, @{theory Refute})
  1294 
  1295 val is_trivial_definition =
  1296   the_default false o try (op aconv o Logic.dest_equals)
  1297 val is_plain_definition =
  1298   let
  1299     fun do_lhs t1 =
  1300       case strip_comb t1 of
  1301         (Const _, args) =>
  1302         forall is_Var args andalso not (has_duplicates (op =) args)
  1303       | _ => false
  1304     fun do_eq (Const (@{const_name "=="}, _) $ t1 $ _) = do_lhs t1
  1305       | do_eq (@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t1 $ _)) =
  1306         do_lhs t1
  1307       | do_eq _ = false
  1308   in do_eq end
  1309 
  1310 fun all_axioms_of ctxt subst =
  1311   let
  1312     val thy = ProofContext.theory_of ctxt
  1313     val axioms_of_thys =
  1314       maps Thm.axioms_of
  1315       #> map (apsnd (subst_atomic subst o prop_of))
  1316       #> filter_out (is_class_axiom o snd)
  1317     val specs = Defs.all_specifications_of (Theory.defs_of thy)
  1318     val def_names = specs |> maps snd |> map_filter #def
  1319                     |> Ord_List.make fast_string_ord
  1320     val thys = thy :: Theory.ancestors_of thy
  1321     val (built_in_thys, user_thys) = List.partition is_built_in_theory thys
  1322     val built_in_axioms = axioms_of_thys built_in_thys
  1323     val user_axioms = axioms_of_thys user_thys
  1324     val (built_in_defs, built_in_nondefs) =
  1325       partition_axioms_by_definitionality ctxt built_in_axioms def_names
  1326       ||> filter (is_typedef_axiom ctxt false)
  1327     val (user_defs, user_nondefs) =
  1328       partition_axioms_by_definitionality ctxt user_axioms def_names
  1329     val (built_in_nondefs, user_nondefs) =
  1330       List.partition (is_typedef_axiom ctxt false) user_nondefs
  1331       |>> append built_in_nondefs
  1332     val defs =
  1333       (thy |> Global_Theory.all_thms_of
  1334            |> filter (curry (op =) Thm.definitionK o Thm.get_kind o snd)
  1335            |> map (prop_of o snd)
  1336            |> filter_out is_trivial_definition
  1337            |> filter is_plain_definition) @
  1338       user_defs @ built_in_defs
  1339   in (defs, built_in_nondefs, user_nondefs) end
  1340 
  1341 fun arity_of_built_in_const thy stds (s, T) =
  1342   if s = @{const_name If} then
  1343     if nth_range_type 3 T = @{typ bool} then NONE else SOME 3
  1344   else
  1345     let val std_nats = is_standard_datatype thy stds nat_T in
  1346       case AList.lookup (op =)
  1347                     (built_in_consts
  1348                      |> std_nats ? append built_in_nat_consts) s of
  1349         SOME n => SOME n
  1350       | NONE =>
  1351         case AList.lookup (op =)
  1352                  (built_in_typed_consts
  1353                   |> std_nats ? append built_in_typed_nat_consts)
  1354                  (s, unarize_type T) of
  1355           SOME n => SOME n
  1356         | NONE =>
  1357           case s of
  1358             @{const_name zero_class.zero} =>
  1359             if is_iterator_type T then SOME 0 else NONE
  1360           | @{const_name Suc} =>
  1361             if is_iterator_type (domain_type T) then SOME 0 else NONE
  1362           | _ => if is_fun_type T andalso is_set_type (domain_type T) then
  1363                    AList.lookup (op =) built_in_set_consts s
  1364                  else
  1365                    NONE
  1366     end
  1367 val is_built_in_const = is_some ooo arity_of_built_in_const
  1368 
  1369 (* This function is designed to work for both real definition axioms and
  1370    simplification rules (equational specifications). *)
  1371 fun term_under_def t =
  1372   case t of
  1373     @{const "==>"} $ _ $ t2 => term_under_def t2
  1374   | Const (@{const_name "=="}, _) $ t1 $ _ => term_under_def t1
  1375   | @{const Trueprop} $ t1 => term_under_def t1
  1376   | Const (@{const_name HOL.eq}, _) $ t1 $ _ => term_under_def t1
  1377   | Abs (_, _, t') => term_under_def t'
  1378   | t1 $ _ => term_under_def t1
  1379   | _ => t
  1380 
  1381 (* Here we crucially rely on "specialize_type" performing a preorder traversal
  1382    of the term, without which the wrong occurrence of a constant could be
  1383    matched in the face of overloading. *)
  1384 fun def_props_for_const thy stds table (x as (s, _)) =
  1385   if is_built_in_const thy stds x then
  1386     []
  1387   else
  1388     these (Symtab.lookup table s)
  1389     |> map_filter (try (specialize_type thy x))
  1390     |> filter (curry (op =) (Const x) o term_under_def)
  1391 
  1392 fun normalized_rhs_of t =
  1393   let
  1394     fun aux (v as Var _) (SOME t) = SOME (lambda v t)
  1395       | aux (c as Const (@{const_name TYPE}, _)) (SOME t) = SOME (lambda c t)
  1396       | aux _ _ = NONE
  1397     val (lhs, rhs) =
  1398       case t of
  1399         Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2)
  1400       | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t1 $ t2) =>
  1401         (t1, t2)
  1402       | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
  1403     val args = strip_comb lhs |> snd
  1404   in fold_rev aux args (SOME rhs) end
  1405 
  1406 fun get_def_of_const thy table (x as (s, _)) =
  1407   x |> def_props_for_const thy [(NONE, false)] table |> List.last
  1408     |> normalized_rhs_of |> Option.map (prefix_abs_vars s)
  1409   handle List.Empty => NONE
  1410 
  1411 fun def_of_const_ext thy (unfold_table, fallback_table) (x as (s, _)) =
  1412   if is_built_in_const thy [(NONE, false)] x orelse original_name s <> s then
  1413     NONE
  1414   else case get_def_of_const thy unfold_table x of
  1415     SOME def => SOME (true, def)
  1416   | NONE => get_def_of_const thy fallback_table x |> Option.map (pair false)
  1417 
  1418 val def_of_const = Option.map snd ooo def_of_const_ext
  1419 
  1420 fun fixpoint_kind_of_rhs (Abs (_, _, t)) = fixpoint_kind_of_rhs t
  1421   | fixpoint_kind_of_rhs (Const (@{const_name lfp}, _) $ Abs _) = Lfp
  1422   | fixpoint_kind_of_rhs (Const (@{const_name gfp}, _) $ Abs _) = Gfp
  1423   | fixpoint_kind_of_rhs _ = NoFp
  1424 
  1425 fun is_mutually_inductive_pred_def thy table t =
  1426   let
  1427     fun is_good_arg (Bound _) = true
  1428       | is_good_arg (Const (s, _)) =
  1429         s = @{const_name True} orelse s = @{const_name False} orelse
  1430         s = @{const_name undefined}
  1431       | is_good_arg _ = false
  1432   in
  1433     case t |> strip_abs_body |> strip_comb of
  1434       (Const x, ts as (_ :: _)) =>
  1435       (case def_of_const thy table x of
  1436          SOME t' => fixpoint_kind_of_rhs t' <> NoFp andalso
  1437                     forall is_good_arg ts
  1438        | NONE => false)
  1439     | _ => false
  1440   end
  1441 fun unfold_mutually_inductive_preds thy table =
  1442   map_aterms (fn t as Const x =>
  1443                  (case def_of_const thy table x of
  1444                     SOME t' =>
  1445                     let val t' = Envir.eta_contract t' in
  1446                       if is_mutually_inductive_pred_def thy table t' then t'
  1447                       else t
  1448                     end
  1449                  | NONE => t)
  1450                | t => t)
  1451 
  1452 fun case_const_names ctxt stds =
  1453   let val thy = ProofContext.theory_of ctxt in
  1454     Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) =>
  1455                     if is_basic_datatype thy stds dtype_s then
  1456                       I
  1457                     else
  1458                       cons (case_name, AList.lookup (op =) descr index
  1459                                        |> the |> #3 |> length))
  1460                 (Datatype.get_all thy) [] @
  1461     map (apsnd length o snd) (#codatatypes (Data.get (Context.Proof ctxt)))
  1462   end
  1463 
  1464 fun fixpoint_kind_of_const thy table x =
  1465   if is_built_in_const thy [(NONE, false)] x then NoFp
  1466   else fixpoint_kind_of_rhs (the (def_of_const thy table x))
  1467   handle Option.Option => NoFp
  1468 
  1469 fun is_real_inductive_pred ({thy, stds, def_tables, intro_table, ...}
  1470                             : hol_context) x =
  1471   fixpoint_kind_of_const thy def_tables x <> NoFp andalso
  1472   not (null (def_props_for_const thy stds intro_table x))
  1473 fun is_inductive_pred hol_ctxt (x as (s, _)) =
  1474   is_real_inductive_pred hol_ctxt x orelse String.isPrefix ubfp_prefix s orelse
  1475   String.isPrefix lbfp_prefix s
  1476 
  1477 fun lhs_of_equation t =
  1478   case t of
  1479     Const (@{const_name all}, _) $ Abs (_, _, t1) => lhs_of_equation t1
  1480   | Const (@{const_name "=="}, _) $ t1 $ _ => SOME t1
  1481   | @{const "==>"} $ _ $ t2 => lhs_of_equation t2
  1482   | @{const Trueprop} $ t1 => lhs_of_equation t1
  1483   | Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1
  1484   | Const (@{const_name HOL.eq}, _) $ t1 $ _ => SOME t1
  1485   | @{const HOL.implies} $ _ $ t2 => lhs_of_equation t2
  1486   | _ => NONE
  1487 fun is_constr_pattern _ (Bound _) = true
  1488   | is_constr_pattern _ (Var _) = true
  1489   | is_constr_pattern ctxt t =
  1490     case strip_comb t of
  1491       (Const x, args) =>
  1492       is_constr_like ctxt x andalso forall (is_constr_pattern ctxt) args
  1493     | _ => false
  1494 fun is_constr_pattern_lhs ctxt t =
  1495   forall (is_constr_pattern ctxt) (snd (strip_comb t))
  1496 fun is_constr_pattern_formula ctxt t =
  1497   case lhs_of_equation t of
  1498     SOME t' => is_constr_pattern_lhs ctxt t'
  1499   | NONE => false
  1500 
  1501 (* Similar to "specialize_type" but returns all matches rather than only the
  1502    first (preorder) match. *)
  1503 fun multi_specialize_type thy slack (s, T) t =
  1504   let
  1505     fun aux (Const (s', T')) ys =
  1506         if s = s' then
  1507           ys |> (if AList.defined (op =) ys T' then
  1508                    I
  1509                  else
  1510                    cons (T', monomorphic_term (Sign.typ_match thy (T', T)
  1511                                                               Vartab.empty) t)
  1512                    handle Type.TYPE_MATCH => I
  1513                         | TERM _ =>
  1514                           if slack then
  1515                             I
  1516                           else
  1517                             raise NOT_SUPPORTED
  1518                                       ("too much polymorphism in axiom \"" ^
  1519                                        Syntax.string_of_term_global thy t ^
  1520                                        "\" involving " ^ quote s))
  1521         else
  1522           ys
  1523       | aux _ ys = ys
  1524   in map snd (fold_aterms aux t []) end
  1525 fun nondef_props_for_const thy slack table (x as (s, _)) =
  1526   these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)
  1527 
  1528 fun unvarify_term (t1 $ t2) = unvarify_term t1 $ unvarify_term t2
  1529   | unvarify_term (Var ((s, 0), T)) = Free (s, T)
  1530   | unvarify_term (Abs (s, T, t')) = Abs (s, T, unvarify_term t')
  1531   | unvarify_term t = t
  1532 fun axiom_for_choice_spec thy =
  1533   unvarify_term
  1534   #> Object_Logic.atomize_term thy
  1535   #> Choice_Specification.close_form
  1536   #> HOLogic.mk_Trueprop
  1537 fun is_choice_spec_fun ({thy, def_tables, nondef_table, choice_spec_table, ...}
  1538                         : hol_context) x =
  1539   case nondef_props_for_const thy true choice_spec_table x of
  1540     [] => false
  1541   | ts => case def_of_const thy def_tables x of
  1542             SOME (Const (@{const_name Eps}, _) $ _) => true
  1543           | SOME _ => false
  1544           | NONE =>
  1545             let val ts' = nondef_props_for_const thy true nondef_table x in
  1546               length ts' = length ts andalso
  1547               forall (fn t =>
  1548                          exists (curry (op aconv) (axiom_for_choice_spec thy t))
  1549                                 ts') ts
  1550             end
  1551 
  1552 fun is_choice_spec_axiom thy choice_spec_table t =
  1553   Symtab.exists (fn (_, ts) =>
  1554                     exists (curry (op aconv) t o axiom_for_choice_spec thy) ts)
  1555                 choice_spec_table
  1556 
  1557 fun is_real_equational_fun ({thy, stds, simp_table, psimp_table, ...}
  1558                             : hol_context) x =
  1559   exists (fn table => not (null (def_props_for_const thy stds table x)))
  1560          [!simp_table, psimp_table]
  1561 fun is_equational_fun_but_no_plain_def hol_ctxt =
  1562   is_real_equational_fun hol_ctxt orf is_inductive_pred hol_ctxt
  1563 
  1564 (** Constant unfolding **)
  1565 
  1566 fun constr_case_body ctxt stds (func_t, (x as (_, T))) =
  1567   let val arg_Ts = binder_types T in
  1568     s_betapplys [] (func_t, map2 (select_nth_constr_arg ctxt stds x (Bound 0))
  1569                                  (index_seq 0 (length arg_Ts)) arg_Ts)
  1570   end
  1571 fun add_constr_case res_T (body_t, guard_t) res_t =
  1572   if res_T = bool_T then
  1573     s_conj (HOLogic.mk_imp (guard_t, body_t), res_t)
  1574   else
  1575     Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
  1576     $ guard_t $ body_t $ res_t
  1577 fun optimized_case_def (hol_ctxt as {ctxt, stds, ...}) dataT res_T func_ts =
  1578   let
  1579     val xs = datatype_constrs hol_ctxt dataT
  1580     val cases =
  1581       func_ts ~~ xs
  1582       |> map (fn (func_t, x) =>
  1583                  (constr_case_body ctxt stds (incr_boundvars 1 func_t, x),
  1584                   discriminate_value hol_ctxt x (Bound 0)))
  1585       |> AList.group (op aconv)
  1586       |> map (apsnd (List.foldl s_disj @{const False}))
  1587       |> sort (int_ord o pairself (size_of_term o snd))
  1588       |> rev
  1589   in
  1590     if res_T = bool_T then
  1591       if forall (member (op =) [@{const False}, @{const True}] o fst) cases then
  1592         case cases of
  1593           [(body_t, _)] => body_t
  1594         | [_, (@{const True}, head_t2)] => head_t2
  1595         | [_, (@{const False}, head_t2)] => @{const Not} $ head_t2
  1596         | _ => raise BAD ("Nitpick_HOL.optimized_case_def", "impossible cases")
  1597       else
  1598         @{const True} |> fold_rev (add_constr_case res_T) cases
  1599     else
  1600       fst (hd cases) |> fold_rev (add_constr_case res_T) (tl cases)
  1601   end
  1602   |> curry absdummy dataT
  1603 
  1604 fun optimized_record_get (hol_ctxt as {thy, ctxt, stds, ...}) s rec_T res_T t =
  1605   let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
  1606     case no_of_record_field thy s rec_T of
  1607       ~1 => (case rec_T of
  1608                Type (_, Ts as _ :: _) =>
  1609                let
  1610                  val rec_T' = List.last Ts
  1611                  val j = num_record_fields thy rec_T - 1
  1612                in
  1613                  select_nth_constr_arg ctxt stds constr_x t j res_T
  1614                  |> optimized_record_get hol_ctxt s rec_T' res_T
  1615                end
  1616              | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
  1617                                 []))
  1618     | j => select_nth_constr_arg ctxt stds constr_x t j res_T
  1619   end
  1620 fun optimized_record_update (hol_ctxt as {thy, ctxt, stds, ...}) s rec_T fun_t
  1621                             rec_t =
  1622   let
  1623     val constr_x as (_, constr_T) = hd (datatype_constrs hol_ctxt rec_T)
  1624     val Ts = binder_types constr_T
  1625     val n = length Ts
  1626     val special_j = no_of_record_field thy s rec_T
  1627     val ts =
  1628       map2 (fn j => fn T =>
  1629                let val t = select_nth_constr_arg ctxt stds constr_x rec_t j T in
  1630                  if j = special_j then
  1631                    s_betapply [] (fun_t, t)
  1632                  else if j = n - 1 andalso special_j = ~1 then
  1633                    optimized_record_update hol_ctxt s
  1634                        (rec_T |> dest_Type |> snd |> List.last) fun_t t
  1635                  else
  1636                    t
  1637                end) (index_seq 0 n) Ts
  1638   in list_comb (Const constr_x, ts) end
  1639 
  1640 (* Prevents divergence in case of cyclic or infinite definition dependencies. *)
  1641 val unfold_max_depth = 255
  1642 
  1643 (* Inline definitions or define as an equational constant? Booleans tend to
  1644    benefit more from inlining, due to the polarity analysis. *)
  1645 val def_inline_threshold_for_booleans = 60
  1646 val def_inline_threshold_for_non_booleans = 20
  1647 
  1648 fun unfold_defs_in_term
  1649         (hol_ctxt as {thy, ctxt, stds, whacks, case_names, def_tables,
  1650                       ground_thm_table, ersatz_table, ...}) =
  1651   let
  1652     fun do_term depth Ts t =
  1653       case t of
  1654         (t0 as Const (@{const_name Int.number_class.number_of},
  1655                       Type (@{type_name fun}, [_, ran_T]))) $ t1 =>
  1656         ((if is_number_type ctxt ran_T then
  1657             let
  1658               val j = t1 |> HOLogic.dest_numeral
  1659                          |> ran_T = nat_T ? Integer.max 0
  1660               val s = numeral_prefix ^ signed_string_of_int j
  1661             in
  1662               if is_integer_like_type ran_T then
  1663                 if is_standard_datatype thy stds ran_T then
  1664                   Const (s, ran_T)
  1665                 else
  1666                   funpow j (curry (op $) (suc_const ran_T)) (zero_const ran_T)
  1667               else
  1668                 do_term depth Ts (Const (@{const_name of_int}, int_T --> ran_T)
  1669                                   $ Const (s, int_T))
  1670             end
  1671             handle TERM _ => raise SAME ()
  1672           else
  1673             raise SAME ())
  1674          handle SAME () =>
  1675                 s_betapply [] (do_term depth Ts t0, do_term depth Ts t1))
  1676       | Const (@{const_name refl_on}, T) $ Const (@{const_name top}, _) $ t2 =>
  1677         do_const depth Ts t (@{const_name refl'}, range_type T) [t2]
  1678       | (t0 as Const (@{const_name Sigma}, Type (_, [T1, Type (_, [T2, T3])])))
  1679         $ t1 $ (t2 as Abs (_, _, t2')) =>
  1680         if loose_bvar1 (t2', 0) then
  1681           s_betapplys Ts (do_term depth Ts t0, map (do_term depth Ts) [t1, t2])
  1682         else
  1683           do_term depth Ts
  1684                   (Const (@{const_name prod}, T1 --> range_type T2 --> T3)
  1685                    $ t1 $ incr_boundvars ~1 t2')
  1686       | Const (x as (@{const_name distinct},
  1687                Type (@{type_name fun}, [Type (@{type_name list}, [T']), _])))
  1688         $ (t1 as _ $ _) =>
  1689         (t1 |> HOLogic.dest_list |> distinctness_formula T'
  1690          handle TERM _ => do_const depth Ts t x [t1])
  1691       | Const (x as (@{const_name If}, _)) $ t1 $ t2 $ t3 =>
  1692         if is_ground_term t1 andalso
  1693            exists (Pattern.matches thy o rpair t1)
  1694                   (Inttab.lookup_list ground_thm_table (hash_term t1)) then
  1695           do_term depth Ts t2
  1696         else
  1697           do_const depth Ts t x [t1, t2, t3]
  1698       | Const (@{const_name Let}, _) $ t1 $ t2 =>
  1699         s_betapply Ts (pairself (do_term depth Ts) (t2, t1))
  1700       | Const x => do_const depth Ts t x []
  1701       | t1 $ t2 =>
  1702         (case strip_comb t of
  1703            (Const x, ts) => do_const depth Ts t x ts
  1704          | _ => s_betapply [] (do_term depth Ts t1, do_term depth Ts t2))
  1705       | Bound _ => t
  1706       | Abs (s, T, body) => Abs (s, T, do_term depth (T :: Ts) body)
  1707       | _ => if member (term_match thy) whacks t then
  1708                Const (@{const_name unknown}, fastype_of1 (Ts, t))
  1709              else
  1710                t
  1711     and select_nth_constr_arg_with_args _ _ (x as (_, T)) [] n res_T =
  1712         (Abs (Name.uu, body_type T,
  1713               select_nth_constr_arg ctxt stds x (Bound 0) n res_T), [])
  1714       | select_nth_constr_arg_with_args depth Ts x (t :: ts) n res_T =
  1715         (select_nth_constr_arg ctxt stds x (do_term depth Ts t) n res_T, ts)
  1716     and quot_rep_of depth Ts abs_T rep_T ts =
  1717       select_nth_constr_arg_with_args depth Ts
  1718           (@{const_name Quot}, rep_T --> abs_T) ts 0 rep_T
  1719     and do_const depth Ts t (x as (s, T)) ts =
  1720       if member (term_match thy) whacks (Const x) then
  1721         Const (@{const_name unknown}, fastype_of1 (Ts, t))
  1722       else case AList.lookup (op =) ersatz_table s of
  1723         SOME s' =>
  1724         do_const (depth + 1) Ts (list_comb (Const (s', T), ts)) (s', T) ts
  1725       | NONE =>
  1726         let
  1727           fun def_inline_threshold () =
  1728             if is_boolean_type (nth_range_type (length ts) T) then
  1729               def_inline_threshold_for_booleans
  1730             else
  1731               def_inline_threshold_for_non_booleans
  1732           val (const, ts) =
  1733             if is_built_in_const thy stds x then
  1734               (Const x, ts)
  1735             else case AList.lookup (op =) case_names s of
  1736               SOME n =>
  1737               if length ts < n then
  1738                 (do_term depth Ts (eta_expand Ts t (n - length ts)), [])
  1739               else
  1740                 let
  1741                   val (dataT, res_T) = nth_range_type n T
  1742                                        |> pairf domain_type range_type
  1743                 in
  1744                   (optimized_case_def hol_ctxt dataT res_T
  1745                                       (map (do_term depth Ts) (take n ts)),
  1746                    drop n ts)
  1747                 end
  1748             | _ =>
  1749               if is_constr ctxt stds x then
  1750                 (Const x, ts)
  1751               else if is_stale_constr ctxt x then
  1752                 raise NOT_SUPPORTED ("(non-co)constructors of codatatypes \
  1753                                      \(\"" ^ s ^ "\")")
  1754               else if is_quot_abs_fun ctxt x then
  1755                 let
  1756                   val rep_T = domain_type T
  1757                   val abs_T = range_type T
  1758                 in
  1759                   (Abs (Name.uu, rep_T,
  1760                         Const (@{const_name Quot}, rep_T --> abs_T)
  1761                                $ (Const (quot_normal_name_for_type ctxt abs_T,
  1762                                          rep_T --> rep_T) $ Bound 0)), ts)
  1763                 end
  1764               else if is_quot_rep_fun ctxt x then
  1765                 quot_rep_of depth Ts (domain_type T) (range_type T) ts
  1766               else if is_record_get thy x then
  1767                 case length ts of
  1768                   0 => (do_term depth Ts (eta_expand Ts t 1), [])
  1769                 | _ => (optimized_record_get hol_ctxt s (domain_type T)
  1770                             (range_type T) (do_term depth Ts (hd ts)), tl ts)
  1771               else if is_record_update thy x then
  1772                 case length ts of
  1773                   2 => (optimized_record_update hol_ctxt
  1774                             (unsuffix Record.updateN s) (nth_range_type 2 T)
  1775                             (do_term depth Ts (hd ts))
  1776                             (do_term depth Ts (nth ts 1)), [])
  1777                 | n => (do_term depth Ts (eta_expand Ts t (2 - n)), [])
  1778               else if is_abs_fun ctxt x andalso
  1779                       is_quot_type ctxt (range_type T) then
  1780                 let
  1781                   val abs_T = range_type T
  1782                   val rep_T = domain_type (domain_type T)
  1783                   val eps_fun = Const (@{const_name Eps},
  1784                                        (rep_T --> bool_T) --> rep_T)
  1785                   val normal_fun =
  1786                     Const (quot_normal_name_for_type ctxt abs_T,
  1787                            rep_T --> rep_T)
  1788                   val abs_fun = Const (@{const_name Quot}, rep_T --> abs_T)
  1789                 in
  1790                   (Abs (Name.uu, rep_T --> bool_T,
  1791                         abs_fun $ (normal_fun $ (eps_fun $ Bound 0)))
  1792                    |> do_term (depth + 1) Ts, ts)
  1793                 end
  1794               else if is_rep_fun ctxt x then
  1795                 let val x' = mate_of_rep_fun ctxt x in
  1796                   if is_constr ctxt stds x' then
  1797                     select_nth_constr_arg_with_args depth Ts x' ts 0
  1798                                                     (range_type T)
  1799                   else if is_quot_type ctxt (domain_type T) then
  1800                     let
  1801                       val abs_T = domain_type T
  1802                       val rep_T = domain_type (range_type T)
  1803                       val (rep_fun, _) = quot_rep_of depth Ts abs_T rep_T []
  1804                       val (equiv_rel, _) =
  1805                         equiv_relation_for_quot_type thy abs_T
  1806                     in
  1807                       (Abs (Name.uu, abs_T, equiv_rel $ (rep_fun $ Bound 0)),
  1808                        ts)
  1809                     end
  1810                   else
  1811                     (Const x, ts)
  1812                 end
  1813               else if is_equational_fun_but_no_plain_def hol_ctxt x orelse
  1814                       is_choice_spec_fun hol_ctxt x then
  1815                 (Const x, ts)
  1816               else case def_of_const_ext thy def_tables x of
  1817                 SOME (unfold, def) =>
  1818                 if depth > unfold_max_depth then
  1819                   raise TOO_LARGE ("Nitpick_HOL.unfold_defs_in_term",
  1820                                    "too many nested definitions (" ^
  1821                                    string_of_int depth ^ ") while expanding " ^
  1822                                    quote s)
  1823                 else if s = @{const_name wfrec'} then
  1824                   (do_term (depth + 1) Ts (s_betapplys Ts (def, ts)), [])
  1825                 else if not unfold andalso
  1826                      size_of_term def > def_inline_threshold () then
  1827                   (Const x, ts)
  1828                 else
  1829                   (do_term (depth + 1) Ts def, ts)
  1830               | NONE => (Const x, ts)
  1831         in
  1832           s_betapplys Ts (const, map (do_term depth Ts) ts)
  1833           |> s_beta_norm Ts
  1834         end
  1835   in do_term 0 [] end
  1836 
  1837 (** Axiom extraction/generation **)
  1838 
  1839 fun extensional_equal j (Type (@{type_name fun}, [dom_T, ran_T])) t1 t2 =
  1840     let val var_t = Var (("x", j), dom_T) in
  1841       extensional_equal (j + 1) ran_T (betapply (t1, var_t))
  1842                         (betapply (t2, var_t))
  1843     end
  1844   | extensional_equal _ T t1 t2 =
  1845     Const (@{const_name HOL.eq}, T --> T --> bool_T) $ t1 $ t2
  1846 
  1847 fun equationalize_term ctxt tag t =
  1848   let
  1849     val j = maxidx_of_term t + 1
  1850     val (prems, concl) = Logic.strip_horn t
  1851   in
  1852     Logic.list_implies (prems,
  1853         case concl of
  1854           @{const Trueprop} $ (Const (@{const_name HOL.eq}, Type (_, [T, _]))
  1855                                $ t1 $ t2) =>
  1856           @{const Trueprop} $ extensional_equal j T t1 t2
  1857         | @{const Trueprop} $ t' =>
  1858           @{const Trueprop} $ HOLogic.mk_eq (t', @{const True})
  1859         | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
  1860           @{const Trueprop} $ extensional_equal j T t1 t2
  1861         | _ => (warning ("Ignoring " ^ quote tag ^ " for non-equation" ^
  1862                          quote (Syntax.string_of_term ctxt t) ^ ".");
  1863                 raise SAME ()))
  1864     |> SOME
  1865   end
  1866   handle SAME () => NONE
  1867 
  1868 fun pair_for_prop t =
  1869   case term_under_def t of
  1870     Const (s, _) => (s, t)
  1871   | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t'])
  1872 
  1873 fun def_table_for get ctxt subst =
  1874   ctxt |> get |> map (pair_for_prop o subst_atomic subst)
  1875        |> AList.group (op =) |> Symtab.make
  1876 
  1877 fun const_def_tables ctxt subst ts =
  1878   (def_table_for (map prop_of o Nitpick_Unfolds.get) ctxt subst,
  1879    fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
  1880         (map pair_for_prop ts) Symtab.empty)
  1881 
  1882 fun paired_with_consts t = map (rpair t) (Term.add_const_names t [])
  1883 fun const_nondef_table ts =
  1884   fold (append o paired_with_consts) ts [] |> AList.group (op =) |> Symtab.make
  1885 
  1886 fun const_simp_table ctxt =
  1887   def_table_for (map_filter (equationalize_term ctxt "nitpick_simp" o prop_of)
  1888                  o Nitpick_Simps.get) ctxt
  1889 fun const_psimp_table ctxt =
  1890   def_table_for (map_filter (equationalize_term ctxt "nitpick_psimp" o prop_of)
  1891                  o Nitpick_Psimps.get) ctxt
  1892 
  1893 fun const_choice_spec_table ctxt subst =
  1894   map (subst_atomic subst o prop_of) (Nitpick_Choice_Specs.get ctxt)
  1895   |> const_nondef_table
  1896 
  1897 fun inductive_intro_table ctxt subst def_tables =
  1898   let val thy = ProofContext.theory_of ctxt in
  1899     def_table_for
  1900         (maps (map (unfold_mutually_inductive_preds thy def_tables o prop_of)
  1901                o snd o snd)
  1902          o filter (fn (cat, _) => cat = Spec_Rules.Inductive orelse
  1903                                   cat = Spec_Rules.Co_Inductive)
  1904          o Spec_Rules.get) ctxt subst
  1905   end
  1906 
  1907 fun ground_theorem_table thy =
  1908   fold ((fn @{const Trueprop} $ t1 =>
  1909             is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)
  1910           | _ => I) o prop_of o snd) (Global_Theory.all_thms_of thy) Inttab.empty
  1911 
  1912 (* TODO: Move to "Nitpick.thy" *)
  1913 val basic_ersatz_table =
  1914   [(@{const_name card}, @{const_name card'}),
  1915    (@{const_name setsum}, @{const_name setsum'}),
  1916    (@{const_name fold_graph}, @{const_name fold_graph'}),
  1917    (@{const_name wf}, @{const_name wf'}),
  1918    (@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
  1919    (@{const_name wfrec}, @{const_name wfrec'})]
  1920 
  1921 fun ersatz_table ctxt =
  1922  basic_ersatz_table
  1923  |> fold (append o snd) (#frac_types (Data.get (Context.Proof ctxt)))
  1924 
  1925 fun add_simps simp_table s eqs =
  1926   Unsynchronized.change simp_table
  1927       (Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s)))
  1928 
  1929 fun inverse_axioms_for_rep_fun ctxt (x as (_, T)) =
  1930   let
  1931     val thy = ProofContext.theory_of ctxt
  1932     val abs_T = domain_type T
  1933   in
  1934     typedef_info ctxt (fst (dest_Type abs_T)) |> the
  1935     |> pairf #Abs_inverse #Rep_inverse
  1936     |> pairself (specialize_type thy x o prop_of o the)
  1937     ||> single |> op ::
  1938   end
  1939 fun optimized_typedef_axioms ctxt (abs_z as (abs_s, _)) =
  1940   let
  1941     val thy = ProofContext.theory_of ctxt
  1942     val abs_T = Type abs_z
  1943   in
  1944     if is_univ_typedef ctxt abs_T then
  1945       []
  1946     else case typedef_info ctxt abs_s of
  1947       SOME {abs_type, rep_type, Rep_name, prop_of_Rep, set_name, ...} =>
  1948       let
  1949         val rep_T = varify_and_instantiate_type ctxt abs_type abs_T rep_type
  1950         val rep_t = Const (Rep_name, abs_T --> rep_T)
  1951         val set_t = Const (set_name, rep_T --> bool_T)
  1952         val set_t' =
  1953           prop_of_Rep |> HOLogic.dest_Trueprop
  1954                       |> specialize_type thy (dest_Const rep_t)
  1955                       |> HOLogic.dest_mem |> snd
  1956       in
  1957         [HOLogic.all_const abs_T
  1958          $ Abs (Name.uu, abs_T, set_t $ (rep_t $ Bound 0))]
  1959         |> set_t <> set_t' ? cons (HOLogic.mk_eq (set_t, set_t'))
  1960         |> map HOLogic.mk_Trueprop
  1961       end
  1962     | NONE => []
  1963   end
  1964 fun optimized_quot_type_axioms ctxt stds abs_z =
  1965   let
  1966     val thy = ProofContext.theory_of ctxt
  1967     val abs_T = Type abs_z
  1968     val rep_T = rep_type_for_quot_type thy abs_T
  1969     val (equiv_rel, partial) = equiv_relation_for_quot_type thy abs_T
  1970     val a_var = Var (("a", 0), abs_T)
  1971     val x_var = Var (("x", 0), rep_T)
  1972     val y_var = Var (("y", 0), rep_T)
  1973     val x = (@{const_name Quot}, rep_T --> abs_T)
  1974     val sel_a_t = select_nth_constr_arg ctxt stds x a_var 0 rep_T
  1975     val normal_fun =
  1976       Const (quot_normal_name_for_type ctxt abs_T, rep_T --> rep_T)
  1977     val normal_x = normal_fun $ x_var
  1978     val normal_y = normal_fun $ y_var
  1979     val is_unknown_t = Const (@{const_name is_unknown}, rep_T --> bool_T)
  1980   in
  1981     [Logic.mk_equals (normal_fun $ sel_a_t, sel_a_t),
  1982      Logic.list_implies
  1983          ([@{const Not} $ (is_unknown_t $ normal_x),
  1984            @{const Not} $ (is_unknown_t $ normal_y),
  1985            equiv_rel $ x_var $ y_var] |> map HOLogic.mk_Trueprop,
  1986            Logic.mk_equals (normal_x, normal_y)),
  1987      Logic.list_implies
  1988          ([HOLogic.mk_Trueprop (@{const Not} $ (is_unknown_t $ normal_x)),
  1989            HOLogic.mk_Trueprop (@{const Not} $ HOLogic.mk_eq (normal_x, x_var))],
  1990           HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))]
  1991     |> partial ? cons (HOLogic.mk_Trueprop (equiv_rel $ sel_a_t $ sel_a_t))
  1992   end
  1993 
  1994 fun codatatype_bisim_axioms (hol_ctxt as {ctxt, stds, ...}) T =
  1995   let
  1996     val xs = datatype_constrs hol_ctxt T
  1997     val set_T = T --> bool_T
  1998     val iter_T = @{typ bisim_iterator}
  1999     val bisim_max = @{const bisim_iterator_max}
  2000     val n_var = Var (("n", 0), iter_T)
  2001     val n_var_minus_1 =
  2002       Const (@{const_name safe_The}, (iter_T --> bool_T) --> iter_T)
  2003       $ Abs ("m", iter_T, HOLogic.eq_const iter_T
  2004                           $ (suc_const iter_T $ Bound 0) $ n_var)
  2005     val x_var = Var (("x", 0), T)
  2006     val y_var = Var (("y", 0), T)
  2007     fun bisim_const T =
  2008       Const (@{const_name bisim}, iter_T --> T --> T --> bool_T)
  2009     fun nth_sub_bisim x n nth_T =
  2010       (if is_codatatype ctxt nth_T then bisim_const nth_T $ n_var_minus_1
  2011        else HOLogic.eq_const nth_T)
  2012       $ select_nth_constr_arg ctxt stds x x_var n nth_T
  2013       $ select_nth_constr_arg ctxt stds x y_var n nth_T
  2014     fun case_func (x as (_, T)) =
  2015       let
  2016         val arg_Ts = binder_types T
  2017         val core_t =
  2018           discriminate_value hol_ctxt x y_var ::
  2019           map2 (nth_sub_bisim x) (index_seq 0 (length arg_Ts)) arg_Ts
  2020           |> foldr1 s_conj
  2021       in List.foldr absdummy core_t arg_Ts end
  2022   in
  2023     [HOLogic.mk_imp
  2024        (HOLogic.mk_disj (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T,
  2025             s_betapply [] (optimized_case_def hol_ctxt T bool_T
  2026                                               (map case_func xs), x_var)),
  2027         bisim_const T $ n_var $ x_var $ y_var),
  2028      HOLogic.eq_const set_T $ (bisim_const T $ bisim_max $ x_var)
  2029      $ (Const (@{const_name insert}, T --> set_T --> set_T)
  2030         $ x_var $ Const (@{const_name bot_class.bot}, set_T))]
  2031     |> map HOLogic.mk_Trueprop
  2032   end
  2033 
  2034 exception NO_TRIPLE of unit
  2035 
  2036 fun triple_for_intro_rule thy x t =
  2037   let
  2038     val prems = Logic.strip_imp_prems t |> map (Object_Logic.atomize_term thy)
  2039     val concl = Logic.strip_imp_concl t |> Object_Logic.atomize_term thy
  2040     val (main, side) = List.partition (exists_Const (curry (op =) x)) prems
  2041     val is_good_head = curry (op =) (Const x) o head_of
  2042   in
  2043     if forall is_good_head main then (side, main, concl) else raise NO_TRIPLE ()
  2044   end
  2045 
  2046 val tuple_for_args = HOLogic.mk_tuple o snd o strip_comb
  2047 fun wf_constraint_for rel side concl main =
  2048   let
  2049     val core = HOLogic.mk_mem (HOLogic.mk_prod
  2050                                (pairself tuple_for_args (main, concl)), Var rel)
  2051     val t = List.foldl HOLogic.mk_imp core side
  2052     val vars = filter_out (curry (op =) rel) (Term.add_vars t [])
  2053   in
  2054     Library.foldl (fn (t', ((x, j), T)) =>
  2055                       HOLogic.all_const T
  2056                       $ Abs (x, T, abstract_over (Var ((x, j), T), t')))
  2057                   (t, vars)
  2058   end
  2059 fun wf_constraint_for_triple rel (side, main, concl) =
  2060   map (wf_constraint_for rel side concl) main |> foldr1 s_conj
  2061 
  2062 fun terminates_by ctxt timeout goal tac =
  2063   can (SINGLE (Classical.safe_tac (claset_of ctxt)) #> the
  2064        #> SINGLE (DETERM_TIMEOUT timeout
  2065                                  (tac ctxt (auto_tac (clasimpset_of ctxt))))
  2066        #> the #> Goal.finish ctxt) goal
  2067 
  2068 val max_cached_wfs = 50
  2069 val cached_timeout =
  2070   Synchronized.var "Nitpick_HOL.cached_timeout" (SOME Time.zeroTime)
  2071 val cached_wf_props =
  2072   Synchronized.var "Nitpick_HOL.cached_wf_props" ([] : (term * bool) list)
  2073 
  2074 val termination_tacs = [Lexicographic_Order.lex_order_tac true,
  2075                         ScnpReconstruct.sizechange_tac]
  2076 
  2077 fun uncached_is_well_founded_inductive_pred
  2078         ({thy, ctxt, stds, debug, tac_timeout, intro_table, ...} : hol_context)
  2079         (x as (_, T)) =
  2080   case def_props_for_const thy stds intro_table x of
  2081     [] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
  2082                       [Const x])
  2083   | intro_ts =>
  2084     (case map (triple_for_intro_rule thy x) intro_ts
  2085           |> filter_out (null o #2) of
  2086        [] => true
  2087      | triples =>
  2088        let
  2089          val binders_T = HOLogic.mk_tupleT (binder_types T)
  2090          val rel_T = HOLogic.mk_prodT (binders_T, binders_T) --> bool_T
  2091          val j = fold Integer.max (map maxidx_of_term intro_ts) 0 + 1
  2092          val rel = (("R", j), rel_T)
  2093          val prop = Const (@{const_name wf}, rel_T --> bool_T) $ Var rel ::
  2094                     map (wf_constraint_for_triple rel) triples
  2095                     |> foldr1 s_conj |> HOLogic.mk_Trueprop
  2096          val _ = if debug then
  2097                    Output.urgent_message ("Wellfoundedness goal: " ^
  2098                              Syntax.string_of_term ctxt prop ^ ".")
  2099                  else
  2100                    ()
  2101        in
  2102          if tac_timeout = Synchronized.value cached_timeout andalso
  2103             length (Synchronized.value cached_wf_props) < max_cached_wfs then
  2104            ()
  2105          else
  2106            (Synchronized.change cached_wf_props (K []);
  2107             Synchronized.change cached_timeout (K tac_timeout));
  2108          case AList.lookup (op =) (Synchronized.value cached_wf_props) prop of
  2109            SOME wf => wf
  2110          | NONE =>
  2111            let
  2112              val goal = prop |> cterm_of thy |> Goal.init
  2113              val wf = exists (terminates_by ctxt tac_timeout goal)
  2114                              termination_tacs
  2115            in Synchronized.change cached_wf_props (cons (prop, wf)); wf end
  2116        end)
  2117     handle List.Empty => false | NO_TRIPLE () => false
  2118 
  2119 (* The type constraint below is a workaround for a Poly/ML crash. *)
  2120 
  2121 fun is_well_founded_inductive_pred
  2122         (hol_ctxt as {thy, wfs, def_tables, wf_cache, ...} : hol_context)
  2123         (x as (s, _)) =
  2124   case triple_lookup (const_match thy) wfs x of
  2125     SOME (SOME b) => b
  2126   | _ => s = @{const_name Nats} orelse s = @{const_name fold_graph'} orelse
  2127          case AList.lookup (op =) (!wf_cache) x of
  2128            SOME (_, wf) => wf
  2129          | NONE =>
  2130            let
  2131              val gfp = (fixpoint_kind_of_const thy def_tables x = Gfp)
  2132              val wf = uncached_is_well_founded_inductive_pred hol_ctxt x
  2133            in
  2134              Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
  2135            end
  2136 
  2137 fun ap_curry [_] _ t = t
  2138   | ap_curry arg_Ts tuple_T t =
  2139     let val n = length arg_Ts in
  2140       list_abs (map (pair "c") arg_Ts,
  2141                 incr_boundvars n t
  2142                 $ mk_flat_tuple tuple_T (map Bound (n - 1 downto 0)))
  2143     end
  2144 
  2145 fun num_occs_of_bound_in_term j (t1 $ t2) =
  2146     op + (pairself (num_occs_of_bound_in_term j) (t1, t2))
  2147   | num_occs_of_bound_in_term j (Abs (_, _, t')) =
  2148     num_occs_of_bound_in_term (j + 1) t'
  2149   | num_occs_of_bound_in_term j (Bound j') = if j' = j then 1 else 0
  2150   | num_occs_of_bound_in_term _ _ = 0
  2151 
  2152 val is_linear_inductive_pred_def =
  2153   let
  2154     fun do_disjunct j (Const (@{const_name Ex}, _) $ Abs (_, _, t2)) =
  2155         do_disjunct (j + 1) t2
  2156       | do_disjunct j t =
  2157         case num_occs_of_bound_in_term j t of
  2158           0 => true
  2159         | 1 => exists (curry (op =) (Bound j) o head_of) (conjuncts_of t)
  2160         | _ => false
  2161     fun do_lfp_def (Const (@{const_name lfp}, _) $ t2) =
  2162         let val (xs, body) = strip_abs t2 in
  2163           case length xs of
  2164             1 => false
  2165           | n => forall (do_disjunct (n - 1)) (disjuncts_of body)
  2166         end
  2167       | do_lfp_def _ = false
  2168   in do_lfp_def o strip_abs_body end
  2169 
  2170 fun n_ptuple_paths 0 = []
  2171   | n_ptuple_paths 1 = []
  2172   | n_ptuple_paths n = [] :: map (cons 2) (n_ptuple_paths (n - 1))
  2173 val ap_n_split = HOLogic.mk_psplits o n_ptuple_paths
  2174 
  2175 val linear_pred_base_and_step_rhss =
  2176   let
  2177     fun aux (Const (@{const_name lfp}, _) $ t2) =
  2178         let
  2179           val (xs, body) = strip_abs t2
  2180           val arg_Ts = map snd (tl xs)
  2181           val tuple_T = HOLogic.mk_tupleT arg_Ts
  2182           val j = length arg_Ts
  2183           fun repair_rec j (Const (@{const_name Ex}, T1) $ Abs (s2, T2, t2')) =
  2184               Const (@{const_name Ex}, T1)
  2185               $ Abs (s2, T2, repair_rec (j + 1) t2')
  2186             | repair_rec j (@{const HOL.conj} $ t1 $ t2) =
  2187               @{const HOL.conj} $ repair_rec j t1 $ repair_rec j t2
  2188             | repair_rec j t =
  2189               let val (head, args) = strip_comb t in
  2190                 if head = Bound j then
  2191                   HOLogic.eq_const tuple_T $ Bound j
  2192                   $ mk_flat_tuple tuple_T args
  2193                 else
  2194                   t
  2195               end
  2196           val (nonrecs, recs) =
  2197             List.partition (curry (op =) 0 o num_occs_of_bound_in_term j)
  2198                            (disjuncts_of body)
  2199           val base_body = nonrecs |> List.foldl s_disj @{const False}
  2200           val step_body = recs |> map (repair_rec j)
  2201                                |> List.foldl s_disj @{const False}
  2202         in
  2203           (list_abs (tl xs, incr_bv (~1, j, base_body))
  2204            |> ap_n_split (length arg_Ts) tuple_T bool_T,
  2205            Abs ("y", tuple_T, list_abs (tl xs, step_body)
  2206                               |> ap_n_split (length arg_Ts) tuple_T bool_T))
  2207         end
  2208       | aux t =
  2209         raise TERM ("Nitpick_HOL.linear_pred_base_and_step_rhss.aux", [t])
  2210   in aux end
  2211 
  2212 fun starred_linear_pred_const (hol_ctxt as {simp_table, ...}) (s, T) def =
  2213   let
  2214     val j = maxidx_of_term def + 1
  2215     val (outer, fp_app) = strip_abs def
  2216     val outer_bounds = map Bound (length outer - 1 downto 0)
  2217     val outer_vars = map (fn (s, T) => Var ((s, j), T)) outer
  2218     val fp_app = subst_bounds (rev outer_vars, fp_app)
  2219     val (outer_Ts, rest_T) = strip_n_binders (length outer) T
  2220     val tuple_arg_Ts = strip_type rest_T |> fst
  2221     val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
  2222     val set_T = tuple_T --> bool_T
  2223     val curried_T = tuple_T --> set_T
  2224     val uncurried_T = Type (@{type_name prod}, [tuple_T, tuple_T]) --> bool_T
  2225     val (base_rhs, step_rhs) = linear_pred_base_and_step_rhss fp_app
  2226     val base_x as (base_s, _) = (base_prefix ^ s, outer_Ts ---> set_T)
  2227     val base_eq = HOLogic.mk_eq (list_comb (Const base_x, outer_vars), base_rhs)
  2228                   |> HOLogic.mk_Trueprop
  2229     val _ = add_simps simp_table base_s [base_eq]
  2230     val step_x as (step_s, _) = (step_prefix ^ s, outer_Ts ---> curried_T)
  2231     val step_eq = HOLogic.mk_eq (list_comb (Const step_x, outer_vars), step_rhs)
  2232                   |> HOLogic.mk_Trueprop
  2233     val _ = add_simps simp_table step_s [step_eq]
  2234   in
  2235     list_abs (outer,
  2236               Const (@{const_name Image}, uncurried_T --> set_T --> set_T)
  2237               $ (Const (@{const_name rtrancl}, uncurried_T --> uncurried_T)
  2238                  $ (Const (@{const_name prod_case}, curried_T --> uncurried_T)
  2239                     $ list_comb (Const step_x, outer_bounds)))
  2240               $ list_comb (Const base_x, outer_bounds)
  2241               |> ap_curry tuple_arg_Ts tuple_T)
  2242     |> unfold_defs_in_term hol_ctxt
  2243   end
  2244 
  2245 fun is_good_starred_linear_pred_type (Type (@{type_name fun}, Ts)) =
  2246     forall (not o (is_fun_type orf is_pair_type)) Ts
  2247   | is_good_starred_linear_pred_type _ = false
  2248 
  2249 fun unrolled_inductive_pred_const (hol_ctxt as {thy, star_linear_preds,
  2250                                                 def_tables, simp_table, ...})
  2251                                   gfp (x as (s, T)) =
  2252   let
  2253     val iter_T = iterator_type_for_const gfp x
  2254     val x' as (s', _) = (unrolled_prefix ^ s, iter_T --> T)
  2255     val unrolled_const = Const x' $ zero_const iter_T
  2256     val def = the (def_of_const thy def_tables x)
  2257   in
  2258     if is_equational_fun_but_no_plain_def hol_ctxt x' then
  2259       unrolled_const (* already done *)
  2260     else if not gfp andalso star_linear_preds andalso
  2261          is_linear_inductive_pred_def def andalso
  2262          is_good_starred_linear_pred_type T then
  2263       starred_linear_pred_const hol_ctxt x def
  2264     else
  2265       let
  2266         val j = maxidx_of_term def + 1
  2267         val (outer, fp_app) = strip_abs def
  2268         val outer_bounds = map Bound (length outer - 1 downto 0)
  2269         val cur = Var ((iter_var_prefix, j + 1), iter_T)
  2270         val next = suc_const iter_T $ cur
  2271         val rhs =
  2272           case fp_app of
  2273             Const _ $ t =>
  2274             s_betapply [] (t, list_comb (Const x', next :: outer_bounds))
  2275           | _ => raise TERM ("Nitpick_HOL.unrolled_inductive_pred_const",
  2276                              [fp_app])
  2277         val (inner, naked_rhs) = strip_abs rhs
  2278         val all = outer @ inner
  2279         val bounds = map Bound (length all - 1 downto 0)
  2280         val vars = map (fn (s, T) => Var ((s, j), T)) all
  2281         val eq = HOLogic.mk_eq (list_comb (Const x', cur :: bounds), naked_rhs)
  2282                  |> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars)
  2283         val _ = add_simps simp_table s' [eq]
  2284       in unrolled_const end
  2285   end
  2286 
  2287 fun raw_inductive_pred_axiom ({thy, def_tables, ...} : hol_context) x =
  2288   let
  2289     val def = the (def_of_const thy def_tables x)
  2290     val (outer, fp_app) = strip_abs def
  2291     val outer_bounds = map Bound (length outer - 1 downto 0)
  2292     val rhs =
  2293       case fp_app of
  2294         Const _ $ t => s_betapply [] (t, list_comb (Const x, outer_bounds))
  2295       | _ => raise TERM ("Nitpick_HOL.raw_inductive_pred_axiom", [fp_app])
  2296     val (inner, naked_rhs) = strip_abs rhs
  2297     val all = outer @ inner
  2298     val bounds = map Bound (length all - 1 downto 0)
  2299     val j = maxidx_of_term def + 1
  2300     val vars = map (fn (s, T) => Var ((s, j), T)) all
  2301   in
  2302     HOLogic.mk_eq (list_comb (Const x, bounds), naked_rhs)
  2303     |> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars)
  2304   end
  2305 fun inductive_pred_axiom hol_ctxt (x as (s, T)) =
  2306   if String.isPrefix ubfp_prefix s orelse String.isPrefix lbfp_prefix s then
  2307     let val x' = (strip_first_name_sep s |> snd, T) in
  2308       raw_inductive_pred_axiom hol_ctxt x' |> subst_atomic [(Const x', Const x)]
  2309     end
  2310   else
  2311     raw_inductive_pred_axiom hol_ctxt x
  2312 
  2313 fun equational_fun_axioms (hol_ctxt as {thy, ctxt, stds, def_tables, simp_table,
  2314                                         psimp_table, ...}) x =
  2315   case def_props_for_const thy stds (!simp_table) x of
  2316     [] => (case def_props_for_const thy stds psimp_table x of
  2317              [] => (if is_inductive_pred hol_ctxt x then
  2318                       [inductive_pred_axiom hol_ctxt x]
  2319                     else case def_of_const thy def_tables x of
  2320                       SOME def =>
  2321                       @{const Trueprop} $ HOLogic.mk_eq (Const x, def)
  2322                       |> equationalize_term ctxt "" |> the |> single
  2323                     | NONE => [])
  2324            | psimps => psimps)
  2325   | simps => simps
  2326 fun is_equational_fun_surely_complete hol_ctxt x =
  2327   case equational_fun_axioms hol_ctxt x of
  2328     [@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t1 $ _)] =>
  2329     strip_comb t1 |> snd |> forall is_Var
  2330   | _ => false
  2331 
  2332 (** Type preprocessing **)
  2333 
  2334 fun merged_type_var_table_for_terms thy ts =
  2335   let
  2336     fun add (s, S) table =
  2337       table
  2338       |> (case AList.lookup (Sign.subsort thy o swap) table S of
  2339             SOME _ => I
  2340           | NONE =>
  2341             filter_out (fn (S', _) => Sign.subsort thy (S, S'))
  2342             #> cons (S, s))
  2343     val tfrees = [] |> fold Term.add_tfrees ts
  2344                     |> sort (string_ord o pairself fst)
  2345   in [] |> fold add tfrees |> rev end
  2346 
  2347 fun merge_type_vars_in_term thy merge_type_vars table =
  2348   merge_type_vars
  2349   ? map_types (map_atyps
  2350         (fn TFree (_, S) =>
  2351             TFree (table |> find_first (fn (S', _) => Sign.subsort thy (S', S))
  2352                          |> the |> swap)
  2353           | T => T))
  2354 
  2355 fun add_ground_types hol_ctxt binarize =
  2356   let
  2357     fun aux T accum =
  2358       case T of
  2359         Type (@{type_name fun}, Ts) => fold aux Ts accum
  2360       | Type (@{type_name prod}, Ts) => fold aux Ts accum
  2361       | Type (@{type_name itself}, [T1]) => aux T1 accum
  2362       | Type (_, Ts) =>
  2363         if member (op =) (@{typ prop} :: @{typ bool} :: accum) T then
  2364           accum
  2365         else
  2366           T :: accum
  2367           |> fold aux (case binarized_and_boxed_datatype_constrs hol_ctxt
  2368                                                                  binarize T of
  2369                          [] => Ts
  2370                        | xs => map snd xs)
  2371       | _ => insert (op =) T accum
  2372   in aux end
  2373 
  2374 fun ground_types_in_type hol_ctxt binarize T =
  2375   add_ground_types hol_ctxt binarize T []
  2376 fun ground_types_in_terms hol_ctxt binarize ts =
  2377   fold (fold_types (add_ground_types hol_ctxt binarize)) ts []
  2378 
  2379 end;