src/HOL/Tools/Nitpick/nitpick_preproc.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (24 months ago)
changeset 66695 91500c024c7f
parent 61770 a20048c78891
child 69593 3dda49e08b9d
permissions -rw-r--r--
tuned;
     1 (*  Title:      HOL/Tools/Nitpick/nitpick_preproc.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2008, 2009, 2010
     4 
     5 Nitpick's HOL preprocessor.
     6 *)
     7 
     8 signature NITPICK_PREPROC =
     9 sig
    10   type hol_context = Nitpick_HOL.hol_context
    11   val preprocess_formulas :
    12     hol_context -> term list -> term
    13     -> term list * term list * term list * bool * bool * bool
    14 end;
    15 
    16 structure Nitpick_Preproc : NITPICK_PREPROC =
    17 struct
    18 
    19 open Nitpick_Util
    20 open Nitpick_HOL
    21 open Nitpick_Mono
    22 
    23 fun is_positive_existential polar quant_s =
    24   (polar = Pos andalso quant_s = @{const_name Ex}) orelse
    25   (polar = Neg andalso quant_s <> @{const_name Ex})
    26 
    27 val is_descr =
    28   member (op =) [@{const_name The}, @{const_name Eps}, @{const_name safe_The}]
    29 
    30 (** Binary coding of integers **)
    31 
    32 (* If a formula contains a numeral whose absolute value is more than this
    33    threshold, the unary coding is likely not to work well and we prefer the
    34    binary coding. *)
    35 val binary_int_threshold = 3
    36 
    37 val may_use_binary_ints =
    38   let
    39     fun aux def (Const (@{const_name Pure.eq}, _) $ t1 $ t2) =
    40         aux def t1 andalso aux false t2
    41       | aux def (@{const Pure.imp} $ t1 $ t2) = aux false t1 andalso aux def t2
    42       | aux def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) =
    43         aux def t1 andalso aux false t2
    44       | aux def (@{const HOL.implies} $ t1 $ t2) = aux false t1 andalso aux def t2
    45       | aux def (t1 $ t2) = aux def t1 andalso aux def t2
    46       | aux def (t as Const (s, _)) =
    47         (not def orelse t <> @{const Suc}) andalso
    48         not (member (op =)
    49                [@{const_name Abs_Frac}, @{const_name Rep_Frac},
    50                 @{const_name nat_gcd}, @{const_name nat_lcm},
    51                 @{const_name Frac}, @{const_name norm_frac}] s)
    52       | aux def (Abs (_, _, t')) = aux def t'
    53       | aux _ _ = true
    54   in aux end
    55 val should_use_binary_ints =
    56   let
    57     fun aux (t1 $ t2) = aux t1 orelse aux t2
    58       | aux (Const (s, T)) =
    59         ((s = @{const_name times} orelse s = @{const_name Rings.divide}) andalso
    60          is_integer_type (body_type T)) orelse
    61         (String.isPrefix numeral_prefix s andalso
    62          let val n = the (Int.fromString (unprefix numeral_prefix s)) in
    63            n < ~ binary_int_threshold orelse n > binary_int_threshold
    64          end)
    65       | aux (Abs (_, _, t')) = aux t'
    66       | aux _ = false
    67   in aux end
    68 
    69 (** Uncurrying **)
    70 
    71 fun add_to_uncurry_table ctxt t =
    72   let
    73     fun aux (t1 $ t2) args table =
    74         let val table = aux t2 [] table in aux t1 (t2 :: args) table end
    75       | aux (Abs (_, _, t')) _ table = aux t' [] table
    76       | aux (t as Const (x as (s, _))) args table =
    77         if is_built_in_const x orelse is_nonfree_constr ctxt x orelse
    78            is_sel s orelse s = @{const_name Sigma} then
    79           table
    80         else
    81           Termtab.map_default (t, 65536) (Integer.min (length args)) table
    82       | aux _ _ table = table
    83   in aux t [] end
    84 
    85 fun uncurry_prefix_for k j =
    86   uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
    87 
    88 fun uncurry_term table t =
    89   let
    90     fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args)
    91       | aux (Abs (s, T, t')) args = s_betapplys [] (Abs (s, T, aux t' []), args)
    92       | aux (t as Const (s, T)) args =
    93         (case Termtab.lookup table t of
    94            SOME n =>
    95            if n >= 2 then
    96              let
    97                val arg_Ts = strip_n_binders n T |> fst
    98                val j =
    99                  if is_iterator_type (hd arg_Ts) then
   100                    1
   101                  else case find_index (not_equal bool_T) arg_Ts of
   102                    ~1 => n
   103                  | j => j
   104                val ((before_args, tuple_args), after_args) =
   105                  args |> chop n |>> chop j
   106                val ((before_arg_Ts, tuple_arg_Ts), rest_T) =
   107                  T |> strip_n_binders n |>> chop j
   108                val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
   109              in
   110                if n - j < 2 then
   111                  s_betapplys [] (t, args)
   112                else
   113                  s_betapplys []
   114                      (Const (uncurry_prefix_for (n - j) j ^ s,
   115                              before_arg_Ts ---> tuple_T --> rest_T),
   116                       before_args @ [mk_flat_tuple tuple_T tuple_args] @
   117                       after_args)
   118              end
   119            else
   120              s_betapplys [] (t, args)
   121          | NONE => s_betapplys [] (t, args))
   122       | aux t args = s_betapplys [] (t, args)
   123   in aux t [] end
   124 
   125 (** Boxing **)
   126 
   127 fun box_fun_and_pair_in_term (hol_ctxt as {ctxt, ...}) def orig_t =
   128   let
   129     fun box_relational_operator_type (Type (@{type_name fun}, Ts)) =
   130         Type (@{type_name fun}, map box_relational_operator_type Ts)
   131       | box_relational_operator_type (Type (@{type_name prod}, Ts)) =
   132         Type (@{type_name prod}, map (box_type hol_ctxt InPair) Ts)
   133       | box_relational_operator_type T = T
   134     fun add_boxed_types_for_var (z as (_, T)) (T', t') =
   135       case t' of
   136         Var z' => z' = z ? insert (op =) T'
   137       | Const (@{const_name Pair}, _) $ t1 $ t2 =>
   138         (case T' of
   139            Type (_, [T1, T2]) =>
   140            fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)]
   141          | _ => raise TYPE ("Nitpick_Preproc.box_fun_and_pair_in_term.\
   142                             \add_boxed_types_for_var", [T'], []))
   143       | _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T
   144     fun box_var_in_def new_Ts old_Ts t (z as (_, T)) =
   145       case t of
   146         @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
   147       | Const (s0, _) $ t1 $ _ =>
   148         if s0 = @{const_name Pure.eq} orelse s0 = @{const_name HOL.eq} then
   149           let
   150             val (t', args) = strip_comb t1
   151             val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
   152           in
   153             case fold (add_boxed_types_for_var z)
   154                       (fst (strip_n_binders (length args) T') ~~ args) [] of
   155               [T''] => T''
   156             | _ => T
   157           end
   158         else
   159           T
   160       | _ => T
   161     and do_quantifier new_Ts old_Ts polar quant_s quant_T abs_s abs_T t =
   162       let
   163         val abs_T' =
   164           if polar = Neut orelse is_positive_existential polar quant_s then
   165             box_type hol_ctxt InFunLHS abs_T
   166           else
   167             abs_T
   168         val body_T = body_type quant_T
   169       in
   170         Const (quant_s, (abs_T' --> body_T) --> body_T)
   171         $ Abs (abs_s, abs_T',
   172                t |> do_term (abs_T' :: new_Ts) (abs_T :: old_Ts) polar)
   173       end
   174     and do_equals new_Ts old_Ts s0 T0 t1 t2 =
   175       let
   176         val (t1, t2) = apply2 (do_term new_Ts old_Ts Neut) (t1, t2)
   177         val (T1, T2) = apply2 (curry fastype_of1 new_Ts) (t1, t2)
   178         val T = if def then T1 else [T1, T2] |> sort (int_ord o apply2 size_of_typ) |> hd
   179       in
   180         list_comb (Const (s0, T --> T --> body_type T0),
   181                    map2 (coerce_term hol_ctxt new_Ts T) [T1, T2] [t1, t2])
   182       end
   183     and do_descr s T =
   184       let val T1 = box_type hol_ctxt InFunLHS (range_type T) in
   185         Const (s, (T1 --> bool_T) --> T1)
   186       end
   187     and do_term new_Ts old_Ts polar t =
   188       case t of
   189         Const (s0 as @{const_name Pure.all}, T0) $ Abs (s1, T1, t1) =>
   190         do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
   191       | Const (s0 as @{const_name Pure.eq}, T0) $ t1 $ t2 =>
   192         do_equals new_Ts old_Ts s0 T0 t1 t2
   193       | @{const Pure.imp} $ t1 $ t2 =>
   194         @{const Pure.imp} $ do_term new_Ts old_Ts (flip_polarity polar) t1
   195         $ do_term new_Ts old_Ts polar t2
   196       | @{const Pure.conjunction} $ t1 $ t2 =>
   197         @{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1
   198         $ do_term new_Ts old_Ts polar t2
   199       | @{const Trueprop} $ t1 =>
   200         @{const Trueprop} $ do_term new_Ts old_Ts polar t1
   201       | @{const Not} $ t1 =>
   202         @{const Not} $ do_term new_Ts old_Ts (flip_polarity polar) t1
   203       | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
   204         do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
   205       | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
   206         do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
   207       | Const (s0 as @{const_name HOL.eq}, T0) $ t1 $ t2 =>
   208         do_equals new_Ts old_Ts s0 T0 t1 t2
   209       | @{const HOL.conj} $ t1 $ t2 =>
   210         @{const HOL.conj} $ do_term new_Ts old_Ts polar t1
   211         $ do_term new_Ts old_Ts polar t2
   212       | @{const HOL.disj} $ t1 $ t2 =>
   213         @{const HOL.disj} $ do_term new_Ts old_Ts polar t1
   214         $ do_term new_Ts old_Ts polar t2
   215       | @{const HOL.implies} $ t1 $ t2 =>
   216         @{const HOL.implies} $ do_term new_Ts old_Ts (flip_polarity polar) t1
   217         $ do_term new_Ts old_Ts polar t2
   218       | Const (x as (s, T)) =>
   219         if is_descr s then
   220           do_descr s T
   221         else
   222           Const (s, if s = @{const_name converse} orelse
   223                        s = @{const_name trancl} then
   224                       box_relational_operator_type T
   225                     else if String.isPrefix quot_normal_prefix s then
   226                       let val T' = box_type hol_ctxt InFunLHS (domain_type T) in
   227                         T' --> T'
   228                       end
   229                     else if is_built_in_const x orelse
   230                             s = @{const_name Sigma} then
   231                       T
   232                     else if is_nonfree_constr ctxt x then
   233                       box_type hol_ctxt InConstr T
   234                     else if is_sel s orelse is_rep_fun ctxt x then
   235                       box_type hol_ctxt InSel T
   236                     else
   237                       box_type hol_ctxt InExpr T)
   238       | t1 $ Abs (s, T, t2') =>
   239         let
   240           val t1 = do_term new_Ts old_Ts Neut t1
   241           val T1 = fastype_of1 (new_Ts, t1)
   242           val (s1, Ts1) = dest_Type T1
   243           val T' = hd (snd (dest_Type (hd Ts1)))
   244           val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2')
   245           val T2 = fastype_of1 (new_Ts, t2)
   246           val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2
   247         in
   248           s_betapply new_Ts (if s1 = @{type_name fun} then
   249                                t1
   250                              else
   251                                select_nth_constr_arg ctxt
   252                                    (@{const_name FunBox},
   253                                     Type (@{type_name fun}, Ts1) --> T1) t1 0
   254                                    (Type (@{type_name fun}, Ts1)), t2)
   255         end
   256       | t1 $ t2 =>
   257         let
   258           val t1 = do_term new_Ts old_Ts Neut t1
   259           val T1 = fastype_of1 (new_Ts, t1)
   260           val (s1, Ts1) = dest_Type T1
   261           val t2 = do_term new_Ts old_Ts Neut t2
   262           val T2 = fastype_of1 (new_Ts, t2)
   263           val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2
   264         in
   265           s_betapply new_Ts (if s1 = @{type_name fun} then
   266                                t1
   267                              else
   268                                select_nth_constr_arg ctxt
   269                                    (@{const_name FunBox},
   270                                     Type (@{type_name fun}, Ts1) --> T1) t1 0
   271                                    (Type (@{type_name fun}, Ts1)), t2)
   272         end
   273       | Free (s, T) => Free (s, box_type hol_ctxt InExpr T)
   274       | Var (z as (x, T)) =>
   275         Var (x, if def then box_var_in_def new_Ts old_Ts orig_t z
   276                 else box_type hol_ctxt InExpr T)
   277       | Bound _ => t
   278       | Abs (s, T, t') =>
   279         Abs (s, T, do_term (T :: new_Ts) (T :: old_Ts) Neut t')
   280   in do_term [] [] Pos orig_t end
   281 
   282 (** Destruction of set membership and comprehensions **)
   283 
   284 fun destroy_set_Collect (Const (@{const_name Set.member}, _) $ t1
   285                          $ (Const (@{const_name Collect}, _) $ t2)) =
   286     destroy_set_Collect (t2 $ t1)
   287   | destroy_set_Collect (t1 $ t2) =
   288     destroy_set_Collect t1 $ destroy_set_Collect t2
   289   | destroy_set_Collect (Abs (s, T, t')) = Abs (s, T, destroy_set_Collect t')
   290   | destroy_set_Collect t = t
   291 
   292 (** Destruction of constructors **)
   293 
   294 val val_var_prefix = nitpick_prefix ^ "v"
   295 
   296 fun fresh_value_var Ts k n j t =
   297   Var ((val_var_prefix ^ nat_subscript (n - j), k), fastype_of1 (Ts, t))
   298 
   299 fun has_heavy_bounds_or_vars Ts t =
   300   let
   301     fun aux [] = false
   302       | aux [T] = is_fun_or_set_type T orelse is_pair_type T
   303       | aux _ = true
   304   in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
   305 
   306 fun pull_out_constr_comb ({ctxt, ...} : hol_context) Ts relax k level t args
   307                          seen =
   308   let val t_comb = list_comb (t, args) in
   309     case t of
   310       Const x =>
   311       if not relax andalso is_constr ctxt x andalso
   312          not (is_fun_or_set_type (fastype_of1 (Ts, t_comb))) andalso
   313          has_heavy_bounds_or_vars Ts t_comb andalso
   314          not (loose_bvar (t_comb, level)) then
   315         let
   316           val (j, seen) = case find_index (curry (op =) t_comb) seen of
   317                             ~1 => (0, t_comb :: seen)
   318                           | j => (j, seen)
   319         in (fresh_value_var Ts k (length seen) j t_comb, seen) end
   320       else
   321         (t_comb, seen)
   322     | _ => (t_comb, seen)
   323   end
   324 
   325 fun equations_for_pulled_out_constrs mk_eq Ts k seen =
   326   let val n = length seen in
   327     map2 (fn j => fn t => mk_eq (fresh_value_var Ts k n j t, t))
   328          (index_seq 0 n) seen
   329   end
   330 
   331 fun pull_out_universal_constrs hol_ctxt def t =
   332   let
   333     val k = maxidx_of_term t + 1
   334     fun do_term Ts def t args seen =
   335       case t of
   336         (t0 as Const (@{const_name Pure.eq}, _)) $ t1 $ t2 =>
   337         do_eq_or_imp Ts true def t0 t1 t2 seen
   338       | (t0 as @{const Pure.imp}) $ t1 $ t2 =>
   339         if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
   340       | (t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
   341         do_eq_or_imp Ts true def t0 t1 t2 seen
   342       | (t0 as @{const HOL.implies}) $ t1 $ t2 =>
   343         do_eq_or_imp Ts false def t0 t1 t2 seen
   344       | Abs (s, T, t') =>
   345         let val (t', seen) = do_term (T :: Ts) def t' [] seen in
   346           (list_comb (Abs (s, T, t'), args), seen)
   347         end
   348       | t1 $ t2 =>
   349         let val (t2, seen) = do_term Ts def t2 [] seen in
   350           do_term Ts def t1 (t2 :: args) seen
   351         end
   352       | _ => pull_out_constr_comb hol_ctxt Ts def k 0 t args seen
   353     and do_eq_or_imp Ts eq def t0 t1 t2 seen =
   354       let
   355         val (t2, seen) = if eq andalso def then (t2, seen)
   356                          else do_term Ts false t2 [] seen
   357         val (t1, seen) = do_term Ts false t1 [] seen
   358       in (t0 $ t1 $ t2, seen) end
   359     val (concl, seen) = do_term [] def t [] []
   360   in
   361     Logic.list_implies (equations_for_pulled_out_constrs Logic.mk_equals [] k
   362                                                          seen, concl)
   363   end
   364 
   365 fun mk_exists v t =
   366   HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)
   367 
   368 fun pull_out_existential_constrs hol_ctxt t =
   369   let
   370     val k = maxidx_of_term t + 1
   371     fun aux Ts num_exists t args seen =
   372       case t of
   373         (t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1) =>
   374         let
   375           val (t1, seen') = aux (T1 :: Ts) (num_exists + 1) t1 [] []
   376           val n = length seen'
   377           fun vars () = map2 (fresh_value_var Ts k n) (index_seq 0 n) seen'
   378         in
   379           (equations_for_pulled_out_constrs HOLogic.mk_eq Ts k seen'
   380            |> List.foldl s_conj t1 |> fold mk_exists (vars ())
   381            |> curry3 Abs s1 T1 |> curry (op $) t0, seen)
   382         end
   383       | t1 $ t2 =>
   384         let val (t2, seen) = aux Ts num_exists t2 [] seen in
   385           aux Ts num_exists t1 (t2 :: args) seen
   386         end
   387       | Abs (s, T, t') =>
   388         let
   389           val (t', seen) = aux (T :: Ts) 0 t' [] (map (incr_boundvars 1) seen)
   390         in (list_comb (Abs (s, T, t'), args), map (incr_boundvars ~1) seen) end
   391       | _ =>
   392         if num_exists > 0 then
   393           pull_out_constr_comb hol_ctxt Ts false k num_exists t args seen
   394         else
   395           (list_comb (t, args), seen)
   396   in aux [] 0 t [] [] |> fst end
   397 
   398 fun destroy_pulled_out_constrs (hol_ctxt as {ctxt, ...}) axiom strong t =
   399   let
   400     val num_occs_of_var =
   401       fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
   402                     | _ => I) t (K 0)
   403     fun aux Ts careful ((t0 as Const (@{const_name Pure.eq}, _)) $ t1 $ t2) =
   404         aux_eq Ts careful true t0 t1 t2
   405       | aux Ts careful ((t0 as @{const Pure.imp}) $ t1 $ t2) =
   406         t0 $ aux Ts false t1 $ aux Ts careful t2
   407       | aux Ts careful ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2) =
   408         aux_eq Ts careful true t0 t1 t2
   409       | aux Ts careful ((t0 as @{const HOL.implies}) $ t1 $ t2) =
   410         t0 $ aux Ts false t1 $ aux Ts careful t2
   411       | aux Ts careful (Abs (s, T, t')) = Abs (s, T, aux (T :: Ts) careful t')
   412       | aux Ts careful (t1 $ t2) = aux Ts careful t1 $ aux Ts careful t2
   413       | aux _ _ t = t
   414     and aux_eq Ts careful pass1 t0 t1 t2 =
   415       ((if careful orelse
   416            not (strong orelse forall (is_constr_pattern ctxt) [t1, t2]) then
   417           raise SAME ()
   418         else if axiom andalso is_Var t2 andalso
   419                 num_occs_of_var (dest_Var t2) = 1 then
   420           @{const True}
   421         else case strip_comb t2 of
   422           (* The first case is not as general as it could be. *)
   423           (Const (@{const_name PairBox}, _),
   424                   [Const (@{const_name fst}, _) $ Var z1,
   425                    Const (@{const_name snd}, _) $ Var z2]) =>
   426           if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True}
   427           else raise SAME ()
   428         | (Const (x as (s, T)), args) =>
   429           let
   430             val (arg_Ts, dataT) = strip_type T
   431             val n = length arg_Ts
   432           in
   433             if length args = n andalso
   434                (is_constr ctxt x orelse s = @{const_name Pair} orelse
   435                 x = (@{const_name Suc}, nat_T --> nat_T)) andalso
   436                (not careful orelse not (is_Var t1) orelse
   437                 String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
   438                 s_let Ts "l" (n + 1) dataT bool_T
   439                       (fn t1 =>
   440                           discriminate_value hol_ctxt x t1 ::
   441                           @{map 3} (sel_eq Ts x t1) (index_seq 0 n) arg_Ts args
   442                           |> foldr1 s_conj) t1
   443             else
   444               raise SAME ()
   445           end
   446         | _ => raise SAME ())
   447        |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop)
   448       handle SAME () => if pass1 then aux_eq Ts careful false t0 t2 t1
   449                         else t0 $ aux Ts false t2 $ aux Ts false t1
   450     and sel_eq Ts x t n nth_T nth_t =
   451       HOLogic.eq_const nth_T $ nth_t $ select_nth_constr_arg ctxt x t n nth_T
   452       |> aux Ts false
   453   in aux [] axiom t end
   454 
   455 (** Destruction of universal and existential equalities **)
   456 
   457 fun curry_assms (@{const Pure.imp} $ (@{const Trueprop}
   458                                    $ (@{const HOL.conj} $ t1 $ t2)) $ t3) =
   459     curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
   460   | curry_assms (@{const Pure.imp} $ t1 $ t2) =
   461     @{const Pure.imp} $ curry_assms t1 $ curry_assms t2
   462   | curry_assms t = t
   463 
   464 val destroy_universal_equalities =
   465   let
   466     fun aux prems zs t =
   467       case t of
   468         @{const Pure.imp} $ t1 $ t2 => aux_implies prems zs t1 t2
   469       | _ => Logic.list_implies (rev prems, t)
   470     and aux_implies prems zs t1 t2 =
   471       case t1 of
   472         Const (@{const_name Pure.eq}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
   473       | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ Var z $ t') =>
   474         aux_eq prems zs z t' t1 t2
   475       | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t' $ Var z) =>
   476         aux_eq prems zs z t' t1 t2
   477       | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
   478     and aux_eq prems zs z t' t1 t2 =
   479       if not (member (op =) zs z) andalso
   480          not (exists_subterm (curry (op =) (Var z)) t') then
   481         aux prems zs (subst_free [(Var z, t')] t2)
   482       else
   483         aux (t1 :: prems) (Term.add_vars t1 zs) t2
   484   in aux [] [] end
   485 
   486 fun find_bound_assign ctxt j =
   487   let
   488     fun do_term _ [] = NONE
   489       | do_term seen (t :: ts) =
   490         let
   491           fun do_eq pass1 t1 t2 =
   492             (if loose_bvar1 (t2, j) then
   493                if pass1 then do_eq false t2 t1 else raise SAME ()
   494              else case t1 of
   495                Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()
   496              | Const (s, Type (@{type_name fun}, [T1, T2])) $ Bound j' =>
   497                if j' = j andalso
   498                   s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then
   499                  SOME (construct_value ctxt
   500                                        (@{const_name FunBox}, T2 --> T1) [t2],
   501                        ts @ seen)
   502                else
   503                  raise SAME ()
   504              | _ => raise SAME ())
   505             handle SAME () => do_term (t :: seen) ts
   506         in
   507           case t of
   508             Const (@{const_name HOL.eq}, _) $ t1 $ t2 => do_eq true t1 t2
   509           | _ => do_term (t :: seen) ts
   510         end
   511   in do_term end
   512 
   513 fun subst_one_bound j arg t =
   514   let
   515     fun aux (Bound i, lev) =
   516         if i < lev then raise SAME ()
   517         else if i = lev then incr_boundvars (lev - j) arg
   518         else Bound (i - 1)
   519       | aux (Abs (a, T, body), lev) = Abs (a, T, aux (body, lev + 1))
   520       | aux (f $ t, lev) =
   521         (aux (f, lev) $ (aux (t, lev) handle SAME () => t)
   522          handle SAME () => f $ aux (t, lev))
   523       | aux _ = raise SAME ()
   524   in aux (t, j) handle SAME () => t end
   525 
   526 fun destroy_existential_equalities ({ctxt, ...} : hol_context) =
   527   let
   528     fun kill [] [] ts = foldr1 s_conj ts
   529       | kill (s :: ss) (T :: Ts) ts =
   530         (case find_bound_assign ctxt (length ss) [] ts of
   531            SOME (_, []) => @{const True}
   532          | SOME (arg_t, ts) =>
   533            kill ss Ts (map (subst_one_bound (length ss)
   534                                 (incr_bv (~1, length ss + 1, arg_t))) ts)
   535          | NONE =>
   536            Const (@{const_name Ex}, (T --> bool_T) --> bool_T)
   537            $ Abs (s, T, kill ss Ts ts))
   538       | kill _ _ _ = raise ListPair.UnequalLengths
   539     fun gather ss Ts (Const (@{const_name Ex}, _) $ Abs (s1, T1, t1)) =
   540         gather (ss @ [s1]) (Ts @ [T1]) t1
   541       | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)
   542       | gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2
   543       | gather [] [] t = t
   544       | gather ss Ts t = kill ss Ts (conjuncts_of (gather [] [] t))
   545   in gather [] [] end
   546 
   547 (** Skolemization **)
   548 
   549 fun skolem_prefix_for k j =
   550   skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
   551 
   552 fun skolemize_term_and_more (hol_ctxt as {thy, def_tables, skolems, ...})
   553                             skolem_depth =
   554   let
   555     val incrs = map (Integer.add 1)
   556     fun aux ss Ts js skolemizable polar t =
   557       let
   558         fun do_quantifier quant_s quant_T abs_s abs_T t =
   559           (if not (loose_bvar1 (t, 0)) then
   560              aux ss Ts js skolemizable polar (incr_boundvars ~1 t)
   561            else if is_positive_existential polar quant_s then
   562              let
   563                val j = length (!skolems) + 1
   564              in
   565                if skolemizable andalso length js <= skolem_depth then
   566                  let
   567                    val sko_s = skolem_prefix_for (length js) j ^ abs_s
   568                    val _ = Unsynchronized.change skolems (cons (sko_s, ss))
   569                    val sko_t = list_comb (Const (sko_s, rev Ts ---> abs_T),
   570                                           map Bound (rev js))
   571                    val abs_t = Abs (abs_s, abs_T,
   572                                     aux ss Ts (incrs js) skolemizable polar t)
   573                  in
   574                    if null js then
   575                      s_betapply Ts (abs_t, sko_t)
   576                    else
   577                      Const (@{const_name Let}, abs_T --> quant_T) $ sko_t
   578                      $ abs_t
   579                  end
   580                else
   581                  raise SAME ()
   582              end
   583            else
   584              raise SAME ())
   585           handle SAME () =>
   586                  Const (quant_s, quant_T)
   587                  $ Abs (abs_s, abs_T,
   588                         aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js)
   589                             (skolemizable andalso
   590                              not (is_higher_order_type abs_T)) polar t)
   591       in
   592         case t of
   593           Const (s0 as @{const_name Pure.all}, T0) $ Abs (s1, T1, t1) =>
   594           do_quantifier s0 T0 s1 T1 t1
   595         | @{const Pure.imp} $ t1 $ t2 =>
   596           @{const Pure.imp} $ aux ss Ts js skolemizable (flip_polarity polar) t1
   597           $ aux ss Ts js skolemizable polar t2
   598         | @{const Pure.conjunction} $ t1 $ t2 =>
   599           @{const Pure.conjunction} $ aux ss Ts js skolemizable polar t1
   600           $ aux ss Ts js skolemizable polar t2
   601         | @{const Trueprop} $ t1 =>
   602           @{const Trueprop} $ aux ss Ts js skolemizable polar t1
   603         | @{const Not} $ t1 =>
   604           @{const Not} $ aux ss Ts js skolemizable (flip_polarity polar) t1
   605         | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
   606           do_quantifier s0 T0 s1 T1 t1
   607         | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
   608           do_quantifier s0 T0 s1 T1 t1
   609         | @{const HOL.conj} $ t1 $ t2 =>
   610           s_conj (apply2 (aux ss Ts js skolemizable polar) (t1, t2))
   611         | @{const HOL.disj} $ t1 $ t2 =>
   612           s_disj (apply2 (aux ss Ts js skolemizable polar) (t1, t2))
   613         | @{const HOL.implies} $ t1 $ t2 =>
   614           @{const HOL.implies} $ aux ss Ts js skolemizable (flip_polarity polar) t1
   615           $ aux ss Ts js skolemizable polar t2
   616         | (t0 as Const (@{const_name Let}, _)) $ t1 $ t2 =>
   617           t0 $ t1 $ aux ss Ts js skolemizable polar t2
   618         | Const (x as (s, T)) =>
   619           if is_raw_inductive_pred hol_ctxt x andalso
   620              not (is_raw_equational_fun hol_ctxt x) andalso
   621              not (is_well_founded_inductive_pred hol_ctxt x) then
   622             let
   623               val gfp = (fixpoint_kind_of_const thy def_tables x = Gfp)
   624               val (pref, connective) =
   625                 if gfp then (lbfp_prefix, @{const HOL.disj})
   626                 else (ubfp_prefix, @{const HOL.conj})
   627               fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x
   628                            |> aux ss Ts js skolemizable polar
   629               fun neg () = Const (pref ^ s, T)
   630             in
   631               case polar |> gfp ? flip_polarity of
   632                 Pos => pos ()
   633               | Neg => neg ()
   634               | Neut =>
   635                 let
   636                   val arg_Ts = binder_types T
   637                   fun app f =
   638                     list_comb (f (), map Bound (length arg_Ts - 1 downto 0))
   639                 in
   640                   fold_rev absdummy arg_Ts (connective $ app pos $ app neg)
   641                 end
   642             end
   643           else
   644             Const x
   645         | t1 $ t2 =>
   646           s_betapply Ts (aux ss Ts js false polar t1,
   647                          aux ss Ts js false Neut t2)
   648         | Abs (s, T, t1) =>
   649           Abs (s, T, aux ss Ts (incrs js) skolemizable polar t1)
   650         | _ => t
   651       end
   652   in aux [] [] [] true Pos end
   653 
   654 (** Function specialization **)
   655 
   656 fun params_in_equation (@{const Pure.imp} $ _ $ t2) = params_in_equation t2
   657   | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
   658   | params_in_equation (Const (@{const_name HOL.eq}, _) $ t1 $ _) =
   659     snd (strip_comb t1)
   660   | params_in_equation _ = []
   661 
   662 fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t =
   663   let
   664     val k = fold Integer.max (map maxidx_of_term (fixed_args @ extra_args)) 0
   665             + 1
   666     val t = map_aterms (fn Var ((s, i), T) => Var ((s, k + i), T) | t' => t') t
   667     val fixed_params = filter_indices fixed_js (params_in_equation t)
   668     fun aux args (Abs (s, T, t)) = list_comb (Abs (s, T, aux [] t), args)
   669       | aux args (t1 $ t2) = aux (aux [] t2 :: args) t1
   670       | aux args t =
   671         if t = Const x then
   672           list_comb (Const x', extra_args @ filter_out_indices fixed_js args)
   673         else
   674           let val j = find_index (curry (op =) t) fixed_params in
   675             list_comb (if j >= 0 then nth fixed_args j else t, args)
   676           end
   677   in aux [] t end
   678 
   679 fun static_args_in_term ({ersatz_table, ...} : hol_context) x t =
   680   let
   681     fun fun_calls (Abs (_, _, t)) _ = fun_calls t []
   682       | fun_calls (t1 $ t2) args = fun_calls t2 [] #> fun_calls t1 (t2 :: args)
   683       | fun_calls t args =
   684         (case t of
   685            Const (x' as (s', T')) =>
   686            x = x' orelse (case AList.lookup (op =) ersatz_table s' of
   687                             SOME s'' => x = (s'', T')
   688                           | NONE => false)
   689          | _ => false) ? cons args
   690     fun call_sets [] [] vs = [vs]
   691       | call_sets [] uss vs = vs :: call_sets uss [] []
   692       | call_sets ([] :: _) _ _ = []
   693       | call_sets ((t :: ts) :: tss) uss vs =
   694         Ord_List.insert Term_Ord.term_ord t vs |> call_sets tss (ts :: uss)
   695     val sets = call_sets (fun_calls t [] []) [] []
   696     val indexed_sets = sets ~~ (index_seq 0 (length sets))
   697   in
   698     fold_rev (fn (set, j) =>
   699                  case set of
   700                    [Var _] => AList.lookup (op =) indexed_sets set = SOME j
   701                               ? cons (j, NONE)
   702                  | [t as Const _] => cons (j, SOME t)
   703                  | [t as Free _] => cons (j, SOME t)
   704                  | _ => I) indexed_sets []
   705   end
   706 
   707 fun static_args_in_terms hol_ctxt x =
   708   map (static_args_in_term hol_ctxt x)
   709   #> fold1 (Ord_List.inter (prod_ord int_ord (option_ord Term_Ord.term_ord)))
   710 
   711 fun overlapping_indices [] _ = []
   712   | overlapping_indices _ [] = []
   713   | overlapping_indices (ps1 as (j1, t1) :: ps1') (ps2 as (j2, t2) :: ps2') =
   714     if j1 < j2 then overlapping_indices ps1' ps2
   715     else if j1 > j2 then overlapping_indices ps1 ps2'
   716     else overlapping_indices ps1' ps2' |> the_default t2 t1 = t2 ? cons j1
   717 
   718 fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep
   719 
   720 (* If a constant's definition is picked up deeper than this threshold, we
   721    prevent excessive specialization by not specializing it. *)
   722 val special_max_depth = 20
   723 
   724 val bound_var_prefix = "b"
   725 
   726 fun special_fun_aconv ((x1, js1, ts1), (x2, js2, ts2)) =
   727   x1 = x2 andalso js1 = js2 andalso length ts1 = length ts2 andalso
   728   forall (op aconv) (ts1 ~~ ts2)
   729 
   730 fun specialize_consts_in_term
   731         (hol_ctxt as {ctxt, thy, specialize, def_tables, simp_table,
   732                       special_funs, ...}) def depth t =
   733   if not specialize orelse depth > special_max_depth then
   734     t
   735   else
   736     let
   737       val blacklist =
   738         if def then case term_under_def t of Const x => [x] | _ => [] else []
   739       fun aux args Ts (Const (x as (s, T))) =
   740           ((if not (member (op =) blacklist x) andalso not (null args) andalso
   741                not (String.isPrefix special_prefix s) andalso
   742                not (is_built_in_const x) andalso
   743                (is_equational_fun hol_ctxt x orelse
   744                 (is_some (def_of_const thy def_tables x) andalso
   745                  not (is_of_class_const thy x) andalso
   746                  not (is_constr ctxt x) andalso
   747                  not (is_choice_spec_fun hol_ctxt x))) then
   748               let
   749                 val eligible_args =
   750                   filter (is_special_eligible_arg true Ts o snd)
   751                          (index_seq 0 (length args) ~~ args)
   752                 val _ = not (null eligible_args) orelse raise SAME ()
   753                 val old_axs = equational_fun_axioms hol_ctxt x
   754                               |> map (destroy_existential_equalities hol_ctxt)
   755                 val static_params = static_args_in_terms hol_ctxt x old_axs
   756                 val fixed_js = overlapping_indices static_params eligible_args
   757                 val _ = not (null fixed_js) orelse raise SAME ()
   758                 val fixed_args = filter_indices fixed_js args
   759                 val vars = fold Term.add_vars fixed_args []
   760                            |> sort (Term_Ord.fast_indexname_ord o apply2 fst)
   761                 val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js))
   762                                     fixed_args []
   763                                |> sort int_ord
   764                 val live_args = filter_out_indices fixed_js args
   765                 val extra_args = map Var vars @ map Bound bound_js @ live_args
   766                 val extra_Ts = map snd vars @ filter_indices bound_js Ts
   767                 val k = maxidx_of_term t + 1
   768                 fun var_for_bound_no j =
   769                   Var ((bound_var_prefix ^
   770                         nat_subscript (find_index (curry (op =) j) bound_js
   771                                        + 1), k),
   772                        nth Ts j)
   773                 val fixed_args_in_axiom =
   774                   map (curry subst_bounds
   775                              (map var_for_bound_no (index_seq 0 (length Ts))))
   776                       fixed_args
   777               in
   778                 case AList.lookup special_fun_aconv (!special_funs)
   779                                   (x, fixed_js, fixed_args_in_axiom) of
   780                   SOME x' => list_comb (Const x', extra_args)
   781                 | NONE =>
   782                   let
   783                     val extra_args_in_axiom =
   784                       map Var vars @ map var_for_bound_no bound_js
   785                     val x' as (s', _) =
   786                       (special_prefix_for (length (!special_funs) + 1) ^ s,
   787                        extra_Ts @ filter_out_indices fixed_js (binder_types T)
   788                        ---> body_type T)
   789                     val new_axs =
   790                       map (specialize_fun_axiom x x' fixed_js
   791                                fixed_args_in_axiom extra_args_in_axiom) old_axs
   792                     val _ =
   793                       Unsynchronized.change special_funs
   794                           (cons ((x, fixed_js, fixed_args_in_axiom), x'))
   795                     val _ = add_simps simp_table s' new_axs
   796                   in list_comb (Const x', extra_args) end
   797               end
   798             else
   799               raise SAME ())
   800            handle SAME () => list_comb (Const x, args))
   801         | aux args Ts (Abs (s, T, t)) =
   802           list_comb (Abs (s, T, aux [] (T :: Ts) t), args)
   803         | aux args Ts (t1 $ t2) = aux (aux [] Ts t2 :: args) Ts t1
   804         | aux args _ t = list_comb (t, args)
   805     in aux [] [] t end
   806 
   807 type special_triple = int list * term list * (string * typ)
   808 
   809 val cong_var_prefix = "c"
   810 
   811 fun special_congruence_axiom T (js1, ts1, x1) (js2, ts2, x2) =
   812   let
   813     val (bounds1, bounds2) = apply2 (map Var o special_bounds) (ts1, ts2)
   814     val Ts = binder_types T
   815     val max_j = fold (fold Integer.max) [js1, js2] ~1
   816     val (eqs, (args1, args2)) =
   817       fold (fn j => case apply2 (fn ps => AList.lookup (op =) ps j)
   818                                   (js1 ~~ ts1, js2 ~~ ts2) of
   819                       (SOME t1, SOME t2) => apfst (cons (t1, t2))
   820                     | (SOME t1, NONE) => apsnd (apsnd (cons t1))
   821                     | (NONE, SOME t2) => apsnd (apfst (cons t2))
   822                     | (NONE, NONE) =>
   823                       let val v = Var ((cong_var_prefix ^ nat_subscript j, 0),
   824                                        nth Ts j) in
   825                         apsnd (apply2 (cons v))
   826                       end) (max_j downto 0) ([], ([], []))
   827   in
   828     Logic.list_implies (eqs |> filter_out (op aconv) |> distinct (op =)
   829                             |> map Logic.mk_equals,
   830                         Logic.mk_equals (list_comb (Const x1, bounds1 @ args1),
   831                                          list_comb (Const x2, bounds2 @ args2)))
   832   end
   833 
   834 fun special_congruence_axioms (hol_ctxt as {special_funs, ...}) ts =
   835   let
   836     val groups =
   837       !special_funs
   838       |> map (fn ((x, js, ts), x') => (x, (js, ts, x')))
   839       |> AList.group (op =)
   840       |> filter_out (is_equational_fun_surely_complete hol_ctxt o fst)
   841       |> map (fn (x, zs) =>
   842                  (x, zs |> member (op =) ts (Const x) ? cons ([], [], x)))
   843     fun generality (js, _, _) = ~(length js)
   844     fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
   845       x1 <> x2 andalso length j2 < length j1 andalso
   846       Ord_List.subset (prod_ord int_ord Term_Ord.term_ord) (j2 ~~ t2, j1 ~~ t1)
   847     fun do_pass_1 _ [] [_] [_] = I
   848       | do_pass_1 T skipped _ [] = do_pass_2 T skipped
   849       | do_pass_1 T skipped all (z :: zs) =
   850         case filter (is_more_specific z) all
   851              |> sort (int_ord o apply2 generality) of
   852           [] => do_pass_1 T (z :: skipped) all zs
   853         | (z' :: _) => cons (special_congruence_axiom T z z')
   854                        #> do_pass_1 T skipped all zs
   855     and do_pass_2 _ [] = I
   856       | do_pass_2 T (z :: zs) =
   857         fold (cons o special_congruence_axiom T z) zs #> do_pass_2 T zs
   858   in fold (fn ((_, T), zs) => do_pass_1 T [] zs zs) groups [] end
   859 
   860 (** Axiom selection **)
   861 
   862 fun defined_free_by_assumption t =
   863   let
   864     fun do_equals u def =
   865       if exists_subterm (curry (op aconv) u) def then NONE else SOME u
   866   in
   867     case t of
   868       Const (@{const_name Pure.eq}, _) $ (u as Free _) $ def => do_equals u def
   869     | @{const Trueprop}
   870       $ (Const (@{const_name HOL.eq}, _) $ (u as Free _) $ def) =>
   871       do_equals u def
   872     | _ => NONE
   873   end
   874 
   875 fun assumption_exclusively_defines_free assm_ts t =
   876   case defined_free_by_assumption t of
   877     SOME u =>
   878     length (filter ((fn SOME u' => u aconv u' | NONE => false)
   879                      o defined_free_by_assumption) assm_ts) = 1
   880   | NONE => false
   881 
   882 fun all_table_entries table = Symtab.fold (append o snd) table []
   883 
   884 fun extra_table tables s =
   885   Symtab.make [(s, apply2 all_table_entries tables |> op @)]
   886 
   887 fun eval_axiom_for_term j t =
   888   Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t)
   889 
   890 val is_trivial_equation = the_default false o try (op aconv o Logic.dest_equals)
   891 
   892 (* Prevents divergence in case of cyclic or infinite axiom dependencies. *)
   893 val axioms_max_depth = 255
   894 
   895 fun axioms_for_term
   896         (hol_ctxt as {thy, ctxt, max_bisim_depth, user_axioms, evals,
   897                       def_tables, nondef_table, choice_spec_table, nondefs,
   898                       ...}) assm_ts neg_t =
   899   let
   900     val (def_assm_ts, nondef_assm_ts) =
   901       List.partition (assumption_exclusively_defines_free assm_ts) assm_ts
   902     val def_assm_table = map (`(the o defined_free_by_assumption)) def_assm_ts
   903     type accumulator = (string * typ) list * (term list * term list)
   904     fun add_axiom get app def depth t (accum as (seen, axs)) =
   905       let
   906         val t = t |> unfold_defs_in_term hol_ctxt
   907                   |> skolemize_term_and_more hol_ctxt ~1 (* FIXME: why ~1? *)
   908       in
   909         if is_trivial_equation t then
   910           accum
   911         else
   912           let val t' = t |> specialize_consts_in_term hol_ctxt def depth in
   913             if exists (member (op aconv) (get axs)) [t, t'] then accum
   914             else add_axioms_for_term (depth + 1) t' (seen, app (cons t') axs)
   915           end
   916       end
   917     and add_def_axiom depth = add_axiom fst apfst true depth
   918     and add_nondef_axiom depth = add_axiom snd apsnd false depth
   919     and add_maybe_def_axiom depth t =
   920       (if head_of t <> @{const Pure.imp} then add_def_axiom
   921        else add_nondef_axiom) depth t
   922     and add_eq_axiom depth t =
   923       (if is_constr_pattern_formula ctxt t then add_def_axiom
   924        else add_nondef_axiom) depth t
   925     and add_axioms_for_term depth t (accum as (seen, axs)) =
   926       case t of
   927         t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
   928       | Const (x as (s, T)) =>
   929         (if member (op aconv) seen t orelse is_built_in_const x then
   930            accum
   931          else
   932            let val accum = (t :: seen, axs) in
   933              if depth > axioms_max_depth then
   934                raise TOO_LARGE ("Nitpick_Preproc.axioms_for_term.\
   935                                 \add_axioms_for_term",
   936                                 "too many nested axioms (" ^
   937                                 string_of_int depth ^ ")")
   938              else if is_of_class_const thy x then
   939                let
   940                  val class = Logic.class_of_const s
   941                  val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]),
   942                                                    class)
   943                  val ax1 = try (specialize_type thy x) of_class
   944                  val ax2 = Option.map (specialize_type thy x o snd)
   945                                       (get_class_def thy class)
   946                in
   947                  fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
   948                       accum
   949                end
   950              else if is_constr ctxt x then
   951                accum
   952              else if is_descr (original_name s) then
   953                fold (add_nondef_axiom depth) (equational_fun_axioms hol_ctxt x)
   954                     accum
   955              else if is_equational_fun hol_ctxt x then
   956                fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)
   957                     accum
   958              else if is_choice_spec_fun hol_ctxt x then
   959                fold (add_nondef_axiom depth)
   960                     (nondef_props_for_const thy true choice_spec_table x) accum
   961              else if is_abs_fun ctxt x then
   962                accum |> fold (add_nondef_axiom depth)
   963                              (nondef_props_for_const thy false nondef_table x)
   964                      |> (is_funky_typedef ctxt (range_type T) orelse
   965                          range_type T = nat_T)
   966                         ? fold (add_maybe_def_axiom depth)
   967                                (nondef_props_for_const thy true
   968                                     (extra_table def_tables s) x)
   969              else if is_rep_fun ctxt x then
   970                accum |> fold (add_nondef_axiom depth)
   971                              (nondef_props_for_const thy false nondef_table x)
   972                      |> (is_funky_typedef ctxt (range_type T) orelse
   973                          range_type T = nat_T)
   974                         ? fold (add_maybe_def_axiom depth)
   975                                (nondef_props_for_const thy true
   976                                     (extra_table def_tables s) x)
   977                      |> add_axioms_for_term depth
   978                                             (Const (mate_of_rep_fun ctxt x))
   979                      |> fold (add_def_axiom depth)
   980                              (inverse_axioms_for_rep_fun ctxt x)
   981              else if s = @{const_name Pure.type} then
   982                accum
   983              else case def_of_const thy def_tables x of
   984                SOME _ =>
   985                fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)
   986                     accum
   987              | NONE =>
   988                accum |> user_axioms <> SOME false
   989                         ? fold (add_nondef_axiom depth)
   990                                (nondef_props_for_const thy false nondef_table x)
   991            end)
   992         |> add_axioms_for_type depth T
   993       | Free (_, T) =>
   994         (if member (op aconv) seen t then
   995            accum
   996          else case AList.lookup (op =) def_assm_table t of
   997            SOME t => add_def_axiom depth t accum
   998          | NONE => accum)
   999         |> add_axioms_for_type depth T
  1000       | Var (_, T) => add_axioms_for_type depth T accum
  1001       | Bound _ => accum
  1002       | Abs (_, T, t) => accum |> add_axioms_for_term depth t
  1003                                |> add_axioms_for_type depth T
  1004     and add_axioms_for_type depth T =
  1005       case T of
  1006         Type (@{type_name fun}, Ts) => fold (add_axioms_for_type depth) Ts
  1007       | Type (@{type_name prod}, Ts) => fold (add_axioms_for_type depth) Ts
  1008       | Type (@{type_name set}, Ts) => fold (add_axioms_for_type depth) Ts
  1009       | @{typ prop} => I
  1010       | @{typ bool} => I
  1011       | TFree (_, S) => add_axioms_for_sort depth T S
  1012       | TVar (_, S) => add_axioms_for_sort depth T S
  1013       | Type (z as (_, Ts)) =>
  1014         fold (add_axioms_for_type depth) Ts
  1015         #> (if is_pure_typedef ctxt T then
  1016               fold (add_maybe_def_axiom depth) (optimized_typedef_axioms ctxt z)
  1017             else if is_quot_type ctxt T then
  1018               fold (add_def_axiom depth) (optimized_quot_type_axioms ctxt z)
  1019             else if max_bisim_depth >= 0 andalso is_codatatype ctxt T then
  1020               fold (add_maybe_def_axiom depth)
  1021                    (codatatype_bisim_axioms hol_ctxt T)
  1022             else
  1023               I)
  1024     and add_axioms_for_sort depth T S =
  1025       let
  1026         val supers = Sign.complete_sort thy S
  1027         val class_axioms =
  1028           maps (fn class => map Thm.prop_of (Axclass.get_info thy class |> #axioms
  1029                                          handle ERROR _ => [])) supers
  1030         val monomorphic_class_axioms =
  1031           map (fn t => case Term.add_tvars t [] of
  1032                          [] => t
  1033                        | [(x, S)] =>
  1034                          Envir.subst_term_types (Vartab.make [(x, (S, T))]) t
  1035                        | _ => raise TERM ("Nitpick_Preproc.axioms_for_term.\
  1036                                           \add_axioms_for_sort", [t]))
  1037               class_axioms
  1038       in fold (add_nondef_axiom depth) monomorphic_class_axioms end
  1039     val (mono_nondefs, poly_nondefs) =
  1040       List.partition (null o Term.hidden_polymorphism) nondefs
  1041     val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals))
  1042                            evals
  1043     val (seen, (defs, nondefs)) =
  1044       ([], ([], []))
  1045       |> add_axioms_for_term 1 neg_t
  1046       |> fold_rev (add_nondef_axiom 1) nondef_assm_ts
  1047       |> fold_rev (add_def_axiom 1) eval_axioms
  1048       |> user_axioms = SOME true ? fold (add_nondef_axiom 1) mono_nondefs
  1049     val defs = defs @ special_congruence_axioms hol_ctxt seen
  1050     val got_all_mono_user_axioms =
  1051       (user_axioms = SOME true orelse null mono_nondefs)
  1052   in (neg_t :: nondefs, defs, got_all_mono_user_axioms, null poly_nondefs) end
  1053 
  1054 (** Simplification of constructor/selector terms **)
  1055 
  1056 fun simplify_constrs_and_sels ctxt t =
  1057   let
  1058     fun is_nth_sel_on constr_s t' n (Const (s, _) $ t) =
  1059         (t = t' andalso is_sel_like_and_no_discr s andalso
  1060          constr_name_for_sel_like s = constr_s andalso sel_no_from_name s = n)
  1061       | is_nth_sel_on _ _ _ _ = false
  1062     fun do_term (Const (@{const_name Rep_Frac}, _)
  1063                  $ (Const (@{const_name Abs_Frac}, _) $ t1)) [] =
  1064         do_term t1 []
  1065       | do_term (Const (@{const_name Abs_Frac}, _)
  1066                  $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] =
  1067         do_term t1 []
  1068       | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)
  1069       | do_term (t as Const (x as (s, T))) (args as _ :: _) =
  1070         ((if is_nonfree_constr ctxt x then
  1071             if length args = num_binder_types T then
  1072               case hd args of
  1073                 Const (_, T') $ t' =>
  1074                 if domain_type T' = body_type T andalso
  1075                    forall (uncurry (is_nth_sel_on s t'))
  1076                           (index_seq 0 (length args) ~~ args) then
  1077                   t'
  1078                 else
  1079                   raise SAME ()
  1080               | _ => raise SAME ()
  1081             else
  1082               raise SAME ()
  1083           else if is_sel_like_and_no_discr s then
  1084             case strip_comb (hd args) of
  1085               (Const (x' as (s', T')), ts') =>
  1086               if is_free_constr ctxt x' andalso
  1087                  constr_name_for_sel_like s = s' andalso
  1088                  not (exists is_pair_type (binder_types T')) then
  1089                 list_comb (nth ts' (sel_no_from_name s), tl args)
  1090               else
  1091                 raise SAME ()
  1092             | _ => raise SAME ()
  1093           else
  1094             raise SAME ())
  1095          handle SAME () => s_betapplys [] (t, args))
  1096       | do_term (Abs (s, T, t')) args =
  1097         s_betapplys [] (Abs (s, T, do_term t' []), args)
  1098       | do_term t args = s_betapplys [] (t, args)
  1099   in do_term t [] end
  1100 
  1101 (** Quantifier massaging: Distributing quantifiers **)
  1102 
  1103 fun distribute_quantifiers t =
  1104   case t of
  1105     (t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) =>
  1106     (case t1 of
  1107        (t10 as @{const HOL.conj}) $ t11 $ t12 =>
  1108        t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
  1109            $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
  1110      | (t10 as @{const Not}) $ t11 =>
  1111        t10 $ distribute_quantifiers (Const (@{const_name Ex}, T0)
  1112                                      $ Abs (s, T1, t11))
  1113      | t1 =>
  1114        if not (loose_bvar1 (t1, 0)) then
  1115          distribute_quantifiers (incr_boundvars ~1 t1)
  1116        else
  1117          t0 $ Abs (s, T1, distribute_quantifiers t1))
  1118   | (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) =>
  1119     (case distribute_quantifiers t1 of
  1120        (t10 as @{const HOL.disj}) $ t11 $ t12 =>
  1121        t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
  1122            $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
  1123      | (t10 as @{const HOL.implies}) $ t11 $ t12 =>
  1124        t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
  1125                                      $ Abs (s, T1, t11))
  1126            $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
  1127      | (t10 as @{const Not}) $ t11 =>
  1128        t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
  1129                                      $ Abs (s, T1, t11))
  1130      | t1 =>
  1131        if not (loose_bvar1 (t1, 0)) then
  1132          distribute_quantifiers (incr_boundvars ~1 t1)
  1133        else
  1134          t0 $ Abs (s, T1, distribute_quantifiers t1))
  1135   | t1 $ t2 => distribute_quantifiers t1 $ distribute_quantifiers t2
  1136   | Abs (s, T, t') => Abs (s, T, distribute_quantifiers t')
  1137   | _ => t
  1138 
  1139 (** Quantifier massaging: Pushing quantifiers inward **)
  1140 
  1141 fun renumber_bounds j n f t =
  1142   case t of
  1143     t1 $ t2 => renumber_bounds j n f t1 $ renumber_bounds j n f t2
  1144   | Abs (s, T, t') => Abs (s, T, renumber_bounds (j + 1) n f t')
  1145   | Bound j' =>
  1146     Bound (if j' >= j andalso j' < j + n then f (j' - j) + j else j')
  1147   | _ => t
  1148 
  1149 (* Maximum number of quantifiers in a cluster for which the exponential
  1150    algorithm is used. Larger clusters use a heuristic inspired by Claessen &
  1151    Soerensson's polynomial binary splitting procedure (p. 5 of their MODEL 2003
  1152    paper). *)
  1153 val quantifier_cluster_threshold = 7
  1154 
  1155 val push_quantifiers_inward =
  1156   let
  1157     fun aux quant_s ss Ts t =
  1158       (case t of
  1159          Const (s0, _) $ Abs (s1, T1, t1 as _ $ _) =>
  1160          if s0 = quant_s then
  1161            aux s0 (s1 :: ss) (T1 :: Ts) t1
  1162          else if quant_s = "" andalso
  1163                  (s0 = @{const_name All} orelse s0 = @{const_name Ex}) then
  1164            aux s0 [s1] [T1] t1
  1165          else
  1166            raise SAME ()
  1167        | _ => raise SAME ())
  1168       handle SAME () =>
  1169              case t of
  1170                t1 $ t2 =>
  1171                if quant_s = "" then
  1172                  aux "" [] [] t1 $ aux "" [] [] t2
  1173                else
  1174                  let
  1175                    fun big_union proj ps =
  1176                      fold (fold (insert (op =)) o proj) ps []
  1177                    val (ts, connective) = strip_any_connective t
  1178                    val T_costs = map typical_card_of_type Ts
  1179                    val t_costs = map size_of_term ts
  1180                    val num_Ts = length Ts
  1181                    val flip = curry (op -) (num_Ts - 1)
  1182                    val t_boundss = map (map flip o loose_bnos) ts
  1183                    fun merge costly_boundss [] = costly_boundss
  1184                      | merge costly_boundss (j :: js) =
  1185                        let
  1186                          val (yeas, nays) =
  1187                            List.partition (fn (bounds, _) =>
  1188                                               member (op =) bounds j)
  1189                                           costly_boundss
  1190                          val yeas_bounds = big_union fst yeas
  1191                          val yeas_cost = Integer.sum (map snd yeas)
  1192                                          * nth T_costs j
  1193                        in merge ((yeas_bounds, yeas_cost) :: nays) js end
  1194                    val cost = Integer.sum o map snd oo merge
  1195                    fun heuristically_best_permutation _ [] = []
  1196                      | heuristically_best_permutation costly_boundss js =
  1197                        let
  1198                          val (costly_boundss, (j, js)) =
  1199                            js |> map (`(merge costly_boundss o single))
  1200                               |> sort (int_ord
  1201                                        o apply2 (Integer.sum o map snd o fst))
  1202                               |> split_list |>> hd ||> pairf hd tl
  1203                        in
  1204                          j :: heuristically_best_permutation costly_boundss js
  1205                        end
  1206                    val js =
  1207                      if length Ts <= quantifier_cluster_threshold then
  1208                        all_permutations (index_seq 0 num_Ts)
  1209                        |> map (`(cost (t_boundss ~~ t_costs)))
  1210                        |> sort (int_ord o apply2 fst) |> hd |> snd
  1211                      else
  1212                        heuristically_best_permutation (t_boundss ~~ t_costs)
  1213                                                       (index_seq 0 num_Ts)
  1214                    val back_js = map (fn j => find_index (curry (op =) j) js)
  1215                                      (index_seq 0 num_Ts)
  1216                    val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip))
  1217                                 ts
  1218                    fun mk_connection [] =
  1219                        raise ARG ("Nitpick_Preproc.push_quantifiers_inward.aux.\
  1220                                   \mk_connection", "")
  1221                      | mk_connection ts_cum_bounds =
  1222                        ts_cum_bounds |> map fst
  1223                        |> foldr1 (fn (t1, t2) => connective $ t1 $ t2)
  1224                    fun build ts_cum_bounds [] = ts_cum_bounds |> mk_connection
  1225                      | build ts_cum_bounds (j :: js) =
  1226                        let
  1227                          val (yeas, nays) =
  1228                            List.partition (fn (_, bounds) =>
  1229                                               member (op =) bounds j)
  1230                                           ts_cum_bounds
  1231                            ||> map (apfst (incr_boundvars ~1))
  1232                        in
  1233                          if null yeas then
  1234                            build nays js
  1235                          else
  1236                            let val T = nth Ts (flip j) in
  1237                              build ((Const (quant_s, (T --> bool_T) --> bool_T)
  1238                                      $ Abs (nth ss (flip j), T,
  1239                                             mk_connection yeas),
  1240                                       big_union snd yeas) :: nays) js
  1241                            end
  1242                        end
  1243                  in build (ts ~~ t_boundss) js end
  1244              | Abs (s, T, t') => Abs (s, T, aux "" [] [] t')
  1245              | _ => t
  1246   in aux "" [] [] end
  1247 
  1248 (** Preprocessor entry point **)
  1249 
  1250 val max_skolem_depth = 3
  1251 
  1252 fun preprocess_formulas
  1253         (hol_ctxt as {ctxt, binary_ints, destroy_constrs, boxes, needs, ...})
  1254         assm_ts neg_t =
  1255   let
  1256     val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
  1257       neg_t |> unfold_defs_in_term hol_ctxt
  1258             |> close_form
  1259             |> skolemize_term_and_more hol_ctxt max_skolem_depth
  1260             |> specialize_consts_in_term hol_ctxt false 0
  1261             |> axioms_for_term hol_ctxt assm_ts
  1262     val binarize =
  1263       case binary_ints of
  1264         SOME false => false
  1265       | _ => forall (may_use_binary_ints false) nondef_ts andalso
  1266              forall (may_use_binary_ints true) def_ts andalso
  1267              (binary_ints = SOME true orelse
  1268               exists should_use_binary_ints (nondef_ts @ def_ts))
  1269     val box = exists (not_equal (SOME false) o snd) boxes
  1270     val table =
  1271       Termtab.empty
  1272       |> box ? fold (add_to_uncurry_table ctxt) (nondef_ts @ def_ts)
  1273     fun do_middle def =
  1274       binarize ? binarize_nat_and_int_in_term
  1275       #> box ? uncurry_term table
  1276       #> box ? box_fun_and_pair_in_term hol_ctxt def
  1277     fun do_tail def =
  1278       destroy_set_Collect
  1279       #> destroy_constrs ? (pull_out_universal_constrs hol_ctxt def
  1280                             #> pull_out_existential_constrs hol_ctxt)
  1281       #> destroy_pulled_out_constrs hol_ctxt def destroy_constrs
  1282       #> curry_assms
  1283       #> destroy_universal_equalities
  1284       #> destroy_existential_equalities hol_ctxt
  1285       #> simplify_constrs_and_sels ctxt
  1286       #> distribute_quantifiers
  1287       #> push_quantifiers_inward
  1288       #> close_form
  1289       #> Term.map_abs_vars shortest_name
  1290     val nondef_ts = nondef_ts |> map (do_middle false)
  1291     val need_ts =
  1292       case needs of
  1293         SOME needs =>
  1294         needs |> map (unfold_defs_in_term hol_ctxt #> do_middle false)
  1295       | NONE => [] (* FIXME: Implement inference. *)
  1296     val nondef_ts = nondef_ts |> map (do_tail false)
  1297     val def_ts = def_ts |> map (do_middle true #> do_tail true)
  1298   in
  1299     (nondef_ts, def_ts, need_ts, got_all_mono_user_axioms, no_poly_user_axioms,
  1300      binarize)
  1301   end
  1302 
  1303 end;