isabelle: src/HOL/Sledgehammer.thy@80420a0f2179 (annotated)

35827 f552152d7747 renamed "ATP_Linkup" theory to "Sledgehammer" blanchet parents: 35826 diff changeset	1	(* Title: HOL/Sledgehammer.thy
38027 505657ddb047 standardize "Author" tags blanchet parents: 38025 diff changeset	2	Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
38028 22dcaec5fa77 minor refactoring blanchet parents: 38027 diff changeset	3	Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
35865 2f8fb5242799 more Sledgehammer refactoring blanchet parents: 35827 diff changeset	4	Author: Fabian Immler, TU Muenchen
2f8fb5242799 more Sledgehammer refactoring blanchet parents: 35827 diff changeset	5	Author: Jasmin Blanchette, TU Muenchen
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	6	*)
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	7
35827 f552152d7747 renamed "ATP_Linkup" theory to "Sledgehammer" blanchet parents: 35826 diff changeset	8	header {* Sledgehammer: Isabelle--ATP Linkup *}
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	9
35827 f552152d7747 renamed "ATP_Linkup" theory to "Sledgehammer" blanchet parents: 35826 diff changeset	10	theory Sledgehammer
33593 ef54e2108b74 tuned imports haftmann parents: 33316 diff changeset	11	imports Plain Hilbert_Choice
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	12	uses
38047 9033c03cc214 consequence of directory renaming blanchet parents: 38028 diff changeset	13	("Tools/ATP/atp_problem.ML")
9033c03cc214 consequence of directory renaming blanchet parents: 38028 diff changeset	14	("Tools/ATP/atp_systems.ML")
38025 b660597a6796 reorder ML files in theory blanchet parents: 38023 diff changeset	15	("~~/src/Tools/Metis/metis.ML")
37574 b8c1f4c46983 renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier"; blanchet parents: 37571 diff changeset	16	("Tools/Sledgehammer/clausifier.ML")
37569 931f5948a32d move "MESON" up; blanchet parents: 37541 diff changeset	17	("Tools/Sledgehammer/meson_tactic.ML")
37578 9367cb36b1c4 renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer blanchet parents: 37577 diff changeset	18	("Tools/Sledgehammer/metis_clauses.ML")
9367cb36b1c4 renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer blanchet parents: 37577 diff changeset	19	("Tools/Sledgehammer/metis_tactics.ML")
37571 76e23303c7ff more moving around of ML files in "Sledgehammer.thy" blanchet parents: 37569 diff changeset	20	("Tools/Sledgehammer/sledgehammer_util.ML")
38988 483879af0643 finished renaming blanchet parents: 38606 diff changeset	21	("Tools/Sledgehammer/sledgehammer_filter.ML")
38282 319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML) blanchet parents: 38047 diff changeset	22	("Tools/Sledgehammer/sledgehammer_translate.ML")
38988 483879af0643 finished renaming blanchet parents: 38606 diff changeset	23	("Tools/Sledgehammer/sledgehammer_reconstruct.ML")
38023 962b0a7f544b more refactoring blanchet parents: 38021 diff changeset	24	("Tools/Sledgehammer/sledgehammer.ML")
38988 483879af0643 finished renaming blanchet parents: 38606 diff changeset	25	("Tools/Sledgehammer/sledgehammer_minimize.ML")
35866 513074557e06 move the Sledgehammer Isar commands together into one file; blanchet parents: 35865 diff changeset	26	("Tools/Sledgehammer/sledgehammer_isar.ML")
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	27	begin
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	28
39036 dff91b90d74c use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd; blanchet parents: 38990 diff changeset	29	lemma TruepropI: "P \<equiv> Q \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
dff91b90d74c use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd; blanchet parents: 38990 diff changeset	30	by simp
dff91b90d74c use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd; blanchet parents: 38990 diff changeset	31
37410 2bf7e6136047 adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf" blanchet parents: 37399 diff changeset	32	definition skolem_id :: "'a \<Rightarrow> 'a" where
2bf7e6136047 adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf" blanchet parents: 37399 diff changeset	33	[no_atp]: "skolem_id = (\<lambda>x. x)"
37399 34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter blanchet parents: 36569 diff changeset	34
36569 3a29eb7606c3 added "no_atp" for theorems that are automatically used or included by Sledgehammer when appropriate (about combinators and fequal) blanchet parents: 36394 diff changeset	35	definition COMBI :: "'a \<Rightarrow> 'a" where
38606 3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed blanchet parents: 38282 diff changeset	36	[no_atp]: "COMBI P = P"
24819 7d8e0a47392e modernized definitions; wenzelm parents: 24742 diff changeset	37
36569 3a29eb7606c3 added "no_atp" for theorems that are automatically used or included by Sledgehammer when appropriate (about combinators and fequal) blanchet parents: 36394 diff changeset	38	definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" where
38606 3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed blanchet parents: 38282 diff changeset	39	[no_atp]: "COMBK P Q = P"
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	40
36569 3a29eb7606c3 added "no_atp" for theorems that are automatically used or included by Sledgehammer when appropriate (about combinators and fequal) blanchet parents: 36394 diff changeset	41	definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where [no_atp]:
38606 3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed blanchet parents: 38282 diff changeset	42	"COMBB P Q R = P (Q R)"
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	43
36569 3a29eb7606c3 added "no_atp" for theorems that are automatically used or included by Sledgehammer when appropriate (about combinators and fequal) blanchet parents: 36394 diff changeset	44	definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
38606 3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed blanchet parents: 38282 diff changeset	45	[no_atp]: "COMBC P Q R = P R Q"
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	46
36569 3a29eb7606c3 added "no_atp" for theorems that are automatically used or included by Sledgehammer when appropriate (about combinators and fequal) blanchet parents: 36394 diff changeset	47	definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where
38606 3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed blanchet parents: 38282 diff changeset	48	[no_atp]: "COMBS P Q R = P R (Q R)"
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	49
36569 3a29eb7606c3 added "no_atp" for theorems that are automatically used or included by Sledgehammer when appropriate (about combinators and fequal) blanchet parents: 36394 diff changeset	50	definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
38606 3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed blanchet parents: 38282 diff changeset	51	"fequal X Y \<longleftrightarrow> (X = Y)"
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed blanchet parents: 38282 diff changeset	52
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed blanchet parents: 38282 diff changeset	53	lemma fequal_imp_equal [no_atp]: "\<not> fequal X Y \<or> X = Y"
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed blanchet parents: 38282 diff changeset	54	by (simp add: fequal_def)
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	55
38606 3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed blanchet parents: 38282 diff changeset	56	lemma equal_imp_fequal [no_atp]: "\<not> X = Y \<or> fequal X Y"
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed blanchet parents: 38282 diff changeset	57	by (simp add: fequal_def)
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	58
38606 3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed blanchet parents: 38282 diff changeset	59	lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y"
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed blanchet parents: 38282 diff changeset	60	by auto
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	61
24827 646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	62	text{Theorems for translation to combinators}
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	63
36569 3a29eb7606c3 added "no_atp" for theorems that are automatically used or included by Sledgehammer when appropriate (about combinators and fequal) blanchet parents: 36394 diff changeset	64	lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
24827 646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	65	apply (rule eq_reflection)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	66	apply (rule ext)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	67	apply (simp add: COMBS_def)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	68	done
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	69
36569 3a29eb7606c3 added "no_atp" for theorems that are automatically used or included by Sledgehammer when appropriate (about combinators and fequal) blanchet parents: 36394 diff changeset	70	lemma abs_I [no_atp]: "\<lambda>x. x \<equiv> COMBI"
24827 646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	71	apply (rule eq_reflection)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	72	apply (rule ext)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	73	apply (simp add: COMBI_def)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	74	done
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	75
36569 3a29eb7606c3 added "no_atp" for theorems that are automatically used or included by Sledgehammer when appropriate (about combinators and fequal) blanchet parents: 36394 diff changeset	76	lemma abs_K [no_atp]: "\<lambda>x. y \<equiv> COMBK y"
24827 646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	77	apply (rule eq_reflection)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	78	apply (rule ext)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	79	apply (simp add: COMBK_def)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	80	done
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	81
36569 3a29eb7606c3 added "no_atp" for theorems that are automatically used or included by Sledgehammer when appropriate (about combinators and fequal) blanchet parents: 36394 diff changeset	82	lemma abs_B [no_atp]: "\<lambda>x. a (g x) \<equiv> COMBB a g"
24827 646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	83	apply (rule eq_reflection)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	84	apply (rule ext)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	85	apply (simp add: COMBB_def)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	86	done
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	87
36569 3a29eb7606c3 added "no_atp" for theorems that are automatically used or included by Sledgehammer when appropriate (about combinators and fequal) blanchet parents: 36394 diff changeset	88	lemma abs_C [no_atp]: "\<lambda>x. (f x) b \<equiv> COMBC f b"
24827 646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	89	apply (rule eq_reflection)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	90	apply (rule ext)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	91	apply (simp add: COMBC_def)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	92	done
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	93
38047 9033c03cc214 consequence of directory renaming blanchet parents: 38028 diff changeset	94	use "Tools/ATP/atp_problem.ML"
9033c03cc214 consequence of directory renaming blanchet parents: 38028 diff changeset	95	use "Tools/ATP/atp_systems.ML"
38025 b660597a6796 reorder ML files in theory blanchet parents: 38023 diff changeset	96	setup ATP_Systems.setup
b660597a6796 reorder ML files in theory blanchet parents: 38023 diff changeset	97
b660597a6796 reorder ML files in theory blanchet parents: 38023 diff changeset	98	use "~~/src/Tools/Metis/metis.ML"
37574 b8c1f4c46983 renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier"; blanchet parents: 37571 diff changeset	99	use "Tools/Sledgehammer/clausifier.ML"
37569 931f5948a32d move "MESON" up; blanchet parents: 37541 diff changeset	100	use "Tools/Sledgehammer/meson_tactic.ML"
931f5948a32d move "MESON" up; blanchet parents: 37541 diff changeset	101	setup Meson_Tactic.setup
37571 76e23303c7ff more moving around of ML files in "Sledgehammer.thy" blanchet parents: 37569 diff changeset	102
37578 9367cb36b1c4 renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer blanchet parents: 37577 diff changeset	103	use "Tools/Sledgehammer/metis_clauses.ML"
9367cb36b1c4 renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer blanchet parents: 37577 diff changeset	104	use "Tools/Sledgehammer/metis_tactics.ML"
39322 80420a0f2179 setup Auto Sledgehammer blanchet parents: 39036 diff changeset	105	setup Metis_Tactics.setup
37578 9367cb36b1c4 renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer blanchet parents: 37577 diff changeset	106
37571 76e23303c7ff more moving around of ML files in "Sledgehammer.thy" blanchet parents: 37569 diff changeset	107	use "Tools/Sledgehammer/sledgehammer_util.ML"
38988 483879af0643 finished renaming blanchet parents: 38606 diff changeset	108	use "Tools/Sledgehammer/sledgehammer_filter.ML"
38282 319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML) blanchet parents: 38047 diff changeset	109	use "Tools/Sledgehammer/sledgehammer_translate.ML"
38988 483879af0643 finished renaming blanchet parents: 38606 diff changeset	110	use "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
38023 962b0a7f544b more refactoring blanchet parents: 38021 diff changeset	111	use "Tools/Sledgehammer/sledgehammer.ML"
962b0a7f544b more refactoring blanchet parents: 38021 diff changeset	112	setup Sledgehammer.setup
38988 483879af0643 finished renaming blanchet parents: 38606 diff changeset	113	use "Tools/Sledgehammer/sledgehammer_minimize.ML"
35866 513074557e06 move the Sledgehammer Isar commands together into one file; blanchet parents: 35865 diff changeset	114	use "Tools/Sledgehammer/sledgehammer_isar.ML"
39322 80420a0f2179 setup Auto Sledgehammer blanchet parents: 39036 diff changeset	115	setup Sledgehammer_Isar.setup
23444 6d4703843f93 added Metis setup (from Metis.thy); wenzelm parents: 21999 diff changeset	116
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	117	end

author	blanchet
	Sat, 11 Sep 2010 10:25:27 +0200
changeset 39322	80420a0f2179
parent 39036	dff91b90d74c
child 39355	104a6d9e493e
permissions	-rw-r--r--