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