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;