# HG changeset patch # User blanchet # Date 1335533077 -7200 # Node ID 2e1636e45770a19c55719988a0c93f2621f5e380 # Parent 71a526ee569ab61ccdba985c02de921018350964 move file to where it belongs diff -r 71a526ee569a -r 2e1636e45770 src/HOL/IsaMakefile --- 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 diff -r 71a526ee569a -r 2e1636e45770 src/HOL/Mirabelle/Mirabelle.thy --- 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 *) diff -r 71a526ee569a -r 2e1636e45770 src/HOL/TPTP/ATP_Problem_Import.thy --- 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 diff -r 71a526ee569a -r 2e1636e45770 src/HOL/TPTP/CASC_Setup.thy --- 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 diff -r 71a526ee569a -r 2e1636e45770 src/HOL/TPTP/TPTP_Parser_Example.thy --- 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" diff -r 71a526ee569a -r 2e1636e45770 src/HOL/TPTP/sledgehammer_tactics.ML --- /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; diff -r 71a526ee569a -r 2e1636e45770 src/HOL/ex/sledgehammer_tactics.ML --- 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;