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