1.1 --- a/src/HOL/IsaMakefile Fri Apr 27 14:07:31 2012 +0200
1.2 +++ b/src/HOL/IsaMakefile Fri Apr 27 15:24:37 2012 +0200
1.3 @@ -1034,7 +1034,7 @@
1.4 ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy \
1.5 ex/SAT_Examples.thy ex/Serbian.thy ex/Set_Theory.thy \
1.6 ex/Simproc_Tests.thy ex/SVC_Oracle.thy \
1.7 - ex/sledgehammer_tactics.ML ex/Seq.thy ex/Sqrt.thy ex/Sqrt_Script.thy \
1.8 + ex/Seq.thy ex/Sqrt.thy ex/Sqrt_Script.thy \
1.9 ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy \
1.10 ex/Transfer_Int_Nat.thy \
1.11 ex/Tree23.thy ex/Unification.thy ex/While_Combinator_Example.thy \
1.12 @@ -1153,7 +1153,8 @@
1.13 TPTP/TPTP_Parser/tptp_syntax.ML \
1.14 TPTP/TPTP_Parser_Test.thy \
1.15 TPTP/atp_problem_import.ML \
1.16 - TPTP/atp_theory_export.ML
1.17 + TPTP/atp_theory_export.ML \
1.18 + TPTP/sledgehammer_tactics.ML
1.19 @$(ISABELLE_TOOL) usedir $(OUT)/HOL TPTP
1.20
1.21
1.22 @@ -1333,7 +1334,7 @@
1.23 Mirabelle/Tools/mirabelle_refute.ML \
1.24 Mirabelle/Tools/mirabelle_sledgehammer.ML \
1.25 Mirabelle/Tools/mirabelle_sledgehammer_filter.ML \
1.26 - ex/sledgehammer_tactics.ML Mirabelle/lib/Tools/mirabelle \
1.27 + TPTP/sledgehammer_tactics.ML Mirabelle/lib/Tools/mirabelle \
1.28 Mirabelle/lib/scripts/mirabelle.pl Library/FrechetDeriv.thy \
1.29 Library/Inner_Product.thy
1.30 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle
2.1 --- a/src/HOL/Mirabelle/Mirabelle.thy Fri Apr 27 14:07:31 2012 +0200
2.2 +++ b/src/HOL/Mirabelle/Mirabelle.thy Fri Apr 27 15:24:37 2012 +0200
2.3 @@ -5,7 +5,7 @@
2.4 theory Mirabelle
2.5 imports Sledgehammer
2.6 uses "Tools/mirabelle.ML"
2.7 - "../ex/sledgehammer_tactics.ML"
2.8 + "../TPTP/sledgehammer_tactics.ML"
2.9 begin
2.10
2.11 (* no multithreading, no parallel proofs *) (* FIXME *)
3.1 --- a/src/HOL/TPTP/ATP_Problem_Import.thy Fri Apr 27 14:07:31 2012 +0200
3.2 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy Fri Apr 27 15:24:37 2012 +0200
3.3 @@ -3,10 +3,9 @@
3.4 *)
3.5
3.6 header {* ATP Problem Importer *}
3.7 -
3.8 theory ATP_Problem_Import
3.9 imports Complex_Main TPTP_Interpret
3.10 -uses "~~/src/HOL/ex/sledgehammer_tactics.ML"
3.11 +uses "sledgehammer_tactics.ML"
3.12 "atp_problem_import.ML"
3.13 begin
3.14
4.1 --- a/src/HOL/TPTP/CASC_Setup.thy Fri Apr 27 14:07:31 2012 +0200
4.2 +++ b/src/HOL/TPTP/CASC_Setup.thy Fri Apr 27 15:24:37 2012 +0200
4.3 @@ -9,7 +9,7 @@
4.4
4.5 theory CASC_Setup
4.6 imports Complex_Main
4.7 -uses "../ex/sledgehammer_tactics.ML"
4.8 +uses "sledgehammer_tactics.ML"
4.9 begin
4.10
4.11 consts
5.1 --- a/src/HOL/TPTP/TPTP_Parser_Example.thy Fri Apr 27 14:07:31 2012 +0200
5.2 +++ b/src/HOL/TPTP/TPTP_Parser_Example.thy Fri Apr 27 15:24:37 2012 +0200
5.3 @@ -6,7 +6,7 @@
5.4
5.5 theory TPTP_Parser_Example
5.6 imports TPTP_Parser TPTP_Interpret
5.7 -uses "~~/src/HOL/ex/sledgehammer_tactics.ML"
5.8 +uses "sledgehammer_tactics.ML"
5.9 begin
5.10
5.11 import_tptp "$TPTP/Problems/CSR/CSR077+1.p"
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML Fri Apr 27 15:24:37 2012 +0200
6.3 @@ -0,0 +1,93 @@
6.4 +(* Title: HOL/TPTP/sledgehammer_tactics.ML
6.5 + Author: Jasmin Blanchette, TU Muenchen
6.6 + Copyright 2010, 2011
6.7 +
6.8 +Sledgehammer as a tactic.
6.9 +*)
6.10 +
6.11 +signature SLEDGEHAMMER_TACTICS =
6.12 +sig
6.13 + type relevance_override = Sledgehammer_Filter.relevance_override
6.14 +
6.15 + val sledgehammer_with_metis_tac :
6.16 + Proof.context -> (string * string) list -> relevance_override -> int
6.17 + -> tactic
6.18 + val sledgehammer_as_oracle_tac :
6.19 + Proof.context -> (string * string) list -> relevance_override -> int
6.20 + -> tactic
6.21 +end;
6.22 +
6.23 +structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
6.24 +struct
6.25 +
6.26 +open Sledgehammer_Filter
6.27 +
6.28 +fun run_prover override_params relevance_override i n ctxt goal =
6.29 + let
6.30 + val chained_ths = [] (* a tactic has no chained ths *)
6.31 + val params as {provers, relevance_thresholds, max_relevant, slice, ...} =
6.32 + Sledgehammer_Isar.default_params ctxt override_params
6.33 + val name = hd provers
6.34 + val prover =
6.35 + Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name
6.36 + val default_max_relevant =
6.37 + Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice name
6.38 + val is_built_in_const =
6.39 + Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
6.40 + val relevance_fudge =
6.41 + Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
6.42 + val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
6.43 + val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
6.44 + val facts =
6.45 + Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override
6.46 + chained_ths hyp_ts concl_t
6.47 + |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
6.48 + (the_default default_max_relevant max_relevant) is_built_in_const
6.49 + relevance_fudge relevance_override chained_ths hyp_ts concl_t
6.50 + val problem =
6.51 + {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
6.52 + facts = map Sledgehammer_Provers.Untranslated_Fact facts}
6.53 + in
6.54 + (case prover params (K (K (K ""))) problem of
6.55 + {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
6.56 + | _ => NONE)
6.57 + handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
6.58 + end
6.59 +
6.60 +fun thms_of_name ctxt name =
6.61 + let
6.62 + val lex = Keyword.get_lexicons
6.63 + val get = maps (Proof_Context.get_fact ctxt o fst)
6.64 + in
6.65 + Source.of_string name
6.66 + |> Symbol.source
6.67 + |> Token.source {do_recover=SOME false} lex Position.start
6.68 + |> Token.source_proper
6.69 + |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
6.70 + |> Source.exhaust
6.71 + end
6.72 +
6.73 +fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th =
6.74 + let
6.75 + val override_params =
6.76 + override_params @
6.77 + [("preplay_timeout", "0")]
6.78 + in
6.79 + case run_prover override_params relevance_override i i ctxt th of
6.80 + SOME facts =>
6.81 + Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt
6.82 + (maps (thms_of_name ctxt) facts) i th
6.83 + | NONE => Seq.empty
6.84 + end
6.85 +
6.86 +fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th =
6.87 + let
6.88 + val thy = Proof_Context.theory_of ctxt
6.89 + val override_params =
6.90 + override_params @
6.91 + [("preplay_timeout", "0"),
6.92 + ("minimize", "false")]
6.93 + val xs = run_prover override_params relevance_override i i ctxt th
6.94 + in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
6.95 +
6.96 +end;
7.1 --- a/src/HOL/ex/sledgehammer_tactics.ML Fri Apr 27 14:07:31 2012 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,93 +0,0 @@
7.4 -(* Title: HOL/ex/sledgehammer_tactics.ML
7.5 - Author: Jasmin Blanchette, TU Muenchen
7.6 - Copyright 2010, 2011
7.7 -
7.8 -Sledgehammer as a tactic.
7.9 -*)
7.10 -
7.11 -signature SLEDGEHAMMER_TACTICS =
7.12 -sig
7.13 - type relevance_override = Sledgehammer_Filter.relevance_override
7.14 -
7.15 - val sledgehammer_with_metis_tac :
7.16 - Proof.context -> (string * string) list -> relevance_override -> int
7.17 - -> tactic
7.18 - val sledgehammer_as_oracle_tac :
7.19 - Proof.context -> (string * string) list -> relevance_override -> int
7.20 - -> tactic
7.21 -end;
7.22 -
7.23 -structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
7.24 -struct
7.25 -
7.26 -open Sledgehammer_Filter
7.27 -
7.28 -fun run_prover override_params relevance_override i n ctxt goal =
7.29 - let
7.30 - val chained_ths = [] (* a tactic has no chained ths *)
7.31 - val params as {provers, relevance_thresholds, max_relevant, slice, ...} =
7.32 - Sledgehammer_Isar.default_params ctxt override_params
7.33 - val name = hd provers
7.34 - val prover =
7.35 - Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name
7.36 - val default_max_relevant =
7.37 - Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice name
7.38 - val is_built_in_const =
7.39 - Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
7.40 - val relevance_fudge =
7.41 - Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
7.42 - val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
7.43 - val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
7.44 - val facts =
7.45 - Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override
7.46 - chained_ths hyp_ts concl_t
7.47 - |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
7.48 - (the_default default_max_relevant max_relevant) is_built_in_const
7.49 - relevance_fudge relevance_override chained_ths hyp_ts concl_t
7.50 - val problem =
7.51 - {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
7.52 - facts = map Sledgehammer_Provers.Untranslated_Fact facts}
7.53 - in
7.54 - (case prover params (K (K (K ""))) problem of
7.55 - {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
7.56 - | _ => NONE)
7.57 - handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
7.58 - end
7.59 -
7.60 -fun thms_of_name ctxt name =
7.61 - let
7.62 - val lex = Keyword.get_lexicons
7.63 - val get = maps (Proof_Context.get_fact ctxt o fst)
7.64 - in
7.65 - Source.of_string name
7.66 - |> Symbol.source
7.67 - |> Token.source {do_recover=SOME false} lex Position.start
7.68 - |> Token.source_proper
7.69 - |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
7.70 - |> Source.exhaust
7.71 - end
7.72 -
7.73 -fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th =
7.74 - let
7.75 - val override_params =
7.76 - override_params @
7.77 - [("preplay_timeout", "0")]
7.78 - in
7.79 - case run_prover override_params relevance_override i i ctxt th of
7.80 - SOME facts =>
7.81 - Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt
7.82 - (maps (thms_of_name ctxt) facts) i th
7.83 - | NONE => Seq.empty
7.84 - end
7.85 -
7.86 -fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th =
7.87 - let
7.88 - val thy = Proof_Context.theory_of ctxt
7.89 - val override_params =
7.90 - override_params @
7.91 - [("preplay_timeout", "0"),
7.92 - ("minimize", "false")]
7.93 - val xs = run_prover override_params relevance_override i i ctxt th
7.94 - in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
7.95 -
7.96 -end;