move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
authorblanchet
Wed Mar 23 10:06:27 2011 +0100 (2011-03-23)
changeset 4207104577a7e0c51
parent 42069 6a147393c62a
child 42072 1492ee6b8085
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
default to "e" rather than "vampire" since E is part of the Isabelle bundle
src/HOL/IsaMakefile
src/HOL/Library/TPTP.thy
src/HOL/Mirabelle/Mirabelle.thy
src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML
src/HOL/ex/ROOT.ML
src/HOL/ex/TPTP.thy
src/HOL/ex/sledgehammer_tactics.ML
     1.1 --- a/src/HOL/IsaMakefile	Wed Mar 23 09:15:49 2011 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Wed Mar 23 10:06:27 2011 +0100
     1.3 @@ -467,8 +467,8 @@
     1.4    Library/Sublist_Order.thy Library/Sum_of_Squares.thy			\
     1.5    Library/Sum_of_Squares/sos_wrapper.ML					\
     1.6    Library/Sum_of_Squares/sum_of_squares.ML				\
     1.7 -  Library/TPTP.thy Library/Transitive_Closure_Table.thy			\
     1.8 -  Library/Univ_Poly.thy Library/While_Combinator.thy Library/Zorn.thy	\
     1.9 +  Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy		\
    1.10 +  Library/While_Combinator.thy Library/Zorn.thy	\
    1.11    $(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML	\
    1.12    Library/reflection.ML Library/reify_data.ML				\
    1.13    Library/Quickcheck_Narrowing.thy \
    1.14 @@ -1048,9 +1048,10 @@
    1.15    ex/Quickcheck_Narrowing_Examples.thy \
    1.16    ex/Quicksort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy		\
    1.17    ex/ReflectionEx.thy ex/Refute_Examples.thy ex/SAT_Examples.thy	\
    1.18 -  ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy ex/Sqrt.thy	\
    1.19 +  ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy			\
    1.20 +  ex/sledgehammer_tactics.ML ex/Sqrt.thy				\
    1.21    ex/Sqrt_Script.thy ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy	\
    1.22 -  ex/Transfer_Ex.thy ex/Tree23.thy ex/Unification.thy			\
    1.23 +  ex/TPTP.thy ex/Transfer_Ex.thy ex/Tree23.thy ex/Unification.thy	\
    1.24    ex/While_Combinator_Example.thy ex/document/root.bib			\
    1.25    ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy	\
    1.26    ../Tools/interpretation_with_defs.ML
    1.27 @@ -1316,9 +1317,9 @@
    1.28    Mirabelle/Tools/mirabelle_refute.ML					\
    1.29    Mirabelle/Tools/mirabelle_sledgehammer.ML 				\
    1.30    Mirabelle/Tools/mirabelle_sledgehammer_filter.ML			\
    1.31 -  Mirabelle/Tools/sledgehammer_tactics.ML 				\
    1.32 -  Mirabelle/lib/Tools/mirabelle Mirabelle/lib/scripts/mirabelle.pl	\
    1.33 -  Library/FrechetDeriv.thy Library/Inner_Product.thy
    1.34 +  ex/sledgehammer_tactics.ML Mirabelle/lib/Tools/mirabelle		\
    1.35 +  Mirabelle/lib/scripts/mirabelle.pl Library/FrechetDeriv.thy		\
    1.36 +  Library/Inner_Product.thy
    1.37  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle
    1.38  	@cd Library; $(ISABELLE_TOOL) mirabelle -q arith Inner_Product.thy # some arbitrary small test case
    1.39  
     2.1 --- a/src/HOL/Library/TPTP.thy	Wed Mar 23 09:15:49 2011 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,50 +0,0 @@
     2.4 -theory TPTP
     2.5 -imports Main
     2.6 -uses "~~/src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML"
     2.7 -begin
     2.8 -
     2.9 -declare mem_def [simp add]
    2.10 -
    2.11 -declare [[smt_oracle]]
    2.12 -
    2.13 -ML {* proofs := 0 *}
    2.14 -
    2.15 -ML {*
    2.16 -fun SOLVE_TIMEOUT seconds name tac st =
    2.17 -  let
    2.18 -    val result =
    2.19 -      TimeLimit.timeLimit (Time.fromSeconds seconds)
    2.20 -        (fn () => SINGLE (SOLVE tac) st) ()
    2.21 -      handle TimeLimit.TimeOut => NONE
    2.22 -        | ERROR _ => NONE
    2.23 -  in
    2.24 -    (case result of
    2.25 -      NONE => (writeln ("FAILURE: " ^ name); Seq.empty)
    2.26 -    | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st'))
    2.27 -  end
    2.28 -*}
    2.29 -
    2.30 -ML {*
    2.31 -fun isabellep_tac max_secs =
    2.32 -   SOLVE_TIMEOUT (max_secs div 5) "sledgehammer"
    2.33 -       (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context}))
    2.34 -   ORELSE
    2.35 -   SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac @{simpset}))
    2.36 -   ORELSE
    2.37 -   SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac @{claset}))
    2.38 -   ORELSE
    2.39 -   SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac @{clasimpset}
    2.40 -       THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context}))
    2.41 -   ORELSE
    2.42 -   SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac @{context} []))
    2.43 -   ORELSE
    2.44 -   SOLVE_TIMEOUT (max_secs div 5) "fast" (ALLGOALS (fast_tac @{claset}))
    2.45 -   ORELSE
    2.46 -   SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac @{claset}))
    2.47 -   ORELSE
    2.48 -   SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac @{clasimpset}))
    2.49 -   ORELSE
    2.50 -   SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac @{clasimpset}))
    2.51 -*}
    2.52 -
    2.53 -end
     3.1 --- a/src/HOL/Mirabelle/Mirabelle.thy	Wed Mar 23 09:15:49 2011 +0100
     3.2 +++ b/src/HOL/Mirabelle/Mirabelle.thy	Wed Mar 23 10:06:27 2011 +0100
     3.3 @@ -5,7 +5,7 @@
     3.4  theory Mirabelle
     3.5  imports Sledgehammer
     3.6  uses "Tools/mirabelle.ML"
     3.7 -     "Tools/sledgehammer_tactics.ML"
     3.8 +     "../ex/sledgehammer_tactics.ML"
     3.9  begin
    3.10  
    3.11  (* no multithreading, no parallel proofs *)  (* FIXME *)
     4.1 --- a/src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML	Wed Mar 23 09:15:49 2011 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,94 +0,0 @@
     4.4 -(*  Title:      HOL/Mirabelle/Tools/sledgehammer_tactics.ML
     4.5 -    Author:     Jasmin Blanchette, TU Muenchen
     4.6 -    Copyright   2010
     4.7 -
     4.8 -Sledgehammer as a tactic.
     4.9 -*)
    4.10 -
    4.11 -signature SLEDGEHAMMER_TACTICS =
    4.12 -sig
    4.13 -  val sledgehammer_with_metis_tac : Proof.context -> int -> tactic
    4.14 -  val sledgehammer_as_unsound_oracle_tac : Proof.context -> int -> tactic
    4.15 -  val sledgehammer_as_oracle_tac : Proof.context -> int -> tactic
    4.16 -end;
    4.17 -
    4.18 -structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
    4.19 -struct
    4.20 -  
    4.21 -fun run_atp force_full_types timeout i n ctxt goal name =
    4.22 -  let
    4.23 -    val chained_ths = [] (* a tactic has no chained ths *)
    4.24 -    val params as {type_sys, relevance_thresholds, max_relevant, ...} =
    4.25 -      ((if force_full_types then [("full_types", "true")] else [])
    4.26 -       @ [("timeout", string_of_int (Time.toSeconds timeout))])
    4.27 -       (* @ [("overlord", "true")] *)
    4.28 -      |> Sledgehammer_Isar.default_params ctxt
    4.29 -    val prover = Sledgehammer_Provers.get_prover ctxt false name
    4.30 -    val default_max_relevant =
    4.31 -      Sledgehammer_Provers.default_max_relevant_for_prover ctxt name
    4.32 -    val is_built_in_const =
    4.33 -      Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
    4.34 -    val relevance_fudge =
    4.35 -      Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
    4.36 -    val relevance_override = {add = [], del = [], only = false}
    4.37 -    val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
    4.38 -    val no_dangerous_types =
    4.39 -      Sledgehammer_ATP_Translate.types_dangerous_types type_sys
    4.40 -    val facts =
    4.41 -      Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types
    4.42 -          relevance_thresholds
    4.43 -          (the_default default_max_relevant max_relevant) is_built_in_const
    4.44 -          relevance_fudge relevance_override chained_ths hyp_ts concl_t
    4.45 -    val problem =
    4.46 -      {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
    4.47 -       facts = map Sledgehammer_Provers.Untranslated_Fact facts,
    4.48 -       smt_filter = NONE}
    4.49 -  in
    4.50 -    (case prover params (K "") problem of
    4.51 -      {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
    4.52 -    | _ => NONE)
    4.53 -      handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
    4.54 -  end
    4.55 -
    4.56 -fun to_period ("." :: _) = []
    4.57 -  | to_period ("" :: ss) = to_period ss
    4.58 -  | to_period (s :: ss) = s :: to_period ss
    4.59 -  | to_period [] = []
    4.60 -
    4.61 -val atp = "vampire" (* or "e" or "spass" etc. *)
    4.62 -
    4.63 -fun thms_of_name ctxt name =
    4.64 -  let
    4.65 -    val lex = Keyword.get_lexicons
    4.66 -    val get = maps (ProofContext.get_fact ctxt o fst)
    4.67 -  in
    4.68 -    Source.of_string name
    4.69 -    |> Symbol.source
    4.70 -    |> Token.source {do_recover=SOME false} lex Position.start
    4.71 -    |> Token.source_proper
    4.72 -    |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
    4.73 -    |> Source.exhaust
    4.74 -  end
    4.75 -
    4.76 -fun sledgehammer_with_metis_tac ctxt i th =
    4.77 -  let
    4.78 -    val timeout = Time.fromSeconds 30
    4.79 -  in
    4.80 -    case run_atp false timeout i i ctxt th atp of
    4.81 -      SOME facts =>
    4.82 -      Metis_Tactics.metis_tac ctxt (maps (thms_of_name ctxt) facts) i th
    4.83 -    | NONE => Seq.empty
    4.84 -  end
    4.85 -
    4.86 -fun generic_sledgehammer_as_oracle_tac force_full_types ctxt i th =
    4.87 -  let
    4.88 -    val thy = ProofContext.theory_of ctxt
    4.89 -    val timeout = Time.fromSeconds 30
    4.90 -    val xs = run_atp force_full_types timeout i i ctxt th atp
    4.91 -  in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
    4.92 -
    4.93 -val sledgehammer_as_unsound_oracle_tac =
    4.94 -  generic_sledgehammer_as_oracle_tac false
    4.95 -val sledgehammer_as_oracle_tac = generic_sledgehammer_as_oracle_tac true
    4.96 -
    4.97 -end;
     5.1 --- a/src/HOL/ex/ROOT.ML	Wed Mar 23 09:15:49 2011 +0100
     5.2 +++ b/src/HOL/ex/ROOT.ML	Wed Mar 23 10:06:27 2011 +0100
     5.3 @@ -73,7 +73,8 @@
     5.4    "Quicksort",
     5.5    "Birthday_Paradoxon",
     5.6    "List_to_Set_Comprehension_Examples",
     5.7 -  "Set_Algebras"
     5.8 +  "Set_Algebras",
     5.9 +  "TPTP"
    5.10  ];
    5.11  
    5.12  if getenv "ISABELLE_GHC" = "" then ()
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/ex/TPTP.thy	Wed Mar 23 10:06:27 2011 +0100
     6.3 @@ -0,0 +1,57 @@
     6.4 +(*  Title:      HOL/ex/TPTP.thy
     6.5 +    Author:     Jasmin Blanchette
     6.6 +    Copyright   2011
     6.7 +
     6.8 +TPTP "IsabelleP" tactic.
     6.9 +*)
    6.10 +
    6.11 +theory TPTP
    6.12 +imports Main
    6.13 +uses "sledgehammer_tactics.ML"
    6.14 +begin
    6.15 +
    6.16 +declare mem_def [simp add]
    6.17 +
    6.18 +declare [[smt_oracle]]
    6.19 +
    6.20 +ML {* proofs := 0 *}
    6.21 +
    6.22 +ML {*
    6.23 +fun SOLVE_TIMEOUT seconds name tac st =
    6.24 +  let
    6.25 +    val result =
    6.26 +      TimeLimit.timeLimit (Time.fromSeconds seconds)
    6.27 +        (fn () => SINGLE (SOLVE tac) st) ()
    6.28 +      handle TimeLimit.TimeOut => NONE
    6.29 +        | ERROR _ => NONE
    6.30 +  in
    6.31 +    (case result of
    6.32 +      NONE => (writeln ("FAILURE: " ^ name); Seq.empty)
    6.33 +    | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st'))
    6.34 +  end
    6.35 +*}
    6.36 +
    6.37 +ML {*
    6.38 +fun isabellep_tac max_secs =
    6.39 +   SOLVE_TIMEOUT (max_secs div 5) "sledgehammer"
    6.40 +       (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context}))
    6.41 +   ORELSE
    6.42 +   SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac @{simpset}))
    6.43 +   ORELSE
    6.44 +   SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac @{claset}))
    6.45 +   ORELSE
    6.46 +   SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac @{clasimpset}
    6.47 +       THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context}))
    6.48 +   ORELSE
    6.49 +   SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac @{context} []))
    6.50 +   ORELSE
    6.51 +   SOLVE_TIMEOUT (max_secs div 5) "fast" (ALLGOALS (fast_tac @{claset}))
    6.52 +   ORELSE
    6.53 +   SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac @{claset}))
    6.54 +   ORELSE
    6.55 +   SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac @{clasimpset}))
    6.56 +   ORELSE
    6.57 +   SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac @{clasimpset}))
    6.58 +*}
    6.59 +
    6.60 +end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Wed Mar 23 10:06:27 2011 +0100
     7.3 @@ -0,0 +1,94 @@
     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 +  val sledgehammer_with_metis_tac : Proof.context -> int -> tactic
    7.14 +  val sledgehammer_as_unsound_oracle_tac : Proof.context -> int -> tactic
    7.15 +  val sledgehammer_as_oracle_tac : Proof.context -> int -> tactic
    7.16 +end;
    7.17 +
    7.18 +structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
    7.19 +struct
    7.20 +
    7.21 +fun run_atp force_full_types timeout i n ctxt goal name =
    7.22 +  let
    7.23 +    val chained_ths = [] (* a tactic has no chained ths *)
    7.24 +    val params as {type_sys, relevance_thresholds, max_relevant, ...} =
    7.25 +      ((if force_full_types then [("full_types", "true")] else [])
    7.26 +       @ [("timeout", string_of_int (Time.toSeconds timeout))])
    7.27 +       (* @ [("overlord", "true")] *)
    7.28 +      |> Sledgehammer_Isar.default_params ctxt
    7.29 +    val prover = Sledgehammer_Provers.get_prover ctxt false name
    7.30 +    val default_max_relevant =
    7.31 +      Sledgehammer_Provers.default_max_relevant_for_prover ctxt name
    7.32 +    val is_built_in_const =
    7.33 +      Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
    7.34 +    val relevance_fudge =
    7.35 +      Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
    7.36 +    val relevance_override = {add = [], del = [], only = false}
    7.37 +    val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
    7.38 +    val no_dangerous_types =
    7.39 +      Sledgehammer_ATP_Translate.types_dangerous_types type_sys
    7.40 +    val facts =
    7.41 +      Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types
    7.42 +          relevance_thresholds
    7.43 +          (the_default default_max_relevant max_relevant) is_built_in_const
    7.44 +          relevance_fudge relevance_override chained_ths hyp_ts concl_t
    7.45 +    val problem =
    7.46 +      {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
    7.47 +       facts = map Sledgehammer_Provers.Untranslated_Fact facts,
    7.48 +       smt_filter = NONE}
    7.49 +  in
    7.50 +    (case prover params (K "") problem of
    7.51 +      {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
    7.52 +    | _ => NONE)
    7.53 +      handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
    7.54 +  end
    7.55 +
    7.56 +fun to_period ("." :: _) = []
    7.57 +  | to_period ("" :: ss) = to_period ss
    7.58 +  | to_period (s :: ss) = s :: to_period ss
    7.59 +  | to_period [] = []
    7.60 +
    7.61 +val atp = "e" (* or "vampire" or "spass" etc. *)
    7.62 +
    7.63 +fun thms_of_name ctxt name =
    7.64 +  let
    7.65 +    val lex = Keyword.get_lexicons
    7.66 +    val get = maps (ProofContext.get_fact ctxt o fst)
    7.67 +  in
    7.68 +    Source.of_string name
    7.69 +    |> Symbol.source
    7.70 +    |> Token.source {do_recover=SOME false} lex Position.start
    7.71 +    |> Token.source_proper
    7.72 +    |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
    7.73 +    |> Source.exhaust
    7.74 +  end
    7.75 +
    7.76 +fun sledgehammer_with_metis_tac ctxt i th =
    7.77 +  let
    7.78 +    val timeout = Time.fromSeconds 30
    7.79 +  in
    7.80 +    case run_atp false timeout i i ctxt th atp of
    7.81 +      SOME facts =>
    7.82 +      Metis_Tactics.metis_tac ctxt (maps (thms_of_name ctxt) facts) i th
    7.83 +    | NONE => Seq.empty
    7.84 +  end
    7.85 +
    7.86 +fun generic_sledgehammer_as_oracle_tac force_full_types ctxt i th =
    7.87 +  let
    7.88 +    val thy = ProofContext.theory_of ctxt
    7.89 +    val timeout = Time.fromSeconds 30
    7.90 +    val xs = run_atp force_full_types timeout i i ctxt th atp
    7.91 +  in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
    7.92 +
    7.93 +val sledgehammer_as_unsound_oracle_tac =
    7.94 +  generic_sledgehammer_as_oracle_tac false
    7.95 +val sledgehammer_as_oracle_tac = generic_sledgehammer_as_oracle_tac true
    7.96 +
    7.97 +end;