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