isabelle: src/HOL/Sledgehammer.thy@2df6ad1dbd66 (annotated)

35827 f552152d7747 renamed "ATP_Linkup" theory to "Sledgehammer" blanchet parents: 35826 diff changeset	1	(* Title: HOL/Sledgehammer.thy
38027 505657ddb047 standardize "Author" tags blanchet parents: 38025 diff changeset	2	Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
38028 22dcaec5fa77 minor refactoring blanchet parents: 38027 diff changeset	3	Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
35865 2f8fb5242799 more Sledgehammer refactoring blanchet parents: 35827 diff changeset	4	Author: Jasmin Blanchette, TU Muenchen
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	5	*)
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	6
35827 f552152d7747 renamed "ATP_Linkup" theory to "Sledgehammer" blanchet parents: 35826 diff changeset	7	header {* Sledgehammer: Isabelle--ATP Linkup *}
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	8
35827 f552152d7747 renamed "ATP_Linkup" theory to "Sledgehammer" blanchet parents: 35826 diff changeset	9	theory Sledgehammer
40181 3788b7adab36 integrated "smt" proof method with Sledgehammer blanchet parents: 40178 diff changeset	10	imports ATP SMT
46950 d0181abdbdac declare command keywords via theory header, including strict checking outside Pure; wenzelm parents: 43085 diff changeset	11	keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	12	begin
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	13
54838 16511f84913c reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated) blanchet parents: 52641 diff changeset	14	lemma size_ne_size_imp_ne: "size x \<noteq> size y \<Longrightarrow> x \<noteq> y"
16511f84913c reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated) blanchet parents: 52641 diff changeset	15	by (erule contrapos_nn) (rule arg_cong)
16511f84913c reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated) blanchet parents: 52641 diff changeset	16
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	17	ML_file "Tools/Sledgehammer/async_manager.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	18	ML_file "Tools/Sledgehammer/sledgehammer_util.ML"
52555 6811291d1869 moved code -> easier debugging smolkas parents: 51179 diff changeset	19	ML_file "Tools/Sledgehammer/sledgehammer_annotate.ML"
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	20	ML_file "Tools/Sledgehammer/sledgehammer_fact.ML"
52555 6811291d1869 moved code -> easier debugging smolkas parents: 51179 diff changeset	21	ML_file "Tools/Sledgehammer/sledgehammer_reconstructor.ML"
50264 a9ec48b98734 renamed sledgehammer_isar_reconstruct to sledgehammer_proof smolkas parents: 50259 diff changeset	22	ML_file "Tools/Sledgehammer/sledgehammer_proof.ML"
52555 6811291d1869 moved code -> easier debugging smolkas parents: 51179 diff changeset	23	ML_file "Tools/Sledgehammer/sledgehammer_print.ML"
50923 141d8f575f6f move preplaying to own structure smolkas parents: 50264 diff changeset	24	ML_file "Tools/Sledgehammer/sledgehammer_preplay.ML"
51130 76d68444cd59 renamed sledgehammer_shrink to sledgehammer_compress smolkas parents: 50923 diff changeset	25	ML_file "Tools/Sledgehammer/sledgehammer_compress.ML"
52592 8a25b17e3d79 optimize isar-proofs by trying different proof methods smolkas parents: 52555 diff changeset	26	ML_file "Tools/Sledgehammer/sledgehammer_try0.ML"
52611 831f7479c74f minimize dependencies (used facts) of Isar proof steps; remove unreferenced steps smolkas parents: 52592 diff changeset	27	ML_file "Tools/Sledgehammer/sledgehammer_minimize_isar.ML"
51179 0d5f8812856f split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations smolkas parents: 51178 diff changeset	28	ML_file "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	29	ML_file "Tools/Sledgehammer/sledgehammer_provers.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	30	ML_file "Tools/Sledgehammer/sledgehammer_minimize.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	31	ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	32	ML_file "Tools/Sledgehammer/sledgehammer_mash.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	33	ML_file "Tools/Sledgehammer/sledgehammer_run.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	34	ML_file "Tools/Sledgehammer/sledgehammer_isar.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	35
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	36	end

author	blanchet
	Thu, 16 Jan 2014 16:20:17 +0100
changeset 55017	2df6ad1dbd66
parent 54838	16511f84913c
child 55198	7a538e58b64e
permissions	-rw-r--r--