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