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