1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Jun 16 11:59:29 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Jun 16 13:50:35 2011 +0200
     1.3 @@ -40,7 +40,9 @@
     1.4      CombVar of name * typ |
     1.5      CombApp of combterm * combterm
     1.6  
     1.7 -  datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
     1.8 +  datatype locality =
     1.9 +    General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
    1.10 +    Chained
    1.11  
    1.12    datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
    1.13    datatype type_level =
    1.14 @@ -534,7 +536,9 @@
    1.15      |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T))
    1.16    | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
    1.17  
    1.18 -datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
    1.19 +datatype locality =
    1.20 +  General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
    1.21 +  Chained
    1.22  
    1.23  (* (quasi-)underapproximation of the truth *)
    1.24  fun is_locality_global Local = false
    1.25 @@ -1357,7 +1361,7 @@
    1.26            (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
    1.27            (if needs_fairly_sound then typed_helper_suffix
    1.28             else untyped_helper_suffix),
    1.29 -          General),
    1.30 +          Helper),
    1.31           let val t = th |> prop_of in
    1.32             t |> should_specialize_helper type_sys t
    1.33                  ? (case types of
    1.34 @@ -1467,12 +1471,12 @@
    1.35    CombApp (CombConst (type_pred, T --> @{typ bool}, [T])
    1.36             |> enforce_type_arg_policy_in_combterm ctxt format type_sys, tm)
    1.37  
    1.38 -fun var_occurs_positively_naked_in_term _ (SOME false) _ accum = accum
    1.39 -  | var_occurs_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
    1.40 +fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
    1.41 +  | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
    1.42      accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
    1.43  fun is_var_nonmonotonic_in_formula _ _ (SOME false) _ = false
    1.44    | is_var_nonmonotonic_in_formula pos phi _ name =
    1.45 -    formula_fold pos (var_occurs_positively_naked_in_term name) phi false
    1.46 +    formula_fold pos (is_var_positively_naked_in_term name) phi false
    1.47  
    1.48  fun mk_const_aterm format type_sys x T_args args =
    1.49    ATerm (x, map_filter (fo_term_for_type_arg format type_sys) T_args @ args)
    1.50 @@ -1666,8 +1670,12 @@
    1.51      (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
    1.52       (case level of
    1.53          Noninf_Nonmono_Types =>
    1.54 +        (* Unlike virtually any other polymorphic fact whose type variables can
    1.55 +           be instantiated by a known infinite type, extensionality actually
    1.56 +           encodes a cardinality constraints. *)
    1.57          not (is_locality_global locality) orelse
    1.58 -        not (is_type_surely_infinite ctxt known_infinite_types T)
    1.59 +        not (is_type_surely_infinite ctxt (if locality = Extensionality then []
    1.60 +                                           else known_infinite_types) T)
    1.61        | Fin_Nonmono_Types => is_type_surely_finite ctxt T
    1.62        | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
    1.63    | add_combterm_nonmonotonic_types _ _ _ _ _ = I