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