src/HOL/Tools/ATP/atp_util.ML
author blanchet
Sun Jul 17 14:21:19 2011 +0200 (2011-07-17)
changeset 43864 58a7b3fdc193
parent 43863 a43d61270142
child 44392 6750b4297691
permissions -rw-r--r--
fixed lambda-liftg: must ensure the formulas are in close form
blanchet@43085
     1
(*  Title:      HOL/Tools/ATP/atp_util.ML
blanchet@43085
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@43085
     3
blanchet@43085
     4
General-purpose functions used by the ATP module.
blanchet@43085
     5
*)
blanchet@43085
     6
blanchet@43085
     7
signature ATP_UTIL =
blanchet@43085
     8
sig
blanchet@43085
     9
  val timestamp : unit -> string
blanchet@43827
    10
  val hash_string : string -> int
blanchet@43827
    11
  val hash_term : term -> int
blanchet@43085
    12
  val strip_spaces : bool -> (char -> bool) -> string -> string
blanchet@43085
    13
  val nat_subscript : int -> string
blanchet@43085
    14
  val unyxml : string -> string
blanchet@43085
    15
  val maybe_quote : string -> string
blanchet@43085
    16
  val string_from_ext_time : bool * Time.time -> string
blanchet@43085
    17
  val string_from_time : Time.time -> string
blanchet@43085
    18
  val varify_type : Proof.context -> typ -> typ
blanchet@43085
    19
  val instantiate_type : theory -> typ -> typ -> typ -> typ
blanchet@43085
    20
  val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ
blanchet@43085
    21
  val typ_of_dtyp :
blanchet@43085
    22
    Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp
blanchet@43085
    23
    -> typ
blanchet@43572
    24
  val is_type_surely_finite : Proof.context -> bool -> typ -> bool
blanchet@43572
    25
  val is_type_surely_infinite : Proof.context -> bool -> typ -> bool
blanchet@43863
    26
  val s_not : term -> term
blanchet@43863
    27
  val s_conj : term * term -> term
blanchet@43863
    28
  val s_disj : term * term -> term
blanchet@43863
    29
  val s_imp : term * term -> term
blanchet@43863
    30
  val s_iff : term * term -> term
blanchet@43864
    31
  val close_form : term -> term
blanchet@43085
    32
  val monomorphic_term : Type.tyenv -> term -> term
blanchet@43085
    33
  val eta_expand : typ list -> term -> int -> term
blanchet@43085
    34
  val transform_elim_prop : term -> term
blanchet@43085
    35
  val specialize_type : theory -> (string * typ) -> term -> term
blanchet@43085
    36
  val strip_subgoal :
blanchet@43085
    37
    Proof.context -> thm -> int -> (string * typ) list * term list * term
blanchet@43085
    38
end;
blanchet@43085
    39
blanchet@43085
    40
structure ATP_Util : ATP_UTIL =
blanchet@43085
    41
struct
blanchet@43085
    42
blanchet@43085
    43
val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
blanchet@43085
    44
blanchet@43085
    45
(* This hash function is recommended in "Compilers: Principles, Techniques, and
blanchet@43085
    46
   Tools" by Aho, Sethi, and Ullman. The "hashpjw" function, which they
blanchet@43085
    47
   particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *)
blanchet@43085
    48
fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
blanchet@43085
    49
fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)
blanchet@43085
    50
fun hashw_string (s : string, w) = CharVector.foldl hashw_char w s
blanchet@43827
    51
fun hashw_term (t1 $ t2) = hashw (hashw_term t1, hashw_term t2)
blanchet@43827
    52
  | hashw_term (Const (s, _)) = hashw_string (s, 0w0)
blanchet@43827
    53
  | hashw_term (Free (s, _)) = hashw_string (s, 0w0)
blanchet@43827
    54
  | hashw_term _ = 0w0
blanchet@43827
    55
blanchet@43827
    56
fun hash_string s = Word.toInt (hashw_string (s, 0w0))
blanchet@43827
    57
val hash_term = Word.toInt o hashw_term
blanchet@43085
    58
blanchet@43085
    59
fun strip_c_style_comment _ [] = []
blanchet@43085
    60
  | strip_c_style_comment is_evil (#"*" :: #"/" :: cs) =
blanchet@43085
    61
    strip_spaces_in_list true is_evil cs
blanchet@43085
    62
  | strip_c_style_comment is_evil (_ :: cs) = strip_c_style_comment is_evil cs
blanchet@43085
    63
and strip_spaces_in_list _ _ [] = []
blanchet@43085
    64
  | strip_spaces_in_list true is_evil (#"%" :: cs) =
blanchet@43085
    65
    strip_spaces_in_list true is_evil
blanchet@43085
    66
                         (cs |> chop_while (not_equal #"\n") |> snd)
blanchet@43085
    67
  | strip_spaces_in_list true is_evil (#"/" :: #"*" :: cs) =
blanchet@43085
    68
    strip_c_style_comment is_evil cs
blanchet@43085
    69
  | strip_spaces_in_list _ _ [c1] = if Char.isSpace c1 then [] else [str c1]
blanchet@43085
    70
  | strip_spaces_in_list skip_comments is_evil [c1, c2] =
blanchet@43085
    71
    strip_spaces_in_list skip_comments is_evil [c1] @
blanchet@43085
    72
    strip_spaces_in_list skip_comments is_evil [c2]
blanchet@43085
    73
  | strip_spaces_in_list skip_comments is_evil (c1 :: c2 :: c3 :: cs) =
blanchet@43085
    74
    if Char.isSpace c1 then
blanchet@43085
    75
      strip_spaces_in_list skip_comments is_evil (c2 :: c3 :: cs)
blanchet@43085
    76
    else if Char.isSpace c2 then
blanchet@43085
    77
      if Char.isSpace c3 then
blanchet@43085
    78
        strip_spaces_in_list skip_comments is_evil (c1 :: c3 :: cs)
blanchet@43085
    79
      else
blanchet@43085
    80
        str c1 :: (if forall is_evil [c1, c3] then [" "] else []) @
blanchet@43085
    81
        strip_spaces_in_list skip_comments is_evil (c3 :: cs)
blanchet@43085
    82
    else
blanchet@43085
    83
      str c1 :: strip_spaces_in_list skip_comments is_evil (c2 :: c3 :: cs)
blanchet@43085
    84
fun strip_spaces skip_comments is_evil =
blanchet@43085
    85
  implode o strip_spaces_in_list skip_comments is_evil o String.explode
blanchet@43085
    86
blanchet@43085
    87
val subscript = implode o map (prefix "\<^isub>") o raw_explode  (* FIXME Symbol.explode (?) *)
blanchet@43085
    88
fun nat_subscript n =
blanchet@43085
    89
  n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
blanchet@43085
    90
blanchet@43085
    91
val unyxml = XML.content_of o YXML.parse_body
blanchet@43085
    92
blanchet@43085
    93
val is_long_identifier = forall Lexicon.is_identifier o space_explode "."
blanchet@43085
    94
fun maybe_quote y =
blanchet@43085
    95
  let val s = unyxml y in
blanchet@43085
    96
    y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso
blanchet@43085
    97
           not (is_long_identifier (perhaps (try (unprefix "?")) s))) orelse
blanchet@43085
    98
           Keyword.is_keyword s) ? quote
blanchet@43085
    99
  end
blanchet@43085
   100
blanchet@43085
   101
fun string_from_ext_time (plus, time) =
blanchet@43085
   102
  let val ms = Time.toMilliseconds time in
blanchet@43085
   103
    (if plus then "> " else "") ^
blanchet@43085
   104
    (if plus andalso ms mod 1000 = 0 then
blanchet@43085
   105
       signed_string_of_int (ms div 1000) ^ " s"
blanchet@43085
   106
     else if ms < 1000 then
blanchet@43085
   107
       signed_string_of_int ms ^ " ms"
blanchet@43085
   108
     else
blanchet@43085
   109
       string_of_real (0.01 * Real.fromInt (ms div 10)) ^ " s")
blanchet@43085
   110
  end
blanchet@43085
   111
blanchet@43085
   112
val string_from_time = string_from_ext_time o pair false
blanchet@43085
   113
blanchet@43085
   114
fun varify_type ctxt T =
blanchet@43085
   115
  Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)]
blanchet@43085
   116
  |> snd |> the_single |> dest_Const |> snd
blanchet@43085
   117
blanchet@43085
   118
(* TODO: use "Term_Subst.instantiateT" instead? *)
blanchet@43085
   119
fun instantiate_type thy T1 T1' T2 =
blanchet@43085
   120
  Same.commit (Envir.subst_type_same
blanchet@43085
   121
                   (Sign.typ_match thy (T1, T1') Vartab.empty)) T2
blanchet@43085
   122
  handle Type.TYPE_MATCH => raise TYPE ("instantiate_type", [T1, T1'], [])
blanchet@43085
   123
blanchet@43085
   124
fun varify_and_instantiate_type ctxt T1 T1' T2 =
blanchet@43085
   125
  let val thy = Proof_Context.theory_of ctxt in
blanchet@43085
   126
    instantiate_type thy (varify_type ctxt T1) T1' (varify_type ctxt T2)
blanchet@43085
   127
  end
blanchet@43085
   128
blanchet@43085
   129
fun typ_of_dtyp _ typ_assoc (Datatype_Aux.DtTFree a) =
blanchet@43085
   130
    the (AList.lookup (op =) typ_assoc (Datatype_Aux.DtTFree a))
blanchet@43085
   131
  | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtType (s, Us)) =
blanchet@43085
   132
    Type (s, map (typ_of_dtyp descr typ_assoc) Us)
blanchet@43085
   133
  | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtRec i) =
blanchet@43085
   134
    let val (s, ds, _) = the (AList.lookup (op =) descr i) in
blanchet@43085
   135
      Type (s, map (typ_of_dtyp descr typ_assoc) ds)
blanchet@43085
   136
    end
blanchet@43085
   137
blanchet@43085
   138
fun datatype_constrs thy (T as Type (s, Ts)) =
blanchet@43085
   139
    (case Datatype.get_info thy s of
blanchet@43085
   140
       SOME {index, descr, ...} =>
blanchet@43085
   141
       let val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the in
blanchet@43085
   142
         map (apsnd (fn Us => map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T))
blanchet@43085
   143
             constrs
blanchet@43085
   144
       end
blanchet@43085
   145
     | NONE => [])
blanchet@43085
   146
  | datatype_constrs _ _ = []
blanchet@43085
   147
blanchet@43085
   148
(* Similar to "Nitpick_HOL.bounded_exact_card_of_type".
blanchet@43085
   149
   0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means
blanchet@43085
   150
   cardinality 2 or more. The specified default cardinality is returned if the
blanchet@43085
   151
   cardinality of the type can't be determined. *)
blanchet@43572
   152
fun tiny_card_of_type ctxt sound default_card T =
blanchet@43085
   153
  let
blanchet@43085
   154
    val thy = Proof_Context.theory_of ctxt
blanchet@43085
   155
    val max = 2 (* 1 would be too small for the "fun" case *)
blanchet@43085
   156
    fun aux slack avoid T =
blanchet@43085
   157
      if member (op =) avoid T then
blanchet@43085
   158
        0
blanchet@43423
   159
      else case T of
blanchet@43423
   160
        Type (@{type_name fun}, [T1, T2]) =>
blanchet@43423
   161
        (case (aux slack avoid T1, aux slack avoid T2) of
blanchet@43423
   162
           (k, 1) => if slack andalso k = 0 then 0 else 1
blanchet@43423
   163
         | (0, _) => 0
blanchet@43423
   164
         | (_, 0) => 0
blanchet@43423
   165
         | (k1, k2) =>
blanchet@43423
   166
           if k1 >= max orelse k2 >= max then max
blanchet@43423
   167
           else Int.min (max, Integer.pow k2 k1))
blanchet@43423
   168
      | @{typ prop} => 2
blanchet@43423
   169
      | @{typ bool} => 2 (* optimization *)
blanchet@43423
   170
      | @{typ nat} => 0 (* optimization *)
blanchet@43423
   171
      | Type ("Int.int", []) => 0 (* optimization *)
blanchet@43423
   172
      | Type (s, _) =>
blanchet@43423
   173
        (case datatype_constrs thy T of
blanchet@43423
   174
           constrs as _ :: _ =>
blanchet@43423
   175
           let
blanchet@43423
   176
             val constr_cards =
blanchet@43423
   177
               map (Integer.prod o map (aux slack (T :: avoid)) o binder_types
blanchet@43423
   178
                    o snd) constrs
blanchet@43423
   179
           in
blanchet@43423
   180
             if exists (curry (op =) 0) constr_cards then 0
blanchet@43423
   181
             else Int.min (max, Integer.sum constr_cards)
blanchet@43423
   182
           end
blanchet@43423
   183
         | [] =>
blanchet@43423
   184
           case Typedef.get_info ctxt s of
blanchet@43423
   185
             ({abs_type, rep_type, ...}, _) :: _ =>
blanchet@43423
   186
             (* We cheat here by assuming that typedef types are infinite if
blanchet@43423
   187
                their underlying type is infinite. This is unsound in general
blanchet@43423
   188
                but it's hard to think of a realistic example where this would
blanchet@43423
   189
                not be the case. We are also slack with representation types:
blanchet@43423
   190
                If a representation type has the form "sigma => tau", we
blanchet@43423
   191
                consider it enough to check "sigma" for infiniteness. (Look
blanchet@43423
   192
                for "slack" in this function.) *)
blanchet@43423
   193
             (case varify_and_instantiate_type ctxt
blanchet@43423
   194
                       (Logic.varifyT_global abs_type) T
blanchet@43423
   195
                       (Logic.varifyT_global rep_type)
blanchet@43423
   196
                   |> aux true avoid of
blanchet@43572
   197
                0 => if sound then default_card else 0
blanchet@43423
   198
              | 1 => 1
blanchet@43423
   199
              | _ => default_card)
blanchet@43423
   200
           | [] => default_card)
blanchet@43423
   201
        (* Very slightly unsound: Type variables are assumed not to be
blanchet@43423
   202
           constrained to cardinality 1. (In practice, the user would most
blanchet@43423
   203
           likely have used "unit" directly anyway.) *)
blanchet@43572
   204
      | TFree _ =>
blanchet@43572
   205
        if default_card = 1 andalso not sound then 2 else default_card
blanchet@43423
   206
      | TVar _ => default_card
blanchet@43085
   207
  in Int.min (max, aux false [] T) end
blanchet@43085
   208
blanchet@43572
   209
fun is_type_surely_finite ctxt sound T = tiny_card_of_type ctxt sound 0 T <> 0
blanchet@43572
   210
fun is_type_surely_infinite ctxt sound T = tiny_card_of_type ctxt sound 1 T = 0
blanchet@43085
   211
blanchet@43863
   212
(* Simple simplifications to ensure that sort annotations don't leave a trail of
blanchet@43863
   213
   spurious "True"s. *)
blanchet@43863
   214
fun s_not (Const (@{const_name All}, T) $ Abs (s, T', t')) =
blanchet@43863
   215
    Const (@{const_name Ex}, T) $ Abs (s, T', s_not t')
blanchet@43863
   216
  | s_not (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
blanchet@43863
   217
    Const (@{const_name All}, T) $ Abs (s, T', s_not t')
blanchet@43863
   218
  | s_not (@{const HOL.implies} $ t1 $ t2) = @{const HOL.conj} $ t1 $ s_not t2
blanchet@43863
   219
  | s_not (@{const HOL.conj} $ t1 $ t2) =
blanchet@43863
   220
    @{const HOL.disj} $ s_not t1 $ s_not t2
blanchet@43863
   221
  | s_not (@{const HOL.disj} $ t1 $ t2) =
blanchet@43863
   222
    @{const HOL.conj} $ s_not t1 $ s_not t2
blanchet@43863
   223
  | s_not (@{const False}) = @{const True}
blanchet@43863
   224
  | s_not (@{const True}) = @{const False}
blanchet@43863
   225
  | s_not (@{const Not} $ t) = t
blanchet@43863
   226
  | s_not t = @{const Not} $ t
blanchet@43863
   227
fun s_conj (@{const True}, t2) = t2
blanchet@43863
   228
  | s_conj (t1, @{const True}) = t1
blanchet@43863
   229
  | s_conj p = HOLogic.mk_conj p
blanchet@43863
   230
fun s_disj (@{const False}, t2) = t2
blanchet@43863
   231
  | s_disj (t1, @{const False}) = t1
blanchet@43863
   232
  | s_disj p = HOLogic.mk_disj p
blanchet@43863
   233
fun s_imp (@{const True}, t2) = t2
blanchet@43863
   234
  | s_imp (t1, @{const False}) = s_not t1
blanchet@43863
   235
  | s_imp p = HOLogic.mk_imp p
blanchet@43863
   236
fun s_iff (@{const True}, t2) = t2
blanchet@43863
   237
  | s_iff (t1, @{const True}) = t1
blanchet@43863
   238
  | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
blanchet@43863
   239
blanchet@43864
   240
fun close_form t =
blanchet@43864
   241
  fold (fn ((x, i), T) => fn t' =>
blanchet@43864
   242
           HOLogic.all_const T $ Abs (x, T, abstract_over (Var ((x, i), T), t')))
blanchet@43864
   243
       (Term.add_vars t []) t
blanchet@43864
   244
blanchet@43171
   245
fun monomorphic_term subst =
blanchet@43085
   246
  map_types (map_type_tvar (fn v =>
blanchet@43085
   247
      case Type.lookup subst v of
blanchet@43085
   248
        SOME typ => typ
blanchet@43171
   249
      | NONE => TVar v))
blanchet@43085
   250
blanchet@43085
   251
fun eta_expand _ t 0 = t
blanchet@43085
   252
  | eta_expand Ts (Abs (s, T, t')) n =
blanchet@43085
   253
    Abs (s, T, eta_expand (T :: Ts) t' (n - 1))
blanchet@43085
   254
  | eta_expand Ts t n =
blanchet@43085
   255
    fold_rev (fn T => fn t' => Abs ("x" ^ nat_subscript n, T, t'))
blanchet@43085
   256
             (List.take (binder_types (fastype_of1 (Ts, t)), n))
blanchet@43085
   257
             (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
blanchet@43085
   258
blanchet@43085
   259
(* Converts an elim-rule into an equivalent theorem that does not have the
blanchet@43085
   260
   predicate variable. Leaves other theorems unchanged. We simply instantiate
blanchet@43085
   261
   the conclusion variable to False. (Cf. "transform_elim_theorem" in
blanchet@43085
   262
   "Meson_Clausify".) *)
blanchet@43085
   263
fun transform_elim_prop t =
blanchet@43085
   264
  case Logic.strip_imp_concl t of
blanchet@43085
   265
    @{const Trueprop} $ Var (z, @{typ bool}) =>
blanchet@43085
   266
    subst_Vars [(z, @{const False})] t
blanchet@43085
   267
  | Var (z, @{typ prop}) => subst_Vars [(z, @{prop False})] t
blanchet@43085
   268
  | _ => t
blanchet@43085
   269
blanchet@43085
   270
fun specialize_type thy (s, T) t =
blanchet@43085
   271
  let
blanchet@43085
   272
    fun subst_for (Const (s', T')) =
blanchet@43085
   273
      if s = s' then
blanchet@43085
   274
        SOME (Sign.typ_match thy (T', T) Vartab.empty)
blanchet@43085
   275
        handle Type.TYPE_MATCH => NONE
blanchet@43085
   276
      else
blanchet@43085
   277
        NONE
blanchet@43085
   278
    | subst_for (t1 $ t2) =
blanchet@43085
   279
      (case subst_for t1 of SOME x => SOME x | NONE => subst_for t2)
blanchet@43085
   280
    | subst_for (Abs (_, _, t')) = subst_for t'
blanchet@43085
   281
    | subst_for _ = NONE
blanchet@43085
   282
  in
blanchet@43085
   283
    case subst_for t of
blanchet@43085
   284
      SOME subst => monomorphic_term subst t
blanchet@43085
   285
    | NONE => raise Type.TYPE_MATCH
blanchet@43085
   286
  end
blanchet@43085
   287
blanchet@43085
   288
fun strip_subgoal ctxt goal i =
blanchet@43085
   289
  let
blanchet@43085
   290
    val (t, (frees, params)) =
blanchet@43085
   291
      Logic.goal_params (prop_of goal) i
blanchet@43085
   292
      ||> (map dest_Free #> Variable.variant_frees ctxt [] #> `(map Free))
blanchet@43085
   293
    val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees)
blanchet@43085
   294
    val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
blanchet@43085
   295
  in (rev params, hyp_ts, concl_t) end
blanchet@43085
   296
blanchet@43085
   297
end;