(*  Title:      HOL/Tools/Nitpick/nitpick_preproc.ML

    Author:     Jasmin Blanchette, TU Muenchen

    Copyright   2008, 2009, 2010

Nitpick's HOL preprocessor.

*)

signature NITPICK_PREPROC =

sig

  type hol_context = Nitpick_HOL.hol_context

  val preprocess_term :

    hol_context -> term

    -> ((term list * term list) * (bool * bool)) * term * bool

end

structure Nitpick_Preproc : NITPICK_PREPROC =

struct

open Nitpick_Util

open Nitpick_HOL

(* polarity -> string -> bool *)

fun is_positive_existential polar quant_s =

  (polar = Pos andalso quant_s = @{const_name Ex}) orelse

  (polar = Neg andalso quant_s <> @{const_name Ex})

(** Binary coding of integers **)

(* If a formula contains a numeral whose absolute value is more than this

   threshold, the unary coding is likely not to work well and we prefer the

   binary coding. *)

val binary_int_threshold = 3

(* term -> bool *)

fun may_use_binary_ints (t1 $ t2) =

    may_use_binary_ints t1 andalso may_use_binary_ints t2

  | may_use_binary_ints (t as Const (s, _)) =

    t <> @{const Suc} andalso

    not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac},

                        @{const_name nat_gcd}, @{const_name nat_lcm},

                        @{const_name Frac}, @{const_name norm_frac}] s)

  | may_use_binary_ints (Abs (_, _, t')) = may_use_binary_ints t'

  | may_use_binary_ints _ = true

fun should_use_binary_ints (t1 $ t2) =

    should_use_binary_ints t1 orelse should_use_binary_ints t2

  | should_use_binary_ints (Const (s, T)) =

    ((s = @{const_name times} orelse s = @{const_name div}) andalso

     is_integer_type (body_type T)) orelse

    (String.isPrefix numeral_prefix s andalso

     let val n = the (Int.fromString (unprefix numeral_prefix s)) in

       n < ~ binary_int_threshold orelse n > binary_int_threshold

     end)

  | should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t'

  | should_use_binary_ints _ = false

(** Uncurrying **)

(* theory -> term -> int Termtab.tab -> int Termtab.tab *)

fun add_to_uncurry_table thy t =

  let

    (* term -> term list -> int Termtab.tab -> int Termtab.tab *)

    fun aux (t1 $ t2) args table =

        let val table = aux t2 [] table in aux t1 (t2 :: args) table end

      | aux (Abs (_, _, t')) _ table = aux t' [] table

      | aux (t as Const (x as (s, _))) args table =

        if is_built_in_const thy [(NONE, true)] true x orelse

           is_constr_like thy x orelse

           is_sel s orelse s = @{const_name Sigma} then

          table

        else

          Termtab.map_default (t, 65536) (curry Int.min (length args)) table

      | aux _ _ table = table

  in aux t [] end

(* int -> int -> string *)

fun uncurry_prefix_for k j =

  uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep

(* int Termtab.tab term -> term *)

fun uncurry_term table t =

  let

    (* term -> term list -> term *)

    fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args)

      | aux (Abs (s, T, t')) args = betapplys (Abs (s, T, aux t' []), args)

      | aux (t as Const (s, T)) args =

        (case Termtab.lookup table t of

           SOME n =>

           if n >= 2 then

             let

               val arg_Ts = strip_n_binders n T |> fst

               val j =

                 if is_iterator_type (hd arg_Ts) then

                   1

                 else case find_index (not_equal bool_T) arg_Ts of

                   ~1 => n

                 | j => j

               val ((before_args, tuple_args), after_args) =

                 args |> chop n |>> chop j

               val ((before_arg_Ts, tuple_arg_Ts), rest_T) =

                 T |> strip_n_binders n |>> chop j

               val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts

             in

               if n - j < 2 then

                 betapplys (t, args)

               else

                 betapplys (Const (uncurry_prefix_for (n - j) j ^ s,

                                   before_arg_Ts ---> tuple_T --> rest_T),

                            before_args @ [mk_flat_tuple tuple_T tuple_args] @

                            after_args)

             end

           else

             betapplys (t, args)

         | NONE => betapplys (t, args))

      | aux t args = betapplys (t, args)

  in aux t [] end

(** Boxing **)

(* hol_context -> typ -> term -> term *)

fun constr_expand (hol_ctxt as {thy, stds, ...}) T t =

  (case head_of t of

     Const x => if is_constr_like thy x then t else raise SAME ()

   | _ => raise SAME ())

  handle SAME () =>

         let

           val x' as (_, T') =

             if is_pair_type T then

               let val (T1, T2) = HOLogic.dest_prodT T in

                 (@{const_name Pair}, T1 --> T2 --> T)

               end

             else

               datatype_constrs hol_ctxt T |> hd

           val arg_Ts = binder_types T'

         in

           list_comb (Const x', map2 (select_nth_constr_arg thy stds x' t)

                                     (index_seq 0 (length arg_Ts)) arg_Ts)

         end

(* (term -> term) -> int -> term -> term *)

fun coerce_bound_no f j t =

  case t of

    t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2

  | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')

  | Bound j' => if j' = j then f t else t

  | _ => t

(* hol_context -> typ -> typ -> term -> term *)

fun coerce_bound_0_in_term hol_ctxt new_T old_T =

  old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0

(* hol_context -> typ list -> typ -> typ -> term -> term *)

and coerce_term (hol_ctxt as {thy, stds, fast_descrs, ...}) Ts new_T old_T t =

  if old_T = new_T then

    t

  else

    case (new_T, old_T) of

      (Type (new_s, new_Ts as [new_T1, new_T2]),

       Type ("fun", [old_T1, old_T2])) =>

      (case eta_expand Ts t 1 of

         Abs (s, _, t') =>

         Abs (s, new_T1,

              t' |> coerce_bound_0_in_term hol_ctxt new_T1 old_T1

                 |> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2)

         |> Envir.eta_contract

         |> new_s <> "fun"

            ? construct_value thy stds

                  (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)

                  o single

       | t' => raise TERM ("Nitpick_Preproc.coerce_term", [t']))

    | (Type (new_s, new_Ts as [new_T1, new_T2]),

       Type (old_s, old_Ts as [old_T1, old_T2])) =>

      if old_s = @{type_name fun_box} orelse

         old_s = @{type_name pair_box} orelse old_s = "*" then

        case constr_expand hol_ctxt old_T t of

          Const (old_s, _) $ t1 =>

          if new_s = "fun" then

            coerce_term hol_ctxt Ts new_T (Type ("fun", old_Ts)) t1

          else

            construct_value thy stds

                (old_s, Type ("fun", new_Ts) --> new_T)

                [coerce_term hol_ctxt Ts (Type ("fun", new_Ts))

                             (Type ("fun", old_Ts)) t1]

        | Const _ $ t1 $ t2 =>

          construct_value thy stds

              (if new_s = "*" then @{const_name Pair}

               else @{const_name PairBox}, new_Ts ---> new_T)

              [coerce_term hol_ctxt Ts new_T1 old_T1 t1,

               coerce_term hol_ctxt Ts new_T2 old_T2 t2]

        | t' => raise TERM ("Nitpick_Preproc.coerce_term", [t'])

      else

        raise TYPE ("Nitpick_Preproc.coerce_term", [new_T, old_T], [t])

    | _ => raise TYPE ("Nitpick_Preproc.coerce_term", [new_T, old_T], [t])

(* hol_context -> bool -> term -> term *)

fun box_fun_and_pair_in_term (hol_ctxt as {thy, stds, fast_descrs, ...}) def

                             orig_t =

  let

    (* typ -> typ *)

    fun box_relational_operator_type (Type ("fun", Ts)) =

        Type ("fun", map box_relational_operator_type Ts)

      | box_relational_operator_type (Type ("*", Ts)) =

        Type ("*", map (box_type hol_ctxt InPair) Ts)

      | box_relational_operator_type T = T

    (* indexname * typ -> typ * term -> typ option list -> typ option list *)

    fun add_boxed_types_for_var (z as (_, T)) (T', t') =

      case t' of

        Var z' => z' = z ? insert (op =) T'

      | Const (@{const_name Pair}, _) $ t1 $ t2 =>

        (case T' of

           Type (_, [T1, T2]) =>

           fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)]

         | _ => raise TYPE ("Nitpick_Preproc.box_fun_and_pair_in_term.\

                            \add_boxed_types_for_var", [T'], []))

      | _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T

    (* typ list -> typ list -> term -> indexname * typ -> typ *)

    fun box_var_in_def new_Ts old_Ts t (z as (_, T)) =

      case t of

        @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z

      | Const (s0, _) $ t1 $ _ =>

        if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then

          let

            val (t', args) = strip_comb t1

            val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')

          in

            case fold (add_boxed_types_for_var z)

                      (fst (strip_n_binders (length args) T') ~~ args) [] of

              [T''] => T''

            | _ => T

          end

        else

          T

      | _ => T

    (* typ list -> typ list -> polarity -> string -> typ -> string -> typ

       -> term -> term *)

    and do_quantifier new_Ts old_Ts polar quant_s quant_T abs_s abs_T t =

      let

        val abs_T' =

          if polar = Neut orelse is_positive_existential polar quant_s then

            box_type hol_ctxt InFunLHS abs_T

          else

            abs_T

        val body_T = body_type quant_T

      in

        Const (quant_s, (abs_T' --> body_T) --> body_T)

        $ Abs (abs_s, abs_T',

               t |> do_term (abs_T' :: new_Ts) (abs_T :: old_Ts) polar)

      end

    (* typ list -> typ list -> string -> typ -> term -> term -> term *)

    and do_equals new_Ts old_Ts s0 T0 t1 t2 =

      let

        val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2)

        val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)

        val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last

      in

        list_comb (Const (s0, T --> T --> body_type T0),

                   map2 (coerce_term hol_ctxt new_Ts T) [T1, T2] [t1, t2])

      end

    (* string -> typ -> term *)

    and do_description_operator s T =

      let val T1 = box_type hol_ctxt InFunLHS (range_type T) in

        Const (s, (T1 --> bool_T) --> T1)

      end

    (* typ list -> typ list -> polarity -> term -> term *)

    and do_term new_Ts old_Ts polar t =

      case t of

        Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>

        do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1

      | Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 =>

        do_equals new_Ts old_Ts s0 T0 t1 t2

      | @{const "==>"} $ t1 $ t2 =>

        @{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1

        $ do_term new_Ts old_Ts polar t2

      | @{const Pure.conjunction} $ t1 $ t2 =>

        @{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1

        $ do_term new_Ts old_Ts polar t2

      | @{const Trueprop} $ t1 =>

        @{const Trueprop} $ do_term new_Ts old_Ts polar t1

      | @{const Not} $ t1 =>

        @{const Not} $ do_term new_Ts old_Ts (flip_polarity polar) t1

      | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>

        do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1

      | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>

        do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1

      | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>

        do_equals new_Ts old_Ts s0 T0 t1 t2

      | @{const "op &"} $ t1 $ t2 =>

        @{const "op &"} $ do_term new_Ts old_Ts polar t1

        $ do_term new_Ts old_Ts polar t2

      | @{const "op |"} $ t1 $ t2 =>

        @{const "op |"} $ do_term new_Ts old_Ts polar t1

        $ do_term new_Ts old_Ts polar t2

      | @{const "op -->"} $ t1 $ t2 =>

        @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1

        $ do_term new_Ts old_Ts polar t2

      | Const (s as @{const_name The}, T) => do_description_operator s T

      | Const (s as @{const_name Eps}, T) => do_description_operator s T

      | Const (s as @{const_name Tha}, T) => do_description_operator s T

      | Const (x as (s, T)) =>

        Const (s, if s = @{const_name converse} orelse

                     s = @{const_name trancl} then

                    box_relational_operator_type T

                  else if String.isPrefix quot_normal_prefix s then

                    let val T' = box_type hol_ctxt InFunLHS (domain_type T) in

                      T' --> T'

                    end

                  else if is_built_in_const thy stds fast_descrs x orelse

                          s = @{const_name Sigma} then

                    T

                  else if is_constr_like thy x then

                    box_type hol_ctxt InConstr T

                  else if is_sel s

                       orelse is_rep_fun thy x then

                    box_type hol_ctxt InSel T

                  else

                    box_type hol_ctxt InExpr T)

      | t1 $ Abs (s, T, t2') =>

        let

          val t1 = do_term new_Ts old_Ts Neut t1

          val T1 = fastype_of1 (new_Ts, t1)

          val (s1, Ts1) = dest_Type T1

          val T' = hd (snd (dest_Type (hd Ts1)))

          val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2')

          val T2 = fastype_of1 (new_Ts, t2)

          val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2

        in

          betapply (if s1 = "fun" then

                      t1

                    else

                      select_nth_constr_arg thy stds

                          (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0

                          (Type ("fun", Ts1)), t2)

        end

      | t1 $ t2 =>

        let

          val t1 = do_term new_Ts old_Ts Neut t1

          val T1 = fastype_of1 (new_Ts, t1)

          val (s1, Ts1) = dest_Type T1

          val t2 = do_term new_Ts old_Ts Neut t2

          val T2 = fastype_of1 (new_Ts, t2)

          val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2

        in

          betapply (if s1 = "fun" then

                      t1

                    else

                      select_nth_constr_arg thy stds

                          (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0

                          (Type ("fun", Ts1)), t2)

        end

      | Free (s, T) => Free (s, box_type hol_ctxt InExpr T)

      | Var (z as (x, T)) =>

        Var (x, if def then box_var_in_def new_Ts old_Ts orig_t z

                else box_type hol_ctxt InExpr T)

      | Bound _ => t

      | Abs (s, T, t') =>

        Abs (s, T, do_term (T :: new_Ts) (T :: old_Ts) Neut t')

  in do_term [] [] Pos orig_t end

(** Destruction of constructors **)

val val_var_prefix = nitpick_prefix ^ "v"

(* typ list -> int -> int -> int -> term -> term *)

fun fresh_value_var Ts k n j t =

  Var ((val_var_prefix ^ nat_subscript (n - j), k), fastype_of1 (Ts, t))

(* typ list -> term -> bool *)

fun has_heavy_bounds_or_vars Ts t =

  let

    (* typ list -> bool *)

    fun aux [] = false

      | aux [T] = is_fun_type T orelse is_pair_type T

      | aux _ = true

  in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end

(* hol_context -> typ list -> bool -> int -> int -> term -> term list

   -> term list -> term * term list *)

fun pull_out_constr_comb ({thy, stds, ...} : hol_context) Ts relax k level t

                         args seen =

  let val t_comb = list_comb (t, args) in

    case t of

      Const x =>

      if not relax andalso is_constr thy stds x andalso

         not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso

         has_heavy_bounds_or_vars Ts t_comb andalso

         not (loose_bvar (t_comb, level)) then

        let

          val (j, seen) = case find_index (curry (op =) t_comb) seen of

                            ~1 => (0, t_comb :: seen)

                          | j => (j, seen)

        in (fresh_value_var Ts k (length seen) j t_comb, seen) end

      else

        (t_comb, seen)

    | _ => (t_comb, seen)

  end

(* (term -> term) -> typ list -> int -> term list -> term list *)

fun equations_for_pulled_out_constrs mk_eq Ts k seen =

  let val n = length seen in

    map2 (fn j => fn t => mk_eq (fresh_value_var Ts k n j t, t))

         (index_seq 0 n) seen

  end

(* hol_context -> bool -> term -> term *)

fun pull_out_universal_constrs hol_ctxt def t =

  let

    val k = maxidx_of_term t + 1

    (* typ list -> bool -> term -> term list -> term list -> term * term list *)

    fun do_term Ts def t args seen =

      case t of

        (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 =>

        do_eq_or_imp Ts true def t0 t1 t2 seen

      | (t0 as @{const "==>"}) $ t1 $ t2 =>

        if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen

      | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>

        do_eq_or_imp Ts true def t0 t1 t2 seen

      | (t0 as @{const "op -->"}) $ t1 $ t2 =>

        do_eq_or_imp Ts false def t0 t1 t2 seen

      | Abs (s, T, t') =>

        let val (t', seen) = do_term (T :: Ts) def t' [] seen in

          (list_comb (Abs (s, T, t'), args), seen)

        end

      | t1 $ t2 =>

        let val (t2, seen) = do_term Ts def t2 [] seen in

          do_term Ts def t1 (t2 :: args) seen

        end

      | _ => pull_out_constr_comb hol_ctxt Ts def k 0 t args seen

    (* typ list -> bool -> bool -> term -> term -> term -> term list

       -> term * term list *)

    and do_eq_or_imp Ts eq def t0 t1 t2 seen =

      let

        val (t2, seen) = if eq andalso def then (t2, seen)

                         else do_term Ts false t2 [] seen

        val (t1, seen) = do_term Ts false t1 [] seen

      in (t0 $ t1 $ t2, seen) end

    val (concl, seen) = do_term [] def t [] []

  in

    Logic.list_implies (equations_for_pulled_out_constrs Logic.mk_equals [] k

                                                         seen, concl)

  end

(* term -> term -> term *)

fun mk_exists v t =

  HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)

(* hol_context -> term -> term *)

fun pull_out_existential_constrs hol_ctxt t =

  let

    val k = maxidx_of_term t + 1

    (* typ list -> int -> term -> term list -> term list -> term * term list *)

    fun aux Ts num_exists t args seen =

      case t of

        (t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1) =>

        let

          val (t1, seen') = aux (T1 :: Ts) (num_exists + 1) t1 [] []

          val n = length seen'

          (* unit -> term list *)

          fun vars () = map2 (fresh_value_var Ts k n) (index_seq 0 n) seen'

        in

          (equations_for_pulled_out_constrs HOLogic.mk_eq Ts k seen'

           |> List.foldl s_conj t1 |> fold mk_exists (vars ())

           |> curry3 Abs s1 T1 |> curry (op $) t0, seen)

        end

      | t1 $ t2 =>

        let val (t2, seen) = aux Ts num_exists t2 [] seen in

          aux Ts num_exists t1 (t2 :: args) seen

        end

      | Abs (s, T, t') =>

        let

          val (t', seen) = aux (T :: Ts) 0 t' [] (map (incr_boundvars 1) seen)

        in (list_comb (Abs (s, T, t'), args), map (incr_boundvars ~1) seen) end

      | _ =>

        if num_exists > 0 then

          pull_out_constr_comb hol_ctxt Ts false k num_exists t args seen

        else

          (list_comb (t, args), seen)

  in aux [] 0 t [] [] |> fst end

(* hol_context -> bool -> term -> term *)

fun destroy_pulled_out_constrs (hol_ctxt as {thy, stds, ...}) axiom t =

  let

    (* styp -> int *)

    val num_occs_of_var =

      fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)

                    | _ => I) t (K 0)

    (* bool -> term -> term *)

    fun aux careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =

        aux_eq careful true t0 t1 t2

      | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =

        t0 $ aux false t1 $ aux careful t2

      | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =

        aux_eq careful true t0 t1 t2

      | aux careful ((t0 as @{const "op -->"}) $ t1 $ t2) =

        t0 $ aux false t1 $ aux careful t2

      | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')

      | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2

      | aux _ t = t

    (* bool -> bool -> term -> term -> term -> term *)

    and aux_eq careful pass1 t0 t1 t2 =

      ((if careful then

          raise SAME ()

        else if axiom andalso is_Var t2 andalso

                num_occs_of_var (dest_Var t2) = 1 then

          @{const True}

        else case strip_comb t2 of

          (* The first case is not as general as it could be. *)

          (Const (@{const_name PairBox}, _),

                  [Const (@{const_name fst}, _) $ Var z1,

                   Const (@{const_name snd}, _) $ Var z2]) =>

          if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True}

          else raise SAME ()

        | (Const (x as (s, T)), args) =>

          let val arg_Ts = binder_types T in

            if length arg_Ts = length args andalso

               (is_constr thy stds x orelse s = @{const_name Pair}) andalso

               (not careful orelse not (is_Var t1) orelse

                String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then

              discriminate_value hol_ctxt x t1 ::

              map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args

              |> foldr1 s_conj

            else

              raise SAME ()

          end

        | _ => raise SAME ())

       |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop)

      handle SAME () => if pass1 then aux_eq careful false t0 t2 t1

                        else t0 $ aux false t2 $ aux false t1

    (* styp -> term -> int -> typ -> term -> term *)

    and sel_eq x t n nth_T nth_t =

      HOLogic.eq_const nth_T $ nth_t

                             $ select_nth_constr_arg thy stds x t n nth_T

      |> aux false

  in aux axiom t end

(** Destruction of universal and existential equalities **)

(* term -> term *)

fun curry_assms (@{const "==>"} $ (@{const Trueprop}

                                   $ (@{const "op &"} $ t1 $ t2)) $ t3) =

    curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))

  | curry_assms (@{const "==>"} $ t1 $ t2) =

    @{const "==>"} $ curry_assms t1 $ curry_assms t2

  | curry_assms t = t

(* term -> term *)

val destroy_universal_equalities =

  let

    (* term list -> (indexname * typ) list -> term -> term *)

    fun aux prems zs t =

      case t of

        @{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2

      | _ => Logic.list_implies (rev prems, t)

    (* term list -> (indexname * typ) list -> term -> term -> term *)

    and aux_implies prems zs t1 t2 =

      case t1 of

        Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2

      | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') =>

        aux_eq prems zs z t' t1 t2

      | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) =>

        aux_eq prems zs z t' t1 t2

      | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2

    (* term list -> (indexname * typ) list -> indexname * typ -> term -> term

       -> term -> term *)

    and aux_eq prems zs z t' t1 t2 =

      if not (member (op =) zs z) andalso

         not (exists_subterm (curry (op =) (Var z)) t') then

        aux prems zs (subst_free [(Var z, t')] t2)

      else

        aux (t1 :: prems) (Term.add_vars t1 zs) t2

  in aux [] [] end

(* theory -> (typ option * bool) list -> int -> term list -> term list

   -> (term * term list) option *)

fun find_bound_assign thy stds j =

  let

    (* term list -> term list -> (term * term list) option *)

    fun do_term _ [] = NONE

      | do_term seen (t :: ts) =

        let

          (* bool -> term -> term -> (term * term list) option *)

          fun do_eq pass1 t1 t2 =

            (if loose_bvar1 (t2, j) then

               if pass1 then do_eq false t2 t1 else raise SAME ()

             else case t1 of

               Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()

             | Const (s, Type ("fun", [T1, T2])) $ Bound j' =>

               if j' = j andalso

                  s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then

                 SOME (construct_value thy stds (@{const_name FunBox}, T2 --> T1)

                                       [t2], ts @ seen)

               else

                 raise SAME ()

             | _ => raise SAME ())

            handle SAME () => do_term (t :: seen) ts

        in

          case t of

            Const (@{const_name "op ="}, _) $ t1 $ t2 => do_eq true t1 t2

          | _ => do_term (t :: seen) ts

        end

  in do_term end

(* int -> term -> term -> term *)

fun subst_one_bound j arg t =

  let

    (* term * int -> term *)

    fun aux (Bound i, lev) =

        if i < lev then raise SAME ()

        else if i = lev then incr_boundvars (lev - j) arg

        else Bound (i - 1)

      | aux (Abs (a, T, body), lev) = Abs (a, T, aux (body, lev + 1))

      | aux (f $ t, lev) =

        (aux (f, lev) $ (aux (t, lev) handle SAME () => t)

         handle SAME () => f $ aux (t, lev))

      | aux _ = raise SAME ()

  in aux (t, j) handle SAME () => t end

(* hol_context -> term -> term *)

fun destroy_existential_equalities ({thy, stds, ...} : hol_context) =

  let

    (* string list -> typ list -> term list -> term *)

    fun kill [] [] ts = foldr1 s_conj ts

      | kill (s :: ss) (T :: Ts) ts =

        (case find_bound_assign thy stds (length ss) [] ts of

           SOME (_, []) => @{const True}

         | SOME (arg_t, ts) =>

           kill ss Ts (map (subst_one_bound (length ss)

                                (incr_bv (~1, length ss + 1, arg_t))) ts)

         | NONE =>

           Const (@{const_name Ex}, (T --> bool_T) --> bool_T)

           $ Abs (s, T, kill ss Ts ts))

      | kill _ _ _ = raise UnequalLengths

    (* string list -> typ list -> term -> term *)

    fun gather ss Ts (Const (@{const_name Ex}, _) $ Abs (s1, T1, t1)) =

        gather (ss @ [s1]) (Ts @ [T1]) t1

      | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)

      | gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2

      | gather [] [] t = t

      | gather ss Ts t = kill ss Ts (conjuncts_of (gather [] [] t))

  in gather [] [] end

(** Skolemization **)

(* int -> int -> string *)

fun skolem_prefix_for k j =

  skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep

(* hol_context -> int -> term -> term *)

fun skolemize_term_and_more (hol_ctxt as {thy, def_table, skolems, ...})

                            skolem_depth =

  let

    (* int list -> int list *)

    val incrs = map (Integer.add 1)

    (* string list -> typ list -> int list -> int -> polarity -> term -> term *)

    fun aux ss Ts js depth polar t =

      let

        (* string -> typ -> string -> typ -> term -> term *)

        fun do_quantifier quant_s quant_T abs_s abs_T t =

          if not (loose_bvar1 (t, 0)) then

            aux ss Ts js depth polar (incr_boundvars ~1 t)

          else if depth <= skolem_depth andalso

                  is_positive_existential polar quant_s then

            let

              val j = length (!skolems) + 1

              val sko_s = skolem_prefix_for (length js) j ^ abs_s

              val _ = Unsynchronized.change skolems (cons (sko_s, ss))

              val sko_t = list_comb (Const (sko_s, rev Ts ---> abs_T),

                                     map Bound (rev js))

              val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) depth polar t)

            in

              if null js then betapply (abs_t, sko_t)

              else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t $ abs_t

            end

          else

            Const (quant_s, quant_T)

            $ Abs (abs_s, abs_T,

                   if is_higher_order_type abs_T then

                     t

                   else

                     aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js)

                         (depth + 1) polar t)

      in

        case t of

          Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>

          do_quantifier s0 T0 s1 T1 t1

        | @{const "==>"} $ t1 $ t2 =>

          @{const "==>"} $ aux ss Ts js depth (flip_polarity polar) t1

          $ aux ss Ts js depth polar t2

        | @{const Pure.conjunction} $ t1 $ t2 =>

          @{const Pure.conjunction} $ aux ss Ts js depth polar t1

          $ aux ss Ts js depth polar t2

        | @{const Trueprop} $ t1 =>

          @{const Trueprop} $ aux ss Ts js depth polar t1

        | @{const Not} $ t1 =>

          @{const Not} $ aux ss Ts js depth (flip_polarity polar) t1

        | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>

          do_quantifier s0 T0 s1 T1 t1

        | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>

          do_quantifier s0 T0 s1 T1 t1

        | @{const "op &"} $ t1 $ t2 =>

          @{const "op &"} $ aux ss Ts js depth polar t1

          $ aux ss Ts js depth polar t2

        | @{const "op |"} $ t1 $ t2 =>

          @{const "op |"} $ aux ss Ts js depth polar t1

          $ aux ss Ts js depth polar t2

        | @{const "op -->"} $ t1 $ t2 =>

          @{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1

          $ aux ss Ts js depth polar t2

        | (t0 as Const (@{const_name Let}, _)) $ t1 $ t2 =>

          t0 $ t1 $ aux ss Ts js depth polar t2

        | Const (x as (s, T)) =>

          if is_inductive_pred hol_ctxt x andalso

             not (is_well_founded_inductive_pred hol_ctxt x) then

            let

              val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)

              val (pref, connective, set_oper) =

                if gfp then

                  (lbfp_prefix, @{const "op |"},

                   @{const_name semilattice_sup_class.sup})

                else

                  (ubfp_prefix, @{const "op &"},

                   @{const_name semilattice_inf_class.inf})

              (* unit -> term *)

              fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x

                           |> aux ss Ts js depth polar

              fun neg () = Const (pref ^ s, T)

            in

              (case polar |> gfp ? flip_polarity of

                 Pos => pos ()

               | Neg => neg ()

               | Neut =>

                 if is_fun_type T then

                   let

                     val ((trunk_arg_Ts, rump_arg_T), body_T) =

                       T |> strip_type |>> split_last

                     val set_T = rump_arg_T --> body_T

                     (* (unit -> term) -> term *)

                     fun app f =

                       list_comb (f (),

                                  map Bound (length trunk_arg_Ts - 1 downto 0))

                   in

                     List.foldr absdummy

                                (Const (set_oper, set_T --> set_T --> set_T)

                                        $ app pos $ app neg) trunk_arg_Ts

                   end

                 else

                   connective $ pos () $ neg ())

            end

          else

            Const x

        | t1 $ t2 =>

          betapply (aux ss Ts [] (skolem_depth + 1) polar t1,

                    aux ss Ts [] depth Neut t2)

        | Abs (s, T, t1) => Abs (s, T, aux ss Ts (incrs js) depth polar t1)

        | _ => t

      end

  in aux [] [] [] 0 Pos end

(** Function specialization **)

(* term -> term list *)

fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2

  | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1

  | params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) =

    snd (strip_comb t1)

  | params_in_equation _ = []

(* styp -> styp -> int list -> term list -> term list -> term -> term *)

fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t =

  let

    val k = fold Integer.max (map maxidx_of_term (fixed_args @ extra_args)) 0

            + 1

    val t = map_aterms (fn Var ((s, i), T) => Var ((s, k + i), T) | t' => t') t

    val fixed_params = filter_indices fixed_js (params_in_equation t)

    (* term list -> term -> term *)

    fun aux args (Abs (s, T, t)) = list_comb (Abs (s, T, aux [] t), args)

      | aux args (t1 $ t2) = aux (aux [] t2 :: args) t1

      | aux args t =

        if t = Const x then

          list_comb (Const x', extra_args @ filter_out_indices fixed_js args)

        else

          let val j = find_index (curry (op =) t) fixed_params in

            list_comb (if j >= 0 then nth fixed_args j else t, args)

          end

  in aux [] t end

(* hol_context -> styp -> (int * term option) list *)

fun static_args_in_term ({ersatz_table, ...} : hol_context) x t =

  let

    (* term -> term list -> term list -> term list list *)

    fun fun_calls (Abs (_, _, t)) _ = fun_calls t []

      | fun_calls (t1 $ t2) args = fun_calls t2 [] #> fun_calls t1 (t2 :: args)

      | fun_calls t args =

        (case t of

           Const (x' as (s', T')) =>

           x = x' orelse (case AList.lookup (op =) ersatz_table s' of

                            SOME s'' => x = (s'', T')

                          | NONE => false)

         | _ => false) ? cons args

    (* term list list -> term list list -> term list -> term list list *)

    fun call_sets [] [] vs = [vs]

      | call_sets [] uss vs = vs :: call_sets uss [] []

      | call_sets ([] :: _) _ _ = []

      | call_sets ((t :: ts) :: tss) uss vs =

        OrdList.insert TermOrd.term_ord t vs |> call_sets tss (ts :: uss)

    val sets = call_sets (fun_calls t [] []) [] []

    val indexed_sets = sets ~~ (index_seq 0 (length sets))

  in

    fold_rev (fn (set, j) =>

                 case set of

                   [Var _] => AList.lookup (op =) indexed_sets set = SOME j

                              ? cons (j, NONE)

                 | [t as Const _] => cons (j, SOME t)

                 | [t as Free _] => cons (j, SOME t)

                 | _ => I) indexed_sets []

  end

(* hol_context -> styp -> term list -> (int * term option) list *)

fun static_args_in_terms hol_ctxt x =

  map (static_args_in_term hol_ctxt x)

  #> fold1 (OrdList.inter (prod_ord int_ord (option_ord TermOrd.term_ord)))

(* (int * term option) list -> (int * term) list -> int list *)

fun overlapping_indices [] _ = []

  | overlapping_indices _ [] = []

  | overlapping_indices (ps1 as (j1, t1) :: ps1') (ps2 as (j2, t2) :: ps2') =

    if j1 < j2 then overlapping_indices ps1' ps2

    else if j1 > j2 then overlapping_indices ps1 ps2'

    else overlapping_indices ps1' ps2' |> the_default t2 t1 = t2 ? cons j1

(* typ list -> term -> bool *)

fun is_eligible_arg Ts t =

  let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in

    null bad_Ts orelse

    (is_higher_order_type (fastype_of1 (Ts, t)) andalso

     forall (not o is_higher_order_type) bad_Ts)

  end

(* int -> string *)

fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep

(* If a constant's definition is picked up deeper than this threshold, we

   prevent excessive specialization by not specializing it. *)

val special_max_depth = 20

val bound_var_prefix = "b"

(* hol_context -> int -> term -> term *)

fun specialize_consts_in_term (hol_ctxt as {specialize, simp_table,

                                            special_funs, ...}) depth t =

  if not specialize orelse depth > special_max_depth then

    t

  else

    let

      val blacklist = if depth = 0 then []

                      else case term_under_def t of Const x => [x] | _ => []

      (* term list -> typ list -> term -> term *)

      fun aux args Ts (Const (x as (s, T))) =

          ((if not (member (op =) blacklist x) andalso not (null args) andalso

               not (String.isPrefix special_prefix s) andalso

               is_equational_fun hol_ctxt x then

              let

                val eligible_args = filter (is_eligible_arg Ts o snd)

                                           (index_seq 0 (length args) ~~ args)

                val _ = not (null eligible_args) orelse raise SAME ()

                val old_axs = equational_fun_axioms hol_ctxt x

                              |> map (destroy_existential_equalities hol_ctxt)

                val static_params = static_args_in_terms hol_ctxt x old_axs

                val fixed_js = overlapping_indices static_params eligible_args

                val _ = not (null fixed_js) orelse raise SAME ()

                val fixed_args = filter_indices fixed_js args

                val vars = fold Term.add_vars fixed_args []

                           |> sort (TermOrd.fast_indexname_ord o pairself fst)

                val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js))

                                    fixed_args []

                               |> sort int_ord

                val live_args = filter_out_indices fixed_js args

                val extra_args = map Var vars @ map Bound bound_js @ live_args

                val extra_Ts = map snd vars @ filter_indices bound_js Ts

                val k = maxidx_of_term t + 1

                (* int -> term *)

                fun var_for_bound_no j =

                  Var ((bound_var_prefix ^

                        nat_subscript (find_index (curry (op =) j) bound_js

                                       + 1), k),

                       nth Ts j)

                val fixed_args_in_axiom =

                  map (curry subst_bounds

                             (map var_for_bound_no (index_seq 0 (length Ts))))

                      fixed_args

              in

                case AList.lookup (op =) (!special_funs)

                                  (x, fixed_js, fixed_args_in_axiom) of

                  SOME x' => list_comb (Const x', extra_args)

                | NONE =>

                  let

                    val extra_args_in_axiom =

                      map Var vars @ map var_for_bound_no bound_js

                    val x' as (s', _) =

                      (special_prefix_for (length (!special_funs) + 1) ^ s,

                       extra_Ts @ filter_out_indices fixed_js (binder_types T)

                       ---> body_type T)

                    val new_axs =

                      map (specialize_fun_axiom x x' fixed_js

                               fixed_args_in_axiom extra_args_in_axiom) old_axs

                    val _ =

                      Unsynchronized.change special_funs

                          (cons ((x, fixed_js, fixed_args_in_axiom), x'))

                    val _ = add_simps simp_table s' new_axs

                  in list_comb (Const x', extra_args) end

              end

            else

              raise SAME ())

           handle SAME () => list_comb (Const x, args))

        | aux args Ts (Abs (s, T, t)) =

          list_comb (Abs (s, T, aux [] (T :: Ts) t), args)

        | aux args Ts (t1 $ t2) = aux (aux [] Ts t2 :: args) Ts t1

        | aux args _ t = list_comb (t, args)

    in aux [] [] t end

type special_triple = int list * term list * styp

val cong_var_prefix = "c"

(* typ -> special_triple -> special_triple -> term *)

fun special_congruence_axiom T (js1, ts1, x1) (js2, ts2, x2) =

  let

    val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2)

    val Ts = binder_types T

    val max_j = fold (fold Integer.max) [js1, js2] ~1

    val (eqs, (args1, args2)) =

      fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j)

                                  (js1 ~~ ts1, js2 ~~ ts2) of

                      (SOME t1, SOME t2) => apfst (cons (t1, t2))

                    | (SOME t1, NONE) => apsnd (apsnd (cons t1))

                    | (NONE, SOME t2) => apsnd (apfst (cons t2))

                    | (NONE, NONE) =>

                      let val v = Var ((cong_var_prefix ^ nat_subscript j, 0),

                                       nth Ts j) in

                        apsnd (pairself (cons v))

                      end) (max_j downto 0) ([], ([], []))

  in

    Logic.list_implies (eqs |> filter_out (op =) |> distinct (op =)

                            |> map Logic.mk_equals,

                        Logic.mk_equals (list_comb (Const x1, bounds1 @ args1),

                                         list_comb (Const x2, bounds2 @ args2)))

    |> close_form (* TODO: needed? *)

  end

(* hol_context -> styp list -> term list *)

fun special_congruence_axioms (hol_ctxt as {special_funs, ...}) xs =

  let

    val groups =

      !special_funs

      |> map (fn ((x, js, ts), x') => (x, (js, ts, x')))

      |> AList.group (op =)

      |> filter_out (is_equational_fun_surely_complete hol_ctxt o fst)

      |> map (fn (x, zs) => (x, zs |> member (op =) xs x ? cons ([], [], x)))

    (* special_triple -> int *)

    fun generality (js, _, _) = ~(length js)

    (* special_triple -> special_triple -> bool *)

    fun is_more_specific (j1, t1, x1) (j2, t2, x2) =

      x1 <> x2 andalso OrdList.subset (prod_ord int_ord TermOrd.term_ord)

                                      (j2 ~~ t2, j1 ~~ t1)

    (* typ -> special_triple list -> special_triple list -> special_triple list

       -> term list -> term list *)

    fun do_pass_1 _ [] [_] [_] = I

      | do_pass_1 T skipped _ [] = do_pass_2 T skipped

      | do_pass_1 T skipped all (z :: zs) =

        case filter (is_more_specific z) all

             |> sort (int_ord o pairself generality) of

          [] => do_pass_1 T (z :: skipped) all zs

        | (z' :: _) => cons (special_congruence_axiom T z z')

                       #> do_pass_1 T skipped all zs

    (* typ -> special_triple list -> term list -> term list *)

    and do_pass_2 _ [] = I

      | do_pass_2 T (z :: zs) =

        fold (cons o special_congruence_axiom T z) zs #> do_pass_2 T zs

  in fold (fn ((_, T), zs) => do_pass_1 T [] zs zs) groups [] end

(** Axiom selection **)

(* Similar to "Refute.specialize_type" but returns all matches rather than only

   the first (preorder) match. *)

(* theory -> styp -> term -> term list *)

fun multi_specialize_type thy slack (s, T) t =

  let

    (* term -> (typ * term) list -> (typ * term) list *)

    fun aux (Const (s', T')) ys =

        if s = s' then

          ys |> (if AList.defined (op =) ys T' then

                   I

                 else

                  cons (T', Refute.monomorphic_term

                                (Sign.typ_match thy (T', T) Vartab.empty) t)

                  handle Type.TYPE_MATCH => I

                       | Refute.REFUTE _ =>

                         if slack then