split "nitpick_hol.ML" into two files to make it more manageable;
authorblanchet
Thu Feb 04 16:03:15 2010 +0100 (2010-02-04)
changeset 3507096136eb6218f
parent 34998 5e492a862b34
child 35071 3df45b0ce819
split "nitpick_hol.ML" into two files to make it more manageable;
more refactoring to come
src/HOL/IsaMakefile
src/HOL/Nitpick.thy
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
src/HOL/Tools/Nitpick/nitpick_scope.ML
     1.1 --- a/src/HOL/IsaMakefile	Thu Feb 04 13:36:52 2010 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Thu Feb 04 16:03:15 2010 +0100
     1.3 @@ -206,6 +206,7 @@
     1.4    Tools/Nitpick/nitpick_mono.ML \
     1.5    Tools/Nitpick/nitpick_nut.ML \
     1.6    Tools/Nitpick/nitpick_peephole.ML \
     1.7 +  Tools/Nitpick/nitpick_preproc.ML \
     1.8    Tools/Nitpick/nitpick_rep.ML \
     1.9    Tools/Nitpick/nitpick_scope.ML \
    1.10    Tools/Nitpick/nitpick_tests.ML \
     2.1 --- a/src/HOL/Nitpick.thy	Thu Feb 04 13:36:52 2010 +0100
     2.2 +++ b/src/HOL/Nitpick.thy	Thu Feb 04 16:03:15 2010 +0100
     2.3 @@ -13,6 +13,7 @@
     2.4       ("Tools/Nitpick/kodkod_sat.ML")
     2.5       ("Tools/Nitpick/nitpick_util.ML")
     2.6       ("Tools/Nitpick/nitpick_hol.ML")
     2.7 +     ("Tools/Nitpick/nitpick_preproc.ML")
     2.8       ("Tools/Nitpick/nitpick_mono.ML")
     2.9       ("Tools/Nitpick/nitpick_scope.ML")
    2.10       ("Tools/Nitpick/nitpick_peephole.ML")
    2.11 @@ -237,6 +238,7 @@
    2.12  use "Tools/Nitpick/kodkod_sat.ML"
    2.13  use "Tools/Nitpick/nitpick_util.ML"
    2.14  use "Tools/Nitpick/nitpick_hol.ML"
    2.15 +use "Tools/Nitpick/nitpick_preproc.ML"
    2.16  use "Tools/Nitpick/nitpick_mono.ML"
    2.17  use "Tools/Nitpick/nitpick_scope.ML"
    2.18  use "Tools/Nitpick/nitpick_peephole.ML"
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Feb 04 13:36:52 2010 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Feb 04 16:03:15 2010 +0100
     3.3 @@ -69,6 +69,7 @@
     3.4  
     3.5  open Nitpick_Util
     3.6  open Nitpick_HOL
     3.7 +open Nitpick_Preproc
     3.8  open Nitpick_Mono
     3.9  open Nitpick_Scope
    3.10  open Nitpick_Peephole
    3.11 @@ -273,7 +274,7 @@
    3.12      val intro_table = inductive_intro_table ctxt def_table
    3.13      val ground_thm_table = ground_theorem_table thy
    3.14      val ersatz_table = ersatz_table thy
    3.15 -    val (ext_ctxt as {wf_cache, ...}) =
    3.16 +    val (hol_ctxt as {wf_cache, ...}) =
    3.17        {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
    3.18         stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
    3.19         binary_ints = binary_ints, destroy_constrs = destroy_constrs,
    3.20 @@ -292,7 +293,7 @@
    3.21      val _ = null (Term.add_tvars assms_t []) orelse
    3.22              raise NOT_SUPPORTED "schematic type variables"
    3.23      val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
    3.24 -         core_t) = preprocess_term ext_ctxt assms_t
    3.25 +         core_t) = preprocess_term hol_ctxt assms_t
    3.26      val got_all_user_axioms =
    3.27        got_all_mono_user_axioms andalso no_poly_user_axioms
    3.28  
    3.29 @@ -319,9 +320,9 @@
    3.30              handle TYPE (_, Ts, ts) =>
    3.31                     raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts)
    3.32  
    3.33 -    val core_u = nut_from_term ext_ctxt Eq core_t
    3.34 -    val def_us = map (nut_from_term ext_ctxt DefEq) def_ts
    3.35 -    val nondef_us = map (nut_from_term ext_ctxt Eq) nondef_ts
    3.36 +    val core_u = nut_from_term hol_ctxt Eq core_t
    3.37 +    val def_us = map (nut_from_term hol_ctxt DefEq) def_ts
    3.38 +    val nondef_us = map (nut_from_term hol_ctxt Eq) nondef_ts
    3.39      val (free_names, const_names) =
    3.40        fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])
    3.41      val (sel_names, nonsel_names) =
    3.42 @@ -344,12 +345,12 @@
    3.43        case triple_lookup (type_match thy) monos T of
    3.44          SOME (SOME b) => b
    3.45        | _ => is_type_always_monotonic T orelse
    3.46 -             formulas_monotonic ext_ctxt T Plus def_ts nondef_ts core_t
    3.47 +             formulas_monotonic hol_ctxt T Plus def_ts nondef_ts core_t
    3.48      fun is_deep_datatype T =
    3.49        is_datatype thy T andalso
    3.50        (is_word_type T orelse
    3.51         exists (curry (op =) T o domain_type o type_of) sel_names)
    3.52 -    val all_Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts)
    3.53 +    val all_Ts = ground_types_in_terms hol_ctxt (core_t :: def_ts @ nondef_ts)
    3.54                   |> sort TermOrd.typ_ord
    3.55      val _ = if verbose andalso binary_ints = SOME true andalso
    3.56                 exists (member (op =) [nat_T, int_T]) all_Ts then
    3.57 @@ -522,7 +523,7 @@
    3.58          val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels
    3.59          val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels
    3.60          val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels
    3.61 -        val dtype_axioms = declarative_axioms_for_datatypes ext_ctxt bits ofs kk
    3.62 +        val dtype_axioms = declarative_axioms_for_datatypes hol_ctxt bits ofs kk
    3.63                                                              rel_table datatypes
    3.64          val declarative_axioms = plain_axioms @ dtype_axioms
    3.65          val univ_card = univ_card nat_card int_card main_j0
    3.66 @@ -553,7 +554,7 @@
    3.67               if loc = "Nitpick_Kodkod.check_arity" andalso
    3.68                  not (Typtab.is_empty ofs) then
    3.69                 problem_for_scope liberal
    3.70 -                   {ext_ctxt = ext_ctxt, card_assigns = card_assigns,
    3.71 +                   {hol_ctxt = hol_ctxt, card_assigns = card_assigns,
    3.72                      bits = bits, bisim_depth = bisim_depth,
    3.73                      datatypes = datatypes, ofs = Typtab.empty}
    3.74               else if loc = "Nitpick.pick_them_nits_in_term.\
    3.75 @@ -891,7 +892,7 @@
    3.76          end
    3.77  
    3.78      val (skipped, the_scopes) =
    3.79 -      all_scopes ext_ctxt sym_break cards_assigns maxes_assigns iters_assigns
    3.80 +      all_scopes hol_ctxt sym_break cards_assigns maxes_assigns iters_assigns
    3.81                   bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
    3.82      val _ = if skipped > 0 then
    3.83                print_m (fn () => "Too many scopes. Skipping " ^
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Feb 04 13:36:52 2010 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Feb 04 16:03:15 2010 +0100
     4.3 @@ -13,7 +13,7 @@
     4.4    type unrolled = styp * styp
     4.5    type wf_cache = (styp * (bool * bool)) list
     4.6  
     4.7 -  type extended_context = {
     4.8 +  type hol_context = {
     4.9      thy: theory,
    4.10      ctxt: Proof.context,
    4.11      max_bisim_depth: int,
    4.12 @@ -46,12 +46,24 @@
    4.13      wf_cache: wf_cache Unsynchronized.ref,
    4.14      constr_cache: (typ * styp list) list Unsynchronized.ref}
    4.15  
    4.16 +  datatype fixpoint_kind = Lfp | Gfp | NoFp
    4.17 +  datatype boxability =
    4.18 +    InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
    4.19 +
    4.20    val name_sep : string
    4.21    val numeral_prefix : string
    4.22 +  val ubfp_prefix : string
    4.23 +  val lbfp_prefix : string
    4.24    val skolem_prefix : string
    4.25 +  val special_prefix : string
    4.26 +  val uncurry_prefix : string
    4.27    val eval_prefix : string
    4.28    val original_name : string -> string
    4.29    val s_conj : term * term -> term
    4.30 +  val s_disj : term * term -> term
    4.31 +  val strip_any_connective : term -> term list * term
    4.32 +  val conjuncts_of : term -> term list
    4.33 +  val disjuncts_of : term -> term list
    4.34    val unbit_and_unbox_type : typ -> typ
    4.35    val string_for_type : Proof.context -> typ -> string
    4.36    val prefix_name : string -> string -> string
    4.37 @@ -76,6 +88,7 @@
    4.38    val is_record_type : typ -> bool
    4.39    val is_number_type : theory -> typ -> bool
    4.40    val const_for_iterator_type : typ -> styp
    4.41 +  val strip_n_binders : int -> typ -> typ list * typ
    4.42    val nth_range_type : int -> typ -> typ
    4.43    val num_factors_in_type : typ -> int
    4.44    val num_binder_types : typ -> int
    4.45 @@ -96,15 +109,18 @@
    4.46    val is_rep_fun : theory -> styp -> bool
    4.47    val is_quot_abs_fun : Proof.context -> styp -> bool
    4.48    val is_quot_rep_fun : Proof.context -> styp -> bool
    4.49 +  val mate_of_rep_fun : theory -> styp -> styp
    4.50 +  val is_constr_like : theory -> styp -> bool
    4.51 +  val is_stale_constr : theory -> styp -> bool
    4.52    val is_constr : theory -> styp -> bool
    4.53 -  val is_stale_constr : theory -> styp -> bool
    4.54    val is_sel : string -> bool
    4.55    val is_sel_like_and_no_discr : string -> bool
    4.56 +  val box_type : hol_context -> boxability -> typ -> typ
    4.57    val discr_for_constr : styp -> styp
    4.58    val num_sels_for_constr_type : typ -> int
    4.59    val nth_sel_name_for_constr_name : string -> int -> string
    4.60    val nth_sel_for_constr : styp -> int -> styp
    4.61 -  val boxed_nth_sel_for_constr : extended_context -> styp -> int -> styp
    4.62 +  val boxed_nth_sel_for_constr : hol_context -> styp -> int -> styp
    4.63    val sel_no_from_name : string -> int
    4.64    val eta_expand : typ list -> term -> int -> term
    4.65    val extensionalize : term -> term
    4.66 @@ -113,19 +129,25 @@
    4.67    val unregister_frac_type : string -> theory -> theory
    4.68    val register_codatatype : typ -> string -> styp list -> theory -> theory
    4.69    val unregister_codatatype : typ -> theory -> theory
    4.70 -  val datatype_constrs : extended_context -> typ -> styp list
    4.71 -  val boxed_datatype_constrs : extended_context -> typ -> styp list
    4.72 -  val num_datatype_constrs : extended_context -> typ -> int
    4.73 +  val datatype_constrs : hol_context -> typ -> styp list
    4.74 +  val boxed_datatype_constrs : hol_context -> typ -> styp list
    4.75 +  val num_datatype_constrs : hol_context -> typ -> int
    4.76    val constr_name_for_sel_like : string -> string
    4.77 -  val boxed_constr_for_sel : extended_context -> styp -> styp
    4.78 +  val boxed_constr_for_sel : hol_context -> styp -> styp
    4.79 +  val discriminate_value : hol_context -> styp -> term -> term
    4.80 +  val select_nth_constr_arg : theory -> styp -> term -> int -> typ -> term
    4.81 +  val construct_value : theory -> styp -> term list -> term
    4.82    val card_of_type : (typ * int) list -> typ -> int
    4.83    val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
    4.84    val bounded_exact_card_of_type :
    4.85 -    extended_context -> int -> int -> (typ * int) list -> typ -> int
    4.86 -  val is_finite_type : extended_context -> typ -> bool
    4.87 +    hol_context -> int -> int -> (typ * int) list -> typ -> int
    4.88 +  val is_finite_type : hol_context -> typ -> bool
    4.89 +  val special_bounds : term list -> (indexname * typ) list
    4.90 +  val is_funky_typedef : theory -> typ -> bool
    4.91    val all_axioms_of : theory -> term list * term list * term list
    4.92    val arity_of_built_in_const : bool -> styp -> int option
    4.93    val is_built_in_const : bool -> styp -> bool
    4.94 +  val term_under_def : term -> term
    4.95    val case_const_names : theory -> (string * int) list
    4.96    val const_def_table : Proof.context -> term list -> const_table
    4.97    val const_nondef_table : term list -> const_table
    4.98 @@ -134,22 +156,33 @@
    4.99    val inductive_intro_table : Proof.context -> const_table -> const_table
   4.100    val ground_theorem_table : theory -> term list Inttab.table
   4.101    val ersatz_table : theory -> (string * string) list
   4.102 +  val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit
   4.103 +  val inverse_axioms_for_rep_fun : theory -> styp -> term list
   4.104 +  val optimized_typedef_axioms : theory -> string * typ list -> term list
   4.105 +  val optimized_quot_type_axioms : theory -> string * typ list -> term list
   4.106    val def_of_const : theory -> const_table -> styp -> term option
   4.107 -  val is_inductive_pred : extended_context -> styp -> bool
   4.108 +  val fixpoint_kind_of_const :
   4.109 +    theory -> const_table -> string * typ -> fixpoint_kind
   4.110 +  val is_inductive_pred : hol_context -> styp -> bool
   4.111 +  val is_equational_fun : hol_context -> styp -> bool
   4.112    val is_constr_pattern_lhs : theory -> term -> bool
   4.113    val is_constr_pattern_formula : theory -> term -> bool
   4.114 +  val unfold_defs_in_term : hol_context -> term -> term
   4.115 +  val codatatype_bisim_axioms : hol_context -> typ -> term list
   4.116 +  val is_well_founded_inductive_pred : hol_context -> styp -> bool
   4.117 +  val unrolled_inductive_pred_const : hol_context -> bool -> styp -> term
   4.118 +  val equational_fun_axioms : hol_context -> styp -> term list
   4.119 +  val is_equational_fun_surely_complete : hol_context -> styp -> bool
   4.120    val merge_type_vars_in_terms : term list -> term list
   4.121 -  val ground_types_in_type : extended_context -> typ -> typ list
   4.122 -  val ground_types_in_terms : extended_context -> term list -> typ list
   4.123 +  val ground_types_in_type : hol_context -> typ -> typ list
   4.124 +  val ground_types_in_terms : hol_context -> term list -> typ list
   4.125    val format_type : int list -> int list -> typ -> typ
   4.126    val format_term_type :
   4.127      theory -> const_table -> (term option * int list) list -> term -> typ
   4.128    val user_friendly_const :
   4.129 -   extended_context -> string * string -> (term option * int list) list
   4.130 +   hol_context -> string * string -> (term option * int list) list
   4.131     -> styp -> term * typ
   4.132    val assign_operator_for_const : styp -> string
   4.133 -  val preprocess_term :
   4.134 -    extended_context -> term -> ((term list * term list) * (bool * bool)) * term
   4.135  end;
   4.136  
   4.137  structure Nitpick_HOL : NITPICK_HOL =
   4.138 @@ -162,7 +195,7 @@
   4.139  type unrolled = styp * styp
   4.140  type wf_cache = (styp * (bool * bool)) list
   4.141  
   4.142 -type extended_context = {
   4.143 +type hol_context = {
   4.144    thy: theory,
   4.145    ctxt: Proof.context,
   4.146    max_bisim_depth: int,
   4.147 @@ -195,6 +228,10 @@
   4.148    wf_cache: wf_cache Unsynchronized.ref,
   4.149    constr_cache: (typ * styp list) list Unsynchronized.ref}
   4.150  
   4.151 +datatype fixpoint_kind = Lfp | Gfp | NoFp
   4.152 +datatype boxability =
   4.153 +  InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
   4.154 +
   4.155  structure Data = Theory_Data(
   4.156    type T = {frac_types: (string * (string * string) list) list,
   4.157              codatatypes: (string * (string * styp list)) list}
   4.158 @@ -222,20 +259,11 @@
   4.159  val special_prefix = nitpick_prefix ^ "sp"
   4.160  val uncurry_prefix = nitpick_prefix ^ "unc"
   4.161  val eval_prefix = nitpick_prefix ^ "eval"
   4.162 -val bound_var_prefix = "b"
   4.163 -val cong_var_prefix = "c"
   4.164  val iter_var_prefix = "i"
   4.165 -val val_var_prefix = nitpick_prefix ^ "v"
   4.166  val arg_var_prefix = "x"
   4.167  
   4.168  (* int -> string *)
   4.169  fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep
   4.170 -fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep
   4.171 -(* int -> int -> string *)
   4.172 -fun skolem_prefix_for k j =
   4.173 -  skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
   4.174 -fun uncurry_prefix_for k j =
   4.175 -  uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
   4.176  
   4.177  (* string -> string * string *)
   4.178  val strip_first_name_sep =
   4.179 @@ -260,9 +288,6 @@
   4.180    | s_disj (t1, t2) =
   4.181      if t1 = @{const True} orelse t2 = @{const True} then @{const True}
   4.182      else HOLogic.mk_disj (t1, t2)
   4.183 -(* term -> term -> term *)
   4.184 -fun mk_exists v t =
   4.185 -  HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)
   4.186  
   4.187  (* term -> term -> term list *)
   4.188  fun strip_connective conn_t (t as (t0 $ t1 $ t2)) =
   4.189 @@ -276,8 +301,8 @@
   4.190        ([t], @{const Not})
   4.191    | strip_any_connective t = ([t], @{const Not})
   4.192  (* term -> term list *)
   4.193 -val conjuncts = strip_connective @{const "op &"}
   4.194 -val disjuncts = strip_connective @{const "op |"}
   4.195 +val conjuncts_of = strip_connective @{const "op &"}
   4.196 +val disjuncts_of = strip_connective @{const "op |"}
   4.197  
   4.198  (* When you add constants to these lists, make sure to handle them in
   4.199     "Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
   4.200 @@ -373,8 +398,6 @@
   4.201  fun shortest_name s = List.last (space_explode "." s) handle List.Empty => ""
   4.202  (* string -> term -> term *)
   4.203  val prefix_abs_vars = Term.map_abs_vars o prefix_name
   4.204 -(* term -> term *)
   4.205 -val shorten_abs_vars = Term.map_abs_vars shortest_name
   4.206  (* string -> string *)
   4.207  fun short_name s =
   4.208    case space_explode name_sep s of
   4.209 @@ -441,7 +464,7 @@
   4.210    | const_for_iterator_type T =
   4.211      raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], [])
   4.212  
   4.213 -(* int -> typ -> typ * typ *)
   4.214 +(* int -> typ -> typ list * typ *)
   4.215  fun strip_n_binders 0 T = ([], T)
   4.216    | strip_n_binders n (Type ("fun", [T1, T2])) =
   4.217      strip_n_binders (n - 1) T2 |>> cons T1
   4.218 @@ -552,7 +575,7 @@
   4.219  val is_real_datatype = is_some oo Datatype.get_info
   4.220  (* theory -> typ -> bool *)
   4.221  fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* FIXME *)
   4.222 -  | is_quot_type _ (Type ("FSet.fset", _)) = true (* FIXME *)
   4.223 +  | is_quot_type _ (Type ("FSet.fset", _)) = true
   4.224    | is_quot_type _ _ = false
   4.225  fun is_codatatype thy (T as Type (s, _)) =
   4.226      not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
   4.227 @@ -619,11 +642,11 @@
   4.228       | NONE => false)
   4.229    | is_rep_fun _ _ = false
   4.230  (* Proof.context -> styp -> bool *)
   4.231 -fun is_quot_abs_fun _ ("IntEx.abs_my_int", _) = true (* FIXME *)
   4.232 -  | is_quot_abs_fun _ ("FSet.abs_fset", _) = true (* FIXME *)
   4.233 +fun is_quot_abs_fun _ ("IntEx.abs_my_int", _) = true
   4.234 +  | is_quot_abs_fun _ ("FSet.abs_fset", _) = true
   4.235    | is_quot_abs_fun _ _ = false
   4.236 -fun is_quot_rep_fun _ ("IntEx.rep_my_int", _) = true (* FIXME *)
   4.237 -  | is_quot_rep_fun _ ("FSet.rep_fset", _) = true (* FIXME *)
   4.238 +fun is_quot_rep_fun _ ("IntEx.rep_my_int", _) = true
   4.239 +  | is_quot_rep_fun _ ("FSet.rep_fset", _) = true
   4.240    | is_quot_rep_fun _ _ = false
   4.241  
   4.242  (* theory -> styp -> styp *)
   4.243 @@ -682,9 +705,6 @@
   4.244    String.isPrefix sel_prefix
   4.245    orf (member (op =) [@{const_name fst}, @{const_name snd}])
   4.246  
   4.247 -datatype boxability =
   4.248 -  InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
   4.249 -
   4.250  (* boxability -> boxability *)
   4.251  fun in_fun_lhs_for InConstr = InSel
   4.252    | in_fun_lhs_for _ = InFunLHS
   4.253 @@ -693,8 +713,8 @@
   4.254    | in_fun_rhs_for InFunRHS1 = InFunRHS2
   4.255    | in_fun_rhs_for _ = InFunRHS1
   4.256  
   4.257 -(* extended_context -> boxability -> typ -> bool *)
   4.258 -fun is_boxing_worth_it (ext_ctxt : extended_context) boxy T =
   4.259 +(* hol_context -> boxability -> typ -> bool *)
   4.260 +fun is_boxing_worth_it (hol_ctxt : hol_context) boxy T =
   4.261    case T of
   4.262      Type ("fun", _) =>
   4.263      (boxy = InPair orelse boxy = InFunLHS) andalso
   4.264 @@ -702,31 +722,31 @@
   4.265    | Type ("*", Ts) =>
   4.266      boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse
   4.267      ((boxy = InExpr orelse boxy = InFunLHS) andalso
   4.268 -     exists (is_boxing_worth_it ext_ctxt InPair)
   4.269 -            (map (box_type ext_ctxt InPair) Ts))
   4.270 +     exists (is_boxing_worth_it hol_ctxt InPair)
   4.271 +            (map (box_type hol_ctxt InPair) Ts))
   4.272    | _ => false
   4.273 -(* extended_context -> boxability -> string * typ list -> string *)
   4.274 -and should_box_type (ext_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) =
   4.275 +(* hol_context -> boxability -> string * typ list -> string *)
   4.276 +and should_box_type (hol_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) =
   4.277    case triple_lookup (type_match thy) boxes (Type z) of
   4.278      SOME (SOME box_me) => box_me
   4.279 -  | _ => is_boxing_worth_it ext_ctxt boxy (Type z)
   4.280 -(* extended_context -> boxability -> typ -> typ *)
   4.281 -and box_type ext_ctxt boxy T =
   4.282 +  | _ => is_boxing_worth_it hol_ctxt boxy (Type z)
   4.283 +(* hol_context -> boxability -> typ -> typ *)
   4.284 +and box_type hol_ctxt boxy T =
   4.285    case T of
   4.286      Type (z as ("fun", [T1, T2])) =>
   4.287      if boxy <> InConstr andalso boxy <> InSel andalso
   4.288 -       should_box_type ext_ctxt boxy z then
   4.289 +       should_box_type hol_ctxt boxy z then
   4.290        Type (@{type_name fun_box},
   4.291 -            [box_type ext_ctxt InFunLHS T1, box_type ext_ctxt InFunRHS1 T2])
   4.292 +            [box_type hol_ctxt InFunLHS T1, box_type hol_ctxt InFunRHS1 T2])
   4.293      else
   4.294 -      box_type ext_ctxt (in_fun_lhs_for boxy) T1
   4.295 -      --> box_type ext_ctxt (in_fun_rhs_for boxy) T2
   4.296 +      box_type hol_ctxt (in_fun_lhs_for boxy) T1
   4.297 +      --> box_type hol_ctxt (in_fun_rhs_for boxy) T2
   4.298    | Type (z as ("*", Ts)) =>
   4.299      if boxy <> InConstr andalso boxy <> InSel
   4.300 -       andalso should_box_type ext_ctxt boxy z then
   4.301 -      Type (@{type_name pair_box}, map (box_type ext_ctxt InSel) Ts)
   4.302 +       andalso should_box_type hol_ctxt boxy z then
   4.303 +      Type (@{type_name pair_box}, map (box_type hol_ctxt InSel) Ts)
   4.304      else
   4.305 -      Type ("*", map (box_type ext_ctxt
   4.306 +      Type ("*", map (box_type hol_ctxt
   4.307                            (if boxy = InConstr orelse boxy = InSel then boxy
   4.308                             else InPair)) Ts)
   4.309    | _ => T
   4.310 @@ -747,9 +767,9 @@
   4.311    | nth_sel_for_constr (s, T) n =
   4.312      (nth_sel_name_for_constr_name s n,
   4.313       body_type T --> nth (maybe_curried_binder_types T) n)
   4.314 -(* extended_context -> styp -> int -> styp *)
   4.315 -fun boxed_nth_sel_for_constr ext_ctxt =
   4.316 -  apsnd (box_type ext_ctxt InSel) oo nth_sel_for_constr
   4.317 +(* hol_context -> styp -> int -> styp *)
   4.318 +fun boxed_nth_sel_for_constr hol_ctxt =
   4.319 +  apsnd (box_type hol_ctxt InSel) oo nth_sel_for_constr
   4.320  
   4.321  (* string -> int *)
   4.322  fun sel_no_from_name s =
   4.323 @@ -791,8 +811,8 @@
   4.324  fun zero_const T = Const (@{const_name zero_nat_inst.zero_nat}, T)
   4.325  fun suc_const T = Const (@{const_name Suc}, T --> T)
   4.326  
   4.327 -(* extended_context -> typ -> styp list *)
   4.328 -fun uncached_datatype_constrs ({thy, stds, ...} : extended_context)
   4.329 +(* hol_context -> typ -> styp list *)
   4.330 +fun uncached_datatype_constrs ({thy, stds, ...} : hol_context)
   4.331                                (T as Type (s, Ts)) =
   4.332      (case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
   4.333         SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs'
   4.334 @@ -829,49 +849,49 @@
   4.335         else
   4.336           [])
   4.337    | uncached_datatype_constrs _ _ = []
   4.338 -(* extended_context -> typ -> styp list *)
   4.339 -fun datatype_constrs (ext_ctxt as {constr_cache, ...}) T =
   4.340 +(* hol_context -> typ -> styp list *)
   4.341 +fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T =
   4.342    case AList.lookup (op =) (!constr_cache) T of
   4.343      SOME xs => xs
   4.344    | NONE =>
   4.345 -    let val xs = uncached_datatype_constrs ext_ctxt T in
   4.346 +    let val xs = uncached_datatype_constrs hol_ctxt T in
   4.347        (Unsynchronized.change constr_cache (cons (T, xs)); xs)
   4.348      end
   4.349 -fun boxed_datatype_constrs ext_ctxt =
   4.350 -  map (apsnd (box_type ext_ctxt InConstr)) o datatype_constrs ext_ctxt
   4.351 -(* extended_context -> typ -> int *)
   4.352 +fun boxed_datatype_constrs hol_ctxt =
   4.353 +  map (apsnd (box_type hol_ctxt InConstr)) o datatype_constrs hol_ctxt
   4.354 +(* hol_context -> typ -> int *)
   4.355  val num_datatype_constrs = length oo datatype_constrs
   4.356  
   4.357  (* string -> string *)
   4.358  fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair}
   4.359    | constr_name_for_sel_like @{const_name snd} = @{const_name Pair}
   4.360    | constr_name_for_sel_like s' = original_name s'
   4.361 -(* extended_context -> styp -> styp *)
   4.362 -fun boxed_constr_for_sel ext_ctxt (s', T') =
   4.363 +(* hol_context -> styp -> styp *)
   4.364 +fun boxed_constr_for_sel hol_ctxt (s', T') =
   4.365    let val s = constr_name_for_sel_like s' in
   4.366 -    AList.lookup (op =) (boxed_datatype_constrs ext_ctxt (domain_type T')) s
   4.367 +    AList.lookup (op =) (boxed_datatype_constrs hol_ctxt (domain_type T')) s
   4.368      |> the |> pair s
   4.369    end
   4.370  
   4.371 -(* extended_context -> styp -> term *)
   4.372 -fun discr_term_for_constr ext_ctxt (x as (s, T)) =
   4.373 +(* hol_context -> styp -> term *)
   4.374 +fun discr_term_for_constr hol_ctxt (x as (s, T)) =
   4.375    let val dataT = body_type T in
   4.376      if s = @{const_name Suc} then
   4.377        Abs (Name.uu, dataT,
   4.378             @{const Not} $ HOLogic.mk_eq (zero_const dataT, Bound 0))
   4.379 -    else if num_datatype_constrs ext_ctxt dataT >= 2 then
   4.380 +    else if num_datatype_constrs hol_ctxt dataT >= 2 then
   4.381        Const (discr_for_constr x)
   4.382      else
   4.383        Abs (Name.uu, dataT, @{const True})
   4.384    end
   4.385 -(* extended_context -> styp -> term -> term *)
   4.386 -fun discriminate_value (ext_ctxt as {thy, ...}) (x as (_, T)) t =
   4.387 +(* hol_context -> styp -> term -> term *)
   4.388 +fun discriminate_value (hol_ctxt as {thy, ...}) (x as (_, T)) t =
   4.389    case strip_comb t of
   4.390      (Const x', args) =>
   4.391      if x = x' then @{const True}
   4.392      else if is_constr_like thy x' then @{const False}
   4.393 -    else betapply (discr_term_for_constr ext_ctxt x, t)
   4.394 -  | _ => betapply (discr_term_for_constr ext_ctxt x, t)
   4.395 +    else betapply (discr_term_for_constr hol_ctxt x, t)
   4.396 +  | _ => betapply (discr_term_for_constr hol_ctxt x, t)
   4.397  
   4.398  (* styp -> term -> term *)
   4.399  fun nth_arg_sel_term_for_constr (x as (s, T)) n =
   4.400 @@ -920,26 +940,6 @@
   4.401        | _ => list_comb (Const x, args)
   4.402      end
   4.403  
   4.404 -(* extended_context -> typ -> term -> term *)
   4.405 -fun constr_expand (ext_ctxt as {thy, ...}) T t =
   4.406 -  (case head_of t of
   4.407 -     Const x => if is_constr_like thy x then t else raise SAME ()
   4.408 -   | _ => raise SAME ())
   4.409 -  handle SAME () =>
   4.410 -         let
   4.411 -           val x' as (_, T') =
   4.412 -             if is_pair_type T then
   4.413 -               let val (T1, T2) = HOLogic.dest_prodT T in
   4.414 -                 (@{const_name Pair}, T1 --> T2 --> T)
   4.415 -               end
   4.416 -             else
   4.417 -               datatype_constrs ext_ctxt T |> hd
   4.418 -           val arg_Ts = binder_types T'
   4.419 -         in
   4.420 -           list_comb (Const x', map2 (select_nth_constr_arg thy x' t)
   4.421 -                                     (index_seq 0 (length arg_Ts)) arg_Ts)
   4.422 -         end
   4.423 -
   4.424  (* (typ * int) list -> typ -> int *)
   4.425  fun card_of_type assigns (Type ("fun", [T1, T2])) =
   4.426      reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
   4.427 @@ -975,8 +975,8 @@
   4.428                      card_of_type assigns T
   4.429                      handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
   4.430                             default_card)
   4.431 -(* extended_context -> int -> (typ * int) list -> typ -> int *)
   4.432 -fun bounded_exact_card_of_type ext_ctxt max default_card assigns T =
   4.433 +(* hol_context -> int -> (typ * int) list -> typ -> int *)
   4.434 +fun bounded_exact_card_of_type hol_ctxt max default_card assigns T =
   4.435    let
   4.436      (* typ list -> typ -> int *)
   4.437      fun aux avoid T =
   4.438 @@ -1006,13 +1006,13 @@
   4.439         | @{typ bool} => 2
   4.440         | @{typ unit} => 1
   4.441         | Type _ =>
   4.442 -         (case datatype_constrs ext_ctxt T of
   4.443 +         (case datatype_constrs hol_ctxt T of
   4.444              [] => if is_integer_type T orelse is_bit_type T then 0
   4.445                    else raise SAME ()
   4.446            | constrs =>
   4.447              let
   4.448                val constr_cards =
   4.449 -                datatype_constrs ext_ctxt T
   4.450 +                datatype_constrs hol_ctxt T
   4.451                  |> map (Integer.prod o map (aux (T :: avoid)) o binder_types
   4.452                          o snd)
   4.453              in
   4.454 @@ -1024,9 +1024,9 @@
   4.455               AList.lookup (op =) assigns T |> the_default default_card
   4.456    in Int.min (max, aux [] T) end
   4.457  
   4.458 -(* extended_context -> typ -> bool *)
   4.459 -fun is_finite_type ext_ctxt =
   4.460 -  not_equal 0 o bounded_exact_card_of_type ext_ctxt 1 2 []
   4.461 +(* hol_context -> typ -> bool *)
   4.462 +fun is_finite_type hol_ctxt =
   4.463 +  not_equal 0 o bounded_exact_card_of_type hol_ctxt 1 2 []
   4.464  
   4.465  (* term -> bool *)
   4.466  fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
   4.467 @@ -1052,7 +1052,7 @@
   4.468    member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
   4.469                   @{type_name int}] s orelse
   4.470    is_frac_type thy (Type (s, []))
   4.471 -(* theory -> term -> bool *)
   4.472 +(* theory -> typ -> bool *)
   4.473  fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
   4.474    | is_funky_typedef _ _ = false
   4.475  (* term -> bool *)
   4.476 @@ -1199,8 +1199,6 @@
   4.477        |> normalized_rhs_of thy |> Option.map (prefix_abs_vars s)
   4.478      handle List.Empty => NONE
   4.479  
   4.480 -datatype fixpoint_kind = Lfp | Gfp | NoFp
   4.481 -
   4.482  (* term -> fixpoint_kind *)
   4.483  fun fixpoint_kind_of_rhs (Abs (_, _, t)) = fixpoint_kind_of_rhs t
   4.484    | fixpoint_kind_of_rhs (Const (@{const_name lfp}, _) $ Abs _) = Lfp
   4.485 @@ -1299,35 +1297,6 @@
   4.486    Unsynchronized.change simp_table
   4.487        (Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s)))
   4.488  
   4.489 -(* Similar to "Refute.specialize_type" but returns all matches rather than only
   4.490 -   the first (preorder) match. *)
   4.491 -(* theory -> styp -> term -> term list *)
   4.492 -fun multi_specialize_type thy slack (x as (s, T)) t =
   4.493 -  let
   4.494 -    (* term -> (typ * term) list -> (typ * term) list *)
   4.495 -    fun aux (Const (s', T')) ys =
   4.496 -        if s = s' then
   4.497 -          ys |> (if AList.defined (op =) ys T' then
   4.498 -                   I
   4.499 -                 else
   4.500 -                  cons (T', Refute.monomorphic_term
   4.501 -                                (Sign.typ_match thy (T', T) Vartab.empty) t)
   4.502 -                  handle Type.TYPE_MATCH => I
   4.503 -                       | Refute.REFUTE _ =>
   4.504 -                         if slack then
   4.505 -                           I
   4.506 -                         else
   4.507 -                           raise NOT_SUPPORTED ("too much polymorphism in \
   4.508 -                                                \axiom involving " ^ quote s))
   4.509 -        else
   4.510 -          ys
   4.511 -      | aux _ ys = ys
   4.512 -  in map snd (fold_aterms aux t []) end
   4.513 -
   4.514 -(* theory -> bool -> const_table -> styp -> term list *)
   4.515 -fun nondef_props_for_const thy slack table (x as (s, _)) =
   4.516 -  these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)
   4.517 -
   4.518  (* theory -> styp -> term list *)
   4.519  fun inverse_axioms_for_rep_fun thy (x as (_, T)) =
   4.520    let val abs_T = domain_type T in
   4.521 @@ -1336,7 +1305,7 @@
   4.522      |> pairself (Refute.specialize_type thy x o prop_of o the)
   4.523      ||> single |> op ::
   4.524    end
   4.525 -(* theory -> styp list -> term list *)
   4.526 +(* theory -> string * typ list -> term list *)
   4.527  fun optimized_typedef_axioms thy (abs_z as (abs_s, abs_Ts)) =
   4.528    let val abs_T = Type abs_z in
   4.529      if is_univ_typedef thy abs_T then
   4.530 @@ -1392,15 +1361,15 @@
   4.531      list_comb (Bound j, map2 (select_nth_constr_arg thy x (Bound 0))
   4.532                               (index_seq 0 (length arg_Ts)) arg_Ts)
   4.533    end
   4.534 -(* extended_context -> typ -> int * styp -> term -> term *)
   4.535 -fun add_constr_case (ext_ctxt as {thy, ...}) res_T (j, x) res_t =
   4.536 +(* hol_context -> typ -> int * styp -> term -> term *)
   4.537 +fun add_constr_case (hol_ctxt as {thy, ...}) res_T (j, x) res_t =
   4.538    Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
   4.539 -  $ discriminate_value ext_ctxt x (Bound 0) $ constr_case_body thy (j, x)
   4.540 +  $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body thy (j, x)
   4.541    $ res_t
   4.542 -(* extended_context -> typ -> typ -> term *)
   4.543 -fun optimized_case_def (ext_ctxt as {thy, ...}) dataT res_T =
   4.544 +(* hol_context -> typ -> typ -> term *)
   4.545 +fun optimized_case_def (hol_ctxt as {thy, ...}) dataT res_T =
   4.546    let
   4.547 -    val xs = datatype_constrs ext_ctxt dataT
   4.548 +    val xs = datatype_constrs hol_ctxt dataT
   4.549      val xs' = filter_out (fn (s, _) => s = @{const_name NonStd}) xs
   4.550      val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs'
   4.551    in
   4.552 @@ -1409,19 +1378,19 @@
   4.553           val (xs'', x) = split_last xs'
   4.554         in
   4.555           constr_case_body thy (1, x)
   4.556 -         |> fold_rev (add_constr_case ext_ctxt res_T)
   4.557 +         |> fold_rev (add_constr_case hol_ctxt res_T)
   4.558                       (length xs' downto 2 ~~ xs'')
   4.559         end
   4.560       else
   4.561         Const (@{const_name undefined}, dataT --> res_T) $ Bound 0
   4.562 -       |> fold_rev (add_constr_case ext_ctxt res_T)
   4.563 +       |> fold_rev (add_constr_case hol_ctxt res_T)
   4.564                     (length xs' downto 1 ~~ xs'))
   4.565      |> fold_rev (curry absdummy) (func_Ts @ [dataT])
   4.566    end
   4.567  
   4.568 -(* extended_context -> string -> typ -> typ -> term -> term *)
   4.569 -fun optimized_record_get (ext_ctxt as {thy, ...}) s rec_T res_T t =
   4.570 -  let val constr_x = hd (datatype_constrs ext_ctxt rec_T) in
   4.571 +(* hol_context -> string -> typ -> typ -> term -> term *)
   4.572 +fun optimized_record_get (hol_ctxt as {thy, ...}) s rec_T res_T t =
   4.573 +  let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
   4.574      case no_of_record_field thy s rec_T of
   4.575        ~1 => (case rec_T of
   4.576                 Type (_, Ts as _ :: _) =>
   4.577 @@ -1430,16 +1399,16 @@
   4.578                   val j = num_record_fields thy rec_T - 1
   4.579                 in
   4.580                   select_nth_constr_arg thy constr_x t j res_T
   4.581 -                 |> optimized_record_get ext_ctxt s rec_T' res_T
   4.582 +                 |> optimized_record_get hol_ctxt s rec_T' res_T
   4.583                 end
   4.584               | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
   4.585                                  []))
   4.586      | j => select_nth_constr_arg thy constr_x t j res_T
   4.587    end
   4.588 -(* extended_context -> string -> typ -> term -> term -> term *)
   4.589 -fun optimized_record_update (ext_ctxt as {thy, ...}) s rec_T fun_t rec_t =
   4.590 +(* hol_context -> string -> typ -> term -> term -> term *)
   4.591 +fun optimized_record_update (hol_ctxt as {thy, ...}) s rec_T fun_t rec_t =
   4.592    let
   4.593 -    val constr_x as (_, constr_T) = hd (datatype_constrs ext_ctxt rec_T)
   4.594 +    val constr_x as (_, constr_T) = hd (datatype_constrs hol_ctxt rec_T)
   4.595      val Ts = binder_types constr_T
   4.596      val n = length Ts
   4.597      val special_j = no_of_record_field thy s rec_T
   4.598 @@ -1450,7 +1419,7 @@
   4.599                          if j = special_j then
   4.600                            betapply (fun_t, t)
   4.601                          else if j = n - 1 andalso special_j = ~1 then
   4.602 -                          optimized_record_update ext_ctxt s
   4.603 +                          optimized_record_update hol_ctxt s
   4.604                                (rec_T |> dest_Type |> snd |> List.last) fun_t t
   4.605                          else
   4.606                            t
   4.607 @@ -1473,19 +1442,19 @@
   4.608      fixpoint_kind_of_rhs (the (def_of_const thy table x))
   4.609      handle Option.Option => NoFp
   4.610  
   4.611 -(* extended_context -> styp -> bool *)
   4.612 +(* hol_context -> styp -> bool *)
   4.613  fun is_real_inductive_pred ({thy, fast_descrs, def_table, intro_table, ...}
   4.614 -                            : extended_context) x =
   4.615 +                            : hol_context) x =
   4.616    not (null (def_props_for_const thy fast_descrs intro_table x)) andalso
   4.617    fixpoint_kind_of_const thy def_table x <> NoFp
   4.618  fun is_real_equational_fun ({thy, fast_descrs, simp_table, psimp_table, ...}
   4.619 -                            : extended_context) x =
   4.620 +                            : hol_context) x =
   4.621    exists (fn table => not (null (def_props_for_const thy fast_descrs table x)))
   4.622           [!simp_table, psimp_table]
   4.623 -fun is_inductive_pred ext_ctxt =
   4.624 -  is_real_inductive_pred ext_ctxt andf (not o is_real_equational_fun ext_ctxt)
   4.625 -fun is_equational_fun (ext_ctxt as {thy, def_table, ...}) =
   4.626 -  (is_real_equational_fun ext_ctxt orf is_real_inductive_pred ext_ctxt
   4.627 +fun is_inductive_pred hol_ctxt =
   4.628 +  is_real_inductive_pred hol_ctxt andf (not o is_real_equational_fun hol_ctxt)
   4.629 +fun is_equational_fun (hol_ctxt as {thy, def_table, ...}) =
   4.630 +  (is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt
   4.631     orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
   4.632    andf (not o has_trivial_definition thy def_table)
   4.633  
   4.634 @@ -1522,11 +1491,11 @@
   4.635      SOME t' => is_constr_pattern_lhs thy t'
   4.636    | NONE => false
   4.637  
   4.638 +(* Prevents divergence in case of cyclic or infinite definition dependencies. *)
   4.639  val unfold_max_depth = 255
   4.640 -val axioms_max_depth = 255
   4.641  
   4.642 -(* extended_context -> term -> term *)
   4.643 -fun unfold_defs_in_term (ext_ctxt as {thy, destroy_constrs, fast_descrs,
   4.644 +(* hol_context -> term -> term *)
   4.645 +fun unfold_defs_in_term (hol_ctxt as {thy, destroy_constrs, fast_descrs,
   4.646                                        case_names, def_table, ground_thm_table,
   4.647                                        ersatz_table, ...}) =
   4.648    let
   4.649 @@ -1600,7 +1569,7 @@
   4.650                  val (dataT, res_T) = nth_range_type n T
   4.651                                       |> pairf domain_type range_type
   4.652                in
   4.653 -                (optimized_case_def ext_ctxt dataT res_T
   4.654 +                (optimized_case_def hol_ctxt dataT res_T
   4.655                   |> do_term (depth + 1) Ts, ts)
   4.656                end
   4.657              | _ =>
   4.658 @@ -1628,11 +1597,11 @@
   4.659                else if is_record_get thy x then
   4.660                  case length ts of
   4.661                    0 => (do_term depth Ts (eta_expand Ts t 1), [])
   4.662 -                | _ => (optimized_record_get ext_ctxt s (domain_type T)
   4.663 +                | _ => (optimized_record_get hol_ctxt s (domain_type T)
   4.664                              (range_type T) (do_term depth Ts (hd ts)), tl ts)
   4.665                else if is_record_update thy x then
   4.666                  case length ts of
   4.667 -                  2 => (optimized_record_update ext_ctxt
   4.668 +                  2 => (optimized_record_update hol_ctxt
   4.669                              (unsuffix Record.updateN s) (nth_range_type 2 T)
   4.670                              (do_term depth Ts (hd ts))
   4.671                              (do_term depth Ts (nth ts 1)), [])
   4.672 @@ -1645,7 +1614,7 @@
   4.673                    else
   4.674                      (Const x, ts)
   4.675                  end
   4.676 -              else if is_equational_fun ext_ctxt x then
   4.677 +              else if is_equational_fun hol_ctxt x then
   4.678                  (Const x, ts)
   4.679                else case def_of_const thy def_table x of
   4.680                  SOME def =>
   4.681 @@ -1662,10 +1631,10 @@
   4.682          in s_betapplys (const, map (do_term depth Ts) ts) |> Envir.beta_norm end
   4.683    in do_term 0 [] end
   4.684  
   4.685 -(* extended_context -> typ -> term list *)
   4.686 -fun codatatype_bisim_axioms (ext_ctxt as {thy, ...}) T =
   4.687 +(* hol_context -> typ -> term list *)
   4.688 +fun codatatype_bisim_axioms (hol_ctxt as {thy, ...}) T =
   4.689    let
   4.690 -    val xs = datatype_constrs ext_ctxt T
   4.691 +    val xs = datatype_constrs hol_ctxt T
   4.692      val set_T = T --> bool_T
   4.693      val iter_T = @{typ bisim_iterator}
   4.694      val bisim_const = Const (@{const_name bisim}, iter_T --> T --> T --> bool_T)
   4.695 @@ -1688,14 +1657,14 @@
   4.696        let
   4.697          val arg_Ts = binder_types T
   4.698          val core_t =
   4.699 -          discriminate_value ext_ctxt x y_var ::
   4.700 +          discriminate_value hol_ctxt x y_var ::
   4.701            map2 (nth_sub_bisim x) (index_seq 0 (length arg_Ts)) arg_Ts
   4.702            |> foldr1 s_conj
   4.703        in List.foldr absdummy core_t arg_Ts end
   4.704    in
   4.705      [HOLogic.eq_const bool_T $ (bisim_const $ n_var $ x_var $ y_var)
   4.706       $ (@{term "op |"} $ (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T)
   4.707 -        $ (betapplys (optimized_case_def ext_ctxt T bool_T,
   4.708 +        $ (betapplys (optimized_case_def hol_ctxt T bool_T,
   4.709                        map case_func xs @ [x_var]))),
   4.710       HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var)
   4.711       $ (Const (@{const_name insert}, T --> set_T --> set_T)
   4.712 @@ -1754,10 +1723,10 @@
   4.713  val termination_tacs = [Lexicographic_Order.lex_order_tac true,
   4.714                          ScnpReconstruct.sizechange_tac]
   4.715  
   4.716 -(* extended_context -> const_table -> styp -> bool *)
   4.717 +(* hol_context -> const_table -> styp -> bool *)
   4.718  fun uncached_is_well_founded_inductive_pred
   4.719          ({thy, ctxt, debug, fast_descrs, tac_timeout, intro_table, ...}
   4.720 -         : extended_context) (x as (_, T)) =
   4.721 +         : hol_context) (x as (_, T)) =
   4.722    case def_props_for_const thy fast_descrs intro_table x of
   4.723      [] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
   4.724                        [Const x])
   4.725 @@ -1797,11 +1766,11 @@
   4.726      handle List.Empty => false
   4.727           | NO_TRIPLE () => false
   4.728  
   4.729 -(* The type constraint below is a workaround for a Poly/ML bug. *)
   4.730 +(* The type constraint below is a workaround for a Poly/ML crash. *)
   4.731  
   4.732 -(* extended_context -> styp -> bool *)
   4.733 +(* hol_context -> styp -> bool *)
   4.734  fun is_well_founded_inductive_pred
   4.735 -        (ext_ctxt as {thy, wfs, def_table, wf_cache, ...} : extended_context)
   4.736 +        (hol_ctxt as {thy, wfs, def_table, wf_cache, ...} : hol_context)
   4.737          (x as (s, _)) =
   4.738    case triple_lookup (const_match thy) wfs x of
   4.739      SOME (SOME b) => b
   4.740 @@ -1811,7 +1780,7 @@
   4.741                  | NONE =>
   4.742                    let
   4.743                      val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
   4.744 -                    val wf = uncached_is_well_founded_inductive_pred ext_ctxt x
   4.745 +                    val wf = uncached_is_well_founded_inductive_pred hol_ctxt x
   4.746                    in
   4.747                      Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
   4.748                    end
   4.749 @@ -1842,14 +1811,14 @@
   4.750        | do_disjunct j t =
   4.751          case num_occs_of_bound_in_term j t of
   4.752            0 => true
   4.753 -        | 1 => exists (curry (op =) (Bound j) o head_of) (conjuncts t)
   4.754 +        | 1 => exists (curry (op =) (Bound j) o head_of) (conjuncts_of t)
   4.755          | _ => false
   4.756      (* term -> bool *)
   4.757      fun do_lfp_def (Const (@{const_name lfp}, _) $ t2) =
   4.758          let val (xs, body) = strip_abs t2 in
   4.759            case length xs of
   4.760              1 => false
   4.761 -          | n => forall (do_disjunct (n - 1)) (disjuncts body)
   4.762 +          | n => forall (do_disjunct (n - 1)) (disjuncts_of body)
   4.763          end
   4.764        | do_lfp_def _ = false
   4.765    in do_lfp_def o strip_abs_body end
   4.766 @@ -1887,7 +1856,7 @@
   4.767                end
   4.768            val (nonrecs, recs) =
   4.769              List.partition (curry (op =) 0 o num_occs_of_bound_in_term j)
   4.770 -                           (disjuncts body)
   4.771 +                           (disjuncts_of body)
   4.772            val base_body = nonrecs |> List.foldl s_disj @{const False}
   4.773            val step_body = recs |> map (repair_rec j)
   4.774                                 |> List.foldl s_disj @{const False} 
   4.775 @@ -1901,8 +1870,8 @@
   4.776          raise TERM ("Nitpick_HOL.linear_pred_base_and_step_rhss.aux", [t])
   4.777    in aux end
   4.778  
   4.779 -(* extended_context -> styp -> term -> term *)
   4.780 -fun starred_linear_pred_const (ext_ctxt as {simp_table, ...}) (x as (s, T))
   4.781 +(* hol_context -> styp -> term -> term *)
   4.782 +fun starred_linear_pred_const (hol_ctxt as {simp_table, ...}) (x as (s, T))
   4.783                                def =
   4.784    let
   4.785      val j = maxidx_of_term def + 1
   4.786 @@ -1933,11 +1902,11 @@
   4.787                      $ list_comb (Const step_x, outer_bounds)))
   4.788                $ list_comb (Const base_x, outer_bounds)
   4.789                |> ap_curry tuple_arg_Ts tuple_T bool_T)
   4.790 -    |> unfold_defs_in_term ext_ctxt
   4.791 +    |> unfold_defs_in_term hol_ctxt
   4.792    end
   4.793  
   4.794 -(* extended_context -> bool -> styp -> term *)
   4.795 -fun unrolled_inductive_pred_const (ext_ctxt as {thy, star_linear_preds,
   4.796 +(* hol_context -> bool -> styp -> term *)
   4.797 +fun unrolled_inductive_pred_const (hol_ctxt as {thy, star_linear_preds,
   4.798                                                  def_table, simp_table, ...})
   4.799                                    gfp (x as (s, T)) =
   4.800    let
   4.801 @@ -1946,11 +1915,11 @@
   4.802      val unrolled_const = Const x' $ zero_const iter_T
   4.803      val def = the (def_of_const thy def_table x)
   4.804    in
   4.805 -    if is_equational_fun ext_ctxt x' then
   4.806 +    if is_equational_fun hol_ctxt x' then
   4.807        unrolled_const (* already done *)
   4.808      else if not gfp andalso is_linear_inductive_pred_def def andalso
   4.809           star_linear_preds then
   4.810 -      starred_linear_pred_const ext_ctxt x def
   4.811 +      starred_linear_pred_const hol_ctxt x def
   4.812      else
   4.813        let
   4.814          val j = maxidx_of_term def + 1
   4.815 @@ -1973,8 +1942,8 @@
   4.816        in unrolled_const end
   4.817    end
   4.818  
   4.819 -(* extended_context -> styp -> term *)
   4.820 -fun raw_inductive_pred_axiom ({thy, def_table, ...} : extended_context) x =
   4.821 +(* hol_context -> styp -> term *)
   4.822 +fun raw_inductive_pred_axiom ({thy, def_table, ...} : hol_context) x =
   4.823    let
   4.824      val def = the (def_of_const thy def_table x)
   4.825      val (outer, fp_app) = strip_abs def
   4.826 @@ -1992,24 +1961,29 @@
   4.827      HOLogic.mk_eq (list_comb (Const x, bounds), naked_rhs)
   4.828      |> HOLogic.mk_Trueprop |> curry subst_bounds (rev vars)
   4.829    end
   4.830 -fun inductive_pred_axiom ext_ctxt (x as (s, T)) =
   4.831 +fun inductive_pred_axiom hol_ctxt (x as (s, T)) =
   4.832    if String.isPrefix ubfp_prefix s orelse String.isPrefix lbfp_prefix s then
   4.833      let val x' = (after_name_sep s, T) in
   4.834 -      raw_inductive_pred_axiom ext_ctxt x' |> subst_atomic [(Const x', Const x)]
   4.835 +      raw_inductive_pred_axiom hol_ctxt x' |> subst_atomic [(Const x', Const x)]
   4.836      end
   4.837    else
   4.838 -    raw_inductive_pred_axiom ext_ctxt x
   4.839 +    raw_inductive_pred_axiom hol_ctxt x
   4.840  
   4.841 -(* extended_context -> styp -> term list *)
   4.842 -fun raw_equational_fun_axioms (ext_ctxt as {thy, fast_descrs, simp_table,
   4.843 +(* hol_context -> styp -> term list *)
   4.844 +fun raw_equational_fun_axioms (hol_ctxt as {thy, fast_descrs, simp_table,
   4.845                                              psimp_table, ...}) (x as (s, _)) =
   4.846    case def_props_for_const thy fast_descrs (!simp_table) x of
   4.847      [] => (case def_props_for_const thy fast_descrs psimp_table x of
   4.848 -             [] => [inductive_pred_axiom ext_ctxt x]
   4.849 +             [] => [inductive_pred_axiom hol_ctxt x]
   4.850             | psimps => psimps)
   4.851    | simps => simps
   4.852 -
   4.853  val equational_fun_axioms = map extensionalize oo raw_equational_fun_axioms
   4.854 +(* hol_context -> styp -> bool *)
   4.855 +fun is_equational_fun_surely_complete hol_ctxt x =
   4.856 +  case raw_equational_fun_axioms hol_ctxt x of
   4.857 +    [@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] =>
   4.858 +    strip_comb t1 |> snd |> forall is_Var
   4.859 +  | _ => false
   4.860  
   4.861  (* term list -> term list *)
   4.862  fun merge_type_vars_in_terms ts =
   4.863 @@ -2028,1261 +2002,27 @@
   4.864        | coalesce T = T
   4.865    in map (map_types (map_atyps coalesce)) ts end
   4.866  
   4.867 -(* extended_context -> typ -> typ list -> typ list *)
   4.868 -fun add_ground_types ext_ctxt T accum =
   4.869 +(* hol_context -> typ -> typ list -> typ list *)
   4.870 +fun add_ground_types hol_ctxt T accum =
   4.871    case T of
   4.872 -    Type ("fun", Ts) => fold (add_ground_types ext_ctxt) Ts accum
   4.873 -  | Type ("*", Ts) => fold (add_ground_types ext_ctxt) Ts accum
   4.874 -  | Type (@{type_name itself}, [T1]) => add_ground_types ext_ctxt T1 accum
   4.875 +    Type ("fun", Ts) => fold (add_ground_types hol_ctxt) Ts accum
   4.876 +  | Type ("*", Ts) => fold (add_ground_types hol_ctxt) Ts accum
   4.877 +  | Type (@{type_name itself}, [T1]) => add_ground_types hol_ctxt T1 accum
   4.878    | Type (_, Ts) =>
   4.879      if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum) T then
   4.880        accum
   4.881      else
   4.882        T :: accum
   4.883 -      |> fold (add_ground_types ext_ctxt)
   4.884 -              (case boxed_datatype_constrs ext_ctxt T of
   4.885 +      |> fold (add_ground_types hol_ctxt)
   4.886 +              (case boxed_datatype_constrs hol_ctxt T of
   4.887                   [] => Ts
   4.888                 | xs => map snd xs)
   4.889    | _ => insert (op =) T accum
   4.890 -(* extended_context -> typ -> typ list *)
   4.891 -fun ground_types_in_type ext_ctxt T = add_ground_types ext_ctxt T []
   4.892 -(* extended_context -> term list -> typ list *)
   4.893 -fun ground_types_in_terms ext_ctxt ts =
   4.894 -  fold (fold_types (add_ground_types ext_ctxt)) ts []
   4.895 -
   4.896 -(* typ list -> int -> term -> bool *)
   4.897 -fun has_heavy_bounds_or_vars Ts level t =
   4.898 -  let
   4.899 -    (* typ list -> bool *)
   4.900 -    fun aux [] = false
   4.901 -      | aux [T] = is_fun_type T orelse is_pair_type T
   4.902 -      | aux _ = true
   4.903 -  in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
   4.904 -
   4.905 -(* typ list -> int -> int -> int -> term -> term *)
   4.906 -fun fresh_value_var Ts k n j t =
   4.907 -  Var ((val_var_prefix ^ nat_subscript (n - j), k), fastype_of1 (Ts, t))
   4.908 -
   4.909 -(* theory -> typ list -> bool -> int -> int -> term -> term list -> term list
   4.910 -   -> term * term list *)
   4.911 -fun pull_out_constr_comb thy Ts relax k level t args seen =
   4.912 -  let val t_comb = list_comb (t, args) in
   4.913 -    case t of
   4.914 -      Const x =>
   4.915 -      if not relax andalso is_constr thy x andalso
   4.916 -         not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso
   4.917 -         has_heavy_bounds_or_vars Ts level t_comb andalso
   4.918 -         not (loose_bvar (t_comb, level)) then
   4.919 -        let
   4.920 -          val (j, seen) = case find_index (curry (op =) t_comb) seen of
   4.921 -                            ~1 => (0, t_comb :: seen)
   4.922 -                          | j => (j, seen)
   4.923 -        in (fresh_value_var Ts k (length seen) j t_comb, seen) end
   4.924 -      else
   4.925 -        (t_comb, seen)
   4.926 -    | _ => (t_comb, seen)
   4.927 -  end
   4.928 -
   4.929 -(* (term -> term) -> typ list -> int -> term list -> term list *)
   4.930 -fun equations_for_pulled_out_constrs mk_eq Ts k seen =
   4.931 -  let val n = length seen in
   4.932 -    map2 (fn j => fn t => mk_eq (fresh_value_var Ts k n j t, t))
   4.933 -         (index_seq 0 n) seen
   4.934 -  end
   4.935 -
   4.936 -(* theory -> bool -> term -> term *)
   4.937 -fun pull_out_universal_constrs thy def t =
   4.938 -  let
   4.939 -    val k = maxidx_of_term t + 1
   4.940 -    (* typ list -> bool -> term -> term list -> term list -> term * term list *)
   4.941 -    fun do_term Ts def t args seen =
   4.942 -      case t of
   4.943 -        (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 =>
   4.944 -        do_eq_or_imp Ts true def t0 t1 t2 seen
   4.945 -      | (t0 as @{const "==>"}) $ t1 $ t2 =>
   4.946 -        if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
   4.947 -      | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
   4.948 -        do_eq_or_imp Ts true def t0 t1 t2 seen
   4.949 -      | (t0 as @{const "op -->"}) $ t1 $ t2 =>
   4.950 -        do_eq_or_imp Ts false def t0 t1 t2 seen
   4.951 -      | Abs (s, T, t') =>
   4.952 -        let val (t', seen) = do_term (T :: Ts) def t' [] seen in
   4.953 -          (list_comb (Abs (s, T, t'), args), seen)
   4.954 -        end
   4.955 -      | t1 $ t2 =>
   4.956 -        let val (t2, seen) = do_term Ts def t2 [] seen in
   4.957 -          do_term Ts def t1 (t2 :: args) seen
   4.958 -        end
   4.959 -      | _ => pull_out_constr_comb thy Ts def k 0 t args seen
   4.960 -    (* typ list -> bool -> bool -> term -> term -> term -> term list
   4.961 -       -> term * term list *)
   4.962 -    and do_eq_or_imp Ts eq def t0 t1 t2 seen =
   4.963 -      let
   4.964 -        val (t2, seen) = if eq andalso def then (t2, seen)
   4.965 -                         else do_term Ts false t2 [] seen
   4.966 -        val (t1, seen) = do_term Ts false t1 [] seen
   4.967 -      in (t0 $ t1 $ t2, seen) end
   4.968 -    val (concl, seen) = do_term [] def t [] []
   4.969 -  in
   4.970 -    Logic.list_implies (equations_for_pulled_out_constrs Logic.mk_equals [] k
   4.971 -                                                         seen, concl)
   4.972 -  end
   4.973 -
   4.974 -(* extended_context -> bool -> term -> term *)
   4.975 -fun destroy_pulled_out_constrs (ext_ctxt as {thy, ...}) axiom t =
   4.976 -  let
   4.977 -    (* styp -> int *)
   4.978 -    val num_occs_of_var =
   4.979 -      fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
   4.980 -                    | _ => I) t (K 0)
   4.981 -    (* bool -> term -> term *)
   4.982 -    fun aux careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =
   4.983 -        aux_eq careful true t0 t1 t2
   4.984 -      | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =
   4.985 -        t0 $ aux false t1 $ aux careful t2
   4.986 -      | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
   4.987 -        aux_eq careful true t0 t1 t2
   4.988 -      | aux careful ((t0 as @{const "op -->"}) $ t1 $ t2) =
   4.989 -        t0 $ aux false t1 $ aux careful t2
   4.990 -      | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')
   4.991 -      | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2
   4.992 -      | aux _ t = t
   4.993 -    (* bool -> bool -> term -> term -> term -> term *)
   4.994 -    and aux_eq careful pass1 t0 t1 t2 =
   4.995 -      ((if careful then
   4.996 -          raise SAME ()
   4.997 -        else if axiom andalso is_Var t2 andalso
   4.998 -                num_occs_of_var (dest_Var t2) = 1 then
   4.999 -          @{const True}
  4.1000 -        else case strip_comb t2 of
  4.1001 -          (* The first case is not as general as it could be. *)
  4.1002 -          (Const (@{const_name PairBox}, _),
  4.1003 -                  [Const (@{const_name fst}, _) $ Var z1,
  4.1004 -                   Const (@{const_name snd}, _) $ Var z2]) =>
  4.1005 -          if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True}
  4.1006 -          else raise SAME ()
  4.1007 -        | (Const (x as (s, T)), args) =>
  4.1008 -          let val arg_Ts = binder_types T in
  4.1009 -            if length arg_Ts = length args andalso
  4.1010 -               (is_constr thy x orelse s = @{const_name Pair} orelse
  4.1011 -                x = (@{const_name Suc}, nat_T --> nat_T)) andalso
  4.1012 -               (not careful orelse not (is_Var t1) orelse
  4.1013 -                String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
  4.1014 -              discriminate_value ext_ctxt x t1 ::
  4.1015 -              map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
  4.1016 -              |> foldr1 s_conj
  4.1017 -            else
  4.1018 -              raise SAME ()
  4.1019 -          end
  4.1020 -        | _ => raise SAME ())
  4.1021 -       |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop)
  4.1022 -      handle SAME () => if pass1 then aux_eq careful false t0 t2 t1
  4.1023 -                        else t0 $ aux false t2 $ aux false t1
  4.1024 -    (* styp -> term -> int -> typ -> term -> term *)
  4.1025 -    and sel_eq x t n nth_T nth_t =
  4.1026 -      HOLogic.eq_const nth_T $ nth_t $ select_nth_constr_arg thy x t n nth_T
  4.1027 -      |> aux false
  4.1028 -  in aux axiom t end
  4.1029 -
  4.1030 -(* theory -> term -> term *)
  4.1031 -fun simplify_constrs_and_sels thy t =
  4.1032 -  let
  4.1033 -    (* term -> int -> term *)
  4.1034 -    fun is_nth_sel_on t' n (Const (s, _) $ t) =
  4.1035 -        (t = t' andalso is_sel_like_and_no_discr s andalso
  4.1036 -         sel_no_from_name s = n)
  4.1037 -      | is_nth_sel_on _ _ _ = false
  4.1038 -    (* term -> term list -> term *)
  4.1039 -    fun do_term (Const (@{const_name Rep_Frac}, _)
  4.1040 -                 $ (Const (@{const_name Abs_Frac}, _) $ t1)) [] = do_term t1 []
  4.1041 -      | do_term (Const (@{const_name Abs_Frac}, _)
  4.1042 -                 $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 []
  4.1043 -      | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)
  4.1044 -      | do_term (t as Const (x as (s, T))) (args as _ :: _) =
  4.1045 -        ((if is_constr_like thy x then
  4.1046 -            if length args = num_binder_types T then
  4.1047 -              case hd args of
  4.1048 -                Const (x' as (_, T')) $ t' =>
  4.1049 -                if domain_type T' = body_type T andalso
  4.1050 -                   forall (uncurry (is_nth_sel_on t'))
  4.1051 -                          (index_seq 0 (length args) ~~ args) then
  4.1052 -                  t'
  4.1053 -                else
  4.1054 -                  raise SAME ()
  4.1055 -              | _ => raise SAME ()
  4.1056 -            else
  4.1057 -              raise SAME ()
  4.1058 -          else if is_sel_like_and_no_discr s then
  4.1059 -            case strip_comb (hd args) of
  4.1060 -              (Const (x' as (s', T')), ts') =>
  4.1061 -              if is_constr_like thy x' andalso
  4.1062 -                 constr_name_for_sel_like s = s' andalso
  4.1063 -                 not (exists is_pair_type (binder_types T')) then
  4.1064 -                list_comb (nth ts' (sel_no_from_name s), tl args)
  4.1065 -              else
  4.1066 -                raise SAME ()
  4.1067 -            | _ => raise SAME ()
  4.1068 -          else
  4.1069 -            raise SAME ())
  4.1070 -         handle SAME () => betapplys (t, args))
  4.1071 -      | do_term (Abs (s, T, t')) args =
  4.1072 -        betapplys (Abs (s, T, do_term t' []), args)
  4.1073 -      | do_term t args = betapplys (t, args)
  4.1074 -  in do_term t [] end
  4.1075 -
  4.1076 -(* term -> term *)
  4.1077 -fun curry_assms (@{const "==>"} $ (@{const Trueprop}
  4.1078 -                                   $ (@{const "op &"} $ t1 $ t2)) $ t3) =
  4.1079 -    curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
  4.1080 -  | curry_assms (@{const "==>"} $ t1 $ t2) =
  4.1081 -    @{const "==>"} $ curry_assms t1 $ curry_assms t2
  4.1082 -  | curry_assms t = t
  4.1083 -
  4.1084 -(* term -> term *)
  4.1085 -val destroy_universal_equalities =
  4.1086 -  let
  4.1087 -    (* term list -> (indexname * typ) list -> term -> term *)
  4.1088 -    fun aux prems zs t =
  4.1089 -      case t of
  4.1090 -        @{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2
  4.1091 -      | _ => Logic.list_implies (rev prems, t)
  4.1092 -    (* term list -> (indexname * typ) list -> term -> term -> term *)
  4.1093 -    and aux_implies prems zs t1 t2 =
  4.1094 -      case t1 of
  4.1095 -        Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
  4.1096 -      | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') =>
  4.1097 -        aux_eq prems zs z t' t1 t2
  4.1098 -      | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) =>
  4.1099 -        aux_eq prems zs z t' t1 t2
  4.1100 -      | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
  4.1101 -    (* term list -> (indexname * typ) list -> indexname * typ -> term -> term
  4.1102 -       -> term -> term *)
  4.1103 -    and aux_eq prems zs z t' t1 t2 =
  4.1104 -      if not (member (op =) zs z) andalso
  4.1105 -         not (exists_subterm (curry (op =) (Var z)) t') then
  4.1106 -        aux prems zs (subst_free [(Var z, t')] t2)
  4.1107 -      else
  4.1108 -        aux (t1 :: prems) (Term.add_vars t1 zs) t2
  4.1109 -  in aux [] [] end
  4.1110 -
  4.1111 -(* theory -> term -> term *)
  4.1112 -fun pull_out_existential_constrs thy t =
  4.1113 -  let
  4.1114 -    val k = maxidx_of_term t + 1
  4.1115 -    (* typ list -> int -> term -> term list -> term list -> term * term list *)
  4.1116 -    fun aux Ts num_exists t args seen =
  4.1117 -      case t of
  4.1118 -        (t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1) =>
  4.1119 -        let
  4.1120 -          val (t1, seen') = aux (T1 :: Ts) (num_exists + 1) t1 [] []
  4.1121 -          val n = length seen'
  4.1122 -          (* unit -> term list *)
  4.1123 -          fun vars () = map2 (fresh_value_var Ts k n) (index_seq 0 n) seen'
  4.1124 -        in
  4.1125 -          (equations_for_pulled_out_constrs HOLogic.mk_eq Ts k seen'
  4.1126 -           |> List.foldl s_conj t1 |> fold mk_exists (vars ())
  4.1127 -           |> curry3 Abs s1 T1 |> curry (op $) t0, seen)
  4.1128 -        end
  4.1129 -      | t1 $ t2 =>
  4.1130 -        let val (t2, seen) = aux Ts num_exists t2 [] seen in
  4.1131 -          aux Ts num_exists t1 (t2 :: args) seen
  4.1132 -        end
  4.1133 -      | Abs (s, T, t') =>
  4.1134 -        let
  4.1135 -          val (t', seen) = aux (T :: Ts) 0 t' [] (map (incr_boundvars 1) seen)
  4.1136 -        in (list_comb (Abs (s, T, t'), args), map (incr_boundvars ~1) seen) end
  4.1137 -      | _ =>
  4.1138 -        if num_exists > 0 then
  4.1139 -          pull_out_constr_comb thy Ts false k num_exists t args seen
  4.1140 -        else
  4.1141 -          (list_comb (t, args), seen)
  4.1142 -  in aux [] 0 t [] [] |> fst end
  4.1143 -
  4.1144 -(* theory -> int -> term list -> term list -> (term * term list) option *)
  4.1145 -fun find_bound_assign _ _ _ [] = NONE
  4.1146 -  | find_bound_assign thy j seen (t :: ts) =
  4.1147 -    let
  4.1148 -      (* bool -> term -> term -> (term * term list) option *)
  4.1149 -      fun aux pass1 t1 t2 =
  4.1150 -        (if loose_bvar1 (t2, j) then
  4.1151 -           if pass1 then aux false t2 t1 else raise SAME ()
  4.1152 -         else case t1 of
  4.1153 -           Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()
  4.1154 -         | Const (s, Type ("fun", [T1, T2])) $ Bound j' =>
  4.1155 -           if j' = j andalso s = sel_prefix_for 0 ^ @{const_name FunBox} then
  4.1156 -             SOME (construct_value thy (@{const_name FunBox}, T2 --> T1) [t2],
  4.1157 -                   ts @ seen)
  4.1158 -           else
  4.1159 -             raise SAME ()
  4.1160 -         | _ => raise SAME ())
  4.1161 -        handle SAME () => find_bound_assign thy j (t :: seen) ts
  4.1162 -    in
  4.1163 -      case t of
  4.1164 -        Const (@{const_name "op ="}, _) $ t1 $ t2 => aux true t1 t2
  4.1165 -      | _ => find_bound_assign thy j (t :: seen) ts
  4.1166 -    end
  4.1167 -
  4.1168 -(* int -> term -> term -> term *)
  4.1169 -fun subst_one_bound j arg t =
  4.1170 -  let
  4.1171 -    fun aux (Bound i, lev) =
  4.1172 -        if i < lev then raise SAME ()
  4.1173 -        else if i = lev then incr_boundvars (lev - j) arg
  4.1174 -        else Bound (i - 1)
  4.1175 -      | aux (Abs (a, T, body), lev) = Abs (a, T, aux (body, lev + 1))
  4.1176 -      | aux (f $ t, lev) =
  4.1177 -        (aux (f, lev) $ (aux (t, lev) handle SAME () => t)
  4.1178 -         handle SAME () => f $ aux (t, lev))
  4.1179 -      | aux _ = raise SAME ()
  4.1180 -  in aux (t, j) handle SAME () => t end
  4.1181 -
  4.1182 -(* theory -> term -> term *)
  4.1183 -fun destroy_existential_equalities thy =
  4.1184 -  let
  4.1185 -    (* string list -> typ list -> term list -> term *)
  4.1186 -    fun kill [] [] ts = foldr1 s_conj ts
  4.1187 -      | kill (s :: ss) (T :: Ts) ts =
  4.1188 -        (case find_bound_assign thy (length ss) [] ts of
  4.1189 -           SOME (_, []) => @{const True}
  4.1190 -         | SOME (arg_t, ts) =>
  4.1191 -           kill ss Ts (map (subst_one_bound (length ss)
  4.1192 -                                (incr_bv (~1, length ss + 1, arg_t))) ts)
  4.1193 -         | NONE =>
  4.1194 -           Const (@{const_name Ex}, (T --> bool_T) --> bool_T)
  4.1195 -           $ Abs (s, T, kill ss Ts ts))
  4.1196 -      | kill _ _ _ = raise UnequalLengths
  4.1197 -    (* string list -> typ list -> term -> term *)
  4.1198 -    fun gather ss Ts ((t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1)) =
  4.1199 -        gather (ss @ [s1]) (Ts @ [T1]) t1
  4.1200 -      | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)
  4.1201 -      | gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2
  4.1202 -      | gather [] [] t = t
  4.1203 -      | gather ss Ts t = kill ss Ts (conjuncts (gather [] [] t))
  4.1204 -  in gather [] [] end
  4.1205 -
  4.1206 -(* term -> term *)
  4.1207 -fun distribute_quantifiers t =
  4.1208 -  case t of
  4.1209 -    (t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) =>
  4.1210 -    (case t1 of
  4.1211 -       (t10 as @{const "op &"}) $ t11 $ t12 =>
  4.1212 -       t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
  4.1213 -           $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
  4.1214 -     | (t10 as @{const Not}) $ t11 =>
  4.1215 -       t10 $ distribute_quantifiers (Const (@{const_name Ex}, T0)
  4.1216 -                                     $ Abs (s, T1, t11))
  4.1217 -     | t1 =>
  4.1218 -       if not (loose_bvar1 (t1, 0)) then
  4.1219 -         distribute_quantifiers (incr_boundvars ~1 t1)
  4.1220 -       else
  4.1221 -         t0 $ Abs (s, T1, distribute_quantifiers t1))
  4.1222 -  | (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) =>
  4.1223 -    (case distribute_quantifiers t1 of
  4.1224 -       (t10 as @{const "op |"}) $ t11 $ t12 =>
  4.1225 -       t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
  4.1226 -           $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
  4.1227 -     | (t10 as @{const "op -->"}) $ t11 $ t12 =>
  4.1228 -       t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
  4.1229 -                                     $ Abs (s, T1, t11))
  4.1230 -           $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
  4.1231 -     | (t10 as @{const Not}) $ t11 =>
  4.1232 -       t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
  4.1233 -                                     $ Abs (s, T1, t11))
  4.1234 -     | t1 =>
  4.1235 -       if not (loose_bvar1 (t1, 0)) then
  4.1236 -         distribute_quantifiers (incr_boundvars ~1 t1)
  4.1237 -       else
  4.1238 -         t0 $ Abs (s, T1, distribute_quantifiers t1))
  4.1239 -  | t1 $ t2 => distribute_quantifiers t1 $ distribute_quantifiers t2
  4.1240 -  | Abs (s, T, t') => Abs (s, T, distribute_quantifiers t')
  4.1241 -  | _ => t
  4.1242 -
  4.1243 -(* int -> int -> (int -> int) -> term -> term *)
  4.1244 -fun renumber_bounds j n f t =
  4.1245 -  case t of
  4.1246 -    t1 $ t2 => renumber_bounds j n f t1 $ renumber_bounds j n f t2
  4.1247 -  | Abs (s, T, t') => Abs (s, T, renumber_bounds (j + 1) n f t')
  4.1248 -  | Bound j' =>
  4.1249 -    Bound (if j' >= j andalso j' < j + n then f (j' - j) + j else j')
  4.1250 -  | _ => t
  4.1251 -
  4.1252 -val quantifier_cluster_threshold = 7
  4.1253 -
  4.1254 -(* theory -> term -> term *)
  4.1255 -fun push_quantifiers_inward thy =
  4.1256 -  let
  4.1257 -    (* string -> string list -> typ list -> term -> term *)
  4.1258 -    fun aux quant_s ss Ts t =
  4.1259 -      (case t of
  4.1260 -         (t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) =>
  4.1261 -         if s0 = quant_s then
  4.1262 -           aux s0 (s1 :: ss) (T1 :: Ts) t1
  4.1263 -         else if quant_s = "" andalso
  4.1264 -                 (s0 = @{const_name All} orelse s0 = @{const_name Ex}) then
  4.1265 -           aux s0 [s1] [T1] t1
  4.1266 -         else
  4.1267 -           raise SAME ()
  4.1268 -       | _ => raise SAME ())
  4.1269 -      handle SAME () =>
  4.1270 -             case t of
  4.1271 -               t1 $ t2 =>
  4.1272 -               if quant_s = "" then
  4.1273 -                 aux "" [] [] t1 $ aux "" [] [] t2
  4.1274 -               else
  4.1275 -                 let
  4.1276 -                   val typical_card = 4
  4.1277 -                   (* ('a -> ''b list) -> 'a list -> ''b list *)
  4.1278 -                   fun big_union proj ps =
  4.1279 -                     fold (fold (insert (op =)) o proj) ps []
  4.1280 -                   val (ts, connective) = strip_any_connective t
  4.1281 -                   val T_costs =
  4.1282 -                     map (bounded_card_of_type 65536 typical_card []) Ts
  4.1283 -                   val t_costs = map size_of_term ts
  4.1284 -                   val num_Ts = length Ts
  4.1285 -                   (* int -> int *)
  4.1286 -                   val flip = curry (op -) (num_Ts - 1)
  4.1287 -                   val t_boundss = map (map flip o loose_bnos) ts
  4.1288 -                   (* (int list * int) list -> int list
  4.1289 -                      -> (int list * int) list *)
  4.1290 -                   fun merge costly_boundss [] = costly_boundss
  4.1291 -                     | merge costly_boundss (j :: js) =
  4.1292 -                       let
  4.1293 -                         val (yeas, nays) =
  4.1294 -                           List.partition (fn (bounds, _) =>
  4.1295 -                                              member (op =) bounds j)
  4.1296 -                                          costly_boundss
  4.1297 -                         val yeas_bounds = big_union fst yeas
  4.1298 -                         val yeas_cost = Integer.sum (map snd yeas)
  4.1299 -                                         * nth T_costs j
  4.1300 -                       in merge ((yeas_bounds, yeas_cost) :: nays) js end
  4.1301 -                   (* (int list * int) list -> int list -> int *)
  4.1302 -                   val cost = Integer.sum o map snd oo merge
  4.1303 -                   (* Inspired by Claessen & Sörensson's polynomial binary
  4.1304 -                      splitting heuristic (p. 5 of their MODEL 2003 paper). *)
  4.1305 -                   (* (int list * int) list -> int list -> int list *)
  4.1306 -                   fun heuristically_best_permutation _ [] = []
  4.1307 -                     | heuristically_best_permutation costly_boundss js =
  4.1308 -                       let
  4.1309 -                         val (costly_boundss, (j, js)) =
  4.1310 -                           js |> map (`(merge costly_boundss o single))
  4.1311 -                              |> sort (int_ord
  4.1312 -                                       o pairself (Integer.sum o map snd o fst))
  4.1313 -                              |> split_list |>> hd ||> pairf hd tl
  4.1314 -                       in
  4.1315 -                         j :: heuristically_best_permutation costly_boundss js
  4.1316 -                       end
  4.1317 -                   val js =
  4.1318 -                     if length Ts <= quantifier_cluster_threshold then
  4.1319 -                       all_permutations (index_seq 0 num_Ts)
  4.1320 -                       |> map (`(cost (t_boundss ~~ t_costs)))
  4.1321 -                       |> sort (int_ord o pairself fst) |> hd |> snd
  4.1322 -                     else
  4.1323 -                       heuristically_best_permutation (t_boundss ~~ t_costs)
  4.1324 -                                                      (index_seq 0 num_Ts)
  4.1325 -                   val back_js = map (fn j => find_index (curry (op =) j) js)
  4.1326 -                                     (index_seq 0 num_Ts)
  4.1327 -                   val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip))
  4.1328 -                                ts
  4.1329 -                   (* (term * int list) list -> term *)
  4.1330 -                   fun mk_connection [] =
  4.1331 -                       raise ARG ("Nitpick_HOL.push_quantifiers_inward.aux.\
  4.1332 -                                  \mk_connection", "")
  4.1333 -                     | mk_connection ts_cum_bounds =
  4.1334 -                       ts_cum_bounds |> map fst
  4.1335 -                       |> foldr1 (fn (t1, t2) => connective $ t1 $ t2)
  4.1336 -                   (* (term * int list) list -> int list -> term *)
  4.1337 -                   fun build ts_cum_bounds [] = ts_cum_bounds |> mk_connection
  4.1338 -                     | build ts_cum_bounds (j :: js) =
  4.1339 -                       let
  4.1340 -                         val (yeas, nays) =
  4.1341 -                           List.partition (fn (_, bounds) =>
  4.1342 -                                              member (op =) bounds j)
  4.1343 -                                          ts_cum_bounds
  4.1344 -                           ||> map (apfst (incr_boundvars ~1))
  4.1345 -                       in
  4.1346 -                         if null yeas then
  4.1347 -                           build nays js
  4.1348 -                         else
  4.1349 -                           let val T = nth Ts (flip j) in
  4.1350 -                             build ((Const (quant_s, (T --> bool_T) --> bool_T)
  4.1351 -                                     $ Abs (nth ss (flip j), T,
  4.1352 -                                            mk_connection yeas),
  4.1353 -                                      big_union snd yeas) :: nays) js
  4.1354 -                           end
  4.1355 -                       end
  4.1356 -                 in build (ts ~~ t_boundss) js end
  4.1357 -             | Abs (s, T, t') => Abs (s, T, aux "" [] [] t')
  4.1358 -             | _ => t
  4.1359 -  in aux "" [] [] end
  4.1360 -
  4.1361 -(* polarity -> string -> bool *)
  4.1362 -fun is_positive_existential polar quant_s =
  4.1363 -  (polar = Pos andalso quant_s = @{const_name Ex}) orelse
  4.1364 -  (polar = Neg andalso quant_s <> @{const_name Ex})
  4.1365 -
  4.1366 -(* extended_context -> int -> term -> term *)
  4.1367 -fun skolemize_term_and_more (ext_ctxt as {thy, def_table, skolems, ...})
  4.1368 -                            skolem_depth =
  4.1369 -  let
  4.1370 -    (* int list -> int list *)
  4.1371 -    val incrs = map (Integer.add 1)
  4.1372 -    (* string list -> typ list -> int list -> int -> polarity -> term -> term *)
  4.1373 -    fun aux ss Ts js depth polar t =
  4.1374 -      let
  4.1375 -        (* string -> typ -> string -> typ -> term -> term *)
  4.1376 -        fun do_quantifier quant_s quant_T abs_s abs_T t =
  4.1377 -          if not (loose_bvar1 (t, 0)) then
  4.1378 -            aux ss Ts js depth polar (incr_boundvars ~1 t)
  4.1379 -          else if depth <= skolem_depth andalso
  4.1380 -                  is_positive_existential polar quant_s then
  4.1381 -            let
  4.1382 -              val j = length (!skolems) + 1
  4.1383 -              val sko_s = skolem_prefix_for (length js) j ^ abs_s
  4.1384 -              val _ = Unsynchronized.change skolems (cons (sko_s, ss))
  4.1385 -              val sko_t = list_comb (Const (sko_s, rev Ts ---> abs_T),
  4.1386 -                                     map Bound (rev js))
  4.1387 -              val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) depth polar t)
  4.1388 -            in
  4.1389 -              if null js then betapply (abs_t, sko_t)
  4.1390 -              else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t $ abs_t
  4.1391 -            end
  4.1392 -          else
  4.1393 -            Const (quant_s, quant_T)
  4.1394 -            $ Abs (abs_s, abs_T,
  4.1395 -                   if is_higher_order_type abs_T then
  4.1396 -                     t
  4.1397 -                   else
  4.1398 -                     aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js)
  4.1399 -                         (depth + 1) polar t)
  4.1400 -      in
  4.1401 -        case t of
  4.1402 -          Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
  4.1403 -          do_quantifier s0 T0 s1 T1 t1
  4.1404 -        | @{const "==>"} $ t1 $ t2 =>
  4.1405 -          @{const "==>"} $ aux ss Ts js depth (flip_polarity polar) t1
  4.1406 -          $ aux ss Ts js depth polar t2
  4.1407 -        | @{const Pure.conjunction} $ t1 $ t2 =>
  4.1408 -          @{const Pure.conjunction} $ aux ss Ts js depth polar t1
  4.1409 -          $ aux ss Ts js depth polar t2
  4.1410 -        | @{const Trueprop} $ t1 =>
  4.1411 -          @{const Trueprop} $ aux ss Ts js depth polar t1
  4.1412 -        | @{const Not} $ t1 =>
  4.1413 -          @{const Not} $ aux ss Ts js depth (flip_polarity polar) t1
  4.1414 -        | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
  4.1415 -          do_quantifier s0 T0 s1 T1 t1
  4.1416 -        | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
  4.1417 -          do_quantifier s0 T0 s1 T1 t1
  4.1418 -        | @{const "op &"} $ t1 $ t2 =>
  4.1419 -          @{const "op &"} $ aux ss Ts js depth polar t1
  4.1420 -          $ aux ss Ts js depth polar t2
  4.1421 -        | @{const "op |"} $ t1 $ t2 =>
  4.1422 -          @{const "op |"} $ aux ss Ts js depth polar t1
  4.1423 -          $ aux ss Ts js depth polar t2
  4.1424 -        | @{const "op -->"} $ t1 $ t2 =>
  4.1425 -          @{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1
  4.1426 -          $ aux ss Ts js depth polar t2
  4.1427 -        | (t0 as Const (@{const_name Let}, T0)) $ t1 $ t2 =>
  4.1428 -          t0 $ t1 $ aux ss Ts js depth polar t2
  4.1429 -        | Const (x as (s, T)) =>
  4.1430 -          if is_inductive_pred ext_ctxt x andalso
  4.1431 -             not (is_well_founded_inductive_pred ext_ctxt x) then
  4.1432 -            let
  4.1433 -              val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
  4.1434 -              val (pref, connective, set_oper) =
  4.1435 -                if gfp then
  4.1436 -                  (lbfp_prefix,
  4.1437 -                   @{const "op |"},
  4.1438 -                   @{const_name upper_semilattice_fun_inst.sup_fun})
  4.1439 -                else
  4.1440 -                  (ubfp_prefix,
  4.1441 -                   @{const "op &"},
  4.1442 -                   @{const_name lower_semilattice_fun_inst.inf_fun})
  4.1443 -              (* unit -> term *)
  4.1444 -              fun pos () = unrolled_inductive_pred_const ext_ctxt gfp x
  4.1445 -                           |> aux ss Ts js depth polar
  4.1446 -              fun neg () = Const (pref ^ s, T)
  4.1447 -            in
  4.1448 -              (case polar |> gfp ? flip_polarity of
  4.1449 -                 Pos => pos ()
  4.1450 -               | Neg => neg ()
  4.1451 -               | Neut =>
  4.1452 -                 if is_fun_type T then
  4.1453 -                   let
  4.1454 -                     val ((trunk_arg_Ts, rump_arg_T), body_T) =
  4.1455 -                       T |> strip_type |>> split_last
  4.1456 -                     val set_T = rump_arg_T --> body_T
  4.1457 -                     (* (unit -> term) -> term *)
  4.1458 -                     fun app f =
  4.1459 -                       list_comb (f (),
  4.1460 -                                  map Bound (length trunk_arg_Ts - 1 downto 0))
  4.1461 -                   in
  4.1462 -                     List.foldr absdummy
  4.1463 -                                (Const (set_oper, set_T --> set_T --> set_T)
  4.1464 -                                        $ app pos $ app neg) trunk_arg_Ts
  4.1465 -                   end
  4.1466 -                 else
  4.1467 -                   connective $ pos () $ neg ())
  4.1468 -            end
  4.1469 -          else
  4.1470 -            Const x
  4.1471 -        | t1 $ t2 =>
  4.1472 -          betapply (aux ss Ts [] (skolem_depth + 1) polar t1,
  4.1473 -                    aux ss Ts [] depth Neut t2)
  4.1474 -        | Abs (s, T, t1) => Abs (s, T, aux ss Ts (incrs js) depth polar t1)
  4.1475 -        | _ => t
  4.1476 -      end
  4.1477 -  in aux [] [] [] 0 Pos end
  4.1478 -
  4.1479 -(* extended_context -> styp -> (int * term option) list *)
  4.1480 -fun static_args_in_term ({ersatz_table, ...} : extended_context) x t =
  4.1481 -  let
  4.1482 -    (* term -> term list -> term list -> term list list *)
  4.1483 -    fun fun_calls (Abs (_, _, t)) _ = fun_calls t []
  4.1484 -      | fun_calls (t1 $ t2) args = fun_calls t2 [] #> fun_calls t1 (t2 :: args)
  4.1485 -      | fun_calls t args =
  4.1486 -        (case t of
  4.1487 -           Const (x' as (s', T')) =>
  4.1488 -           x = x' orelse (case AList.lookup (op =) ersatz_table s' of
  4.1489 -                            SOME s'' => x = (s'', T')
  4.1490 -                          | NONE => false)
  4.1491 -         | _ => false) ? cons args
  4.1492 -    (* term list list -> term list list -> term list -> term list list *)
  4.1493 -    fun call_sets [] [] vs = [vs]
  4.1494 -      | call_sets [] uss vs = vs :: call_sets uss [] []
  4.1495 -      | call_sets ([] :: _) _ _ = []
  4.1496 -      | call_sets ((t :: ts) :: tss) uss vs =
  4.1497 -        OrdList.insert TermOrd.term_ord t vs |> call_sets tss (ts :: uss)
  4.1498 -    val sets = call_sets (fun_calls t [] []) [] []
  4.1499 -    val indexed_sets = sets ~~ (index_seq 0 (length sets))
  4.1500 -  in
  4.1501 -    fold_rev (fn (set, j) =>
  4.1502 -                 case set of
  4.1503 -                   [Var _] => AList.lookup (op =) indexed_sets set = SOME j
  4.1504 -                              ? cons (j, NONE)
  4.1505 -                 | [t as Const _] => cons (j, SOME t)
  4.1506 -                 | [t as Free _] => cons (j, SOME t)
  4.1507 -                 | _ => I) indexed_sets []
  4.1508 -  end
  4.1509 -(* extended_context -> styp -> term list -> (int * term option) list *)
  4.1510 -fun static_args_in_terms ext_ctxt x =
  4.1511 -  map (static_args_in_term ext_ctxt x)
  4.1512 -  #> fold1 (OrdList.inter (prod_ord int_ord (option_ord TermOrd.term_ord)))
  4.1513 -
  4.1514 -(* term -> term list *)
  4.1515 -fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2
  4.1516 -  | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
  4.1517 -  | params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) =
  4.1518 -    snd (strip_comb t1)
  4.1519 -  | params_in_equation _ = []
  4.1520 -
  4.1521 -(* styp -> styp -> int list -> term list -> term list -> term -> term *)
  4.1522 -fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t =
  4.1523 -  let
  4.1524 -    val k = fold Integer.max (map maxidx_of_term (fixed_args @ extra_args)) 0
  4.1525 -            + 1
  4.1526 -    val t = map_aterms (fn Var ((s, i), T) => Var ((s, k + i), T) | t' => t') t
  4.1527 -    val fixed_params = filter_indices fixed_js (params_in_equation t)
  4.1528 -    (* term list -> term -> term *)
  4.1529 -    fun aux args (Abs (s, T, t)) = list_comb (Abs (s, T, aux [] t), args)
  4.1530 -      | aux args (t1 $ t2) = aux (aux [] t2 :: args) t1
  4.1531 -      | aux args t =
  4.1532 -        if t = Const x then
  4.1533 -          list_comb (Const x', extra_args @ filter_out_indices fixed_js args)
  4.1534 -        else
  4.1535 -          let val j = find_index (curry (op =) t) fixed_params in
  4.1536 -            list_comb (if j >= 0 then nth fixed_args j else t, args)
  4.1537 -          end
  4.1538 -  in aux [] t end
  4.1539 -
  4.1540 -(* typ list -> term -> bool *)
  4.1541 -fun is_eligible_arg Ts t =
  4.1542 -  let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in
  4.1543 -    null bad_Ts orelse
  4.1544 -    (is_higher_order_type (fastype_of1 (Ts, t)) andalso
  4.1545 -     forall (not o is_higher_order_type) bad_Ts)
  4.1546 -  end
  4.1547 -
  4.1548 -(* (int * term option) list -> (int * term) list -> int list *)
  4.1549 -fun overlapping_indices [] _ = []
  4.1550 -  | overlapping_indices _ [] = []
  4.1551 -  | overlapping_indices (ps1 as (j1, t1) :: ps1') (ps2 as (j2, t2) :: ps2') =
  4.1552 -    if j1 < j2 then overlapping_indices ps1' ps2
  4.1553 -    else if j1 > j2 then overlapping_indices ps1 ps2'
  4.1554 -    else overlapping_indices ps1' ps2' |> the_default t2 t1 = t2 ? cons j1
  4.1555 -
  4.1556 -val special_depth = 20
  4.1557 -
  4.1558 -(* extended_context -> int -> term -> term *)
  4.1559 -fun specialize_consts_in_term (ext_ctxt as {thy, specialize, simp_table,
  4.1560 -                                            special_funs, ...}) depth t =
  4.1561 -  if not specialize orelse depth > special_depth then
  4.1562 -    t
  4.1563 -  else
  4.1564 -    let
  4.1565 -      val blacklist = if depth = 0 then []
  4.1566 -                      else case term_under_def t of Const x => [x] | _ => []
  4.1567 -      (* term list -> typ list -> term -> term *)
  4.1568 -      fun aux args Ts (Const (x as (s, T))) =
  4.1569 -          ((if not (member (op =) blacklist x) andalso not (null args) andalso
  4.1570 -               not (String.isPrefix special_prefix s) andalso
  4.1571 -               is_equational_fun ext_ctxt x then
  4.1572 -              let
  4.1573 -                val eligible_args = filter (is_eligible_arg Ts o snd)
  4.1574 -                                           (index_seq 0 (length args) ~~ args)
  4.1575 -                val _ = not (null eligible_args) orelse raise SAME ()
  4.1576 -                val old_axs = equational_fun_axioms ext_ctxt x
  4.1577 -                              |> map (destroy_existential_equalities thy)
  4.1578 -                val static_params = static_args_in_terms ext_ctxt x old_axs
  4.1579 -                val fixed_js = overlapping_indices static_params eligible_args
  4.1580 -                val _ = not (null fixed_js) orelse raise SAME ()
  4.1581 -                val fixed_args = filter_indices fixed_js args
  4.1582 -                val vars = fold Term.add_vars fixed_args []
  4.1583 -                           |> sort (TermOrd.fast_indexname_ord o pairself fst)
  4.1584 -                val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js))
  4.1585 -                                    fixed_args []
  4.1586 -                               |> sort int_ord
  4.1587 -                val live_args = filter_out_indices fixed_js args
  4.1588 -                val extra_args = map Var vars @ map Bound bound_js @ live_args
  4.1589 -                val extra_Ts = map snd vars @ filter_indices bound_js Ts
  4.1590 -                val k = maxidx_of_term t + 1
  4.1591 -                (* int -> term *)
  4.1592 -                fun var_for_bound_no j =
  4.1593 -                  Var ((bound_var_prefix ^
  4.1594 -                        nat_subscript (find_index (curry (op =) j) bound_js
  4.1595 -                                       + 1), k),
  4.1596 -                       nth Ts j)
  4.1597 -                val fixed_args_in_axiom =
  4.1598 -                  map (curry subst_bounds
  4.1599 -                             (map var_for_bound_no (index_seq 0 (length Ts))))
  4.1600 -                      fixed_args
  4.1601 -              in
  4.1602 -                case AList.lookup (op =) (!special_funs)
  4.1603 -                                  (x, fixed_js, fixed_args_in_axiom) of
  4.1604 -                  SOME x' => list_comb (Const x', extra_args)
  4.1605 -                | NONE =>
  4.1606 -                  let
  4.1607 -                    val extra_args_in_axiom =
  4.1608 -                      map Var vars @ map var_for_bound_no bound_js
  4.1609 -                    val x' as (s', _) =
  4.1610 -                      (special_prefix_for (length (!special_funs) + 1) ^ s,
  4.1611 -                       extra_Ts @ filter_out_indices fixed_js (binder_types T)
  4.1612 -                       ---> body_type T)
  4.1613 -                    val new_axs =
  4.1614 -                      map (specialize_fun_axiom x x' fixed_js
  4.1615 -                               fixed_args_in_axiom extra_args_in_axiom) old_axs
  4.1616 -                    val _ =
  4.1617 -                      Unsynchronized.change special_funs
  4.1618 -                          (cons ((x, fixed_js, fixed_args_in_axiom), x'))
  4.1619 -                    val _ = add_simps simp_table s' new_axs
  4.1620 -                  in list_comb (Const x', extra_args) end
  4.1621 -              end
  4.1622 -            else
  4.1623 -              raise SAME ())
  4.1624 -           handle SAME () => list_comb (Const x, args))
  4.1625 -        | aux args Ts (Abs (s, T, t)) =
  4.1626 -          list_comb (Abs (s, T, aux [] (T :: Ts) t), args)
  4.1627 -        | aux args Ts (t1 $ t2) = aux (aux [] Ts t2 :: args) Ts t1
  4.1628 -        | aux args _ t = list_comb (t, args)
  4.1629 -    in aux [] [] t end
  4.1630 -
  4.1631 -(* theory -> term -> int Termtab.tab -> int Termtab.tab *)
  4.1632 -fun add_to_uncurry_table thy t =
  4.1633 -  let
  4.1634 -    (* term -> term list -> int Termtab.tab -> int Termtab.tab *)
  4.1635 -    fun aux (t1 $ t2) args table =
  4.1636 -        let val table = aux t2 [] table in aux t1 (t2 :: args) table end
  4.1637 -      | aux (Abs (_, _, t')) _ table = aux t' [] table
  4.1638 -      | aux (t as Const (x as (s, _))) args table =
  4.1639 -        if is_built_in_const true x orelse is_constr_like thy x orelse
  4.1640 -           is_sel s orelse s = @{const_name Sigma} then
  4.1641 -          table
  4.1642 -        else
  4.1643 -          Termtab.map_default (t, 65536) (curry Int.min (length args)) table
  4.1644 -      | aux _ _ table = table
  4.1645 -  in aux t [] end
  4.1646 -
  4.1647 -(* int Termtab.tab term -> term *)
  4.1648 -fun uncurry_term table t =
  4.1649 -  let
  4.1650 -    (* term -> term list -> term *)
  4.1651 -    fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args)
  4.1652 -      | aux (Abs (s, T, t')) args = betapplys (Abs (s, T, aux t' []), args)
  4.1653 -      | aux (t as Const (s, T)) args =
  4.1654 -        (case Termtab.lookup table t of
  4.1655 -           SOME n =>
  4.1656 -           if n >= 2 then
  4.1657 -             let
  4.1658 -               val (arg_Ts, rest_T) = strip_n_binders n T
  4.1659 -               val j =
  4.1660 -                 if hd arg_Ts = @{typ bisim_iterator} orelse
  4.1661 -                    is_fp_iterator_type (hd arg_Ts) then
  4.1662 -                   1
  4.1663 -                 else case find_index (not_equal bool_T) arg_Ts of
  4.1664 -                   ~1 => n
  4.1665 -                 | j => j
  4.1666 -               val ((before_args, tuple_args), after_args) =
  4.1667 -                 args |> chop n |>> chop j
  4.1668 -               val ((before_arg_Ts, tuple_arg_Ts), rest_T) =
  4.1669 -                 T |> strip_n_binders n |>> chop j
  4.1670 -               val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
  4.1671 -             in
  4.1672 -               if n - j < 2 then
  4.1673 -                 betapplys (t, args)
  4.1674 -               else
  4.1675 -                 betapplys (Const (uncurry_prefix_for (n - j) j ^ s,
  4.1676 -                                   before_arg_Ts ---> tuple_T --> rest_T),
  4.1677 -                            before_args @ [mk_flat_tuple tuple_T tuple_args] @
  4.1678 -                            after_args)
  4.1679 -             end
  4.1680 -           else
  4.1681 -             betapplys (t, args)
  4.1682 -         | NONE => betapplys (t, args))
  4.1683 -      | aux t args = betapplys (t, args)
  4.1684 -  in aux t [] end
  4.1685 -
  4.1686 -(* (term -> term) -> int -> term -> term *)
  4.1687 -fun coerce_bound_no f j t =
  4.1688 -  case t of
  4.1689 -    t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
  4.1690 -  | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
  4.1691 -  | Bound j' => if j' = j then f t else t
  4.1692 -  | _ => t
  4.1693 -
  4.1694 -(* extended_context -> bool -> term -> term *)
  4.1695 -fun box_fun_and_pair_in_term (ext_ctxt as {thy, fast_descrs, ...}) def orig_t =
  4.1696 -  let
  4.1697 -    (* typ -> typ *)
  4.1698 -    fun box_relational_operator_type (Type ("fun", Ts)) =
  4.1699 -        Type ("fun", map box_relational_operator_type Ts)
  4.1700 -      | box_relational_operator_type (Type ("*", Ts)) =
  4.1701 -        Type ("*", map (box_type ext_ctxt InPair) Ts)
  4.1702 -      | box_relational_operator_type T = T
  4.1703 -    (* typ -> typ -> term -> term *)
  4.1704 -    fun coerce_bound_0_in_term new_T old_T =
  4.1705 -      old_T <> new_T ? coerce_bound_no (coerce_term [new_T] old_T new_T) 0
  4.1706 -    (* typ list -> typ -> term -> term *)
  4.1707 -    and coerce_term Ts new_T old_T t =
  4.1708 -      if old_T = new_T then
  4.1709 -        t
  4.1710 -      else
  4.1711 -        case (new_T, old_T) of
  4.1712 -          (Type (new_s, new_Ts as [new_T1, new_T2]),
  4.1713 -           Type ("fun", [old_T1, old_T2])) =>
  4.1714 -          (case eta_expand Ts t 1 of
  4.1715 -             Abs (s, _, t') =>
  4.1716 -             Abs (s, new_T1,
  4.1717 -                  t' |> coerce_bound_0_in_term new_T1 old_T1
  4.1718 -                     |> coerce_term (new_T1 :: Ts) new_T2 old_T2)
  4.1719 -             |> Envir.eta_contract
  4.1720 -             |> new_s <> "fun"
  4.1721 -                ? construct_value thy (@{const_name FunBox},
  4.1722 -                                       Type ("fun", new_Ts) --> new_T) o single
  4.1723 -           | t' => raise TERM ("Nitpick_HOL.box_fun_and_pair_in_term.\
  4.1724 -                               \coerce_term", [t']))
  4.1725 -        | (Type (new_s, new_Ts as [new_T1, new_T2]),
  4.1726 -           Type (old_s, old_Ts as [old_T1, old_T2])) =>
  4.1727 -          if old_s = @{type_name fun_box} orelse
  4.1728 -             old_s = @{type_name pair_box} orelse old_s = "*" then
  4.1729 -            case constr_expand ext_ctxt old_T t of
  4.1730 -              Const (@{const_name FunBox}, _) $ t1 =>
  4.1731 -              if new_s = "fun" then
  4.1732 -                coerce_term Ts new_T (Type ("fun", old_Ts)) t1
  4.1733 -              else
  4.1734 -                construct_value thy
  4.1735 -                    (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
  4.1736 -                     [coerce_term Ts (Type ("fun", new_Ts))
  4.1737 -                                  (Type ("fun", old_Ts)) t1]
  4.1738 -            | Const _ $ t1 $ t2 =>
  4.1739 -              construct_value thy
  4.1740 -                  (if new_s = "*" then @{const_name Pair}
  4.1741 -                   else @{const_name PairBox}, new_Ts ---> new_T)
  4.1742 -                  [coerce_term Ts new_T1 old_T1 t1,
  4.1743 -                   coerce_term Ts new_T2 old_T2 t2]
  4.1744 -            | t' => raise TERM ("Nitpick_HOL.box_fun_and_pair_in_term.\
  4.1745 -                                \coerce_term", [t'])
  4.1746 -          else
  4.1747 -            raise TYPE ("coerce_term", [new_T, old_T], [t])
  4.1748 -        | _ => raise TYPE ("coerce_term", [new_T, old_T], [t])
  4.1749 -    (* indexname * typ -> typ * term -> typ option list -> typ option list *)
  4.1750 -    fun add_boxed_types_for_var (z as (_, T)) (T', t') =
  4.1751 -      case t' of
  4.1752 -        Var z' => z' = z ? insert (op =) T'
  4.1753 -      | Const (@{const_name Pair}, _) $ t1 $ t2 =>
  4.1754 -        (case T' of
  4.1755 -           Type (_, [T1, T2]) =>
  4.1756 -           fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)]
  4.1757 -         | _ => raise TYPE ("Nitpick_HOL.box_fun_and_pair_in_term.\
  4.1758 -                            \add_boxed_types_for_var", [T'], []))
  4.1759 -      | _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T
  4.1760 -    (* typ list -> typ list -> term -> indexname * typ -> typ *)
  4.1761 -    fun box_var_in_def new_Ts old_Ts t (z as (_, T)) =
  4.1762 -      case t of
  4.1763 -        @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
  4.1764 -      | Const (s0, _) $ t1 $ _ =>
  4.1765 -        if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then
  4.1766 -          let
  4.1767 -            val (t', args) = strip_comb t1
  4.1768 -            val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
  4.1769 -          in
  4.1770 -            case fold (add_boxed_types_for_var z)
  4.1771 -                      (fst (strip_n_binders (length args) T') ~~ args) [] of
  4.1772 -              [T''] => T''
  4.1773 -            | _ => T
  4.1774 -          end
  4.1775 -        else
  4.1776 -          T
  4.1777 -      | _ => T
  4.1778 -    (* typ list -> typ list -> polarity -> string -> typ -> string -> typ
  4.1779 -       -> term -> term *)
  4.1780 -    and do_quantifier new_Ts old_Ts polar quant_s quant_T abs_s abs_T t =
  4.1781 -      let
  4.1782 -        val abs_T' =
  4.1783 -          if polar = Neut orelse is_positive_existential polar quant_s then
  4.1784 -            box_type ext_ctxt InFunLHS abs_T
  4.1785 -          else
  4.1786 -            abs_T
  4.1787 -        val body_T = body_type quant_T
  4.1788 -      in
  4.1789 -        Const (quant_s, (abs_T' --> body_T) --> body_T)
  4.1790 -        $ Abs (abs_s, abs_T',
  4.1791 -               t |> do_term (abs_T' :: new_Ts) (abs_T :: old_Ts) polar)
  4.1792 -      end
  4.1793 -    (* typ list -> typ list -> string -> typ -> term -> term -> term *)
  4.1794 -    and do_equals new_Ts old_Ts s0 T0 t1 t2 =
  4.1795 -      let
  4.1796 -        val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2)
  4.1797 -        val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
  4.1798 -        val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last
  4.1799 -      in
  4.1800 -        list_comb (Const (s0, T --> T --> body_type T0),
  4.1801 -                   map2 (coerce_term new_Ts T) [T1, T2] [t1, t2])
  4.1802 -      end
  4.1803 -    (* string -> typ -> term *)
  4.1804 -    and do_description_operator s T =
  4.1805 -      let val T1 = box_type ext_ctxt InFunLHS (range_type T) in
  4.1806 -        Const (s, (T1 --> bool_T) --> T1)
  4.1807 -      end
  4.1808 -    (* typ list -> typ list -> polarity -> term -> term *)
  4.1809 -    and do_term new_Ts old_Ts polar t =
  4.1810 -      case t of
  4.1811 -        Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
  4.1812 -        do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
  4.1813 -      | Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 =>
  4.1814 -        do_equals new_Ts old_Ts s0 T0 t1 t2
  4.1815 -      | @{const "==>"} $ t1 $ t2 =>
  4.1816 -        @{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
  4.1817 -        $ do_term new_Ts old_Ts polar t2
  4.1818 -      | @{const Pure.conjunction} $ t1 $ t2 =>
  4.1819 -        @{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1
  4.1820 -        $ do_term new_Ts old_Ts polar t2
  4.1821 -      | @{const Trueprop} $ t1 =>
  4.1822 -        @{const Trueprop} $ do_term new_Ts old_Ts polar t1
  4.1823 -      | @{const Not} $ t1 =>
  4.1824 -        @{const Not} $ do_term new_Ts old_Ts (flip_polarity polar) t1
  4.1825 -      | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
  4.1826 -        do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
  4.1827 -      | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
  4.1828 -        do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
  4.1829 -      | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>
  4.1830 -        do_equals new_Ts old_Ts s0 T0 t1 t2
  4.1831 -      | @{const "op &"} $ t1 $ t2 =>
  4.1832 -        @{const "op &"} $ do_term new_Ts old_Ts polar t1
  4.1833 -        $ do_term new_Ts old_Ts polar t2
  4.1834 -      | @{const "op |"} $ t1 $ t2 =>
  4.1835 -        @{const "op |"} $ do_term new_Ts old_Ts polar t1
  4.1836 -        $ do_term new_Ts old_Ts polar t2
  4.1837 -      | @{const "op -->"} $ t1 $ t2 =>
  4.1838 -        @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
  4.1839 -        $ do_term new_Ts old_Ts polar t2
  4.1840 -      | Const (s as @{const_name The}, T) => do_description_operator s T
  4.1841 -      | Const (s as @{const_name Eps}, T) => do_description_operator s T
  4.1842 -      | Const (@{const_name quot_normal}, Type ("fun", [_, T2])) =>
  4.1843 -        let val T' = box_type ext_ctxt InSel T2 in
  4.1844 -          Const (@{const_name quot_normal}, T' --> T')
  4.1845 -        end
  4.1846 -      | Const (s as @{const_name Tha}, T) => do_description_operator s T
  4.1847 -      | Const (x as (s, T)) =>
  4.1848 -        Const (s, if s = @{const_name converse} orelse
  4.1849 -                     s = @{const_name trancl} then
  4.1850 -                    box_relational_operator_type T
  4.1851 -                  else if is_built_in_const fast_descrs x orelse
  4.1852 -                          s = @{const_name Sigma} then
  4.1853 -                    T
  4.1854 -                  else if is_constr_like thy x then
  4.1855 -                    box_type ext_ctxt InConstr T
  4.1856 -                  else if is_sel s
  4.1857 -                       orelse is_rep_fun thy x then
  4.1858 -                    box_type ext_ctxt InSel T
  4.1859 -                  else
  4.1860 -                    box_type ext_ctxt InExpr T)
  4.1861 -      | t1 $ Abs (s, T, t2') =>
  4.1862 -        let
  4.1863 -          val t1 = do_term new_Ts old_Ts Neut t1
  4.1864 -          val T1 = fastype_of1 (new_Ts, t1)
  4.1865 -          val (s1, Ts1) = dest_Type T1
  4.1866 -          val T' = hd (snd (dest_Type (hd Ts1)))
  4.1867 -          val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2')
  4.1868 -          val T2 = fastype_of1 (new_Ts, t2)
  4.1869 -          val t2 = coerce_term new_Ts (hd Ts1) T2 t2
  4.1870 -        in
  4.1871 -          betapply (if s1 = "fun" then
  4.1872 -                      t1
  4.1873 -                    else
  4.1874 -                      select_nth_constr_arg thy
  4.1875 -                          (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
  4.1876 -                          (Type ("fun", Ts1)), t2)
  4.1877 -        end
  4.1878 -      | t1 $ t2 =>
  4.1879 -        let
  4.1880 -          val t1 = do_term new_Ts old_Ts Neut t1
  4.1881 -          val T1 = fastype_of1 (new_Ts, t1)
  4.1882 -          val (s1, Ts1) = dest_Type T1
  4.1883 -          val t2 = do_term new_Ts old_Ts Neut t2
  4.1884 -          val T2 = fastype_of1 (new_Ts, t2)
  4.1885 -          val t2 = coerce_term new_Ts (hd Ts1) T2 t2
  4.1886 -        in
  4.1887 -          betapply (if s1 = "fun" then
  4.1888 -                      t1
  4.1889 -                    else
  4.1890 -                      select_nth_constr_arg thy
  4.1891 -                          (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
  4.1892 -                          (Type ("fun", Ts1)), t2)
  4.1893 -        end
  4.1894 -      | Free (s, T) => Free (s, box_type ext_ctxt InExpr T)
  4.1895 -      | Var (z as (x, T)) =>
  4.1896 -        Var (x, if def then box_var_in_def new_Ts old_Ts orig_t z
  4.1897 -                else box_type ext_ctxt InExpr T)
  4.1898 -      | Bound _ => t
  4.1899 -      | Abs (s, T, t') =>
  4.1900 -        Abs (s, T, do_term (T :: new_Ts) (T :: old_Ts) Neut t')
  4.1901 -  in do_term [] [] Pos orig_t end
  4.1902 -
  4.1903 -(* int -> term -> term *)
  4.1904 -fun eval_axiom_for_term j t =
  4.1905 -  Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t)
  4.1906 -
  4.1907 -(* extended_context -> styp -> bool *)
  4.1908 -fun is_equational_fun_surely_complete ext_ctxt x =
  4.1909 -  case raw_equational_fun_axioms ext_ctxt x of
  4.1910 -    [@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)] =>
  4.1911 -    strip_comb t1 |> snd |> forall is_Var
  4.1912 -  | _ => false
  4.1913 -
  4.1914 -type special = int list * term list * styp
  4.1915 -
  4.1916 -(* styp -> special -> special -> term *)
  4.1917 -fun special_congruence_axiom (s, T) (js1, ts1, x1) (js2, ts2, x2) =
  4.1918 -  let
  4.1919 -    val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2)
  4.1920 -    val Ts = binder_types T
  4.1921 -    val max_j = fold (fold Integer.max) [js1, js2] ~1
  4.1922 -    val (eqs, (args1, args2)) =
  4.1923 -      fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j)
  4.1924 -                                  (js1 ~~ ts1, js2 ~~ ts2) of
  4.1925 -                      (SOME t1, SOME t2) => apfst (cons (t1, t2))
  4.1926 -                    | (SOME t1, NONE) => apsnd (apsnd (cons t1))
  4.1927 -                    | (NONE, SOME t2) => apsnd (apfst (cons t2))
  4.1928 -                    | (NONE, NONE) =>
  4.1929 -                      let val v = Var ((cong_var_prefix ^ nat_subscript j, 0),
  4.1930 -                                       nth Ts j) in
  4.1931 -                        apsnd (pairself (cons v))
  4.1932 -                      end) (max_j downto 0) ([], ([], []))
  4.1933 -  in
  4.1934 -    Logic.list_implies (eqs |> filter_out (op =) |> distinct (op =)
  4.1935 -                            |> map Logic.mk_equals,
  4.1936 -                        Logic.mk_equals (list_comb (Const x1, bounds1 @ args1),
  4.1937 -                                         list_comb (Const x2, bounds2 @ args2)))
  4.1938 -    |> Refute.close_form (* TODO: needed? *)
  4.1939 -  end
  4.1940 -
  4.1941 -(* extended_context -> styp list -> term list *)
  4.1942 -fun special_congruence_axioms (ext_ctxt as {special_funs, ...}) xs =
  4.1943 -  let
  4.1944 -    val groups =
  4.1945 -      !special_funs
  4.1946 -      |> map (fn ((x, js, ts), x') => (x, (js, ts, x')))
  4.1947 -      |> AList.group (op =)
  4.1948 -      |> filter_out (is_equational_fun_surely_complete ext_ctxt o fst)
  4.1949 -      |> map (fn (x, zs) => (x, zs |> member (op =) xs x ? cons ([], [], x)))
  4.1950 -    (* special -> int *)
  4.1951 -    fun generality (js, _, _) = ~(length js)
  4.1952 -    (* special -> special -> bool *)
  4.1953 -    fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
  4.1954 -      x1 <> x2 andalso OrdList.subset (prod_ord int_ord TermOrd.term_ord)
  4.1955 -                                      (j2 ~~ t2, j1 ~~ t1)
  4.1956 -    (* styp -> special list -> special list -> special list -> term list
  4.1957 -       -> term list *)
  4.1958 -    fun do_pass_1 _ [] [_] [_] = I
  4.1959 -      | do_pass_1 x skipped _ [] = do_pass_2 x skipped
  4.1960 -      | do_pass_1 x skipped all (z :: zs) =
  4.1961 -        case filter (is_more_specific z) all
  4.1962 -             |> sort (int_ord o pairself generality) of
  4.1963 -          [] => do_pass_1 x (z :: skipped) all zs
  4.1964 -        | (z' :: _) => cons (special_congruence_axiom x z z')
  4.1965 -                       #> do_pass_1 x skipped all zs
  4.1966 -    (* styp -> special list -> term list -> term list *)
  4.1967 -    and do_pass_2 _ [] = I
  4.1968 -      | do_pass_2 x (z :: zs) =
  4.1969 -        fold (cons o special_congruence_axiom x z) zs #> do_pass_2 x zs
  4.1970 -  in fold (fn (x, zs) => do_pass_1 x [] zs zs) groups [] end
  4.1971 -
  4.1972 -(* term -> bool *)
  4.1973 -val is_trivial_equation = the_default false o try (op aconv o Logic.dest_equals)
  4.1974 -
  4.1975 -(* 'a Symtab.table -> 'a list *)
  4.1976 -fun all_table_entries table = Symtab.fold (append o snd) table []
  4.1977 -(* const_table -> string -> const_table *)
  4.1978 -fun extra_table table s = Symtab.make [(s, all_table_entries table)]
  4.1979 -
  4.1980 -(* extended_context -> term -> (term list * term list) * (bool * bool) *)
  4.1981 -fun axioms_for_term
  4.1982 -        (ext_ctxt as {thy, max_bisim_depth, user_axioms, fast_descrs, evals,
  4.1983 -                      def_table, nondef_table, user_nondefs, ...}) t =
  4.1984 -  let
  4.1985 -    type accumulator = styp list * (term list * term list)
  4.1986 -    (* (term list * term list -> term list)
  4.1987 -       -> ((term list -> term list) -> term list * term list
  4.1988 -           -> term list * term list)
  4.1989 -       -> int -> term -> accumulator -> accumulator *)
  4.1990 -    fun add_axiom get app depth t (accum as (xs, axs)) =
  4.1991 -      let
  4.1992 -        val t = t |> unfold_defs_in_term ext_ctxt
  4.1993 -                  |> skolemize_term_and_more ext_ctxt ~1
  4.1994 -      in
  4.1995 -        if is_trivial_equation t then
  4.1996 -          accum
  4.1997 -        else
  4.1998 -          let val t' = t |> specialize_consts_in_term ext_ctxt depth in
  4.1999 -            if exists (member (op aconv) (get axs)) [t, t'] then accum
  4.2000 -            else add_axioms_for_term (depth + 1) t' (xs, app (cons t') axs)
  4.2001 -          end
  4.2002 -      end
  4.2003 -    (* int -> term -> accumulator -> accumulator *)
  4.2004 -    and add_def_axiom depth = add_axiom fst apfst depth
  4.2005 -    and add_nondef_axiom depth = add_axiom snd apsnd depth
  4.2006 -    and add_maybe_def_axiom depth t =
  4.2007 -      (if head_of t <> @{const "==>"} then add_def_axiom
  4.2008 -       else add_nondef_axiom) depth t
  4.2009 -    and add_eq_axiom depth t =
  4.2010 -      (if is_constr_pattern_formula thy t then add_def_axiom
  4.2011 -       else add_nondef_axiom) depth t
  4.2012 -    (* int -> term -> accumulator -> accumulator *)
  4.2013 -    and add_axioms_for_term depth t (accum as (xs, axs)) =
  4.2014 -      case t of
  4.2015 -        t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
  4.2016 -      | Const (x as (s, T)) =>
  4.2017 -        (if member (op =) xs x orelse is_built_in_const fast_descrs x then
  4.2018 -           accum
  4.2019 -         else
  4.2020 -           let val accum as (xs, _) = (x :: xs, axs) in
  4.2021 -             if depth > axioms_max_depth then
  4.2022 -               raise TOO_LARGE ("Nitpick_HOL.axioms_for_term.\
  4.2023 -                                \add_axioms_for_term",
  4.2024 -                                "too many nested axioms (" ^
  4.2025 -                                string_of_int depth ^ ")")
  4.2026 -             else if Refute.is_const_of_class thy x then
  4.2027 -               let
  4.2028 -                 val class = Logic.class_of_const s
  4.2029 -                 val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]),
  4.2030 -                                                   class)
  4.2031 -                 val ax1 = try (Refute.specialize_type thy x) of_class
  4.2032 -                 val ax2 = Option.map (Refute.specialize_type thy x o snd)
  4.2033 -                                      (Refute.get_classdef thy class)
  4.2034 -               in
  4.2035 -                 fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
  4.2036 -                      accum
  4.2037 -               end
  4.2038 -             else if is_constr thy x then
  4.2039 -               accum
  4.2040 -             else if is_equational_fun ext_ctxt x then
  4.2041 -               fold (add_eq_axiom depth) (equational_fun_axioms ext_ctxt x)
  4.2042 -                    accum
  4.2043 -             else if is_abs_fun thy x then
  4.2044 -               if is_quot_type thy (range_type T) then
  4.2045 -                 raise NOT_SUPPORTED "\"Abs_\" function of quotient type"
  4.2046 -               else
  4.2047 -                 accum |> fold (add_nondef_axiom depth)
  4.2048 -                               (nondef_props_for_const thy false nondef_table x)
  4.2049 -                       |> is_funky_typedef thy (range_type T)
  4.2050 -                          ? fold (add_maybe_def_axiom depth)
  4.2051 -                                 (nondef_props_for_const thy true
  4.2052 -                                                    (extra_table def_table s) x)
  4.2053 -             else if is_rep_fun thy x then
  4.2054 -               if is_quot_type thy (domain_type T) then
  4.2055 -                 raise NOT_SUPPORTED "\"Rep_\" function of quotient type"
  4.2056 -               else
  4.2057 -                 accum |> fold (add_nondef_axiom depth)
  4.2058 -                               (nondef_props_for_const thy false nondef_table x)
  4.2059 -                       |> is_funky_typedef thy (range_type T)
  4.2060 -                          ? fold (add_maybe_def_axiom depth)
  4.2061 -                                 (nondef_props_for_const thy true
  4.2062 -                                                    (extra_table def_table s) x)
  4.2063 -                       |> add_axioms_for_term depth
  4.2064 -                                              (Const (mate_of_rep_fun thy x))
  4.2065 -                       |> fold (add_def_axiom depth)
  4.2066 -                               (inverse_axioms_for_rep_fun thy x)
  4.2067 -             else
  4.2068 -               accum |> user_axioms <> SOME false
  4.2069 -                        ? fold (add_nondef_axiom depth)
  4.2070 -                               (nondef_props_for_const thy false nondef_table x)
  4.2071 -           end)
  4.2072 -        |> add_axioms_for_type depth T
  4.2073 -      | Free (_, T) => add_axioms_for_type depth T accum
  4.2074 -      | Var (_, T) => add_axioms_for_type depth T accum
  4.2075 -      | Bound _ => accum
  4.2076 -      | Abs (_, T, t) => accum |> add_axioms_for_term depth t
  4.2077 -                               |> add_axioms_for_type depth T
  4.2078 -    (* int -> typ -> accumulator -> accumulator *)
  4.2079 -    and add_axioms_for_type depth T =
  4.2080 -      case T of
  4.2081 -        Type ("fun", Ts) => fold (add_axioms_for_type depth) Ts
  4.2082 -      | Type ("*", Ts) => fold (add_axioms_for_type depth) Ts
  4.2083 -      | @{typ prop} => I
  4.2084 -      | @{typ bool} => I
  4.2085 -      | @{typ unit} => I
  4.2086 -      | TFree (_, S) => add_axioms_for_sort depth T S
  4.2087 -      | TVar (_, S) => add_axioms_for_sort depth T S
  4.2088 -      | Type (z as (s, Ts)) =>
  4.2089 -        fold (add_axioms_for_type depth) Ts
  4.2090 -        #> (if is_pure_typedef thy T then
  4.2091 -              fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
  4.2092 -            else if is_quot_type thy T then
  4.2093 -              fold (add_def_axiom depth) (optimized_quot_type_axioms thy z)
  4.2094 -            else if max_bisim_depth >= 0 andalso is_codatatype thy T then
  4.2095 -              fold (add_maybe_def_axiom depth)
  4.2096 -                   (codatatype_bisim_axioms ext_ctxt T)
  4.2097 -            else
  4.2098 -              I)
  4.2099 -    (* int -> typ -> sort -> accumulator -> accumulator *)
  4.2100 -    and add_axioms_for_sort depth T S =
  4.2101 -      let
  4.2102 -        val supers = Sign.complete_sort thy S
  4.2103 -        val class_axioms =
  4.2104 -          maps (fn class => map prop_of (AxClass.get_info thy class |> #axioms
  4.2105 -                                         handle ERROR _ => [])) supers
  4.2106 -        val monomorphic_class_axioms =
  4.2107 -          map (fn t => case Term.add_tvars t [] of
  4.2108 -                         [] => t
  4.2109 -                       | [(x, S)] =>
  4.2110 -                         Refute.monomorphic_term (Vartab.make [(x, (S, T))]) t
  4.2111 -                       | _ => raise TERM ("Nitpick_HOL.axioms_for_term.\
  4.2112 -                                          \add_axioms_for_sort", [t]))
  4.2113 -              class_axioms
  4.2114 -      in fold (add_nondef_axiom depth) monomorphic_class_axioms end
  4.2115 -    val (mono_user_nondefs, poly_user_nondefs) =
  4.2116 -      List.partition (null o Term.hidden_polymorphism) user_nondefs
  4.2117 -    val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals))
  4.2118 -                           evals
  4.2119 -    val (xs, (defs, nondefs)) =
  4.2120 -      ([], ([], [])) |> add_axioms_for_term 1 t 
  4.2121 -                     |> fold_rev (add_def_axiom 1) eval_axioms
  4.2122 -                     |> user_axioms = SOME true
  4.2123 -                        ? fold (add_nondef_axiom 1) mono_user_nondefs
  4.2124 -    val defs = defs @ special_congruence_axioms ext_ctxt xs
  4.2125 -  in
  4.2126 -    ((defs, nondefs), (user_axioms = SOME true orelse null mono_user_nondefs,
  4.2127 -                       null poly_user_nondefs))
  4.2128 -  end
  4.2129 +(* hol_context -> typ -> typ list *)
  4.2130 +fun ground_types_in_type hol_ctxt T = add_ground_types hol_ctxt T []
  4.2131 +(* hol_context -> term list -> typ list *)
  4.2132 +fun ground_types_in_terms hol_ctxt ts =
  4.2133 +  fold (fold_types (add_ground_types hol_ctxt)) ts []
  4.2134  
  4.2135  (* theory -> const_table -> styp -> int list *)
  4.2136  fun const_format thy def_table (x as (s, T)) =
  4.2137 @@ -3356,10 +2096,10 @@
  4.2138                   |> map (rev o filter_out (member (op =) js))
  4.2139                   |> filter_out null |> map length |> rev
  4.2140  
  4.2141 -(* extended_context -> string * string -> (term option * int list) list
  4.2142 +(* hol_context -> string * string -> (term option * int list) list
  4.2143     -> styp -> term * typ *)
  4.2144  fun user_friendly_const ({thy, evals, def_table, skolems, special_funs, ...}
  4.2145 -                         : extended_context) (base_name, step_name) formats =
  4.2146 +                         : hol_context) (base_name, step_name) formats =
  4.2147    let
  4.2148      val default_format = the (AList.lookup (op =) formats NONE)
  4.2149      (* styp -> term * typ *)
  4.2150 @@ -3460,7 +2200,7 @@
  4.2151             (t, format_term_type thy def_table formats t)
  4.2152           end)
  4.2153        |>> map_types unbit_and_unbox_type
  4.2154 -      |>> shorten_names_in_term |>> shorten_abs_vars
  4.2155 +      |>> shorten_names_in_term |>> Term.map_abs_vars shortest_name
  4.2156    in do_const end
  4.2157  
  4.2158  (* styp -> string *)
  4.2159 @@ -3474,84 +2214,4 @@
  4.2160    else
  4.2161      "="
  4.2162  
  4.2163 -val binary_int_threshold = 4
  4.2164 -
  4.2165 -(* term -> bool *)
  4.2166 -fun may_use_binary_ints (t1 $ t2) =
  4.2167 -    may_use_binary_ints t1 andalso may_use_binary_ints t2
  4.2168 -  | may_use_binary_ints (t as Const (s, _)) =
  4.2169 -    t <> @{const Suc} andalso
  4.2170 -    not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac},
  4.2171 -                        @{const_name nat_gcd}, @{const_name nat_lcm},
  4.2172 -                        @{const_name Frac}, @{const_name norm_frac}] s)
  4.2173 -  | may_use_binary_ints (Abs (_, _, t')) = may_use_binary_ints t'
  4.2174 -  | may_use_binary_ints _ = true
  4.2175 -fun should_use_binary_ints (t1 $ t2) =
  4.2176 -    should_use_binary_ints t1 orelse should_use_binary_ints t2
  4.2177 -  | should_use_binary_ints (Const (s, _)) =
  4.2178 -    member (op =) [@{const_name times_nat_inst.times_nat},
  4.2179 -                   @{const_name div_nat_inst.div_nat},
  4.2180 -                   @{const_name times_int_inst.times_int},
  4.2181 -                   @{const_name div_int_inst.div_int}] s orelse
  4.2182 -    (String.isPrefix numeral_prefix s andalso
  4.2183 -     let val n = the (Int.fromString (unprefix numeral_prefix s)) in
  4.2184 -       n <= ~ binary_int_threshold orelse n >= binary_int_threshold
  4.2185 -     end)
  4.2186 -  | should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t'
  4.2187 -  | should_use_binary_ints _ = false
  4.2188 -
  4.2189 -(* typ -> typ *)
  4.2190 -fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}
  4.2191 -  | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}
  4.2192 -  | binarize_nat_and_int_in_type (Type (s, Ts)) =
  4.2193 -    Type (s, map binarize_nat_and_int_in_type Ts)
  4.2194 -  | binarize_nat_and_int_in_type T = T
  4.2195 -(* term -> term *)
  4.2196 -val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type
  4.2197 -
  4.2198 -(* extended_context -> term
  4.2199 -   -> ((term list * term list) * (bool * bool)) * term *)
  4.2200 -fun preprocess_term (ext_ctxt as {thy, binary_ints, destroy_constrs, boxes,
  4.2201 -                                  skolemize, uncurry, ...}) t =
  4.2202 -  let
  4.2203 -    val skolem_depth = if skolemize then 4 else ~1
  4.2204 -    val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
  4.2205 -         core_t) = t |> unfold_defs_in_term ext_ctxt
  4.2206 -                     |> Refute.close_form
  4.2207 -                     |> skolemize_term_and_more ext_ctxt skolem_depth
  4.2208 -                     |> specialize_consts_in_term ext_ctxt 0
  4.2209 -                     |> `(axioms_for_term ext_ctxt)
  4.2210 -    val binarize =
  4.2211 -      case binary_ints of
  4.2212 -        SOME false => false
  4.2213 -      | _ =>
  4.2214 -        forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
  4.2215 -        (binary_ints = SOME true orelse
  4.2216 -         exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
  4.2217 -    val box = exists (not_equal (SOME false) o snd) boxes
  4.2218 -    val table =
  4.2219 -      Termtab.empty |> uncurry
  4.2220 -        ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts)
  4.2221 -    (* bool -> bool -> term -> term *)
  4.2222 -    fun do_rest def core =
  4.2223 -      binarize ? binarize_nat_and_int_in_term
  4.2224 -      #> uncurry ? uncurry_term table
  4.2225 -      #> box ? box_fun_and_pair_in_term ext_ctxt def
  4.2226 -      #> destroy_constrs ? (pull_out_universal_constrs thy def
  4.2227 -                            #> pull_out_existential_constrs thy
  4.2228 -                            #> destroy_pulled_out_constrs ext_ctxt def)
  4.2229 -      #> curry_assms
  4.2230 -      #> destroy_universal_equalities
  4.2231 -      #> destroy_existential_equalities thy
  4.2232 -      #> simplify_constrs_and_sels thy
  4.2233 -      #> distribute_quantifiers
  4.2234 -      #> push_quantifiers_inward thy
  4.2235 -      #> not core ? Refute.close_form
  4.2236 -      #> shorten_abs_vars
  4.2237 -  in
  4.2238 -    (((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts),
  4.2239 -      (got_all_mono_user_axioms, no_poly_user_axioms)),
  4.2240 -     do_rest false true core_t)
  4.2241 -  end
  4.2242 -
  4.2243  end;
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Feb 04 13:36:52 2010 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Feb 04 16:03:15 2010 +0100
     5.3 @@ -7,7 +7,7 @@
     5.4  
     5.5  signature NITPICK_KODKOD =
     5.6  sig
     5.7 -  type extended_context = Nitpick_HOL.extended_context
     5.8 +  type hol_context = Nitpick_HOL.hol_context
     5.9    type dtype_spec = Nitpick_Scope.dtype_spec
    5.10    type kodkod_constrs = Nitpick_Peephole.kodkod_constrs
    5.11    type nut = Nitpick_Nut.nut
    5.12 @@ -33,7 +33,7 @@
    5.13    val merge_bounds : Kodkod.bound list -> Kodkod.bound list
    5.14    val declarative_axiom_for_plain_rel : kodkod_constrs -> nut -> Kodkod.formula
    5.15    val declarative_axioms_for_datatypes :
    5.16 -    extended_context -> int -> int Typtab.table -> kodkod_constrs
    5.17 +    hol_context -> int -> int Typtab.table -> kodkod_constrs
    5.18      -> nut NameTable.table -> dtype_spec list -> Kodkod.formula list
    5.19    val kodkod_formula_from_nut :
    5.20      int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula
    5.21 @@ -732,12 +732,12 @@
    5.22  (* nut NameTable.table -> styp -> KK.rel_expr *)
    5.23  fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr
    5.24  
    5.25 -(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
    5.26 +(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
    5.27     -> styp -> int -> nfa_transition list *)
    5.28 -fun nfa_transitions_for_sel ext_ctxt ({kk_project, ...} : kodkod_constrs)
    5.29 +fun nfa_transitions_for_sel hol_ctxt ({kk_project, ...} : kodkod_constrs)
    5.30                              rel_table (dtypes : dtype_spec list) constr_x n =
    5.31    let
    5.32 -    val x as (_, T) = boxed_nth_sel_for_constr ext_ctxt constr_x n
    5.33 +    val x as (_, T) = boxed_nth_sel_for_constr hol_ctxt constr_x n
    5.34      val (r, R, arity) = const_triple rel_table x
    5.35      val type_schema = type_schema_of_rep T R
    5.36    in
    5.37 @@ -746,17 +746,17 @@
    5.38                     else SOME (kk_project r (map KK.Num [0, j]), T))
    5.39                 (index_seq 1 (arity - 1) ~~ tl type_schema)
    5.40    end
    5.41 -(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
    5.42 +(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
    5.43     -> styp -> nfa_transition list *)
    5.44 -fun nfa_transitions_for_constr ext_ctxt kk rel_table dtypes (x as (_, T)) =
    5.45 -  maps (nfa_transitions_for_sel ext_ctxt kk rel_table dtypes x)
    5.46 +fun nfa_transitions_for_constr hol_ctxt kk rel_table dtypes (x as (_, T)) =
    5.47 +  maps (nfa_transitions_for_sel hol_ctxt kk rel_table dtypes x)
    5.48         (index_seq 0 (num_sels_for_constr_type T))
    5.49 -(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
    5.50 +(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
    5.51     -> dtype_spec -> nfa_entry option *)
    5.52  fun nfa_entry_for_datatype _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
    5.53    | nfa_entry_for_datatype _ _ _ _ {deep = false, ...} = NONE
    5.54 -  | nfa_entry_for_datatype ext_ctxt kk rel_table dtypes {typ, constrs, ...} =
    5.55 -    SOME (typ, maps (nfa_transitions_for_constr ext_ctxt kk rel_table dtypes
    5.56 +  | nfa_entry_for_datatype hol_ctxt kk rel_table dtypes {typ, constrs, ...} =
    5.57 +    SOME (typ, maps (nfa_transitions_for_constr hol_ctxt kk rel_table dtypes
    5.58                       o #const) constrs)
    5.59  
    5.60  val empty_rel = KK.Product (KK.None, KK.None)
    5.61 @@ -812,23 +812,23 @@
    5.62  fun acyclicity_axiom_for_datatype dtypes kk nfa start =
    5.63    #kk_no kk (#kk_intersect kk
    5.64                   (loop_path_rel_expr kk nfa (map fst nfa) start) KK.Iden)
    5.65 -(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
    5.66 +(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
    5.67     -> KK.formula list *)
    5.68 -fun acyclicity_axioms_for_datatypes ext_ctxt kk rel_table dtypes =
    5.69 -  map_filter (nfa_entry_for_datatype ext_ctxt kk rel_table dtypes) dtypes
    5.70 +fun acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes =
    5.71 +  map_filter (nfa_entry_for_datatype hol_ctxt kk rel_table dtypes) dtypes
    5.72    |> strongly_connected_sub_nfas
    5.73    |> maps (fn nfa => map (acyclicity_axiom_for_datatype dtypes kk nfa o fst)
    5.74                           nfa)
    5.75  
    5.76 -(* extended_context -> int -> kodkod_constrs -> nut NameTable.table
    5.77 -   -> KK.rel_expr -> constr_spec -> int -> KK.formula *)
    5.78 -fun sel_axiom_for_sel ext_ctxt j0
    5.79 +(* hol_context -> int -> kodkod_constrs -> nut NameTable.table -> KK.rel_expr
    5.80 +   -> constr_spec -> int -> KK.formula *)
    5.81 +fun sel_axiom_for_sel hol_ctxt j0
    5.82          (kk as {kk_all, kk_implies, kk_formula_if, kk_subset, kk_rel_eq, kk_no,
    5.83                  kk_join, ...}) rel_table dom_r
    5.84          ({const, delta, epsilon, exclusive, explicit_max, ...} : constr_spec)
    5.85          n =
    5.86    let
    5.87 -    val x as (_, T) = boxed_nth_sel_for_constr ext_ctxt const n
    5.88 +    val x as (_, T) = boxed_nth_sel_for_constr hol_ctxt const n
    5.89      val (r, R, arity) = const_triple rel_table x
    5.90      val R2 = dest_Func R |> snd
    5.91      val z = (epsilon - delta, delta + j0)
    5.92 @@ -842,9 +842,9 @@
    5.93                                (kk_n_ary_function kk R2 r') (kk_no r'))
    5.94        end
    5.95    end
    5.96 -(* extended_context -> int -> int -> kodkod_constrs -> nut NameTable.table
    5.97 +(* hol_context -> int -> int -> kodkod_constrs -> nut NameTable.table
    5.98     -> constr_spec -> KK.formula list *)
    5.99 -fun sel_axioms_for_constr ext_ctxt bits j0 kk rel_table
   5.100 +fun sel_axioms_for_constr hol_ctxt bits j0 kk rel_table
   5.101          (constr as {const, delta, epsilon, explicit_max, ...}) =
   5.102    let
   5.103      val honors_explicit_max =
   5.104 @@ -866,19 +866,19 @@
   5.105                               " too small for \"max\"")
   5.106        in
   5.107          max_axiom ::
   5.108 -        map (sel_axiom_for_sel ext_ctxt j0 kk rel_table ran_r constr)
   5.109 +        map (sel_axiom_for_sel hol_ctxt j0 kk rel_table ran_r constr)
   5.110              (index_seq 0 (num_sels_for_constr_type (snd const)))
   5.111        end
   5.112    end
   5.113 -(* extended_context -> int -> int -> kodkod_constrs -> nut NameTable.table
   5.114 +(* hol_context -> int -> int -> kodkod_constrs -> nut NameTable.table
   5.115     -> dtype_spec -> KK.formula list *)
   5.116 -fun sel_axioms_for_datatype ext_ctxt bits j0 kk rel_table
   5.117 +fun sel_axioms_for_datatype hol_ctxt bits j0 kk rel_table
   5.118                              ({constrs, ...} : dtype_spec) =
   5.119 -  maps (sel_axioms_for_constr ext_ctxt bits j0 kk rel_table) constrs
   5.120 +  maps (sel_axioms_for_constr hol_ctxt bits j0 kk rel_table) constrs
   5.121  
   5.122 -(* extended_context -> kodkod_constrs -> nut NameTable.table -> constr_spec
   5.123 +(* hol_context -> kodkod_constrs -> nut NameTable.table -> constr_spec
   5.124     -> KK.formula list *)
   5.125 -fun uniqueness_axiom_for_constr ext_ctxt
   5.126 +fun uniqueness_axiom_for_constr hol_ctxt
   5.127          ({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...}
   5.128           : kodkod_constrs) rel_table ({const, ...} : constr_spec) =
   5.129    let
   5.130 @@ -887,7 +887,7 @@
   5.131        kk_rel_eq (kk_join (KK.Var (1, 0)) r) (kk_join (KK.Var (1, 1)) r)
   5.132      val num_sels = num_sels_for_constr_type (snd const)
   5.133      val triples = map (const_triple rel_table
   5.134 -                       o boxed_nth_sel_for_constr ext_ctxt const)
   5.135 +                       o boxed_nth_sel_for_constr hol_ctxt const)
   5.136                        (~1 upto num_sels - 1)
   5.137      val j0 = case triples |> hd |> #2 of
   5.138                 Func (Atom (_, j0), _) => j0
   5.139 @@ -903,11 +903,11 @@
   5.140                    (fold1 kk_and (map (conjunct_for_sel o #1) (tl triples)))
   5.141                    (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))
   5.142    end
   5.143 -(* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec
   5.144 +(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec
   5.145     -> KK.formula list *)
   5.146 -fun uniqueness_axioms_for_datatype ext_ctxt kk rel_table
   5.147 +fun uniqueness_axioms_for_datatype hol_ctxt kk rel_table
   5.148                                     ({constrs, ...} : dtype_spec) =
   5.149 -  map (uniqueness_axiom_for_constr ext_ctxt kk rel_table) constrs
   5.150 +  map (uniqueness_axiom_for_constr hol_ctxt kk rel_table) constrs
   5.151  
   5.152  (* constr_spec -> int *)
   5.153  fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta
   5.154 @@ -924,22 +924,22 @@
   5.155         kk_disjoint_sets kk rs]
   5.156      end
   5.157  
   5.158 -(* extended_context -> int -> int Typtab.table -> kodkod_constrs
   5.159 +(* hol_context -> int -> int Typtab.table -> kodkod_constrs
   5.160     -> nut NameTable.table -> dtype_spec -> KK.formula list *)
   5.161  fun other_axioms_for_datatype _ _ _ _ _ {deep = false, ...} = []
   5.162 -  | other_axioms_for_datatype ext_ctxt bits ofs kk rel_table
   5.163 +  | other_axioms_for_datatype hol_ctxt bits ofs kk rel_table
   5.164                                (dtype as {typ, ...}) =
   5.165      let val j0 = offset_of_type ofs typ in
   5.166 -      sel_axioms_for_datatype ext_ctxt bits j0 kk rel_table dtype @
   5.167 -      uniqueness_axioms_for_datatype ext_ctxt kk rel_table dtype @
   5.168 +      sel_axioms_for_datatype hol_ctxt bits j0 kk rel_table dtype @
   5.169 +      uniqueness_axioms_for_datatype hol_ctxt kk rel_table dtype @
   5.170        partition_axioms_for_datatype j0 kk rel_table dtype
   5.171      end
   5.172  
   5.173 -(* extended_context -> int -> int Typtab.table -> kodkod_constrs
   5.174 +(* hol_context -> int -> int Typtab.table -> kodkod_constrs
   5.175     -> nut NameTable.table -> dtype_spec list -> KK.formula list *)
   5.176 -fun declarative_axioms_for_datatypes ext_ctxt bits ofs kk rel_table dtypes =
   5.177 -  acyclicity_axioms_for_datatypes ext_ctxt kk rel_table dtypes @
   5.178 -  maps (other_axioms_for_datatype ext_ctxt bits ofs kk rel_table) dtypes
   5.179 +fun declarative_axioms_for_datatypes hol_ctxt bits ofs kk rel_table dtypes =
   5.180 +  acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes @
   5.181 +  maps (other_axioms_for_datatype hol_ctxt bits ofs kk rel_table) dtypes
   5.182  
   5.183  (* int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> KK.formula *)
   5.184  fun kodkod_formula_from_nut bits ofs liberal
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Feb 04 13:36:52 2010 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Feb 04 16:03:15 2010 +0100
     6.3 @@ -251,7 +251,7 @@
     6.4     -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ -> typ -> rep
     6.5     -> int list list -> term *)
     6.6  fun reconstruct_term (maybe_name, base_name, step_name, abs_name)
     6.7 -        ({ext_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...}
     6.8 +        ({hol_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...}
     6.9           : scope) sel_names rel_table bounds =
    6.10    let
    6.11      val for_auto = (maybe_name = "")
    6.12 @@ -400,7 +400,7 @@
    6.13                              else NONE)
    6.14                          (discr_jsss ~~ constrs) |> the
    6.15              val arg_Ts = curried_binder_types constr_T
    6.16 -            val sel_xs = map (boxed_nth_sel_for_constr ext_ctxt constr_x)
    6.17 +            val sel_xs = map (boxed_nth_sel_for_constr hol_ctxt constr_x)
    6.18                               (index_seq 0 (length arg_Ts))
    6.19              val sel_Rs =
    6.20                map (fn x => get_first
    6.21 @@ -586,7 +586,7 @@
    6.22    -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list
    6.23    -> Pretty.T * bool *)
    6.24  fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
    6.25 -        ({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, stds, wfs,
    6.26 +        ({hol_ctxt as {thy, ctxt, max_bisim_depth, boxes, stds, wfs,
    6.27                         user_axioms, debug, binary_ints, destroy_constrs,
    6.28                         specialize, skolemize, star_linear_preds, uncurry,
    6.29                         fast_descrs, tac_timeout, evals, case_names, def_table,
    6.30 @@ -598,7 +598,7 @@
    6.31    let
    6.32      val (wacky_names as (_, base_name, step_name, _), ctxt) =
    6.33        add_wacky_syntax ctxt
    6.34 -    val ext_ctxt =
    6.35 +    val hol_ctxt =
    6.36        {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
    6.37         stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
    6.38         binary_ints = binary_ints, destroy_constrs = destroy_constrs,
    6.39 @@ -612,7 +612,7 @@
    6.40         ersatz_table = ersatz_table, skolems = skolems,
    6.41         special_funs = special_funs, unrolled_preds = unrolled_preds,
    6.42         wf_cache = wf_cache, constr_cache = constr_cache}
    6.43 -    val scope = {ext_ctxt = ext_ctxt, card_assigns = card_assigns,
    6.44 +    val scope = {hol_ctxt = hol_ctxt, card_assigns = card_assigns,
    6.45                   bits = bits, bisim_depth = bisim_depth, datatypes = datatypes,
    6.46                   ofs = ofs}
    6.47      (* typ -> typ -> rep -> int list list -> term *)
    6.48 @@ -644,7 +644,7 @@
    6.49              end
    6.50            | ConstName (s, T, _) =>
    6.51              (assign_operator_for_const (s, T),
    6.52 -             user_friendly_const ext_ctxt (base_name, step_name) formats (s, T),
    6.53 +             user_friendly_const hol_ctxt (base_name, step_name) formats (s, T),
    6.54               T)
    6.55            | _ => raise NUT ("Nitpick_Model.reconstruct_hol_model.\
    6.56                              \pretty_for_assign", [name])
    6.57 @@ -724,7 +724,7 @@
    6.58  
    6.59  (* scope -> Time.time option -> nut list -> nut list -> nut NameTable.table
    6.60     -> KK.raw_bound list -> term -> bool option *)
    6.61 -fun prove_hol_model (scope as {ext_ctxt as {thy, ctxt, debug, ...},
    6.62 +fun prove_hol_model (scope as {hol_ctxt as {thy, ctxt, debug, ...},
    6.63                                 card_assigns, ...})
    6.64                      auto_timeout free_names sel_names rel_table bounds prop =
    6.65    let
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Feb 04 13:36:52 2010 +0100
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Feb 04 16:03:15 2010 +0100
     7.3 @@ -8,10 +8,10 @@
     7.4  signature NITPICK_MONO =
     7.5  sig
     7.6    datatype sign = Plus | Minus
     7.7 -  type extended_context = Nitpick_HOL.extended_context
     7.8 +  type hol_context = Nitpick_HOL.hol_context
     7.9  
    7.10    val formulas_monotonic :
    7.11 -    extended_context -> typ -> sign -> term list -> term list -> term -> bool
    7.12 +    hol_context -> typ -> sign -> term list -> term list -> term -> bool
    7.13  end;
    7.14  
    7.15  structure Nitpick_Mono : NITPICK_MONO =
    7.16 @@ -35,7 +35,7 @@
    7.17    CRec of string * typ list
    7.18  
    7.19  type cdata =
    7.20 -  {ext_ctxt: extended_context,
    7.21 +  {hol_ctxt: hol_context,
    7.22     alpha_T: typ,
    7.23     max_fresh: int Unsynchronized.ref,
    7.24     datatype_cache: ((string * typ list) * ctype) list Unsynchronized.ref,
    7.25 @@ -114,9 +114,9 @@
    7.26    | flatten_ctype (CType (_, Cs)) = maps flatten_ctype Cs
    7.27    | flatten_ctype C = [C]
    7.28  
    7.29 -(* extended_context -> typ -> cdata *)
    7.30 -fun initial_cdata ext_ctxt alpha_T =
    7.31 -  ({ext_ctxt = ext_ctxt, alpha_T = alpha_T, max_fresh = Unsynchronized.ref 0,
    7.32 +(* hol_context -> typ -> cdata *)
    7.33 +fun initial_cdata hol_ctxt alpha_T =
    7.34 +  ({hol_ctxt = hol_ctxt, alpha_T = alpha_T, max_fresh = Unsynchronized.ref 0,
    7.35      datatype_cache = Unsynchronized.ref [],
    7.36      constr_cache = Unsynchronized.ref []} : cdata)
    7.37  
    7.38 @@ -188,7 +188,7 @@
    7.39    in List.app repair_one (!constr_cache) end
    7.40  
    7.41  (* cdata -> typ -> ctype *)
    7.42 -fun fresh_ctype_for_type ({ext_ctxt as {thy, ...}, alpha_T, max_fresh,
    7.43 +fun fresh_ctype_for_type ({hol_ctxt as {thy, ...}, alpha_T, max_fresh,
    7.44                             datatype_cache, constr_cache, ...} : cdata) =
    7.45    let
    7.46      (* typ -> typ -> ctype *)
    7.47 @@ -217,7 +217,7 @@
    7.48            | NONE =>
    7.49              let
    7.50                val _ = Unsynchronized.change datatype_cache (cons (z, CRec z))
    7.51 -              val xs = datatype_constrs ext_ctxt T
    7.52 +              val xs = datatype_constrs hol_ctxt T
    7.53                val (all_Cs, constr_Cs) =
    7.54                  fold_rev (fn (_, T') => fn (all_Cs, constr_Cs) =>
    7.55                               let
    7.56 @@ -264,7 +264,7 @@
    7.57    end
    7.58  
    7.59  (* cdata -> styp -> ctype *)
    7.60 -fun ctype_for_constr (cdata as {ext_ctxt as {thy, ...}, alpha_T, constr_cache,
    7.61 +fun ctype_for_constr (cdata as {hol_ctxt as {thy, ...}, alpha_T, constr_cache,
    7.62                                  ...}) (x as (_, T)) =
    7.63    if could_exist_alpha_sub_ctype thy alpha_T T then
    7.64      case AList.lookup (op =) (!constr_cache) x of
    7.65 @@ -278,8 +278,8 @@
    7.66                   AList.lookup (op =) (!constr_cache) x |> the)
    7.67    else
    7.68      fresh_ctype_for_type cdata T
    7.69 -fun ctype_for_sel (cdata as {ext_ctxt, ...}) (x as (s, _)) =
    7.70 -  x |> boxed_constr_for_sel ext_ctxt |> ctype_for_constr cdata
    7.71 +fun ctype_for_sel (cdata as {hol_ctxt, ...}) (x as (s, _)) =
    7.72 +  x |> boxed_constr_for_sel hol_ctxt |> ctype_for_constr cdata
    7.73      |> sel_ctype_from_constr_ctype s
    7.74  
    7.75  (* literal list -> ctype -> ctype *)
    7.76 @@ -549,7 +549,7 @@
    7.77    handle List.Empty => initial_gamma
    7.78  
    7.79  (* cdata -> term -> accumulator -> ctype * accumulator *)
    7.80 -fun consider_term (cdata as {ext_ctxt as {ctxt, thy, def_table, ...}, alpha_T,
    7.81 +fun consider_term (cdata as {hol_ctxt as {ctxt, thy, def_table, ...}, alpha_T,
    7.82                               max_fresh, ...}) =
    7.83    let
    7.84      (* typ -> ctype *)
    7.85 @@ -806,7 +806,7 @@
    7.86    in do_term end
    7.87  
    7.88  (* cdata -> sign -> term -> accumulator -> accumulator *)
    7.89 -fun consider_general_formula (cdata as {ext_ctxt as {ctxt, ...}, ...}) =
    7.90 +fun consider_general_formula (cdata as {hol_ctxt as {ctxt, ...}, ...}) =
    7.91    let
    7.92      (* typ -> ctype *)
    7.93      val ctype_for = fresh_ctype_for_type cdata
    7.94 @@ -895,7 +895,7 @@
    7.95    not (is_harmless_axiom t) ? consider_general_formula cdata sn t
    7.96  
    7.97  (* cdata -> term -> accumulator -> accumulator *)
    7.98 -fun consider_definitional_axiom (cdata as {ext_ctxt as {thy, ...}, ...}) t =
    7.99 +fun consider_definitional_axiom (cdata as {hol_ctxt as {thy, ...}, ...}) t =
   7.100    if not (is_constr_pattern_formula thy t) then
   7.101      consider_nondefinitional_axiom cdata Plus t
   7.102    else if is_harmless_axiom t then
   7.103 @@ -945,13 +945,13 @@
   7.104    map (fn (x, C) => string_for_ctype_of_term ctxt lits (Const x) C) consts
   7.105    |> cat_lines |> print_g
   7.106  
   7.107 -(* extended_context -> typ -> sign -> term list -> term list -> term -> bool *)
   7.108 -fun formulas_monotonic (ext_ctxt as {ctxt, ...}) alpha_T sn def_ts nondef_ts
   7.109 +(* hol_context -> typ -> sign -> term list -> term list -> term -> bool *)
   7.110 +fun formulas_monotonic (hol_ctxt as {ctxt, ...}) alpha_T sn def_ts nondef_ts
   7.111                         core_t =
   7.112    let
   7.113      val _ = print_g ("****** " ^ string_for_ctype CAlpha ^ " is " ^
   7.114                       Syntax.string_of_typ ctxt alpha_T)
   7.115 -    val cdata as {max_fresh, ...} = initial_cdata ext_ctxt alpha_T
   7.116 +    val cdata as {max_fresh, ...} = initial_cdata hol_ctxt alpha_T
   7.117      val (gamma, cset) =
   7.118        (initial_gamma, slack)
   7.119        |> fold (consider_definitional_axiom cdata) def_ts
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Thu Feb 04 13:36:52 2010 +0100
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Thu Feb 04 16:03:15 2010 +0100
     8.3 @@ -8,7 +8,7 @@
     8.4  signature NITPICK_NUT =
     8.5  sig
     8.6    type special_fun = Nitpick_HOL.special_fun
     8.7 -  type extended_context = Nitpick_HOL.extended_context
     8.8 +  type hol_context = Nitpick_HOL.hol_context
     8.9    type scope = Nitpick_Scope.scope
    8.10    type name_pool = Nitpick_Peephole.name_pool
    8.11    type rep = Nitpick_Rep.rep
    8.12 @@ -106,7 +106,7 @@
    8.13    val name_ord : (nut * nut) -> order
    8.14    val the_name : 'a NameTable.table -> nut -> 'a
    8.15    val the_rel : nut NameTable.table -> nut -> Kodkod.n_ary_index
    8.16 -  val nut_from_term : extended_context -> op2 -> term -> nut
    8.17 +  val nut_from_term : hol_context -> op2 -> term -> nut
    8.18    val choose_reps_for_free_vars :
    8.19      scope -> nut list -> rep NameTable.table -> nut list * rep NameTable.table
    8.20    val choose_reps_for_consts :
    8.21 @@ -466,8 +466,8 @@
    8.22  fun factorize (z as (Type ("*", _), _)) = maps factorize [mk_fst z, mk_snd z]
    8.23    | factorize z = [z]
    8.24  
    8.25 -(* extended_context -> op2 -> term -> nut *)
    8.26 -fun nut_from_term (ext_ctxt as {thy, fast_descrs, special_funs, ...}) eq =
    8.27 +(* hol_context -> op2 -> term -> nut *)
    8.28 +fun nut_from_term (hol_ctxt as {thy, fast_descrs, special_funs, ...}) eq =
    8.29    let
    8.30      (* string list -> typ list -> term -> nut *)
    8.31      fun aux eq ss Ts t =
    8.32 @@ -597,7 +597,7 @@
    8.33            Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
    8.34          | (Const (@{const_name Suc}, T), []) => Cst (Suc, T, Any)
    8.35          | (Const (@{const_name finite}, T), [t1]) =>
    8.36 -          (if is_finite_type ext_ctxt (domain_type T) then
    8.37 +          (if is_finite_type hol_ctxt (domain_type T) then
    8.38               Cst (True, bool_T, Any)
    8.39             else case t1 of
    8.40               Const (@{const_name top}, _) => Cst (False, bool_T, Any)
    8.41 @@ -712,7 +712,7 @@
    8.42    in (v :: vs, NameTable.update (v, R) table) end
    8.43  (* scope -> bool -> nut -> nut list * rep NameTable.table
    8.44     -> nut list * rep NameTable.table *)
    8.45 -fun choose_rep_for_const (scope as {ext_ctxt as {thy, ctxt, ...}, datatypes,
    8.46 +fun choose_rep_for_const (scope as {hol_ctxt as {thy, ctxt, ...}, datatypes,
    8.47                                      ofs, ...}) all_exact v (vs, table) =
    8.48    let
    8.49      val x as (s, T) = (nickname_of v, type_of v)
    8.50 @@ -747,10 +747,10 @@
    8.51  
    8.52  (* scope -> styp -> int -> nut list * rep NameTable.table
    8.53     -> nut list * rep NameTable.table *)
    8.54 -fun choose_rep_for_nth_sel_for_constr (scope as {ext_ctxt, ...}) (x as (_, T)) n
    8.55 +fun choose_rep_for_nth_sel_for_constr (scope as {hol_ctxt, ...}) (x as (_, T)) n
    8.56                                        (vs, table) =
    8.57    let
    8.58 -    val (s', T') = boxed_nth_sel_for_constr ext_ctxt x n
    8.59 +    val (s', T') = boxed_nth_sel_for_constr hol_ctxt x n
    8.60      val R' = if n = ~1 orelse is_word_type (body_type T) orelse
    8.61                  (is_fun_type (range_type T') andalso
    8.62                   is_boolean_type (body_type T')) then
    8.63 @@ -890,7 +890,7 @@
    8.64    | untuple f u = if rep_of u = Unit then [] else [f u]
    8.65  
    8.66  (* scope -> bool -> rep NameTable.table -> bool -> nut -> nut *)
    8.67 -fun choose_reps_in_nut (scope as {ext_ctxt as {thy, ctxt, ...}, card_assigns,
    8.68 +fun choose_reps_in_nut (scope as {hol_ctxt as {thy, ctxt, ...}, card_assigns,
    8.69                                    bits, datatypes, ofs, ...})
    8.70                         liberal table def =
    8.71    let
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Feb 04 16:03:15 2010 +0100
     9.3 @@ -0,0 +1,1431 @@
     9.4 +(*  Title:      HOL/Tools/Nitpick/nitpick_preproc.ML
     9.5 +    Author:     Jasmin Blanchette, TU Muenchen
     9.6 +    Copyright   2008, 2009, 2010
     9.7 +
     9.8 +Nitpick's HOL preprocessor.
     9.9 +*)
    9.10 +
    9.11 +signature NITPICK_PREPROC =
    9.12 +sig
    9.13 +  type hol_context = Nitpick_HOL.hol_context
    9.14 +  val preprocess_term :
    9.15 +    hol_context -> term -> ((term list * term list) * (bool * bool)) * term
    9.16 +end
    9.17 +
    9.18 +structure Nitpick_Preproc : NITPICK_PREPROC =
    9.19 +struct
    9.20 +
    9.21 +open Nitpick_Util
    9.22 +open Nitpick_HOL
    9.23 +
    9.24 +(* polarity -> string -> bool *)
    9.25 +fun is_positive_existential polar quant_s =
    9.26 +  (polar = Pos andalso quant_s = @{const_name Ex}) orelse
    9.27 +  (polar = Neg andalso quant_s <> @{const_name Ex})
    9.28 +
    9.29 +(** Binary coding of integers **)
    9.30 +
    9.31 +(* If a formula contains a numeral whose absolute value is more than this
    9.32 +   threshold, the unary coding is likely not to work well and we prefer the
    9.33 +   binary coding. *)
    9.34 +val binary_int_threshold = 3
    9.35 +
    9.36 +(* term -> bool *)
    9.37 +fun may_use_binary_ints (t1 $ t2) =
    9.38 +    may_use_binary_ints t1 andalso may_use_binary_ints t2
    9.39 +  | may_use_binary_ints (t as Const (s, _)) =
    9.40 +    t <> @{const Suc} andalso
    9.41 +    not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac},
    9.42 +                        @{const_name nat_gcd}, @{const_name nat_lcm},
    9.43 +                        @{const_name Frac}, @{const_name norm_frac}] s)
    9.44 +  | may_use_binary_ints (Abs (_, _, t')) = may_use_binary_ints t'
    9.45 +  | may_use_binary_ints _ = true
    9.46 +fun should_use_binary_ints (t1 $ t2) =
    9.47 +    should_use_binary_ints t1 orelse should_use_binary_ints t2
    9.48 +  | should_use_binary_ints (Const (s, _)) =
    9.49 +    member (op =) [@{const_name times_nat_inst.times_nat},
    9.50 +                   @{const_name div_nat_inst.div_nat},
    9.51 +                   @{const_name times_int_inst.times_int},
    9.52 +                   @{const_name div_int_inst.div_int}] s orelse
    9.53 +    (String.isPrefix numeral_prefix s andalso
    9.54 +     let val n = the (Int.fromString (unprefix numeral_prefix s)) in
    9.55 +       n < ~ binary_int_threshold orelse n > binary_int_threshold
    9.56 +     end)
    9.57 +  | should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t'
    9.58 +  | should_use_binary_ints _ = false
    9.59 +
    9.60 +(* typ -> typ *)
    9.61 +fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}
    9.62 +  | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}
    9.63 +  | binarize_nat_and_int_in_type (Type (s, Ts)) =
    9.64 +    Type (s, map binarize_nat_and_int_in_type Ts)
    9.65 +  | binarize_nat_and_int_in_type T = T
    9.66 +(* term -> term *)
    9.67 +val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type
    9.68 +
    9.69 +(** Uncurrying **)
    9.70 +
    9.71 +(* theory -> term -> int Termtab.tab -> int Termtab.tab *)
    9.72 +fun add_to_uncurry_table thy t =
    9.73 +  let
    9.74 +    (* term -> term list -> int Termtab.tab -> int Termtab.tab *)
    9.75 +    fun aux (t1 $ t2) args table =
    9.76 +        let val table = aux t2 [] table in aux t1 (t2 :: args) table end
    9.77 +      | aux (Abs (_, _, t')) _ table = aux t' [] table
    9.78 +      | aux (t as Const (x as (s, _))) args table =
    9.79 +        if is_built_in_const true x orelse is_constr_like thy x orelse
    9.80 +           is_sel s orelse s = @{const_name Sigma} then
    9.81 +          table
    9.82 +        else
    9.83 +          Termtab.map_default (t, 65536) (curry Int.min (length args)) table
    9.84 +      | aux _ _ table = table
    9.85 +  in aux t [] end
    9.86 +
    9.87 +(* int -> int -> string *)
    9.88 +fun uncurry_prefix_for k j =
    9.89 +  uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
    9.90 +
    9.91 +(* int Termtab.tab term -> term *)
    9.92 +fun uncurry_term table t =
    9.93 +  let
    9.94 +    (* term -> term list -> term *)
    9.95 +    fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args)
    9.96 +      | aux (Abs (s, T, t')) args = betapplys (Abs (s, T, aux t' []), args)
    9.97 +      | aux (t as Const (s, T)) args =
    9.98 +        (case Termtab.lookup table t of
    9.99 +           SOME n =>
   9.100 +           if n >= 2 then
   9.101 +             let
   9.102 +               val (arg_Ts, rest_T) = strip_n_binders n T
   9.103 +               val j =
   9.104 +                 if hd arg_Ts = @{typ bisim_iterator} orelse
   9.105 +                    is_fp_iterator_type (hd arg_Ts) then
   9.106 +                   1
   9.107 +                 else case find_index (not_equal bool_T) arg_Ts of
   9.108 +                   ~1 => n
   9.109 +                 | j => j
   9.110 +               val ((before_args, tuple_args), after_args) =
   9.111 +                 args |> chop n |>> chop j
   9.112 +               val ((before_arg_Ts, tuple_arg_Ts), rest_T) =
   9.113 +                 T |> strip_n_binders n |>> chop j
   9.114 +               val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
   9.115 +             in
   9.116 +               if n - j < 2 then
   9.117 +                 betapplys (t, args)
   9.118 +               else
   9.119 +                 betapplys (Const (uncurry_prefix_for (n - j) j ^ s,
   9.120 +                                   before_arg_Ts ---> tuple_T --> rest_T),
   9.121 +                            before_args @ [mk_flat_tuple tuple_T tuple_args] @
   9.122 +                            after_args)
   9.123 +             end
   9.124 +           else
   9.125 +             betapplys (t, args)
   9.126 +         | NONE => betapplys (t, args))
   9.127 +      | aux t args = betapplys (t, args)
   9.128 +  in aux t [] end
   9.129 +
   9.130 +(** Boxing **)
   9.131 +
   9.132 +(* hol_context -> typ -> term -> term *)
   9.133 +fun constr_expand (hol_ctxt as {thy, ...}) T t =
   9.134 +  (case head_of t of
   9.135 +     Const x => if is_constr_like thy x then t else raise SAME ()
   9.136 +   | _ => raise SAME ())
   9.137 +  handle SAME () =>
   9.138 +         let
   9.139 +           val x' as (_, T') =
   9.140 +             if is_pair_type T then
   9.141 +               let val (T1, T2) = HOLogic.dest_prodT T in
   9.142 +                 (@{const_name Pair}, T1 --> T2 --> T)
   9.143 +               end
   9.144 +             else
   9.145 +               datatype_constrs hol_ctxt T |> hd
   9.146 +           val arg_Ts = binder_types T'
   9.147 +         in
   9.148 +           list_comb (Const x', map2 (select_nth_constr_arg thy x' t)
   9.149 +                                     (index_seq 0 (length arg_Ts)) arg_Ts)
   9.150 +         end
   9.151 +
   9.152 +(* hol_context -> bool -> term -> term *)
   9.153 +fun box_fun_and_pair_in_term (hol_ctxt as {thy, fast_descrs, ...}) def orig_t =
   9.154 +  let
   9.155 +    (* typ -> typ *)
   9.156 +    fun box_relational_operator_type (Type ("fun", Ts)) =
   9.157 +        Type ("fun", map box_relational_operator_type Ts)
   9.158 +      | box_relational_operator_type (Type ("*", Ts)) =
   9.159 +        Type ("*", map (box_type hol_ctxt InPair) Ts)
   9.160 +      | box_relational_operator_type T = T
   9.161 +    (* (term -> term) -> int -> term -> term *)
   9.162 +    fun coerce_bound_no f j t =
   9.163 +      case t of
   9.164 +        t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
   9.165 +      | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
   9.166 +      | Bound j' => if j' = j then f t else t
   9.167 +      | _ => t
   9.168 +    (* typ -> typ -> term -> term *)
   9.169 +    fun coerce_bound_0_in_term new_T old_T =
   9.170 +      old_T <> new_T ? coerce_bound_no (coerce_term [new_T] old_T new_T) 0
   9.171 +    (* typ list -> typ -> term -> term *)
   9.172 +    and coerce_term Ts new_T old_T t =
   9.173 +      if old_T = new_T then
   9.174 +        t
   9.175 +      else
   9.176 +        case (new_T, old_T) of
   9.177 +          (Type (new_s, new_Ts as [new_T1, new_T2]),
   9.178 +           Type ("fun", [old_T1, old_T2])) =>
   9.179 +          (case eta_expand Ts t 1 of
   9.180 +             Abs (s, _, t') =>
   9.181 +             Abs (s, new_T1,
   9.182 +                  t' |> coerce_bound_0_in_term new_T1 old_T1
   9.183 +                     |> coerce_term (new_T1 :: Ts) new_T2 old_T2)
   9.184 +             |> Envir.eta_contract
   9.185 +             |> new_s <> "fun"
   9.186 +                ? construct_value thy (@{const_name FunBox},
   9.187 +                                       Type ("fun", new_Ts) --> new_T) o single
   9.188 +           | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\
   9.189 +                               \coerce_term", [t']))
   9.190 +        | (Type (new_s, new_Ts as [new_T1, new_T2]),
   9.191 +           Type (old_s, old_Ts as [old_T1, old_T2])) =>
   9.192 +          if old_s = @{type_name fun_box} orelse
   9.193 +             old_s = @{type_name pair_box} orelse old_s = "*" then
   9.194 +            case constr_expand hol_ctxt old_T t of
   9.195 +              Const (@{const_name FunBox}, _) $ t1 =>
   9.196 +              if new_s = "fun" then
   9.197 +                coerce_term Ts new_T (Type ("fun", old_Ts)) t1
   9.198 +              else
   9.199 +                construct_value thy
   9.200 +                    (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
   9.201 +                     [coerce_term Ts (Type ("fun", new_Ts))
   9.202 +                                  (Type ("fun", old_Ts)) t1]
   9.203 +            | Const _ $ t1 $ t2 =>
   9.204 +              construct_value thy
   9.205 +                  (if new_s = "*" then @{const_name Pair}
   9.206 +                   else @{const_name PairBox}, new_Ts ---> new_T)
   9.207 +                  [coerce_term Ts new_T1 old_T1 t1,
   9.208 +                   coerce_term Ts new_T2 old_T2 t2]
   9.209 +            | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\
   9.210 +                                \coerce_term", [t'])
   9.211 +          else
   9.212 +            raise TYPE ("coerce_term", [new_T, old_T], [t])
   9.213 +        | _ => raise TYPE ("coerce_term", [new_T, old_T], [t])
   9.214 +    (* indexname * typ -> typ * term -> typ option list -> typ option list *)
   9.215 +    fun add_boxed_types_for_var (z as (_, T)) (T', t') =
   9.216 +      case t' of
   9.217 +        Var z' => z' = z ? insert (op =) T'
   9.218 +      | Const (@{const_name Pair}, _) $ t1 $ t2 =>
   9.219 +        (case T' of
   9.220 +           Type (_, [T1, T2]) =>
   9.221 +           fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)]
   9.222 +         | _ => raise TYPE ("Nitpick_Preproc.box_fun_and_pair_in_term.\
   9.223 +                            \add_boxed_types_for_var", [T'], []))
   9.224 +      | _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T
   9.225 +    (* typ list -> typ list -> term -> indexname * typ -> typ *)
   9.226 +    fun box_var_in_def new_Ts old_Ts t (z as (_, T)) =
   9.227 +      case t of
   9.228 +        @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
   9.229 +      | Const (s0, _) $ t1 $ _ =>
   9.230 +        if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then
   9.231 +          let
   9.232 +            val (t', args) = strip_comb t1
   9.233 +            val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
   9.234 +          in
   9.235 +            case fold (add_boxed_types_for_var z)
   9.236 +                      (fst (strip_n_binders (length args) T') ~~ args) [] of
   9.237 +              [T''] => T''
   9.238 +            | _ => T
   9.239 +          end
   9.240 +        else
   9.241 +          T
   9.242 +      | _ => T
   9.243 +    (* typ list -> typ list -> polarity -> string -> typ -> string -> typ
   9.244 +       -> term -> term *)
   9.245 +    and do_quantifier new_Ts old_Ts polar quant_s quant_T abs_s abs_T t =
   9.246 +      let
   9.247 +        val abs_T' =
   9.248 +          if polar = Neut orelse is_positive_existential polar quant_s then
   9.249 +            box_type hol_ctxt InFunLHS abs_T
   9.250 +          else
   9.251 +            abs_T
   9.252 +        val body_T = body_type quant_T
   9.253 +      in
   9.254 +        Const (quant_s, (abs_T' --> body_T) --> body_T)
   9.255 +        $ Abs (abs_s, abs_T',
   9.256 +               t |> do_term (abs_T' :: new_Ts) (abs_T :: old_Ts) polar)
   9.257 +      end
   9.258 +    (* typ list -> typ list -> string -> typ -> term -> term -> term *)
   9.259 +    and do_equals new_Ts old_Ts s0 T0 t1 t2 =
   9.260 +      let
   9.261 +        val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2)
   9.262 +        val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
   9.263 +        val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last
   9.264 +      in
   9.265 +        list_comb (Const (s0, T --> T --> body_type T0),
   9.266 +                   map2 (coerce_term new_Ts T) [T1, T2] [t1, t2])
   9.267 +      end
   9.268 +    (* string -> typ -> term *)
   9.269 +    and do_description_operator s T =
   9.270 +      let val T1 = box_type hol_ctxt InFunLHS (range_type T) in
   9.271 +        Const (s, (T1 --> bool_T) --> T1)
   9.272 +      end
   9.273 +    (* typ list -> typ list -> polarity -> term -> term *)
   9.274 +    and do_term new_Ts old_Ts polar t =
   9.275 +      case t of
   9.276 +        Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
   9.277 +        do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
   9.278 +      | Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 =>
   9.279 +        do_equals new_Ts old_Ts s0 T0 t1 t2
   9.280 +      | @{const "==>"} $ t1 $ t2 =>
   9.281 +        @{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
   9.282 +        $ do_term new_Ts old_Ts polar t2
   9.283 +      | @{const Pure.conjunction} $ t1 $ t2 =>
   9.284 +        @{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1
   9.285 +        $ do_term new_Ts old_Ts polar t2
   9.286 +      | @{const Trueprop} $ t1 =>
   9.287 +        @{const Trueprop} $ do_term new_Ts old_Ts polar t1
   9.288 +      | @{const Not} $ t1 =>
   9.289 +        @{const Not} $ do_term new_Ts old_Ts (flip_polarity polar) t1
   9.290 +      | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
   9.291 +        do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
   9.292 +      | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
   9.293 +        do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
   9.294 +      | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>
   9.295 +        do_equals new_Ts old_Ts s0 T0 t1 t2
   9.296 +      | @{const "op &"} $ t1 $ t2 =>
   9.297 +        @{const "op &"} $ do_term new_Ts old_Ts polar t1
   9.298 +        $ do_term new_Ts old_Ts polar t2
   9.299 +      | @{const "op |"} $ t1 $ t2 =>
   9.300 +        @{const "op |"} $ do_term new_Ts old_Ts polar t1
   9.301 +        $ do_term new_Ts old_Ts polar t2
   9.302 +      | @{const "op -->"} $ t1 $ t2 =>
   9.303 +        @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
   9.304 +        $ do_term new_Ts old_Ts polar t2
   9.305 +      | Const (s as @{const_name The}, T) => do_description_operator s T
   9.306 +      | Const (s as @{const_name Eps}, T) => do_description_operator s T
   9.307 +      | Const (@{const_name quot_normal}, Type ("fun", [_, T2])) =>
   9.308 +        let val T' = box_type hol_ctxt InSel T2 in
   9.309 +          Const (@{const_name quot_normal}, T' --> T')
   9.310 +        end
   9.311 +      | Const (s as @{const_name Tha}, T) => do_description_operator s T
   9.312 +      | Const (x as (s, T)) =>
   9.313 +        Const (s, if s = @{const_name converse} orelse
   9.314 +                     s = @{const_name trancl} then
   9.315 +                    box_relational_operator_type T
   9.316 +                  else if is_built_in_const fast_descrs x orelse
   9.317 +                          s = @{const_name Sigma} then
   9.318 +                    T
   9.319 +                  else if is_constr_like thy x then
   9.320 +                    box_type hol_ctxt InConstr T
   9.321 +                  else if is_sel s
   9.322 +                       orelse is_rep_fun thy x then
   9.323 +                    box_type hol_ctxt InSel T
   9.324 +                  else
   9.325 +                    box_type hol_ctxt InExpr T)
   9.326 +      | t1 $ Abs (s, T, t2') =>
   9.327 +        let
   9.328 +          val t1 = do_term new_Ts old_Ts Neut t1
   9.329 +          val T1 = fastype_of1 (new_Ts, t1)
   9.330 +          val (s1, Ts1) = dest_Type T1
   9.331 +          val T' = hd (snd (dest_Type (hd Ts1)))
   9.332 +          val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2')
   9.333 +          val T2 = fastype_of1 (new_Ts, t2)
   9.334 +          val t2 = coerce_term new_Ts (hd Ts1) T2 t2
   9.335 +        in
   9.336 +          betapply (if s1 = "fun" then
   9.337 +                      t1
   9.338 +                    else
   9.339 +                      select_nth_constr_arg thy
   9.340 +                          (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
   9.341 +                          (Type ("fun", Ts1)), t2)
   9.342 +        end
   9.343 +      | t1 $ t2 =>
   9.344 +        let
   9.345 +          val t1 = do_term new_Ts old_Ts Neut t1
   9.346 +          val T1 = fastype_of1 (new_Ts, t1)
   9.347 +          val (s1, Ts1) = dest_Type T1
   9.348 +          val t2 = do_term new_Ts old_Ts Neut t2
   9.349 +          val T2 = fastype_of1 (new_Ts, t2)
   9.350 +          val t2 = coerce_term new_Ts (hd Ts1) T2 t2
   9.351 +        in
   9.352 +          betapply (if s1 = "fun" then
   9.353 +                      t1
   9.354 +                    else
   9.355 +                      select_nth_constr_arg thy
   9.356 +                          (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
   9.357 +                          (Type ("fun", Ts1)), t2)
   9.358 +        end
   9.359 +      | Free (s, T) => Free (s, box_type hol_ctxt InExpr T)
   9.360 +      | Var (z as (x, T)) =>
   9.361 +        Var (x, if def then box_var_in_def new_Ts old_Ts orig_t z
   9.362 +                else box_type hol_ctxt InExpr T)
   9.363 +      | Bound _ => t
   9.364 +      | Abs (s, T, t') =>
   9.365 +        Abs (s, T, do_term (T :: new_Ts) (T :: old_Ts) Neut t')
   9.366 +  in do_term [] [] Pos orig_t end
   9.367 +
   9.368 +(** Destruction of constructors **)
   9.369 +
   9.370 +val val_var_prefix = nitpick_prefix ^ "v"
   9.371 +
   9.372 +(* typ list -> int -> int -> int -> term -> term *)
   9.373 +fun fresh_value_var Ts k n j t =
   9.374 +  Var ((val_var_prefix ^ nat_subscript (n - j), k), fastype_of1 (Ts, t))
   9.375 +
   9.376 +(* typ list -> int -> term -> bool *)
   9.377 +fun has_heavy_bounds_or_vars Ts level t =
   9.378 +  let
   9.379 +    (* typ list -> bool *)
   9.380 +    fun aux [] = false
   9.381 +      | aux [T] = is_fun_type T orelse is_pair_type T
   9.382 +      | aux _ = true
   9.383 +  in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
   9.384 +
   9.385 +(* theory -> typ list -> bool -> int -> int -> term -> term list -> term list
   9.386 +   -> term * term list *)
   9.387 +fun pull_out_constr_comb thy Ts relax k level t args seen =
   9.388 +  let val t_comb = list_comb (t, args) in
   9.389 +    case t of
   9.390 +      Const x =>
   9.391 +      if not relax andalso is_constr thy x andalso
   9.392 +         not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso
   9.393 +         has_heavy_bounds_or_vars Ts level t_comb andalso
   9.394 +         not (loose_bvar (t_comb, level)) then
   9.395 +        let
   9.396 +          val (j, seen) = case find_index (curry (op =) t_comb) seen of
   9.397 +                            ~1 => (0, t_comb :: seen)
   9.398 +                          | j => (j, seen)
   9.399 +        in (fresh_value_var Ts k (length seen) j t_comb, seen) end
   9.400 +      else
   9.401 +        (t_comb, seen)
   9.402 +    | _ => (t_comb, seen)
   9.403 +  end
   9.404 +
   9.405 +(* (term -> term) -> typ list -> int -> term list -> term list *)
   9.406 +fun equations_for_pulled_out_constrs mk_eq Ts k seen =
   9.407 +  let val n = length seen in
   9.408 +    map2 (fn j => fn t => mk_eq (fresh_value_var Ts k n j t, t))
   9.409 +         (index_seq 0 n) seen
   9.410 +  end
   9.411 +
   9.412 +(* theory -> bool -> term -> term *)
   9.413 +fun pull_out_universal_constrs thy def t =
   9.414 +  let
   9.415 +    val k = maxidx_of_term t + 1
   9.416 +    (* typ list -> bool -> term -> term list -> term list -> term * term list *)
   9.417 +    fun do_term Ts def t args seen =
   9.418 +      case t of
   9.419 +        (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 =>
   9.420 +        do_eq_or_imp Ts true def t0 t1 t2 seen
   9.421 +      | (t0 as @{const "==>"}) $ t1 $ t2 =>
   9.422 +        if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
   9.423 +      | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
   9.424 +        do_eq_or_imp Ts true def t0 t1 t2 seen
   9.425 +      | (t0 as @{const "op -->"}) $ t1 $ t2 =>
   9.426 +        do_eq_or_imp Ts false def t0 t1 t2 seen
   9.427 +      | Abs (s, T, t') =>
   9.428 +        let val (t', seen) = do_term (T :: Ts) def t' [] seen in
   9.429 +          (list_comb (Abs (s, T, t'), args), seen)
   9.430 +        end
   9.431 +      | t1 $ t2 =>
   9.432 +        let val (t2, seen) = do_term Ts def t2 [] seen in
   9.433 +          do_term Ts def t1 (t2 :: args) seen
   9.434 +        end
   9.435 +      | _ => pull_out_constr_comb thy Ts def k 0 t args seen
   9.436 +    (* typ list -> bool -> bool -> term -> term -> term -> term list
   9.437 +       -> term * term list *)
   9.438 +    and do_eq_or_imp Ts eq def t0 t1 t2 seen =
   9.439 +      let
   9.440 +        val (t2, seen) = if eq andalso def then (t2, seen)
   9.441 +                         else do_term Ts false t2 [] seen
   9.442 +        val (t1, seen) = do_term Ts false t1 [] seen
   9.443 +      in (t0 $ t1 $ t2, seen) end
   9.444 +    val (concl, seen) = do_term [] def t [] []
   9.445 +  in
   9.446 +    Logic.list_implies (equations_for_pulled_out_constrs Logic.mk_equals [] k
   9.447 +                                                         seen, concl)
   9.448 +  end
   9.449 +
   9.450 +(* term -> term -> term *)
   9.451 +fun mk_exists v t =
   9.452 +  HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)
   9.453 +
   9.454 +(* theory -> term -> term *)
   9.455 +fun pull_out_existential_constrs thy t =
   9.456 +  let
   9.457 +    val k = maxidx_of_term t + 1
   9.458 +    (* typ list -> int -> term -> term list -> term list -> term * term list *)
   9.459 +    fun aux Ts num_exists t args seen =
   9.460 +      case t of
   9.461 +        (t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1) =>
   9.462 +        let
   9.463 +          val (t1, seen') = aux (T1 :: Ts) (num_exists + 1) t1 [] []
   9.464 +          val n = length seen'
   9.465 +          (* unit -> term list *)
   9.466 +          fun vars () = map2 (fresh_value_var Ts k n) (index_seq 0 n) seen'
   9.467 +        in
   9.468 +          (equations_for_pulled_out_constrs HOLogic.mk_eq Ts k seen'
   9.469 +           |> List.foldl s_conj t1 |> fold mk_exists (vars ())
   9.470 +           |> curry3 Abs s1 T1 |> curry (op $) t0, seen)
   9.471 +        end
   9.472 +      | t1 $ t2 =>
   9.473 +        let val (t2, seen) = aux Ts num_exists t2 [] seen in
   9.474 +          aux Ts num_exists t1 (t2 :: args) seen
   9.475 +        end
   9.476 +      | Abs (s, T, t') =>
   9.477 +        let
   9.478 +          val (t', seen) = aux (T :: Ts) 0 t' [] (map (incr_boundvars 1) seen)
   9.479 +        in (list_comb (Abs (s, T, t'), args), map (incr_boundvars ~1) seen) end
   9.480 +      | _ =>
   9.481 +        if num_exists > 0 then
   9.482 +          pull_out_constr_comb thy Ts false k num_exists t args seen
   9.483 +        else
   9.484 +          (list_comb (t, args), seen)
   9.485 +  in aux [] 0 t [] [] |> fst end
   9.486 +
   9.487 +(* hol_context -> bool -> term -> term *)
   9.488 +fun destroy_pulled_out_constrs (hol_ctxt as {thy, ...}) axiom t =
   9.489 +  let
   9.490 +    (* styp -> int *)
   9.491 +    val num_occs_of_var =
   9.492 +      fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
   9.493 +                    | _ => I) t (K 0)
   9.494 +    (* bool -> term -> term *)
   9.495 +    fun aux careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =
   9.496 +        aux_eq careful true t0 t1 t2
   9.497 +      | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =
   9.498 +        t0 $ aux false t1 $ aux careful t2
   9.499 +      | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
   9.500 +        aux_eq careful true t0 t1 t2
   9.501 +      | aux careful ((t0 as @{const "op -->"}) $ t1 $ t2) =
   9.502 +        t0 $ aux false t1 $ aux careful t2
   9.503 +      | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')
   9.504 +      | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2
   9.505 +      | aux _ t = t
   9.506 +    (* bool -> bool -> term -> term -> term -> term *)
   9.507 +    and aux_eq careful pass1 t0 t1 t2 =
   9.508 +      ((if careful then
   9.509 +          raise SAME ()
   9.510 +        else if axiom andalso is_Var t2 andalso
   9.511 +                num_occs_of_var (dest_Var t2) = 1 then
   9.512 +          @{const True}
   9.513 +        else case strip_comb t2 of
   9.514 +          (* The first case is not as general as it could be. *)
   9.515 +          (Const (@{const_name PairBox}, _),
   9.516 +                  [Const (@{const_name fst}, _) $ Var z1,
   9.517 +                   Const (@{const_name snd}, _) $ Var z2]) =>
   9.518 +          if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True}
   9.519 +          else raise SAME ()
   9.520 +        | (Const (x as (s, T)), args) =>
   9.521 +          let val arg_Ts = binder_types T in
   9.522 +            if length arg_Ts = length args andalso
   9.523 +               (is_constr thy x orelse s = @{const_name Pair} orelse
   9.524 +                x = (@{const_name Suc}, nat_T --> nat_T)) andalso
   9.525 +               (not careful orelse not (is_Var t1) orelse
   9.526 +                String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
   9.527 +              discriminate_value hol_ctxt x t1 ::
   9.528 +              map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
   9.529 +              |> foldr1 s_conj
   9.530 +            else
   9.531 +              raise SAME ()
   9.532 +          end
   9.533 +        | _ => raise SAME ())
   9.534 +       |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop)
   9.535 +      handle SAME () => if pass1 then aux_eq careful false t0 t2 t1
   9.536 +                        else t0 $ aux false t2 $ aux false t1
   9.537 +    (* styp -> term -> int -> typ -> term -> term *)
   9.538 +    and sel_eq x t n nth_T nth_t =
   9.539 +      HOLogic.eq_const nth_T $ nth_t $ select_nth_constr_arg thy x t n nth_T
   9.540 +      |> aux false
   9.541 +  in aux axiom t end
   9.542 +
   9.543 +(** Destruction of universal and existential equalities **)
   9.544 +
   9.545 +(* term -> term *)
   9.546 +fun curry_assms (@{const "==>"} $ (@{const Trueprop}
   9.547 +                                   $ (@{const "op &"} $ t1 $ t2)) $ t3) =
   9.548 +    curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
   9.549 +  | curry_assms (@{const "==>"} $ t1 $ t2) =
   9.550 +    @{const "==>"} $ curry_assms t1 $ curry_assms t2
   9.551 +  | curry_assms t = t
   9.552 +
   9.553 +(* term -> term *)
   9.554 +val destroy_universal_equalities =
   9.555 +  let
   9.556 +    (* term list -> (indexname * typ) list -> term -> term *)
   9.557 +    fun aux prems zs t =
   9.558 +      case t of
   9.559 +        @{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2
   9.560 +      | _ => Logic.list_implies (rev prems, t)
   9.561 +    (* term list -> (indexname * typ) list -> term -> term -> term *)
   9.562 +    and aux_implies prems zs t1 t2 =
   9.563 +      case t1 of
   9.564 +        Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
   9.565 +      | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') =>
   9.566 +        aux_eq prems zs z t' t1 t2
   9.567 +      | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) =>
   9.568 +        aux_eq prems zs z t' t1 t2
   9.569 +      | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
   9.570 +    (* term list -> (indexname * typ) list -> indexname * typ -> term -> term
   9.571 +       -> term -> term *)
   9.572 +    and aux_eq prems zs z t' t1 t2 =
   9.573 +      if not (member (op =) zs z) andalso
   9.574 +         not (exists_subterm (curry (op =) (Var z)) t') then
   9.575 +        aux prems zs (subst_free [(Var z, t')] t2)
   9.576 +      else
   9.577 +        aux (t1 :: prems) (Term.add_vars t1 zs) t2
   9.578 +  in aux [] [] end
   9.579 +
   9.580 +(* theory -> int -> term list -> term list -> (term * term list) option *)
   9.581 +fun find_bound_assign _ _ _ [] = NONE
   9.582 +  | find_bound_assign thy j seen (t :: ts) =
   9.583 +    let
   9.584 +      (* bool -> term -> term -> (term * term list) option *)
   9.585 +      fun aux pass1 t1 t2 =
   9.586 +        (if loose_bvar1 (t2, j) then
   9.587 +           if pass1 then aux false t2 t1 else raise SAME ()
   9.588 +         else case t1 of
   9.589 +           Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()
   9.590 +         | Const (s, Type ("fun", [T1, T2])) $ Bound j' =>
   9.591 +           if j' = j andalso
   9.592 +              s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then
   9.593 +             SOME (construct_value thy (@{const_name FunBox}, T2 --> T1) [t2],
   9.594 +                   ts @ seen)
   9.595 +           else
   9.596 +             raise SAME ()
   9.597 +         | _ => raise SAME ())
   9.598 +        handle SAME () => find_bound_assign thy j (t :: seen) ts
   9.599 +    in
   9.600 +      case t of
   9.601 +        Const (@{const_name "op ="}, _) $ t1 $ t2 => aux true t1 t2
   9.602 +      | _ => find_bound_assign thy j (t :: seen) ts
   9.603 +    end
   9.604 +
   9.605 +(* int -> term -> term -> term *)
   9.606 +fun subst_one_bound j arg t =
   9.607 +  let
   9.608 +    fun aux (Bound i, lev) =
   9.609 +        if i < lev then raise SAME ()
   9.610 +        else if i = lev then incr_boundvars (lev - j) arg
   9.611 +        else Bound (i - 1)
   9.612 +      | aux (Abs (a, T, body), lev) = Abs (a, T, aux (body, lev + 1))
   9.613 +      | aux (f $ t, lev) =
   9.614 +        (aux (f, lev) $ (aux (t, lev) handle SAME () => t)
   9.615 +         handle SAME () => f $ aux (t, lev))
   9.616 +      | aux _ = raise SAME ()
   9.617 +  in aux (t, j) handle SAME () => t end
   9.618 +
   9.619 +(* theory -> term -> term *)
   9.620 +fun destroy_existential_equalities thy =
   9.621 +  let
   9.622 +    (* string list -> typ list -> term list -> term *)
   9.623 +    fun kill [] [] ts = foldr1 s_conj ts
   9.624 +      | kill (s :: ss) (T :: Ts) ts =
   9.625 +        (case find_bound_assign thy (length ss) [] ts of
   9.626 +           SOME (_, []) => @{const True}
   9.627 +         | SOME (arg_t, ts) =>
   9.628 +           kill ss Ts (map (subst_one_bound (length ss)
   9.629 +                                (incr_bv (~1, length ss + 1, arg_t))) ts)
   9.630 +         | NONE =>
   9.631 +           Const (@{const_name Ex}, (T --> bool_T) --> bool_T)
   9.632 +           $ Abs (s, T, kill ss Ts ts))
   9.633 +      | kill _ _ _ = raise UnequalLengths
   9.634 +    (* string list -> typ list -> term -> term *)
   9.635 +    fun gather ss Ts ((t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1)) =
   9.636 +        gather (ss @ [s1]) (Ts @ [T1]) t1
   9.637 +      | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)
   9.638 +      | gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2
   9.639 +      | gather [] [] t = t
   9.640 +      | gather ss Ts t = kill ss Ts (conjuncts_of (gather [] [] t))
   9.641 +  in gather [] [] end
   9.642 +
   9.643 +(** Skolemization **)
   9.644 +
   9.645 +(* int -> int -> string *)
   9.646 +fun skolem_prefix_for k j =
   9.647 +  skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
   9.648 +
   9.649 +(* hol_context -> int -> term -> term *)
   9.650 +fun skolemize_term_and_more (hol_ctxt as {thy, def_table, skolems, ...})
   9.651 +                            skolem_depth =
   9.652 +  let
   9.653 +    (* int list -> int list *)
   9.654 +    val incrs = map (Integer.add 1)
   9.655 +    (* string list -> typ list -> int list -> int -> polarity -> term -> term *)
   9.656 +    fun aux ss Ts js depth polar t =
   9.657 +      let
   9.658 +        (* string -> typ -> string -> typ -> term -> term *)
   9.659 +        fun do_quantifier quant_s quant_T abs_s abs_T t =
   9.660 +          if not (loose_bvar1 (t, 0)) then
   9.661 +            aux ss Ts js depth polar (incr_boundvars ~1 t)
   9.662 +          else if depth <= skolem_depth andalso
   9.663 +                  is_positive_existential polar quant_s then
   9.664 +            let
   9.665 +              val j = length (!skolems) + 1
   9.666 +              val sko_s = skolem_prefix_for (length js) j ^ abs_s
   9.667 +              val _ = Unsynchronized.change skolems (cons (sko_s, ss))
   9.668 +              val sko_t = list_comb (Const (sko_s, rev Ts ---> abs_T),
   9.669 +                                     map Bound (rev js))
   9.670 +              val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) depth polar t)
   9.671 +            in
   9.672 +              if null js then betapply (abs_t, sko_t)
   9.673 +              else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t $ abs_t
   9.674 +            end
   9.675 +          else
   9.676 +            Const (quant_s, quant_T)
   9.677 +            $ Abs (abs_s, abs_T,
   9.678 +                   if is_higher_order_type abs_T then
   9.679 +                     t
   9.680 +                   else
   9.681 +                     aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js)
   9.682 +                         (depth + 1) polar t)
   9.683 +      in
   9.684 +        case t of
   9.685 +          Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
   9.686 +          do_quantifier s0 T0 s1 T1 t1
   9.687 +        | @{const "==>"} $ t1 $ t2 =>
   9.688 +          @{const "==>"} $ aux ss Ts js depth (flip_polarity polar) t1
   9.689 +          $ aux ss Ts js depth polar t2
   9.690 +        | @{const Pure.conjunction} $ t1 $ t2 =>
   9.691 +          @{const Pure.conjunction} $ aux ss Ts js depth polar t1
   9.692 +          $ aux ss Ts js depth polar t2
   9.693 +        | @{const Trueprop} $ t1 =>
   9.694 +          @{const Trueprop} $ aux ss Ts js depth polar t1
   9.695 +        | @{const Not} $ t1 =>
   9.696 +          @{const Not} $ aux ss Ts js depth (flip_polarity polar) t1
   9.697 +        | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
   9.698 +          do_quantifier s0 T0 s1 T1 t1
   9.699 +        | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
   9.700 +          do_quantifier s0 T0 s1 T1 t1
   9.701 +        | @{const "op &"} $ t1 $ t2 =>
   9.702 +          @{const "op &"} $ aux ss Ts js depth polar t1
   9.703 +          $ aux ss Ts js depth polar t2
   9.704 +        | @{const "op |"} $ t1 $ t2 =>
   9.705 +          @{const "op |"} $ aux ss Ts js depth polar t1
   9.706 +          $ aux ss Ts js depth polar t2
   9.707 +        | @{const "op -->"} $ t1 $ t2 =>
   9.708 +          @{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1
   9.709 +          $ aux ss Ts js depth polar t2
   9.710 +        | (t0 as Const (@{const_name Let}, T0)) $ t1 $ t2 =>
   9.711 +          t0 $ t1 $ aux ss Ts js depth polar t2
   9.712 +        | Const (x as (s, T)) =>
   9.713 +          if is_inductive_pred hol_ctxt x andalso
   9.714 +             not (is_well_founded_inductive_pred hol_ctxt x) then
   9.715 +            let
   9.716 +              val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
   9.717 +              val (pref, connective, set_oper) =
   9.718 +                if gfp then
   9.719 +                  (lbfp_prefix,
   9.720 +                   @{const "op |"},
   9.721 +                   @{const_name upper_semilattice_fun_inst.sup_fun})
   9.722 +                else
   9.723 +                  (ubfp_prefix,
   9.724 +                   @{const "op &"},
   9.725 +                   @{const_name lower_semilattice_fun_inst.inf_fun})
   9.726 +              (* unit -> term *)
   9.727 +              fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x
   9.728 +                           |> aux ss Ts js depth polar
   9.729 +              fun neg () = Const (pref ^ s, T)
   9.730 +            in
   9.731 +              (case polar |> gfp ? flip_polarity of
   9.732 +                 Pos => pos ()
   9.733 +               | Neg => neg ()
   9.734 +               | Neut =>
   9.735 +                 if is_fun_type T then
   9.736 +                   let
   9.737 +                     val ((trunk_arg_Ts, rump_arg_T), body_T) =
   9.738 +                       T |> strip_type |>> split_last
   9.739 +                     val set_T = rump_arg_T --> body_T
   9.740 +                     (* (unit -> term) -> term *)
   9.741 +                     fun app f =
   9.742 +                       list_comb (f (),
   9.743 +                                  map Bound (length trunk_arg_Ts - 1 downto 0))
   9.744 +                   in
   9.745 +                     List.foldr absdummy
   9.746 +                                (Const (set_oper, set_T --> set_T --> set_T)
   9.747 +                                        $ app pos $ app neg) trunk_arg_Ts
   9.748 +                   end
   9.749 +                 else
   9.750 +                   connective $ pos () $ neg ())
   9.751 +            end
   9.752 +          else
   9.753 +            Const x
   9.754 +        | t1 $ t2 =>
   9.755 +          betapply (aux ss Ts [] (skolem_depth + 1) polar t1,
   9.756 +                    aux ss Ts [] depth Neut t2)
   9.757 +        | Abs (s, T, t1) => Abs (s, T, aux ss Ts (incrs js) depth polar t1)
   9.758 +        | _ => t
   9.759 +      end
   9.760 +  in aux [] [] [] 0 Pos end
   9.761 +
   9.762 +(** Function specialization **)
   9.763 +
   9.764 +(* term -> term list *)
   9.765 +fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2
   9.766 +  | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
   9.767 +  | params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) =
   9.768 +    snd (strip_comb t1)
   9.769 +  | params_in_equation _ = []
   9.770 +
   9.771 +(* styp -> styp -> int list -> term list -> term list -> term -> term *)
   9.772 +fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t =
   9.773 +  let
   9.774 +    val k = fold Integer.max (map maxidx_of_term (fixed_args @ extra_args)) 0
   9.775 +            + 1
   9.776 +    val t = map_aterms (fn Var ((s, i), T) => Var ((s, k + i), T) | t' => t') t
   9.777 +    val fixed_params = filter_indices fixed_js (params_in_equation t)
   9.778 +    (* term list -> term -> term *)
   9.779 +    fun aux args (Abs (s, T, t)) = list_comb (Abs (s, T, aux [] t), args)
   9.780 +      | aux args (t1 $ t2) = aux (aux [] t2 :: args) t1
   9.781 +      | aux args t =
   9.782 +        if t = Const x then
   9.783 +          list_comb (Const x', extra_args @ filter_out_indices fixed_js args)
   9.784 +        else
   9.785 +          let val j = find_index (curry (op =) t) fixed_params in
   9.786 +            list_comb (if j >= 0 then nth fixed_args j else t, args)
   9.787 +          end
   9.788 +  in aux [] t end
   9.789 +
   9.790 +(* hol_context -> styp -> (int * term option) list *)
   9.791 +fun static_args_in_term ({ersatz_table, ...} : hol_context) x t =
   9.792 +  let
   9.793 +    (* term -> term list -> term list -> term list list *)
   9.794 +    fun fun_calls (Abs (_, _, t)) _ = fun_calls t []
   9.795 +      | fun_calls (t1 $ t2) args = fun_calls t2 [] #> fun_calls t1 (t2 :: args)
   9.796 +      | fun_calls t args =
   9.797 +        (case t of
   9.798 +           Const (x' as (s', T')) =>
   9.799 +           x = x' orelse (case AList.lookup (op =) ersatz_table s' of
   9.800 +                            SOME s'' => x = (s'', T')
   9.801 +                          | NONE => false)
   9.802 +         | _ => false) ? cons args
   9.803 +    (* term list list -> term list list -> term list -> term list list *)
   9.804 +    fun call_sets [] [] vs = [vs]
   9.805 +      | call_sets [] uss vs = vs :: call_sets uss [] []
   9.806 +      | call_sets ([] :: _) _ _ = []
   9.807 +      | call_sets ((t :: ts) :: tss) uss vs =
   9.808 +        OrdList.insert TermOrd.term_ord t vs |> call_sets tss (ts :: uss)
   9.809 +    val sets = call_sets (fun_calls t [] []) [] []
   9.810 +    val indexed_sets = sets ~~ (index_seq 0 (length sets))
   9.811 +  in
   9.812 +    fold_rev (fn (set, j) =>
   9.813 +                 case set of
   9.814 +                   [Var _] => AList.lookup (op =) indexed_sets set = SOME j
   9.815 +                              ? cons (j, NONE)
   9.816 +                 | [t as Const _] => cons (j, SOME t)
   9.817 +                 | [t as Free _] => cons (j, SOME t)
   9.818 +                 | _ => I) indexed_sets []
   9.819 +  end
   9.820 +(* hol_context -> styp -> term list -> (int * term option) list *)
   9.821 +fun static_args_in_terms hol_ctxt x =
   9.822 +  map (static_args_in_term hol_ctxt x)
   9.823 +  #> fold1 (OrdList.inter (prod_ord int_ord (option_ord TermOrd.term_ord)))
   9.824 +
   9.825 +(* (int * term option) list -> (int * term) list -> int list *)
   9.826 +fun overlapping_indices [] _ = []
   9.827 +  | overlapping_indices _ [] = []
   9.828 +  | overlapping_indices (ps1 as (j1, t1) :: ps1') (ps2 as (j2, t2) :: ps2') =
   9.829 +    if j1 < j2 then overlapping_indices ps1' ps2
   9.830 +    else if j1 > j2 then overlapping_indices ps1 ps2'
   9.831 +    else overlapping_indices ps1' ps2' |> the_default t2 t1 = t2 ? cons j1
   9.832 +
   9.833 +(* typ list -> term -> bool *)
   9.834 +fun is_eligible_arg Ts t =
   9.835 +  let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in
   9.836 +    null bad_Ts orelse
   9.837 +    (is_higher_order_type (fastype_of1 (Ts, t)) andalso
   9.838 +     forall (not o is_higher_order_type) bad_Ts)
   9.839 +  end
   9.840 +
   9.841 +(* int -> string *)
   9.842 +fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep
   9.843 +
   9.844 +(* If a constant's definition is picked up deeper than this threshold, we
   9.845 +   prevent excessive specialization by not specializing it. *)
   9.846 +val special_max_depth = 20
   9.847 +
   9.848 +val bound_var_prefix = "b"
   9.849 +
   9.850 +(* hol_context -> int -> term -> term *)
   9.851 +fun specialize_consts_in_term (hol_ctxt as {thy, specialize, simp_table,
   9.852 +                                            special_funs, ...}) depth t =
   9.853 +  if not specialize orelse depth > special_max_depth then
   9.854 +    t
   9.855 +  else
   9.856 +    let
   9.857 +      val blacklist = if depth = 0 then []
   9.858 +                      else case term_under_def t of Const x => [x] | _ => []
   9.859 +      (* term list -> typ list -> term -> term *)
   9.860 +      fun aux args Ts (Const (x as (s, T))) =
   9.861 +          ((if not (member (op =) blacklist x) andalso not (null args) andalso
   9.862 +               not (String.isPrefix special_prefix s) andalso
   9.863 +               is_equational_fun hol_ctxt x then
   9.864 +              let
   9.865 +                val eligible_args = filter (is_eligible_arg Ts o snd)
   9.866 +                                           (index_seq 0 (length args) ~~ args)
   9.867 +                val _ = not (null eligible_args) orelse raise SAME ()
   9.868 +                val old_axs = equational_fun_axioms hol_ctxt x
   9.869 +                              |> map (destroy_existential_equalities thy)
   9.870 +                val static_params = static_args_in_terms hol_ctxt x old_axs
   9.871 +                val fixed_js = overlapping_indices static_params eligible_args
   9.872 +                val _ = not (null fixed_js) orelse raise SAME ()
   9.873 +                val fixed_args = filter_indices fixed_js args
   9.874 +                val vars = fold Term.add_vars fixed_args []
   9.875 +                           |> sort (TermOrd.fast_indexname_ord o pairself fst)
   9.876 +                val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js))
   9.877 +                                    fixed_args []
   9.878 +                               |> sort int_ord
   9.879 +                val live_args = filter_out_indices fixed_js args
   9.880 +                val extra_args = map Var vars @ map Bound bound_js @ live_args
   9.881 +                val extra_Ts = map snd vars @ filter_indices bound_js Ts
   9.882 +                val k = maxidx_of_term t + 1
   9.883 +                (* int -> term *)
   9.884 +                fun var_for_bound_no j =
   9.885 +                  Var ((bound_var_prefix ^
   9.886 +                        nat_subscript (find_index (curry (op =) j) bound_js
   9.887 +                                       + 1), k),
   9.888 +                       nth Ts j)
   9.889 +                val fixed_args_in_axiom =
   9.890 +                  map (curry subst_bounds
   9.891 +                             (map var_for_bound_no (index_seq 0 (length Ts))))
   9.892 +                      fixed_args
   9.893 +              in
   9.894 +                case AList.lookup (op =) (!special_funs)
   9.895 +                                  (x, fixed_js, fixed_args_in_axiom) of
   9.896 +                  SOME x' => list_comb (Const x', extra_args)
   9.897 +                | NONE =>
   9.898 +                  let
   9.899 +                    val extra_args_in_axiom =
   9.900 +                      map Var vars @ map var_for_bound_no bound_js
   9.901 +                    val x' as (s', _) =
   9.902 +                      (special_prefix_for (length (!special_funs) + 1) ^ s,
   9.903 +                       extra_Ts @ filter_out_indices fixed_js (binder_types T)
   9.904 +                       ---> body_type T)
   9.905 +                    val new_axs =
   9.906 +                      map (specialize_fun_axiom x x' fixed_js
   9.907 +                               fixed_args_in_axiom extra_args_in_axiom) old_axs
   9.908 +                    val _ =
   9.909 +                      Unsynchronized.change special_funs
   9.910 +                          (cons ((x, fixed_js, fixed_args_in_axiom), x'))
   9.911 +                    val _ = add_simps simp_table s' new_axs
   9.912 +                  in list_comb (Const x', extra_args) end
   9.913 +              end
   9.914 +            else
   9.915 +              raise SAME ())
   9.916 +           handle SAME () => list_comb (Const x, args))
   9.917 +        | aux args Ts (Abs (s, T, t)) =
   9.918 +          list_comb (Abs (s, T, aux [] (T :: Ts) t), args)
   9.919 +        | aux args Ts (t1 $ t2) = aux (aux [] Ts t2 :: args) Ts t1
   9.920 +        | aux args _ t = list_comb (t, args)
   9.921 +    in aux [] [] t end
   9.922 +
   9.923 +type special_triple = int list * term list * styp
   9.924 +
   9.925 +val cong_var_prefix = "c"
   9.926 +
   9.927 +(* styp -> special_triple -> special_triple -> term *)
   9.928 +fun special_congruence_axiom (s, T) (js1, ts1, x1) (js2, ts2, x2) =
   9.929 +  let
   9.930 +    val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2)
   9.931 +    val Ts = binder_types T
   9.932 +    val max_j = fold (fold Integer.max) [js1, js2] ~1
   9.933 +    val (eqs, (args1, args2)) =
   9.934 +      fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j)
   9.935 +                                  (js1 ~~ ts1, js2 ~~ ts2) of
   9.936 +                      (SOME t1, SOME t2) => apfst (cons (t1, t2))
   9.937 +                    | (SOME t1, NONE) => apsnd (apsnd (cons t1))
   9.938 +                    | (NONE, SOME t2) => apsnd (apfst (cons t2))
   9.939 +                    | (NONE, NONE) =>
   9.940 +                      let val v = Var ((cong_var_prefix ^ nat_subscript j, 0),
   9.941 +                                       nth Ts j) in
   9.942 +                        apsnd (pairself (cons v))
   9.943 +                      end) (max_j downto 0) ([], ([], []))
   9.944 +  in
   9.945 +    Logic.list_implies (eqs |> filter_out (op =) |> distinct (op =)
   9.946 +                            |> map Logic.mk_equals,
   9.947 +                        Logic.mk_equals (list_comb (Const x1, bounds1 @ args1),
   9.948 +                                         list_comb (Const x2, bounds2 @ args2)))
   9.949 +    |> Refute.close_form (* TODO: needed? *)
   9.950 +  end
   9.951 +
   9.952 +(* hol_context -> styp list -> term list *)
   9.953 +fun special_congruence_axioms (hol_ctxt as {special_funs, ...}) xs =
   9.954 +  let
   9.955 +    val groups =
   9.956 +      !special_funs
   9.957 +      |> map (fn ((x, js, ts), x') => (x, (js, ts, x')))
   9.958 +      |> AList.group (op =)
   9.959 +      |> filter_out (is_equational_fun_surely_complete hol_ctxt o fst)
   9.960 +      |> map (fn (x, zs) => (x, zs |> member (op =) xs x ? cons ([], [], x)))
   9.961 +    (* special_triple -> int *)
   9.962 +    fun generality (js, _, _) = ~(length js)
   9.963 +    (* special_triple -> special_triple -> bool *)
   9.964 +    fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
   9.965 +      x1 <> x2 andalso OrdList.subset (prod_ord int_ord TermOrd.term_ord)
   9.966 +                                      (j2 ~~ t2, j1 ~~ t1)
   9.967 +    (* styp -> special_triple list -> special_triple list -> special_triple list
   9.968 +       -> term list -> term list *)
   9.969 +    fun do_pass_1 _ [] [_] [_] = I
   9.970 +      | do_pass_1 x skipped _ [] = do_pass_2 x skipped
   9.971 +      | do_pass_1 x skipped all (z :: zs) =
   9.972 +        case filter (is_more_specific z) all
   9.973 +             |> sort (int_ord o pairself generality) of
   9.974 +          [] => do_pass_1 x (z :: skipped) all zs
   9.975 +        | (z' :: _) => cons (special_congruence_axiom x z z')
   9.976 +                       #> do_pass_1 x skipped all zs
   9.977 +    (* styp -> special_triple list -> term list -> term list *)
   9.978 +    and do_pass_2 _ [] = I
   9.979 +      | do_pass_2 x (z :: zs) =
   9.980 +        fold (cons o special_congruence_axiom x z) zs #> do_pass_2 x zs
   9.981 +  in fold (fn (x, zs) => do_pass_1 x [] zs zs) groups [] end
   9.982 +
   9.983 +(** Axiom selection **)
   9.984 +
   9.985 +(* Similar to "Refute.specialize_type" but returns all matches rather than only
   9.986 +   the first (preorder) match. *)
   9.987 +(* theory -> styp -> term -> term list *)
   9.988 +fun multi_specialize_type thy slack (x as (s, T)) t =
   9.989 +  let
   9.990 +    (* term -> (typ * term) list -> (typ * term) list *)
   9.991 +    fun aux (Const (s', T')) ys =
   9.992 +        if s = s' then
   9.993 +          ys |> (if AList.defined (op =) ys T' then
   9.994 +                   I
   9.995 +                 else
   9.996 +                  cons (T', Refute.monomorphic_term
   9.997 +                                (Sign.typ_match thy (T', T) Vartab.empty) t)
   9.998 +                  handle Type.TYPE_MATCH => I
   9.999 +                       | Refute.REFUTE _ =>
  9.1000 +                         if slack then
  9.1001 +                           I
  9.1002 +                         else
  9.1003 +                           raise NOT_SUPPORTED ("too much polymorphism in \
  9.1004 +                                                \axiom involving " ^ quote s))
  9.1005 +        else
  9.1006 +          ys
  9.1007 +      | aux _ ys = ys
  9.1008 +  in map snd (fold_aterms aux t []) end
  9.1009 +
  9.1010 +(* theory -> bool -> const_table -> styp -> term list *)
  9.1011 +fun nondef_props_for_const thy slack table (x as (s, _)) =
  9.1012 +  these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)
  9.1013 +
  9.1014 +(* 'a Symtab.table -> 'a list *)
  9.1015 +fun all_table_entries table = Symtab.fold (append o snd) table []
  9.1016 +(* const_table -> string -> const_table *)
  9.1017 +fun extra_table table s = Symtab.make [(s, all_table_entries table)]
  9.1018 +
  9.1019 +(* int -> term -> term *)
  9.1020 +fun eval_axiom_for_term j t =
  9.1021 +  Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t)
  9.1022 +
  9.1023 +(* term -> bool *)
  9.1024 +val is_trivial_equation = the_default false o try (op aconv o Logic.dest_equals)
  9.1025 +
  9.1026 +(* Prevents divergence in case of cyclic or infinite axiom dependencies. *)
  9.1027 +val axioms_max_depth = 255
  9.1028 +
  9.1029 +(* hol_context -> term -> (term list * term list) * (bool * bool) *)
  9.1030 +fun axioms_for_term
  9.1031 +        (hol_ctxt as {thy, max_bisim_depth, user_axioms, fast_descrs, evals,
  9.1032 +                      def_table, nondef_table, user_nondefs, ...}) t =
  9.1033 +  let
  9.1034 +    type accumulator = styp list * (term list * term list)
  9.1035 +    (* (term list * term list -> term list)
  9.1036 +       -> ((term list -> term list) -> term list * term list
  9.1037 +           -> term list * term list)
  9.1038 +       -> int -> term -> accumulator -> accumulator *)
  9.1039 +    fun add_axiom get app depth t (accum as (xs, axs)) =
  9.1040 +      let
  9.1041 +        val t = t |> unfold_defs_in_term hol_ctxt
  9.1042 +                  |> skolemize_term_and_more hol_ctxt ~1
  9.1043 +      in
  9.1044 +        if is_trivial_equation t then
  9.1045 +          accum
  9.1046 +        else
  9.1047 +          let val t' = t |> specialize_consts_in_term hol_ctxt depth in
  9.1048 +            if exists (member (op aconv) (get axs)) [t, t'] then accum
  9.1049 +            else add_axioms_for_term (depth + 1) t' (xs, app (cons t') axs)
  9.1050 +          end
  9.1051 +      end
  9.1052 +    (* int -> term -> accumulator -> accumulator *)
  9.1053 +    and add_def_axiom depth = add_axiom fst apfst depth
  9.1054 +    and add_nondef_axiom depth = add_axiom snd apsnd depth
  9.1055 +    and add_maybe_def_axiom depth t =
  9.1056 +      (if head_of t <> @{const "==>"} then add_def_axiom
  9.1057 +       else add_nondef_axiom) depth t
  9.1058 +    and add_eq_axiom depth t =
  9.1059 +      (if is_constr_pattern_formula thy t then add_def_axiom
  9.1060 +       else add_nondef_axiom) depth t
  9.1061 +    (* int -> term -> accumulator -> accumulator *)
  9.1062 +    and add_axioms_for_term depth t (accum as (xs, axs)) =
  9.1063 +      case t of
  9.1064 +        t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
  9.1065 +      | Const (x as (s, T)) =>
  9.1066 +        (if member (op =) xs x orelse is_built_in_const fast_descrs x then
  9.1067 +           accum
  9.1068 +         else
  9.1069 +           let val accum as (xs, _) = (x :: xs, axs) in
  9.1070 +             if depth > axioms_max_depth then
  9.1071 +               raise TOO_LARGE ("Nitpick_Preproc.axioms_for_term.\
  9.1072 +                                \add_axioms_for_term",
  9.1073 +                                "too many nested axioms (" ^
  9.1074 +                                string_of_int depth ^ ")")
  9.1075 +             else if Refute.is_const_of_class thy x then
  9.1076 +               let
  9.1077 +                 val class = Logic.class_of_const s
  9.1078 +                 val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]),
  9.1079 +                                                   class)
  9.1080 +                 val ax1 = try (Refute.specialize_type thy x) of_class
  9.1081 +                 val ax2 = Option.map (Refute.specialize_type thy x o snd)
  9.1082 +                                      (Refute.get_classdef thy class)
  9.1083 +               in
  9.1084 +                 fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
  9.1085 +                      accum
  9.1086 +               end
  9.1087 +             else if is_constr thy x then
  9.1088 +               accum
  9.1089 +             else if is_equational_fun hol_ctxt x then
  9.1090 +               fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)
  9.1091 +                    accum
  9.1092 +             else if is_abs_fun thy x then
  9.1093 +               if is_quot_type thy (range_type T) then
  9.1094 +                 raise NOT_SUPPORTED "\"Abs_\" function of quotient type"
  9.1095 +               else
  9.1096 +                 accum |> fold (add_nondef_axiom depth)
  9.1097 +                               (nondef_props_for_const thy false nondef_table x)
  9.1098 +                       |> is_funky_typedef thy (range_type T)
  9.1099 +                          ? fold (add_maybe_def_axiom depth)
  9.1100 +                                 (nondef_props_for_const thy true
  9.1101 +                                                    (extra_table def_table s) x)
  9.1102 +             else if is_rep_fun thy x then
  9.1103 +               if is_quot_type thy (domain_type T) then
  9.1104 +                 raise NOT_SUPPORTED "\"Rep_\" function of quotient type"
  9.1105 +               else
  9.1106 +                 accum |> fold (add_nondef_axiom depth)
  9.1107 +                               (nondef_props_for_const thy false nondef_table x)
  9.1108 +                       |> is_funky_typedef thy (range_type T)
  9.1109 +                          ? fold (add_maybe_def_axiom depth)
  9.1110 +                                 (nondef_props_for_const thy true
  9.1111 +                                                    (extra_table def_table s) x)
  9.1112 +                       |> add_axioms_for_term depth
  9.1113 +                                              (Const (mate_of_rep_fun thy x))
  9.1114 +                       |> fold (add_def_axiom depth)
  9.1115 +                               (inverse_axioms_for_rep_fun thy x)
  9.1116 +             else
  9.1117 +               accum |> user_axioms <> SOME false
  9.1118 +                        ? fold (add_nondef_axiom depth)
  9.1119 +                               (nondef_props_for_const thy false nondef_table x)
  9.1120 +           end)
  9.1121 +        |> add_axioms_for_type depth T
  9.1122 +      | Free (_, T) => add_axioms_for_type depth T accum
  9.1123 +      | Var (_, T) => add_axioms_for_type depth T accum
  9.1124 +      | Bound _ => accum
  9.1125 +      | Abs (_, T, t) => accum |> add_axioms_for_term depth t
  9.1126 +                               |> add_axioms_for_type depth T
  9.1127 +    (* int -> typ -> accumulator -> accumulator *)
  9.1128 +    and add_axioms_for_type depth T =
  9.1129 +      case T of
  9.1130 +        Type ("fun", Ts) => fold (add_axioms_for_type depth) Ts
  9.1131 +      | Type ("*", Ts) => fold (add_axioms_for_type depth) Ts
  9.1132 +      | @{typ prop} => I
  9.1133 +      | @{typ bool} => I
  9.1134 +      | @{typ unit} => I
  9.1135 +      | TFree (_, S) => add_axioms_for_sort depth T S
  9.1136 +      | TVar (_, S) => add_axioms_for_sort depth T S
  9.1137 +      | Type (z as (s, Ts)) =>
  9.1138 +        fold (add_axioms_for_type depth) Ts
  9.1139 +        #> (if is_pure_typedef thy T then
  9.1140 +              fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
  9.1141 +            else if is_quot_type thy T then
  9.1142 +              fold (add_def_axiom depth) (optimized_quot_type_axioms thy z)
  9.1143 +            else if max_bisim_depth >= 0 andalso is_codatatype thy T then
  9.1144 +              fold (add_maybe_def_axiom depth)
  9.1145 +                   (codatatype_bisim_axioms hol_ctxt T)
  9.1146 +            else
  9.1147 +              I)
  9.1148 +    (* int -> typ -> sort -> accumulator -> accumulator *)
  9.1149 +    and add_axioms_for_sort depth T S =
  9.1150 +      let
  9.1151 +        val supers = Sign.complete_sort thy S
  9.1152 +        val class_axioms =
  9.1153 +          maps (fn class => map prop_of (AxClass.get_info thy class |> #axioms
  9.1154 +                                         handle ERROR _ => [])) supers
  9.1155 +        val monomorphic_class_axioms =
  9.1156 +          map (fn t => case Term.add_tvars t [] of
  9.1157 +                         [] => t
  9.1158 +                       | [(x, S)] =>
  9.1159 +                         Refute.monomorphic_term (Vartab.make [(x, (S, T))]) t
  9.1160 +                       | _ => raise TERM ("Nitpick_Preproc.axioms_for_term.\
  9.1161 +                                          \add_axioms_for_sort", [t]))
  9.1162 +              class_axioms
  9.1163 +      in fold (add_nondef_axiom depth) monomorphic_class_axioms end
  9.1164 +    val (mono_user_nondefs, poly_user_nondefs) =
  9.1165 +      List.partition (null o Term.hidden_polymorphism) user_nondefs
  9.1166 +    val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals))
  9.1167 +                           evals
  9.1168 +    val (xs, (defs, nondefs)) =
  9.1169 +      ([], ([], [])) |> add_axioms_for_term 1 t 
  9.1170 +                     |> fold_rev (add_def_axiom 1) eval_axioms
  9.1171 +                     |> user_axioms = SOME true
  9.1172 +                        ? fold (add_nondef_axiom 1) mono_user_nondefs
  9.1173 +    val defs = defs @ special_congruence_axioms hol_ctxt xs
  9.1174 +  in
  9.1175 +    ((defs, nondefs), (user_axioms = SOME true orelse null mono_user_nondefs,
  9.1176 +                       null poly_user_nondefs))
  9.1177 +  end
  9.1178 +
  9.1179 +(** Simplification of constructor/selector terms **)
  9.1180 +
  9.1181 +(* theory -> term -> term *)
  9.1182 +fun simplify_constrs_and_sels thy t =
  9.1183 +  let
  9.1184 +    (* term -> int -> term *)
  9.1185 +    fun is_nth_sel_on t' n (Const (s, _) $ t) =
  9.1186 +        (t = t' andalso is_sel_like_and_no_discr s andalso
  9.1187 +         sel_no_from_name s = n)
  9.1188 +      | is_nth_sel_on _ _ _ = false
  9.1189 +    (* term -> term list -> term *)
  9.1190 +    fun do_term (Const (@{const_name Rep_Frac}, _)
  9.1191 +                 $ (Const (@{const_name Abs_Frac}, _) $ t1)) [] = do_term t1 []
  9.1192 +      | do_term (Const (@{const_name Abs_Frac}, _)
  9.1193 +                 $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 []
  9.1194 +      | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)
  9.1195 +      | do_term (t as Const (x as (s, T))) (args as _ :: _) =
  9.1196 +        ((if is_constr_like thy x then
  9.1197 +            if length args = num_binder_types T then
  9.1198 +              case hd args of
  9.1199 +                Const (x' as (_, T')) $ t' =>
  9.1200 +                if domain_type T' = body_type T andalso
  9.1201 +                   forall (uncurry (is_nth_sel_on t'))
  9.1202 +                          (index_seq 0 (length args) ~~ args) then
  9.1203 +                  t'
  9.1204 +                else
  9.1205 +                  raise SAME ()
  9.1206 +              | _ => raise SAME ()
  9.1207 +            else
  9.1208 +              raise SAME ()
  9.1209 +          else if is_sel_like_and_no_discr s then
  9.1210 +            case strip_comb (hd args) of
  9.1211 +              (Const (x' as (s', T')), ts') =>
  9.1212 +              if is_constr_like thy x' andalso
  9.1213 +                 constr_name_for_sel_like s = s' andalso
  9.1214 +                 not (exists is_pair_type (binder_types T')) then
  9.1215 +                list_comb (nth ts' (sel_no_from_name s), tl args)
  9.1216 +              else
  9.1217 +                raise SAME ()
  9.1218 +            | _ => raise SAME ()
  9.1219 +          else
  9.1220 +            raise SAME ())
  9.1221 +         handle SAME () => betapplys (t, args))
  9.1222 +      | do_term (Abs (s, T, t')) args =
  9.1223 +        betapplys (Abs (s, T, do_term t' []), args)
  9.1224 +      | do_term t args = betapplys (t, args)
  9.1225 +  in do_term t [] end
  9.1226 +
  9.1227 +(** Quantifier massaging: Distributing quantifiers **)
  9.1228 +
  9.1229 +(* term -> term *)
  9.1230 +fun distribute_quantifiers t =
  9.1231 +  case t of
  9.1232 +    (t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) =>
  9.1233 +    (case t1 of
  9.1234 +       (t10 as @{const "op &"}) $ t11 $ t12 =>
  9.1235 +       t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
  9.1236 +           $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
  9.1237 +     | (t10 as @{const Not}) $ t11 =>
  9.1238 +       t10 $ distribute_quantifiers (Const (@{const_name Ex}, T0)
  9.1239 +                                     $ Abs (s, T1, t11))
  9.1240 +     | t1 =>
  9.1241 +       if not (loose_bvar1 (t1, 0)) then
  9.1242 +         distribute_quantifiers (incr_boundvars ~1 t1)
  9.1243 +       else
  9.1244 +         t0 $ Abs (s, T1, distribute_quantifiers t1))
  9.1245 +  | (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) =>
  9.1246 +    (case distribute_quantifiers t1 of
  9.1247 +       (t10 as @{const "op |"}) $ t11 $ t12 =>
  9.1248 +       t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
  9.1249 +           $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
  9.1250 +     | (t10 as @{const "op -->"}) $ t11 $ t12 =>
  9.1251 +       t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
  9.1252 +                                     $ Abs (s, T1, t11))
  9.1253 +           $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
  9.1254 +     | (t10 as @{const Not}) $ t11 =>
  9.1255 +       t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
  9.1256 +                                     $ Abs (s, T1, t11))
  9.1257 +     | t1 =>
  9.1258 +       if not (loose_bvar1 (t1, 0)) then
  9.1259 +         distribute_quantifiers (incr_boundvars ~1 t1)
  9.1260 +       else
  9.1261 +         t0 $ Abs (s, T1, distribute_quantifiers t1))
  9.1262 +  | t1 $ t2 => distribute_quantifiers t1 $ distribute_quantifiers t2
  9.1263 +  | Abs (s, T, t') => Abs (s, T, distribute_quantifiers t')
  9.1264 +  | _ => t
  9.1265 +
  9.1266 +(** Quantifier massaging: Pushing quantifiers inward **)
  9.1267 +
  9.1268 +(* int -> int -> (int -> int) -> term -> term *)
  9.1269 +fun renumber_bounds j n f t =
  9.1270 +  case t of
  9.1271 +    t1 $ t2 => renumber_bounds j n f t1 $ renumber_bounds j n f t2
  9.1272 +  | Abs (s, T, t') => Abs (s, T, renumber_bounds (j + 1) n f t')
  9.1273 +  | Bound j' =>
  9.1274 +    Bound (if j' >= j andalso j' < j + n then f (j' - j) + j else j')
  9.1275 +  | _ => t
  9.1276 +
  9.1277 +(* Maximum number of quantifiers in a cluster for which the exponential
  9.1278 +   algorithm is used. Larger clusters use a heuristic inspired by Claessen &
  9.1279 +   Sörensson's polynomial binary splitting procedure (p. 5 of their MODEL 2003
  9.1280 +   paper). *)
  9.1281 +val quantifier_cluster_threshold = 7
  9.1282 +
  9.1283 +(* theory -> term -> term *)
  9.1284 +fun push_quantifiers_inward thy =
  9.1285 +  let
  9.1286 +    (* string -> string list -> typ list -> term -> term *)
  9.1287 +    fun aux quant_s ss Ts t =
  9.1288 +      (case t of
  9.1289 +         (t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) =>
  9.1290 +         if s0 = quant_s then
  9.1291 +           aux s0 (s1 :: ss) (T1 :: Ts) t1
  9.1292 +         else if quant_s = "" andalso
  9.1293 +                 (s0 = @{const_name All} orelse s0 = @{const_name Ex}) then
  9.1294 +           aux s0 [s1] [T1] t1
  9.1295 +         else
  9.1296 +           raise SAME ()
  9.1297 +       | _ => raise SAME ())
  9.1298 +      handle SAME () =>
  9.1299 +             case t of
  9.1300 +               t1 $ t2 =>
  9.1301 +               if quant_s = "" then
  9.1302 +                 aux "" [] [] t1 $ aux "" [] [] t2
  9.1303 +               else
  9.1304 +                 let
  9.1305 +                   val typical_card = 4
  9.1306 +                   (* ('a -> ''b list) -> 'a list -> ''b list *)
  9.1307 +                   fun big_union proj ps =
  9.1308 +                     fold (fold (insert (op =)) o proj) ps []
  9.1309 +                   val (ts, connective) = strip_any_connective t
  9.1310 +                   val T_costs =
  9.1311 +                     map (bounded_card_of_type 65536 typical_card []) Ts
  9.1312 +                   val t_costs = map size_of_term ts
  9.1313 +                   val num_Ts = length Ts
  9.1314 +                   (* int -> int *)
  9.1315 +                   val flip = curry (op -) (num_Ts - 1)
  9.1316 +                   val t_boundss = map (map flip o loose_bnos) ts
  9.1317 +                   (* (int list * int) list -> int list
  9.1318 +                      -> (int list * int) list *)
  9.1319 +                   fun merge costly_boundss [] = costly_boundss
  9.1320 +                     | merge costly_boundss (j :: js) =
  9.1321 +                       let
  9.1322 +                         val (yeas, nays) =
  9.1323 +                           List.partition (fn (bounds, _) =>
  9.1324 +                                              member (op =) bounds j)
  9.1325 +                                          costly_boundss
  9.1326 +                         val yeas_bounds = big_union fst yeas
  9.1327 +                         val yeas_cost = Integer.sum (map snd yeas)
  9.1328 +                                         * nth T_costs j
  9.1329 +                       in merge ((yeas_bounds, yeas_cost) :: nays) js end
  9.1330 +                   (* (int list * int) list -> int list -> int *)
  9.1331 +                   val cost = Integer.sum o map snd oo merge
  9.1332 +                   (* (int list * int) list -> int list -> int list *)
  9.1333 +                   fun heuristically_best_permutation _ [] = []
  9.1334 +                     | heuristically_best_permutation costly_boundss js =
  9.1335 +                       let
  9.1336 +                         val (costly_boundss, (j, js)) =
  9.1337 +                           js |> map (`(merge costly_boundss o single))
  9.1338 +                              |> sort (int_ord
  9.1339 +                                       o pairself (Integer.sum o map snd o fst))
  9.1340 +                              |> split_list |>> hd ||> pairf hd tl
  9.1341 +                       in
  9.1342 +                         j :: heuristically_best_permutation costly_boundss js
  9.1343 +                       end
  9.1344 +                   val js =
  9.1345 +                     if length Ts <= quantifier_cluster_threshold then
  9.1346 +                       all_permutations (index_seq 0 num_Ts)
  9.1347 +                       |> map (`(cost (t_boundss ~~ t_costs)))
  9.1348 +                       |> sort (int_ord o pairself fst) |> hd |> snd
  9.1349 +                     else
  9.1350 +                       heuristically_best_permutation (t_boundss ~~ t_costs)
  9.1351 +                                                      (index_seq 0 num_Ts)
  9.1352 +                   val back_js = map (fn j => find_index (curry (op =) j) js)
  9.1353 +                                     (index_seq 0 num_Ts)
  9.1354 +                   val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip))
  9.1355 +                                ts
  9.1356 +                   (* (term * int list) list -> term *)
  9.1357 +                   fun mk_connection [] =
  9.1358 +                       raise ARG ("Nitpick_Preproc.push_quantifiers_inward.aux.\
  9.1359 +                                  \mk_connection", "")
  9.1360 +                     | mk_connection ts_cum_bounds =
  9.1361 +                       ts_cum_bounds |> map fst
  9.1362 +                       |> foldr1 (fn (t1, t2) => connective $ t1 $ t2)
  9.1363 +                   (* (term * int list) list -> int list -> term *)
  9.1364 +                   fun build ts_cum_bounds [] = ts_cum_bounds |> mk_connection
  9.1365 +                     | build ts_cum_bounds (j :: js) =
  9.1366 +                       let
  9.1367 +                         val (yeas, nays) =
  9.1368 +                           List.partition (fn (_, bounds) =>
  9.1369 +                                              member (op =) bounds j)
  9.1370 +                                          ts_cum_bounds
  9.1371 +                           ||> map (apfst (incr_boundvars ~1))
  9.1372 +                       in
  9.1373 +                         if null yeas then
  9.1374 +                           build nays js
  9.1375 +                         else
  9.1376 +                           let val T = nth Ts (flip j) in
  9.1377 +                             build ((Const (quant_s, (T --> bool_T) --> bool_T)
  9.1378 +                                     $ Abs (nth ss (flip j), T,
  9.1379 +                                            mk_connection yeas),
  9.1380 +                                      big_union snd yeas) :: nays) js
  9.1381 +                           end
  9.1382 +                       end
  9.1383 +                 in build (ts ~~ t_boundss) js end
  9.1384 +             | Abs (s, T, t') => Abs (s, T, aux "" [] [] t')
  9.1385 +             | _ => t
  9.1386 +  in aux "" [] [] end
  9.1387 +
  9.1388 +(** Preprocessor entry point **)
  9.1389 +
  9.1390 +(* hol_context -> term -> ((term list * term list) * (bool * bool)) * term *)
  9.1391 +fun preprocess_term (hol_ctxt as {thy, binary_ints, destroy_constrs, boxes,
  9.1392 +                                  skolemize, uncurry, ...}) t =
  9.1393 +  let
  9.1394 +    val skolem_depth = if skolemize then 4 else ~1
  9.1395 +    val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
  9.1396 +         core_t) = t |> unfold_defs_in_term hol_ctxt
  9.1397 +                     |> Refute.close_form
  9.1398 +                     |> skolemize_term_and_more hol_ctxt skolem_depth
  9.1399 +                     |> specialize_consts_in_term hol_ctxt 0
  9.1400 +                     |> `(axioms_for_term hol_ctxt)
  9.1401 +    val binarize =
  9.1402 +      case binary_ints of
  9.1403 +        SOME false => false
  9.1404 +      | _ =>
  9.1405 +        forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
  9.1406 +        (binary_ints = SOME true orelse
  9.1407 +         exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
  9.1408 +    val box = exists (not_equal (SOME false) o snd) boxes
  9.1409 +    val table =
  9.1410 +      Termtab.empty |> uncurry
  9.1411 +        ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts)
  9.1412 +    (* bool -> bool -> term -> term *)
  9.1413 +    fun do_rest def core =
  9.1414 +      binarize ? binarize_nat_and_int_in_term
  9.1415 +      #> uncurry ? uncurry_term table
  9.1416 +      #> box ? box_fun_and_pair_in_term hol_ctxt def
  9.1417 +      #> destroy_constrs ? (pull_out_universal_constrs thy def
  9.1418 +                            #> pull_out_existential_constrs thy
  9.1419 +                            #> destroy_pulled_out_constrs hol_ctxt def)
  9.1420 +      #> curry_assms
  9.1421 +      #> destroy_universal_equalities
  9.1422 +      #> destroy_existential_equalities thy
  9.1423 +      #> simplify_constrs_and_sels thy
  9.1424 +      #> distribute_quantifiers
  9.1425 +      #> push_quantifiers_inward thy
  9.1426 +      #> not core ? Refute.close_form
  9.1427 +      #> Term.map_abs_vars shortest_name
  9.1428 +  in
  9.1429 +    (((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts),
  9.1430 +      (got_all_mono_user_axioms, no_poly_user_axioms)),
  9.1431 +     do_rest false true core_t)
  9.1432 +  end
  9.1433 +
  9.1434 +end;
    10.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Thu Feb 04 13:36:52 2010 +0100
    10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Thu Feb 04 16:03:15 2010 +0100
    10.3 @@ -8,7 +8,7 @@
    10.4  signature NITPICK_SCOPE =
    10.5  sig
    10.6    type styp = Nitpick_Util.styp
    10.7 -  type extended_context = Nitpick_HOL.extended_context
    10.8 +  type hol_context = Nitpick_HOL.hol_context
    10.9  
   10.10    type constr_spec = {
   10.11      const: styp,
   10.12 @@ -28,7 +28,7 @@
   10.13      constrs: constr_spec list}
   10.14  
   10.15    type scope = {
   10.16 -    ext_ctxt: extended_context,
   10.17 +    hol_ctxt: hol_context,
   10.18      card_assigns: (typ * int) list,
   10.19      bits: int,
   10.20      bisim_depth: int,
   10.21 @@ -47,7 +47,7 @@
   10.22    val scopes_equivalent : scope -> scope -> bool
   10.23    val scope_less_eq : scope -> scope -> bool
   10.24    val all_scopes :
   10.25 -    extended_context -> int -> (typ option * int list) list
   10.26 +    hol_context -> int -> (typ option * int list) list
   10.27      -> (styp option * int list) list -> (styp option * int list) list
   10.28      -> int list -> int list -> typ list -> typ list -> typ list
   10.29      -> int * scope list
   10.30 @@ -77,7 +77,7 @@
   10.31    constrs: constr_spec list}
   10.32  
   10.33  type scope = {
   10.34 -  ext_ctxt: extended_context,
   10.35 +  hol_ctxt: hol_context,
   10.36    card_assigns: (typ * int) list,
   10.37    bits: int,
   10.38    bisim_depth: int,
   10.39 @@ -131,7 +131,7 @@
   10.40  
   10.41  (* (string -> string) -> scope
   10.42     -> string list * string list * string list * string list * string list *)
   10.43 -fun quintuple_for_scope quote ({ext_ctxt as {thy, ctxt, ...}, card_assigns,
   10.44 +fun quintuple_for_scope quote ({hol_ctxt as {thy, ctxt, ...}, card_assigns,
   10.45                                  bits, bisim_depth, datatypes, ...} : scope) =
   10.46    let
   10.47      val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit}, @{typ \<xi>},
   10.48 @@ -240,10 +240,9 @@
   10.49  
   10.50  val max_bits = 31 (* Kodkod limit *)
   10.51  
   10.52 -(* extended_context -> (typ option * int list) list
   10.53 -   -> (styp option * int list) list -> (styp option * int list) list -> int list
   10.54 -   -> int list -> typ -> block *)
   10.55 -fun block_for_type (ext_ctxt as {thy, ...}) cards_assigns maxes_assigns
   10.56 +(* hol_context -> (typ option * int list) list -> (styp option * int list) list
   10.57 +   -> (styp option * int list) list -> int list -> int list -> typ -> block *)
   10.58 +fun block_for_type (hol_ctxt as {thy, ...}) cards_assigns maxes_assigns
   10.59                     iters_assigns bitss bisim_depths T =
   10.60    if T = @{typ unsigned_bit} then
   10.61      [(Card T, map (Integer.min max_bits o Integer.max 1) bitss)]
   10.62 @@ -261,18 +260,18 @@
   10.63                                              (const_for_iterator_type T)))]
   10.64    else
   10.65      (Card T, lookup_type_ints_assign thy cards_assigns T) ::
   10.66 -    (case datatype_constrs ext_ctxt T of
   10.67 +    (case datatype_constrs hol_ctxt T of
   10.68         [_] => []
   10.69       | constrs => map_filter (row_for_constr thy maxes_assigns) constrs)
   10.70  
   10.71 -(* extended_context -> (typ option * int list) list
   10.72 -   -> (styp option * int list) list -> (styp option * int list) list -> int list
   10.73 -   -> int list -> typ list -> typ list -> block list *)
   10.74 -fun blocks_for_types ext_ctxt cards_assigns maxes_assigns iters_assigns bitss
   10.75 +(* hol_context -> (typ option * int list) list -> (styp option * int list) list
   10.76 +   -> (styp option * int list) list -> int list -> int list -> typ list
   10.77 +   -> typ list -> block list *)
   10.78 +fun blocks_for_types hol_ctxt cards_assigns maxes_assigns iters_assigns bitss
   10.79                       bisim_depths mono_Ts nonmono_Ts =
   10.80    let
   10.81      (* typ -> block *)
   10.82 -    val block_for = block_for_type ext_ctxt cards_assigns maxes_assigns
   10.83 +    val block_for = block_for_type hol_ctxt cards_assigns maxes_assigns
   10.84                                     iters_assigns bitss bisim_depths
   10.85      val mono_block = maps block_for mono_Ts
   10.86      val nonmono_blocks = map block_for nonmono_Ts
   10.87 @@ -313,10 +312,10 @@
   10.88  
   10.89  type scope_desc = (typ * int) list * (styp * int) list
   10.90  
   10.91 -(* extended_context -> scope_desc -> typ * int -> bool *)
   10.92 -fun is_surely_inconsistent_card_assign ext_ctxt (card_assigns, max_assigns)
   10.93 +(* hol_context -> scope_desc -> typ * int -> bool *)
   10.94 +fun is_surely_inconsistent_card_assign hol_ctxt (card_assigns, max_assigns)
   10.95                                         (T, k) =
   10.96 -  case datatype_constrs ext_ctxt T of
   10.97 +  case datatype_constrs hol_ctxt T of
   10.98      [] => false
   10.99    | xs =>
  10.100      let
  10.101 @@ -329,20 +328,20 @@
  10.102          | effective_max card max = Int.min (card, max)
  10.103        val max = map2 effective_max dom_cards maxes |> Integer.sum
  10.104      in max < k end
  10.105 -(* extended_context -> (typ * int) list -> (typ * int) list
  10.106 -   -> (styp * int) list -> bool *)
  10.107 -fun is_surely_inconsistent_scope_description ext_ctxt seen rest max_assigns =
  10.108 -  exists (is_surely_inconsistent_card_assign ext_ctxt
  10.109 +(* hol_context -> (typ * int) list -> (typ * int) list -> (styp * int) list
  10.110 +   -> bool *)
  10.111 +fun is_surely_inconsistent_scope_description hol_ctxt seen rest max_assigns =
  10.112 +  exists (is_surely_inconsistent_card_assign hol_ctxt
  10.113                                               (seen @ rest, max_assigns)) seen
  10.114  
  10.115 -(* extended_context -> scope_desc -> (typ * int) list option *)
  10.116 -fun repair_card_assigns ext_ctxt (card_assigns, max_assigns) =
  10.117 +(* hol_context -> scope_desc -> (typ * int) list option *)
  10.118 +fun repair_card_assigns hol_ctxt (card_assigns, max_assigns) =
  10.119    let
  10.120      (* (typ * int) list -> (typ * int) list -> (typ * int) list option *)
  10.121      fun aux seen [] = SOME seen
  10.122        | aux seen ((T, 0) :: _) = NONE
  10.123        | aux seen ((T, k) :: rest) =
  10.124 -        (if is_surely_inconsistent_scope_description ext_ctxt ((T, k) :: seen)
  10.125 +        (if is_surely_inconsistent_scope_description hol_ctxt ((T, k) :: seen)
  10.126                                                       rest max_assigns then
  10.127             raise SAME ()
  10.128           else
  10.129 @@ -374,12 +373,12 @@
  10.130  (* block -> scope_desc *)
  10.131  fun scope_descriptor_from_block block =
  10.132    fold_rev add_row_to_scope_descriptor block ([], [])
  10.133 -(* extended_context -> block list -> int list -> scope_desc option *)
  10.134 -fun scope_descriptor_from_combination (ext_ctxt as {thy, ...}) blocks columns =
  10.135 +(* hol_context -> block list -> int list -> scope_desc option *)
  10.136 +fun scope_descriptor_from_combination (hol_ctxt as {thy, ...}) blocks columns =
  10.137    let
  10.138      val (card_assigns, max_assigns) =
  10.139        maps project_block (columns ~~ blocks) |> scope_descriptor_from_block
  10.140 -    val card_assigns = repair_card_assigns ext_ctxt (card_assigns, max_assigns)
  10.141 +    val card_assigns = repair_card_assigns hol_ctxt (card_assigns, max_assigns)
  10.142                         |> the
  10.143    in
  10.144      SOME (map (repair_iterator_assign thy card_assigns) card_assigns,
  10.145 @@ -449,25 +448,25 @@
  10.146       explicit_max = max, total = total} :: constrs
  10.147    end
  10.148  
  10.149 -(* extended_context -> (typ * int) list -> typ -> bool *)
  10.150 -fun has_exact_card ext_ctxt card_assigns T =
  10.151 +(* hol_context -> (typ * int) list -> typ -> bool *)
  10.152 +fun has_exact_card hol_ctxt card_assigns T =
  10.153    let val card = card_of_type card_assigns T in
  10.154 -    card = bounded_exact_card_of_type ext_ctxt (card + 1) 0 card_assigns T
  10.155 +    card = bounded_exact_card_of_type hol_ctxt (card + 1) 0 card_assigns T
  10.156    end
  10.157  
  10.158 -(* extended_context -> typ list -> scope_desc -> typ * int -> dtype_spec *)
  10.159 -fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...}) deep_dataTs
  10.160 +(* hol_context -> typ list -> scope_desc -> typ * int -> dtype_spec *)
  10.161 +fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, ...}) deep_dataTs
  10.162                                          (desc as (card_assigns, _)) (T, card) =
  10.163    let
  10.164      val deep = member (op =) deep_dataTs T
  10.165      val co = is_codatatype thy T
  10.166 -    val xs = boxed_datatype_constrs ext_ctxt T
  10.167 +    val xs = boxed_datatype_constrs hol_ctxt T
  10.168      val self_recs = map (is_self_recursive_constr_type o snd) xs
  10.169      val (num_self_recs, num_non_self_recs) =
  10.170        List.partition I self_recs |> pairself length
  10.171 -    val complete = has_exact_card ext_ctxt card_assigns T
  10.172 +    val complete = has_exact_card hol_ctxt card_assigns T
  10.173      val concrete = xs |> maps (binder_types o snd) |> maps binder_types
  10.174 -                      |> forall (has_exact_card ext_ctxt card_assigns)
  10.175 +                      |> forall (has_exact_card hol_ctxt card_assigns)
  10.176      (* int -> int *)
  10.177      fun sum_dom_cards max =
  10.178        map (domain_card max card_assigns o snd) xs |> Integer.sum
  10.179 @@ -487,12 +486,12 @@
  10.180      min_bits_for_nat_value (fold Integer.max
  10.181          (map snd card_assigns @ map snd max_assigns) 0)
  10.182  
  10.183 -(* extended_context -> int -> typ list -> scope_desc -> scope *)
  10.184 -fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break deep_dataTs
  10.185 +(* hol_context -> int -> typ list -> scope_desc -> scope *)
  10.186 +fun scope_from_descriptor (hol_ctxt as {thy, ...}) sym_break deep_dataTs
  10.187                            (desc as (card_assigns, _)) =
  10.188    let
  10.189      val datatypes =
  10.190 -      map (datatype_spec_from_scope_descriptor ext_ctxt deep_dataTs desc)
  10.191 +      map (datatype_spec_from_scope_descriptor hol_ctxt deep_dataTs desc)
  10.192            (filter (is_datatype thy o fst) card_assigns)
  10.193      val bits = card_of_type card_assigns @{typ signed_bit} - 1
  10.194                 handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
  10.195 @@ -500,7 +499,7 @@
  10.196                        handle TYPE ("Nitpick_HOL.card_of_type", _, _) => 0
  10.197      val bisim_depth = card_of_type card_assigns @{typ bisim_iterator} - 1
  10.198    in
  10.199 -    {ext_ctxt = ext_ctxt, card_assigns = card_assigns, datatypes = datatypes,
  10.200 +    {hol_ctxt = hol_ctxt, card_assigns = card_assigns, datatypes = datatypes,
  10.201       bits = bits, bisim_depth = bisim_depth,
  10.202       ofs = if sym_break <= 0 then Typtab.empty
  10.203             else offset_table_for_card_assigns thy card_assigns datatypes}
  10.204 @@ -521,26 +520,26 @@
  10.205  val max_scopes = 4096
  10.206  val distinct_threshold = 512
  10.207  
  10.208 -(* extended_context -> int -> (typ option * int list) list
  10.209 +(* hol_context -> int -> (typ option * int list) list
  10.210     -> (styp option * int list) list -> (styp option * int list) list -> int list
  10.211     -> typ list -> typ list -> typ list -> int * scope list *)
  10.212 -fun all_scopes (ext_ctxt as {thy, ...}) sym_break cards_assigns maxes_assigns
  10.213 +fun all_scopes (hol_ctxt as {thy, ...}) sym_break cards_assigns maxes_assigns
  10.214                 iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs =
  10.215    let
  10.216      val cards_assigns = repair_cards_assigns_wrt_boxing thy mono_Ts
  10.217                                                          cards_assigns
  10.218 -    val blocks = blocks_for_types ext_ctxt cards_assigns maxes_assigns
  10.219 +    val blocks = blocks_for_types hol_ctxt cards_assigns maxes_assigns
  10.220                                    iters_assigns bitss bisim_depths mono_Ts
  10.221                                    nonmono_Ts
  10.222      val ranks = map rank_of_block blocks
  10.223      val all = all_combinations_ordered_smartly (map (rpair 0) ranks)
  10.224      val head = take max_scopes all
  10.225 -    val descs = map_filter (scope_descriptor_from_combination ext_ctxt blocks)
  10.226 +    val descs = map_filter (scope_descriptor_from_combination hol_ctxt blocks)
  10.227                             head
  10.228    in
  10.229      (length all - length head,
  10.230       descs |> length descs <= distinct_threshold ? distinct (op =)
  10.231 -           |> map (scope_from_descriptor ext_ctxt sym_break deep_dataTs))
  10.232 +           |> map (scope_from_descriptor hol_ctxt sym_break deep_dataTs))
  10.233    end
  10.234  
  10.235  end;