author | blanchet |
Wed, 29 Sep 2010 23:26:39 +0200 | |
changeset 39889 | 21d556f10944 |
parent 39720 | 0b93a954da4f |
child 39890 | a1695e2169d0 |
permissions | -rw-r--r-- |
35827 | 1 |
(* Title: HOL/Sledgehammer.thy |
38027 | 2 |
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory |
38028 | 3 |
Author: Jia Meng, Cambridge University Computer Laboratory and NICTA |
35865 | 4 |
Author: Fabian Immler, TU Muenchen |
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 | 8 |
header {* Sledgehammer: Isabelle--ATP Linkup *} |
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
9 |
|
35827 | 10 |
theory Sledgehammer |
33593 | 11 |
imports Plain Hilbert_Choice |
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
12 |
uses |
38047 | 13 |
("Tools/ATP/atp_problem.ML") |
39452 | 14 |
("Tools/ATP/atp_proof.ML") |
38047 | 15 |
("Tools/ATP/atp_systems.ML") |
38025 | 16 |
("~~/src/Tools/Metis/metis.ML") |
39889 | 17 |
("Tools/Sledgehammer/meson_clausify.ML") |
39494
bf7dd4902321
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents:
39452
diff
changeset
|
18 |
("Tools/Sledgehammer/metis_translate.ML") |
39495
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
39494
diff
changeset
|
19 |
("Tools/Sledgehammer/metis_reconstruct.ML") |
37578
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") |
38988 | 22 |
("Tools/Sledgehammer/sledgehammer_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") |
38988 | 24 |
("Tools/Sledgehammer/sledgehammer_reconstruct.ML") |
38023 | 25 |
("Tools/Sledgehammer/sledgehammer.ML") |
38988 | 26 |
("Tools/Sledgehammer/sledgehammer_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 |
|
39036
dff91b90d74c
use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
blanchet
parents:
38990
diff
changeset
|
30 |
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
|
31 |
by simp |
dff91b90d74c
use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
blanchet
parents:
38990
diff
changeset
|
32 |
|
39355 | 33 |
definition skolem :: "'a \<Rightarrow> 'a" where |
34 |
[no_atp]: "skolem = (\<lambda>x. x)" |
|
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
36569
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 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
|
37 |
[no_atp]: "COMBI P = P" |
24819 | 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 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
|
40 |
[no_atp]: "COMBK P Q = P" |
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 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
|
43 |
"COMBB P Q R = P (Q R)" |
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 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
|
46 |
[no_atp]: "COMBC P Q R = P R Q" |
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 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
|
49 |
[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
|
50 |
|
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
|
51 |
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
|
52 |
"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
|
53 |
|
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 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
|
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_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
|
58 |
by (simp add: fequal_def) |
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
59 |
|
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
|
60 |
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
|
61 |
by auto |
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
62 |
|
24827 | 63 |
text{*Theorems for translation to combinators*} |
64 |
||
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
|
65 |
lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g" |
24827 | 66 |
apply (rule eq_reflection) |
67 |
apply (rule ext) |
|
68 |
apply (simp add: COMBS_def) |
|
69 |
done |
|
70 |
||
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
|
71 |
lemma abs_I [no_atp]: "\<lambda>x. x \<equiv> COMBI" |
24827 | 72 |
apply (rule eq_reflection) |
73 |
apply (rule ext) |
|
74 |
apply (simp add: COMBI_def) |
|
75 |
done |
|
76 |
||
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
|
77 |
lemma abs_K [no_atp]: "\<lambda>x. y \<equiv> COMBK y" |
24827 | 78 |
apply (rule eq_reflection) |
79 |
apply (rule ext) |
|
80 |
apply (simp add: COMBK_def) |
|
81 |
done |
|
82 |
||
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
|
83 |
lemma abs_B [no_atp]: "\<lambda>x. a (g x) \<equiv> COMBB a g" |
24827 | 84 |
apply (rule eq_reflection) |
85 |
apply (rule ext) |
|
86 |
apply (simp add: COMBB_def) |
|
87 |
done |
|
88 |
||
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
|
89 |
lemma abs_C [no_atp]: "\<lambda>x. (f x) b \<equiv> COMBC f b" |
24827 | 90 |
apply (rule eq_reflection) |
91 |
apply (rule ext) |
|
92 |
apply (simp add: COMBC_def) |
|
93 |
done |
|
94 |
||
38047 | 95 |
use "Tools/ATP/atp_problem.ML" |
39452 | 96 |
use "Tools/ATP/atp_proof.ML" |
38047 | 97 |
use "Tools/ATP/atp_systems.ML" |
38025 | 98 |
setup ATP_Systems.setup |
99 |
||
100 |
use "~~/src/Tools/Metis/metis.ML" |
|
39889 | 101 |
use "Tools/Sledgehammer/meson_clausify.ML" |
39720
0b93a954da4f
rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"
blanchet
parents:
39495
diff
changeset
|
102 |
setup Meson_Clausifier.setup |
37571
76e23303c7ff
more moving around of ML files in "Sledgehammer.thy"
blanchet
parents:
37569
diff
changeset
|
103 |
|
39494
bf7dd4902321
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents:
39452
diff
changeset
|
104 |
use "Tools/Sledgehammer/metis_translate.ML" |
39495
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
39494
diff
changeset
|
105 |
use "Tools/Sledgehammer/metis_reconstruct.ML" |
37578
9367cb36b1c4
renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
blanchet
parents:
37577
diff
changeset
|
106 |
use "Tools/Sledgehammer/metis_tactics.ML" |
39322 | 107 |
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
|
108 |
|
37571
76e23303c7ff
more moving around of ML files in "Sledgehammer.thy"
blanchet
parents:
37569
diff
changeset
|
109 |
use "Tools/Sledgehammer/sledgehammer_util.ML" |
38988 | 110 |
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
|
111 |
use "Tools/Sledgehammer/sledgehammer_translate.ML" |
38988 | 112 |
use "Tools/Sledgehammer/sledgehammer_reconstruct.ML" |
38023 | 113 |
use "Tools/Sledgehammer/sledgehammer.ML" |
114 |
setup Sledgehammer.setup |
|
38988 | 115 |
use "Tools/Sledgehammer/sledgehammer_minimize.ML" |
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
116 |
use "Tools/Sledgehammer/sledgehammer_isar.ML" |
39322 | 117 |
setup Sledgehammer_Isar.setup |
23444 | 118 |
|
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
119 |
end |