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