# HG changeset patch # User blanchet # Date 1300871187 -3600 # Node ID 04577a7e0c51fea48864f94a0363d0352c81fca0 # Parent 6a147393c62a65a2a6551b0fd1c650bb10622c4e 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 diff -r 6a147393c62a -r 04577a7e0c51 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Mar 23 09:15:49 2011 +0100 +++ b/src/HOL/IsaMakefile Wed Mar 23 10:06:27 2011 +0100 @@ -467,8 +467,8 @@ Library/Sublist_Order.thy Library/Sum_of_Squares.thy \ Library/Sum_of_Squares/sos_wrapper.ML \ Library/Sum_of_Squares/sum_of_squares.ML \ - Library/TPTP.thy Library/Transitive_Closure_Table.thy \ - Library/Univ_Poly.thy Library/While_Combinator.thy Library/Zorn.thy \ + Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy \ + Library/While_Combinator.thy Library/Zorn.thy \ $(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML \ Library/reflection.ML Library/reify_data.ML \ Library/Quickcheck_Narrowing.thy \ @@ -1048,9 +1048,10 @@ ex/Quickcheck_Narrowing_Examples.thy \ ex/Quicksort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \ ex/ReflectionEx.thy ex/Refute_Examples.thy ex/SAT_Examples.thy \ - ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy ex/Sqrt.thy \ + ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy \ + ex/sledgehammer_tactics.ML ex/Sqrt.thy \ ex/Sqrt_Script.thy ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy \ - ex/Transfer_Ex.thy ex/Tree23.thy ex/Unification.thy \ + ex/TPTP.thy ex/Transfer_Ex.thy ex/Tree23.thy ex/Unification.thy \ ex/While_Combinator_Example.thy ex/document/root.bib \ ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \ ../Tools/interpretation_with_defs.ML @@ -1316,9 +1317,9 @@ Mirabelle/Tools/mirabelle_refute.ML \ Mirabelle/Tools/mirabelle_sledgehammer.ML \ Mirabelle/Tools/mirabelle_sledgehammer_filter.ML \ - Mirabelle/Tools/sledgehammer_tactics.ML \ - Mirabelle/lib/Tools/mirabelle Mirabelle/lib/scripts/mirabelle.pl \ - Library/FrechetDeriv.thy Library/Inner_Product.thy + ex/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 @cd Library; $(ISABELLE_TOOL) mirabelle -q arith Inner_Product.thy # some arbitrary small test case diff -r 6a147393c62a -r 04577a7e0c51 src/HOL/Library/TPTP.thy --- a/src/HOL/Library/TPTP.thy Wed Mar 23 09:15:49 2011 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,50 +0,0 @@ -theory TPTP -imports Main -uses "~~/src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML" -begin - -declare mem_def [simp add] - -declare [[smt_oracle]] - -ML {* proofs := 0 *} - -ML {* -fun SOLVE_TIMEOUT seconds name tac st = - let - val result = - TimeLimit.timeLimit (Time.fromSeconds seconds) - (fn () => SINGLE (SOLVE tac) st) () - handle TimeLimit.TimeOut => NONE - | ERROR _ => NONE - in - (case result of - NONE => (writeln ("FAILURE: " ^ name); Seq.empty) - | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st')) - end -*} - -ML {* -fun isabellep_tac max_secs = - SOLVE_TIMEOUT (max_secs div 5) "sledgehammer" - (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context})) - ORELSE - SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac @{simpset})) - ORELSE - SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac @{claset})) - ORELSE - SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac @{clasimpset} - THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context})) - ORELSE - SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac @{context} [])) - ORELSE - SOLVE_TIMEOUT (max_secs div 5) "fast" (ALLGOALS (fast_tac @{claset})) - ORELSE - SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac @{claset})) - ORELSE - SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac @{clasimpset})) - ORELSE - SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac @{clasimpset})) -*} - -end diff -r 6a147393c62a -r 04577a7e0c51 src/HOL/Mirabelle/Mirabelle.thy --- a/src/HOL/Mirabelle/Mirabelle.thy Wed Mar 23 09:15:49 2011 +0100 +++ b/src/HOL/Mirabelle/Mirabelle.thy Wed Mar 23 10:06:27 2011 +0100 @@ -5,7 +5,7 @@ theory Mirabelle imports Sledgehammer uses "Tools/mirabelle.ML" - "Tools/sledgehammer_tactics.ML" + "../ex/sledgehammer_tactics.ML" begin (* no multithreading, no parallel proofs *) (* FIXME *) diff -r 6a147393c62a -r 04577a7e0c51 src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML --- a/src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML Wed Mar 23 09:15:49 2011 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,94 +0,0 @@ -(* Title: HOL/Mirabelle/Tools/sledgehammer_tactics.ML - Author: Jasmin Blanchette, TU Muenchen - Copyright 2010 - -Sledgehammer as a tactic. -*) - -signature SLEDGEHAMMER_TACTICS = -sig - val sledgehammer_with_metis_tac : Proof.context -> int -> tactic - val sledgehammer_as_unsound_oracle_tac : Proof.context -> int -> tactic - val sledgehammer_as_oracle_tac : Proof.context -> int -> tactic -end; - -structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS = -struct - -fun run_atp force_full_types timeout i n ctxt goal name = - let - val chained_ths = [] (* a tactic has no chained ths *) - val params as {type_sys, relevance_thresholds, max_relevant, ...} = - ((if force_full_types then [("full_types", "true")] else []) - @ [("timeout", string_of_int (Time.toSeconds timeout))]) - (* @ [("overlord", "true")] *) - |> Sledgehammer_Isar.default_params ctxt - val prover = Sledgehammer_Provers.get_prover ctxt false name - val default_max_relevant = - Sledgehammer_Provers.default_max_relevant_for_prover ctxt 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 relevance_override = {add = [], del = [], only = false} - val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i - val no_dangerous_types = - Sledgehammer_ATP_Translate.types_dangerous_types type_sys - val facts = - Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types - 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, - smt_filter = NONE} - in - (case prover params (K "") problem of - {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME - | _ => NONE) - handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE) - end - -fun to_period ("." :: _) = [] - | to_period ("" :: ss) = to_period ss - | to_period (s :: ss) = s :: to_period ss - | to_period [] = [] - -val atp = "vampire" (* or "e" or "spass" etc. *) - -fun thms_of_name ctxt name = - let - val lex = Keyword.get_lexicons - val get = maps (ProofContext.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 i th = - let - val timeout = Time.fromSeconds 30 - in - case run_atp false timeout i i ctxt th atp of - SOME facts => - Metis_Tactics.metis_tac ctxt (maps (thms_of_name ctxt) facts) i th - | NONE => Seq.empty - end - -fun generic_sledgehammer_as_oracle_tac force_full_types ctxt i th = - let - val thy = ProofContext.theory_of ctxt - val timeout = Time.fromSeconds 30 - val xs = run_atp force_full_types timeout i i ctxt th atp - in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end - -val sledgehammer_as_unsound_oracle_tac = - generic_sledgehammer_as_oracle_tac false -val sledgehammer_as_oracle_tac = generic_sledgehammer_as_oracle_tac true - -end; diff -r 6a147393c62a -r 04577a7e0c51 src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Wed Mar 23 09:15:49 2011 +0100 +++ b/src/HOL/ex/ROOT.ML Wed Mar 23 10:06:27 2011 +0100 @@ -73,7 +73,8 @@ "Quicksort", "Birthday_Paradoxon", "List_to_Set_Comprehension_Examples", - "Set_Algebras" + "Set_Algebras", + "TPTP" ]; if getenv "ISABELLE_GHC" = "" then () diff -r 6a147393c62a -r 04577a7e0c51 src/HOL/ex/TPTP.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/TPTP.thy Wed Mar 23 10:06:27 2011 +0100 @@ -0,0 +1,57 @@ +(* Title: HOL/ex/TPTP.thy + Author: Jasmin Blanchette + Copyright 2011 + +TPTP "IsabelleP" tactic. +*) + +theory TPTP +imports Main +uses "sledgehammer_tactics.ML" +begin + +declare mem_def [simp add] + +declare [[smt_oracle]] + +ML {* proofs := 0 *} + +ML {* +fun SOLVE_TIMEOUT seconds name tac st = + let + val result = + TimeLimit.timeLimit (Time.fromSeconds seconds) + (fn () => SINGLE (SOLVE tac) st) () + handle TimeLimit.TimeOut => NONE + | ERROR _ => NONE + in + (case result of + NONE => (writeln ("FAILURE: " ^ name); Seq.empty) + | SOME st' => (writeln ("SUCCESS: " ^ name); Seq.single st')) + end +*} + +ML {* +fun isabellep_tac max_secs = + SOLVE_TIMEOUT (max_secs div 5) "sledgehammer" + (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context})) + ORELSE + SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac @{simpset})) + ORELSE + SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac @{claset})) + ORELSE + SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac @{clasimpset} + THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac @{context})) + ORELSE + SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac @{context} [])) + ORELSE + SOLVE_TIMEOUT (max_secs div 5) "fast" (ALLGOALS (fast_tac @{claset})) + ORELSE + SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac @{claset})) + ORELSE + SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac @{clasimpset})) + ORELSE + SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac @{clasimpset})) +*} + +end diff -r 6a147393c62a -r 04577a7e0c51 src/HOL/ex/sledgehammer_tactics.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/sledgehammer_tactics.ML Wed Mar 23 10:06:27 2011 +0100 @@ -0,0 +1,94 @@ +(* Title: HOL/ex/sledgehammer_tactics.ML + Author: Jasmin Blanchette, TU Muenchen + Copyright 2010, 2011 + +Sledgehammer as a tactic. +*) + +signature SLEDGEHAMMER_TACTICS = +sig + val sledgehammer_with_metis_tac : Proof.context -> int -> tactic + val sledgehammer_as_unsound_oracle_tac : Proof.context -> int -> tactic + val sledgehammer_as_oracle_tac : Proof.context -> int -> tactic +end; + +structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS = +struct + +fun run_atp force_full_types timeout i n ctxt goal name = + let + val chained_ths = [] (* a tactic has no chained ths *) + val params as {type_sys, relevance_thresholds, max_relevant, ...} = + ((if force_full_types then [("full_types", "true")] else []) + @ [("timeout", string_of_int (Time.toSeconds timeout))]) + (* @ [("overlord", "true")] *) + |> Sledgehammer_Isar.default_params ctxt + val prover = Sledgehammer_Provers.get_prover ctxt false name + val default_max_relevant = + Sledgehammer_Provers.default_max_relevant_for_prover ctxt 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 relevance_override = {add = [], del = [], only = false} + val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i + val no_dangerous_types = + Sledgehammer_ATP_Translate.types_dangerous_types type_sys + val facts = + Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types + 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, + smt_filter = NONE} + in + (case prover params (K "") problem of + {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME + | _ => NONE) + handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE) + end + +fun to_period ("." :: _) = [] + | to_period ("" :: ss) = to_period ss + | to_period (s :: ss) = s :: to_period ss + | to_period [] = [] + +val atp = "e" (* or "vampire" or "spass" etc. *) + +fun thms_of_name ctxt name = + let + val lex = Keyword.get_lexicons + val get = maps (ProofContext.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 i th = + let + val timeout = Time.fromSeconds 30 + in + case run_atp false timeout i i ctxt th atp of + SOME facts => + Metis_Tactics.metis_tac ctxt (maps (thms_of_name ctxt) facts) i th + | NONE => Seq.empty + end + +fun generic_sledgehammer_as_oracle_tac force_full_types ctxt i th = + let + val thy = ProofContext.theory_of ctxt + val timeout = Time.fromSeconds 30 + val xs = run_atp force_full_types timeout i i ctxt th atp + in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end + +val sledgehammer_as_unsound_oracle_tac = + generic_sledgehammer_as_oracle_tac false +val sledgehammer_as_oracle_tac = generic_sledgehammer_as_oracle_tac true + +end;