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