src/HOL/Tools/Nitpick/nitpick_hol.ML
author blanchet
Fri Nov 13 15:59:53 2009 +0100 (2009-11-13)
changeset 33705 947184dc75c9
parent 33583 b5e0909cd5ea
child 33706 7017aee615d6
permissions -rw-r--r--
removed a few global names in Nitpick (styp, nat_less, pairf)
     1 (*  Title:      HOL/Nitpick/Tools/nitpick_hol.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2008, 2009
     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 extended_context = {
    17     thy: theory,
    18     ctxt: Proof.context,
    19     max_bisim_depth: int,
    20     boxes: (typ option * bool option) list,
    21     wfs: (styp option * bool option) list,
    22     user_axioms: bool option,
    23     debug: bool,
    24     destroy_constrs: bool,
    25     specialize: bool,
    26     skolemize: bool,
    27     star_linear_preds: bool,
    28     uncurry: bool,
    29     fast_descrs: 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     intro_table: const_table,
    39     ground_thm_table: term list Inttab.table,
    40     ersatz_table: (string * string) list,
    41     skolems: (string * string list) list Unsynchronized.ref,
    42     special_funs: special_fun list Unsynchronized.ref,
    43     unrolled_preds: unrolled list Unsynchronized.ref,
    44     wf_cache: wf_cache Unsynchronized.ref,
    45     constr_cache: (typ * styp list) list Unsynchronized.ref}
    46 
    47   val name_sep : string
    48   val numeral_prefix : string
    49   val skolem_prefix : string
    50   val eval_prefix : string
    51   val original_name : string -> string
    52   val unbox_type : typ -> typ
    53   val string_for_type : Proof.context -> typ -> string
    54   val prefix_name : string -> string -> string
    55   val short_name : string -> string
    56   val short_const_name : string -> string
    57   val shorten_const_names_in_term : term -> term
    58   val type_match : theory -> typ * typ -> bool
    59   val const_match : theory -> styp * styp -> bool
    60   val term_match : theory -> term * term -> bool
    61   val is_TFree : typ -> bool
    62   val is_higher_order_type : typ -> bool
    63   val is_fun_type : typ -> bool
    64   val is_set_type : typ -> bool
    65   val is_pair_type : typ -> bool
    66   val is_lfp_iterator_type : typ -> bool
    67   val is_gfp_iterator_type : typ -> bool
    68   val is_fp_iterator_type : typ -> bool
    69   val is_boolean_type : typ -> bool
    70   val is_integer_type : typ -> bool
    71   val is_record_type : typ -> bool
    72   val is_number_type : theory -> typ -> bool
    73   val const_for_iterator_type : typ -> styp
    74   val nth_range_type : int -> typ -> typ
    75   val num_factors_in_type : typ -> int
    76   val num_binder_types : typ -> int
    77   val curried_binder_types : typ -> typ list
    78   val mk_flat_tuple : typ -> term list -> term
    79   val dest_n_tuple : int -> term -> term list
    80   val instantiate_type : theory -> typ -> typ -> typ -> typ
    81   val is_codatatype : theory -> typ -> bool
    82   val is_pure_typedef : theory -> typ -> bool
    83   val is_univ_typedef : theory -> typ -> bool
    84   val is_datatype : theory -> typ -> bool
    85   val is_record_constr : styp -> bool
    86   val is_record_get : theory -> styp -> bool
    87   val is_record_update : theory -> styp -> bool
    88   val is_abs_fun : theory -> styp -> bool
    89   val is_rep_fun : theory -> styp -> bool
    90   val is_constr : theory -> styp -> bool
    91   val is_stale_constr : theory -> styp -> bool
    92   val is_sel : string -> bool
    93   val discr_for_constr : styp -> styp
    94   val num_sels_for_constr_type : typ -> int
    95   val nth_sel_name_for_constr_name : string -> int -> string
    96   val nth_sel_for_constr : styp -> int -> styp
    97   val boxed_nth_sel_for_constr : extended_context -> styp -> int -> styp
    98   val sel_no_from_name : string -> int
    99   val eta_expand : typ list -> term -> int -> term
   100   val extensionalize : term -> term
   101   val distinctness_formula : typ -> term list -> term
   102   val register_frac_type : string -> (string * string) list -> theory -> theory
   103   val unregister_frac_type : string -> theory -> theory
   104   val register_codatatype : typ -> string -> styp list -> theory -> theory
   105   val unregister_codatatype : typ -> theory -> theory
   106   val datatype_constrs : extended_context -> typ -> styp list
   107   val boxed_datatype_constrs : extended_context -> typ -> styp list
   108   val num_datatype_constrs : extended_context -> typ -> int
   109   val constr_name_for_sel_like : string -> string
   110   val boxed_constr_for_sel : extended_context -> styp -> styp
   111   val card_of_type : (typ * int) list -> typ -> int
   112   val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
   113   val bounded_precise_card_of_type :
   114     extended_context -> int -> int -> (typ * int) list -> typ -> int
   115   val is_finite_type : extended_context -> typ -> bool
   116   val all_axioms_of : theory -> term list * term list * term list
   117   val arity_of_built_in_const : bool -> styp -> int option
   118   val is_built_in_const : bool -> styp -> bool
   119   val case_const_names : theory -> (string * int) list
   120   val const_def_table : Proof.context -> term list -> const_table
   121   val const_nondef_table : term list -> const_table
   122   val const_simp_table : Proof.context -> const_table
   123   val const_psimp_table : Proof.context -> const_table
   124   val inductive_intro_table : Proof.context -> const_table -> const_table
   125   val ground_theorem_table : theory -> term list Inttab.table
   126   val ersatz_table : theory -> (string * string) list
   127   val def_of_const : theory -> const_table -> styp -> term option
   128   val is_inductive_pred : extended_context -> styp -> bool
   129   val is_constr_pattern_lhs : theory -> term -> bool
   130   val is_constr_pattern_formula : theory -> term -> bool
   131   val merge_type_vars_in_terms : term list -> term list
   132   val ground_types_in_type : extended_context -> typ -> typ list
   133   val ground_types_in_terms : extended_context -> term list -> typ list
   134   val format_type : int list -> int list -> typ -> typ
   135   val format_term_type :
   136     theory -> const_table -> (term option * int list) list -> term -> typ
   137   val user_friendly_const :
   138    extended_context -> string * string -> (term option * int list) list
   139    -> styp -> term * typ
   140   val assign_operator_for_const : styp -> string
   141   val preprocess_term :
   142     extended_context -> term -> ((term list * term list) * (bool * bool)) * term
   143 end;
   144 
   145 structure Nitpick_HOL : NITPICK_HOL =
   146 struct
   147 
   148 open Nitpick_Util
   149 
   150 type const_table = term list Symtab.table
   151 type special_fun = (styp * int list * term list) * styp
   152 type unrolled = styp * styp
   153 type wf_cache = (styp * (bool * bool)) list
   154 
   155 type extended_context = {
   156   thy: theory,
   157   ctxt: Proof.context,
   158   max_bisim_depth: int,
   159   boxes: (typ option * bool option) list,
   160   wfs: (styp option * bool option) list,
   161   user_axioms: bool option,
   162   debug: bool,
   163   destroy_constrs: bool,
   164   specialize: bool,
   165   skolemize: bool,
   166   star_linear_preds: bool,
   167   uncurry: bool,
   168   fast_descrs: bool,
   169   tac_timeout: Time.time option,
   170   evals: term list,
   171   case_names: (string * int) list,
   172   def_table: const_table,
   173   nondef_table: const_table,
   174   user_nondefs: term list,
   175   simp_table: const_table Unsynchronized.ref,
   176   psimp_table: const_table,
   177   intro_table: const_table,
   178   ground_thm_table: term list Inttab.table,
   179   ersatz_table: (string * string) list,
   180   skolems: (string * string list) list Unsynchronized.ref,
   181   special_funs: special_fun list Unsynchronized.ref,
   182   unrolled_preds: unrolled list Unsynchronized.ref,
   183   wf_cache: wf_cache Unsynchronized.ref,
   184   constr_cache: (typ * styp list) list Unsynchronized.ref}
   185 
   186 structure Data = Theory_Data(
   187   type T = {frac_types: (string * (string * string) list) list,
   188             codatatypes: (string * (string * styp list)) list}
   189   val empty = {frac_types = [], codatatypes = []}
   190   val extend = I
   191   fun merge ({frac_types = fs1, codatatypes = cs1},
   192                {frac_types = fs2, codatatypes = cs2}) : T =
   193     {frac_types = AList.merge (op =) (op =) (fs1, fs2),
   194      codatatypes = AList.merge (op =) (op =) (cs1, cs2)})
   195 
   196 (* term * term -> term *)
   197 fun s_conj (t1, @{const True}) = t1
   198   | s_conj (@{const True}, t2) = t2
   199   | s_conj (t1, t2) = if @{const False} mem [t1, t2] then @{const False}
   200                       else HOLogic.mk_conj (t1, t2)
   201 fun s_disj (t1, @{const False}) = t1
   202   | s_disj (@{const False}, t2) = t2
   203   | s_disj (t1, t2) = if @{const True} mem [t1, t2] then @{const True}
   204                       else HOLogic.mk_disj (t1, t2)
   205 (* term -> term -> term *)
   206 fun mk_exists v t =
   207   HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)
   208 
   209 (* term -> term -> term list *)
   210 fun strip_connective conn_t (t as (t0 $ t1 $ t2)) =
   211     if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t]
   212   | strip_connective _ t = [t]
   213 (* term -> term list * term *)
   214 fun strip_any_connective (t as (t0 $ t1 $ t2)) =
   215     if t0 mem [@{const "op &"}, @{const "op |"}] then
   216       (strip_connective t0 t, t0)
   217     else
   218       ([t], @{const Not})
   219   | strip_any_connective t = ([t], @{const Not})
   220 (* term -> term list *)
   221 val conjuncts = strip_connective @{const "op &"}
   222 val disjuncts = strip_connective @{const "op |"}
   223 
   224 val name_sep = "$"
   225 val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep
   226 val sel_prefix = nitpick_prefix ^ "sel"
   227 val discr_prefix = nitpick_prefix ^ "is" ^ name_sep
   228 val set_prefix = nitpick_prefix ^ "set" ^ name_sep
   229 val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep
   230 val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep
   231 val nwf_prefix = nitpick_prefix ^ "nwf" ^ name_sep
   232 val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep
   233 val base_prefix = nitpick_prefix ^ "base" ^ name_sep
   234 val step_prefix = nitpick_prefix ^ "step" ^ name_sep
   235 val ubfp_prefix = nitpick_prefix ^ "ubfp" ^ name_sep
   236 val lbfp_prefix = nitpick_prefix ^ "lbfp" ^ name_sep
   237 val skolem_prefix = nitpick_prefix ^ "sk"
   238 val special_prefix = nitpick_prefix ^ "sp"
   239 val uncurry_prefix = nitpick_prefix ^ "unc"
   240 val eval_prefix = nitpick_prefix ^ "eval"
   241 val bound_var_prefix = "b"
   242 val cong_var_prefix = "c"
   243 val iter_var_prefix = "i"
   244 val val_var_prefix = nitpick_prefix ^ "v"
   245 val arg_var_prefix = "x"
   246 
   247 (* int -> string *)
   248 fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep
   249 fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep
   250 (* int -> int -> string *)
   251 fun skolem_prefix_for k j =
   252   skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
   253 fun uncurry_prefix_for k j =
   254   uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
   255 
   256 (* string -> string * string *)
   257 val strip_first_name_sep =
   258   Substring.full #> Substring.position name_sep ##> Substring.triml 1
   259   #> pairself Substring.string
   260 (* string -> string *)
   261 fun original_name s =
   262   if String.isPrefix nitpick_prefix s then
   263     case strip_first_name_sep s of (s1, "") => s1 | (_, s2) => original_name s2
   264   else
   265     s
   266 val after_name_sep = snd o strip_first_name_sep
   267 
   268 (* When you add constants to these lists, make sure to handle them in
   269    "Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
   270    well. *)
   271 val built_in_consts =
   272   [(@{const_name all}, 1),
   273    (@{const_name "=="}, 2),
   274    (@{const_name "==>"}, 2),
   275    (@{const_name Pure.conjunction}, 2),
   276    (@{const_name Trueprop}, 1),
   277    (@{const_name Not}, 1),
   278    (@{const_name False}, 0),
   279    (@{const_name True}, 0),
   280    (@{const_name All}, 1),
   281    (@{const_name Ex}, 1),
   282    (@{const_name "op ="}, 2),
   283    (@{const_name "op &"}, 2),
   284    (@{const_name "op |"}, 2),
   285    (@{const_name "op -->"}, 2),
   286    (@{const_name If}, 3),
   287    (@{const_name Let}, 2),
   288    (@{const_name Unity}, 0),
   289    (@{const_name Pair}, 2),
   290    (@{const_name fst}, 1),
   291    (@{const_name snd}, 1),
   292    (@{const_name Id}, 0),
   293    (@{const_name insert}, 2),
   294    (@{const_name converse}, 1),
   295    (@{const_name trancl}, 1),
   296    (@{const_name rel_comp}, 2),
   297    (@{const_name image}, 2),
   298    (@{const_name Suc}, 0),
   299    (@{const_name finite}, 1),
   300    (@{const_name nat}, 0),
   301    (@{const_name zero_nat_inst.zero_nat}, 0),
   302    (@{const_name one_nat_inst.one_nat}, 0),
   303    (@{const_name plus_nat_inst.plus_nat}, 0),
   304    (@{const_name minus_nat_inst.minus_nat}, 0),
   305    (@{const_name times_nat_inst.times_nat}, 0),
   306    (@{const_name div_nat_inst.div_nat}, 0),
   307    (@{const_name div_nat_inst.mod_nat}, 0),
   308    (@{const_name ord_nat_inst.less_nat}, 2),
   309    (@{const_name ord_nat_inst.less_eq_nat}, 2),
   310    (@{const_name nat_gcd}, 0),
   311    (@{const_name nat_lcm}, 0),
   312    (@{const_name zero_int_inst.zero_int}, 0),
   313    (@{const_name one_int_inst.one_int}, 0),
   314    (@{const_name plus_int_inst.plus_int}, 0),
   315    (@{const_name minus_int_inst.minus_int}, 0),
   316    (@{const_name times_int_inst.times_int}, 0),
   317    (@{const_name div_int_inst.div_int}, 0),
   318    (@{const_name div_int_inst.mod_int}, 0),
   319    (@{const_name uminus_int_inst.uminus_int}, 0),
   320    (@{const_name ord_int_inst.less_int}, 2),
   321    (@{const_name ord_int_inst.less_eq_int}, 2),
   322    (@{const_name Tha}, 1),
   323    (@{const_name Frac}, 0),
   324    (@{const_name norm_frac}, 0)]
   325 val built_in_descr_consts =
   326   [(@{const_name The}, 1),
   327    (@{const_name Eps}, 1)]
   328 val built_in_typed_consts =
   329   [((@{const_name of_nat}, nat_T --> int_T), 0)]
   330 val built_in_set_consts =
   331   [(@{const_name lower_semilattice_fun_inst.inf_fun}, 2),
   332    (@{const_name upper_semilattice_fun_inst.sup_fun}, 2),
   333    (@{const_name minus_fun_inst.minus_fun}, 2),
   334    (@{const_name ord_fun_inst.less_eq_fun}, 2)]
   335 
   336 (* typ -> typ *)
   337 fun unbox_type (Type (@{type_name fun_box}, Ts)) =
   338     Type ("fun", map unbox_type Ts)
   339   | unbox_type (Type (@{type_name pair_box}, Ts)) =
   340     Type ("*", map unbox_type Ts)
   341   | unbox_type (Type (s, Ts)) = Type (s, map unbox_type Ts)
   342   | unbox_type T = T
   343 (* Proof.context -> typ -> string *)
   344 fun string_for_type ctxt = Syntax.string_of_typ ctxt o unbox_type
   345 
   346 (* string -> string -> string *)
   347 val prefix_name = Long_Name.qualify o Long_Name.base_name
   348 (* string -> string *)
   349 fun short_name s = List.last (space_explode "." s) handle List.Empty => ""
   350 (* string -> term -> term *)
   351 val prefix_abs_vars = Term.map_abs_vars o prefix_name
   352 (* term -> term *)
   353 val shorten_abs_vars = Term.map_abs_vars short_name
   354 (* string -> string *)
   355 fun short_const_name s =
   356   case space_explode name_sep s of
   357     [_] => s |> String.isPrefix nitpick_prefix s ? unprefix nitpick_prefix
   358   | ss => map short_name ss |> space_implode "_"
   359 (* term -> term *)
   360 val shorten_const_names_in_term =
   361   map_aterms (fn Const (s, T) => Const (short_const_name s, T) | t => t)
   362 
   363 (* theory -> typ * typ -> bool *)
   364 fun type_match thy (T1, T2) =
   365   (Sign.typ_match thy (T2, T1) Vartab.empty; true)
   366   handle Type.TYPE_MATCH => false
   367 (* theory -> styp * styp -> bool *)
   368 fun const_match thy ((s1, T1), (s2, T2)) =
   369   s1 = s2 andalso type_match thy (T1, T2)
   370 (* theory -> term * term -> bool *)
   371 fun term_match thy (Const x1, Const x2) = const_match thy (x1, x2)
   372   | term_match thy (Free (s1, T1), Free (s2, T2)) =
   373     const_match thy ((short_name s1, T1), (short_name s2, T2))
   374   | term_match thy (t1, t2) = t1 aconv t2
   375 
   376 (* typ -> bool *)
   377 fun is_TFree (TFree _) = true
   378   | is_TFree _ = false
   379 fun is_higher_order_type (Type ("fun", _)) = true
   380   | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
   381   | is_higher_order_type _ = false
   382 fun is_fun_type (Type ("fun", _)) = true
   383   | is_fun_type _ = false
   384 fun is_set_type (Type ("fun", [_, @{typ bool}])) = true
   385   | is_set_type _ = false
   386 fun is_pair_type (Type ("*", _)) = true
   387   | is_pair_type _ = false
   388 fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s
   389   | is_lfp_iterator_type _ = false
   390 fun is_gfp_iterator_type (Type (s, _)) = String.isPrefix gfp_iterator_prefix s
   391   | is_gfp_iterator_type _ = false
   392 val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type
   393 val is_boolean_type = equal prop_T orf equal bool_T
   394 val is_integer_type =
   395   member (op =) [nat_T, int_T, @{typ bisim_iterator}] orf is_fp_iterator_type
   396 val is_record_type = not o null o Record.dest_recTs
   397 (* theory -> typ -> bool *)
   398 fun is_frac_type thy (Type (s, [])) =
   399     not (null (these (AList.lookup (op =) (#frac_types (Data.get thy)) s)))
   400   | is_frac_type _ _ = false
   401 fun is_number_type thy = is_integer_type orf is_frac_type thy
   402 
   403 (* bool -> styp -> typ *)
   404 fun iterator_type_for_const gfp (s, T) =
   405   Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s,
   406         binder_types T)
   407 (* typ -> styp *)
   408 fun const_for_iterator_type (Type (s, Ts)) = (after_name_sep s, Ts ---> bool_T)
   409   | const_for_iterator_type T =
   410     raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], [])
   411 
   412 (* int -> typ -> typ * typ *)
   413 fun strip_n_binders 0 T = ([], T)
   414   | strip_n_binders n (Type ("fun", [T1, T2])) =
   415     strip_n_binders (n - 1) T2 |>> cons T1
   416   | strip_n_binders n (Type (@{type_name fun_box}, Ts)) =
   417     strip_n_binders n (Type ("fun", Ts))
   418   | strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], [])
   419 (* typ -> typ *)
   420 val nth_range_type = snd oo strip_n_binders
   421 
   422 (* typ -> int *)
   423 fun num_factors_in_type (Type ("*", [T1, T2])) =
   424     fold (Integer.add o num_factors_in_type) [T1, T2] 0
   425   | num_factors_in_type _ = 1
   426 fun num_binder_types (Type ("fun", [_, T2])) = 1 + num_binder_types T2
   427   | num_binder_types _ = 0
   428 (* typ -> typ list *)
   429 val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types
   430 fun maybe_curried_binder_types T =
   431   (if is_pair_type (body_type T) then binder_types else curried_binder_types) T
   432 
   433 (* typ -> term list -> term *)
   434 fun mk_flat_tuple _ [t] = t
   435   | mk_flat_tuple (Type ("*", [T1, T2])) (t :: ts) =
   436     HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts)
   437   | mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts)
   438 (* int -> term -> term list *)
   439 fun dest_n_tuple 1 t = [t]
   440   | dest_n_tuple n t = HOLogic.dest_prod t ||> dest_n_tuple (n - 1) |> op ::
   441 
   442 (* int -> typ -> typ list *)
   443 fun dest_n_tuple_type 1 T = [T]
   444   | dest_n_tuple_type n (Type (_, [T1, T2])) =
   445     T1 :: dest_n_tuple_type (n - 1) T2
   446   | dest_n_tuple_type _ T =
   447     raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], [])
   448 
   449 (* (typ * typ) list -> typ -> typ *)
   450 fun typ_subst [] T = T
   451   | typ_subst ps T =
   452     let
   453       (* typ -> typ *)
   454       fun subst T =
   455         case AList.lookup (op =) ps T of
   456           SOME T' => T'
   457         | NONE => case T of Type (s, Ts) => Type (s, map subst Ts) | _ => T
   458     in subst T end
   459 
   460 (* theory -> typ -> typ -> typ -> typ *)
   461 fun instantiate_type thy T1 T1' T2 =
   462   Same.commit (Envir.subst_type_same
   463                    (Sign.typ_match thy (Logic.varifyT T1, T1') Vartab.empty))
   464               (Logic.varifyT T2)
   465   handle Type.TYPE_MATCH =>
   466          raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], [])
   467 
   468 (* theory -> typ -> typ -> styp *)
   469 fun repair_constr_type thy body_T' T =
   470   instantiate_type thy (body_type T) body_T' T
   471 
   472 (* string -> (string * string) list -> theory -> theory *)
   473 fun register_frac_type frac_s ersaetze thy =
   474   let
   475     val {frac_types, codatatypes} = Data.get thy
   476     val frac_types = AList.update (op =) (frac_s, ersaetze) frac_types
   477   in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
   478 (* string -> theory -> theory *)
   479 fun unregister_frac_type frac_s = register_frac_type frac_s []
   480 
   481 (* typ -> string -> styp list -> theory -> theory *)
   482 fun register_codatatype co_T case_name constr_xs thy =
   483   let
   484     val {frac_types, codatatypes} = Data.get thy
   485     val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs
   486     val (co_s, co_Ts) = dest_Type co_T
   487     val _ =
   488       if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) then ()
   489       else raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], [])
   490     val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs))
   491                                    codatatypes
   492   in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
   493 (* typ -> theory -> theory *)
   494 fun unregister_codatatype co_T = register_codatatype co_T "" []
   495 
   496 type typedef_info =
   497   {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
   498    set_def: thm option, prop_of_Rep: thm, set_name: string,
   499    Rep_inverse: thm option}
   500 
   501 (* theory -> string -> typedef_info *)
   502 fun typedef_info thy s =
   503   if is_frac_type thy (Type (s, [])) then
   504     SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
   505           Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
   506           set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
   507                           |> Logic.varify,
   508           set_name = @{const_name Frac}, Rep_inverse = NONE}
   509   else case Typedef.get_info thy s of
   510     SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Rep_inverse,
   511           ...} =>
   512     SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
   513           Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
   514           set_name = set_prefix ^ s, Rep_inverse = SOME Rep_inverse}
   515   | NONE => NONE
   516 
   517 (* string -> bool *)
   518 fun is_basic_datatype s =
   519     s mem [@{type_name "*"}, @{type_name bool}, @{type_name unit},
   520            @{type_name nat}, @{type_name int}]
   521 (* theory -> string -> bool *)
   522 val is_typedef = is_some oo typedef_info
   523 val is_real_datatype = is_some oo Datatype.get_info
   524 (* theory -> typ -> bool *)
   525 fun is_codatatype thy (T as Type (s, _)) =
   526     not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
   527                |> Option.map snd |> these))
   528   | is_codatatype _ _ = false
   529 fun is_pure_typedef thy (T as Type (s, _)) =
   530     is_typedef thy s andalso
   531     not (is_real_datatype thy s orelse is_codatatype thy T
   532          orelse is_record_type T orelse is_integer_type T)
   533   | is_pure_typedef _ _ = false
   534 fun is_univ_typedef thy (Type (s, _)) =
   535     (case typedef_info thy s of
   536        SOME {set_def, prop_of_Rep, ...} =>
   537        (case set_def of
   538           SOME thm =>
   539           try (fst o dest_Const o snd o Logic.dest_equals o prop_of) thm
   540         | NONE =>
   541           try (fst o dest_Const o snd o HOLogic.dest_mem
   542                o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name UNIV}
   543      | NONE => false)
   544   | is_univ_typedef _ _ = false
   545 fun is_datatype thy (T as Type (s, _)) =
   546     (is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind})
   547     andalso not (is_basic_datatype s)
   548   | is_datatype _ _ = false
   549 
   550 (* theory -> typ -> (string * typ) list * (string * typ) *)
   551 fun all_record_fields thy T =
   552   let val (recs, more) = Record.get_extT_fields thy T in
   553     recs @ more :: all_record_fields thy (snd more)
   554   end
   555   handle TYPE _ => []
   556 (* styp -> bool *)
   557 fun is_record_constr (x as (s, T)) =
   558   String.isSuffix Record.extN s andalso
   559   let val dataT = body_type T in
   560     is_record_type dataT andalso
   561     s = unsuffix Record.ext_typeN (fst (dest_Type dataT)) ^ Record.extN
   562   end
   563 (* theory -> typ -> int *)
   564 val num_record_fields = Integer.add 1 o length o fst oo Record.get_extT_fields
   565 (* theory -> string -> typ -> int *)
   566 fun no_of_record_field thy s T1 =
   567   find_index (equal s o fst) (Record.get_extT_fields thy T1 ||> single |> op @)
   568 (* theory -> styp -> bool *)
   569 fun is_record_get thy (s, Type ("fun", [T1, _])) =
   570     exists (equal s o fst) (all_record_fields thy T1)
   571   | is_record_get _ _ = false
   572 fun is_record_update thy (s, T) =
   573   String.isSuffix Record.updateN s andalso
   574   exists (equal (unsuffix Record.updateN s) o fst)
   575          (all_record_fields thy (body_type T))
   576   handle TYPE _ => false
   577 fun is_abs_fun thy (s, Type ("fun", [_, Type (s', _)])) =
   578     (case typedef_info thy s' of
   579        SOME {Abs_name, ...} => s = Abs_name
   580      | NONE => false)
   581   | is_abs_fun _ _ = false
   582 fun is_rep_fun thy (s, Type ("fun", [Type (s', _), _])) =
   583     (case typedef_info thy s' of
   584        SOME {Rep_name, ...} => s = Rep_name
   585      | NONE => false)
   586   | is_rep_fun _ _ = false
   587 
   588 (* theory -> styp -> styp *)
   589 fun mate_of_rep_fun thy (x as (_, Type ("fun", [T1 as Type (s', _), T2]))) =
   590     (case typedef_info thy s' of
   591        SOME {Abs_name, ...} => (Abs_name, Type ("fun", [T2, T1]))
   592      | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
   593   | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
   594 
   595 (* theory -> styp -> bool *)
   596 fun is_coconstr thy (s, T) =
   597   let
   598     val {codatatypes, ...} = Data.get thy
   599     val co_T = body_type T
   600     val co_s = dest_Type co_T |> fst
   601   in
   602     exists (fn (s', T') => s = s' andalso repair_constr_type thy co_T T' = T)
   603            (AList.lookup (op =) codatatypes co_s |> Option.map snd |> these)
   604   end
   605   handle TYPE ("dest_Type", _, _) => false
   606 fun is_constr_like thy (s, T) =
   607   s mem [@{const_name FunBox}, @{const_name PairBox}] orelse
   608   let val (x as (s, T)) = (s, unbox_type T) in
   609     Refute.is_IDT_constructor thy x orelse is_record_constr x
   610     orelse (is_abs_fun thy x andalso is_pure_typedef thy (range_type T))
   611     orelse s mem [@{const_name Zero_Rep}, @{const_name Suc_Rep}]
   612     orelse x = (@{const_name zero_nat_inst.zero_nat}, nat_T)
   613     orelse is_coconstr thy x
   614   end
   615 fun is_stale_constr thy (x as (_, T)) =
   616   is_codatatype thy (body_type T) andalso is_constr_like thy x
   617   andalso not (is_coconstr thy x)
   618 fun is_constr thy (x as (_, T)) =
   619   is_constr_like thy x
   620   andalso not (is_basic_datatype (fst (dest_Type (body_type T))))
   621   andalso not (is_stale_constr thy x)
   622 (* string -> bool *)
   623 val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
   624 val is_sel_like_and_no_discr =
   625   String.isPrefix sel_prefix
   626   orf (member (op =) [@{const_name fst}, @{const_name snd}])
   627 
   628 datatype boxability =
   629   InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
   630 
   631 (* boxability -> boxability *)
   632 fun in_fun_lhs_for InConstr = InSel
   633   | in_fun_lhs_for _ = InFunLHS
   634 fun in_fun_rhs_for InConstr = InConstr
   635   | in_fun_rhs_for InSel = InSel
   636   | in_fun_rhs_for InFunRHS1 = InFunRHS2
   637   | in_fun_rhs_for _ = InFunRHS1
   638 
   639 (* extended_context -> boxability -> typ -> bool *)
   640 fun is_boxing_worth_it (ext_ctxt : extended_context) boxy T =
   641   case T of
   642     Type ("fun", _) =>
   643     boxy mem [InPair, InFunLHS] andalso not (is_boolean_type (body_type T))
   644   | Type ("*", Ts) =>
   645     boxy mem [InPair, InFunRHS1, InFunRHS2]
   646     orelse (boxy mem [InExpr, InFunLHS]
   647             andalso exists (is_boxing_worth_it ext_ctxt InPair)
   648                            (map (box_type ext_ctxt InPair) Ts))
   649   | _ => false
   650 (* extended_context -> boxability -> string * typ list -> string *)
   651 and should_box_type (ext_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) =
   652   case triple_lookup (type_match thy) boxes (Type z) of
   653     SOME (SOME box_me) => box_me
   654   | _ => is_boxing_worth_it ext_ctxt boxy (Type z)
   655 (* extended_context -> boxability -> typ -> typ *)
   656 and box_type ext_ctxt boxy T =
   657   case T of
   658     Type (z as ("fun", [T1, T2])) =>
   659     if not (boxy mem [InConstr, InSel])
   660        andalso should_box_type ext_ctxt boxy z then
   661       Type (@{type_name fun_box},
   662             [box_type ext_ctxt InFunLHS T1, box_type ext_ctxt InFunRHS1 T2])
   663     else
   664       box_type ext_ctxt (in_fun_lhs_for boxy) T1
   665       --> box_type ext_ctxt (in_fun_rhs_for boxy) T2
   666   | Type (z as ("*", Ts)) =>
   667     if should_box_type ext_ctxt boxy z then
   668       Type (@{type_name pair_box}, map (box_type ext_ctxt InSel) Ts)
   669     else
   670       Type ("*", map (box_type ext_ctxt
   671                                (if boxy mem [InConstr, InSel] then boxy
   672                                 else InPair)) Ts)
   673   | _ => T
   674 
   675 (* styp -> styp *)
   676 fun discr_for_constr (s, T) = (discr_prefix ^ s, body_type T --> bool_T)
   677 
   678 (* typ -> int *)
   679 fun num_sels_for_constr_type T = length (maybe_curried_binder_types T)
   680 (* string -> int -> string *)
   681 fun nth_sel_name_for_constr_name s n =
   682   if s = @{const_name Pair} then
   683     if n = 0 then @{const_name fst} else @{const_name snd}
   684   else
   685     sel_prefix_for n ^ s
   686 (* styp -> int -> styp *)
   687 fun nth_sel_for_constr x ~1 = discr_for_constr x
   688   | nth_sel_for_constr (s, T) n =
   689     (nth_sel_name_for_constr_name s n,
   690      body_type T --> nth (maybe_curried_binder_types T) n)
   691 (* extended_context -> styp -> int -> styp *)
   692 fun boxed_nth_sel_for_constr ext_ctxt =
   693   apsnd (box_type ext_ctxt InSel) oo nth_sel_for_constr
   694 
   695 (* string -> int *)
   696 fun sel_no_from_name s =
   697   if String.isPrefix discr_prefix s then
   698     ~1
   699   else if String.isPrefix sel_prefix s then
   700     s |> unprefix sel_prefix |> Int.fromString |> the
   701   else if s = @{const_name snd} then
   702     1
   703   else
   704     0
   705 
   706 (* typ list -> term -> int -> term *)
   707 fun eta_expand _ t 0 = t
   708   | eta_expand Ts (Abs (s, T, t')) n =
   709     Abs (s, T, eta_expand (T :: Ts) t' (n - 1))
   710   | eta_expand Ts t n =
   711     fold_rev (curry3 Abs ("x\<^isub>\<eta>" ^ nat_subscript n))
   712              (List.take (binder_types (fastype_of1 (Ts, t)), n))
   713              (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
   714 
   715 (* term -> term *)
   716 fun extensionalize t =
   717   case t of
   718     (t0 as @{const Trueprop}) $ t1 => t0 $ extensionalize t1
   719   | Const (@{const_name "op ="}, _) $ t1 $ Abs (s, T, t2) =>
   720     let val v = Var ((s, maxidx_of_term t + 1), T) in
   721       extensionalize (HOLogic.mk_eq (t1 $ v, subst_bound (v, t2)))
   722     end
   723   | _ => t
   724 
   725 (* typ -> term list -> term *)
   726 fun distinctness_formula T =
   727   all_distinct_unordered_pairs_of
   728   #> map (fn (t1, t2) => @{const Not} $ (HOLogic.eq_const T $ t1 $ t2))
   729   #> List.foldr (s_conj o swap) @{const True}
   730 
   731 (* typ -> term *)
   732 fun zero_const T = Const (@{const_name zero_nat_inst.zero_nat}, T)
   733 fun suc_const T = Const (@{const_name Suc}, T --> T)
   734 
   735 (* theory -> typ -> styp list *)
   736 fun uncached_datatype_constrs thy (T as Type (s, Ts)) =
   737     (case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
   738        SOME (_, xs' as (_ :: _)) =>
   739        map (apsnd (repair_constr_type thy T)) xs'
   740      | _ =>
   741        if is_datatype thy T then
   742          case Datatype.get_info thy s of
   743            SOME {index, descr, ...} =>
   744            let
   745              val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the
   746            in
   747              map (fn (s', Us) =>
   748                      (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us
   749                           ---> T)) constrs
   750            end
   751          | NONE =>
   752            if is_record_type T then
   753              let
   754                val s' = unsuffix Record.ext_typeN s ^ Record.extN
   755                val T' = (Record.get_extT_fields thy T
   756                         |> apsnd single |> uncurry append |> map snd) ---> T
   757              in [(s', T')] end
   758            else case typedef_info thy s of
   759              SOME {abs_type, rep_type, Abs_name, ...} =>
   760              [(Abs_name, instantiate_type thy abs_type T rep_type --> T)]
   761            | NONE =>
   762              if T = @{typ ind} then
   763                [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]
   764              else
   765                []
   766        else
   767          [])
   768   | uncached_datatype_constrs _ _ = []
   769 (* extended_context -> typ -> styp list *)
   770 fun datatype_constrs (ext_ctxt as {thy, constr_cache, ...} : extended_context)
   771                      T =
   772   case AList.lookup (op =) (!constr_cache) T of
   773     SOME xs => xs
   774   | NONE =>
   775     let val xs = uncached_datatype_constrs thy T in
   776       (Unsynchronized.change constr_cache (cons (T, xs)); xs)
   777     end
   778 fun boxed_datatype_constrs ext_ctxt =
   779   map (apsnd (box_type ext_ctxt InConstr)) o datatype_constrs ext_ctxt
   780 (* extended_context -> typ -> int *)
   781 val num_datatype_constrs = length oo datatype_constrs
   782 
   783 (* string -> string *)
   784 fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair}
   785   | constr_name_for_sel_like @{const_name snd} = @{const_name Pair}
   786   | constr_name_for_sel_like s' = original_name s'
   787 (* extended_context -> styp -> styp *)
   788 fun boxed_constr_for_sel ext_ctxt (s', T') =
   789   let val s = constr_name_for_sel_like s' in
   790     AList.lookup (op =) (boxed_datatype_constrs ext_ctxt (domain_type T')) s
   791     |> the |> pair s
   792   end
   793 (* extended_context -> styp -> term *)
   794 fun discr_term_for_constr ext_ctxt (x as (s, T)) =
   795   let val dataT = body_type T in
   796     if s = @{const_name Suc} then
   797       Abs (Name.uu, dataT,
   798            @{const Not} $ HOLogic.mk_eq (zero_const dataT, Bound 0))
   799     else if num_datatype_constrs ext_ctxt dataT >= 2 then
   800       Const (discr_for_constr x)
   801     else
   802       Abs (Name.uu, dataT, @{const True})
   803   end
   804 
   805 (* extended_context -> styp -> term -> term *)
   806 fun discriminate_value (ext_ctxt as {thy, ...}) (x as (_, T)) t =
   807   case strip_comb t of
   808     (Const x', args) =>
   809     if x = x' then @{const True}
   810     else if is_constr_like thy x' then @{const False}
   811     else betapply (discr_term_for_constr ext_ctxt x, t)
   812   | _ => betapply (discr_term_for_constr ext_ctxt x, t)
   813 
   814 (* styp -> term -> term *)
   815 fun nth_arg_sel_term_for_constr (x as (s, T)) n =
   816   let val (arg_Ts, dataT) = strip_type T in
   817     if dataT = nat_T then
   818       @{term "%n::nat. minus_nat_inst.minus_nat n one_nat_inst.one_nat"}
   819     else if is_pair_type dataT then
   820       Const (nth_sel_for_constr x n)
   821     else
   822       let
   823         (* int -> typ -> int * term *)
   824         fun aux m (Type ("*", [T1, T2])) =
   825             let
   826               val (m, t1) = aux m T1
   827               val (m, t2) = aux m T2
   828             in (m, HOLogic.mk_prod (t1, t2)) end
   829           | aux m T =
   830             (m + 1, Const (nth_sel_name_for_constr_name s m, dataT --> T)
   831                     $ Bound 0)
   832         val m = fold (Integer.add o num_factors_in_type)
   833                      (List.take (arg_Ts, n)) 0
   834       in Abs ("x", dataT, aux m (nth arg_Ts n) |> snd) end
   835   end
   836 (* theory -> styp -> term -> int -> typ -> term *)
   837 fun select_nth_constr_arg thy x t n res_T =
   838   case strip_comb t of
   839     (Const x', args) =>
   840     if x = x' then nth args n
   841     else if is_constr_like thy x' then Const (@{const_name unknown}, res_T)
   842     else betapply (nth_arg_sel_term_for_constr x n, t)
   843   | _ => betapply (nth_arg_sel_term_for_constr x n, t)
   844 
   845 (* theory -> styp -> term list -> term *)
   846 fun construct_value _ x [] = Const x
   847   | construct_value thy (x as (s, _)) args =
   848     let val args = map Envir.eta_contract args in
   849       case hd args of
   850         Const (x' as (s', _)) $ t =>
   851         if is_sel_like_and_no_discr s' andalso constr_name_for_sel_like s' = s
   852            andalso forall (fn (n, t') =>
   853                               select_nth_constr_arg thy x t n dummyT = t')
   854                           (index_seq 0 (length args) ~~ args) then
   855           t
   856         else
   857           list_comb (Const x, args)
   858       | _ => list_comb (Const x, args)
   859     end
   860 
   861 (* extended_context -> typ -> term -> term *)
   862 fun constr_expand (ext_ctxt as {thy, ...}) T t =
   863   (case head_of t of
   864      Const x => if is_constr_like thy x then t else raise SAME ()
   865    | _ => raise SAME ())
   866   handle SAME () =>
   867          let
   868            val x' as (_, T') =
   869              if is_pair_type T then
   870                let val (T1, T2) = HOLogic.dest_prodT T in
   871                  (@{const_name Pair}, [T1, T2] ---> T)
   872                end
   873              else
   874                datatype_constrs ext_ctxt T |> the_single
   875            val arg_Ts = binder_types T'
   876          in
   877            list_comb (Const x', map2 (select_nth_constr_arg thy x' t)
   878                                      (index_seq 0 (length arg_Ts)) arg_Ts)
   879          end
   880 
   881 (* (typ * int) list -> typ -> int *)
   882 fun card_of_type asgns (Type ("fun", [T1, T2])) =
   883     reasonable_power (card_of_type asgns T2) (card_of_type asgns T1)
   884   | card_of_type asgns (Type ("*", [T1, T2])) =
   885     card_of_type asgns T1 * card_of_type asgns T2
   886   | card_of_type _ (Type (@{type_name itself}, _)) = 1
   887   | card_of_type _ @{typ prop} = 2
   888   | card_of_type _ @{typ bool} = 2
   889   | card_of_type _ @{typ unit} = 1
   890   | card_of_type asgns T =
   891     case AList.lookup (op =) asgns T of
   892       SOME k => k
   893     | NONE => if T = @{typ bisim_iterator} then 0
   894               else raise TYPE ("Nitpick_HOL.card_of_type", [T], [])
   895 (* int -> (typ * int) list -> typ -> int *)
   896 fun bounded_card_of_type max default_card asgns (Type ("fun", [T1, T2])) =
   897     let
   898       val k1 = bounded_card_of_type max default_card asgns T1
   899       val k2 = bounded_card_of_type max default_card asgns T2
   900     in
   901       if k1 = max orelse k2 = max then max
   902       else Int.min (max, reasonable_power k2 k1)
   903     end
   904   | bounded_card_of_type max default_card asgns (Type ("*", [T1, T2])) =
   905     let
   906       val k1 = bounded_card_of_type max default_card asgns T1
   907       val k2 = bounded_card_of_type max default_card asgns T2
   908     in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end
   909   | bounded_card_of_type max default_card asgns T =
   910     Int.min (max, if default_card = ~1 then
   911                     card_of_type asgns T
   912                   else
   913                     card_of_type asgns T
   914                     handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
   915                            default_card)
   916 (* extended_context -> int -> (typ * int) list -> typ -> int *)
   917 fun bounded_precise_card_of_type ext_ctxt max default_card asgns T =
   918   let
   919     (* typ list -> typ -> int *)
   920     fun aux avoid T =
   921       (if T mem avoid then
   922          0
   923        else case T of
   924          Type ("fun", [T1, T2]) =>
   925          let
   926            val k1 = aux avoid T1
   927            val k2 = aux avoid T2
   928          in
   929            if k1 = 0 orelse k2 = 0 then 0
   930            else if k1 >= max orelse k2 >= max then max
   931            else Int.min (max, reasonable_power k2 k1)
   932          end
   933        | Type ("*", [T1, T2]) =>
   934          let
   935            val k1 = aux avoid T1
   936            val k2 = aux avoid T2
   937          in
   938            if k1 = 0 orelse k2 = 0 then 0
   939            else if k1 >= max orelse k2 >= max then max
   940            else Int.min (max, k1 * k2)
   941          end
   942        | Type (@{type_name itself}, _) => 1
   943        | @{typ prop} => 2
   944        | @{typ bool} => 2
   945        | @{typ unit} => 1
   946        | Type _ =>
   947          (case datatype_constrs ext_ctxt T of
   948             [] => if is_integer_type T then 0 else raise SAME ()
   949           | constrs =>
   950             let
   951               val constr_cards =
   952                 datatype_constrs ext_ctxt T
   953                 |> map (Integer.prod o map (aux (T :: avoid)) o binder_types
   954                         o snd)
   955             in
   956               if exists (equal 0) constr_cards then 0
   957               else Integer.sum constr_cards
   958             end)
   959        | _ => raise SAME ())
   960       handle SAME () => AList.lookup (op =) asgns T |> the_default default_card
   961   in Int.min (max, aux [] T) end
   962 
   963 (* extended_context -> typ -> bool *)
   964 fun is_finite_type ext_ctxt =
   965   not_equal 0 o bounded_precise_card_of_type ext_ctxt 1 2 []
   966 
   967 (* term -> bool *)
   968 fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
   969   | is_ground_term (Const _) = true
   970   | is_ground_term _ = false
   971 
   972 (* term -> word -> word *)
   973 fun hashw_term (t1 $ t2) = Polyhash.hashw (hashw_term t1, hashw_term t2)
   974   | hashw_term (Const (s, _)) = Polyhash.hashw_string (s, 0w0)
   975   | hashw_term _ = 0w0
   976 (* term -> int *)
   977 val hash_term = Word.toInt o hashw_term
   978 
   979 (* term list -> (indexname * typ) list *)
   980 fun special_bounds ts =
   981   fold Term.add_vars ts [] |> sort (TermOrd.fast_indexname_ord o pairself fst)
   982 
   983 (* indexname * typ -> term -> term *)
   984 fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
   985 
   986 (* theory -> string -> bool *)
   987 fun is_funky_typedef_name thy s =
   988   s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
   989          @{type_name int}]
   990   orelse is_frac_type thy (Type (s, []))
   991 (* theory -> term -> bool *)
   992 fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
   993   | is_funky_typedef _ _ = false
   994 (* term -> bool *)
   995 fun is_arity_type_axiom (Const (@{const_name HOL.type_class}, _)
   996                          $ Const (@{const_name TYPE}, _)) = true
   997   | is_arity_type_axiom _ = false
   998 (* theory -> bool -> term -> bool *)
   999 fun is_typedef_axiom thy boring (@{const "==>"} $ _ $ t2) =
  1000     is_typedef_axiom thy boring t2
  1001   | is_typedef_axiom thy boring
  1002         (@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
  1003          $ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) =
  1004     boring <> is_funky_typedef_name thy s andalso is_typedef thy s
  1005   | is_typedef_axiom _ _ _ = false
  1006 
  1007 (* Distinguishes between (1) constant definition axioms, (2) type arity and
  1008    typedef axioms, and (3) other axioms, and returns the pair ((1), (3)).
  1009    Typedef axioms are uninteresting to Nitpick, because it can retrieve them
  1010    using "typedef_info". *)
  1011 (* theory -> (string * term) list -> string list -> term list * term list *)
  1012 fun partition_axioms_by_definitionality thy axioms def_names =
  1013   let
  1014     val axioms = sort (fast_string_ord o pairself fst) axioms
  1015     val defs = OrdList.inter (fast_string_ord o apsnd fst) def_names axioms
  1016     val nondefs =
  1017       OrdList.subtract (fast_string_ord o apsnd fst) def_names axioms
  1018       |> filter_out ((is_arity_type_axiom orf is_typedef_axiom thy true) o snd)
  1019   in pairself (map snd) (defs, nondefs) end
  1020 
  1021 (* Ideally we would check against "Complex_Main", not "Refute", but any theory
  1022    will do as long as it contains all the "axioms" and "axiomatization"
  1023    commands. *)
  1024 (* theory -> bool *)
  1025 fun is_built_in_theory thy = Theory.subthy (thy, @{theory Refute})
  1026 
  1027 (* term -> bool *)
  1028 val is_plain_definition =
  1029   let
  1030     (* term -> bool *)
  1031     fun do_lhs t1 =
  1032       case strip_comb t1 of
  1033         (Const _, args) => forall is_Var args
  1034                            andalso not (has_duplicates (op =) args)
  1035       | _ => false
  1036     fun do_eq (Const (@{const_name "=="}, _) $ t1 $ _) = do_lhs t1
  1037       | do_eq (@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)) =
  1038         do_lhs t1
  1039       | do_eq _ = false
  1040   in do_eq end
  1041 
  1042 (* theory -> term list * term list * term list *)
  1043 fun all_axioms_of thy =
  1044   let
  1045     (* theory list -> term list *)
  1046     val axioms_of_thys = maps Thm.axioms_of #> map (apsnd prop_of)
  1047     val specs = Defs.all_specifications_of (Theory.defs_of thy)
  1048     val def_names = specs |> maps snd |> filter #is_def |> map #name
  1049                     |> OrdList.make fast_string_ord
  1050     val thys = thy :: Theory.ancestors_of thy
  1051     val (built_in_thys, user_thys) = List.partition is_built_in_theory thys
  1052     val built_in_axioms = axioms_of_thys built_in_thys
  1053     val user_axioms = axioms_of_thys user_thys
  1054     val (built_in_defs, built_in_nondefs) =
  1055       partition_axioms_by_definitionality thy built_in_axioms def_names
  1056       ||> filter (is_typedef_axiom thy false)
  1057     val (user_defs, user_nondefs) =
  1058       partition_axioms_by_definitionality thy user_axioms def_names
  1059     val (built_in_nondefs, user_nondefs) =
  1060       List.partition (is_typedef_axiom thy false) user_nondefs
  1061       |>> append built_in_nondefs
  1062     val defs = (thy |> PureThy.all_thms_of
  1063                     |> filter (equal Thm.definitionK o Thm.get_kind o snd)
  1064                     |> map (prop_of o snd) |> filter is_plain_definition) @
  1065                user_defs @ built_in_defs
  1066   in (defs, built_in_nondefs, user_nondefs) end
  1067 
  1068 (* bool -> styp -> int option *)
  1069 fun arity_of_built_in_const fast_descrs (s, T) =
  1070   if s = @{const_name If} then
  1071     if nth_range_type 3 T = @{typ bool} then NONE else SOME 3
  1072   else case AList.lookup (op =)
  1073                 (built_in_consts
  1074                  |> fast_descrs ? append built_in_descr_consts) s of
  1075     SOME n => SOME n
  1076   | NONE =>
  1077     case AList.lookup (op =) built_in_typed_consts (s, T) of
  1078       SOME n => SOME n
  1079     | NONE =>
  1080       if is_fun_type T andalso is_set_type (domain_type T) then
  1081         AList.lookup (op =) built_in_set_consts s
  1082       else
  1083         NONE
  1084 (* bool -> styp -> bool *)
  1085 val is_built_in_const = is_some oo arity_of_built_in_const
  1086 
  1087 (* This function is designed to work for both real definition axioms and
  1088    simplification rules (equational specifications). *)
  1089 (* term -> term *)
  1090 fun term_under_def t =
  1091   case t of
  1092     @{const "==>"} $ _ $ t2 => term_under_def t2
  1093   | Const (@{const_name "=="}, _) $ t1 $ _ => term_under_def t1
  1094   | @{const Trueprop} $ t1 => term_under_def t1
  1095   | Const (@{const_name "op ="}, _) $ t1 $ _ => term_under_def t1
  1096   | Abs (_, _, t') => term_under_def t'
  1097   | t1 $ _ => term_under_def t1
  1098   | _ => t
  1099 
  1100 (* Here we crucially rely on "Refute.specialize_type" performing a preorder
  1101    traversal of the term, without which the wrong occurrence of a constant could
  1102    be matched in the face of overloading. *)
  1103 (* theory -> bool -> const_table -> styp -> term list *)
  1104 fun def_props_for_const thy fast_descrs table (x as (s, _)) =
  1105   if is_built_in_const fast_descrs x then
  1106     []
  1107   else
  1108     these (Symtab.lookup table s)
  1109     |> map_filter (try (Refute.specialize_type thy x))
  1110     |> filter (equal (Const x) o term_under_def)
  1111 
  1112 (* term -> term *)
  1113 fun normalized_rhs_of thy t =
  1114   let
  1115     (* term -> term *)
  1116     fun aux (v as Var _) t = lambda v t
  1117       | aux (c as Const (@{const_name TYPE}, T)) t = lambda c t
  1118       | aux _ _ = raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
  1119     val (lhs, rhs) =
  1120       case t of
  1121         Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2)
  1122       | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ t2) =>
  1123         (t1, t2)
  1124       | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
  1125     val args = strip_comb lhs |> snd
  1126   in fold_rev aux args rhs end
  1127 
  1128 (* theory -> const_table -> styp -> term option *)
  1129 fun def_of_const thy table (x as (s, _)) =
  1130   if is_built_in_const false x orelse original_name s <> s then
  1131     NONE
  1132   else
  1133     x |> def_props_for_const thy false table |> List.last
  1134       |> normalized_rhs_of thy |> prefix_abs_vars s |> SOME
  1135     handle List.Empty => NONE
  1136 
  1137 datatype fixpoint_kind = Lfp | Gfp | NoFp
  1138 
  1139 (* term -> fixpoint_kind *)
  1140 fun fixpoint_kind_of_rhs (Abs (_, _, t)) = fixpoint_kind_of_rhs t
  1141   | fixpoint_kind_of_rhs (Const (@{const_name lfp}, _) $ Abs _) = Lfp
  1142   | fixpoint_kind_of_rhs (Const (@{const_name gfp}, _) $ Abs _) = Gfp
  1143   | fixpoint_kind_of_rhs _ = NoFp
  1144 
  1145 (* theory -> const_table -> term -> bool *)
  1146 fun is_mutually_inductive_pred_def thy table t =
  1147   let
  1148     (* term -> bool *)
  1149     fun is_good_arg (Bound _) = true
  1150       | is_good_arg (Const (s, _)) =
  1151         s mem [@{const_name True}, @{const_name False}, @{const_name undefined}]
  1152       | is_good_arg _ = false
  1153   in
  1154     case t |> strip_abs_body |> strip_comb of
  1155       (Const x, ts as (_ :: _)) =>
  1156       (case def_of_const thy table x of
  1157          SOME t' => fixpoint_kind_of_rhs t' <> NoFp andalso forall is_good_arg ts
  1158        | NONE => false)
  1159     | _ => false
  1160   end
  1161 (* theory -> const_table -> term -> term *)
  1162 fun unfold_mutually_inductive_preds thy table =
  1163   map_aterms (fn t as Const x =>
  1164                  (case def_of_const thy table x of
  1165                     SOME t' =>
  1166                     let val t' = Envir.eta_contract t' in
  1167                       if is_mutually_inductive_pred_def thy table t' then t'
  1168                       else t
  1169                     end
  1170                  | NONE => t)
  1171                | t => t)
  1172 
  1173 (* term -> string * term *)
  1174 fun pair_for_prop t =
  1175   case term_under_def t of
  1176     Const (s, _) => (s, t)
  1177   | Free _ => raise NOT_SUPPORTED "local definitions"
  1178   | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t'])
  1179 
  1180 (* (Proof.context -> term list) -> Proof.context -> const_table *)
  1181 fun table_for get ctxt =
  1182   get ctxt |> map pair_for_prop |> AList.group (op =) |> Symtab.make
  1183 
  1184 (* theory -> (string * int) list *)
  1185 fun case_const_names thy =
  1186   Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) =>
  1187                   if is_basic_datatype dtype_s then
  1188                     I
  1189                   else
  1190                     cons (case_name, AList.lookup (op =) descr index
  1191                                      |> the |> #3 |> length))
  1192               (Datatype.get_all thy) [] @
  1193   map (apsnd length o snd) (#codatatypes (Data.get thy))
  1194 
  1195 (* Proof.context -> term list -> const_table *)
  1196 fun const_def_table ctxt ts =
  1197   table_for (map prop_of o Nitpick_Defs.get) ctxt
  1198   |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
  1199           (map pair_for_prop ts)
  1200 (* term list -> const_table *)
  1201 fun const_nondef_table ts =
  1202   fold (fn t => append (map (fn s => (s, t)) (Term.add_const_names t []))) ts []
  1203   |> AList.group (op =) |> Symtab.make
  1204 (* Proof.context -> const_table *)
  1205 val const_simp_table = table_for (map prop_of o Nitpick_Simps.get)
  1206 val const_psimp_table = table_for (map prop_of o Nitpick_Psimps.get)
  1207 (* Proof.context -> const_table -> const_table *)
  1208 fun inductive_intro_table ctxt def_table =
  1209   table_for (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt)
  1210                                                   def_table o prop_of)
  1211              o Nitpick_Intros.get) ctxt
  1212 (* theory -> term list Inttab.table *)
  1213 fun ground_theorem_table thy =
  1214   fold ((fn @{const Trueprop} $ t1 =>
  1215             is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1)
  1216           | _ => I) o prop_of o snd) (PureThy.all_thms_of thy) Inttab.empty
  1217 
  1218 val basic_ersatz_table =
  1219   [(@{const_name prod_case}, @{const_name split}),
  1220    (@{const_name card}, @{const_name card'}),
  1221    (@{const_name setsum}, @{const_name setsum'}),
  1222    (@{const_name fold_graph}, @{const_name fold_graph'}),
  1223    (@{const_name wf}, @{const_name wf'}),
  1224    (@{const_name wf_wfrec}, @{const_name wf_wfrec'}),
  1225    (@{const_name wfrec}, @{const_name wfrec'})]
  1226 
  1227 (* theory -> (string * string) list *)
  1228 fun ersatz_table thy =
  1229   fold (append o snd) (#frac_types (Data.get thy)) basic_ersatz_table
  1230 
  1231 (* const_table Unsynchronized.ref -> string -> term list -> unit *)
  1232 fun add_simps simp_table s eqs =
  1233   Unsynchronized.change simp_table
  1234       (Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s)))
  1235 
  1236 (* Similar to "Refute.specialize_type" but returns all matches rather than only
  1237    the first (preorder) match. *)
  1238 (* theory -> styp -> term -> term list *)
  1239 fun multi_specialize_type thy slack (x as (s, T)) t =
  1240   let
  1241     (* term -> (typ * term) list -> (typ * term) list *)
  1242     fun aux (Const (s', T')) ys =
  1243         if s = s' then
  1244           ys |> (if AList.defined (op =) ys T' then
  1245                    I
  1246                  else
  1247                   cons (T', Refute.monomorphic_term
  1248                                 (Sign.typ_match thy (T', T) Vartab.empty) t)
  1249                   handle Type.TYPE_MATCH => I
  1250                        | Refute.REFUTE _ =>
  1251                          if slack then
  1252                            I
  1253                          else
  1254                            raise NOT_SUPPORTED ("too much polymorphism in \
  1255                                                 \axiom involving " ^ quote s))
  1256         else
  1257           ys
  1258       | aux _ ys = ys
  1259   in map snd (fold_aterms aux t []) end
  1260 
  1261 (* theory -> bool -> const_table -> styp -> term list *)
  1262 fun nondef_props_for_const thy slack table (x as (s, _)) =
  1263   these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)
  1264 
  1265 (* theory -> styp list -> term list *)
  1266 fun optimized_typedef_axioms thy (abs_s, abs_Ts) =
  1267   let val abs_T = Type (abs_s, abs_Ts) in
  1268     if is_univ_typedef thy abs_T then
  1269       []
  1270     else case typedef_info thy abs_s of
  1271       SOME {abs_type, rep_type, Abs_name, Rep_name, prop_of_Rep, set_name,
  1272             ...} =>
  1273       let
  1274         val rep_T = instantiate_type thy abs_type abs_T rep_type
  1275         val rep_t = Const (Rep_name, abs_T --> rep_T)
  1276         val set_t = Const (set_name, rep_T --> bool_T)
  1277         val set_t' =
  1278           prop_of_Rep |> HOLogic.dest_Trueprop
  1279                       |> Refute.specialize_type thy (dest_Const rep_t)
  1280                       |> HOLogic.dest_mem |> snd
  1281       in
  1282         [HOLogic.all_const abs_T
  1283          $ Abs (Name.uu, abs_T, set_t $ (rep_t $ Bound 0))]
  1284         |> set_t <> set_t' ? cons (HOLogic.mk_eq (set_t, set_t'))
  1285         |> map HOLogic.mk_Trueprop
  1286       end
  1287     | NONE => []
  1288   end
  1289 (* theory -> styp -> term *)
  1290 fun inverse_axiom_for_rep_fun thy (x as (_, T)) =
  1291   typedef_info thy (fst (dest_Type (domain_type T)))
  1292   |> the |> #Rep_inverse |> the |> prop_of |> Refute.specialize_type thy x
  1293 
  1294 (* theory -> int * styp -> term *)
  1295 fun constr_case_body thy (j, (x as (_, T))) =
  1296   let val arg_Ts = binder_types T in
  1297     list_comb (Bound j, map2 (select_nth_constr_arg thy x (Bound 0))
  1298                              (index_seq 0 (length arg_Ts)) arg_Ts)
  1299   end
  1300 (* extended_context -> typ -> int * styp -> term -> term *)
  1301 fun add_constr_case (ext_ctxt as {thy, ...}) res_T (j, x) res_t =
  1302   Const (@{const_name If}, [bool_T, res_T, res_T] ---> res_T)
  1303   $ discriminate_value ext_ctxt x (Bound 0) $ constr_case_body thy (j, x)
  1304   $ res_t
  1305 (* extended_context -> typ -> typ -> term *)
  1306 fun optimized_case_def (ext_ctxt as {thy, ...}) dataT res_T =
  1307   let
  1308     val xs = datatype_constrs ext_ctxt dataT
  1309     val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
  1310     val (xs', x) = split_last xs
  1311   in
  1312     constr_case_body thy (1, x)
  1313     |> fold_rev (add_constr_case ext_ctxt res_T) (length xs downto 2 ~~ xs')
  1314     |> fold_rev (curry absdummy) (func_Ts @ [dataT])
  1315   end
  1316 
  1317 (* extended_context -> string -> typ -> typ -> term -> term *)
  1318 fun optimized_record_get (ext_ctxt as {thy, ...}) s rec_T res_T t =
  1319   let val constr_x = the_single (datatype_constrs ext_ctxt rec_T) in
  1320     case no_of_record_field thy s rec_T of
  1321       ~1 => (case rec_T of
  1322                Type (_, Ts as _ :: _) =>
  1323                let
  1324                  val rec_T' = List.last Ts
  1325                  val j = num_record_fields thy rec_T - 1
  1326                in
  1327                  select_nth_constr_arg thy constr_x t j res_T
  1328                  |> optimized_record_get ext_ctxt s rec_T' res_T
  1329                end
  1330              | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
  1331                                 []))
  1332     | j => select_nth_constr_arg thy constr_x t j res_T
  1333   end
  1334 (* extended_context -> string -> typ -> term -> term -> term *)
  1335 fun optimized_record_update (ext_ctxt as {thy, ...}) s rec_T fun_t rec_t =
  1336   let
  1337     val constr_x as (_, constr_T) = the_single (datatype_constrs ext_ctxt rec_T)
  1338     val Ts = binder_types constr_T
  1339     val n = length Ts
  1340     val special_j = no_of_record_field thy s rec_T
  1341     val ts = map2 (fn j => fn T =>
  1342                       let
  1343                         val t = select_nth_constr_arg thy constr_x rec_t j T
  1344                       in
  1345                         if j = special_j then
  1346                           betapply (fun_t, t)
  1347                         else if j = n - 1 andalso special_j = ~1 then
  1348                           optimized_record_update ext_ctxt s
  1349                               (rec_T |> dest_Type |> snd |> List.last) fun_t t
  1350                         else
  1351                           t
  1352                       end) (index_seq 0 n) Ts
  1353   in list_comb (Const constr_x, ts) end
  1354 
  1355 (* Constants "c" whose definition is of the form "c == c'", where "c'" is also a
  1356    constant, are said to be trivial. For those, we ignore the simplification
  1357    rules and use the definition instead, to ensure that built-in symbols like
  1358    "ord_nat_inst.less_eq_nat" are picked up correctly. *)
  1359 (* theory -> const_table -> styp -> bool *)
  1360 fun has_trivial_definition thy table x =
  1361   case def_of_const thy table x of SOME (Const _) => true | _ => false
  1362 
  1363 (* theory -> const_table -> string * typ -> fixpoint_kind *)
  1364 fun fixpoint_kind_of_const thy table x =
  1365   if is_built_in_const false x then
  1366     NoFp
  1367   else
  1368     fixpoint_kind_of_rhs (the (def_of_const thy table x))
  1369     handle Option.Option => NoFp
  1370 
  1371 (* extended_context -> styp -> bool *)
  1372 fun is_real_inductive_pred ({thy, fast_descrs, def_table, intro_table, ...}
  1373                             : extended_context) x =
  1374   not (null (def_props_for_const thy fast_descrs intro_table x))
  1375   andalso fixpoint_kind_of_const thy def_table x <> NoFp
  1376 fun is_real_equational_fun ({thy, fast_descrs, simp_table, psimp_table, ...}
  1377                             : extended_context) x =
  1378   exists (fn table => not (null (def_props_for_const thy fast_descrs table x)))
  1379          [!simp_table, psimp_table]
  1380 fun is_inductive_pred ext_ctxt =
  1381   is_real_inductive_pred ext_ctxt andf (not o is_real_equational_fun ext_ctxt)
  1382 fun is_equational_fun (ext_ctxt as {thy, def_table, ...}) =
  1383   (is_real_equational_fun ext_ctxt orf is_real_inductive_pred ext_ctxt
  1384    orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
  1385   andf (not o has_trivial_definition thy def_table)
  1386 
  1387 (* term * term -> term *)
  1388 fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
  1389   | s_betapply (Const (@{const_name If}, _) $ @{const False} $ _, t) = t
  1390   | s_betapply p = betapply p
  1391 (* term * term list -> term *)
  1392 val s_betapplys = Library.foldl s_betapply
  1393 
  1394 (* term -> term *)
  1395 fun lhs_of_equation t =
  1396   case t of
  1397     Const (@{const_name all}, _) $ Abs (_, _, t1) => lhs_of_equation t1
  1398   | Const (@{const_name "=="}, _) $ t1 $ _ => SOME t1
  1399   | @{const "==>"} $ _ $ t2 => lhs_of_equation t2
  1400   | @{const Trueprop} $ t1 => lhs_of_equation t1
  1401   | Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1
  1402   | Const (@{const_name "op ="}, _) $ t1 $ _ => SOME t1
  1403   | @{const "op -->"} $ _ $ t2 => lhs_of_equation t2
  1404   | _ => NONE
  1405 (* theory -> term -> bool *)
  1406 fun is_constr_pattern _ (Bound _) = true
  1407   | is_constr_pattern thy t =
  1408     case strip_comb t of
  1409       (Const (x as (s, _)), args) =>
  1410       is_constr_like thy x andalso forall (is_constr_pattern thy) args
  1411     | _ => false
  1412 fun is_constr_pattern_lhs thy t =
  1413   forall (is_constr_pattern thy) (snd (strip_comb t))
  1414 fun is_constr_pattern_formula thy t =
  1415   case lhs_of_equation t of
  1416     SOME t' => is_constr_pattern_lhs thy t'
  1417   | NONE => false
  1418 
  1419 val unfold_max_depth = 63
  1420 val axioms_max_depth = 63
  1421 
  1422 (* extended_context -> term -> term *)
  1423 fun unfold_defs_in_term (ext_ctxt as {thy, destroy_constrs, fast_descrs,
  1424                                       case_names, def_table, ground_thm_table,
  1425                                       ersatz_table, ...}) =
  1426   let
  1427     (* int -> typ list -> term -> term *)
  1428     fun do_term depth Ts t =
  1429       case t of
  1430         (t0 as Const (@{const_name Int.number_class.number_of},
  1431                       Type ("fun", [_, ran_T]))) $ t1 =>
  1432         ((if is_number_type thy ran_T then
  1433             let
  1434               val j = t1 |> HOLogic.dest_numeral
  1435                          |> ran_T <> int_T ? curry Int.max 0
  1436               val s = numeral_prefix ^ signed_string_of_int j
  1437             in
  1438               if is_integer_type ran_T then
  1439                 Const (s, ran_T)
  1440               else
  1441                 do_term depth Ts (Const (@{const_name of_int}, int_T --> ran_T)
  1442                                   $ Const (s, int_T))
  1443             end
  1444             handle TERM _ => raise SAME ()
  1445           else
  1446             raise SAME ())
  1447          handle SAME () => betapply (do_term depth Ts t0, do_term depth Ts t1))
  1448       | Const (@{const_name refl_on}, T) $ Const (@{const_name UNIV}, _) $ t2 =>
  1449         do_const depth Ts t (@{const_name refl'}, range_type T) [t2]
  1450       | (t0 as Const (x as (@{const_name Sigma}, T))) $ t1
  1451         $ (t2 as Abs (_, _, t2')) =>
  1452         betapplys (t0 |> loose_bvar1 (t2', 0) ? do_term depth Ts,
  1453                    map (do_term depth Ts) [t1, t2])
  1454       | Const (x as (@{const_name distinct},
  1455                Type ("fun", [Type (@{type_name list}, [T']), _])))
  1456         $ (t1 as _ $ _) =>
  1457         (t1 |> HOLogic.dest_list |> distinctness_formula T'
  1458          handle TERM _ => do_const depth Ts t x [t1])
  1459       | (t0 as Const (x as (@{const_name If}, _))) $ t1 $ t2 $ t3 =>
  1460         if is_ground_term t1
  1461            andalso exists (Pattern.matches thy o rpair t1)
  1462                           (Inttab.lookup_list ground_thm_table
  1463                                               (hash_term t1)) then
  1464           do_term depth Ts t2
  1465         else
  1466           do_const depth Ts t x [t1, t2, t3]
  1467       | Const x $ t1 $ t2 $ t3 => do_const depth Ts t x [t1, t2, t3]
  1468       | Const x $ t1 $ t2 => do_const depth Ts t x [t1, t2]
  1469       | Const x $ t1 => do_const depth Ts t x [t1]
  1470       | Const x => do_const depth Ts t x []
  1471       | t1 $ t2 => betapply (do_term depth Ts t1, do_term depth Ts t2)
  1472       | Free _ => t
  1473       | Var _ => t
  1474       | Bound _ => t
  1475       | Abs (s, T, body) => Abs (s, T, do_term depth (T :: Ts) body)
  1476     (* int -> typ list -> styp -> term list -> int -> typ -> term * term list *)
  1477     and select_nth_constr_arg_with_args _ _ (x as (_, T)) [] n res_T =
  1478         (Abs (Name.uu, body_type T,
  1479               select_nth_constr_arg thy x (Bound 0) n res_T), [])
  1480       | select_nth_constr_arg_with_args depth Ts x (t :: ts) n res_T =
  1481         (select_nth_constr_arg thy x (do_term depth Ts t) n res_T, ts)
  1482     (* int -> typ list -> term -> styp -> term list -> term *)
  1483     and do_const depth Ts t (x as (s, T)) ts =
  1484       case AList.lookup (op =) ersatz_table s of
  1485         SOME s' =>
  1486         do_const (depth + 1) Ts (list_comb (Const (s', T), ts)) (s', T) ts
  1487       | NONE =>
  1488         let
  1489           val (const, ts) =
  1490             if is_built_in_const fast_descrs x then
  1491               if s = @{const_name finite} then
  1492                 if is_finite_type ext_ctxt (domain_type T) then
  1493                   (Abs ("A", domain_type T, @{const True}), ts)
  1494                 else case ts of
  1495                   [Const (@{const_name UNIV}, _)] => (@{const False}, [])
  1496                 | _ => (Const x, ts)
  1497               else
  1498                 (Const x, ts)
  1499             else case AList.lookup (op =) case_names s of
  1500               SOME n =>
  1501               let
  1502                 val (dataT, res_T) = nth_range_type n T
  1503                                      |> pairf domain_type range_type
  1504               in
  1505                 (optimized_case_def ext_ctxt dataT res_T
  1506                  |> do_term (depth + 1) Ts, ts)
  1507               end
  1508             | _ =>
  1509               if is_constr thy x then
  1510                 (Const x, ts)
  1511               else if is_stale_constr thy x then
  1512                 raise NOT_SUPPORTED ("(non-co-)constructors of codatatypes \
  1513                                      \(\"" ^ s ^ "\")")
  1514               else if is_record_get thy x then
  1515                 case length ts of
  1516                   0 => (do_term depth Ts (eta_expand Ts t 1), [])
  1517                 | _ => (optimized_record_get ext_ctxt s (domain_type T)
  1518                                              (range_type T) (hd ts), tl ts)
  1519               else if is_record_update thy x then
  1520                 case length ts of
  1521                   2 => (optimized_record_update ext_ctxt
  1522                             (unsuffix Record.updateN s) (nth_range_type 2 T)
  1523                             (do_term depth Ts (hd ts))
  1524                             (do_term depth Ts (nth ts 1)), [])
  1525                 | n => (do_term depth Ts (eta_expand Ts t (2 - n)), [])
  1526               else if is_rep_fun thy x then
  1527                 let val x' = mate_of_rep_fun thy x in
  1528                   if is_constr thy x' then
  1529                     select_nth_constr_arg_with_args depth Ts x' ts 0
  1530                                                     (range_type T)
  1531                   else
  1532                     (Const x, ts)
  1533                 end
  1534               else if is_equational_fun ext_ctxt x then
  1535                 (Const x, ts)
  1536               else case def_of_const thy def_table x of
  1537                 SOME def =>
  1538                 if depth > unfold_max_depth then
  1539                   raise LIMIT ("Nitpick_HOL.unfold_defs_in_term",
  1540                                "too many nested definitions (" ^
  1541                                string_of_int depth ^ ") while expanding " ^
  1542                                quote s)
  1543                 else if s = @{const_name wfrec'} then
  1544                   (do_term (depth + 1) Ts (betapplys (def, ts)), [])
  1545                 else
  1546                   (do_term (depth + 1) Ts def, ts)
  1547               | NONE => (Const x, ts)
  1548         in s_betapplys (const, map (do_term depth Ts) ts) |> Envir.beta_norm end
  1549   in do_term 0 [] end
  1550 
  1551 (* extended_context -> typ -> term list *)
  1552 fun codatatype_bisim_axioms (ext_ctxt as {thy, ...}) T =
  1553   let
  1554     val xs = datatype_constrs ext_ctxt T
  1555     val set_T = T --> bool_T
  1556     val iter_T = @{typ bisim_iterator}
  1557     val bisim_const = Const (@{const_name bisim}, [iter_T, T, T] ---> bool_T)
  1558     val bisim_max = @{const bisim_iterator_max}
  1559     val n_var = Var (("n", 0), iter_T)
  1560     val n_var_minus_1 =
  1561       Const (@{const_name Tha}, (iter_T --> bool_T) --> iter_T)
  1562       $ Abs ("m", iter_T, HOLogic.eq_const iter_T
  1563                           $ (suc_const iter_T $ Bound 0) $ n_var)
  1564     val x_var = Var (("x", 0), T)
  1565     val y_var = Var (("y", 0), T)
  1566     (* styp -> int -> typ -> term *)
  1567     fun nth_sub_bisim x n nth_T =
  1568       (if is_codatatype thy nth_T then bisim_const $ n_var_minus_1
  1569        else HOLogic.eq_const nth_T)
  1570       $ select_nth_constr_arg thy x x_var n nth_T
  1571       $ select_nth_constr_arg thy x y_var n nth_T
  1572     (* styp -> term *)
  1573     fun case_func (x as (_, T)) =
  1574       let
  1575         val arg_Ts = binder_types T
  1576         val core_t =
  1577           discriminate_value ext_ctxt x y_var ::
  1578           map2 (nth_sub_bisim x) (index_seq 0 (length arg_Ts)) arg_Ts
  1579           |> foldr1 s_conj
  1580       in List.foldr absdummy core_t arg_Ts end
  1581   in
  1582     [HOLogic.eq_const bool_T $ (bisim_const $ n_var $ x_var $ y_var)
  1583      $ (@{term "op |"} $ (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T)
  1584         $ (betapplys (optimized_case_def ext_ctxt T bool_T,
  1585                       map case_func xs @ [x_var]))),
  1586      HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var)
  1587      $ (Const (@{const_name insert}, [T, set_T] ---> set_T)
  1588         $ x_var $ Const (@{const_name bot_fun_inst.bot_fun}, set_T))]
  1589     |> map HOLogic.mk_Trueprop
  1590   end
  1591 
  1592 exception NO_TRIPLE of unit
  1593 
  1594 (* theory -> styp -> term -> term list * term list * term *)
  1595 fun triple_for_intro_rule thy x t =
  1596   let
  1597     val prems = Logic.strip_imp_prems t |> map (ObjectLogic.atomize_term thy)
  1598     val concl = Logic.strip_imp_concl t |> ObjectLogic.atomize_term thy
  1599     val (main, side) = List.partition (exists_Const (equal x)) prems
  1600     (* term -> bool *)
  1601      val is_good_head = equal (Const x) o head_of
  1602   in
  1603     if forall is_good_head main then (side, main, concl) else raise NO_TRIPLE ()
  1604   end
  1605 
  1606 (* term -> term *)
  1607 val tuple_for_args = HOLogic.mk_tuple o snd o strip_comb
  1608 
  1609 (* indexname * typ -> term list -> term -> term -> term *)
  1610 fun wf_constraint_for rel side concl main =
  1611   let
  1612     val core = HOLogic.mk_mem (HOLogic.mk_prod (tuple_for_args main,
  1613                                                 tuple_for_args concl), Var rel)
  1614     val t = List.foldl HOLogic.mk_imp core side
  1615     val vars = filter (not_equal rel) (Term.add_vars t [])
  1616   in
  1617     Library.foldl (fn (t', ((x, j), T)) =>
  1618                       HOLogic.all_const T
  1619                       $ Abs (x, T, abstract_over (Var ((x, j), T), t')))
  1620                   (t, vars)
  1621   end
  1622 
  1623 (* indexname * typ -> term list * term list * term -> term *)
  1624 fun wf_constraint_for_triple rel (side, main, concl) =
  1625   map (wf_constraint_for rel side concl) main |> foldr1 s_conj
  1626 
  1627 (* Proof.context -> Time.time option -> thm
  1628    -> (Proof.context -> tactic -> tactic) -> bool *)
  1629 fun terminates_by ctxt timeout goal tac =
  1630   can (SINGLE (Classical.safe_tac (claset_of ctxt)) #> the
  1631        #> SINGLE (DETERM_TIMEOUT timeout
  1632                                  (tac ctxt (auto_tac (clasimpset_of ctxt))))
  1633        #> the #> Goal.finish ctxt) goal
  1634 
  1635 val max_cached_wfs = 100
  1636 val cached_timeout = Unsynchronized.ref (SOME Time.zeroTime)
  1637 val cached_wf_props : (term * bool) list Unsynchronized.ref =
  1638   Unsynchronized.ref []
  1639 
  1640 val termination_tacs = [Lexicographic_Order.lex_order_tac true,
  1641                         ScnpReconstruct.sizechange_tac]
  1642 
  1643 (* extended_context -> const_table -> styp -> bool *)
  1644 fun uncached_is_well_founded_inductive_pred
  1645         ({thy, ctxt, debug, fast_descrs, tac_timeout, intro_table, ...}
  1646          : extended_context) (x as (_, T)) =
  1647   case def_props_for_const thy fast_descrs intro_table x of
  1648     [] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
  1649                       [Const x])
  1650   | intro_ts =>
  1651     (case map (triple_for_intro_rule thy x) intro_ts
  1652           |> filter_out (null o #2) of
  1653        [] => true
  1654      | triples =>
  1655        let
  1656          val binders_T = HOLogic.mk_tupleT (binder_types T)
  1657          val rel_T = HOLogic.mk_prodT (binders_T, binders_T) --> bool_T
  1658          val j = List.foldl Int.max 0 (map maxidx_of_term intro_ts) + 1
  1659          val rel = (("R", j), rel_T)
  1660          val prop = Const (@{const_name wf}, rel_T --> bool_T) $ Var rel ::
  1661                     map (wf_constraint_for_triple rel) triples
  1662                     |> foldr1 s_conj |> HOLogic.mk_Trueprop
  1663          val _ = if debug then
  1664                    priority ("Wellfoundedness goal: " ^
  1665                              Syntax.string_of_term ctxt prop ^ ".")
  1666                  else
  1667                    ()
  1668        in
  1669          if tac_timeout = (!cached_timeout)
  1670             andalso length (!cached_wf_props) < max_cached_wfs then
  1671            ()
  1672          else
  1673            (cached_wf_props := []; cached_timeout := tac_timeout);
  1674          case AList.lookup (op =) (!cached_wf_props) prop of
  1675            SOME wf => wf
  1676          | NONE =>
  1677            let
  1678              val goal = prop |> cterm_of thy |> Goal.init
  1679              val wf = exists (terminates_by ctxt tac_timeout goal)
  1680                              termination_tacs
  1681            in Unsynchronized.change cached_wf_props (cons (prop, wf)); wf end
  1682        end)
  1683     handle List.Empty => false
  1684          | NO_TRIPLE () => false
  1685 
  1686 (* The type constraint below is a workaround for a Poly/ML bug. *)
  1687 
  1688 (* extended_context -> styp -> bool *)
  1689 fun is_well_founded_inductive_pred
  1690         (ext_ctxt as {thy, wfs, def_table, wf_cache, ...} : extended_context)
  1691         (x as (s, _)) =
  1692   case triple_lookup (const_match thy) wfs x of
  1693     SOME (SOME b) => b
  1694   | _ => s mem [@{const_name Nats}, @{const_name fold_graph'}]
  1695          orelse case AList.lookup (op =) (!wf_cache) x of
  1696                   SOME (_, wf) => wf
  1697                 | NONE =>
  1698                   let
  1699                     val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
  1700                     val wf = uncached_is_well_founded_inductive_pred ext_ctxt x
  1701                   in
  1702                     Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
  1703                   end
  1704 
  1705 (* typ list -> typ -> typ -> term -> term *)
  1706 fun ap_curry [_] _ _ t = t
  1707   | ap_curry arg_Ts tuple_T body_T t =
  1708     let val n = length arg_Ts in
  1709       list_abs (map (pair "c") arg_Ts,
  1710                 incr_boundvars n t
  1711                 $ mk_flat_tuple tuple_T (map Bound (n - 1 downto 0)))
  1712     end
  1713 
  1714 (* int -> term -> int *)
  1715 fun num_occs_of_bound_in_term j (t1 $ t2) =
  1716     op + (pairself (num_occs_of_bound_in_term j) (t1, t2))
  1717   | num_occs_of_bound_in_term j (Abs (s, T, t')) =
  1718     num_occs_of_bound_in_term (j + 1) t'
  1719   | num_occs_of_bound_in_term j (Bound j') = if j' = j then 1 else 0
  1720   | num_occs_of_bound_in_term _ _ = 0
  1721 
  1722 (* term -> bool *)
  1723 val is_linear_inductive_pred_def =
  1724   let
  1725     (* int -> term -> bool *)
  1726     fun do_disjunct j (Const (@{const_name Ex}, _) $ Abs (_, _, t2)) =
  1727         do_disjunct (j + 1) t2
  1728       | do_disjunct j t =
  1729         case num_occs_of_bound_in_term j t of
  1730           0 => true
  1731         | 1 => exists (equal (Bound j) o head_of) (conjuncts t)
  1732         | _ => false
  1733     (* term -> bool *)
  1734     fun do_lfp_def (Const (@{const_name lfp}, _) $ t2) =
  1735         let val (xs, body) = strip_abs t2 in
  1736           case length xs of
  1737             1 => false
  1738           | n => forall (do_disjunct (n - 1)) (disjuncts body)
  1739         end
  1740       | do_lfp_def _ = false
  1741   in do_lfp_def o strip_abs_body end
  1742 
  1743 (* typ -> typ -> term -> term *)
  1744 fun ap_split tuple_T =
  1745   HOLogic.mk_psplits (HOLogic.flat_tupleT_paths tuple_T) tuple_T
  1746 
  1747 (* term -> term * term *)
  1748 val linear_pred_base_and_step_rhss =
  1749   let
  1750     (* term -> term *)
  1751     fun aux (Const (@{const_name lfp}, _) $ t2) =
  1752         let
  1753           val (xs, body) = strip_abs t2
  1754           val arg_Ts = map snd (tl xs)
  1755           val tuple_T = HOLogic.mk_tupleT arg_Ts
  1756           val j = length arg_Ts
  1757           (* int -> term -> term *)
  1758           fun repair_rec j (Const (@{const_name Ex}, T1) $ Abs (s2, T2, t2')) =
  1759               Const (@{const_name Ex}, T1)
  1760               $ Abs (s2, T2, repair_rec (j + 1) t2')
  1761             | repair_rec j (@{const "op &"} $ t1 $ t2) =
  1762               @{const "op &"} $ repair_rec j t1 $ repair_rec j t2
  1763             | repair_rec j t =
  1764               let val (head, args) = strip_comb t in
  1765                 if head = Bound j then
  1766                   HOLogic.eq_const tuple_T $ Bound j
  1767                   $ mk_flat_tuple tuple_T args
  1768                 else
  1769                   t
  1770               end
  1771           val (nonrecs, recs) =
  1772             List.partition (equal 0 o num_occs_of_bound_in_term j)
  1773                            (disjuncts body)
  1774           val base_body = nonrecs |> List.foldl s_disj @{const False}
  1775           val step_body = recs |> map (repair_rec j)
  1776                                |> List.foldl s_disj @{const False} 
  1777         in
  1778           (list_abs (tl xs, incr_bv (~1, j, base_body))
  1779            |> ap_split tuple_T bool_T,
  1780            Abs ("y", tuple_T, list_abs (tl xs, step_body)
  1781                               |> ap_split tuple_T bool_T))
  1782         end
  1783       | aux t =
  1784         raise TERM ("Nitpick_HOL.linear_pred_base_and_step_rhss.aux", [t])
  1785   in aux end
  1786 
  1787 (* extended_context -> styp -> term -> term *)
  1788 fun closed_linear_pred_const (ext_ctxt as {simp_table, ...}) (x as (s, T)) def =
  1789   let
  1790     val j = maxidx_of_term def + 1
  1791     val (outer, fp_app) = strip_abs def
  1792     val outer_bounds = map Bound (length outer - 1 downto 0)
  1793     val outer_vars = map (fn (s, T) => Var ((s, j), T)) outer
  1794     val fp_app = subst_bounds (rev outer_vars, fp_app)
  1795     val (outer_Ts, rest_T) = strip_n_binders (length outer) T
  1796     val tuple_arg_Ts = strip_type rest_T |> fst
  1797     val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
  1798     val set_T = tuple_T --> bool_T
  1799     val curried_T = tuple_T --> set_T
  1800     val uncurried_T = Type ("*", [tuple_T, tuple_T]) --> bool_T
  1801     val (base_rhs, step_rhs) = linear_pred_base_and_step_rhss fp_app
  1802     val base_x as (base_s, _) = (base_prefix ^ s, outer_Ts ---> set_T)
  1803     val base_eq = HOLogic.mk_eq (list_comb (Const base_x, outer_vars), base_rhs)
  1804                   |> HOLogic.mk_Trueprop
  1805     val _ = add_simps simp_table base_s [base_eq]
  1806     val step_x as (step_s, _) = (step_prefix ^ s, outer_Ts ---> curried_T)
  1807     val step_eq = HOLogic.mk_eq (list_comb (Const step_x, outer_vars), step_rhs)
  1808                   |> HOLogic.mk_Trueprop
  1809     val _ = add_simps simp_table step_s [step_eq]
  1810   in
  1811     list_abs (outer,
  1812               Const (@{const_name Image}, uncurried_T --> set_T --> set_T)
  1813               $ (Const (@{const_name rtrancl}, uncurried_T --> uncurried_T)
  1814                  $ (Const (@{const_name split}, curried_T --> uncurried_T)
  1815                     $ list_comb (Const step_x, outer_bounds)))
  1816               $ list_comb (Const base_x, outer_bounds)
  1817               |> ap_curry tuple_arg_Ts tuple_T bool_T)
  1818     |> unfold_defs_in_term ext_ctxt
  1819   end
  1820 
  1821 (* extended_context -> bool -> styp -> term *)
  1822 fun unrolled_inductive_pred_const (ext_ctxt as {thy, star_linear_preds,
  1823                                                 def_table, simp_table, ...})
  1824                                   gfp (x as (s, T)) =
  1825   let
  1826     val iter_T = iterator_type_for_const gfp x
  1827     val x' as (s', _) = (unrolled_prefix ^ s, iter_T --> T)
  1828     val unrolled_const = Const x' $ zero_const iter_T
  1829     val def = the (def_of_const thy def_table x)
  1830   in
  1831     if is_equational_fun ext_ctxt x' then
  1832       unrolled_const (* already done *)
  1833     else if not gfp andalso is_linear_inductive_pred_def def
  1834          andalso star_linear_preds then
  1835       closed_linear_pred_const ext_ctxt x def
  1836     else
  1837       let
  1838         val j = maxidx_of_term def + 1
  1839         val (outer, fp_app) = strip_abs def
  1840         val outer_bounds = map Bound (length outer - 1 downto 0)
  1841         val cur = Var ((iter_var_prefix, j + 1), iter_T)
  1842         val next = suc_const iter_T $ cur
  1843         val rhs = case fp_app of
  1844                     Const _ $ t =>
  1845                     betapply (t, list_comb (Const x', next :: outer_bounds))
  1846                   | _ => raise TERM ("Nitpick_HOL.unrolled_inductive_pred_\
  1847                                      \const", [fp_app])
  1848         val (inner, naked_rhs) = strip_abs rhs
  1849         val all = outer @ inner
  1850         val bounds = map Bound (length all - 1 downto 0)
  1851         val vars = map (fn (s, T) => Var ((s, j), T)) all
  1852         val eq = HOLogic.mk_eq (list_comb (Const x', cur :: bounds), naked_rhs)
  1853                  |> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars)
  1854         val _ = add_simps simp_table s' [eq]
  1855       in unrolled_const end
  1856   end
  1857 
  1858 (* extended_context -> styp -> term *)
  1859 fun raw_inductive_pred_axiom ({thy, def_table, ...} : extended_context) x =
  1860   let
  1861     val def = the (def_of_const thy def_table x)
  1862     val (outer, fp_app) = strip_abs def
  1863     val outer_bounds = map Bound (length outer - 1 downto 0)
  1864     val rhs = case fp_app of
  1865                 Const _ $ t => betapply (t, list_comb (Const x, outer_bounds))
  1866               | _ => raise TERM ("Nitpick_HOL.raw_inductive_pred_axiom",
  1867                                  [fp_app])
  1868     val (inner, naked_rhs) = strip_abs rhs
  1869     val all = outer @ inner
  1870     val bounds = map Bound (length all - 1 downto 0)
  1871     val j = maxidx_of_term def + 1
  1872     val vars = map (fn (s, T) => Var ((s, j), T)) all
  1873   in
  1874     HOLogic.mk_eq (list_comb (Const x, bounds), naked_rhs)
  1875     |> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars)
  1876   end
  1877 fun inductive_pred_axiom ext_ctxt (x as (s, T)) =
  1878   if String.isPrefix ubfp_prefix s orelse String.isPrefix lbfp_prefix s then
  1879     let val x' = (after_name_sep s, T) in
  1880       raw_inductive_pred_axiom ext_ctxt x' |> subst_atomic [(Const x', Const x)]
  1881     end
  1882   else
  1883     raw_inductive_pred_axiom ext_ctxt x
  1884 
  1885 (* extended_context -> styp -> term list *)
  1886 fun raw_equational_fun_axioms (ext_ctxt as {thy, fast_descrs, simp_table,
  1887                                             psimp_table, ...}) (x as (s, _)) =
  1888   case def_props_for_const thy fast_descrs (!simp_table) x of
  1889     [] => (case def_props_for_const thy fast_descrs psimp_table x of
  1890              [] => [inductive_pred_axiom ext_ctxt x]
  1891            | psimps => psimps)
  1892   | simps => simps
  1893 
  1894 val equational_fun_axioms = map extensionalize oo raw_equational_fun_axioms
  1895 
  1896 (* term list -> term list *)
  1897 fun merge_type_vars_in_terms ts =
  1898   let
  1899     (* typ -> (sort * string) list -> (sort * string) list *)
  1900     fun add_type (TFree (s, S)) table =
  1901         (case AList.lookup (op =) table S of
  1902            SOME s' =>
  1903            if string_ord (s', s) = LESS then AList.update (op =) (S, s') table
  1904            else table
  1905          | NONE => (S, s) :: table)
  1906       | add_type _ table = table
  1907     val table = fold (fold_types (fold_atyps add_type)) ts []
  1908     (* typ -> typ *)
  1909     fun coalesce (TFree (s, S)) = TFree (AList.lookup (op =) table S |> the, S)
  1910       | coalesce T = T
  1911   in map (map_types (map_atyps coalesce)) ts end
  1912 
  1913 (* extended_context -> typ -> typ list -> typ list *)
  1914 fun add_ground_types ext_ctxt T accum =
  1915   case T of
  1916     Type ("fun", Ts) => fold (add_ground_types ext_ctxt) Ts accum
  1917   | Type ("*", Ts) => fold (add_ground_types ext_ctxt) Ts accum
  1918   | Type (@{type_name itself}, [T1]) => add_ground_types ext_ctxt T1 accum
  1919   | Type (_, Ts) =>
  1920     if T mem @{typ prop} :: @{typ bool} :: @{typ unit} :: accum then
  1921       accum
  1922     else
  1923       T :: accum
  1924       |> fold (add_ground_types ext_ctxt)
  1925               (case boxed_datatype_constrs ext_ctxt T of
  1926                  [] => Ts
  1927                | xs => map snd xs)
  1928   | _ => insert (op =) T accum
  1929 (* extended_context -> typ -> typ list *)
  1930 fun ground_types_in_type ext_ctxt T = add_ground_types ext_ctxt T []
  1931 (* extended_context -> term list -> typ list *)
  1932 fun ground_types_in_terms ext_ctxt ts =
  1933   fold (fold_types (add_ground_types ext_ctxt)) ts []
  1934 
  1935 (* typ list -> int -> term -> bool *)
  1936 fun has_heavy_bounds_or_vars Ts level t =
  1937   let
  1938     (* typ list -> bool *)
  1939     fun aux [] = false
  1940       | aux [T] = is_fun_type T orelse is_pair_type T
  1941       | aux _ = true
  1942   in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
  1943 
  1944 (* typ list -> int -> int -> int -> term -> term *)
  1945 fun fresh_value_var Ts k n j t =
  1946   Var ((val_var_prefix ^ nat_subscript (n - j), k), fastype_of1 (Ts, t))
  1947 
  1948 (* theory -> typ list -> bool -> int -> int -> term -> term list -> term list
  1949    -> term * term list *)
  1950 fun pull_out_constr_comb thy Ts relax k level t args seen =
  1951   let val t_comb = list_comb (t, args) in
  1952     case t of
  1953       Const x =>
  1954       if not relax andalso is_constr thy x
  1955          andalso not (is_fun_type (fastype_of1 (Ts, t_comb)))
  1956          andalso has_heavy_bounds_or_vars Ts level t_comb
  1957          andalso not (loose_bvar (t_comb, level)) then
  1958         let
  1959           val (j, seen) = case find_index (equal t_comb) seen of
  1960                             ~1 => (0, t_comb :: seen)
  1961                           | j => (j, seen)
  1962         in (fresh_value_var Ts k (length seen) j t_comb, seen) end
  1963       else
  1964         (t_comb, seen)
  1965     | _ => (t_comb, seen)
  1966   end
  1967 
  1968 (* (term -> term) -> typ list -> int -> term list -> term list *)
  1969 fun equations_for_pulled_out_constrs mk_eq Ts k seen =
  1970   let val n = length seen in
  1971     map2 (fn j => fn t => mk_eq (fresh_value_var Ts k n j t, t))
  1972          (index_seq 0 n) seen
  1973   end
  1974 
  1975 (* theory -> bool -> term -> term *)
  1976 fun pull_out_universal_constrs thy def t =
  1977   let
  1978     val k = maxidx_of_term t + 1
  1979     (* typ list -> bool -> term -> term list -> term list -> term * term list *)
  1980     fun do_term Ts def t args seen =
  1981       case t of
  1982         (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 =>
  1983         do_eq_or_imp Ts def t0 t1 t2 seen
  1984       | (t0 as @{const "==>"}) $ t1 $ t2 => do_eq_or_imp Ts def t0 t1 t2 seen
  1985       | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
  1986         do_eq_or_imp Ts def t0 t1 t2 seen
  1987       | (t0 as @{const "op -->"}) $ t1 $ t2 => do_eq_or_imp Ts def t0 t1 t2 seen
  1988       | Abs (s, T, t') =>
  1989         let val (t', seen) = do_term (T :: Ts) def t' [] seen in
  1990           (list_comb (Abs (s, T, t'), args), seen)
  1991         end
  1992       | t1 $ t2 =>
  1993         let val (t2, seen) = do_term Ts def t2 [] seen in
  1994           do_term Ts def t1 (t2 :: args) seen
  1995         end
  1996       | _ => pull_out_constr_comb thy Ts def k 0 t args seen
  1997     (* typ list -> bool -> term -> term -> term -> term list
  1998        -> term * term list *)
  1999     and do_eq_or_imp Ts def t0 t1 t2 seen =
  2000       let
  2001         val (t2, seen) = do_term Ts def t2 [] seen
  2002         val (t1, seen) = do_term Ts false t1 [] seen
  2003       in (t0 $ t1 $ t2, seen) end
  2004     val (concl, seen) = do_term [] def t [] []
  2005   in
  2006     Logic.list_implies (equations_for_pulled_out_constrs Logic.mk_equals [] k
  2007                                                          seen, concl)
  2008   end
  2009 
  2010 (* extended_context -> bool -> term -> term *)
  2011 fun destroy_pulled_out_constrs (ext_ctxt as {thy, ...}) axiom t =
  2012   let
  2013     (* styp -> int *)
  2014     val num_occs_of_var =
  2015       fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
  2016                     | _ => I) t (K 0)
  2017     (* bool -> term -> term *)
  2018     fun aux careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =
  2019         aux_eq careful true t0 t1 t2
  2020       | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =
  2021         t0 $ aux false t1 $ aux careful t2
  2022       | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
  2023         aux_eq careful true t0 t1 t2
  2024       | aux careful ((t0 as @{const "op -->"}) $ t1 $ t2) =
  2025         t0 $ aux false t1 $ aux careful t2
  2026       | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')
  2027       | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2
  2028       | aux _ t = t
  2029     (* bool -> bool -> term -> term -> term -> term *)
  2030     and aux_eq careful pass1 t0 t1 t2 =
  2031       (if careful then
  2032          raise SAME ()
  2033        else if axiom andalso is_Var t2
  2034                andalso num_occs_of_var (dest_Var t2) = 1 then
  2035          @{const True}
  2036        else case strip_comb t2 of
  2037          (Const (x as (s, T)), args) =>
  2038          let val arg_Ts = binder_types T in
  2039            if length arg_Ts = length args
  2040               andalso (is_constr thy x orelse s mem [@{const_name Pair}]
  2041                        orelse x = dest_Const @{const Suc})
  2042               andalso (not careful orelse not (is_Var t1)
  2043                        orelse String.isPrefix val_var_prefix
  2044                                               (fst (fst (dest_Var t1)))) then
  2045              discriminate_value ext_ctxt x t1 ::
  2046              map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
  2047              |> foldr1 s_conj
  2048              |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop
  2049            else
  2050              raise SAME ()
  2051          end
  2052        | _ => raise SAME ())
  2053       handle SAME () => if pass1 then aux_eq careful false t0 t2 t1
  2054                         else t0 $ aux false t2 $ aux false t1
  2055     (* styp -> term -> int -> typ -> term -> term *)
  2056     and sel_eq x t n nth_T nth_t =
  2057       HOLogic.eq_const nth_T $ nth_t $ select_nth_constr_arg thy x t n nth_T
  2058       |> aux false
  2059   in aux axiom t end
  2060 
  2061 (* theory -> term -> term *)
  2062 fun simplify_constrs_and_sels thy t =
  2063   let
  2064     (* term -> int -> term *)
  2065     fun is_nth_sel_on t' n (Const (s, _) $ t) =
  2066         (t = t' andalso is_sel_like_and_no_discr s
  2067          andalso sel_no_from_name s = n)
  2068       | is_nth_sel_on _ _ _ = false
  2069     (* term -> term list -> term *)
  2070     fun do_term (Const (@{const_name Rep_Frac}, _)
  2071                  $ (Const (@{const_name Abs_Frac}, _) $ t1)) [] = do_term t1 []
  2072       | do_term (Const (@{const_name Abs_Frac}, _)
  2073                  $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 []
  2074       | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)
  2075       | do_term (t as Const (x as (s, T))) (args as _ :: _) =
  2076         ((if is_constr_like thy x then
  2077             if length args = num_binder_types T then
  2078               case hd args of
  2079                 Const (x' as (_, T')) $ t' =>
  2080                 if domain_type T' = body_type T
  2081                    andalso forall (uncurry (is_nth_sel_on t'))
  2082                                   (index_seq 0 (length args) ~~ args) then
  2083                   t'
  2084                 else
  2085                   raise SAME ()
  2086               | _ => raise SAME ()
  2087             else
  2088               raise SAME ()
  2089           else if is_sel_like_and_no_discr s then
  2090             case strip_comb (hd args) of
  2091               (Const (x' as (s', T')), ts') =>
  2092               if is_constr_like thy x'
  2093                  andalso constr_name_for_sel_like s = s'
  2094                  andalso not (exists is_pair_type (binder_types T')) then
  2095                 list_comb (nth ts' (sel_no_from_name s), tl args)
  2096               else
  2097                 raise SAME ()
  2098             | _ => raise SAME ()
  2099           else
  2100             raise SAME ())
  2101          handle SAME () => betapplys (t, args))
  2102       | do_term (Abs (s, T, t')) args =
  2103         betapplys (Abs (s, T, do_term t' []), args)
  2104       | do_term t args = betapplys (t, args)
  2105   in do_term t [] end
  2106 
  2107 (* term -> term *)
  2108 fun curry_assms (@{const "==>"} $ (@{const Trueprop}
  2109                                    $ (@{const "op &"} $ t1 $ t2)) $ t3) =
  2110     curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
  2111   | curry_assms (@{const "==>"} $ t1 $ t2) =
  2112     @{const "==>"} $ curry_assms t1 $ curry_assms t2
  2113   | curry_assms t = t
  2114 
  2115 (* term -> term *)
  2116 val destroy_universal_equalities =
  2117   let
  2118     (* term list -> (indexname * typ) list -> term -> term *)
  2119     fun aux prems zs t =
  2120       case t of
  2121         @{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2
  2122       | _ => Logic.list_implies (rev prems, t)
  2123     (* term list -> (indexname * typ) list -> term -> term -> term *)
  2124     and aux_implies prems zs t1 t2 =
  2125       case t1 of
  2126         Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
  2127       | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') =>
  2128         aux_eq prems zs z t' t1 t2
  2129       | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) =>
  2130         aux_eq prems zs z t' t1 t2
  2131       | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
  2132     (* term list -> (indexname * typ) list -> indexname * typ -> term -> term
  2133        -> term -> term *)
  2134     and aux_eq prems zs z t' t1 t2 =
  2135       if not (z mem zs) andalso not (exists_subterm (equal (Var z)) t') then
  2136         aux prems zs (subst_free [(Var z, t')] t2)
  2137       else
  2138         aux (t1 :: prems) (Term.add_vars t1 zs) t2
  2139   in aux [] [] end
  2140 
  2141 (* theory -> term -> term *)
  2142 fun pull_out_existential_constrs thy t =
  2143   let
  2144     val k = maxidx_of_term t + 1
  2145     (* typ list -> int -> term -> term list -> term list -> term * term list *)
  2146     fun aux Ts num_exists t args seen =
  2147       case t of
  2148         (t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1) =>
  2149         let
  2150           val (t1, seen') = aux (T1 :: Ts) (num_exists + 1) t1 [] []
  2151           val n = length seen'
  2152           (* unit -> term list *)
  2153           fun vars () = map2 (fresh_value_var Ts k n) (index_seq 0 n) seen'
  2154         in
  2155           (equations_for_pulled_out_constrs HOLogic.mk_eq Ts k seen'
  2156            |> List.foldl s_conj t1 |> fold mk_exists (vars ())
  2157            |> curry3 Abs s1 T1 |> curry (op $) t0, seen)
  2158         end
  2159       | t1 $ t2 =>
  2160         let val (t2, seen) = aux Ts num_exists t2 [] seen in
  2161           aux Ts num_exists t1 (t2 :: args) seen
  2162         end
  2163       | Abs (s, T, t') =>
  2164         let
  2165           val (t', seen) = aux (T :: Ts) 0 t' [] (map (incr_boundvars 1) seen)
  2166         in (list_comb (Abs (s, T, t'), args), map (incr_boundvars ~1) seen) end
  2167       | _ =>
  2168         if num_exists > 0 then
  2169           pull_out_constr_comb thy Ts false k num_exists t args seen
  2170         else
  2171           (list_comb (t, args), seen)
  2172   in aux [] 0 t [] [] |> fst end
  2173 
  2174 (* theory -> int -> term list -> term list -> (term * term list) option *)
  2175 fun find_bound_assign _ _ _ [] = NONE
  2176   | find_bound_assign thy j seen (t :: ts) =
  2177     let
  2178       (* bool -> term -> term -> (term * term list) option *)
  2179       fun aux pass1 t1 t2 =
  2180         (if loose_bvar1 (t2, j) then
  2181            if pass1 then aux false t2 t1 else raise SAME ()
  2182          else case t1 of
  2183            Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()
  2184          | Const (s, Type ("fun", [T1, T2])) $ Bound j' =>
  2185            if j' = j andalso s = sel_prefix_for 0 ^ @{const_name FunBox} then
  2186              SOME (construct_value thy (@{const_name FunBox}, T2 --> T1) [t2],
  2187                    ts @ seen)
  2188            else
  2189              raise SAME ()
  2190          | _ => raise SAME ())
  2191         handle SAME () => find_bound_assign thy j (t :: seen) ts
  2192     in
  2193       case t of
  2194         Const (@{const_name "op ="}, _) $ t1 $ t2 => aux true t1 t2
  2195       | _ => find_bound_assign thy j (t :: seen) ts
  2196     end
  2197 
  2198 (* int -> term -> term -> term *)
  2199 fun subst_one_bound j arg t =
  2200   let
  2201     fun aux (Bound i, lev) =
  2202         if i < lev then raise SAME ()
  2203         else if i = lev then incr_boundvars (lev - j) arg
  2204         else Bound (i - 1)
  2205       | aux (Abs (a, T, body), lev) = Abs (a, T, aux (body, lev + 1))
  2206       | aux (f $ t, lev) =
  2207         (aux (f, lev) $ (aux (t, lev) handle SAME () => t)
  2208          handle SAME () => f $ aux (t, lev))
  2209       | aux _ = raise SAME ()
  2210   in aux (t, j) handle SAME () => t end
  2211 
  2212 (* theory -> term -> term *)
  2213 fun destroy_existential_equalities thy =
  2214   let
  2215     (* string list -> typ list -> term list -> term *)
  2216     fun kill [] [] ts = foldr1 s_conj ts
  2217       | kill (s :: ss) (T :: Ts) ts =
  2218         (case find_bound_assign thy (length ss) [] ts of
  2219            SOME (_, []) => @{const True}
  2220          | SOME (arg_t, ts) =>
  2221            kill ss Ts (map (subst_one_bound (length ss)
  2222                                 (incr_bv (~1, length ss + 1, arg_t))) ts)
  2223          | NONE =>
  2224            Const (@{const_name Ex}, (T --> bool_T) --> bool_T)
  2225            $ Abs (s, T, kill ss Ts ts))
  2226       | kill _ _ _ = raise UnequalLengths
  2227     (* string list -> typ list -> term -> term *)
  2228     fun gather ss Ts ((t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1)) =
  2229         gather (ss @ [s1]) (Ts @ [T1]) t1
  2230       | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)
  2231       | gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2
  2232       | gather [] [] t = t
  2233       | gather ss Ts t = kill ss Ts (conjuncts (gather [] [] t))
  2234   in gather [] [] end
  2235 
  2236 (* term -> term *)
  2237 fun distribute_quantifiers t =
  2238   case t of
  2239     (t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) =>
  2240     (case t1 of
  2241        (t10 as @{const "op &"}) $ t11 $ t12 =>
  2242        t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
  2243            $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
  2244      | (t10 as @{const Not}) $ t11 =>
  2245        t10 $ distribute_quantifiers (Const (@{const_name Ex}, T0)
  2246                                      $ Abs (s, T1, t11))
  2247      | t1 =>
  2248        if not (loose_bvar1 (t1, 0)) then
  2249          distribute_quantifiers (incr_boundvars ~1 t1)
  2250        else
  2251          t0 $ Abs (s, T1, distribute_quantifiers t1))
  2252   | (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) =>
  2253     (case distribute_quantifiers t1 of
  2254        (t10 as @{const "op |"}) $ t11 $ t12 =>
  2255        t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
  2256            $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
  2257      | (t10 as @{const "op -->"}) $ t11 $ t12 =>
  2258        t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
  2259                                      $ Abs (s, T1, t11))
  2260            $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
  2261      | (t10 as @{const Not}) $ t11 =>
  2262        t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
  2263                                      $ Abs (s, T1, t11))
  2264      | t1 =>
  2265        if not (loose_bvar1 (t1, 0)) then
  2266          distribute_quantifiers (incr_boundvars ~1 t1)
  2267        else
  2268          t0 $ Abs (s, T1, distribute_quantifiers t1))
  2269   | t1 $ t2 => distribute_quantifiers t1 $ distribute_quantifiers t2
  2270   | Abs (s, T, t') => Abs (s, T, distribute_quantifiers t')
  2271   | _ => t
  2272 
  2273 (* int -> int -> (int -> int) -> term -> term *)
  2274 fun renumber_bounds j n f t =
  2275   case t of
  2276     t1 $ t2 => renumber_bounds j n f t1 $ renumber_bounds j n f t2
  2277   | Abs (s, T, t') => Abs (s, T, renumber_bounds (j + 1) n f t')
  2278   | Bound j' =>
  2279     Bound (if j' >= j andalso j' < j + n then f (j' - j) + j else j')
  2280   | _ => t
  2281 
  2282 val quantifier_cluster_max_size = 8
  2283 
  2284 (* theory -> term -> term *)
  2285 fun push_quantifiers_inward thy =
  2286   let
  2287     (* string -> string list -> typ list -> term -> term *)
  2288     fun aux quant_s ss Ts t =
  2289       (case t of
  2290          (t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) =>
  2291          if s0 = quant_s andalso length Ts < quantifier_cluster_max_size then
  2292            aux s0 (s1 :: ss) (T1 :: Ts) t1
  2293          else if quant_s = ""
  2294                  andalso s0 mem [@{const_name All}, @{const_name Ex}] then
  2295            aux s0 [s1] [T1] t1
  2296          else
  2297            raise SAME ()
  2298        | _ => raise SAME ())
  2299       handle SAME () =>
  2300              case t of
  2301                t1 $ t2 =>
  2302                if quant_s = "" then
  2303                  aux "" [] [] t1 $ aux "" [] [] t2
  2304                else
  2305                  let
  2306                    val typical_card = 4
  2307                    (* ('a -> ''b list) -> 'a list -> ''b list *)
  2308                    fun big_union proj ps =
  2309                      fold (fold (insert (op =)) o proj) ps []
  2310                    val (ts, connective) = strip_any_connective t
  2311                    val T_costs =
  2312                      map (bounded_card_of_type 65536 typical_card []) Ts
  2313                    val t_costs = map size_of_term ts
  2314                    val num_Ts = length Ts
  2315                    (* int -> int *)
  2316                    val flip = curry (op -) (num_Ts - 1)
  2317                    val t_boundss = map (map flip o loose_bnos) ts
  2318                    (* (int list * int) list -> int list -> int *)
  2319                    fun cost boundss_cum_costs [] =
  2320                        map snd boundss_cum_costs |> Integer.sum
  2321                      | cost boundss_cum_costs (j :: js) =
  2322                        let
  2323                          val (yeas, nays) =
  2324                            List.partition (fn (bounds, _) => j mem bounds)
  2325                                           boundss_cum_costs
  2326                          val yeas_bounds = big_union fst yeas
  2327                          val yeas_cost = Integer.sum (map snd yeas)
  2328                                          * nth T_costs j
  2329                        in cost ((yeas_bounds, yeas_cost) :: nays) js end
  2330                    val js = all_permutations (index_seq 0 num_Ts)
  2331                             |> map (`(cost (t_boundss ~~ t_costs)))
  2332                             |> sort (int_ord o pairself fst) |> hd |> snd
  2333                    val back_js = map (fn j => find_index (equal j) js)
  2334                                      (index_seq 0 num_Ts)
  2335                    val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip))
  2336                                 ts
  2337                    (* (term * int list) list -> term *)
  2338                    fun mk_connection [] =
  2339                        raise ARG ("Nitpick_HOL.push_quantifiers_inward.aux.\
  2340                                   \mk_connection", "")
  2341                      | mk_connection ts_cum_bounds =
  2342                        ts_cum_bounds |> map fst
  2343                        |> foldr1 (fn (t1, t2) => connective $ t1 $ t2)
  2344                    (* (term * int list) list -> int list -> term *)
  2345                    fun build ts_cum_bounds [] = ts_cum_bounds |> mk_connection
  2346                      | build ts_cum_bounds (j :: js) =
  2347                        let
  2348                          val (yeas, nays) =
  2349                            List.partition (fn (_, bounds) => j mem bounds)
  2350                                           ts_cum_bounds
  2351                            ||> map (apfst (incr_boundvars ~1))
  2352                        in
  2353                          if null yeas then
  2354                            build nays js
  2355                          else
  2356                            let val T = nth Ts (flip j) in
  2357                              build ((Const (quant_s, (T --> bool_T) --> bool_T)
  2358                                      $ Abs (nth ss (flip j), T,
  2359                                             mk_connection yeas),
  2360                                       big_union snd yeas) :: nays) js
  2361                            end
  2362                        end
  2363                  in build (ts ~~ t_boundss) js end
  2364              | Abs (s, T, t') => Abs (s, T, aux "" [] [] t')
  2365              | _ => t
  2366   in aux "" [] [] end
  2367 
  2368 (* polarity -> string -> bool *)
  2369 fun is_positive_existential polar quant_s =
  2370   (polar = Pos andalso quant_s = @{const_name Ex})
  2371   orelse (polar = Neg andalso quant_s <> @{const_name Ex})
  2372 
  2373 (* extended_context -> int -> term -> term *)
  2374 fun skolemize_term_and_more (ext_ctxt as {thy, def_table, skolems, ...})
  2375                             skolem_depth =
  2376   let
  2377     (* int list -> int list *)
  2378     val incrs = map (Integer.add 1)
  2379     (* string list -> typ list -> int list -> int -> polarity -> term -> term *)
  2380     fun aux ss Ts js depth polar t =
  2381       let
  2382         (* string -> typ -> string -> typ -> term -> term *)
  2383         fun do_quantifier quant_s quant_T abs_s abs_T t =
  2384           if not (loose_bvar1 (t, 0)) then
  2385             aux ss Ts js depth polar (incr_boundvars ~1 t)
  2386           else if depth <= skolem_depth
  2387                   andalso is_positive_existential polar quant_s then
  2388             let
  2389               val j = length (!skolems) + 1
  2390               val sko_s = skolem_prefix_for (length js) j ^ abs_s
  2391               val _ = Unsynchronized.change skolems (cons (sko_s, ss))
  2392               val sko_t = list_comb (Const (sko_s, rev Ts ---> abs_T),
  2393                                      map Bound (rev js))
  2394               val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) depth polar t)
  2395             in
  2396               if null js then betapply (abs_t, sko_t)
  2397               else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t $ abs_t
  2398             end
  2399           else
  2400             Const (quant_s, quant_T)
  2401             $ Abs (abs_s, abs_T,
  2402                    if is_higher_order_type abs_T then
  2403                      t
  2404                    else
  2405                      aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js)
  2406                          (depth + 1) polar t)
  2407       in
  2408         case t of
  2409           Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
  2410           do_quantifier s0 T0 s1 T1 t1
  2411         | @{const "==>"} $ t1 $ t2 =>
  2412           @{const "==>"} $ aux ss Ts js depth (flip_polarity polar) t1
  2413           $ aux ss Ts js depth polar t2
  2414         | @{const Pure.conjunction} $ t1 $ t2 =>
  2415           @{const Pure.conjunction} $ aux ss Ts js depth polar t1
  2416           $ aux ss Ts js depth polar t2
  2417         | @{const Trueprop} $ t1 =>
  2418           @{const Trueprop} $ aux ss Ts js depth polar t1
  2419         | @{const Not} $ t1 =>
  2420           @{const Not} $ aux ss Ts js depth (flip_polarity polar) t1
  2421         | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
  2422           do_quantifier s0 T0 s1 T1 t1
  2423         | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
  2424           do_quantifier s0 T0 s1 T1 t1
  2425         | @{const "op &"} $ t1 $ t2 =>
  2426           @{const "op &"} $ aux ss Ts js depth polar t1
  2427           $ aux ss Ts js depth polar t2
  2428         | @{const "op |"} $ t1 $ t2 =>
  2429           @{const "op |"} $ aux ss Ts js depth polar t1
  2430           $ aux ss Ts js depth polar t2
  2431         | @{const "op -->"} $ t1 $ t2 =>
  2432           @{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1
  2433           $ aux ss Ts js depth polar t2
  2434         | (t0 as Const (@{const_name Let}, T0)) $ t1 $ t2 =>
  2435           t0 $ t1 $ aux ss Ts js depth polar t2
  2436         | Const (x as (s, T)) =>
  2437           if is_inductive_pred ext_ctxt x
  2438              andalso not (is_well_founded_inductive_pred ext_ctxt x) then
  2439             let
  2440               val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
  2441               val (pref, connective, set_oper) =
  2442                 if gfp then
  2443                   (lbfp_prefix,
  2444                    @{const "op |"},
  2445                    @{const_name upper_semilattice_fun_inst.sup_fun})
  2446                 else
  2447                   (ubfp_prefix,
  2448                    @{const "op &"},
  2449                    @{const_name lower_semilattice_fun_inst.inf_fun})
  2450               (* unit -> term *)
  2451               fun pos () = unrolled_inductive_pred_const ext_ctxt gfp x
  2452                            |> aux ss Ts js depth polar
  2453               fun neg () = Const (pref ^ s, T)
  2454             in
  2455               (case polar |> gfp ? flip_polarity of
  2456                  Pos => pos ()
  2457                | Neg => neg ()
  2458                | Neut =>
  2459                  if is_fun_type T then
  2460                    let
  2461                      val ((trunk_arg_Ts, rump_arg_T), body_T) =
  2462                        T |> strip_type |>> split_last
  2463                      val set_T = rump_arg_T --> body_T
  2464                      (* (unit -> term) -> term *)
  2465                      fun app f =
  2466                        list_comb (f (),
  2467                                   map Bound (length trunk_arg_Ts - 1 downto 0))
  2468                    in
  2469                      List.foldl absdummy
  2470                                 (Const (set_oper, [set_T, set_T] ---> set_T)
  2471                                         $ app pos $ app neg) trunk_arg_Ts
  2472                    end
  2473                  else
  2474                    connective $ pos () $ neg ())
  2475             end
  2476           else
  2477             Const x
  2478         | t1 $ t2 =>
  2479           betapply (aux ss Ts [] (skolem_depth + 1) polar t1,
  2480                     aux ss Ts [] depth Neut t2)
  2481         | Abs (s, T, t1) => Abs (s, T, aux ss Ts (incrs js) depth polar t1)
  2482         | _ => t
  2483       end
  2484   in aux [] [] [] 0 Pos end
  2485 
  2486 (* extended_context -> styp -> (int * term option) list *)
  2487 fun static_args_in_term ({ersatz_table, ...} : extended_context) x t =
  2488   let
  2489     (* term -> term list -> term list -> term list list *)
  2490     fun fun_calls (Abs (_, _, t)) _ = fun_calls t []
  2491       | fun_calls (t1 $ t2) args = fun_calls t2 [] #> fun_calls t1 (t2 :: args)
  2492       | fun_calls t args =
  2493         (case t of
  2494            Const (x' as (s', T')) =>
  2495            x = x' orelse (case AList.lookup (op =) ersatz_table s' of
  2496                             SOME s'' => x = (s'', T')
  2497                           | NONE => false)
  2498          | _ => false) ? cons args
  2499     (* term list list -> term list list -> term list -> term list list *)
  2500     fun call_sets [] [] vs = [vs]
  2501       | call_sets [] uss vs = vs :: call_sets uss [] []
  2502       | call_sets ([] :: _) _ _ = []
  2503       | call_sets ((t :: ts) :: tss) uss vs =
  2504         OrdList.insert TermOrd.term_ord t vs |> call_sets tss (ts :: uss)
  2505     val sets = call_sets (fun_calls t [] []) [] []
  2506     val indexed_sets = sets ~~ (index_seq 0 (length sets))
  2507   in
  2508     fold_rev (fn (set, j) =>
  2509                  case set of
  2510                    [Var _] => AList.lookup (op =) indexed_sets set = SOME j
  2511                               ? cons (j, NONE)
  2512                  | [t as Const _] => cons (j, SOME t)
  2513                  | [t as Free _] => cons (j, SOME t)
  2514                  | _ => I) indexed_sets []
  2515   end
  2516 (* extended_context -> styp -> term list -> (int * term option) list *)
  2517 fun static_args_in_terms ext_ctxt x =
  2518   map (static_args_in_term ext_ctxt x)
  2519   #> fold1 (OrdList.inter (prod_ord int_ord (option_ord TermOrd.term_ord)))
  2520 
  2521 (* term -> term list *)
  2522 fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2
  2523   | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
  2524   | params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) =
  2525     snd (strip_comb t1)
  2526   | params_in_equation _ = []
  2527 
  2528 (* styp -> styp -> int list -> term list -> term list -> term -> term *)
  2529 fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t =
  2530   let
  2531     val k = fold Integer.max (map maxidx_of_term (fixed_args @ extra_args)) 0
  2532             + 1
  2533     val t = map_aterms (fn Var ((s, i), T) => Var ((s, k + i), T) | t' => t') t
  2534     val fixed_params = filter_indices fixed_js (params_in_equation t)
  2535     (* term list -> term -> term *)
  2536     fun aux args (Abs (s, T, t)) = list_comb (Abs (s, T, aux [] t), args)
  2537       | aux args (t1 $ t2) = aux (aux [] t2 :: args) t1
  2538       | aux args t =
  2539         if t = Const x then
  2540           list_comb (Const x', extra_args @ filter_out_indices fixed_js args)
  2541         else
  2542           let val j = find_index (equal t) fixed_params in
  2543             list_comb (if j >= 0 then nth fixed_args j else t, args)
  2544           end
  2545   in aux [] t end
  2546 
  2547 (* typ list -> term -> bool *)
  2548 fun is_eligible_arg Ts t =
  2549   let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in
  2550     null bad_Ts
  2551     orelse (is_higher_order_type (fastype_of1 (Ts, t))
  2552             andalso forall (not o is_higher_order_type) bad_Ts)
  2553   end
  2554 
  2555 (* (int * term option) list -> (int * term) list -> int list *)
  2556 fun overlapping_indices [] _ = []
  2557   | overlapping_indices _ [] = []
  2558   | overlapping_indices (ps1 as (j1, t1) :: ps1') (ps2 as (j2, t2) :: ps2') =
  2559     if j1 < j2 then overlapping_indices ps1' ps2
  2560     else if j1 > j2 then overlapping_indices ps1 ps2'
  2561     else overlapping_indices ps1' ps2' |> the_default t2 t1 = t2 ? cons j1
  2562 
  2563 val special_depth = 20
  2564 
  2565 (* extended_context -> int -> term -> term *)
  2566 fun specialize_consts_in_term (ext_ctxt as {thy, specialize, simp_table,
  2567                                             special_funs, ...}) depth t =
  2568   if not specialize orelse depth > special_depth then
  2569     t
  2570   else
  2571     let
  2572       val blacklist = if depth = 0 then []
  2573                       else case term_under_def t of Const x => [x] | _ => []
  2574       (* term list -> typ list -> term -> term *)
  2575       fun aux args Ts (Const (x as (s, T))) =
  2576           ((if not (x mem blacklist) andalso not (null args)
  2577                andalso not (String.isPrefix special_prefix s)
  2578                andalso is_equational_fun ext_ctxt x then
  2579               let
  2580                 val eligible_args = filter (is_eligible_arg Ts o snd)
  2581                                            (index_seq 0 (length args) ~~ args)
  2582                 val _ = not (null eligible_args) orelse raise SAME ()
  2583                 val old_axs = equational_fun_axioms ext_ctxt x
  2584                               |> map (destroy_existential_equalities thy)
  2585                 val static_params = static_args_in_terms ext_ctxt x old_axs
  2586                 val fixed_js = overlapping_indices static_params eligible_args
  2587                 val _ = not (null fixed_js) orelse raise SAME ()
  2588                 val fixed_args = filter_indices fixed_js args
  2589                 val vars = fold Term.add_vars fixed_args []
  2590                            |> sort (TermOrd.fast_indexname_ord o pairself fst)
  2591                 val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js))
  2592                                     fixed_args []
  2593                                |> sort int_ord
  2594                 val live_args = filter_out_indices fixed_js args
  2595                 val extra_args = map Var vars @ map Bound bound_js @ live_args
  2596                 val extra_Ts = map snd vars @ filter_indices bound_js Ts
  2597                 val k = maxidx_of_term t + 1
  2598                 (* int -> term *)
  2599                 fun var_for_bound_no j =
  2600                   Var ((bound_var_prefix ^
  2601                         nat_subscript (find_index (equal j) bound_js + 1), k),
  2602                        nth Ts j)
  2603                 val fixed_args_in_axiom =
  2604                   map (curry subst_bounds
  2605                              (map var_for_bound_no (index_seq 0 (length Ts))))
  2606                       fixed_args
  2607               in
  2608                 case AList.lookup (op =) (!special_funs)
  2609                                   (x, fixed_js, fixed_args_in_axiom) of
  2610                   SOME x' => list_comb (Const x', extra_args)
  2611                 | NONE =>
  2612                   let
  2613                     val extra_args_in_axiom =
  2614                       map Var vars @ map var_for_bound_no bound_js
  2615                     val x' as (s', _) =
  2616                       (special_prefix_for (length (!special_funs) + 1) ^ s,
  2617                        extra_Ts @ filter_out_indices fixed_js (binder_types T)
  2618                        ---> body_type T)
  2619                     val new_axs =
  2620                       map (specialize_fun_axiom x x' fixed_js
  2621                                fixed_args_in_axiom extra_args_in_axiom) old_axs
  2622                     val _ =
  2623                       Unsynchronized.change special_funs
  2624                           (cons ((x, fixed_js, fixed_args_in_axiom), x'))
  2625                     val _ = add_simps simp_table s' new_axs
  2626                   in list_comb (Const x', extra_args) end
  2627               end
  2628             else
  2629               raise SAME ())
  2630            handle SAME () => list_comb (Const x, args))
  2631         | aux args Ts (Abs (s, T, t)) =
  2632           list_comb (Abs (s, T, aux [] (T :: Ts) t), args)
  2633         | aux args Ts (t1 $ t2) = aux (aux [] Ts t2 :: args) Ts t1
  2634         | aux args _ t = list_comb (t, args)
  2635     in aux [] [] t end
  2636 
  2637 (* theory -> term -> int Termtab.tab -> int Termtab.tab *)
  2638 fun add_to_uncurry_table thy t =
  2639   let
  2640     (* term -> term list -> int Termtab.tab -> int Termtab.tab *)
  2641     fun aux (t1 $ t2) args table =
  2642         let val table = aux t2 [] table in aux t1 (t2 :: args) table end
  2643       | aux (Abs (_, _, t')) _ table = aux t' [] table
  2644       | aux (t as Const (x as (s, _))) args table =
  2645         if is_built_in_const false x orelse is_constr_like thy x orelse is_sel s
  2646            orelse s = @{const_name Sigma} then
  2647           table
  2648         else
  2649           Termtab.map_default (t, 65536) (curry Int.min (length args)) table
  2650       | aux _ _ table = table
  2651   in aux t [] end
  2652 
  2653 (* int Termtab.tab term -> term *)
  2654 fun uncurry_term table t =
  2655   let
  2656     (* term -> term list -> term *)
  2657     fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args)
  2658       | aux (Abs (s, T, t')) args = betapplys (Abs (s, T, aux t' []), args)
  2659       | aux (t as Const (s, T)) args =
  2660         (case Termtab.lookup table t of
  2661            SOME n =>
  2662            if n >= 2 then
  2663              let
  2664                val (arg_Ts, rest_T) = strip_n_binders n T
  2665                val j =
  2666                  if hd arg_Ts = @{typ bisim_iterator}
  2667                     orelse is_fp_iterator_type (hd arg_Ts) then
  2668                    1
  2669                  else case find_index (not_equal bool_T) arg_Ts of
  2670                    ~1 => n
  2671                  | j => j
  2672                val ((before_args, tuple_args), after_args) =
  2673                  args |> chop n |>> chop j
  2674                val ((before_arg_Ts, tuple_arg_Ts), rest_T) =
  2675                  T |> strip_n_binders n |>> chop j
  2676                val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
  2677              in
  2678                if n - j < 2 then
  2679                  betapplys (t, args)
  2680                else
  2681                  betapplys (Const (uncurry_prefix_for (n - j) j ^ s,
  2682                                    before_arg_Ts ---> tuple_T --> rest_T),
  2683                             before_args @ [mk_flat_tuple tuple_T tuple_args] @
  2684                             after_args)
  2685              end
  2686            else
  2687              betapplys (t, args)
  2688          | NONE => betapplys (t, args))
  2689       | aux t args = betapplys (t, args)
  2690   in aux t [] end
  2691 
  2692 (* (term -> term) -> int -> term -> term *)
  2693 fun coerce_bound_no f j t =
  2694   case t of
  2695     t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
  2696   | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
  2697   | Bound j' => if j' = j then f t else t
  2698   | _ => t
  2699 
  2700 (* extended_context -> bool -> term -> term *)
  2701 fun box_fun_and_pair_in_term (ext_ctxt as {thy, fast_descrs, ...}) def orig_t =
  2702   let
  2703     (* typ -> typ *)
  2704     fun box_relational_operator_type (Type ("fun", Ts)) =
  2705         Type ("fun", map box_relational_operator_type Ts)
  2706       | box_relational_operator_type (Type ("*", Ts)) =
  2707         Type ("*", map (box_type ext_ctxt InPair) Ts)
  2708       | box_relational_operator_type T = T
  2709     (* typ -> typ -> term -> term *)
  2710     fun coerce_bound_0_in_term new_T old_T =
  2711       old_T <> new_T ? coerce_bound_no (coerce_term [new_T] old_T new_T) 0
  2712     (* typ list -> typ -> term -> term *)
  2713     and coerce_term Ts new_T old_T t =
  2714       if old_T = new_T then
  2715         t
  2716       else
  2717         case (new_T, old_T) of
  2718           (Type (new_s, new_Ts as [new_T1, new_T2]),
  2719            Type ("fun", [old_T1, old_T2])) =>
  2720           (case eta_expand Ts t 1 of
  2721              Abs (s, _, t') =>
  2722              Abs (s, new_T1,
  2723                   t' |> coerce_bound_0_in_term new_T1 old_T1
  2724                      |> coerce_term (new_T1 :: Ts) new_T2 old_T2)
  2725              |> Envir.eta_contract
  2726              |> new_s <> "fun"
  2727                 ? construct_value thy (@{const_name FunBox},
  2728                                        Type ("fun", new_Ts) --> new_T) o single
  2729            | t' => raise TERM ("Nitpick_HOL.box_fun_and_pair_in_term.\
  2730                                \coerce_term", [t']))
  2731         | (Type (new_s, new_Ts as [new_T1, new_T2]),
  2732            Type (old_s, old_Ts as [old_T1, old_T2])) =>
  2733           if old_s mem [@{type_name fun_box}, @{type_name pair_box}, "*"] then
  2734             case constr_expand ext_ctxt old_T t of
  2735               Const (@{const_name FunBox}, _) $ t1 =>
  2736               if new_s = "fun" then
  2737                 coerce_term Ts new_T (Type ("fun", old_Ts)) t1
  2738               else
  2739                 construct_value thy
  2740                     (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
  2741                      [coerce_term Ts (Type ("fun", new_Ts))
  2742                                   (Type ("fun", old_Ts)) t1]
  2743             | Const _ $ t1 $ t2 =>
  2744               construct_value thy
  2745                   (if new_s = "*" then @{const_name Pair}
  2746                    else @{const_name PairBox}, new_Ts ---> new_T)
  2747                   [coerce_term Ts new_T1 old_T1 t1,
  2748                    coerce_term Ts new_T2 old_T2 t2]
  2749             | t' => raise TERM ("Nitpick_HOL.box_fun_and_pair_in_term.\
  2750                                 \coerce_term", [t'])
  2751           else
  2752             raise TYPE ("coerce_term", [new_T, old_T], [t])
  2753         | _ => raise TYPE ("coerce_term", [new_T, old_T], [t])
  2754     (* indexname * typ -> typ * term -> typ option list -> typ option list *)
  2755     fun add_boxed_types_for_var (z as (_, T)) (T', t') =
  2756       case t' of
  2757         Var z' => z' = z ? insert (op =) T'
  2758       | Const (@{const_name Pair}, _) $ t1 $ t2 =>
  2759         (case T' of
  2760            Type (_, [T1, T2]) =>
  2761            fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)]
  2762          | _ => raise TYPE ("Nitpick_HOL.box_fun_and_pair_in_term.\
  2763                             \add_boxed_types_for_var", [T'], []))
  2764       | _ => exists_subterm (equal (Var z)) t' ? insert (op =) T
  2765     (* typ list -> typ list -> term -> indexname * typ -> typ *)
  2766     fun box_var_in_def new_Ts old_Ts t (z as (_, T)) =
  2767       case t of
  2768         @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
  2769       | Const (s0, _) $ t1 $ _ =>
  2770         if s0 mem [@{const_name "=="}, @{const_name "op ="}] then
  2771           let
  2772             val (t', args) = strip_comb t1
  2773             val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
  2774           in
  2775             case fold (add_boxed_types_for_var z)
  2776                       (fst (strip_n_binders (length args) T') ~~ args) [] of
  2777               [T''] => T''
  2778             | _ => T
  2779           end
  2780         else
  2781           T
  2782       | _ => T
  2783     (* typ list -> typ list -> polarity -> string -> typ -> string -> typ
  2784        -> term -> term *)
  2785     and do_quantifier new_Ts old_Ts polar quant_s quant_T abs_s abs_T t =
  2786       let
  2787         val abs_T' =
  2788           if polar = Neut orelse is_positive_existential polar quant_s then
  2789             box_type ext_ctxt InFunLHS abs_T
  2790           else
  2791             abs_T
  2792         val body_T = body_type quant_T
  2793       in
  2794         Const (quant_s, (abs_T' --> body_T) --> body_T)
  2795         $ Abs (abs_s, abs_T',
  2796                t |> do_term (abs_T' :: new_Ts) (abs_T :: old_Ts) polar)
  2797       end
  2798     (* typ list -> typ list -> string -> typ -> term -> term -> term *)
  2799     and do_equals new_Ts old_Ts s0 T0 t1 t2 =
  2800       let
  2801         val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2)
  2802         val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
  2803         val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last
  2804       in
  2805         list_comb (Const (s0, [T, T] ---> body_type T0),
  2806                    map2 (coerce_term new_Ts T) [T1, T2] [t1, t2])
  2807       end
  2808     (* string -> typ -> term *)
  2809     and do_description_operator s T =
  2810       let val T1 = box_type ext_ctxt InFunLHS (range_type T) in
  2811         Const (s, (T1 --> bool_T) --> T1)
  2812       end
  2813     (* typ list -> typ list -> polarity -> term -> term *)
  2814     and do_term new_Ts old_Ts polar t =
  2815       case t of
  2816         Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
  2817         do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
  2818       | Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 =>
  2819         do_equals new_Ts old_Ts s0 T0 t1 t2
  2820       | @{const "==>"} $ t1 $ t2 =>
  2821         @{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
  2822         $ do_term new_Ts old_Ts polar t2
  2823       | @{const Pure.conjunction} $ t1 $ t2 =>
  2824         @{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1
  2825         $ do_term new_Ts old_Ts polar t2
  2826       | @{const Trueprop} $ t1 =>
  2827         @{const Trueprop} $ do_term new_Ts old_Ts polar t1
  2828       | @{const Not} $ t1 =>
  2829         @{const Not} $ do_term new_Ts old_Ts (flip_polarity polar) t1
  2830       | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
  2831         do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
  2832       | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
  2833         do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
  2834       | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>
  2835         do_equals new_Ts old_Ts s0 T0 t1 t2
  2836       | @{const "op &"} $ t1 $ t2 =>
  2837         @{const "op &"} $ do_term new_Ts old_Ts polar t1
  2838         $ do_term new_Ts old_Ts polar t2
  2839       | @{const "op |"} $ t1 $ t2 =>
  2840         @{const "op |"} $ do_term new_Ts old_Ts polar t1
  2841         $ do_term new_Ts old_Ts polar t2
  2842       | @{const "op -->"} $ t1 $ t2 =>
  2843         @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
  2844         $ do_term new_Ts old_Ts polar t2
  2845       | Const (s as @{const_name The}, T) => do_description_operator s T
  2846       | Const (s as @{const_name Eps}, T) => do_description_operator s T
  2847       | Const (s as @{const_name Tha}, T) => do_description_operator s T
  2848       | Const (x as (s, T)) =>
  2849         Const (s, if s mem [@{const_name converse}, @{const_name trancl}] then
  2850                     box_relational_operator_type T
  2851                   else if is_built_in_const fast_descrs x
  2852                           orelse s = @{const_name Sigma} then
  2853                     T
  2854                   else if is_constr_like thy x then
  2855                     box_type ext_ctxt InConstr T
  2856                   else if is_sel s orelse is_rep_fun thy x then
  2857                     box_type ext_ctxt InSel T
  2858                   else
  2859                     box_type ext_ctxt InExpr T)
  2860       | t1 $ Abs (s, T, t2') =>
  2861         let
  2862           val t1 = do_term new_Ts old_Ts Neut t1
  2863           val T1 = fastype_of1 (new_Ts, t1)
  2864           val (s1, Ts1) = dest_Type T1
  2865           val T' = hd (snd (dest_Type (hd Ts1)))
  2866           val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2')
  2867           val T2 = fastype_of1 (new_Ts, t2)
  2868           val t2 = coerce_term new_Ts (hd Ts1) T2 t2
  2869         in
  2870           betapply (if s1 = "fun" then
  2871                       t1
  2872                     else
  2873                       select_nth_constr_arg thy
  2874                           (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
  2875                           (Type ("fun", Ts1)), t2)
  2876         end
  2877       | t1 $ t2 =>
  2878         let
  2879           val t1 = do_term new_Ts old_Ts Neut t1
  2880           val T1 = fastype_of1 (new_Ts, t1)
  2881           val (s1, Ts1) = dest_Type T1
  2882           val t2 = do_term new_Ts old_Ts Neut t2
  2883           val T2 = fastype_of1 (new_Ts, t2)
  2884           val t2 = coerce_term new_Ts (hd Ts1) T2 t2
  2885         in
  2886           betapply (if s1 = "fun" then
  2887                       t1
  2888                     else
  2889                       select_nth_constr_arg thy
  2890                           (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
  2891                           (Type ("fun", Ts1)), t2)
  2892         end
  2893       | Free (s, T) => Free (s, box_type ext_ctxt InExpr T)
  2894       | Var (z as (x, T)) =>
  2895         Var (x, if def then box_var_in_def new_Ts old_Ts orig_t z
  2896                 else box_type ext_ctxt InExpr T)
  2897       | Bound _ => t
  2898       | Abs (s, T, t') =>
  2899         Abs (s, T, do_term (T :: new_Ts) (T :: old_Ts) Neut t')
  2900   in do_term [] [] Pos orig_t end
  2901 
  2902 (* int -> term -> term *)
  2903 fun eval_axiom_for_term j t =
  2904   Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t)
  2905 
  2906 (* extended_context -> styp -> bool *)
  2907 fun is_equational_fun_surely_complete ext_ctxt x =
  2908   case raw_equational_fun_axioms ext_ctxt x of
  2909     [@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] =>
  2910     strip_comb t1 |> snd |> forall is_Var
  2911   | _ => false
  2912 
  2913 type special = int list * term list * styp
  2914 
  2915 (* styp -> special -> special -> term *)
  2916 fun special_congruence_axiom (s, T) (js1, ts1, x1) (js2, ts2, x2) =
  2917   let
  2918     val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2)
  2919     val Ts = binder_types T
  2920     val max_j = fold (fold (curry Int.max)) [js1, js2] ~1
  2921     val (eqs, (args1, args2)) =
  2922       fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j)
  2923                                   (js1 ~~ ts1, js2 ~~ ts2) of
  2924                       (SOME t1, SOME t2) => apfst (cons (t1, t2))
  2925                     | (SOME t1, NONE) => apsnd (apsnd (cons t1))
  2926                     | (NONE, SOME t2) => apsnd (apfst (cons t2))
  2927                     | (NONE, NONE) =>
  2928                       let val v = Var ((cong_var_prefix ^ nat_subscript j, 0),
  2929                                        nth Ts j) in
  2930                         apsnd (pairself (cons v))
  2931                       end) (max_j downto 0) ([], ([], []))
  2932   in
  2933     Logic.list_implies (eqs |> filter_out (op =) |> distinct (op =)
  2934                             |> map Logic.mk_equals,
  2935                         Logic.mk_equals (list_comb (Const x1, bounds1 @ args1),
  2936                                          list_comb (Const x2, bounds2 @ args2)))
  2937     |> Refute.close_form
  2938   end
  2939 
  2940 (* extended_context -> styp list -> term list *)
  2941 fun special_congruence_axioms (ext_ctxt as {special_funs, ...}) xs =
  2942   let
  2943     val groups =
  2944       !special_funs
  2945       |> map (fn ((x, js, ts), x') => (x, (js, ts, x')))
  2946       |> AList.group (op =)
  2947       |> filter_out (is_equational_fun_surely_complete ext_ctxt o fst)
  2948       |> map (fn (x, zs) => (x, zs |> (x mem xs) ? cons ([], [], x)))
  2949     (* special -> int *)
  2950     fun generality (js, _, _) = ~(length js)
  2951     (* special -> special -> bool *)
  2952     fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
  2953       x1 <> x2 andalso OrdList.subset (prod_ord int_ord TermOrd.term_ord)
  2954                                       (j2 ~~ t2, j1 ~~ t1)
  2955     (* styp -> special list -> special list -> special list -> term list
  2956        -> term list *)
  2957     fun do_pass_1 _ [] [_] [_] = I
  2958       | do_pass_1 x skipped _ [] = do_pass_2 x skipped
  2959       | do_pass_1 x skipped all (z :: zs) =
  2960         case filter (is_more_specific z) all
  2961              |> sort (int_ord o pairself generality) of
  2962           [] => do_pass_1 x (z :: skipped) all zs
  2963         | (z' :: _) => cons (special_congruence_axiom x z z')
  2964                        #> do_pass_1 x skipped all zs
  2965     (* styp -> special list -> term list -> term list *)
  2966     and do_pass_2 _ [] = I
  2967       | do_pass_2 x (z :: zs) =
  2968         fold (cons o special_congruence_axiom x z) zs #> do_pass_2 x zs
  2969   in fold (fn (x, zs) => do_pass_1 x [] zs zs) groups [] end
  2970 
  2971 (* term -> bool *)
  2972 val is_trivial_equation = the_default false o try (op aconv o Logic.dest_equals)
  2973 
  2974 (* 'a Symtab.table -> 'a list *)
  2975 fun all_table_entries table = Symtab.fold (append o snd) table []
  2976 (* const_table -> string -> const_table *)
  2977 fun extra_table table s = Symtab.make [(s, all_table_entries table)]
  2978 
  2979 (* extended_context -> term -> (term list * term list) * (bool * bool) *)
  2980 fun axioms_for_term
  2981         (ext_ctxt as {thy, max_bisim_depth, user_axioms, fast_descrs, evals,
  2982                       def_table, nondef_table, user_nondefs, ...}) t =
  2983   let
  2984     type accumulator = styp list * (term list * term list)
  2985     (* (term list * term list -> term list)
  2986        -> ((term list -> term list) -> term list * term list
  2987            -> term list * term list)
  2988        -> int -> term -> accumulator -> accumulator *)
  2989     fun add_axiom get app depth t (accum as (xs, axs)) =
  2990       let
  2991         val t = t |> unfold_defs_in_term ext_ctxt
  2992                   |> skolemize_term_and_more ext_ctxt ~1
  2993       in
  2994         if is_trivial_equation t then
  2995           accum
  2996         else
  2997           let val t' = t |> specialize_consts_in_term ext_ctxt depth in
  2998             if exists (member (op aconv) (get axs)) [t, t'] then accum
  2999             else add_axioms_for_term (depth + 1) t' (xs, app (cons t') axs)
  3000           end
  3001       end
  3002     (* int -> term -> accumulator -> accumulator *)
  3003     and add_nondef_axiom depth = add_axiom snd apsnd depth
  3004     and add_def_axiom depth t =
  3005       (if head_of t = @{const "==>"} then add_nondef_axiom
  3006        else add_axiom fst apfst) depth t
  3007     (* int -> term -> accumulator -> accumulator *)
  3008     and add_axioms_for_term depth t (accum as (xs, axs)) =
  3009       case t of
  3010         t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
  3011       | Const (x as (s, T)) =>
  3012         (if x mem xs orelse is_built_in_const fast_descrs x then
  3013            accum
  3014          else
  3015            let val accum as (xs, _) = (x :: xs, axs) in
  3016              if depth > axioms_max_depth then
  3017                raise LIMIT ("Nitpick_HOL.axioms_for_term.add_axioms_for_term",
  3018                             "too many nested axioms (" ^ string_of_int depth ^
  3019                             ")")
  3020              else if Refute.is_const_of_class thy x then
  3021                let
  3022                  val class = Logic.class_of_const s
  3023                  val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]),
  3024                                                    class)
  3025                  val ax1 = try (Refute.specialize_type thy x) of_class
  3026                  val ax2 = Option.map (Refute.specialize_type thy x o snd)
  3027                                       (Refute.get_classdef thy class)
  3028                in fold (add_def_axiom depth) (map_filter I [ax1, ax2]) accum end
  3029              else if is_constr thy x then
  3030                accum
  3031              else if is_equational_fun ext_ctxt x then
  3032                fold (add_def_axiom depth) (equational_fun_axioms ext_ctxt x)
  3033                     accum
  3034              else if is_abs_fun thy x then
  3035                accum |> fold (add_nondef_axiom depth)
  3036                              (nondef_props_for_const thy false nondef_table x)
  3037                      |> is_funky_typedef thy (range_type T)
  3038                         ? fold (add_def_axiom depth)
  3039                                (nondef_props_for_const thy true
  3040                                                     (extra_table def_table s) x)
  3041              else if is_rep_fun thy x then
  3042                accum |> fold (add_nondef_axiom depth)
  3043                              (nondef_props_for_const thy false nondef_table x)
  3044                      |> is_funky_typedef thy (range_type T)
  3045                         ? fold (add_def_axiom depth)
  3046                                (nondef_props_for_const thy true
  3047                                                     (extra_table def_table s) x)
  3048                      |> add_axioms_for_term depth
  3049                                             (Const (mate_of_rep_fun thy x))
  3050                      |> add_def_axiom depth (inverse_axiom_for_rep_fun thy x)
  3051              else
  3052                accum |> user_axioms <> SOME false
  3053                         ? fold (add_nondef_axiom depth)
  3054                                (nondef_props_for_const thy false nondef_table x)
  3055            end)
  3056         |> add_axioms_for_type depth T
  3057       | Free (_, T) => add_axioms_for_type depth T accum
  3058       | Var (_, T) => add_axioms_for_type depth T accum
  3059       | Bound _ => accum
  3060       | Abs (_, T, t) => accum |> add_axioms_for_term depth t
  3061                                |> add_axioms_for_type depth T
  3062     (* int -> typ -> accumulator -> accumulator *)
  3063     and add_axioms_for_type depth T =
  3064       case T of
  3065         Type ("fun", Ts) => fold (add_axioms_for_type depth) Ts
  3066       | Type ("*", Ts) => fold (add_axioms_for_type depth) Ts
  3067       | @{typ prop} => I
  3068       | @{typ bool} => I
  3069       | @{typ unit} => I
  3070       | TFree (_, S) => add_axioms_for_sort depth T S
  3071       | TVar (_, S) => add_axioms_for_sort depth T S
  3072       | Type (z as (_, Ts)) =>
  3073         fold (add_axioms_for_type depth) Ts
  3074         #> (if is_pure_typedef thy T then
  3075               fold (add_def_axiom depth) (optimized_typedef_axioms thy z)
  3076             else if max_bisim_depth >= 0 andalso is_codatatype thy T then
  3077               fold (add_def_axiom depth) (codatatype_bisim_axioms ext_ctxt T)
  3078             else
  3079               I)
  3080     (* int -> typ -> sort -> accumulator -> accumulator *)
  3081     and add_axioms_for_sort depth T S =
  3082       let
  3083         val supers = Sign.complete_sort thy S
  3084         val class_axioms =
  3085           maps (fn class => map prop_of (AxClass.get_info thy class |> #axioms
  3086                                          handle ERROR _ => [])) supers
  3087         val monomorphic_class_axioms =
  3088           map (fn t => case Term.add_tvars t [] of
  3089                          [] => t
  3090                        | [(x, S)] =>
  3091                          Refute.monomorphic_term (Vartab.make [(x, (S, T))]) t
  3092                        | _ => raise TERM ("Nitpick_HOL.axioms_for_term.\
  3093                                           \add_axioms_for_sort", [t]))
  3094               class_axioms
  3095       in fold (add_nondef_axiom depth) monomorphic_class_axioms end
  3096     val (mono_user_nondefs, poly_user_nondefs) =
  3097       List.partition (null o Term.hidden_polymorphism) user_nondefs
  3098     val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals))
  3099                            evals
  3100     val (xs, (defs, nondefs)) =
  3101       ([], ([], [])) |> add_axioms_for_term 1 t 
  3102                      |> fold_rev (add_def_axiom 1) eval_axioms
  3103                      |> user_axioms = SOME true
  3104                         ? fold (add_nondef_axiom 1) mono_user_nondefs
  3105     val defs = defs @ special_congruence_axioms ext_ctxt xs
  3106   in
  3107     ((defs, nondefs), (user_axioms = SOME true orelse null mono_user_nondefs,
  3108                        null poly_user_nondefs))
  3109   end
  3110 
  3111 (* theory -> const_table -> styp -> int list *)
  3112 fun const_format thy def_table (x as (s, T)) =
  3113   if String.isPrefix unrolled_prefix s then
  3114     const_format thy def_table (original_name s, range_type T)
  3115   else if String.isPrefix skolem_prefix s then
  3116     let
  3117       val k = unprefix skolem_prefix s
  3118               |> strip_first_name_sep |> fst |> space_explode "@"
  3119               |> hd |> Int.fromString |> the
  3120     in [k, num_binder_types T - k] end
  3121   else if original_name s <> s then
  3122     [num_binder_types T]
  3123   else case def_of_const thy def_table x of
  3124     SOME t' => if fixpoint_kind_of_rhs t' <> NoFp then
  3125                  let val k = length (strip_abs_vars t') in
  3126                    [k, num_binder_types T - k]
  3127                  end
  3128                else
  3129                  [num_binder_types T]
  3130   | NONE => [num_binder_types T]
  3131 (* int list -> int list -> int list *)
  3132 fun intersect_formats _ [] = []
  3133   | intersect_formats [] _ = []
  3134   | intersect_formats ks1 ks2 =
  3135     let val ((ks1', k1), (ks2', k2)) = pairself split_last (ks1, ks2) in
  3136       intersect_formats (ks1' @ (if k1 > k2 then [k1 - k2] else []))
  3137                         (ks2' @ (if k2 > k1 then [k2 - k1] else [])) @
  3138       [Int.min (k1, k2)]
  3139     end
  3140 
  3141 (* theory -> const_table -> (term option * int list) list -> term -> int list *)
  3142 fun lookup_format thy def_table formats t =
  3143   case AList.lookup (fn (SOME x, SOME y) =>
  3144                         (term_match thy) (x, y) | _ => false)
  3145                     formats (SOME t) of
  3146     SOME format => format
  3147   | NONE => let val format = the (AList.lookup (op =) formats NONE) in
  3148               case t of
  3149                 Const x => intersect_formats format
  3150                                              (const_format thy def_table x)
  3151               | _ => format
  3152             end
  3153 
  3154 (* int list -> int list -> typ -> typ *)
  3155 fun format_type default_format format T =
  3156   let
  3157     val T = unbox_type T
  3158     val format = format |> filter (curry (op <) 0)
  3159   in
  3160     if forall (equal 1) format then
  3161       T
  3162     else
  3163       let
  3164         val (binder_Ts, body_T) = strip_type T
  3165         val batched =
  3166           binder_Ts
  3167           |> map (format_type default_format default_format)
  3168           |> rev |> chunk_list_unevenly (rev format)
  3169           |> map (HOLogic.mk_tupleT o rev)
  3170       in List.foldl (op -->) body_T batched end
  3171   end
  3172 (* theory -> const_table -> (term option * int list) list -> term -> typ *)
  3173 fun format_term_type thy def_table formats t =
  3174   format_type (the (AList.lookup (op =) formats NONE))
  3175               (lookup_format thy def_table formats t) (fastype_of t)
  3176 
  3177 (* int list -> int -> int list -> int list *)
  3178 fun repair_special_format js m format =
  3179   m - 1 downto 0 |> chunk_list_unevenly (rev format)
  3180                  |> map (rev o filter_out (member (op =) js))
  3181                  |> filter_out null |> map length |> rev
  3182 
  3183 (* extended_context -> string * string -> (term option * int list) list
  3184    -> styp -> term * typ *)
  3185 fun user_friendly_const ({thy, evals, def_table, skolems, special_funs, ...}
  3186                          : extended_context) (base_name, step_name) formats =
  3187   let
  3188     val default_format = the (AList.lookup (op =) formats NONE)
  3189     (* styp -> term * typ *)
  3190     fun do_const (x as (s, T)) =
  3191       (if String.isPrefix special_prefix s then
  3192          let
  3193            (* term -> term *)
  3194            val do_term = map_aterms (fn Const x => fst (do_const x) | t' => t')
  3195            val (x' as (_, T'), js, ts) =
  3196              AList.find (op =) (!special_funs) (s, unbox_type T) |> the_single
  3197            val max_j = List.last js
  3198            val Ts = List.take (binder_types T', max_j + 1)
  3199            val missing_js = filter_out (member (op =) js) (0 upto max_j)
  3200            val missing_Ts = filter_indices missing_js Ts
  3201            (* int -> indexname *)
  3202            fun nth_missing_var n =
  3203              ((arg_var_prefix ^ nat_subscript (n + 1), 0), nth missing_Ts n)
  3204            val missing_vars = map nth_missing_var (0 upto length missing_js - 1)
  3205            val vars = special_bounds ts @ missing_vars
  3206            val ts' = map2 (fn T => fn j =>
  3207                               case AList.lookup (op =) (js ~~ ts) j of
  3208                                 SOME t => do_term t
  3209                               | NONE =>
  3210                                 Var (nth missing_vars
  3211                                          (find_index (equal j) missing_js)))
  3212                           Ts (0 upto max_j)
  3213            val t = do_const x' |> fst
  3214            val format =
  3215              case AList.lookup (fn (SOME t1, SOME t2) => term_match thy (t1, t2)
  3216                                  | _ => false) formats (SOME t) of
  3217                SOME format =>
  3218                repair_special_format js (num_binder_types T') format
  3219              | NONE =>
  3220                const_format thy def_table x'
  3221                |> repair_special_format js (num_binder_types T')
  3222                |> intersect_formats default_format
  3223          in
  3224            (list_comb (t, ts') |> fold_rev abs_var vars,
  3225             format_type default_format format T)
  3226          end
  3227        else if String.isPrefix uncurry_prefix s then
  3228          let
  3229            val (ss, s') = unprefix uncurry_prefix s
  3230                           |> strip_first_name_sep |>> space_explode "@"
  3231          in
  3232            if String.isPrefix step_prefix s' then
  3233              do_const (s', T)
  3234            else
  3235              let
  3236                val k = the (Int.fromString (hd ss))
  3237                val j = the (Int.fromString (List.last ss))
  3238                val (before_Ts, (tuple_T, rest_T)) =
  3239                  strip_n_binders j T ||> (strip_n_binders 1 #>> hd)
  3240                val T' = before_Ts ---> dest_n_tuple_type k tuple_T ---> rest_T
  3241              in do_const (s', T') end
  3242          end
  3243        else if String.isPrefix unrolled_prefix s then
  3244          let val t = Const (original_name s, range_type T) in
  3245            (lambda (Free (iter_var_prefix, nat_T)) t,
  3246             format_type default_format
  3247                         (lookup_format thy def_table formats t) T)
  3248          end
  3249        else if String.isPrefix base_prefix s then
  3250          (Const (base_name, T --> T) $ Const (unprefix base_prefix s, T),
  3251           format_type default_format default_format T)
  3252        else if String.isPrefix step_prefix s then
  3253          (Const (step_name, T --> T) $ Const (unprefix step_prefix s, T),
  3254           format_type default_format default_format T)
  3255        else if String.isPrefix skolem_prefix s then
  3256          let
  3257            val ss = the (AList.lookup (op =) (!skolems) s)
  3258            val (Ts, Ts') = chop (length ss) (binder_types T)
  3259            val frees = map Free (ss ~~ Ts)
  3260            val s' = original_name s
  3261          in
  3262            (fold lambda frees (Const (s', Ts' ---> T)),
  3263             format_type default_format
  3264                         (lookup_format thy def_table formats (Const x)) T)
  3265          end
  3266        else if String.isPrefix eval_prefix s then
  3267          let
  3268            val t = nth evals (the (Int.fromString (unprefix eval_prefix s)))
  3269          in (t, format_term_type thy def_table formats t) end
  3270        else if s = @{const_name undefined_fast_The} then
  3271          (Const (nitpick_prefix ^ "The fallback", T),
  3272           format_type default_format
  3273                       (lookup_format thy def_table formats
  3274                            (Const (@{const_name The}, (T --> bool_T) --> T))) T)
  3275        else if s = @{const_name undefined_fast_Eps} then
  3276          (Const (nitpick_prefix ^ "Eps fallback", T),
  3277           format_type default_format
  3278                       (lookup_format thy def_table formats
  3279                            (Const (@{const_name Eps}, (T --> bool_T) --> T))) T)
  3280        else
  3281          let val t = Const (original_name s, T) in
  3282            (t, format_term_type thy def_table formats t)
  3283          end)
  3284       |>> map_types (typ_subst [(@{typ bisim_iterator}, nat_T)] o unbox_type)
  3285       |>> shorten_const_names_in_term |>> shorten_abs_vars
  3286   in do_const end
  3287 
  3288 (* styp -> string *)
  3289 fun assign_operator_for_const (s, T) =
  3290   if String.isPrefix ubfp_prefix s then
  3291     if is_fun_type T then "\<subseteq>" else "\<le>"
  3292   else if String.isPrefix lbfp_prefix s then
  3293     if is_fun_type T then "\<supseteq>" else "\<ge>"
  3294   else if original_name s <> s then
  3295     assign_operator_for_const (after_name_sep s, T)
  3296   else
  3297     "="
  3298 
  3299 (* extended_context -> term
  3300    -> ((term list * term list) * (bool * bool)) * term *)
  3301 fun preprocess_term (ext_ctxt as {thy, destroy_constrs, boxes, skolemize,
  3302                                   uncurry, ...}) t =
  3303   let
  3304     val skolem_depth = if skolemize then 4 else ~1
  3305     val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
  3306          core_t) = t |> unfold_defs_in_term ext_ctxt
  3307                      |> Refute.close_form
  3308                      |> skolemize_term_and_more ext_ctxt skolem_depth
  3309                      |> specialize_consts_in_term ext_ctxt 0
  3310                      |> `(axioms_for_term ext_ctxt)
  3311     val maybe_box = exists (not_equal (SOME false) o snd) boxes
  3312     val table =
  3313       Termtab.empty |> uncurry
  3314         ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts)
  3315     (* bool -> bool -> term -> term *)
  3316     fun do_rest def core =
  3317       uncurry ? uncurry_term table
  3318       #> maybe_box ? box_fun_and_pair_in_term ext_ctxt def
  3319       #> destroy_constrs ? (pull_out_universal_constrs thy def
  3320                             #> pull_out_existential_constrs thy
  3321                             #> destroy_pulled_out_constrs ext_ctxt def)
  3322       #> curry_assms
  3323       #> destroy_universal_equalities
  3324       #> destroy_existential_equalities thy
  3325       #> simplify_constrs_and_sels thy
  3326       #> distribute_quantifiers
  3327       #> push_quantifiers_inward thy
  3328       #> not core ? Refute.close_form
  3329       #> shorten_abs_vars
  3330   in
  3331     (((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts),
  3332       (got_all_mono_user_axioms, no_poly_user_axioms)),
  3333      do_rest false true core_t)
  3334   end
  3335 
  3336 end;