isabelle: src/HOL/Sledgehammer.thy@7c25451ae2c1 (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
60758 d8d85a8172b5 isabelle update_cartouches; wenzelm parents: 59471 diff changeset	7	section \<open>Sledgehammer: Isabelle--ATP Linkup\<close>
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
58061 3d060f43accb renamed new SMT module from 'SMT2' to 'SMT' blanchet parents: 57266 diff changeset	10	imports Presburger SMT
63432 ba7901e94e7b tuned; wenzelm parents: 60758 diff changeset	11	keywords
ba7901e94e7b tuned; wenzelm parents: 60758 diff changeset	12	"sledgehammer" :: diag and
ba7901e94e7b tuned; wenzelm parents: 60758 diff changeset	13	"sledgehammer_params" :: thy_decl
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	14	begin
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	15
73418 7d7d959547a1 support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl); wenzelm parents: 72593 diff changeset	16	ML_file \<open>Tools/ATP/system_on_tptp.ML\<close>
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	17	ML_file \<open>Tools/Sledgehammer/async_manager_legacy.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	18	ML_file \<open>Tools/Sledgehammer/sledgehammer_util.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	19	ML_file \<open>Tools/Sledgehammer/sledgehammer_fact.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	20	ML_file \<open>Tools/Sledgehammer/sledgehammer_proof_methods.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	21	ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_annotate.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	22	ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_proof.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	23	ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_preplay.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	24	ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_compress.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	25	ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_minimize.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	26	ML_file \<open>Tools/Sledgehammer/sledgehammer_isar.ML\<close>
72400 abfeed05c323 tune filename desharna parents: 72342 diff changeset	27	ML_file \<open>Tools/Sledgehammer/sledgehammer_atp_systems.ML\<close>
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	28	ML_file \<open>Tools/Sledgehammer/sledgehammer_prover.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	29	ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_atp.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	30	ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_smt.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	31	ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_minimize.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	32	ML_file \<open>Tools/Sledgehammer/sledgehammer_mepo.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	33	ML_file \<open>Tools/Sledgehammer/sledgehammer_mash.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	34	ML_file \<open>Tools/Sledgehammer/sledgehammer.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63432 diff changeset	35	ML_file \<open>Tools/Sledgehammer/sledgehammer_commands.ML\<close>
73684 a63d76ba0a03 avoid duplicate loading of ML file; wenzelm parents: 73418 diff changeset	36	ML_file \<open>Tools/Sledgehammer/sledgehammer_tactics.ML\<close>
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48380 diff changeset	37
77602 7c25451ae2c1 use simplifier to classify the missing assumptions in Sledgehammer's abduction mechanism blanchet parents: 75341 diff changeset	38	(*
7c25451ae2c1 use simplifier to classify the missing assumptions in Sledgehammer's abduction mechanism blanchet parents: 75341 diff changeset	39	lemma "x - y + y = (x::nat)"
7c25451ae2c1 use simplifier to classify the missing assumptions in Sledgehammer's abduction mechanism blanchet parents: 75341 diff changeset	40	sledgehammer[e, abduce = 10]
7c25451ae2c1 use simplifier to classify the missing assumptions in Sledgehammer's abduction mechanism blanchet parents: 75341 diff changeset	41	oops
7c25451ae2c1 use simplifier to classify the missing assumptions in Sledgehammer's abduction mechanism blanchet parents: 75341 diff changeset	42	*)
7c25451ae2c1 use simplifier to classify the missing assumptions in Sledgehammer's abduction mechanism blanchet parents: 75341 diff changeset	43
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	44	end

author	blanchet
	Fri, 10 Mar 2023 15:27:18 +0100
changeset 77602	7c25451ae2c1
parent 75341	72cbbb4d98f3
child 77670	b9e9b818d7b0
permissions	-rw-r--r--