# HG changeset patch
# User blanchet
# Date 1351679001 -3600
# Node ID 33e18e9916a884b94b2f35807502489622b40ca9
# Parent  724cfe0131823845c03cb6874c8c25140d75cb61
use metaquantification when possible in Isar proofs

diff -r 724cfe013182 -r 33e18e9916a8 src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Wed Oct 31 11:23:21 2012 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML	Wed Oct 31 11:23:21 2012 +0100
@@ -39,12 +39,6 @@
 
 (** TPTP parsing **)
 
-(* cf. "close_form" in "refute.ML" *)
-fun close_form t =
-  fold (fn ((s, i), T) => fn t' =>
-           Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t')))
-       (Term.add_vars t []) t
-
 fun read_tptp_file thy postproc file_name =
   let
     fun has_role role (_, role', _, _) = (role' = role)
diff -r 724cfe013182 -r 33e18e9916a8 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Oct 31 11:23:21 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Oct 31 11:23:21 2012 +0100
@@ -23,8 +23,9 @@
   val partial_type_encs : string list
   val metis_default_lam_trans : string
   val metis_call : string -> string -> string
+  val forall_of : term -> term -> term
+  val exists_of : term -> term -> term
   val unalias_type_enc : string -> string list
-  val forall_of : term -> term -> term
   val term_from_atp :
     Proof.context -> bool -> int Symtab.table -> typ option ->
     (string, string) ho_term -> term
diff -r 724cfe013182 -r 33e18e9916a8 src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Wed Oct 31 11:23:21 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML	Wed Oct 31 11:23:21 2012 +0100
@@ -34,6 +34,7 @@
   val s_disj : term * term -> term
   val s_imp : term * term -> term
   val s_iff : term * term -> term
+  val close_form : term -> term
   val hol_close_form_prefix : string
   val hol_close_form : term -> term
   val hol_open_form : (string -> string) -> term -> term
@@ -298,6 +299,12 @@
   | s_iff (t1, @{const True}) = t1
   | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
 
+(* cf. "close_form" in "refute.ML" *)
+fun close_form t =
+  fold (fn ((s, i), T) => fn t' =>
+           Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t')))
+       (Term.add_vars t []) t
+
 val hol_close_form_prefix = "ATP.close_form."
 
 fun hol_close_form t =
diff -r 724cfe013182 -r 33e18e9916a8 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Oct 31 11:23:21 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Oct 31 11:23:21 2012 +0100
@@ -770,7 +770,7 @@
 
     (* Enrich context with local facts *)
     val thy = Proof_Context.theory_of ctxt
-    fun sorry t = Skip_Proof.make_thm thy (HOLogic.mk_Trueprop t)
+    fun sorry t = Skip_Proof.make_thm thy t
     fun enrich_ctxt' (Prove (_, lbl, t, _)) ctxt = 
         ctxt |> lbl <> no_label
           ? Proof_Context.put_thms false (string_for_label lbl, SOME [sorry t])
@@ -790,7 +790,7 @@
           |>> map string_for_label |> op @
           |> map (the_single o thms_of_name rich_ctxt)
           |> (if member (op =) qs Then then cons (the s0 |> thmify) else I)
-        val goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop t)
+        val goal = Goal.prove ctxt [] [] t
         fun tac {context = ctxt, prems = _} =
           Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1
       in
@@ -884,8 +884,13 @@
           |> fold (fn Definition_Step _ => I (* FIXME *)
                     | Inference_Step ((s, _), t, _, _) =>
                       Symtab.update_new (s,
-                          t |> fold forall_of (map Var (Term.add_vars t []))
-                            |> member (op = o apsnd fst) tainted s ? s_not))
+                          if member (op = o apsnd fst) tainted s then
+                            t |> s_not
+                              |> fold exists_of (map Var (Term.add_vars t []))
+                              |> HOLogic.mk_Trueprop
+                          else
+                            t |> HOLogic.mk_Trueprop
+                              |> close_form))
                   atp_proof
         fun prop_of_clause c =
           fold (curry s_disj) (map_filter (Symtab.lookup props o fst) c)