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