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