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