move file to where it belongs
authorblanchet
Fri Apr 27 15:24:37 2012 +0200 (2012-04-27)
changeset 477902e1636e45770
parent 47789 71a526ee569a
child 47791 c17cc1380642
move file to where it belongs
src/HOL/IsaMakefile
src/HOL/Mirabelle/Mirabelle.thy
src/HOL/TPTP/ATP_Problem_Import.thy
src/HOL/TPTP/CASC_Setup.thy
src/HOL/TPTP/TPTP_Parser_Example.thy
src/HOL/TPTP/sledgehammer_tactics.ML
src/HOL/ex/sledgehammer_tactics.ML
     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;