--- a/src/HOL/ATP.thy Wed Jul 30 14:03:12 2014 +0200
+++ b/src/HOL/ATP.thy Wed Jul 30 14:03:12 2014 +0200
@@ -6,7 +6,7 @@
header {* Automatic Theorem Provers (ATPs) *}
theory ATP
-imports Meson
+imports Meson Hilbert_Choice
begin
subsection {* ATP problems and proofs *}
--- a/src/HOL/Tools/ATP/atp_problem.ML Wed Jul 30 14:03:12 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Wed Jul 30 14:03:12 2014 +0200
@@ -76,6 +76,8 @@
val tptp_ho_exists : string
val tptp_choice : string
val tptp_ho_choice : string
+ val tptp_hilbert_choice : string
+ val tptp_hilbert_the : string
val tptp_not : string
val tptp_and : string
val tptp_not_and : string
@@ -239,6 +241,8 @@
val tptp_iff = "<=>"
val tptp_not_iff = "<~>"
val tptp_app = "@"
+val tptp_hilbert_choice = "@+"
+val tptp_hilbert_the = "@-"
val tptp_not_infix = "!"
val tptp_equal = "="
val tptp_not_equal = "!="
--- a/src/HOL/Tools/ATP/atp_proof.ML Wed Jul 30 14:03:12 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Jul 30 14:03:12 2014 +0200
@@ -478,10 +478,19 @@
[tptp_and, tptp_not_and, tptp_or, tptp_not_or, tptp_implies, tptp_if, tptp_iff, tptp_not_iff,
tptp_equal, tptp_app]
+fun parse_one_in_list list =
+ foldl1 (op ||) (map Scan.this_string list)
+
fun parse_binary_op x =
- (foldl1 (op ||) (map Scan.this_string tptp_binary_ops)
+ (parse_one_in_list tptp_binary_ops
>> (fn c => if c = tptp_equal then "equal" else c)) x
+val parse_fo_quantifier =
+ parse_one_in_list [tptp_forall, tptp_exists, tptp_lambda, tptp_hilbert_choice, tptp_hilbert_the]
+
+val parse_ho_quantifier =
+ parse_one_in_list [tptp_ho_forall, tptp_ho_exists, tptp_hilbert_choice, tptp_hilbert_the]
+
fun parse_thf0_type x =
(($$ "(" |-- parse_thf0_type --| $$ ")" || scan_general_id >> (fn t => AType ((t, []), [])))
-- Scan.option ($$ tptp_fun_type |-- parse_thf0_type)
@@ -491,6 +500,8 @@
fun mk_ho_of_fo_quant q =
if q = tptp_forall then tptp_ho_forall
else if q = tptp_exists then tptp_ho_exists
+ else if q = tptp_hilbert_choice then tptp_hilbert_choice
+ else if q = tptp_hilbert_the then tptp_hilbert_the
else raise Fail ("unrecognized quantification: " ^ q)
fun remove_thf_app (ATerm ((x, ty), arg)) =
@@ -508,8 +519,7 @@
|| $$ "(" |-- parse_thf0_typed_var --| $$ ")") x
fun parse_simple_thf0_term x =
- ((Scan.this_string tptp_forall || Scan.this_string tptp_exists || Scan.this_string tptp_lambda)
- -- ($$ "[" |-- parse_thf0_typed_var --| $$ "]" --| $$ ":") -- parse_thf0_term
+ (parse_fo_quantifier -- ($$ "[" |-- parse_thf0_typed_var --| $$ "]" --| $$ ":") -- parse_thf0_term
>> (fn ((q, ys), t) =>
fold_rev
(fn (var, ty) => fn r =>
@@ -521,7 +531,7 @@
ys t)
|| Scan.this_string tptp_not |-- parse_thf0_term >> mk_app (mk_simple_aterm tptp_not)
|| scan_general_id --| $$ ":" -- parse_thf0_type >> (fn (var, typ) => ATerm ((var, [typ]), []))
- || (Scan.this_string tptp_ho_forall || Scan.this_string tptp_ho_exists) >> mk_simple_aterm
+ || parse_ho_quantifier >> mk_simple_aterm
|| $$ "(" |-- parse_thf0_term --| $$ ")"
|| scan_general_id >> mk_simple_aterm) x
and parse_thf0_term x =
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Jul 30 14:03:12 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Jul 30 14:03:12 2014 +0200
@@ -269,6 +269,8 @@
else if s = tptp_not then HOLogic.Not
else if s = tptp_ho_forall then HOLogic.all_const dummyT
else if s = tptp_ho_exists then HOLogic.exists_const dummyT
+ else if s = tptp_hilbert_choice then HOLogic.choice_const dummyT
+ else if s = tptp_hilbert_the then @{term "The"}
else
(case unprefix_and_unascii const_prefix s of
SOME s' =>
--- a/src/HOL/Tools/SMT2/smt2_systems.ML Wed Jul 30 14:03:12 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML Wed Jul 30 14:03:12 2014 +0200
@@ -103,8 +103,9 @@
"--disable-banner",
"--max-time=" ^ string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout))]),
smt_options = [],
- default_max_relevant = 250 (* FUDGE *),
- outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "warning : proof_done: status is still open"),
+ default_max_relevant = 120 (* FUDGE *),
+ outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat"
+ "warning : proof_done: status is still open"),
parse_proof = SOME VeriT_Proof_Parse.parse_proof,
replay = NONE }
--- a/src/HOL/Tools/SMT2/verit_proof.ML Wed Jul 30 14:03:12 2014 +0200
+++ b/src/HOL/Tools/SMT2/verit_proof.ML Wed Jul 30 14:03:12 2014 +0200
@@ -306,7 +306,7 @@
{fix sk ....}
hence "..sk.."
thus "(if ..)"
- last step does not work: the step before is buggy. Without the proof work.*)
+ last step does not work: the step before is buggy. Without it, the proof work.*)
mk_node id veriT_tmp_skolemize (if null prems then [mk_string_id (~num_of_steps - id)]
else prems) concl' []
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 30 14:03:12 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 30 14:03:12 2014 +0200
@@ -48,6 +48,7 @@
val e_skolemize_rule = "skolemize"
val leo2_extcnf_combined_rule = "extcnf_combined"
+val satallax_skolemize_rule = "tab_ex"
val spass_pirate_datatype_rule = "DT"
val vampire_skolemisation_rule = "skolemisation"
val veriT_tmp_skolemize_rule = "tmp_skolemize"
@@ -61,7 +62,8 @@
val skolemize_rules =
[e_skolemize_rule, spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule,
-zipperposition_cnf_rule, leo2_extcnf_combined_rule, veriT_tmp_skolemize_rule]
+zipperposition_cnf_rule, leo2_extcnf_combined_rule, veriT_tmp_skolemize_rule,
+satallax_skolemize_rule]
val is_skolemize_rule = member (op =) skolemize_rules
val is_arith_rule = (String.isPrefix z3_th_lemma_rule) orf (member (op =) veriT_arith_rules)