# HG changeset patch
# User blanchet
# Date 1308225035 -7200
# Node ID 926bfe067a32bb5c73ac08297c21fdd3e7ceaa00
# Parent  957617fe07650e1879a05e9d6fa96580c027a58f
fixed soundness bug related to extensionality

diff -r 957617fe0765 -r 926bfe067a32 src/HOL/Tools/ATP/atp_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Thu Jun 16 11:59:29 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Thu Jun 16 13:50:35 2011 +0200
@@ -215,7 +215,7 @@
     union (op =) (resolve_fact facts_offset fact_names name)
   | add_fact ctxt _ _ (Inference (_, _, deps)) =
     if AList.defined (op =) deps leo2_ext then
-      insert (op =) (ext_name ctxt, General (* or Chained... *))
+      insert (op =) (ext_name ctxt, Extensionality)
     else
       I
   | add_fact _ _ _ _ = I
diff -r 957617fe0765 -r 926bfe067a32 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Jun 16 11:59:29 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Jun 16 13:50:35 2011 +0200
@@ -40,7 +40,9 @@
     CombVar of name * typ |
     CombApp of combterm * combterm
 
-  datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
+  datatype locality =
+    General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
+    Chained
 
   datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
   datatype type_level =
@@ -534,7 +536,9 @@
     |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T))
   | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
 
-datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
+datatype locality =
+  General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
+  Chained
 
 (* (quasi-)underapproximation of the truth *)
 fun is_locality_global Local = false
@@ -1357,7 +1361,7 @@
           (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
           (if needs_fairly_sound then typed_helper_suffix
            else untyped_helper_suffix),
-          General),
+          Helper),
          let val t = th |> prop_of in
            t |> should_specialize_helper type_sys t
                 ? (case types of
@@ -1467,12 +1471,12 @@
   CombApp (CombConst (type_pred, T --> @{typ bool}, [T])
            |> enforce_type_arg_policy_in_combterm ctxt format type_sys, tm)
 
-fun var_occurs_positively_naked_in_term _ (SOME false) _ accum = accum
-  | var_occurs_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
+fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
+  | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
     accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
 fun is_var_nonmonotonic_in_formula _ _ (SOME false) _ = false
   | is_var_nonmonotonic_in_formula pos phi _ name =
-    formula_fold pos (var_occurs_positively_naked_in_term name) phi false
+    formula_fold pos (is_var_positively_naked_in_term name) phi false
 
 fun mk_const_aterm format type_sys x T_args args =
   ATerm (x, map_filter (fo_term_for_type_arg format type_sys) T_args @ args)
@@ -1666,8 +1670,12 @@
     (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
      (case level of
         Noninf_Nonmono_Types =>
+        (* Unlike virtually any other polymorphic fact whose type variables can
+           be instantiated by a known infinite type, extensionality actually
+           encodes a cardinality constraints. *)
         not (is_locality_global locality) orelse
-        not (is_type_surely_infinite ctxt known_infinite_types T)
+        not (is_type_surely_infinite ctxt (if locality = Extensionality then []
+                                           else known_infinite_types) T)
       | Fin_Nonmono_Types => is_type_surely_finite ctxt T
       | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
   | add_combterm_nonmonotonic_types _ _ _ _ _ = I
diff -r 957617fe0765 -r 926bfe067a32 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Jun 16 11:59:29 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu Jun 16 13:50:35 2011 +0200
@@ -141,9 +141,11 @@
   in
     (ths, (0, []))
     |-> fold (fn th => fn (j, rest) =>
-                 (j + 1, ((nth_name j,
-                          if member Thm.eq_thm_prop chained_ths th then Chained
-                          else General), th) :: rest))
+                 (j + 1,
+                  ((nth_name j,
+                    if member Thm.eq_thm_prop chained_ths th then Chained
+                    else if Thm.eq_thm_prop (th, @{thm ext}) then Extensionality
+                    else General), th) :: rest))
     |> snd
   end
 
@@ -479,13 +481,13 @@
                         chained_const_irrel_weight (irrel_weight_for fudge) swap
                         const_tab chained_const_tab
 
-fun locality_bonus (_ : relevance_fudge) General = 0.0
-  | locality_bonus {intro_bonus, ...} Intro = intro_bonus
+fun locality_bonus ({intro_bonus, ...} : relevance_fudge) Intro = intro_bonus
   | locality_bonus {elim_bonus, ...} Elim = elim_bonus
   | locality_bonus {simp_bonus, ...} Simp = simp_bonus
   | locality_bonus {local_bonus, ...} Local = local_bonus
   | locality_bonus {assum_bonus, ...} Assum = assum_bonus
   | locality_bonus {chained_bonus, ...} Chained = chained_bonus
+  | locality_bonus _ _ = 0.0
 
 fun is_odd_const_name s =
   s = abs_name orelse String.isPrefix skolem_prefix s orelse
@@ -827,7 +829,10 @@
       if is_chained th then
         Chained
       else if global then
-        Termtab.lookup clasimpset_table (prop_of th) |> the_default General
+        case Termtab.lookup clasimpset_table (prop_of th) of
+          SOME loc => loc
+        | NONE => if Thm.eq_thm_prop (th, @{thm ext}) then Extensionality
+                  else General
       else
         if is_assum th then Assum else Local
     fun is_good_unnamed_local th =