isabelle: src/HOL/Sledgehammer.thy@ae4dc5ac983f (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
75029 dc6769b86fd6 crude implementation of centralized slicing blanchet parents: 73684 diff changeset	38	(*
dc6769b86fd6 crude implementation of centralized slicing blanchet parents: 73684 diff changeset	39	lemma "1 + 1 = 2 \<and> 0 + (x::nat) = x"
75031 ae4dc5ac983f implemented 'max_proofs' mechanism blanchet parents: 75030 diff changeset	40	sledgehammer [max_proofs = 3]
75030 919fb49ba201 document new option 'max_proofs' blanchet parents: 75029 diff changeset	41	oops
75029 dc6769b86fd6 crude implementation of centralized slicing blanchet parents: 73684 diff changeset	42	*)
dc6769b86fd6 crude implementation of centralized slicing blanchet parents: 73684 diff changeset	43
dc6769b86fd6 crude implementation of centralized slicing blanchet parents: 73684 diff changeset	44	(*
dc6769b86fd6 crude implementation of centralized slicing blanchet parents: 73684 diff changeset	45	declare nat_induct[no_atp]
dc6769b86fd6 crude implementation of centralized slicing blanchet parents: 73684 diff changeset	46	declare nat_induct_non_zero[no_atp]
dc6769b86fd6 crude implementation of centralized slicing blanchet parents: 73684 diff changeset	47
dc6769b86fd6 crude implementation of centralized slicing blanchet parents: 73684 diff changeset	48	lemma "P 0 \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (Suc n)) \<Longrightarrow> P n"
dc6769b86fd6 crude implementation of centralized slicing blanchet parents: 73684 diff changeset	49	sledgehammer [cvc4] (add: nat.induct)
dc6769b86fd6 crude implementation of centralized slicing blanchet parents: 73684 diff changeset	50	*)
dc6769b86fd6 crude implementation of centralized slicing blanchet parents: 73684 diff changeset	51
dc6769b86fd6 crude implementation of centralized slicing blanchet parents: 73684 diff changeset	52	(*
dc6769b86fd6 crude implementation of centralized slicing blanchet parents: 73684 diff changeset	53	lemma "1 + 1 = 2 \<and> 0 + (x::nat) = x"
dc6769b86fd6 crude implementation of centralized slicing blanchet parents: 73684 diff changeset	54	sledgehammer [verbose, e, dont_preplay, max_facts = 2] (add_0_left one_add_one)
dc6769b86fd6 crude implementation of centralized slicing blanchet parents: 73684 diff changeset	55	*)
dc6769b86fd6 crude implementation of centralized slicing blanchet parents: 73684 diff changeset	56
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	57	end

author	blanchet
	Mon, 31 Jan 2022 16:09:23 +0100
changeset 75031	ae4dc5ac983f
parent 75030	919fb49ba201
child 75032	8d08bc7e8f98
permissions	-rw-r--r--