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