isabelle: src/HOL/Sledgehammer.thy@dca8d06ecbba (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
57231 dca8d06ecbba reduces Sledgehammer dependencies blanchet parents: 57215 diff changeset	10	imports Presburger ATP SMT2
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
57215 6fc0e3d4e1e5 moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle blanchet parents: 57208 diff changeset	17	(* Has all needed simplification lemmas for logic.
6fc0e3d4e1e5 moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle blanchet parents: 57208 diff changeset	18	"HOL.simp_thms(35-42)" are about \<exists> and \<forall>. These lemmas are left out for now. *)
6fc0e3d4e1e5 moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle blanchet parents: 57208 diff changeset	19	lemmas waldmeister_fol = simp_thms(1-34) disj_absorb disj_left_absorb conj_absorb conj_left_absorb
6fc0e3d4e1e5 moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle blanchet parents: 57208 diff changeset	20	eq_ac disj_comms disj_assoc conj_comms conj_assoc
6fc0e3d4e1e5 moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle blanchet parents: 57208 diff changeset	21
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	22	ML_file "Tools/Sledgehammer/async_manager.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	23	ML_file "Tools/Sledgehammer/sledgehammer_util.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	24	ML_file "Tools/Sledgehammer/sledgehammer_fact.ML"
55287 ffa306239316 renamed ML file blanchet parents: 55267 diff changeset	25	ML_file "Tools/Sledgehammer/sledgehammer_proof_methods.ML"
55211 5d027af93a08 moved ML code around blanchet parents: 55205 diff changeset	26	ML_file "Tools/Sledgehammer/sledgehammer_isar_annotate.ML"
55202 824c48a539c9 renamed many Sledgehammer ML files to clarify structure blanchet parents: 55201 diff changeset	27	ML_file "Tools/Sledgehammer/sledgehammer_isar_proof.ML"
824c48a539c9 renamed many Sledgehammer ML files to clarify structure blanchet parents: 55201 diff changeset	28	ML_file "Tools/Sledgehammer/sledgehammer_isar_preplay.ML"
824c48a539c9 renamed many Sledgehammer ML files to clarify structure blanchet parents: 55201 diff changeset	29	ML_file "Tools/Sledgehammer/sledgehammer_isar_compress.ML"
824c48a539c9 renamed many Sledgehammer ML files to clarify structure blanchet parents: 55201 diff changeset	30	ML_file "Tools/Sledgehammer/sledgehammer_isar_minimize.ML"
824c48a539c9 renamed many Sledgehammer ML files to clarify structure blanchet parents: 55201 diff changeset	31	ML_file "Tools/Sledgehammer/sledgehammer_isar.ML"
55201 1ee776da8da7 renamed ML file blanchet parents: 55198 diff changeset	32	ML_file "Tools/Sledgehammer/sledgehammer_prover.ML"
55205 8450622db0c5 refactor large ML file blanchet parents: 55202 diff changeset	33	ML_file "Tools/Sledgehammer/sledgehammer_prover_atp.ML"
56081 72fad75baf7e integrate SMT2 with Sledgehammer blanchet parents: 56078 diff changeset	34	ML_file "Tools/Sledgehammer/sledgehammer_prover_smt2.ML"
57215 6fc0e3d4e1e5 moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle blanchet parents: 57208 diff changeset	35	ML_file "Tools/Sledgehammer/sledgehammer_prover_waldmeister.ML"
55202 824c48a539c9 renamed many Sledgehammer ML files to clarify structure blanchet parents: 55201 diff changeset	36	ML_file "Tools/Sledgehammer/sledgehammer_prover_minimize.ML"
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	37	ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	38	ML_file "Tools/Sledgehammer/sledgehammer_mash.ML"
55202 824c48a539c9 renamed many Sledgehammer ML files to clarify structure blanchet parents: 55201 diff changeset	39	ML_file "Tools/Sledgehammer/sledgehammer.ML"
55198 7a538e58b64e tuned ML file name blanchet parents: 54838 diff changeset	40	ML_file "Tools/Sledgehammer/sledgehammer_commands.ML"
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	41
57215 6fc0e3d4e1e5 moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle blanchet parents: 57208 diff changeset	42	hide_fact (open) waldmeister_fol
6fc0e3d4e1e5 moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle blanchet parents: 57208 diff changeset	43
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	44	end

author	blanchet
	Thu, 12 Jun 2014 01:00:49 +0200
changeset 57231	dca8d06ecbba
parent 57215	6fc0e3d4e1e5
child 57242	25aff3b8d550
permissions	-rw-r--r--