src/HOL/Tools/Nitpick/nitpick_preproc.ML
changeset 35070 96136eb6218f
child 35078 6fd1052fe463
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Feb 04 16:03:15 2010 +0100
@@ -0,0 +1,1431 @@
+(*  Title:      HOL/Tools/Nitpick/nitpick_preproc.ML
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2008, 2009, 2010
+
+Nitpick's HOL preprocessor.
+*)
+
+signature NITPICK_PREPROC =
+sig
+  type hol_context = Nitpick_HOL.hol_context
+  val preprocess_term :
+    hol_context -> term -> ((term list * term list) * (bool * bool)) * term
+end
+
+structure Nitpick_Preproc : NITPICK_PREPROC =
+struct
+
+open Nitpick_Util
+open Nitpick_HOL
+
+(* polarity -> string -> bool *)
+fun is_positive_existential polar quant_s =
+  (polar = Pos andalso quant_s = @{const_name Ex}) orelse
+  (polar = Neg andalso quant_s <> @{const_name Ex})
+
+(** Binary coding of integers **)
+
+(* If a formula contains a numeral whose absolute value is more than this
+   threshold, the unary coding is likely not to work well and we prefer the
+   binary coding. *)
+val binary_int_threshold = 3
+
+(* term -> bool *)
+fun may_use_binary_ints (t1 $ t2) =
+    may_use_binary_ints t1 andalso may_use_binary_ints t2
+  | may_use_binary_ints (t as Const (s, _)) =
+    t <> @{const Suc} andalso
+    not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac},
+                        @{const_name nat_gcd}, @{const_name nat_lcm},
+                        @{const_name Frac}, @{const_name norm_frac}] s)
+  | may_use_binary_ints (Abs (_, _, t')) = may_use_binary_ints t'
+  | may_use_binary_ints _ = true
+fun should_use_binary_ints (t1 $ t2) =
+    should_use_binary_ints t1 orelse should_use_binary_ints t2
+  | should_use_binary_ints (Const (s, _)) =
+    member (op =) [@{const_name times_nat_inst.times_nat},
+                   @{const_name div_nat_inst.div_nat},
+                   @{const_name times_int_inst.times_int},
+                   @{const_name div_int_inst.div_int}] s orelse
+    (String.isPrefix numeral_prefix s andalso
+     let val n = the (Int.fromString (unprefix numeral_prefix s)) in
+       n < ~ binary_int_threshold orelse n > binary_int_threshold
+     end)
+  | should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t'
+  | should_use_binary_ints _ = false
+
+(* typ -> typ *)
+fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}
+  | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}
+  | binarize_nat_and_int_in_type (Type (s, Ts)) =
+    Type (s, map binarize_nat_and_int_in_type Ts)
+  | binarize_nat_and_int_in_type T = T
+(* term -> term *)
+val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type
+
+(** Uncurrying **)
+
+(* theory -> term -> int Termtab.tab -> int Termtab.tab *)
+fun add_to_uncurry_table thy t =
+  let
+    (* term -> term list -> int Termtab.tab -> int Termtab.tab *)
+    fun aux (t1 $ t2) args table =
+        let val table = aux t2 [] table in aux t1 (t2 :: args) table end
+      | aux (Abs (_, _, t')) _ table = aux t' [] table
+      | aux (t as Const (x as (s, _))) args table =
+        if is_built_in_const true x orelse is_constr_like thy x orelse
+           is_sel s orelse s = @{const_name Sigma} then
+          table
+        else
+          Termtab.map_default (t, 65536) (curry Int.min (length args)) table
+      | aux _ _ table = table
+  in aux t [] end
+
+(* int -> int -> string *)
+fun uncurry_prefix_for k j =
+  uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
+
+(* int Termtab.tab term -> term *)
+fun uncurry_term table t =
+  let
+    (* term -> term list -> term *)
+    fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args)
+      | aux (Abs (s, T, t')) args = betapplys (Abs (s, T, aux t' []), args)
+      | aux (t as Const (s, T)) args =
+        (case Termtab.lookup table t of
+           SOME n =>
+           if n >= 2 then
+             let
+               val (arg_Ts, rest_T) = strip_n_binders n T
+               val j =
+                 if hd arg_Ts = @{typ bisim_iterator} orelse
+                    is_fp_iterator_type (hd arg_Ts) then
+                   1
+                 else case find_index (not_equal bool_T) arg_Ts of
+                   ~1 => n
+                 | j => j
+               val ((before_args, tuple_args), after_args) =
+                 args |> chop n |>> chop j
+               val ((before_arg_Ts, tuple_arg_Ts), rest_T) =
+                 T |> strip_n_binders n |>> chop j
+               val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
+             in
+               if n - j < 2 then
+                 betapplys (t, args)
+               else
+                 betapplys (Const (uncurry_prefix_for (n - j) j ^ s,
+                                   before_arg_Ts ---> tuple_T --> rest_T),
+                            before_args @ [mk_flat_tuple tuple_T tuple_args] @
+                            after_args)
+             end
+           else
+             betapplys (t, args)
+         | NONE => betapplys (t, args))
+      | aux t args = betapplys (t, args)
+  in aux t [] end
+
+(** Boxing **)
+
+(* hol_context -> typ -> term -> term *)
+fun constr_expand (hol_ctxt as {thy, ...}) T t =
+  (case head_of t of
+     Const x => if is_constr_like thy x then t else raise SAME ()
+   | _ => raise SAME ())
+  handle SAME () =>
+         let
+           val x' as (_, T') =
+             if is_pair_type T then
+               let val (T1, T2) = HOLogic.dest_prodT T in
+                 (@{const_name Pair}, T1 --> T2 --> T)
+               end
+             else
+               datatype_constrs hol_ctxt T |> hd
+           val arg_Ts = binder_types T'
+         in
+           list_comb (Const x', map2 (select_nth_constr_arg thy x' t)
+                                     (index_seq 0 (length arg_Ts)) arg_Ts)
+         end
+
+(* hol_context -> bool -> term -> term *)
+fun box_fun_and_pair_in_term (hol_ctxt as {thy, fast_descrs, ...}) def orig_t =
+  let
+    (* typ -> typ *)
+    fun box_relational_operator_type (Type ("fun", Ts)) =
+        Type ("fun", map box_relational_operator_type Ts)
+      | box_relational_operator_type (Type ("*", Ts)) =
+        Type ("*", map (box_type hol_ctxt InPair) Ts)
+      | box_relational_operator_type T = T
+    (* (term -> term) -> int -> term -> term *)
+    fun coerce_bound_no f j t =
+      case t of
+        t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
+      | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
+      | Bound j' => if j' = j then f t else t
+      | _ => t
+    (* typ -> typ -> term -> term *)
+    fun coerce_bound_0_in_term new_T old_T =
+      old_T <> new_T ? coerce_bound_no (coerce_term [new_T] old_T new_T) 0
+    (* typ list -> typ -> term -> term *)
+    and coerce_term Ts new_T old_T t =
+      if old_T = new_T then
+        t
+      else
+        case (new_T, old_T) of
+          (Type (new_s, new_Ts as [new_T1, new_T2]),
+           Type ("fun", [old_T1, old_T2])) =>
+          (case eta_expand Ts t 1 of
+             Abs (s, _, t') =>
+             Abs (s, new_T1,
+                  t' |> coerce_bound_0_in_term new_T1 old_T1
+                     |> coerce_term (new_T1 :: Ts) new_T2 old_T2)
+             |> Envir.eta_contract
+             |> new_s <> "fun"
+                ? construct_value thy (@{const_name FunBox},
+                                       Type ("fun", new_Ts) --> new_T) o single
+           | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\
+                               \coerce_term", [t']))
+        | (Type (new_s, new_Ts as [new_T1, new_T2]),
+           Type (old_s, old_Ts as [old_T1, old_T2])) =>
+          if old_s = @{type_name fun_box} orelse
+             old_s = @{type_name pair_box} orelse old_s = "*" then
+            case constr_expand hol_ctxt old_T t of
+              Const (@{const_name FunBox}, _) $ t1 =>
+              if new_s = "fun" then
+                coerce_term Ts new_T (Type ("fun", old_Ts)) t1
+              else
+                construct_value thy
+                    (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
+                     [coerce_term Ts (Type ("fun", new_Ts))
+                                  (Type ("fun", old_Ts)) t1]
+            | Const _ $ t1 $ t2 =>
+              construct_value thy
+                  (if new_s = "*" then @{const_name Pair}
+                   else @{const_name PairBox}, new_Ts ---> new_T)
+                  [coerce_term Ts new_T1 old_T1 t1,
+                   coerce_term Ts new_T2 old_T2 t2]
+            | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\
+                                \coerce_term", [t'])
+          else
+            raise TYPE ("coerce_term", [new_T, old_T], [t])
+        | _ => raise TYPE ("coerce_term", [new_T, old_T], [t])
+    (* indexname * typ -> typ * term -> typ option list -> typ option list *)
+    fun add_boxed_types_for_var (z as (_, T)) (T', t') =
+      case t' of
+        Var z' => z' = z ? insert (op =) T'
+      | Const (@{const_name Pair}, _) $ t1 $ t2 =>
+        (case T' of
+           Type (_, [T1, T2]) =>
+           fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)]
+         | _ => raise TYPE ("Nitpick_Preproc.box_fun_and_pair_in_term.\
+                            \add_boxed_types_for_var", [T'], []))
+      | _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T
+    (* typ list -> typ list -> term -> indexname * typ -> typ *)
+    fun box_var_in_def new_Ts old_Ts t (z as (_, T)) =
+      case t of
+        @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
+      | Const (s0, _) $ t1 $ _ =>
+        if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then
+          let
+            val (t', args) = strip_comb t1
+            val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
+          in
+            case fold (add_boxed_types_for_var z)
+                      (fst (strip_n_binders (length args) T') ~~ args) [] of
+              [T''] => T''
+            | _ => T
+          end
+        else
+          T
+      | _ => T
+    (* typ list -> typ list -> polarity -> string -> typ -> string -> typ
+       -> term -> term *)
+    and do_quantifier new_Ts old_Ts polar quant_s quant_T abs_s abs_T t =
+      let
+        val abs_T' =
+          if polar = Neut orelse is_positive_existential polar quant_s then
+            box_type hol_ctxt InFunLHS abs_T
+          else
+            abs_T
+        val body_T = body_type quant_T
+      in
+        Const (quant_s, (abs_T' --> body_T) --> body_T)
+        $ Abs (abs_s, abs_T',
+               t |> do_term (abs_T' :: new_Ts) (abs_T :: old_Ts) polar)
+      end
+    (* typ list -> typ list -> string -> typ -> term -> term -> term *)
+    and do_equals new_Ts old_Ts s0 T0 t1 t2 =
+      let
+        val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2)
+        val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
+        val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last
+      in
+        list_comb (Const (s0, T --> T --> body_type T0),
+                   map2 (coerce_term new_Ts T) [T1, T2] [t1, t2])
+      end
+    (* string -> typ -> term *)
+    and do_description_operator s T =
+      let val T1 = box_type hol_ctxt InFunLHS (range_type T) in
+        Const (s, (T1 --> bool_T) --> T1)
+      end
+    (* typ list -> typ list -> polarity -> term -> term *)
+    and do_term new_Ts old_Ts polar t =
+      case t of
+        Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
+        do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
+      | Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 =>
+        do_equals new_Ts old_Ts s0 T0 t1 t2
+      | @{const "==>"} $ t1 $ t2 =>
+        @{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
+        $ do_term new_Ts old_Ts polar t2
+      | @{const Pure.conjunction} $ t1 $ t2 =>
+        @{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1
+        $ do_term new_Ts old_Ts polar t2
+      | @{const Trueprop} $ t1 =>
+        @{const Trueprop} $ do_term new_Ts old_Ts polar t1
+      | @{const Not} $ t1 =>
+        @{const Not} $ do_term new_Ts old_Ts (flip_polarity polar) t1
+      | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
+        do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
+      | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
+        do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
+      | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>
+        do_equals new_Ts old_Ts s0 T0 t1 t2
+      | @{const "op &"} $ t1 $ t2 =>
+        @{const "op &"} $ do_term new_Ts old_Ts polar t1
+        $ do_term new_Ts old_Ts polar t2
+      | @{const "op |"} $ t1 $ t2 =>
+        @{const "op |"} $ do_term new_Ts old_Ts polar t1
+        $ do_term new_Ts old_Ts polar t2
+      | @{const "op -->"} $ t1 $ t2 =>
+        @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
+        $ do_term new_Ts old_Ts polar t2
+      | Const (s as @{const_name The}, T) => do_description_operator s T
+      | Const (s as @{const_name Eps}, T) => do_description_operator s T
+      | Const (@{const_name quot_normal}, Type ("fun", [_, T2])) =>
+        let val T' = box_type hol_ctxt InSel T2 in
+          Const (@{const_name quot_normal}, T' --> T')
+        end
+      | Const (s as @{const_name Tha}, T) => do_description_operator s T
+      | Const (x as (s, T)) =>
+        Const (s, if s = @{const_name converse} orelse
+                     s = @{const_name trancl} then
+                    box_relational_operator_type T
+                  else if is_built_in_const fast_descrs x orelse
+                          s = @{const_name Sigma} then
+                    T
+                  else if is_constr_like thy x then
+                    box_type hol_ctxt InConstr T
+                  else if is_sel s
+                       orelse is_rep_fun thy x then
+                    box_type hol_ctxt InSel T
+                  else
+                    box_type hol_ctxt InExpr T)
+      | t1 $ Abs (s, T, t2') =>
+        let
+          val t1 = do_term new_Ts old_Ts Neut t1
+          val T1 = fastype_of1 (new_Ts, t1)
+          val (s1, Ts1) = dest_Type T1
+          val T' = hd (snd (dest_Type (hd Ts1)))
+          val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2')
+          val T2 = fastype_of1 (new_Ts, t2)
+          val t2 = coerce_term new_Ts (hd Ts1) T2 t2
+        in
+          betapply (if s1 = "fun" then
+                      t1
+                    else
+                      select_nth_constr_arg thy
+                          (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
+                          (Type ("fun", Ts1)), t2)
+        end
+      | t1 $ t2 =>
+        let
+          val t1 = do_term new_Ts old_Ts Neut t1
+          val T1 = fastype_of1 (new_Ts, t1)
+          val (s1, Ts1) = dest_Type T1
+          val t2 = do_term new_Ts old_Ts Neut t2
+          val T2 = fastype_of1 (new_Ts, t2)
+          val t2 = coerce_term new_Ts (hd Ts1) T2 t2
+        in
+          betapply (if s1 = "fun" then
+                      t1
+                    else
+                      select_nth_constr_arg thy
+                          (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
+                          (Type ("fun", Ts1)), t2)
+        end
+      | Free (s, T) => Free (s, box_type hol_ctxt InExpr T)
+      | Var (z as (x, T)) =>
+        Var (x, if def then box_var_in_def new_Ts old_Ts orig_t z
+                else box_type hol_ctxt InExpr T)
+      | Bound _ => t
+      | Abs (s, T, t') =>
+        Abs (s, T, do_term (T :: new_Ts) (T :: old_Ts) Neut t')
+  in do_term [] [] Pos orig_t end
+
+(** Destruction of constructors **)
+
+val val_var_prefix = nitpick_prefix ^ "v"
+
+(* typ list -> int -> int -> int -> term -> term *)
+fun fresh_value_var Ts k n j t =
+  Var ((val_var_prefix ^ nat_subscript (n - j), k), fastype_of1 (Ts, t))
+
+(* typ list -> int -> term -> bool *)
+fun has_heavy_bounds_or_vars Ts level t =
+  let
+    (* typ list -> bool *)
+    fun aux [] = false
+      | aux [T] = is_fun_type T orelse is_pair_type T
+      | aux _ = true
+  in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
+
+(* theory -> typ list -> bool -> int -> int -> term -> term list -> term list
+   -> term * term list *)
+fun pull_out_constr_comb thy Ts relax k level t args seen =
+  let val t_comb = list_comb (t, args) in
+    case t of
+      Const x =>
+      if not relax andalso is_constr thy x andalso
+         not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso
+         has_heavy_bounds_or_vars Ts level t_comb andalso
+         not (loose_bvar (t_comb, level)) then
+        let
+          val (j, seen) = case find_index (curry (op =) t_comb) seen of
+                            ~1 => (0, t_comb :: seen)
+                          | j => (j, seen)
+        in (fresh_value_var Ts k (length seen) j t_comb, seen) end
+      else
+        (t_comb, seen)
+    | _ => (t_comb, seen)
+  end
+
+(* (term -> term) -> typ list -> int -> term list -> term list *)
+fun equations_for_pulled_out_constrs mk_eq Ts k seen =
+  let val n = length seen in
+    map2 (fn j => fn t => mk_eq (fresh_value_var Ts k n j t, t))
+         (index_seq 0 n) seen
+  end
+
+(* theory -> bool -> term -> term *)
+fun pull_out_universal_constrs thy def t =
+  let
+    val k = maxidx_of_term t + 1
+    (* typ list -> bool -> term -> term list -> term list -> term * term list *)
+    fun do_term Ts def t args seen =
+      case t of
+        (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 =>
+        do_eq_or_imp Ts true def t0 t1 t2 seen
+      | (t0 as @{const "==>"}) $ t1 $ t2 =>
+        if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
+      | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
+        do_eq_or_imp Ts true def t0 t1 t2 seen
+      | (t0 as @{const "op -->"}) $ t1 $ t2 =>
+        do_eq_or_imp Ts false def t0 t1 t2 seen
+      | Abs (s, T, t') =>
+        let val (t', seen) = do_term (T :: Ts) def t' [] seen in
+          (list_comb (Abs (s, T, t'), args), seen)
+        end
+      | t1 $ t2 =>
+        let val (t2, seen) = do_term Ts def t2 [] seen in
+          do_term Ts def t1 (t2 :: args) seen
+        end
+      | _ => pull_out_constr_comb thy Ts def k 0 t args seen
+    (* typ list -> bool -> bool -> term -> term -> term -> term list
+       -> term * term list *)
+    and do_eq_or_imp Ts eq def t0 t1 t2 seen =
+      let
+        val (t2, seen) = if eq andalso def then (t2, seen)
+                         else do_term Ts false t2 [] seen
+        val (t1, seen) = do_term Ts false t1 [] seen
+      in (t0 $ t1 $ t2, seen) end
+    val (concl, seen) = do_term [] def t [] []
+  in
+    Logic.list_implies (equations_for_pulled_out_constrs Logic.mk_equals [] k
+                                                         seen, concl)
+  end
+
+(* term -> term -> term *)
+fun mk_exists v t =
+  HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)
+
+(* theory -> term -> term *)
+fun pull_out_existential_constrs thy t =
+  let
+    val k = maxidx_of_term t + 1
+    (* typ list -> int -> term -> term list -> term list -> term * term list *)
+    fun aux Ts num_exists t args seen =
+      case t of
+        (t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1) =>
+        let
+          val (t1, seen') = aux (T1 :: Ts) (num_exists + 1) t1 [] []
+          val n = length seen'
+          (* unit -> term list *)
+          fun vars () = map2 (fresh_value_var Ts k n) (index_seq 0 n) seen'
+        in
+          (equations_for_pulled_out_constrs HOLogic.mk_eq Ts k seen'
+           |> List.foldl s_conj t1 |> fold mk_exists (vars ())
+           |> curry3 Abs s1 T1 |> curry (op $) t0, seen)
+        end
+      | t1 $ t2 =>
+        let val (t2, seen) = aux Ts num_exists t2 [] seen in
+          aux Ts num_exists t1 (t2 :: args) seen
+        end
+      | Abs (s, T, t') =>
+        let
+          val (t', seen) = aux (T :: Ts) 0 t' [] (map (incr_boundvars 1) seen)
+        in (list_comb (Abs (s, T, t'), args), map (incr_boundvars ~1) seen) end
+      | _ =>
+        if num_exists > 0 then
+          pull_out_constr_comb thy Ts false k num_exists t args seen
+        else
+          (list_comb (t, args), seen)
+  in aux [] 0 t [] [] |> fst end
+
+(* hol_context -> bool -> term -> term *)
+fun destroy_pulled_out_constrs (hol_ctxt as {thy, ...}) axiom t =
+  let
+    (* styp -> int *)
+    val num_occs_of_var =
+      fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
+                    | _ => I) t (K 0)
+    (* bool -> term -> term *)
+    fun aux careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =
+        aux_eq careful true t0 t1 t2
+      | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =
+        t0 $ aux false t1 $ aux careful t2
+      | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
+        aux_eq careful true t0 t1 t2
+      | aux careful ((t0 as @{const "op -->"}) $ t1 $ t2) =
+        t0 $ aux false t1 $ aux careful t2
+      | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')
+      | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2
+      | aux _ t = t
+    (* bool -> bool -> term -> term -> term -> term *)
+    and aux_eq careful pass1 t0 t1 t2 =
+      ((if careful then
+          raise SAME ()
+        else if axiom andalso is_Var t2 andalso
+                num_occs_of_var (dest_Var t2) = 1 then
+          @{const True}
+        else case strip_comb t2 of
+          (* The first case is not as general as it could be. *)
+          (Const (@{const_name PairBox}, _),
+                  [Const (@{const_name fst}, _) $ Var z1,
+                   Const (@{const_name snd}, _) $ Var z2]) =>
+          if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True}
+          else raise SAME ()
+        | (Const (x as (s, T)), args) =>
+          let val arg_Ts = binder_types T in
+            if length arg_Ts = length args andalso
+               (is_constr thy x orelse s = @{const_name Pair} orelse
+                x = (@{const_name Suc}, nat_T --> nat_T)) andalso
+               (not careful orelse not (is_Var t1) orelse
+                String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
+              discriminate_value hol_ctxt x t1 ::
+              map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
+              |> foldr1 s_conj
+            else
+              raise SAME ()
+          end
+        | _ => raise SAME ())
+       |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop)
+      handle SAME () => if pass1 then aux_eq careful false t0 t2 t1
+                        else t0 $ aux false t2 $ aux false t1
+    (* styp -> term -> int -> typ -> term -> term *)
+    and sel_eq x t n nth_T nth_t =
+      HOLogic.eq_const nth_T $ nth_t $ select_nth_constr_arg thy x t n nth_T
+      |> aux false
+  in aux axiom t end
+
+(** Destruction of universal and existential equalities **)
+
+(* term -> term *)
+fun curry_assms (@{const "==>"} $ (@{const Trueprop}
+                                   $ (@{const "op &"} $ t1 $ t2)) $ t3) =
+    curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
+  | curry_assms (@{const "==>"} $ t1 $ t2) =
+    @{const "==>"} $ curry_assms t1 $ curry_assms t2
+  | curry_assms t = t
+
+(* term -> term *)
+val destroy_universal_equalities =
+  let
+    (* term list -> (indexname * typ) list -> term -> term *)
+    fun aux prems zs t =
+      case t of
+        @{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2
+      | _ => Logic.list_implies (rev prems, t)
+    (* term list -> (indexname * typ) list -> term -> term -> term *)
+    and aux_implies prems zs t1 t2 =
+      case t1 of
+        Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
+      | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') =>
+        aux_eq prems zs z t' t1 t2
+      | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) =>
+        aux_eq prems zs z t' t1 t2
+      | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
+    (* term list -> (indexname * typ) list -> indexname * typ -> term -> term
+       -> term -> term *)
+    and aux_eq prems zs z t' t1 t2 =
+      if not (member (op =) zs z) andalso
+         not (exists_subterm (curry (op =) (Var z)) t') then
+        aux prems zs (subst_free [(Var z, t')] t2)
+      else
+        aux (t1 :: prems) (Term.add_vars t1 zs) t2
+  in aux [] [] end
+
+(* theory -> int -> term list -> term list -> (term * term list) option *)
+fun find_bound_assign _ _ _ [] = NONE
+  | find_bound_assign thy j seen (t :: ts) =
+    let
+      (* bool -> term -> term -> (term * term list) option *)
+      fun aux pass1 t1 t2 =
+        (if loose_bvar1 (t2, j) then
+           if pass1 then aux false t2 t1 else raise SAME ()
+         else case t1 of
+           Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()
+         | Const (s, Type ("fun", [T1, T2])) $ Bound j' =>
+           if j' = j andalso
+              s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then
+             SOME (construct_value thy (@{const_name FunBox}, T2 --> T1) [t2],
+                   ts @ seen)
+           else
+             raise SAME ()
+         | _ => raise SAME ())
+        handle SAME () => find_bound_assign thy j (t :: seen) ts
+    in
+      case t of
+        Const (@{const_name "op ="}, _) $ t1 $ t2 => aux true t1 t2
+      | _ => find_bound_assign thy j (t :: seen) ts
+    end
+
+(* int -> term -> term -> term *)
+fun subst_one_bound j arg t =
+  let
+    fun aux (Bound i, lev) =
+        if i < lev then raise SAME ()
+        else if i = lev then incr_boundvars (lev - j) arg
+        else Bound (i - 1)
+      | aux (Abs (a, T, body), lev) = Abs (a, T, aux (body, lev + 1))
+      | aux (f $ t, lev) =
+        (aux (f, lev) $ (aux (t, lev) handle SAME () => t)
+         handle SAME () => f $ aux (t, lev))
+      | aux _ = raise SAME ()
+  in aux (t, j) handle SAME () => t end
+
+(* theory -> term -> term *)
+fun destroy_existential_equalities thy =
+  let
+    (* string list -> typ list -> term list -> term *)
+    fun kill [] [] ts = foldr1 s_conj ts
+      | kill (s :: ss) (T :: Ts) ts =
+        (case find_bound_assign thy (length ss) [] ts of
+           SOME (_, []) => @{const True}
+         | SOME (arg_t, ts) =>
+           kill ss Ts (map (subst_one_bound (length ss)
+                                (incr_bv (~1, length ss + 1, arg_t))) ts)
+         | NONE =>
+           Const (@{const_name Ex}, (T --> bool_T) --> bool_T)
+           $ Abs (s, T, kill ss Ts ts))
+      | kill _ _ _ = raise UnequalLengths
+    (* string list -> typ list -> term -> term *)
+    fun gather ss Ts ((t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1)) =
+        gather (ss @ [s1]) (Ts @ [T1]) t1
+      | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)
+      | gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2
+      | gather [] [] t = t
+      | gather ss Ts t = kill ss Ts (conjuncts_of (gather [] [] t))
+  in gather [] [] end
+
+(** Skolemization **)
+
+(* int -> int -> string *)
+fun skolem_prefix_for k j =
+  skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
+
+(* hol_context -> int -> term -> term *)
+fun skolemize_term_and_more (hol_ctxt as {thy, def_table, skolems, ...})
+                            skolem_depth =
+  let
+    (* int list -> int list *)
+    val incrs = map (Integer.add 1)
+    (* string list -> typ list -> int list -> int -> polarity -> term -> term *)
+    fun aux ss Ts js depth polar t =
+      let
+        (* string -> typ -> string -> typ -> term -> term *)
+        fun do_quantifier quant_s quant_T abs_s abs_T t =
+          if not (loose_bvar1 (t, 0)) then
+            aux ss Ts js depth polar (incr_boundvars ~1 t)
+          else if depth <= skolem_depth andalso
+                  is_positive_existential polar quant_s then
+            let
+              val j = length (!skolems) + 1
+              val sko_s = skolem_prefix_for (length js) j ^ abs_s
+              val _ = Unsynchronized.change skolems (cons (sko_s, ss))
+              val sko_t = list_comb (Const (sko_s, rev Ts ---> abs_T),
+                                     map Bound (rev js))
+              val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) depth polar t)
+            in
+              if null js then betapply (abs_t, sko_t)
+              else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t $ abs_t
+            end
+          else
+            Const (quant_s, quant_T)
+            $ Abs (abs_s, abs_T,
+                   if is_higher_order_type abs_T then
+                     t
+                   else
+                     aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js)
+                         (depth + 1) polar t)
+      in
+        case t of
+          Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
+          do_quantifier s0 T0 s1 T1 t1
+        | @{const "==>"} $ t1 $ t2 =>
+          @{const "==>"} $ aux ss Ts js depth (flip_polarity polar) t1
+          $ aux ss Ts js depth polar t2
+        | @{const Pure.conjunction} $ t1 $ t2 =>
+          @{const Pure.conjunction} $ aux ss Ts js depth polar t1
+          $ aux ss Ts js depth polar t2
+        | @{const Trueprop} $ t1 =>
+          @{const Trueprop} $ aux ss Ts js depth polar t1
+        | @{const Not} $ t1 =>
+          @{const Not} $ aux ss Ts js depth (flip_polarity polar) t1
+        | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
+          do_quantifier s0 T0 s1 T1 t1
+        | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
+          do_quantifier s0 T0 s1 T1 t1
+        | @{const "op &"} $ t1 $ t2 =>
+          @{const "op &"} $ aux ss Ts js depth polar t1
+          $ aux ss Ts js depth polar t2
+        | @{const "op |"} $ t1 $ t2 =>
+          @{const "op |"} $ aux ss Ts js depth polar t1
+          $ aux ss Ts js depth polar t2
+        | @{const "op -->"} $ t1 $ t2 =>
+          @{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1
+          $ aux ss Ts js depth polar t2
+        | (t0 as Const (@{const_name Let}, T0)) $ t1 $ t2 =>
+          t0 $ t1 $ aux ss Ts js depth polar t2
+        | Const (x as (s, T)) =>
+          if is_inductive_pred hol_ctxt x andalso
+             not (is_well_founded_inductive_pred hol_ctxt x) then
+            let
+              val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
+              val (pref, connective, set_oper) =
+                if gfp then
+                  (lbfp_prefix,
+                   @{const "op |"},
+                   @{const_name upper_semilattice_fun_inst.sup_fun})
+                else
+                  (ubfp_prefix,
+                   @{const "op &"},
+                   @{const_name lower_semilattice_fun_inst.inf_fun})
+              (* unit -> term *)
+              fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x
+                           |> aux ss Ts js depth polar
+              fun neg () = Const (pref ^ s, T)
+            in
+              (case polar |> gfp ? flip_polarity of
+                 Pos => pos ()
+               | Neg => neg ()
+               | Neut =>
+                 if is_fun_type T then
+                   let
+                     val ((trunk_arg_Ts, rump_arg_T), body_T) =
+                       T |> strip_type |>> split_last
+                     val set_T = rump_arg_T --> body_T
+                     (* (unit -> term) -> term *)
+                     fun app f =
+                       list_comb (f (),
+                                  map Bound (length trunk_arg_Ts - 1 downto 0))
+                   in
+                     List.foldr absdummy
+                                (Const (set_oper, set_T --> set_T --> set_T)
+                                        $ app pos $ app neg) trunk_arg_Ts
+                   end
+                 else
+                   connective $ pos () $ neg ())
+            end
+          else
+            Const x
+        | t1 $ t2 =>
+          betapply (aux ss Ts [] (skolem_depth + 1) polar t1,
+                    aux ss Ts [] depth Neut t2)
+        | Abs (s, T, t1) => Abs (s, T, aux ss Ts (incrs js) depth polar t1)
+        | _ => t
+      end
+  in aux [] [] [] 0 Pos end
+
+(** Function specialization **)
+
+(* term -> term list *)
+fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2
+  | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
+  | params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) =
+    snd (strip_comb t1)
+  | params_in_equation _ = []
+
+(* styp -> styp -> int list -> term list -> term list -> term -> term *)
+fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t =
+  let
+    val k = fold Integer.max (map maxidx_of_term (fixed_args @ extra_args)) 0
+            + 1
+    val t = map_aterms (fn Var ((s, i), T) => Var ((s, k + i), T) | t' => t') t
+    val fixed_params = filter_indices fixed_js (params_in_equation t)
+    (* term list -> term -> term *)
+    fun aux args (Abs (s, T, t)) = list_comb (Abs (s, T, aux [] t), args)
+      | aux args (t1 $ t2) = aux (aux [] t2 :: args) t1
+      | aux args t =
+        if t = Const x then
+          list_comb (Const x', extra_args @ filter_out_indices fixed_js args)
+        else
+          let val j = find_index (curry (op =) t) fixed_params in
+            list_comb (if j >= 0 then nth fixed_args j else t, args)
+          end
+  in aux [] t end
+
+(* hol_context -> styp -> (int * term option) list *)
+fun static_args_in_term ({ersatz_table, ...} : hol_context) x t =
+  let
+    (* term -> term list -> term list -> term list list *)
+    fun fun_calls (Abs (_, _, t)) _ = fun_calls t []
+      | fun_calls (t1 $ t2) args = fun_calls t2 [] #> fun_calls t1 (t2 :: args)
+      | fun_calls t args =
+        (case t of
+           Const (x' as (s', T')) =>
+           x = x' orelse (case AList.lookup (op =) ersatz_table s' of
+                            SOME s'' => x = (s'', T')
+                          | NONE => false)
+         | _ => false) ? cons args
+    (* term list list -> term list list -> term list -> term list list *)
+    fun call_sets [] [] vs = [vs]
+      | call_sets [] uss vs = vs :: call_sets uss [] []
+      | call_sets ([] :: _) _ _ = []
+      | call_sets ((t :: ts) :: tss) uss vs =
+        OrdList.insert TermOrd.term_ord t vs |> call_sets tss (ts :: uss)
+    val sets = call_sets (fun_calls t [] []) [] []
+    val indexed_sets = sets ~~ (index_seq 0 (length sets))
+  in
+    fold_rev (fn (set, j) =>
+                 case set of
+                   [Var _] => AList.lookup (op =) indexed_sets set = SOME j
+                              ? cons (j, NONE)
+                 | [t as Const _] => cons (j, SOME t)
+                 | [t as Free _] => cons (j, SOME t)
+                 | _ => I) indexed_sets []
+  end
+(* hol_context -> styp -> term list -> (int * term option) list *)
+fun static_args_in_terms hol_ctxt x =
+  map (static_args_in_term hol_ctxt x)
+  #> fold1 (OrdList.inter (prod_ord int_ord (option_ord TermOrd.term_ord)))
+
+(* (int * term option) list -> (int * term) list -> int list *)
+fun overlapping_indices [] _ = []
+  | overlapping_indices _ [] = []
+  | overlapping_indices (ps1 as (j1, t1) :: ps1') (ps2 as (j2, t2) :: ps2') =
+    if j1 < j2 then overlapping_indices ps1' ps2
+    else if j1 > j2 then overlapping_indices ps1 ps2'
+    else overlapping_indices ps1' ps2' |> the_default t2 t1 = t2 ? cons j1
+
+(* typ list -> term -> bool *)
+fun is_eligible_arg Ts t =
+  let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in
+    null bad_Ts orelse
+    (is_higher_order_type (fastype_of1 (Ts, t)) andalso
+     forall (not o is_higher_order_type) bad_Ts)
+  end
+
+(* int -> string *)
+fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep
+
+(* If a constant's definition is picked up deeper than this threshold, we
+   prevent excessive specialization by not specializing it. *)
+val special_max_depth = 20
+
+val bound_var_prefix = "b"
+
+(* hol_context -> int -> term -> term *)
+fun specialize_consts_in_term (hol_ctxt as {thy, specialize, simp_table,
+                                            special_funs, ...}) depth t =
+  if not specialize orelse depth > special_max_depth then
+    t
+  else
+    let
+      val blacklist = if depth = 0 then []
+                      else case term_under_def t of Const x => [x] | _ => []
+      (* term list -> typ list -> term -> term *)
+      fun aux args Ts (Const (x as (s, T))) =
+          ((if not (member (op =) blacklist x) andalso not (null args) andalso
+               not (String.isPrefix special_prefix s) andalso
+               is_equational_fun hol_ctxt x then
+              let
+                val eligible_args = filter (is_eligible_arg Ts o snd)
+                                           (index_seq 0 (length args) ~~ args)
+                val _ = not (null eligible_args) orelse raise SAME ()
+                val old_axs = equational_fun_axioms hol_ctxt x
+                              |> map (destroy_existential_equalities thy)
+                val static_params = static_args_in_terms hol_ctxt x old_axs
+                val fixed_js = overlapping_indices static_params eligible_args
+                val _ = not (null fixed_js) orelse raise SAME ()
+                val fixed_args = filter_indices fixed_js args
+                val vars = fold Term.add_vars fixed_args []
+                           |> sort (TermOrd.fast_indexname_ord o pairself fst)
+                val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js))
+                                    fixed_args []
+                               |> sort int_ord
+                val live_args = filter_out_indices fixed_js args
+                val extra_args = map Var vars @ map Bound bound_js @ live_args
+                val extra_Ts = map snd vars @ filter_indices bound_js Ts
+                val k = maxidx_of_term t + 1
+                (* int -> term *)
+                fun var_for_bound_no j =
+                  Var ((bound_var_prefix ^
+                        nat_subscript (find_index (curry (op =) j) bound_js
+                                       + 1), k),
+                       nth Ts j)
+                val fixed_args_in_axiom =
+                  map (curry subst_bounds
+                             (map var_for_bound_no (index_seq 0 (length Ts))))
+                      fixed_args
+              in
+                case AList.lookup (op =) (!special_funs)
+                                  (x, fixed_js, fixed_args_in_axiom) of
+                  SOME x' => list_comb (Const x', extra_args)
+                | NONE =>
+                  let
+                    val extra_args_in_axiom =
+                      map Var vars @ map var_for_bound_no bound_js
+                    val x' as (s', _) =
+                      (special_prefix_for (length (!special_funs) + 1) ^ s,
+                       extra_Ts @ filter_out_indices fixed_js (binder_types T)
+                       ---> body_type T)
+                    val new_axs =
+                      map (specialize_fun_axiom x x' fixed_js
+                               fixed_args_in_axiom extra_args_in_axiom) old_axs
+                    val _ =
+                      Unsynchronized.change special_funs
+                          (cons ((x, fixed_js, fixed_args_in_axiom), x'))
+                    val _ = add_simps simp_table s' new_axs
+                  in list_comb (Const x', extra_args) end
+              end
+            else
+              raise SAME ())
+           handle SAME () => list_comb (Const x, args))
+        | aux args Ts (Abs (s, T, t)) =
+          list_comb (Abs (s, T, aux [] (T :: Ts) t), args)
+        | aux args Ts (t1 $ t2) = aux (aux [] Ts t2 :: args) Ts t1
+        | aux args _ t = list_comb (t, args)
+    in aux [] [] t end
+
+type special_triple = int list * term list * styp
+
+val cong_var_prefix = "c"
+
+(* styp -> special_triple -> special_triple -> term *)
+fun special_congruence_axiom (s, T) (js1, ts1, x1) (js2, ts2, x2) =
+  let
+    val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2)
+    val Ts = binder_types T
+    val max_j = fold (fold Integer.max) [js1, js2] ~1
+    val (eqs, (args1, args2)) =
+      fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j)
+                                  (js1 ~~ ts1, js2 ~~ ts2) of
+                      (SOME t1, SOME t2) => apfst (cons (t1, t2))
+                    | (SOME t1, NONE) => apsnd (apsnd (cons t1))
+                    | (NONE, SOME t2) => apsnd (apfst (cons t2))
+                    | (NONE, NONE) =>
+                      let val v = Var ((cong_var_prefix ^ nat_subscript j, 0),
+                                       nth Ts j) in
+                        apsnd (pairself (cons v))
+                      end) (max_j downto 0) ([], ([], []))
+  in
+    Logic.list_implies (eqs |> filter_out (op =) |> distinct (op =)
+                            |> map Logic.mk_equals,
+                        Logic.mk_equals (list_comb (Const x1, bounds1 @ args1),
+                                         list_comb (Const x2, bounds2 @ args2)))
+    |> Refute.close_form (* TODO: needed? *)
+  end
+
+(* hol_context -> styp list -> term list *)
+fun special_congruence_axioms (hol_ctxt as {special_funs, ...}) xs =
+  let
+    val groups =
+      !special_funs
+      |> map (fn ((x, js, ts), x') => (x, (js, ts, x')))
+      |> AList.group (op =)
+      |> filter_out (is_equational_fun_surely_complete hol_ctxt o fst)
+      |> map (fn (x, zs) => (x, zs |> member (op =) xs x ? cons ([], [], x)))
+    (* special_triple -> int *)
+    fun generality (js, _, _) = ~(length js)
+    (* special_triple -> special_triple -> bool *)
+    fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
+      x1 <> x2 andalso OrdList.subset (prod_ord int_ord TermOrd.term_ord)
+                                      (j2 ~~ t2, j1 ~~ t1)
+    (* styp -> special_triple list -> special_triple list -> special_triple list
+       -> term list -> term list *)
+    fun do_pass_1 _ [] [_] [_] = I
+      | do_pass_1 x skipped _ [] = do_pass_2 x skipped
+      | do_pass_1 x skipped all (z :: zs) =
+        case filter (is_more_specific z) all
+             |> sort (int_ord o pairself generality) of
+          [] => do_pass_1 x (z :: skipped) all zs
+        | (z' :: _) => cons (special_congruence_axiom x z z')
+                       #> do_pass_1 x skipped all zs
+    (* styp -> special_triple list -> term list -> term list *)
+    and do_pass_2 _ [] = I
+      | do_pass_2 x (z :: zs) =
+        fold (cons o special_congruence_axiom x z) zs #> do_pass_2 x zs
+  in fold (fn (x, zs) => do_pass_1 x [] zs zs) groups [] end
+
+(** Axiom selection **)
+
+(* Similar to "Refute.specialize_type" but returns all matches rather than only
+   the first (preorder) match. *)
+(* theory -> styp -> term -> term list *)
+fun multi_specialize_type thy slack (x as (s, T)) t =
+  let
+    (* term -> (typ * term) list -> (typ * term) list *)
+    fun aux (Const (s', T')) ys =
+        if s = s' then
+          ys |> (if AList.defined (op =) ys T' then
+                   I
+                 else
+                  cons (T', Refute.monomorphic_term
+                                (Sign.typ_match thy (T', T) Vartab.empty) t)
+                  handle Type.TYPE_MATCH => I
+                       | Refute.REFUTE _ =>
+                         if slack then
+                           I
+                         else
+                           raise NOT_SUPPORTED ("too much polymorphism in \
+                                                \axiom involving " ^ quote s))
+        else
+          ys
+      | aux _ ys = ys
+  in map snd (fold_aterms aux t []) end
+
+(* theory -> bool -> const_table -> styp -> term list *)
+fun nondef_props_for_const thy slack table (x as (s, _)) =
+  these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)
+
+(* 'a Symtab.table -> 'a list *)
+fun all_table_entries table = Symtab.fold (append o snd) table []
+(* const_table -> string -> const_table *)
+fun extra_table table s = Symtab.make [(s, all_table_entries table)]
+
+(* int -> term -> term *)
+fun eval_axiom_for_term j t =
+  Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t)
+
+(* term -> bool *)
+val is_trivial_equation = the_default false o try (op aconv o Logic.dest_equals)
+
+(* Prevents divergence in case of cyclic or infinite axiom dependencies. *)
+val axioms_max_depth = 255
+
+(* hol_context -> term -> (term list * term list) * (bool * bool) *)
+fun axioms_for_term
+        (hol_ctxt as {thy, max_bisim_depth, user_axioms, fast_descrs, evals,
+                      def_table, nondef_table, user_nondefs, ...}) t =
+  let
+    type accumulator = styp list * (term list * term list)
+    (* (term list * term list -> term list)
+       -> ((term list -> term list) -> term list * term list
+           -> term list * term list)
+       -> int -> term -> accumulator -> accumulator *)
+    fun add_axiom get app depth t (accum as (xs, axs)) =
+      let
+        val t = t |> unfold_defs_in_term hol_ctxt
+                  |> skolemize_term_and_more hol_ctxt ~1
+      in
+        if is_trivial_equation t then
+          accum
+        else
+          let val t' = t |> specialize_consts_in_term hol_ctxt depth in
+            if exists (member (op aconv) (get axs)) [t, t'] then accum
+            else add_axioms_for_term (depth + 1) t' (xs, app (cons t') axs)
+          end
+      end
+    (* int -> term -> accumulator -> accumulator *)
+    and add_def_axiom depth = add_axiom fst apfst depth
+    and add_nondef_axiom depth = add_axiom snd apsnd depth
+    and add_maybe_def_axiom depth t =
+      (if head_of t <> @{const "==>"} then add_def_axiom
+       else add_nondef_axiom) depth t
+    and add_eq_axiom depth t =
+      (if is_constr_pattern_formula thy t then add_def_axiom
+       else add_nondef_axiom) depth t
+    (* int -> term -> accumulator -> accumulator *)
+    and add_axioms_for_term depth t (accum as (xs, axs)) =
+      case t of
+        t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
+      | Const (x as (s, T)) =>
+        (if member (op =) xs x orelse is_built_in_const fast_descrs x then
+           accum
+         else
+           let val accum as (xs, _) = (x :: xs, axs) in
+             if depth > axioms_max_depth then
+               raise TOO_LARGE ("Nitpick_Preproc.axioms_for_term.\
+                                \add_axioms_for_term",
+                                "too many nested axioms (" ^
+                                string_of_int depth ^ ")")
+             else if Refute.is_const_of_class thy x then
+               let
+                 val class = Logic.class_of_const s
+                 val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]),
+                                                   class)
+                 val ax1 = try (Refute.specialize_type thy x) of_class
+                 val ax2 = Option.map (Refute.specialize_type thy x o snd)
+                                      (Refute.get_classdef thy class)
+               in
+                 fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
+                      accum
+               end
+             else if is_constr thy x then
+               accum
+             else if is_equational_fun hol_ctxt x then
+               fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)
+                    accum
+             else if is_abs_fun thy x then
+               if is_quot_type thy (range_type T) then
+                 raise NOT_SUPPORTED "\"Abs_\" function of quotient type"
+               else
+                 accum |> fold (add_nondef_axiom depth)
+                               (nondef_props_for_const thy false nondef_table x)
+                       |> is_funky_typedef thy (range_type T)
+                          ? fold (add_maybe_def_axiom depth)
+                                 (nondef_props_for_const thy true
+                                                    (extra_table def_table s) x)
+             else if is_rep_fun thy x then
+               if is_quot_type thy (domain_type T) then
+                 raise NOT_SUPPORTED "\"Rep_\" function of quotient type"
+               else
+                 accum |> fold (add_nondef_axiom depth)
+                               (nondef_props_for_const thy false nondef_table x)
+                       |> is_funky_typedef thy (range_type T)
+                          ? fold (add_maybe_def_axiom depth)
+                                 (nondef_props_for_const thy true
+                                                    (extra_table def_table s) x)
+                       |> add_axioms_for_term depth
+                                              (Const (mate_of_rep_fun thy x))
+                       |> fold (add_def_axiom depth)
+                               (inverse_axioms_for_rep_fun thy x)
+             else
+               accum |> user_axioms <> SOME false
+                        ? fold (add_nondef_axiom depth)
+                               (nondef_props_for_const thy false nondef_table x)
+           end)
+        |> add_axioms_for_type depth T
+      | Free (_, T) => add_axioms_for_type depth T accum
+      | Var (_, T) => add_axioms_for_type depth T accum
+      | Bound _ => accum
+      | Abs (_, T, t) => accum |> add_axioms_for_term depth t
+                               |> add_axioms_for_type depth T
+    (* int -> typ -> accumulator -> accumulator *)
+    and add_axioms_for_type depth T =
+      case T of
+        Type ("fun", Ts) => fold (add_axioms_for_type depth) Ts
+      | Type ("*", Ts) => fold (add_axioms_for_type depth) Ts
+      | @{typ prop} => I
+      | @{typ bool} => I
+      | @{typ unit} => I
+      | TFree (_, S) => add_axioms_for_sort depth T S
+      | TVar (_, S) => add_axioms_for_sort depth T S
+      | Type (z as (s, Ts)) =>
+        fold (add_axioms_for_type depth) Ts
+        #> (if is_pure_typedef thy T then
+              fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
+            else if is_quot_type thy T then
+              fold (add_def_axiom depth) (optimized_quot_type_axioms thy z)
+            else if max_bisim_depth >= 0 andalso is_codatatype thy T then
+              fold (add_maybe_def_axiom depth)
+                   (codatatype_bisim_axioms hol_ctxt T)
+            else
+              I)
+    (* int -> typ -> sort -> accumulator -> accumulator *)
+    and add_axioms_for_sort depth T S =
+      let
+        val supers = Sign.complete_sort thy S
+        val class_axioms =
+          maps (fn class => map prop_of (AxClass.get_info thy class |> #axioms
+                                         handle ERROR _ => [])) supers
+        val monomorphic_class_axioms =
+          map (fn t => case Term.add_tvars t [] of
+                         [] => t
+                       | [(x, S)] =>
+                         Refute.monomorphic_term (Vartab.make [(x, (S, T))]) t
+                       | _ => raise TERM ("Nitpick_Preproc.axioms_for_term.\
+                                          \add_axioms_for_sort", [t]))
+              class_axioms
+      in fold (add_nondef_axiom depth) monomorphic_class_axioms end
+    val (mono_user_nondefs, poly_user_nondefs) =
+      List.partition (null o Term.hidden_polymorphism) user_nondefs
+    val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals))
+                           evals
+    val (xs, (defs, nondefs)) =
+      ([], ([], [])) |> add_axioms_for_term 1 t 
+                     |> fold_rev (add_def_axiom 1) eval_axioms
+                     |> user_axioms = SOME true
+                        ? fold (add_nondef_axiom 1) mono_user_nondefs
+    val defs = defs @ special_congruence_axioms hol_ctxt xs
+  in
+    ((defs, nondefs), (user_axioms = SOME true orelse null mono_user_nondefs,
+                       null poly_user_nondefs))
+  end
+
+(** Simplification of constructor/selector terms **)
+
+(* theory -> term -> term *)
+fun simplify_constrs_and_sels thy t =
+  let
+    (* term -> int -> term *)
+    fun is_nth_sel_on t' n (Const (s, _) $ t) =
+        (t = t' andalso is_sel_like_and_no_discr s andalso
+         sel_no_from_name s = n)
+      | is_nth_sel_on _ _ _ = false
+    (* term -> term list -> term *)
+    fun do_term (Const (@{const_name Rep_Frac}, _)
+                 $ (Const (@{const_name Abs_Frac}, _) $ t1)) [] = do_term t1 []
+      | do_term (Const (@{const_name Abs_Frac}, _)
+                 $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 []
+      | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)
+      | do_term (t as Const (x as (s, T))) (args as _ :: _) =
+        ((if is_constr_like thy x then
+            if length args = num_binder_types T then
+              case hd args of
+                Const (x' as (_, T')) $ t' =>
+                if domain_type T' = body_type T andalso
+                   forall (uncurry (is_nth_sel_on t'))
+                          (index_seq 0 (length args) ~~ args) then
+                  t'
+                else
+                  raise SAME ()
+              | _ => raise SAME ()
+            else
+              raise SAME ()
+          else if is_sel_like_and_no_discr s then
+            case strip_comb (hd args) of
+              (Const (x' as (s', T')), ts') =>
+              if is_constr_like thy x' andalso
+                 constr_name_for_sel_like s = s' andalso
+                 not (exists is_pair_type (binder_types T')) then
+                list_comb (nth ts' (sel_no_from_name s), tl args)
+              else
+                raise SAME ()
+            | _ => raise SAME ()
+          else
+            raise SAME ())
+         handle SAME () => betapplys (t, args))
+      | do_term (Abs (s, T, t')) args =
+        betapplys (Abs (s, T, do_term t' []), args)
+      | do_term t args = betapplys (t, args)
+  in do_term t [] end
+
+(** Quantifier massaging: Distributing quantifiers **)
+
+(* term -> term *)
+fun distribute_quantifiers t =
+  case t of
+    (t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) =>
+    (case t1 of
+       (t10 as @{const "op &"}) $ t11 $ t12 =>
+       t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
+           $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
+     | (t10 as @{const Not}) $ t11 =>
+       t10 $ distribute_quantifiers (Const (@{const_name Ex}, T0)
+                                     $ Abs (s, T1, t11))
+     | t1 =>
+       if not (loose_bvar1 (t1, 0)) then
+         distribute_quantifiers (incr_boundvars ~1 t1)
+       else
+         t0 $ Abs (s, T1, distribute_quantifiers t1))
+  | (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) =>
+    (case distribute_quantifiers t1 of
+       (t10 as @{const "op |"}) $ t11 $ t12 =>
+       t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
+           $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
+     | (t10 as @{const "op -->"}) $ t11 $ t12 =>
+       t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
+                                     $ Abs (s, T1, t11))
+           $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
+     | (t10 as @{const Not}) $ t11 =>
+       t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
+                                     $ Abs (s, T1, t11))
+     | t1 =>
+       if not (loose_bvar1 (t1, 0)) then
+         distribute_quantifiers (incr_boundvars ~1 t1)
+       else
+         t0 $ Abs (s, T1, distribute_quantifiers t1))
+  | t1 $ t2 => distribute_quantifiers t1 $ distribute_quantifiers t2
+  | Abs (s, T, t') => Abs (s, T, distribute_quantifiers t')
+  | _ => t
+
+(** Quantifier massaging: Pushing quantifiers inward **)
+
+(* int -> int -> (int -> int) -> term -> term *)
+fun renumber_bounds j n f t =
+  case t of
+    t1 $ t2 => renumber_bounds j n f t1 $ renumber_bounds j n f t2
+  | Abs (s, T, t') => Abs (s, T, renumber_bounds (j + 1) n f t')
+  | Bound j' =>
+    Bound (if j' >= j andalso j' < j + n then f (j' - j) + j else j')
+  | _ => t
+
+(* Maximum number of quantifiers in a cluster for which the exponential
+   algorithm is used. Larger clusters use a heuristic inspired by Claessen &
+   Sörensson's polynomial binary splitting procedure (p. 5 of their MODEL 2003
+   paper). *)
+val quantifier_cluster_threshold = 7
+
+(* theory -> term -> term *)
+fun push_quantifiers_inward thy =
+  let
+    (* string -> string list -> typ list -> term -> term *)
+    fun aux quant_s ss Ts t =
+      (case t of
+         (t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) =>
+         if s0 = quant_s then
+           aux s0 (s1 :: ss) (T1 :: Ts) t1
+         else if quant_s = "" andalso
+                 (s0 = @{const_name All} orelse s0 = @{const_name Ex}) then
+           aux s0 [s1] [T1] t1
+         else
+           raise SAME ()
+       | _ => raise SAME ())
+      handle SAME () =>
+             case t of
+               t1 $ t2 =>
+               if quant_s = "" then
+                 aux "" [] [] t1 $ aux "" [] [] t2
+               else
+                 let
+                   val typical_card = 4
+                   (* ('a -> ''b list) -> 'a list -> ''b list *)
+                   fun big_union proj ps =
+                     fold (fold (insert (op =)) o proj) ps []
+                   val (ts, connective) = strip_any_connective t
+                   val T_costs =
+                     map (bounded_card_of_type 65536 typical_card []) Ts
+                   val t_costs = map size_of_term ts
+                   val num_Ts = length Ts
+                   (* int -> int *)
+                   val flip = curry (op -) (num_Ts - 1)
+                   val t_boundss = map (map flip o loose_bnos) ts
+                   (* (int list * int) list -> int list
+                      -> (int list * int) list *)
+                   fun merge costly_boundss [] = costly_boundss
+                     | merge costly_boundss (j :: js) =
+                       let
+                         val (yeas, nays) =
+                           List.partition (fn (bounds, _) =>
+                                              member (op =) bounds j)
+                                          costly_boundss
+                         val yeas_bounds = big_union fst yeas
+                         val yeas_cost = Integer.sum (map snd yeas)
+                                         * nth T_costs j
+                       in merge ((yeas_bounds, yeas_cost) :: nays) js end
+                   (* (int list * int) list -> int list -> int *)
+                   val cost = Integer.sum o map snd oo merge
+                   (* (int list * int) list -> int list -> int list *)
+                   fun heuristically_best_permutation _ [] = []
+                     | heuristically_best_permutation costly_boundss js =
+                       let
+                         val (costly_boundss, (j, js)) =
+                           js |> map (`(merge costly_boundss o single))
+                              |> sort (int_ord
+                                       o pairself (Integer.sum o map snd o fst))
+                              |> split_list |>> hd ||> pairf hd tl
+                       in
+                         j :: heuristically_best_permutation costly_boundss js
+                       end
+                   val js =
+                     if length Ts <= quantifier_cluster_threshold then
+                       all_permutations (index_seq 0 num_Ts)
+                       |> map (`(cost (t_boundss ~~ t_costs)))
+                       |> sort (int_ord o pairself fst) |> hd |> snd
+                     else
+                       heuristically_best_permutation (t_boundss ~~ t_costs)
+                                                      (index_seq 0 num_Ts)
+                   val back_js = map (fn j => find_index (curry (op =) j) js)
+                                     (index_seq 0 num_Ts)
+                   val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip))
+                                ts
+                   (* (term * int list) list -> term *)
+                   fun mk_connection [] =
+                       raise ARG ("Nitpick_Preproc.push_quantifiers_inward.aux.\
+                                  \mk_connection", "")
+                     | mk_connection ts_cum_bounds =
+                       ts_cum_bounds |> map fst
+                       |> foldr1 (fn (t1, t2) => connective $ t1 $ t2)
+                   (* (term * int list) list -> int list -> term *)
+                   fun build ts_cum_bounds [] = ts_cum_bounds |> mk_connection
+                     | build ts_cum_bounds (j :: js) =
+                       let
+                         val (yeas, nays) =
+                           List.partition (fn (_, bounds) =>
+                                              member (op =) bounds j)
+                                          ts_cum_bounds
+                           ||> map (apfst (incr_boundvars ~1))
+                       in
+                         if null yeas then
+                           build nays js
+                         else
+                           let val T = nth Ts (flip j) in
+                             build ((Const (quant_s, (T --> bool_T) --> bool_T)
+                                     $ Abs (nth ss (flip j), T,
+                                            mk_connection yeas),
+                                      big_union snd yeas) :: nays) js
+                           end
+                       end
+                 in build (ts ~~ t_boundss) js end
+             | Abs (s, T, t') => Abs (s, T, aux "" [] [] t')
+             | _ => t
+  in aux "" [] [] end
+
+(** Preprocessor entry point **)
+
+(* hol_context -> term -> ((term list * term list) * (bool * bool)) * term *)
+fun preprocess_term (hol_ctxt as {thy, binary_ints, destroy_constrs, boxes,
+                                  skolemize, uncurry, ...}) t =
+  let
+    val skolem_depth = if skolemize then 4 else ~1
+    val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
+         core_t) = t |> unfold_defs_in_term hol_ctxt
+                     |> Refute.close_form
+                     |> skolemize_term_and_more hol_ctxt skolem_depth
+                     |> specialize_consts_in_term hol_ctxt 0
+                     |> `(axioms_for_term hol_ctxt)
+    val binarize =
+      case binary_ints of
+        SOME false => false
+      | _ =>
+        forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
+        (binary_ints = SOME true orelse
+         exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
+    val box = exists (not_equal (SOME false) o snd) boxes
+    val table =
+      Termtab.empty |> uncurry
+        ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts)
+    (* bool -> bool -> term -> term *)
+    fun do_rest def core =
+      binarize ? binarize_nat_and_int_in_term
+      #> uncurry ? uncurry_term table
+      #> box ? box_fun_and_pair_in_term hol_ctxt def
+      #> destroy_constrs ? (pull_out_universal_constrs thy def
+                            #> pull_out_existential_constrs thy
+                            #> destroy_pulled_out_constrs hol_ctxt def)
+      #> curry_assms
+      #> destroy_universal_equalities
+      #> destroy_existential_equalities thy
+      #> simplify_constrs_and_sels thy
+      #> distribute_quantifiers
+      #> push_quantifiers_inward thy
+      #> not core ? Refute.close_form
+      #> Term.map_abs_vars shortest_name
+  in
+    (((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts),
+      (got_all_mono_user_axioms, no_poly_user_axioms)),
+     do_rest false true core_t)
+  end
+
+end;