imported patch hilbert_choice_support
authorfleury
Wed Jul 30 14:03:12 2014 +0200 (2014-07-30)
changeset 577099cda0c64c37a
parent 57708 4b52c1b319ce
child 57710 323a57d7455c
imported patch hilbert_choice_support
src/HOL/ATP.thy
src/HOL/Tools/ATP/atp_problem.ML
src/HOL/Tools/ATP/atp_proof.ML
src/HOL/Tools/ATP/atp_proof_reconstruct.ML
src/HOL/Tools/SMT2/smt2_systems.ML
src/HOL/Tools/SMT2/verit_proof.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
     1.1 --- a/src/HOL/ATP.thy	Wed Jul 30 14:03:12 2014 +0200
     1.2 +++ b/src/HOL/ATP.thy	Wed Jul 30 14:03:12 2014 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Automatic Theorem Provers (ATPs) *}
     1.5  
     1.6  theory ATP
     1.7 -imports Meson
     1.8 +imports Meson Hilbert_Choice
     1.9  begin
    1.10  
    1.11  subsection {* ATP problems and proofs *}
     2.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Wed Jul 30 14:03:12 2014 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed Jul 30 14:03:12 2014 +0200
     2.3 @@ -76,6 +76,8 @@
     2.4    val tptp_ho_exists : string
     2.5    val tptp_choice : string
     2.6    val tptp_ho_choice : string
     2.7 +  val tptp_hilbert_choice : string
     2.8 +  val tptp_hilbert_the : string
     2.9    val tptp_not : string
    2.10    val tptp_and : string
    2.11    val tptp_not_and : string
    2.12 @@ -239,6 +241,8 @@
    2.13  val tptp_iff = "<=>"
    2.14  val tptp_not_iff = "<~>"
    2.15  val tptp_app = "@"
    2.16 +val tptp_hilbert_choice = "@+"
    2.17 +val tptp_hilbert_the = "@-"
    2.18  val tptp_not_infix = "!"
    2.19  val tptp_equal = "="
    2.20  val tptp_not_equal = "!="
     3.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Jul 30 14:03:12 2014 +0200
     3.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Jul 30 14:03:12 2014 +0200
     3.3 @@ -478,10 +478,19 @@
     3.4    [tptp_and, tptp_not_and, tptp_or, tptp_not_or, tptp_implies, tptp_if, tptp_iff, tptp_not_iff,
     3.5     tptp_equal, tptp_app]
     3.6  
     3.7 +fun parse_one_in_list list =
     3.8 +  foldl1 (op ||) (map Scan.this_string list)
     3.9 +
    3.10  fun parse_binary_op x =
    3.11 -  (foldl1 (op ||) (map Scan.this_string tptp_binary_ops)
    3.12 +  (parse_one_in_list tptp_binary_ops
    3.13     >> (fn c => if c = tptp_equal then "equal" else c)) x
    3.14  
    3.15 +val parse_fo_quantifier =
    3.16 +   parse_one_in_list [tptp_forall, tptp_exists, tptp_lambda, tptp_hilbert_choice, tptp_hilbert_the]
    3.17 +
    3.18 +val parse_ho_quantifier =
    3.19 +   parse_one_in_list [tptp_ho_forall, tptp_ho_exists, tptp_hilbert_choice, tptp_hilbert_the]
    3.20 +
    3.21  fun parse_thf0_type x =
    3.22    (($$ "(" |-- parse_thf0_type --| $$ ")" || scan_general_id >> (fn t => AType ((t, []), [])))
    3.23     -- Scan.option ($$ tptp_fun_type |-- parse_thf0_type)
    3.24 @@ -491,6 +500,8 @@
    3.25  fun mk_ho_of_fo_quant q =
    3.26    if q = tptp_forall then tptp_ho_forall
    3.27    else if q = tptp_exists then tptp_ho_exists
    3.28 +  else if q = tptp_hilbert_choice then tptp_hilbert_choice
    3.29 +  else if q = tptp_hilbert_the then tptp_hilbert_the
    3.30    else raise Fail ("unrecognized quantification: " ^ q)
    3.31  
    3.32  fun remove_thf_app (ATerm ((x, ty), arg)) =
    3.33 @@ -508,8 +519,7 @@
    3.34     || $$ "(" |-- parse_thf0_typed_var --| $$ ")") x
    3.35  
    3.36  fun parse_simple_thf0_term x =
    3.37 -  ((Scan.this_string tptp_forall || Scan.this_string tptp_exists || Scan.this_string tptp_lambda)
    3.38 -        -- ($$ "[" |-- parse_thf0_typed_var --| $$ "]" --| $$ ":") -- parse_thf0_term
    3.39 +  (parse_fo_quantifier -- ($$ "[" |-- parse_thf0_typed_var --| $$ "]" --| $$ ":") -- parse_thf0_term
    3.40        >> (fn ((q, ys), t) =>
    3.41            fold_rev
    3.42              (fn (var, ty) => fn r =>
    3.43 @@ -521,7 +531,7 @@
    3.44              ys t)
    3.45    || Scan.this_string tptp_not |-- parse_thf0_term >> mk_app (mk_simple_aterm tptp_not)
    3.46    || scan_general_id --| $$ ":" -- parse_thf0_type >> (fn (var, typ) => ATerm ((var, [typ]), []))
    3.47 -  || (Scan.this_string tptp_ho_forall || Scan.this_string tptp_ho_exists) >> mk_simple_aterm
    3.48 +  || parse_ho_quantifier >> mk_simple_aterm
    3.49    || $$ "(" |-- parse_thf0_term --| $$ ")"
    3.50    || scan_general_id >> mk_simple_aterm) x
    3.51  and parse_thf0_term x =
     4.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Jul 30 14:03:12 2014 +0200
     4.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Jul 30 14:03:12 2014 +0200
     4.3 @@ -269,6 +269,8 @@
     4.4          else if s = tptp_not then HOLogic.Not
     4.5          else if s = tptp_ho_forall then HOLogic.all_const dummyT
     4.6          else if s = tptp_ho_exists then HOLogic.exists_const dummyT
     4.7 +        else if s = tptp_hilbert_choice then HOLogic.choice_const dummyT
     4.8 +        else if s = tptp_hilbert_the then @{term "The"}
     4.9          else
    4.10            (case unprefix_and_unascii const_prefix s of
    4.11              SOME s' =>
     5.1 --- a/src/HOL/Tools/SMT2/smt2_systems.ML	Wed Jul 30 14:03:12 2014 +0200
     5.2 +++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Wed Jul 30 14:03:12 2014 +0200
     5.3 @@ -103,8 +103,9 @@
     5.4      "--disable-banner",
     5.5      "--max-time=" ^ string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout))]),
     5.6    smt_options = [],
     5.7 -  default_max_relevant = 250 (* FUDGE *),
     5.8 -  outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "warning : proof_done: status is still open"),
     5.9 +  default_max_relevant = 120 (* FUDGE *),
    5.10 +  outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat"
    5.11 +              "warning : proof_done: status is still open"),
    5.12    parse_proof = SOME VeriT_Proof_Parse.parse_proof,
    5.13    replay = NONE }
    5.14  
     6.1 --- a/src/HOL/Tools/SMT2/verit_proof.ML	Wed Jul 30 14:03:12 2014 +0200
     6.2 +++ b/src/HOL/Tools/SMT2/verit_proof.ML	Wed Jul 30 14:03:12 2014 +0200
     6.3 @@ -306,7 +306,7 @@
     6.4           {fix sk ....}
     6.5           hence "..sk.."
     6.6           thus "(if ..)"
     6.7 -      last step does not work: the step before is buggy. Without the proof work.*)
     6.8 +      last step does not work: the step before is buggy. Without it, the proof work.*)
     6.9          mk_node id veriT_tmp_skolemize (if null prems then [mk_string_id (~num_of_steps - id)]
    6.10            else prems) concl' []
    6.11        end
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 30 14:03:12 2014 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 30 14:03:12 2014 +0200
     7.3 @@ -48,6 +48,7 @@
     7.4  
     7.5  val e_skolemize_rule = "skolemize"
     7.6  val leo2_extcnf_combined_rule = "extcnf_combined"
     7.7 +val satallax_skolemize_rule = "tab_ex"
     7.8  val spass_pirate_datatype_rule = "DT"
     7.9  val vampire_skolemisation_rule = "skolemisation"
    7.10  val veriT_tmp_skolemize_rule = "tmp_skolemize"
    7.11 @@ -61,7 +62,8 @@
    7.12  
    7.13  val skolemize_rules =
    7.14    [e_skolemize_rule, spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule,
    7.15 -zipperposition_cnf_rule, leo2_extcnf_combined_rule, veriT_tmp_skolemize_rule]
    7.16 +zipperposition_cnf_rule, leo2_extcnf_combined_rule, veriT_tmp_skolemize_rule,
    7.17 +satallax_skolemize_rule]
    7.18  
    7.19  val is_skolemize_rule = member (op =) skolemize_rules
    7.20  val is_arith_rule = (String.isPrefix z3_th_lemma_rule) orf (member (op =) veriT_arith_rules)