isabelle: src/HOL/ATP.thy@a89b4bc311a5 (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"
43085 0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	15	("Tools/ATP/atp_translate.ML")
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	16	("Tools/ATP/atp_reconstruct.ML")
45522 3b951bbd2bee compile blanchet parents: 44087 diff changeset	17	("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	18	begin
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	19
43085 0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	20	subsection {* Higher-order reasoning helpers *}
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	21
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	22	definition fFalse :: bool where [no_atp]:
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	23	"fFalse \<longleftrightarrow> False"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	24
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	25	definition fTrue :: bool where [no_atp]:
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	26	"fTrue \<longleftrightarrow> True"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	27
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	28	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	29	"fNot P \<longleftrightarrow> \<not> P"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	30
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	31	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	32	"fconj P Q \<longleftrightarrow> P \<and> Q"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	33
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	34	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	35	"fdisj P Q \<longleftrightarrow> P \<or> Q"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	36
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	37	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	38	"fimplies P Q \<longleftrightarrow> (P \<longrightarrow> Q)"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	39
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	40	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	41	"fequal x y \<longleftrightarrow> (x = y)"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	42
43678 56d352659500 improved translation of lambdas in THF nik parents: 43108 diff changeset	43	definition fAll :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
56d352659500 improved translation of lambdas in THF nik parents: 43108 diff changeset	44	"fAll P \<longleftrightarrow> All P"
56d352659500 improved translation of lambdas in THF nik parents: 43108 diff changeset	45
56d352659500 improved translation of lambdas in THF nik parents: 43108 diff changeset	46	definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
56d352659500 improved translation of lambdas in THF nik parents: 43108 diff changeset	47	"fEx P \<longleftrightarrow> Ex P"
43085 0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	48
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	49	subsection {* Setup *}
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	50
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	51	use "Tools/ATP/atp_translate.ML"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	52	use "Tools/ATP/atp_reconstruct.ML"
45522 3b951bbd2bee compile blanchet parents: 44087 diff changeset	53	use "Tools/ATP/atp_systems.ML"
43085 0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	54
39951 ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	55	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	56
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	57	end

author	wenzelm
	Sun, 20 Nov 2011 21:05:23 +0100
changeset 45605	a89b4bc311a5
parent 45522	3b951bbd2bee
child 45877	b18f62e40429
permissions	-rw-r--r--