# HG changeset patch
# User blanchet
# Date 1304267843 -7200
# Node ID 02df3b78a4381cd7510a3ee22287114c9a253aea
# Parent  d1f7c4a01dbe33f99235a61c5311e931ba7d25de
get rid of "explicit_forall" prover-specific option, even if that means some clutter -- foralls will be necessary to attach types to variables

diff -r d1f7c4a01dbe -r 02df3b78a438 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Sun May 01 18:37:23 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Sun May 01 18:37:23 2011 +0200
@@ -16,7 +16,6 @@
      slices: unit -> (real * (bool * int)) list,
      proof_delims: (string * string) list,
      known_failures: (failure * string) list,
-     explicit_forall: bool,
      use_conjecture_for_hypotheses: bool}
 
   datatype e_weight_method =
@@ -63,7 +62,6 @@
    slices: unit -> (real * (bool * int)) list,
    proof_delims: (string * string) list,
    known_failures: (failure * string) list,
-   explicit_forall: bool,
    use_conjecture_for_hypotheses: bool}
 
 val known_perl_failures =
@@ -188,7 +186,6 @@
        "# Cannot determine problem status within resource limit"),
       (OutOfResources, "SZS status: ResourceOut"),
       (OutOfResources, "SZS status ResourceOut")],
-   explicit_forall = false,
    use_conjecture_for_hypotheses = true}
 
 val e = (eN, e_config)
@@ -217,7 +214,6 @@
       (MalformedInput, "Free Variable"),
       (SpassTooOld, "tptp2dfg"),
       (InternalError, "Please report this error")],
-   explicit_forall = true,
    use_conjecture_for_hypotheses = true}
 
 val spass = (spassN, spass_config)
@@ -251,7 +247,6 @@
       (Unprovable, "Termination reason: Satisfiable"),
       (VampireTooOld, "not a valid option"),
       (Interrupted, "Aborted by signal SIGINT")],
-   explicit_forall = false,
    use_conjecture_for_hypotheses = true}
 
 val vampire = (vampireN, vampire_config)
@@ -272,7 +267,6 @@
       (IncompleteUnprovable, "SZS status Satisfiable"),
       (ProofMissing, "\nunsat"),
       (ProofMissing, "SZS status Unsatisfiable")],
-   explicit_forall = true,
    use_conjecture_for_hypotheses = false}
 
 val z3_atp = (z3_atpN, z3_atp_config)
@@ -322,7 +316,6 @@
    known_failures =
      known_failures @ known_perl_failures @
      [(TimedOut, "says Timeout")],
-   explicit_forall = true,
    use_conjecture_for_hypotheses = use_conjecture_for_hypotheses}
 
 fun int_average f xs = fold (Integer.add o f) xs 0 div length xs
diff -r d1f7c4a01dbe -r 02df3b78a438 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:23 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:23 2011 +0200
@@ -29,7 +29,7 @@
     -> translated_formula option * ((string * 'a) * thm)
   val unmangled_const : string -> string * string fo_term list
   val prepare_atp_problem :
-    Proof.context -> bool -> bool -> type_system -> bool -> term list -> term
+    Proof.context -> bool -> type_system -> bool -> term list -> term
     -> (translated_formula option * ((string * 'a) * thm)) list
     -> string problem * string Symtab.table * int * (string * 'a) list vector
   val atp_problem_weights : string problem -> (string * real) list
@@ -291,7 +291,7 @@
   metis_helpers |> map fst |> sort_distinct string_ord |> map (rpair 0)
   |> Symtab.make
 
-fun get_helper_facts ctxt explicit_forall type_sys formulas =
+fun get_helper_facts ctxt type_sys formulas =
   let
     val no_dangerous_types = type_system_types_dangerous_types type_sys
     val ct = init_counters |> fold count_formula formulas
@@ -317,7 +317,7 @@
        in
          [Fof (helper_prefix ^ ascii_of "ti_ti", Axiom,
                AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")]))
-               |> explicit_forall ? close_universally, NONE)]
+               |> close_universally, NONE)]
        end
      else
        [])
@@ -652,7 +652,7 @@
   else
     t |> not (is_pred_sym pred_sym_tab s) ? boolify
 
-fun repair_formula thy explicit_forall type_sys sym_tab =
+fun repair_formula thy type_sys sym_tab =
   let
     val pred_sym_tab = case type_sys of Tags _ => NONE | _ => sym_tab
     fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
@@ -660,13 +660,11 @@
       | aux (AAtom tm) =
         AAtom (tm |> repair_applications_in_term thy type_sys sym_tab
                   |> repair_predicates_in_term pred_sym_tab)
-  in aux #> explicit_forall ? close_universally end
+  in aux #> close_universally end
 
-fun repair_problem_line thy explicit_forall type_sys sym_tab
-                        (Fof (ident, kind, phi, source)) =
-  Fof (ident, kind, repair_formula thy explicit_forall type_sys sym_tab phi,
-       source)
-fun repair_problem thy = map o apsnd o map ooo repair_problem_line thy
+fun repair_problem_line thy type_sys sym_tab (Fof (ident, kind, phi, source)) =
+  Fof (ident, kind, repair_formula thy type_sys sym_tab phi, source)
+fun repair_problem thy = map o apsnd o map oo repair_problem_line thy
 
 fun dest_Fof (Fof z) = z
 
@@ -682,8 +680,8 @@
     if heading = needle then j
     else offset_of_heading_in_problem needle problem (j + length lines)
 
-fun prepare_atp_problem ctxt readable_names explicit_forall type_sys
-                        explicit_apply hyp_ts concl_t facts =
+fun prepare_atp_problem ctxt readable_names type_sys explicit_apply hyp_ts
+                        concl_t facts =
   let
     val thy = Proof_Context.theory_of ctxt
     val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
@@ -699,13 +697,14 @@
        (conjsN, map (problem_line_for_conjecture ctxt type_sys) conjs),
        (free_typesN, problem_lines_for_free_types type_sys (facts @ conjs))]
     val sym_tab = sym_table_for_problem explicit_apply problem
-    val problem = problem |> repair_problem thy explicit_forall type_sys sym_tab
+    val problem = problem |> repair_problem thy type_sys sym_tab
+    val helper_facts =
+      get_helper_facts ctxt type_sys (maps (map (#3 o dest_Fof) o snd) problem)
     val helper_lines =
-      get_helper_facts ctxt explicit_forall type_sys
-                       (maps (map (#3 o dest_Fof) o snd) problem)
+      helper_facts
       |>> map (pair 0
                #> problem_line_for_fact ctxt helper_prefix type_sys
-               #> repair_problem_line thy explicit_forall type_sys sym_tab)
+               #> repair_problem_line thy type_sys sym_tab)
       |> op @
     val (problem, pool) =
       problem |> AList.update (op =) (helpersN, helper_lines)
diff -r d1f7c4a01dbe -r 02df3b78a438 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun May 01 18:37:23 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun May 01 18:37:23 2011 +0200
@@ -336,7 +336,7 @@
 
 fun run_atp auto name
         ({exec, required_execs, arguments, slices, proof_delims, known_failures,
-          explicit_forall, use_conjecture_for_hypotheses, ...} : atp_config)
+          use_conjecture_for_hypotheses, ...} : atp_config)
         ({debug, verbose, overlord, max_relevant, monomorphize,
           monomorphize_limit, type_sys, explicit_apply, isar_proof,
           isar_shrink_factor, slicing, timeout, ...} : params)
@@ -433,9 +433,8 @@
                   else
                     ()
                 val (atp_problem, pool, conjecture_offset, fact_names) =
-                  prepare_atp_problem ctxt readable_names explicit_forall
-                                      type_sys explicit_apply hyp_ts concl_t
-                                      facts
+                  prepare_atp_problem ctxt readable_names type_sys
+                                      explicit_apply hyp_ts concl_t facts
                 fun weights () = atp_problem_weights atp_problem
                 val core =
                   File.shell_path command ^ " " ^