--- a/src/HOL/IsaMakefile Fri Apr 27 14:07:31 2012 +0200
+++ b/src/HOL/IsaMakefile Fri Apr 27 15:24:37 2012 +0200
@@ -1034,7 +1034,7 @@
ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy \
ex/SAT_Examples.thy ex/Serbian.thy ex/Set_Theory.thy \
ex/Simproc_Tests.thy ex/SVC_Oracle.thy \
- ex/sledgehammer_tactics.ML ex/Seq.thy ex/Sqrt.thy ex/Sqrt_Script.thy \
+ ex/Seq.thy ex/Sqrt.thy ex/Sqrt_Script.thy \
ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy \
ex/Transfer_Int_Nat.thy \
ex/Tree23.thy ex/Unification.thy ex/While_Combinator_Example.thy \
@@ -1153,7 +1153,8 @@
TPTP/TPTP_Parser/tptp_syntax.ML \
TPTP/TPTP_Parser_Test.thy \
TPTP/atp_problem_import.ML \
- TPTP/atp_theory_export.ML
+ TPTP/atp_theory_export.ML \
+ TPTP/sledgehammer_tactics.ML
@$(ISABELLE_TOOL) usedir $(OUT)/HOL TPTP
@@ -1333,7 +1334,7 @@
Mirabelle/Tools/mirabelle_refute.ML \
Mirabelle/Tools/mirabelle_sledgehammer.ML \
Mirabelle/Tools/mirabelle_sledgehammer_filter.ML \
- ex/sledgehammer_tactics.ML Mirabelle/lib/Tools/mirabelle \
+ TPTP/sledgehammer_tactics.ML Mirabelle/lib/Tools/mirabelle \
Mirabelle/lib/scripts/mirabelle.pl Library/FrechetDeriv.thy \
Library/Inner_Product.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle
--- a/src/HOL/Mirabelle/Mirabelle.thy Fri Apr 27 14:07:31 2012 +0200
+++ b/src/HOL/Mirabelle/Mirabelle.thy Fri Apr 27 15:24:37 2012 +0200
@@ -5,7 +5,7 @@
theory Mirabelle
imports Sledgehammer
uses "Tools/mirabelle.ML"
- "../ex/sledgehammer_tactics.ML"
+ "../TPTP/sledgehammer_tactics.ML"
begin
(* no multithreading, no parallel proofs *) (* FIXME *)
--- a/src/HOL/TPTP/ATP_Problem_Import.thy Fri Apr 27 14:07:31 2012 +0200
+++ b/src/HOL/TPTP/ATP_Problem_Import.thy Fri Apr 27 15:24:37 2012 +0200
@@ -3,10 +3,9 @@
*)
header {* ATP Problem Importer *}
-
theory ATP_Problem_Import
imports Complex_Main TPTP_Interpret
-uses "~~/src/HOL/ex/sledgehammer_tactics.ML"
+uses "sledgehammer_tactics.ML"
"atp_problem_import.ML"
begin
--- a/src/HOL/TPTP/CASC_Setup.thy Fri Apr 27 14:07:31 2012 +0200
+++ b/src/HOL/TPTP/CASC_Setup.thy Fri Apr 27 15:24:37 2012 +0200
@@ -9,7 +9,7 @@
theory CASC_Setup
imports Complex_Main
-uses "../ex/sledgehammer_tactics.ML"
+uses "sledgehammer_tactics.ML"
begin
consts
--- a/src/HOL/TPTP/TPTP_Parser_Example.thy Fri Apr 27 14:07:31 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser_Example.thy Fri Apr 27 15:24:37 2012 +0200
@@ -6,7 +6,7 @@
theory TPTP_Parser_Example
imports TPTP_Parser TPTP_Interpret
-uses "~~/src/HOL/ex/sledgehammer_tactics.ML"
+uses "sledgehammer_tactics.ML"
begin
import_tptp "$TPTP/Problems/CSR/CSR077+1.p"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML Fri Apr 27 15:24:37 2012 +0200
@@ -0,0 +1,93 @@
+(* Title: HOL/TPTP/sledgehammer_tactics.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2010, 2011
+
+Sledgehammer as a tactic.
+*)
+
+signature SLEDGEHAMMER_TACTICS =
+sig
+ type relevance_override = Sledgehammer_Filter.relevance_override
+
+ val sledgehammer_with_metis_tac :
+ Proof.context -> (string * string) list -> relevance_override -> int
+ -> tactic
+ val sledgehammer_as_oracle_tac :
+ Proof.context -> (string * string) list -> relevance_override -> int
+ -> tactic
+end;
+
+structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
+struct
+
+open Sledgehammer_Filter
+
+fun run_prover override_params relevance_override i n ctxt goal =
+ let
+ val chained_ths = [] (* a tactic has no chained ths *)
+ val params as {provers, relevance_thresholds, max_relevant, slice, ...} =
+ Sledgehammer_Isar.default_params ctxt override_params
+ val name = hd provers
+ val prover =
+ Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name
+ val default_max_relevant =
+ Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice name
+ val is_built_in_const =
+ Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
+ val relevance_fudge =
+ Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
+ val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
+ val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
+ val facts =
+ Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override
+ chained_ths hyp_ts concl_t
+ |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
+ (the_default default_max_relevant max_relevant) is_built_in_const
+ relevance_fudge relevance_override chained_ths hyp_ts concl_t
+ val problem =
+ {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
+ facts = map Sledgehammer_Provers.Untranslated_Fact facts}
+ in
+ (case prover params (K (K (K ""))) problem of
+ {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
+ | _ => NONE)
+ handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
+ end
+
+fun thms_of_name ctxt name =
+ let
+ val lex = Keyword.get_lexicons
+ val get = maps (Proof_Context.get_fact ctxt o fst)
+ in
+ Source.of_string name
+ |> Symbol.source
+ |> Token.source {do_recover=SOME false} lex Position.start
+ |> Token.source_proper
+ |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
+ |> Source.exhaust
+ end
+
+fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th =
+ let
+ val override_params =
+ override_params @
+ [("preplay_timeout", "0")]
+ in
+ case run_prover override_params relevance_override i i ctxt th of
+ SOME facts =>
+ Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt
+ (maps (thms_of_name ctxt) facts) i th
+ | NONE => Seq.empty
+ end
+
+fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val override_params =
+ override_params @
+ [("preplay_timeout", "0"),
+ ("minimize", "false")]
+ val xs = run_prover override_params relevance_override i i ctxt th
+ in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
+
+end;
--- a/src/HOL/ex/sledgehammer_tactics.ML Fri Apr 27 14:07:31 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,93 +0,0 @@
-(* Title: HOL/ex/sledgehammer_tactics.ML
- Author: Jasmin Blanchette, TU Muenchen
- Copyright 2010, 2011
-
-Sledgehammer as a tactic.
-*)
-
-signature SLEDGEHAMMER_TACTICS =
-sig
- type relevance_override = Sledgehammer_Filter.relevance_override
-
- val sledgehammer_with_metis_tac :
- Proof.context -> (string * string) list -> relevance_override -> int
- -> tactic
- val sledgehammer_as_oracle_tac :
- Proof.context -> (string * string) list -> relevance_override -> int
- -> tactic
-end;
-
-structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
-struct
-
-open Sledgehammer_Filter
-
-fun run_prover override_params relevance_override i n ctxt goal =
- let
- val chained_ths = [] (* a tactic has no chained ths *)
- val params as {provers, relevance_thresholds, max_relevant, slice, ...} =
- Sledgehammer_Isar.default_params ctxt override_params
- val name = hd provers
- val prover =
- Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name
- val default_max_relevant =
- Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice name
- val is_built_in_const =
- Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
- val relevance_fudge =
- Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
- val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
- val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
- val facts =
- Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override
- chained_ths hyp_ts concl_t
- |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
- (the_default default_max_relevant max_relevant) is_built_in_const
- relevance_fudge relevance_override chained_ths hyp_ts concl_t
- val problem =
- {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
- facts = map Sledgehammer_Provers.Untranslated_Fact facts}
- in
- (case prover params (K (K (K ""))) problem of
- {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
- | _ => NONE)
- handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
- end
-
-fun thms_of_name ctxt name =
- let
- val lex = Keyword.get_lexicons
- val get = maps (Proof_Context.get_fact ctxt o fst)
- in
- Source.of_string name
- |> Symbol.source
- |> Token.source {do_recover=SOME false} lex Position.start
- |> Token.source_proper
- |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
- |> Source.exhaust
- end
-
-fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th =
- let
- val override_params =
- override_params @
- [("preplay_timeout", "0")]
- in
- case run_prover override_params relevance_override i i ctxt th of
- SOME facts =>
- Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt
- (maps (thms_of_name ctxt) facts) i th
- | NONE => Seq.empty
- end
-
-fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th =
- let
- val thy = Proof_Context.theory_of ctxt
- val override_params =
- override_params @
- [("preplay_timeout", "0"),
- ("minimize", "false")]
- val xs = run_prover override_params relevance_override i i ctxt th
- in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
-
-end;