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