isabelle: src/HOL/Sledgehammer.thy@3daaf23b9ab4 (annotated)

35827 f552152d7747 renamed "ATP_Linkup" theory to "Sledgehammer" blanchet parents: 35826 diff changeset	1	(* Title: HOL/Sledgehammer.thy
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	2	Author: Lawrence C Paulson
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	3	Author: Jia Meng, 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
35865 2f8fb5242799 more Sledgehammer refactoring blanchet parents: 35827 diff changeset	13	"~~/src/Tools/Metis/metis.ML"
37574 b8c1f4c46983 renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier"; blanchet parents: 37571 diff changeset	14	("Tools/Sledgehammer/clausifier.ML")
37569 931f5948a32d move "MESON" up; blanchet parents: 37541 diff changeset	15	("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	16	("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	17	("Tools/Sledgehammer/metis_tactics.ML")
37571 76e23303c7ff more moving around of ML files in "Sledgehammer.thy" blanchet parents: 37569 diff changeset	18	("Tools/Sledgehammer/sledgehammer_util.ML")
35825 a6aad5a70ed4 move Sledgehammer files in a directory of their own blanchet parents: 33593 diff changeset	19	("Tools/Sledgehammer/sledgehammer_fact_filter.ML")
37509 f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes blanchet parents: 37410 diff changeset	20	("Tools/Sledgehammer/sledgehammer_tptp_format.ML")
37579 61a01843a028 reorder ML files blanchet parents: 37578 diff changeset	21	("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML")
37583 9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration blanchet parents: 37579 diff changeset	22	("Tools/ATP_Manager/async_manager.ML")
32327 0971cc0b6a57 src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place; wenzelm parents: 31835 diff changeset	23	("Tools/ATP_Manager/atp_manager.ML")
36377 b3dce4c715d0 now rename the file "atp_wrapper.ML" to "atp_systems.ML" + fix typo in "SystemOnTPTP" script blanchet parents: 36376 diff changeset	24	("Tools/ATP_Manager/atp_systems.ML")
36375 2482446a604c move the minimizer to the Sledgehammer directory blanchet parents: 36064 diff changeset	25	("Tools/Sledgehammer/sledgehammer_fact_minimizer.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
37410 2bf7e6136047 adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf" blanchet parents: 37399 diff changeset	29	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	30	[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	31
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	32	definition COMBI :: "'a \<Rightarrow> 'a" where
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	[no_atp]: "COMBI P \<equiv> P"
24819 7d8e0a47392e modernized definitions; wenzelm parents: 24742 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 COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" where
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	[no_atp]: "COMBK P Q \<equiv> P"
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: 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 COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where [no_atp]:
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	"COMBB P Q R \<equiv> P (Q R)"
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 COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
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	[no_atp]: "COMBC P Q R \<equiv> P R Q"
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 COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where
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	[no_atp]: "COMBS P Q R \<equiv> P R (Q R)"
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 fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
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	"fequal X Y \<equiv> (X = Y)"
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	lemma fequal_imp_equal [no_atp]: "fequal X Y \<Longrightarrow> X = Y"
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	51	by (simp add: fequal_def)
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	52
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	53	lemma equal_imp_fequal [no_atp]: "X = Y \<Longrightarrow> fequal X Y"
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	54	by (simp add: fequal_def)
d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	55
24827 646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	56	text{Theorems for translation to combinators}
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	57
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	58	lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
24827 646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	59	apply (rule eq_reflection)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	60	apply (rule ext)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	61	apply (simp add: COMBS_def)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	62	done
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_I [no_atp]: "\<lambda>x. x \<equiv> COMBI"
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: COMBI_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_K [no_atp]: "\<lambda>x. y \<equiv> COMBK y"
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: COMBK_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_B [no_atp]: "\<lambda>x. a (g x) \<equiv> COMBB a g"
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: COMBB_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_C [no_atp]: "\<lambda>x. (f x) b \<equiv> COMBC f b"
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: COMBC_def)
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	86	done
646bdc51eb7d combinator translation paulson parents: 24819 diff changeset	87
37574 b8c1f4c46983 renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier"; blanchet parents: 37571 diff changeset	88	use "Tools/Sledgehammer/clausifier.ML"
37569 931f5948a32d move "MESON" up; blanchet parents: 37541 diff changeset	89	use "Tools/Sledgehammer/meson_tactic.ML"
931f5948a32d move "MESON" up; blanchet parents: 37541 diff changeset	90	setup Meson_Tactic.setup
37571 76e23303c7ff more moving around of ML files in "Sledgehammer.thy" blanchet parents: 37569 diff changeset	91
37578 9367cb36b1c4 renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer blanchet parents: 37577 diff changeset	92	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	93	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	94
37571 76e23303c7ff more moving around of ML files in "Sledgehammer.thy" blanchet parents: 37569 diff changeset	95	use "Tools/Sledgehammer/sledgehammer_util.ML"
35825 a6aad5a70ed4 move Sledgehammer files in a directory of their own blanchet parents: 33593 diff changeset	96	use "Tools/Sledgehammer/sledgehammer_fact_filter.ML"
37509 f39464d971c4 factor out TPTP format output into file of its own, to facilitate further changes blanchet parents: 37410 diff changeset	97	use "Tools/Sledgehammer/sledgehammer_tptp_format.ML"
37579 61a01843a028 reorder ML files blanchet parents: 37578 diff changeset	98	use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML"
37583 9ce2451647d5 factored non-ATP specific code from "ATP_Manager" out, so that it can be reused for the LEO-II integration blanchet parents: 37579 diff changeset	99	use "Tools/ATP_Manager/async_manager.ML"
35867 16279c4c7a33 move all ATP setup code into ATP_Wrapper blanchet parents: 35866 diff changeset	100	use "Tools/ATP_Manager/atp_manager.ML"
36377 b3dce4c715d0 now rename the file "atp_wrapper.ML" to "atp_systems.ML" + fix typo in "SystemOnTPTP" script blanchet parents: 36376 diff changeset	101	use "Tools/ATP_Manager/atp_systems.ML"
36376 e83d52a52449 renamed module "ATP_Wrapper" to "ATP_Systems" blanchet parents: 36375 diff changeset	102	setup ATP_Systems.setup
36375 2482446a604c move the minimizer to the Sledgehammer directory blanchet parents: 36064 diff changeset	103	use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
35866 513074557e06 move the Sledgehammer Isar commands together into one file; blanchet parents: 35865 diff changeset	104	use "Tools/Sledgehammer/sledgehammer_isar.ML"
35826 1590abc3d42a renamed Sledgehammer structures blanchet parents: 35825 diff changeset	105	setup Metis_Tactics.setup
23444 6d4703843f93 added Metis setup (from Metis.thy); wenzelm parents: 21999 diff changeset	106
21254 d53f76357f41 incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup; wenzelm parents: diff changeset	107	end

author	haftmann
	Thu, 08 Jul 2010 16:19:24 +0200
changeset 37744	3daaf23b9ab4
parent 37622	b3f572839570
child 38019	e207a64e1e0b
permissions	-rw-r--r--