merged

--- a/src/HOL/Tools/ATP/atp_problem.ML	Wed Jun 08 22:06:05 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed Jun 08 22:13:49 2011 +0200
@@ -351,9 +351,8 @@
       val (n, phis) = phi |> try (clausify_formula true) |> these |> `length
     in
       map2 (fn phi => fn j =>
-               Formula (ident ^
-                        (if n > 1 then "_cls" ^ string_of_int j else ""),
-                        kind, phi, source, info))
+               Formula (ident ^ replicate_string (j - 1) "x", kind, phi, source,
+                        info))
            phis (1 upto n)
     end
   | clausify_formula_line _ = []

--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Wed Jun 08 22:06:05 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Wed Jun 08 22:13:49 2011 +0200
@@ -225,25 +225,26 @@
   | add_fact _ _ _ _ _ = I
 
 fun used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof =
-  if null atp_proof then Vector.foldl (op @) [] fact_names
+  if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names
   else fold (add_fact ctxt type_sys facts_offset fact_names) atp_proof []
 
-fun is_conjecture_referred_to_in_proof conjecture_shape =
+fun is_conjecture_used_in_proof conjecture_shape =
   exists (fn Inference (name, _, []) => is_conjecture conjecture_shape name
            | _ => false)
 
-fun used_facts_in_unsound_atp_proof ctxt type_sys conjecture_shape facts_offset
+fun used_facts_in_unsound_atp_proof _ _ _ _ _ [] = NONE
+  | used_facts_in_unsound_atp_proof ctxt type_sys conjecture_shape facts_offset
                                     fact_names atp_proof =
-  let
-    val used_facts =
-      used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof
-  in
-    if forall (is_locality_global o snd) used_facts andalso
-       not (is_conjecture_referred_to_in_proof conjecture_shape atp_proof) then
-      SOME (map fst used_facts)
-    else
-      NONE
-  end
+    let
+      val used_facts =
+        used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof
+    in
+      if forall (is_locality_global o snd) used_facts andalso
+         not (is_conjecture_used_in_proof conjecture_shape atp_proof) then
+        SOME (map fst used_facts)
+      else
+        NONE
+    end
 
 fun uses_typed_helpers typed_helpers =
   exists (fn Inference (name, _, []) => is_typed_helper typed_helpers name

--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Jun 08 22:06:05 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Jun 08 22:13:49 2011 +0200
@@ -432,7 +432,7 @@
              [(OutOfResources, "Too many function symbols"),
               (Crashed, "Unrecoverable Segmentation Fault")]
              Hypothesis Hypothesis [CNF_UEQ]
-             (K (50, ["poly_args"]) (* FUDGE *))
+             (K (50, ["mangled_args", "mangled_tags?"]) (* FUDGE *))
 
 (* Setup *)
 

--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 08 22:06:05 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 08 22:13:49 2011 +0200
@@ -625,7 +625,7 @@
        CNF_UEQ =>
        (CNF_UEQ, case type_sys of
                    Preds stuff =>
-                   (if is_type_sys_fairly_sound type_sys then Preds else Tags)
+                   (if is_type_sys_fairly_sound type_sys then Tags else Preds)
                        stuff
                  | _ => type_sys)
      | format => (format, type_sys))
@@ -975,16 +975,15 @@
      atomic_types = atomic_types}
   end
 
-fun make_fact ctxt format type_sys keep_trivial eq_as_iff preproc presimp_consts
+fun make_fact ctxt format type_sys eq_as_iff preproc presimp_consts
               ((name, loc), t) =
   let val thy = Proof_Context.theory_of ctxt in
-    case (keep_trivial,
-          t |> preproc ? preprocess_prop ctxt presimp_consts Axiom
-            |> make_formula thy format type_sys eq_as_iff name loc Axiom) of
-      (false,
-       formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...}) =>
+    case t |> preproc ? preprocess_prop ctxt presimp_consts Axiom
+           |> make_formula thy format type_sys (eq_as_iff andalso format <> CNF)
+                           name loc Axiom of
+      formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} =>
       if s = tptp_true then NONE else SOME formula
-    | (_, formula) => SOME formula
+    | formula => SOME formula
   end
 
 fun make_conjecture ctxt format prem_kind type_sys preproc presimp_consts ts =
@@ -1005,7 +1004,7 @@
                 t |> preproc ?
                      (preprocess_prop ctxt presimp_consts kind #> freeze_term)
                   |> make_formula thy format type_sys (format <> CNF)
-                                  (string_of_int j) General kind
+                                  (string_of_int j) Local kind
                   |> maybe_negate
               end)
          (0 upto last) ts
@@ -1354,7 +1353,7 @@
                    | _ => I)
          end)
       val make_facts =
-        map_filter (make_fact ctxt format type_sys false false false [])
+        map_filter (make_fact ctxt format type_sys false false [])
       val fairly_sound = is_type_sys_fairly_sound type_sys
     in
       helper_table
@@ -1417,8 +1416,7 @@
     val thy = Proof_Context.theory_of ctxt
     val fact_ts = facts |> map snd
     val presimp_consts = Meson.presimplified_consts ctxt
-    val make_fact =
-      make_fact ctxt format type_sys false true true presimp_consts
+    val make_fact = make_fact ctxt format type_sys true preproc presimp_consts
     val (facts, fact_names) =
       facts |> map (fn (name, t) => (name, t) |> make_fact |> rpair name)
             |> map_filter (try (apfst the))
@@ -1648,21 +1646,22 @@
 
 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
    out with monotonicity" paper presented at CADE 2011. *)
-fun add_combterm_nonmonotonic_types _ _ (SOME false) _ = I
-  | add_combterm_nonmonotonic_types ctxt level _
+fun add_combterm_nonmonotonic_types _ _ _ (SOME false) _ = I
+  | add_combterm_nonmonotonic_types ctxt level locality _
         (CombApp (CombApp (CombConst ((s, _), Type (_, [T, _]), _), tm1),
                            tm2)) =
     (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
      (case level of
         Nonmonotonic_Types =>
+        not (is_locality_global locality) orelse
         not (is_type_surely_infinite ctxt known_infinite_types T)
       | Finite_Types => is_type_surely_finite ctxt T
       | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
-  | add_combterm_nonmonotonic_types _ _ _ _ = I
-fun add_fact_nonmonotonic_types ctxt level ({kind, combformula, ...}
+  | add_combterm_nonmonotonic_types _ _ _ _ _ = I
+fun add_fact_nonmonotonic_types ctxt level ({kind, locality, combformula, ...}
                                             : translated_formula) =
   formula_fold (SOME (kind <> Conjecture))
-               (add_combterm_nonmonotonic_types ctxt level) combformula
+               (add_combterm_nonmonotonic_types ctxt level locality) combformula
 fun nonmonotonic_types_for_facts ctxt type_sys facts =
   let val level = level_of_type_sys type_sys in
     if level = Nonmonotonic_Types orelse level = Finite_Types then

--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Jun 08 22:06:05 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Jun 08 22:13:49 2011 +0200
@@ -230,7 +230,8 @@
 (* Match untyped terms. *)
 fun untyped_aconv (Const (a, _), Const(b, _)) = (a = b)
   | untyped_aconv (Free (a, _), Free (b, _)) = (a = b)
-  | untyped_aconv (Var ((a, _), _), Var ((b, _), _)) = (a = b)
+  | untyped_aconv (Var ((a, _), _), Var ((b, _), _)) =
+    (a = b) (* ignore variable numbers *)
   | untyped_aconv (Bound i, Bound j) = (i = j)
   | untyped_aconv (Abs (_, _, t), Abs (_, _, u)) = untyped_aconv (t, u)
   | untyped_aconv (t1 $ t2, u1 $ u2) =

--- a/src/HOL/Tools/Metis/metis_translate.ML	Wed Jun 08 22:06:05 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Wed Jun 08 22:13:49 2011 +0200
@@ -145,6 +145,8 @@
       if ident = type_tag_idempotence_helper_name orelse
          String.isPrefix lightweight_tags_sym_formula_prefix ident then
         Isa_Reflexive_or_Trivial |> some
+      else if String.isPrefix conjecture_prefix ident then
+        NONE
       else if String.isPrefix helper_prefix ident then
         case (String.isSuffix typed_helper_suffix ident,
               space_explode "_" ident) of
@@ -155,12 +157,11 @@
           |> prepare_helper
           |> Isa_Raw |> some
         | _ => raise Fail ("malformed helper identifier " ^ quote ident)
-      else case try (unprefix conjecture_prefix) ident of
+      else case try (unprefix fact_prefix) ident of
         SOME s =>
-        let val j = the (Int.fromString s) in
-          if j = length clauses then NONE
-          else Meson.make_meta_clause (nth clauses j) |> Isa_Raw |> some
-        end
+        let
+          val j = s |> space_explode "_" |> List.last |> Int.fromString |> the
+        in Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some end
       | NONE => TrueI |> Isa_Raw |> some
     end
   | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
@@ -169,31 +170,40 @@
 fun prepare_metis_problem ctxt type_sys conj_clauses fact_clauses =
   let
     val type_sys = type_sys_from_string type_sys
+    val (conj_clauses, fact_clauses) =
+      if polymorphism_of_type_sys type_sys = Polymorphic then
+        (conj_clauses, fact_clauses)
+      else
+        conj_clauses @ fact_clauses
+        |> map (pair 0)
+        |> rpair ctxt
+        |-> Monomorph.monomorph atp_schematic_consts_of
+        |> fst |> chop (length conj_clauses)
+        |> pairself (maps (map (zero_var_indexes o snd)))
+    val num_conjs = length conj_clauses
     val clauses =
-      conj_clauses @ fact_clauses
-      |> (if polymorphism_of_type_sys type_sys = Polymorphic then
-            I
-          else
-            map (pair 0)
-            #> rpair ctxt
-            #-> Monomorph.monomorph atp_schematic_consts_of
-            #> fst #> maps (map (zero_var_indexes o snd)))
+      map2 (fn j => pair (Int.toString j, Local))
+           (0 upto num_conjs - 1) conj_clauses @
+      (* "General" below isn't quite correct; the fact could be local. *)
+      map2 (fn j => pair (Int.toString (num_conjs + j), General))
+           (0 upto length fact_clauses - 1) fact_clauses
     val (old_skolems, props) =
-      fold_rev (fn clause => fn (old_skolems, props) =>
-                   clause |> prop_of |> Logic.strip_imp_concl
-                          |> conceal_old_skolem_terms (length clauses)
-                                                      old_skolems
-                          ||> (fn prop => prop :: props))
-           clauses ([], [])
-(*
-val _ = tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
-*)
+      fold_rev (fn (name, th) => fn (old_skolems, props) =>
+                   th |> prop_of |> Logic.strip_imp_concl
+                      |> conceal_old_skolem_terms (length clauses) old_skolems
+                      ||> (fn prop => (name, prop) :: props))
+               clauses ([], [])
+    (*
+    val _ =
+      tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
+    *)
     val (atp_problem, _, _, _, _, _, sym_tab) =
-      prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys false false props
-                          @{prop False} []
-(*
-val _ = tracing ("ATP PROBLEM: " ^ cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
-*)
+      prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys false false []
+                          @{prop False} props
+    (*
+    val _ = tracing ("ATP PROBLEM: " ^
+                     cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
+    *)
     (* "rev" is for compatibility *)
     val axioms =
       atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jun 08 22:06:05 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jun 08 22:13:49 2011 +0200
@@ -19,7 +19,7 @@
   val timeoutN : string
   val unknownN : string
   val auto_minimize_min_facts : int Config.T
-  val auto_minimize_max_seconds : real Config.T
+  val auto_minimize_max_time : real Config.T
   val get_minimizing_prover : Proof.context -> mode -> string -> prover
   val run_sledgehammer :
     params -> mode -> int -> relevance_override -> (string -> minimize_command)
@@ -69,15 +69,15 @@
 val auto_minimize_min_facts =
   Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
       (fn generic => Config.get_generic generic binary_min_facts)
-val auto_minimize_max_seconds =
-  Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_seconds}
+val auto_minimize_max_time =
+  Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time}
       (K 5.0)
 
 fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...})
              ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
              (result as {outcome, used_facts, run_time_in_msecs, preplay,
                          message, message_tail} : prover_result) =
-  if is_some outcome then
+  if is_some outcome orelse null used_facts then
     result
   else
     let
@@ -90,7 +90,7 @@
             let
               fun can_min_fast_enough msecs =
                 0.001 * Real.fromInt ((num_facts + 2) * msecs)
-                <= Config.get ctxt auto_minimize_max_seconds
+                <= Config.get ctxt auto_minimize_max_time
               val prover_fast_enough =
                 run_time_in_msecs |> Option.map can_min_fast_enough
                                   |> the_default false