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