# HG changeset patch
# User blanchet
# Date 1336919461 -7200
# Node ID 12de57c5eee551138bc96f9c64108b9bc7b40c17
# Parent  2168126446bb543fa107b6633812f7cb2401ad72
get rid of "conj_sym_kind" -- most interesting provers now have built-in sorts, and for the others (e.g. E) "Hypothesis" isn't too bad a default

diff -r 2168126446bb -r 12de57c5eee5 src/HOL/TPTP/atp_theory_export.ML
--- a/src/HOL/TPTP/atp_theory_export.ML	Sun May 13 16:31:01 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Sun May 13 16:31:01 2012 +0200
@@ -183,8 +183,8 @@
       |> map (fn ((_, loc), th) =>
                  ((Thm.get_name_hint th, loc),
                    th |> prop_of |> mono ? monomorphize_term ctxt))
-      |> prepare_atp_problem ctxt format Axiom Axiom type_enc true combsN false
-                             false true [] @{prop False}
+      |> prepare_atp_problem ctxt format Axiom type_enc true combsN false false
+                             true [] @{prop False}
       |> #1
     val atp_problem =
       atp_problem
diff -r 2168126446bb -r 12de57c5eee5 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Sun May 13 16:31:01 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Sun May 13 16:31:01 2012 +0200
@@ -100,8 +100,8 @@
     Proof.context -> type_enc -> string -> term list -> term list * term list
   val factsN : string
   val prepare_atp_problem :
-    Proof.context -> atp_format -> formula_kind -> formula_kind -> type_enc
-    -> bool -> string -> bool -> bool -> bool -> term list -> term
+    Proof.context -> atp_format -> formula_kind -> type_enc -> bool -> string
+    -> bool -> bool -> bool -> term list -> term
     -> ((string * stature) * term) list
     -> string problem * string Symtab.table * (string * stature) list vector
        * (string * term) list * int Symtab.table
@@ -2284,15 +2284,14 @@
                ? curry ATyAbs (map (tvar_name o fst o dest_TVar) T_args))
   end
 
-fun honor_conj_sym_kind in_conj conj_sym_kind =
-  if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
-  else (Axiom, I)
+fun honor_conj_sym_kind in_conj =
+  if in_conj then (Hypothesis, I) else (Axiom, I)
 
-fun formula_line_for_guards_sym_decl ctxt conj_sym_kind mono type_enc n s j
+fun formula_line_for_guards_sym_decl ctxt mono type_enc n s j
                                      (s', T_args, T, _, ary, in_conj) =
   let
     val thy = Proof_Context.theory_of ctxt
-    val (kind, maybe_negate) = honor_conj_sym_kind in_conj conj_sym_kind
+    val (kind, maybe_negate) = honor_conj_sym_kind in_conj
     val (arg_Ts, res_T) = chop_fun ary T
     val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
     val bounds =
@@ -2326,7 +2325,7 @@
              NONE, isabelle_info inductiveN helper_rank)
   end
 
-fun formula_lines_for_tags_sym_decl ctxt conj_sym_kind mono type_enc n s
+fun formula_lines_for_tags_sym_decl ctxt mono type_enc n s
         (j, (s', T_args, T, pred_sym, ary, in_conj)) =
   let
     val thy = Proof_Context.theory_of ctxt
@@ -2335,7 +2334,7 @@
     val ident_base =
       tags_sym_formula_prefix ^ s ^
       (if n > 1 then "_" ^ string_of_int j else "")
-    val (kind, maybe_negate) = honor_conj_sym_kind in_conj conj_sym_kind
+    val (kind, maybe_negate) = honor_conj_sym_kind in_conj
     val (arg_Ts, res_T) = chop_fun ary T
     val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)
     val bounds = bound_names |> map (fn name => ATerm (name, []))
@@ -2377,7 +2376,7 @@
     end
   | rationalize_decls _ decls = decls
 
-fun problem_lines_for_sym_decls ctxt conj_sym_kind mono type_enc (s, decls) =
+fun problem_lines_for_sym_decls ctxt mono type_enc (s, decls) =
   case type_enc of
     Native _ => [decl_line_for_sym ctxt mono type_enc s (hd decls)]
   | Guards (_, level) =>
@@ -2390,8 +2389,7 @@
                          o result_type_of_decl)
     in
       (0 upto length decls - 1, decls)
-      |-> map2 (formula_line_for_guards_sym_decl ctxt conj_sym_kind mono
-                                                 type_enc n s)
+      |-> map2 (formula_line_for_guards_sym_decl ctxt mono type_enc n s)
     end
   | Tags (_, level) =>
     if granularity_of_type_level level = All_Vars then
@@ -2399,30 +2397,26 @@
     else
       let val n = length decls in
         (0 upto n - 1 ~~ decls)
-        |> maps (formula_lines_for_tags_sym_decl ctxt conj_sym_kind mono
-                                                 type_enc n s)
+        |> maps (formula_lines_for_tags_sym_decl ctxt mono type_enc n s)
       end
 
-fun problem_lines_for_sym_decl_table ctxt conj_sym_kind mono type_enc mono_Ts
-                                     sym_decl_tab =
+fun problem_lines_for_sym_decl_table ctxt mono type_enc mono_Ts sym_decl_tab =
   let
     val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst
     val mono_lines = problem_lines_for_mono_types ctxt mono type_enc mono_Ts
     val decl_lines =
-      fold_rev (append o problem_lines_for_sym_decls ctxt conj_sym_kind mono
-                             type_enc)
-               syms []
+      fold_rev (append o problem_lines_for_sym_decls ctxt mono type_enc) syms []
   in mono_lines @ decl_lines end
 
 fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
 
-fun do_uncurried_alias_lines_for_sym ctxt monom_constrs conj_sym_kind mono
-        type_enc sym_tab0 sym_tab base_s0 types in_conj =
+fun do_uncurried_alias_lines_for_sym ctxt monom_constrs mono type_enc sym_tab0
+                                     sym_tab base_s0 types in_conj =
   let
     fun do_alias ary =
       let
         val thy = Proof_Context.theory_of ctxt
-        val (kind, maybe_negate) = honor_conj_sym_kind in_conj conj_sym_kind
+        val (kind, maybe_negate) = honor_conj_sym_kind in_conj
         val base_name = base_s0 |> `(make_fixed_const (SOME type_enc))
         val T = case types of [T] => T | _ => robust_const_type thy base_s0
         val T_args = robust_const_typargs thy (base_s0, T)
@@ -2461,28 +2455,28 @@
             else pair_append (do_alias (ary - 1)))
       end
   in do_alias end
-fun uncurried_alias_lines_for_sym ctxt monom_constrs conj_sym_kind mono type_enc
-        sym_tab0 sym_tab (s, {min_ary, types, in_conj, ...} : sym_info) =
+fun uncurried_alias_lines_for_sym ctxt monom_constrs mono type_enc sym_tab0
+        sym_tab (s, {min_ary, types, in_conj, ...} : sym_info) =
   case unprefix_and_unascii const_prefix s of
     SOME mangled_s =>
     if String.isSubstring uncurried_alias_sep mangled_s then
       let
         val base_s0 = mangled_s |> unmangled_const_name |> hd |> invert_const
       in
-        do_uncurried_alias_lines_for_sym ctxt monom_constrs conj_sym_kind mono
-            type_enc sym_tab0 sym_tab base_s0 types in_conj min_ary
+        do_uncurried_alias_lines_for_sym ctxt monom_constrs mono type_enc
+            sym_tab0 sym_tab base_s0 types in_conj min_ary
       end
     else
       ([], [])
   | NONE => ([], [])
-fun uncurried_alias_lines_for_sym_table ctxt monom_constrs conj_sym_kind mono
-        type_enc uncurried_aliases sym_tab0 sym_tab =
+fun uncurried_alias_lines_for_sym_table ctxt monom_constrs mono type_enc
+                                        uncurried_aliases sym_tab0 sym_tab =
   ([], [])
   |> uncurried_aliases
      ? Symtab.fold_rev
            (pair_append
-            o uncurried_alias_lines_for_sym ctxt monom_constrs conj_sym_kind
-                  mono type_enc sym_tab0 sym_tab) sym_tab
+            o uncurried_alias_lines_for_sym ctxt monom_constrs mono type_enc
+                                            sym_tab0 sym_tab) sym_tab
 
 val implicit_declsN = "Should-be-implicit typings"
 val explicit_declsN = "Explicit typings"
@@ -2575,9 +2569,9 @@
 
 val app_op_and_predicator_threshold = 50
 
-fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
-                        lam_trans uncurried_aliases readable_names preproc
-                        hyp_ts concl_t facts =
+fun prepare_atp_problem ctxt format prem_kind type_enc exporter lam_trans
+                        uncurried_aliases readable_names preproc hyp_ts concl_t
+                        facts =
   let
     val thy = Proof_Context.theory_of ctxt
     val type_enc = type_enc |> adjust_type_enc format
@@ -2619,13 +2613,12 @@
       helpers @ conjs @ facts |> monotonic_types_for_facts ctxt mono type_enc
     val class_decl_lines = decl_lines_for_classes type_enc classes
     val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) =
-      uncurried_alias_lines_for_sym_table ctxt monom_constrs conj_sym_kind mono
-          type_enc uncurried_aliases sym_tab0 sym_tab
+      uncurried_alias_lines_for_sym_table ctxt monom_constrs mono type_enc
+                                          uncurried_aliases sym_tab0 sym_tab
     val sym_decl_lines =
       (conjs, helpers @ facts, uncurried_alias_eq_tms)
       |> sym_decl_table_for_facts thy type_enc sym_tab
-      |> problem_lines_for_sym_decl_table ctxt conj_sym_kind mono type_enc
-                                          mono_Ts
+      |> problem_lines_for_sym_decl_table ctxt mono type_enc mono_Ts
     val num_facts = length facts
     val fact_lines =
       map (formula_line_for_fact ctxt polym_constrs fact_prefix
diff -r 2168126446bb -r 12de57c5eee5 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Sun May 13 16:31:01 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Sun May 13 16:31:01 2012 +0200
@@ -22,7 +22,6 @@
           * (unit -> (string * real) list) -> string,
      proof_delims : (string * string) list,
      known_failures : (failure * string) list,
-     conj_sym_kind : formula_kind,
      prem_kind : formula_kind,
      best_slices :
        Proof.context -> (real * (bool * (slice_spec * string))) list}
@@ -59,7 +58,7 @@
   val remote_prefix : string
   val remote_atp :
     string -> string -> string list -> (string * string) list
-    -> (failure * string) list -> formula_kind -> formula_kind
+    -> (failure * string) list -> formula_kind
     -> (Proof.context -> slice_spec * string) -> string * (unit -> atp_config)
   val add_atp : string * (unit -> atp_config) -> theory -> theory
   val get_atp : theory -> string -> (unit -> atp_config)
@@ -90,7 +89,6 @@
         * (unit -> (string * real) list) -> string,
    proof_delims : (string * string) list,
    known_failures : (failure * string) list,
-   conj_sym_kind : formula_kind,
    prem_kind : formula_kind,
    best_slices : Proof.context -> (real * (bool * (slice_spec * string))) list}
 
@@ -196,7 +194,6 @@
      [(ProofMissing, ": Valid"),
       (TimedOut, ": Timeout"),
       (GaveUp, ": Unknown")],
-   conj_sym_kind = Hypothesis,
    prem_kind = Hypothesis,
    best_slices = fn _ =>
      (* FUDGE *)
@@ -304,7 +301,6 @@
      known_szs_status_failures @
      [(TimedOut, "Failure: Resource limit exceeded (time)"),
       (TimedOut, "time limit exceeded")],
-   conj_sym_kind = Hypothesis,
    prem_kind = Conjecture,
    best_slices = fn ctxt =>
      let val heuristic = effective_e_selection_heuristic ctxt in
@@ -336,7 +332,6 @@
      known_szs_status_failures @
      [(TimedOut, "CPU time limit exceeded, terminating"),
       (GaveUp, "No.of.Axioms")],
-   conj_sym_kind = Axiom,
    prem_kind = Hypothesis,
    best_slices = fn ctxt =>
      (* FUDGE *)
@@ -361,7 +356,6 @@
    proof_delims =
      [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")],
    known_failures = known_szs_status_failures,
-   conj_sym_kind = Axiom,
    prem_kind = Definition (* motivated by "isabelle tptp_sledgehammer" tool *),
    best_slices =
      (* FUDGE *)
@@ -395,7 +389,6 @@
       (MalformedInput, "Free Variable"),
       (Unprovable, "No formulae and clauses found in input file"),
       (InternalError, "Please report this error")],
-   conj_sym_kind = Hypothesis,
    prem_kind = Conjecture,
    best_slices = fn ctxt =>
      (* FUDGE *)
@@ -421,7 +414,6 @@
      |> extra_options <> "" ? prefix (extra_options ^ " "),
    proof_delims = #proof_delims spass_old_config,
    known_failures = #known_failures spass_old_config,
-   conj_sym_kind = #conj_sym_kind spass_old_config,
    prem_kind = #prem_kind spass_old_config,
    best_slices = fn _ =>
      (* FUDGE *)
@@ -470,7 +462,6 @@
       (Unprovable, "Satisfiability detected"),
       (Unprovable, "Termination reason: Satisfiable"),
       (Interrupted, "Aborted by signal SIGINT")],
-   conj_sym_kind = Conjecture,
    prem_kind = Conjecture,
    best_slices = fn ctxt =>
      (* FUDGE *)
@@ -499,7 +490,6 @@
      "MBQI=true -tptp -t:" ^ string_of_int (to_secs 1 timeout),
    proof_delims = [],
    known_failures = known_szs_status_failures,
-   conj_sym_kind = Hypothesis,
    prem_kind = Hypothesis,
    best_slices =
      (* FUDGE *)
@@ -519,7 +509,6 @@
    arguments = K (K (K (K (K "")))),
    proof_delims = [],
    known_failures = known_szs_status_failures,
-   conj_sym_kind = Hypothesis,
    prem_kind = Hypothesis,
    best_slices =
      K [(1.0, (false, ((200, format, type_enc,
@@ -572,7 +561,7 @@
 val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
 
 fun remote_config system_name system_versions proof_delims known_failures
-                  conj_sym_kind prem_kind best_slice : atp_config =
+                  prem_kind best_slice : atp_config =
   {exec = (["ISABELLE_ATP"], "scripts/remote_atp"),
    required_vars = [],
    arguments = fn _ => fn _ => fn command => fn timeout => fn _ =>
@@ -581,21 +570,20 @@
      "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)),
    proof_delims = union (op =) tstp_proof_delims proof_delims,
    known_failures = known_failures @ known_perl_failures @ known_says_failures,
-   conj_sym_kind = conj_sym_kind,
    prem_kind = prem_kind,
    best_slices = fn ctxt => [(1.0, (false, best_slice ctxt))]}
 
 fun remotify_config system_name system_versions best_slice
-        ({proof_delims, known_failures, conj_sym_kind, prem_kind, ...}
-         : atp_config) : atp_config =
+        ({proof_delims, known_failures, prem_kind, ...} : atp_config)
+        : atp_config =
   remote_config system_name system_versions proof_delims known_failures
-                conj_sym_kind prem_kind best_slice
+                prem_kind best_slice
 
 fun remote_atp name system_name system_versions proof_delims known_failures
-               conj_sym_kind prem_kind best_slice =
+               prem_kind best_slice =
   (remote_prefix ^ name,
-   fn () => remote_config system_name system_versions proof_delims known_failures
-                          conj_sym_kind prem_kind best_slice)
+   fn () => remote_config system_name system_versions proof_delims
+                          known_failures prem_kind best_slice)
 fun remotify_atp (name, config) system_name system_versions best_slice =
   (remote_prefix ^ name,
    remotify_config system_name system_versions best_slice o config)
@@ -618,21 +606,20 @@
   remotify_atp z3_tptp "Z3" ["3.0"]
       (K ((250, z3_tff0, "mono_native", combsN, false), "") (* FUDGE *))
 val remote_e_sine =
-  remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom Conjecture
+  remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Conjecture
       (K ((500, FOF, "mono_guards??", combsN, false), "") (* FUDGE *))
 val remote_iprover =
-  remote_atp iproverN "iProver" [] [] [] Axiom Conjecture
+  remote_atp iproverN "iProver" [] [] [] Conjecture
       (K ((150, FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
 val remote_iprover_eq =
-  remote_atp iprover_eqN "iProver-Eq" [] [] [] Axiom Conjecture
+  remote_atp iprover_eqN "iProver-Eq" [] [] [] Conjecture
       (K ((150, FOF, "mono_guards??", liftingN, false), "") (* FUDGE *))
 val remote_snark =
   remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
-      [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
+      [("refutation.", "end_refutation.")] [] Hypothesis
       (K ((100, explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *))
 val remote_e_tofof =
-  remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
-      Hypothesis
+  remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Hypothesis
       (K ((150, explicit_tff0, "mono_native", liftingN, false), "") (* FUDGE *))
 val remote_waldmeister =
   remote_atp waldmeisterN "Waldmeister" ["710"]
@@ -640,7 +627,7 @@
       [(OutOfResources, "Too many function symbols"),
        (Inappropriate, "****  Unexpected end of file."),
        (Crashed, "Unrecoverable Segmentation Fault")]
-      Hypothesis Hypothesis
+      Hypothesis
       (K ((50, CNF_UEQ, "raw_mono_tags??", combsN, false), "") (* FUDGE *))
 
 (* Setup *)
diff -r 2168126446bb -r 12de57c5eee5 src/HOL/Tools/Metis/metis_generate.ML
--- a/src/HOL/Tools/Metis/metis_generate.ML	Sun May 13 16:31:01 2012 +0200
+++ b/src/HOL/Tools/Metis/metis_generate.ML	Sun May 13 16:31:01 2012 +0200
@@ -242,8 +242,8 @@
     *)
     val lam_trans = if lam_trans = combsN then no_lamsN else lam_trans
     val (atp_problem, _, _, lifted, sym_tab) =
-      prepare_atp_problem ctxt CNF Hypothesis Hypothesis type_enc false
-                          lam_trans false false false [] @{prop False} props
+      prepare_atp_problem ctxt CNF Hypothesis type_enc false lam_trans false
+                          false false [] @{prop False} props
     (*
     val _ = tracing ("ATP PROBLEM: " ^
                      cat_lines (lines_for_atp_problem CNF atp_problem))
diff -r 2168126446bb -r 12de57c5eee5 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun May 13 16:31:01 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun May 13 16:31:01 2012 +0200
@@ -579,7 +579,7 @@
 
 fun run_atp mode name
         ({exec, required_vars, arguments, proof_delims, known_failures,
-          conj_sym_kind, prem_kind, best_slices, ...} : atp_config)
+          prem_kind, best_slices, ...} : atp_config)
         (params as {debug, verbose, overlord, type_enc, strict, lam_trans,
                     uncurried_aliases, max_relevant, max_mono_iters,
                     max_new_mono_instances, isar_proof, isar_shrink_factor,
@@ -710,9 +710,9 @@
                     |> polymorphism_of_type_enc type_enc <> Polymorphic
                        ? monomorphize_facts
                     |> map (apsnd prop_of)
-                    |> prepare_atp_problem ctxt format conj_sym_kind prem_kind
-                           type_enc false lam_trans uncurried_aliases
-                           readable_names true hyp_ts concl_t
+                    |> prepare_atp_problem ctxt format prem_kind type_enc false
+                           lam_trans uncurried_aliases readable_names true
+                           hyp_ts concl_t
                 fun sel_weights () = atp_problem_selection_weights atp_problem
                 fun ord_info () = atp_problem_term_order_info atp_problem
                 val ord = effective_term_order ctxt name