isabelle: src/HOL/ex/CASC_Setup.thy@fad8634cee62 (annotated)

42601 cddab94eeb14 renamed theory to make its purpose clearer blanchet parents: 42213 diff changeset	1	(* Title: HOL/ex/CASC_Setup.thy
42071 04577a7e0c51 move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex" blanchet parents: 42063 diff changeset	2	Author: Jasmin Blanchette
04577a7e0c51 move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex" blanchet parents: 42063 diff changeset	3	Copyright 2011
04577a7e0c51 move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex" blanchet parents: 42063 diff changeset	4
42601 cddab94eeb14 renamed theory to make its purpose clearer blanchet parents: 42213 diff changeset	5	Setup for Isabelle, Nitpick, and Refute for participating at CASC in the THF and
cddab94eeb14 renamed theory to make its purpose clearer blanchet parents: 42213 diff changeset	6	TNT divisions. This theory file should be loaded by the Isabelle theory files
cddab94eeb14 renamed theory to make its purpose clearer blanchet parents: 42213 diff changeset	7	generated by Geoff Sutcliffe's TPTP2X tool from the original THF0 files.
42071 04577a7e0c51 move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex" blanchet parents: 42063 diff changeset	8	*)
04577a7e0c51 move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex" blanchet parents: 42063 diff changeset	9
42601 cddab94eeb14 renamed theory to make its purpose clearer blanchet parents: 42213 diff changeset	10	theory CASC_Setup
42063 a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	11	imports Main
42071 04577a7e0c51 move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex" blanchet parents: 42063 diff changeset	12	uses "sledgehammer_tactics.ML"
42063 a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	13	begin
a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	14
a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	15	declare mem_def [simp add]
a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	16
a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	17	declare [[smt_oracle]]
a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	18
42106 ed1d40888b1b specify proper defaults for Nitpick and Refute on TPTP + tuning blanchet parents: 42078 diff changeset	19	refute_params [maxtime = 10000, no_assms, expect = genuine]
ed1d40888b1b specify proper defaults for Nitpick and Refute on TPTP + tuning blanchet parents: 42078 diff changeset	20	nitpick_params [timeout = none, card = 1-50, verbose, dont_box, no_assms,
42211 9e2673711c77 make sure that Nitpick problem generation for cardinality 50 doesn't cause problems for lower cardinality by specifying the "batch_size" option blanchet parents: 42106 diff changeset	21	batch_size = 1, expect = genuine]
42106 ed1d40888b1b specify proper defaults for Nitpick and Refute on TPTP + tuning blanchet parents: 42078 diff changeset	22
42078 d5bf0ce40bd7 isolate change of Proofterm.proofs in TPTP.thy from rest of session; wenzelm parents: 42071 diff changeset	23	ML {* Proofterm.proofs := 0 *}
42063 a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	24
a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	25	ML {*
a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	26	fun SOLVE_TIMEOUT seconds name tac st =
a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	27	let
a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	28	val result =
a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	29	TimeLimit.timeLimit (Time.fromSeconds seconds)
a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	30	(fn () => SINGLE (SOLVE tac) st) ()
a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	31	handle TimeLimit.TimeOut => NONE
a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	32	\| ERROR _ => NONE
a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	33	in
a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	34	(case result of
42213 bac7733a13c9 use the proper contexts/simpsets/etc. in the TPTP proof method blanchet parents: 42211 diff changeset	35	NONE => (warning ("FAILURE: " ^ name); Seq.empty)
bac7733a13c9 use the proper contexts/simpsets/etc. in the TPTP proof method blanchet parents: 42211 diff changeset	36	\| SOME st' => (warning ("SUCCESS: " ^ name); Seq.single st'))
42063 a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	37	end
a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	38	*}
a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	39
a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	40	ML {*
42800 df2dc9406287 just one universal Proof.context -- discontinued claset/clasimpset; wenzelm parents: 42601 diff changeset	41	fun isabellep_tac ctxt max_secs =
42213 bac7733a13c9 use the proper contexts/simpsets/etc. in the TPTP proof method blanchet parents: 42211 diff changeset	42	SOLVE_TIMEOUT (max_secs div 10) "smt" (ALLGOALS (SMT_Solver.smt_tac ctxt []))
42063 a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	43	ORELSE
42213 bac7733a13c9 use the proper contexts/simpsets/etc. in the TPTP proof method blanchet parents: 42211 diff changeset	44	SOLVE_TIMEOUT (max_secs div 5) "sledgehammer"
bac7733a13c9 use the proper contexts/simpsets/etc. in the TPTP proof method blanchet parents: 42211 diff changeset	45	(ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
42063 a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	46	ORELSE
42800 df2dc9406287 just one universal Proof.context -- discontinued claset/clasimpset; wenzelm parents: 42601 diff changeset	47	SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac (simpset_of ctxt)))
42213 bac7733a13c9 use the proper contexts/simpsets/etc. in the TPTP proof method blanchet parents: 42211 diff changeset	48	ORELSE
42800 df2dc9406287 just one universal Proof.context -- discontinued claset/clasimpset; wenzelm parents: 42601 diff changeset	49	SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac ctxt))
42063 a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	50	ORELSE
42800 df2dc9406287 just one universal Proof.context -- discontinued claset/clasimpset; wenzelm parents: 42601 diff changeset	51	SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt
42213 bac7733a13c9 use the proper contexts/simpsets/etc. in the TPTP proof method blanchet parents: 42211 diff changeset	52	THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
42063 a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	53	ORELSE
43205 23b81469499f more preparations towards hijacking Metis blanchet parents: 43161 diff changeset	54	SOLVE_TIMEOUT (max_secs div 10) "metis"
43212 050a03afe024 Metis code cleanup blanchet parents: 43211 diff changeset	55	(ALLGOALS (Metis_Tactics.metis_tac [] ctxt []))
42063 a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	56	ORELSE
42800 df2dc9406287 just one universal Proof.context -- discontinued claset/clasimpset; wenzelm parents: 42601 diff changeset	57	SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt))
42063 a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	58	ORELSE
42800 df2dc9406287 just one universal Proof.context -- discontinued claset/clasimpset; wenzelm parents: 42601 diff changeset	59	SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac ctxt))
42063 a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	60	ORELSE
42800 df2dc9406287 just one universal Proof.context -- discontinued claset/clasimpset; wenzelm parents: 42601 diff changeset	61	SOLVE_TIMEOUT (max_secs div 10) "force" (ALLGOALS (force_tac ctxt))
42063 a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	62	ORELSE
42800 df2dc9406287 just one universal Proof.context -- discontinued claset/clasimpset; wenzelm parents: 42601 diff changeset	63	SOLVE_TIMEOUT max_secs "fastsimp" (ALLGOALS (fast_simp_tac ctxt))
42063 a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	64	*}
a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	65
42827 8bfdcaf30551 provide isabellep as a method blanchet parents: 42800 diff changeset	66	method_setup isabellep = {*
43161 27dcda8fc89b tuned CASC method blanchet parents: 42827 diff changeset	67	Scan.lift (Scan.optional Parse.nat 1) >>
42827 8bfdcaf30551 provide isabellep as a method blanchet parents: 42800 diff changeset	68	(fn m => fn ctxt => SIMPLE_METHOD (isabellep_tac ctxt m))
43161 27dcda8fc89b tuned CASC method blanchet parents: 42827 diff changeset	69	*} "combination of Isabelle provers and oracles for CASC"
42827 8bfdcaf30551 provide isabellep as a method blanchet parents: 42800 diff changeset	70
42063 a2a69b32d899 added "TPTP" theory with IsabelleP tactic, so that it is maintained alongside with Isabelle and that the CASC version of Isabelle is provided by Isabelle itself instead of being stored on the TPTP servers blanchet parents: diff changeset	71	end

author	wenzelm
	Sat, 09 Jul 2011 21:53:27 +0200
changeset 43721	fad8634cee62
parent 43212	050a03afe024
permissions	-rw-r--r--