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