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

author	wenzelm
	Mon, 11 Jul 2011 17:14:30 +0200
changeset 43751	8c7f69f1825b
parent 43678	56d352659500
child 44087	8e491cb8841c
permissions	-rw-r--r--