isabelle: src/HOL/Sledgehammer.thy@df379a447753 (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/async_manager.ML")
9033c03cc214 consequence of directory renaming blanchet parents: 38028 diff changeset	14	("Tools/ATP/atp_problem.ML")
9033c03cc214 consequence of directory renaming blanchet parents: 38028 diff changeset	15	("Tools/ATP/atp_systems.ML")
38025 b660597a6796 reorder ML files in theory blanchet parents: 38023 diff changeset	16	("~~/src/Tools/Metis/metis.ML")
37574 b8c1f4c46983 renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier"; blanchet parents: 37571 diff changeset	17	("Tools/Sledgehammer/clausifier.ML")
37569 931f5948a32d move "MESON" up; blanchet parents: 37541 diff changeset	18	("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	19	("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	20	("Tools/Sledgehammer/metis_tactics.ML")
37571 76e23303c7ff more moving around of ML files in "Sledgehammer.thy" blanchet parents: 37569 diff changeset	21	("Tools/Sledgehammer/sledgehammer_util.ML")
35825 a6aad5a70ed4 move Sledgehammer files in a directory of their own blanchet parents: 33593 diff changeset	22	("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
38282 319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML) blanchet parents: 38047 diff changeset	23	("Tools/Sledgehammer/sledgehammer_translate.ML")
37579 61a01843a028 reorder ML files blanchet parents: 37578 diff changeset	24	("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
38023 962b0a7f544b more refactoring blanchet parents: 38021 diff changeset	25	("Tools/Sledgehammer/sledgehammer.ML")
38282 319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML) blanchet parents: 38047 diff changeset	26	("Tools/Sledgehammer/sledgehammer_fact_minimize.ML")
35866 513074557e06 move the Sledgehammer Isar commands together into one file; blanchet parents: 35865 diff changeset	27	("Tools/Sledgehammer/sledgehammer_isar.ML")
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	28	begin
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	29
37410 2bf7e6136047 adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf" blanchet parents: 37399 diff changeset	30	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	31	[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	32
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	33	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	34	[no_atp]: "COMBI P = P"
24819 7d8e0a47392e modernized definitions; wenzelm parents: 24742 diff changeset	35
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	36	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	37	[no_atp]: "COMBK P Q = P"
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	38
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	39	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	40	"COMBB P Q R = P (Q R)"
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	41
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	42	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	43	[no_atp]: "COMBC P Q R = P R Q"
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	44
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	45	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	46	[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	47
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	48	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	49	"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	50
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	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	52	by (simp add: fequal_def)
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	53
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	54	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	55	by (simp add: fequal_def)
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	56
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	57	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	58	by auto
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	59
24827 646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	60	text{Theorems for translation to combinators}
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	61
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	62	lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
24827 646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	63	apply (rule eq_reflection)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	64	apply (rule ext)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	65	apply (simp add: COMBS_def)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	66	done
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	67
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	68	lemma abs_I [no_atp]: "\<lambda>x. x \<equiv> COMBI"
24827 646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	69	apply (rule eq_reflection)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	70	apply (rule ext)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	71	apply (simp add: COMBI_def)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	72	done
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	73
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	74	lemma abs_K [no_atp]: "\<lambda>x. y \<equiv> COMBK y"
24827 646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	75	apply (rule eq_reflection)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	76	apply (rule ext)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	77	apply (simp add: COMBK_def)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	78	done
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	79
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	80	lemma abs_B [no_atp]: "\<lambda>x. a (g x) \<equiv> COMBB a g"
24827 646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	81	apply (rule eq_reflection)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	82	apply (rule ext)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	83	apply (simp add: COMBB_def)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	84	done
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	85
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	86	lemma abs_C [no_atp]: "\<lambda>x. (f x) b \<equiv> COMBC f b"
24827 646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	87	apply (rule eq_reflection)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	88	apply (rule ext)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	89	apply (simp add: COMBC_def)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	90	done
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	91
38047 9033c03cc214 consequence of directory renaming blanchet parents: 38028 diff changeset	92	use "Tools/ATP/async_manager.ML"
9033c03cc214 consequence of directory renaming blanchet parents: 38028 diff changeset	93	use "Tools/ATP/atp_problem.ML"
9033c03cc214 consequence of directory renaming blanchet parents: 38028 diff changeset	94	use "Tools/ATP/atp_systems.ML"
38025 b660597a6796 reorder ML files in theory blanchet parents: 38023 diff changeset	95	setup ATP_Systems.setup
b660597a6796 reorder ML files in theory blanchet parents: 38023 diff changeset	96
b660597a6796 reorder ML files in theory blanchet parents: 38023 diff changeset	97	use "~~/src/Tools/Metis/metis.ML"
37574 b8c1f4c46983 renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier"; blanchet parents: 37571 diff changeset	98	use "Tools/Sledgehammer/clausifier.ML"
37569 931f5948a32d move "MESON" up; blanchet parents: 37541 diff changeset	99	use "Tools/Sledgehammer/meson_tactic.ML"
931f5948a32d move "MESON" up; blanchet parents: 37541 diff changeset	100	setup Meson_Tactic.setup
37571 76e23303c7ff more moving around of ML files in "Sledgehammer.thy" blanchet parents: 37569 diff changeset	101
37578 9367cb36b1c4 renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer blanchet parents: 37577 diff changeset	102	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	103	use "Tools/Sledgehammer/metis_tactics.ML"
9367cb36b1c4 renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer blanchet parents: 37577 diff changeset	104
37571 76e23303c7ff more moving around of ML files in "Sledgehammer.thy" blanchet parents: 37569 diff changeset	105	use "Tools/Sledgehammer/sledgehammer_util.ML"
35825 a6aad5a70ed4 move Sledgehammer files in a directory of their own blanchet parents: 33593 diff changeset	106	use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
38282 319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML) blanchet parents: 38047 diff changeset	107	use "Tools/Sledgehammer/sledgehammer_translate.ML"
37579 61a01843a028 reorder ML files blanchet parents: 37578 diff changeset	108	use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
38023 962b0a7f544b more refactoring blanchet parents: 38021 diff changeset	109	use "Tools/Sledgehammer/sledgehammer.ML"
962b0a7f544b more refactoring blanchet parents: 38021 diff changeset	110	setup Sledgehammer.setup
38282 319c59682c51 move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML) blanchet parents: 38047 diff changeset	111	use "Tools/Sledgehammer/sledgehammer_fact_minimize.ML"
35866 513074557e06 move the Sledgehammer Isar commands together into one file; blanchet parents: 35865 diff changeset	112	use "Tools/Sledgehammer/sledgehammer_isar.ML"
35826 1590abc3d42a renamed Sledgehammer structures blanchet parents: 35825 diff changeset	113	setup Metis_Tactics.setup
23444 6d4703843f93 added Metis setup (from Metis.thy); wenzelm parents: 21999 diff changeset	114
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	115	end

author	hoelzl
	Fri, 27 Aug 2010 14:06:12 +0200
changeset 39089	df379a447753
parent 38606	3003ddbd46d9
child 38988	483879af0643
permissions	-rw-r--r--