isabelle: src/HOL/ATP.thy@78211f66cf8d (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
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	42
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	43	subsection {* Setup *}
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	44
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	45	use "Tools/ATP/atp_translate.ML"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	46	use "Tools/ATP/atp_reconstruct.ML"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	47
39951 ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	48	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	49
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	50	end

author	wenzelm
	Wed, 29 Jun 2011 20:39:41 +0200
changeset 43596	78211f66cf8d
parent 43108	eb1e31eb7449
child 43678	56d352659500
permissions	-rw-r--r--