isabelle: src/HOL/ATP.thy@df1369a42393 (annotated)

39951 ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	1	(* Title: HOL/ATP.thy
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	2	Author: Fabian Immler, TU Muenchen
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	3	Author: Jasmin Blanchette, TU Muenchen
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	4	*)
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	5
39958 88c9aa5666de tuned comments blanchet parents: 39951 diff changeset	6	header {* Automatic Theorem Provers (ATPs) *}
39951 ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	7
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	8	theory ATP
43085 0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	9	imports Meson
44087 8e491cb8841c load lambda-lifting structure earlier, so it can be used in Metis blanchet parents: 43678 diff changeset	10	uses "Tools/lambda_lifting.ML"
8e491cb8841c load lambda-lifting structure earlier, so it can be used in Metis blanchet parents: 43678 diff changeset	11	"Tools/monomorph.ML"
43108 eb1e31eb7449 use "monomorph.ML" in "ATP" theory (so the new Metis can use it) blanchet parents: 43085 diff changeset	12	"Tools/ATP/atp_util.ML"
43085 0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	13	"Tools/ATP/atp_problem.ML"
40178 00152d17855b reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers blanchet parents: 40121 diff changeset	14	"Tools/ATP/atp_proof.ML"
45877 b18f62e40429 added new proof redirection code blanchet parents: 45522 diff changeset	15	"Tools/ATP/atp_redirect.ML"
43085 0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	16	("Tools/ATP/atp_translate.ML")
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	17	("Tools/ATP/atp_reconstruct.ML")
45522 3b951bbd2bee compile blanchet parents: 44087 diff changeset	18	("Tools/ATP/atp_systems.ML")
39951 ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	19	begin
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	20
43085 0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	21	subsection {* Higher-order reasoning helpers *}
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	22
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	23	definition fFalse :: bool where [no_atp]:
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	24	"fFalse \<longleftrightarrow> False"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	25
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	26	definition fTrue :: bool where [no_atp]:
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	27	"fTrue \<longleftrightarrow> True"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	28
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	29	definition fNot :: "bool \<Rightarrow> bool" where [no_atp]:
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	30	"fNot P \<longleftrightarrow> \<not> P"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	31
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	32	definition fconj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	33	"fconj P Q \<longleftrightarrow> P \<and> Q"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	34
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	35	definition fdisj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	36	"fdisj P Q \<longleftrightarrow> P \<or> Q"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	37
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	38	definition fimplies :: "bool \<Rightarrow> bool \<Rightarrow> bool" where [no_atp]:
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	39	"fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	40
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	41	definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	42	"fequal x y \<longleftrightarrow> (x = y)"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	43
43678 56d352659500 improved translation of lambdas in THF nik parents: 43108 diff changeset	44	definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
56d352659500 improved translation of lambdas in THF nik parents: 43108 diff changeset	45	"fAll P \<longleftrightarrow> All P"
56d352659500 improved translation of lambdas in THF nik parents: 43108 diff changeset	46
56d352659500 improved translation of lambdas in THF nik parents: 43108 diff changeset	47	definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
56d352659500 improved translation of lambdas in THF nik parents: 43108 diff changeset	48	"fEx P \<longleftrightarrow> Ex P"
43085 0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	49
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	50	subsection {* Setup *}
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	51
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	52	use "Tools/ATP/atp_translate.ML"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	53	use "Tools/ATP/atp_reconstruct.ML"
45522 3b951bbd2bee compile blanchet parents: 44087 diff changeset	54	use "Tools/ATP/atp_systems.ML"
43085 0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	55
39951 ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	56	setup ATP_Systems.setup
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	57
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	58	end

author	wenzelm
	Sat, 14 Jan 2012 12:36:43 +0100
changeset 46204	df1369a42393
parent 45877	b18f62e40429
child 46320	0b8b73b49848
permissions	-rw-r--r--