added 'skolem' method, esp. for 'obtain's generated from Z3 proofs
--- a/src/HOL/Sledgehammer.thy Thu Aug 28 16:58:26 2014 +0200
+++ b/src/HOL/Sledgehammer.thy Thu Aug 28 16:58:27 2014 +0200
@@ -33,4 +33,8 @@
ML_file "Tools/Sledgehammer/sledgehammer.ML"
ML_file "Tools/Sledgehammer/sledgehammer_commands.ML"
+method_setup skolem = {*
+ Scan.succeed (SIMPLE_METHOD' o Sledgehammer_Proof_Methods.skolem_tac)
+*} "solve skolemization goals"
+
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Aug 28 16:58:26 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Aug 28 16:58:27 2014 +0200
@@ -137,7 +137,7 @@
basic_systematic_methods @ basic_arith_methods @ basic_simp_based_methods @
[Metis_Method (SOME full_typesN, NONE), Metis_Method (SOME no_typesN, NONE)]
val rewrite_methods = basic_simp_based_methods @ basic_systematic_methods @ basic_arith_methods
-val skolem_methods = basic_systematic_methods @ [Auto_Choice_Method]
+val skolem_methods = basic_systematic_methods @ [Skolem_Method]
fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
(one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Thu Aug 28 16:58:26 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Thu Aug 28 16:58:27 2014 +0200
@@ -18,8 +18,8 @@
Simp_Method |
Simp_Size_Method |
Auto_Method |
- Auto_Choice_Method |
Force_Method |
+ Skolem_Method |
Linarith_Method |
Presburger_Method |
Algebra_Method
@@ -32,7 +32,7 @@
type one_line_params =
((string * stature) list * (proof_method * play_outcome)) * string * int * int
- val skolemize_tac : Proof.context -> int -> tactic
+ val skolem_tac : Proof.context -> int -> tactic
val is_proof_method_direct : proof_method -> bool
val string_of_proof_method : Proof.context -> string list -> proof_method -> string
val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
@@ -49,6 +49,10 @@
open ATP_Problem_Generate
open ATP_Proof_Reconstruct
+fun skolem_tac ctxt =
+ TRY o Atomize_Elim.atomize_elim_tac ctxt THEN'
+ SELECT_GOAL (Clasimp.auto_tac (ctxt addSIs @{thms choice}) THEN ALLGOALS (blast_tac ctxt))
+
datatype proof_method =
Metis_Method of string option * string option |
Meson_Method |
@@ -58,8 +62,8 @@
Simp_Method |
Simp_Size_Method |
Auto_Method |
- Auto_Choice_Method |
Force_Method |
+ Skolem_Method |
Linarith_Method |
Presburger_Method |
Algebra_Method
@@ -95,8 +99,8 @@
| Simp_Method => if null ss then "simp" else "simp add:"
| Simp_Size_Method => "simp add: " ^ short_thm_name ctxt @{thm size_ne_size_imp_ne}
| Auto_Method => "auto"
- | Auto_Choice_Method => "atomize_elim, auto intro!: " ^ short_thm_name ctxt @{thm choice}
| Force_Method => "force"
+ | Skolem_Method => "skolem"
| Linarith_Method => "linarith"
| Presburger_Method => "presburger"
| Algebra_Method => "algebra")
@@ -129,17 +133,14 @@
SATx_Method => SAT.satx_tac ctxt
| Blast_Method => blast_tac ctxt
| Auto_Method => SELECT_GOAL (Clasimp.auto_tac (silence_methods ctxt))
- | Auto_Choice_Method =>
- Atomize_Elim.atomize_elim_tac ctxt THEN'
- SELECT_GOAL (Clasimp.auto_tac (silence_methods ctxt addSIs @{thms choice}))
- | Force_Method => SELECT_GOAL (Clasimp.auto_tac (silence_methods ctxt))
+ | Force_Method => Clasimp.force_tac (silence_methods ctxt)
+ | Skolemize_method => skolem_tac (silence_methods ctxt)
| Linarith_Method =>
let val ctxt = Config.put Lin_Arith.verbose false ctxt in Lin_Arith.tac ctxt end
| Presburger_Method => Cooper.tac true [] [] ctxt
| Algebra_Method => Groebner.algebra_tac [] [] ctxt))
-val simp_based_methods =
- [Simp_Method, Simp_Size_Method, Auto_Method, Auto_Choice_Method, Force_Method]
+val simp_based_methods = [Simp_Method, Simp_Size_Method, Auto_Method, Force_Method, Skolem_Method]
fun thms_influence_proof_method ctxt meth ths =
not (member (op =) simp_based_methods meth) orelse