# HG changeset patch
# User paulson
# Date 1233231840 0
# Node ID aba49b4fe95974900e6fb5294a4aeb5852a17c2d
# Parent  fa6f988f1c502c8fcfcf83d5f91d687b90993d95# Parent  40bf9f4e7a4ed81e6ce9a1f0320684c1f79bff4b
Automated merge with ssh://paulson@atbroy100.informatik.tu-muenchen.de//home/isabelle-repository/repos/isabelle

diff -r fa6f988f1c50 -r aba49b4fe959 src/HOL/MetisExamples/Abstraction.thy
--- a/src/HOL/MetisExamples/Abstraction.thy	Thu Jan 29 09:35:51 2009 +0000
+++ b/src/HOL/MetisExamples/Abstraction.thy	Thu Jan 29 12:24:00 2009 +0000
@@ -62,9 +62,9 @@
 
 ML{*AtpWrapper.problem_name := "Abstraction__Sigma_Collect"*}
 lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
-(*???metis cannot prove this
-by (metis CollectD SigmaD1 SigmaD2 UN_eq)
-Also, UN_eq is unnecessary*)
+(*???metis says this is satisfiable!
+by (metis CollectD SigmaD1 SigmaD2)
+*)
 by (meson CollectD SigmaD1 SigmaD2)
 
 
diff -r fa6f988f1c50 -r aba49b4fe959 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Thu Jan 29 09:35:51 2009 +0000
+++ b/src/HOL/Tools/meson.ML	Thu Jan 29 12:24:00 2009 +0000
@@ -15,7 +15,6 @@
   val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
   val finish_cnf: thm list -> thm list
   val make_nnf: thm -> thm
-  val make_nnf1: thm -> thm
   val skolemize: thm -> thm
   val is_fol_term: theory -> term -> bool
   val make_clauses: thm list -> thm list
@@ -296,7 +295,7 @@
 (*Any need to extend this list with
   "HOL.type_class","HOL.eq_class","Pure.term"?*)
 val has_meta_conn =
-    exists_Const (member (op =) ["==", "==>", "all", "prop"] o #1);
+    exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1);
 
 fun apply_skolem_ths (th, rls) =
   let fun tryall [] = raise THM("apply_skolem_ths", 0, th::rls)
@@ -519,19 +518,21 @@
 
 (*Pull existential quantifiers to front. This accomplishes Skolemization for
   clauses that arise from a subgoal.*)
-fun skolemize th =
+fun skolemize1 th =
   if not (has_conns ["Ex"] (prop_of th)) then th
-  else (skolemize (tryres(th, [choice, conj_exD1, conj_exD2,
+  else (skolemize1 (tryres(th, [choice, conj_exD1, conj_exD2,
                               disj_exD, disj_exD1, disj_exD2])))
     handle THM ("tryres", _, _) =>
-        skolemize (forward_res skolemize
+        skolemize1 (forward_res skolemize1
                    (tryres (th, [conj_forward, disj_forward, all_forward])))
     handle THM ("tryres", _, _) => 
-        forward_res skolemize (rename_bvs_RS th ex_forward);
+        forward_res skolemize1 (rename_bvs_RS th ex_forward);
+
+fun skolemize th = skolemize1 (make_nnf th);
 
 fun skolemize_nnf_list [] = []
   | skolemize_nnf_list (th::ths) = 
-      skolemize (make_nnf th) :: skolemize_nnf_list ths
+      skolemize th :: skolemize_nnf_list ths
       handle THM _ => (*RS can fail if Unify.search_bound is too small*)
        (warning ("Failed to Skolemize " ^ Display.string_of_thm th);
         skolemize_nnf_list ths);
diff -r fa6f988f1c50 -r aba49b4fe959 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Thu Jan 29 09:35:51 2009 +0000
+++ b/src/HOL/Tools/res_clause.ML	Thu Jan 29 12:24:00 2009 +0000
@@ -279,6 +279,14 @@
 (*Given a list of sorted type variables, return a list of type literals.*)
 fun add_typs Ts = foldl (op union) [] (map sorts_on_typs Ts);
 
+(*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear.
+  * Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
+    in a lemma has the same sort as 'a in the conjecture.
+  * Deleting such clauses will lead to problems with locales in other use of local results
+    where 'a is fixed. Probably we should delete clauses unless the sorts agree.
+  * Currently we include a class constraint in the clause, exactly as with TVars.
+*)
+
 (** make axiom and conjecture clauses. **)
 
 fun get_tvar_strs [] = []