isabelle: src/HOL/ATP.thy@0a2f5b86bdd7 (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
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	10	uses "Tools/ATP/atp_util.ML"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	11	"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	12	"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	13	"Tools/ATP/atp_systems.ML"
43085 0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	14	("Tools/ATP/atp_translate.ML")
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	15	("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	16	begin
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	17
43085 0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	18	subsection {* Higher-order reasoning helpers *}
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	19
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	20	definition fFalse :: bool where [no_atp]:
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	21	"fFalse \<longleftrightarrow> False"
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 fTrue :: bool where [no_atp]:
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	24	"fTrue \<longleftrightarrow> True"
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 fNot :: "bool \<Rightarrow> bool" where [no_atp]:
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	27	"fNot P \<longleftrightarrow> \<not> P"
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 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	30	"fconj P Q \<longleftrightarrow> P \<and> Q"
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 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	33	"fdisj P Q \<longleftrightarrow> P \<or> 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 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	36	"fimplies P Q \<longleftrightarrow> (P \<longrightarrow> 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 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	39	"fequal x y \<longleftrightarrow> (x = y)"
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
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	42	subsection {* Setup *}
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	43
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	44	use "Tools/ATP/atp_translate.ML"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	45	use "Tools/ATP/atp_reconstruct.ML"
0a2f5b86bdd7 first step in sharing more code between ATP and Metis translation blanchet parents: 40178 diff changeset	46
39951 ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	47	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	48
ff60a6e4edfe factor out "ATP" from "Sledgehammer" (cf. "SAT" vs. "Refute", etc.) -- the theories now reflect the directory structure blanchet parents: diff changeset	49	end

author	blanchet
	Tue, 31 May 2011 16:38:36 +0200
changeset 43085	0a2f5b86bdd7
parent 40178	00152d17855b
child 43108	eb1e31eb7449
permissions	-rw-r--r--