author | blanchet |
Tue, 31 Aug 2010 23:50:59 +0200 | |
changeset 38988 | 483879af0643 |
parent 38606 | 3003ddbd46d9 |
child 38990 | 7fba3ccc755a |
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/async_manager.ML") |
14 |
("Tools/ATP/atp_problem.ML") |
|
15 |
("Tools/ATP/atp_systems.ML") |
|
38025 | 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 | 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") |
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 |
|
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 | 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 | 60 |
text{*Theorems for translation to combinators*} |
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 | 63 |
apply (rule eq_reflection) |
64 |
apply (rule ext) |
|
65 |
apply (simp add: COMBS_def) |
|
66 |
done |
|
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 | 69 |
apply (rule eq_reflection) |
70 |
apply (rule ext) |
|
71 |
apply (simp add: COMBI_def) |
|
72 |
done |
|
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 | 75 |
apply (rule eq_reflection) |
76 |
apply (rule ext) |
|
77 |
apply (simp add: COMBK_def) |
|
78 |
done |
|
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 | 81 |
apply (rule eq_reflection) |
82 |
apply (rule ext) |
|
83 |
apply (simp add: COMBB_def) |
|
84 |
done |
|
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 | 87 |
apply (rule eq_reflection) |
88 |
apply (rule ext) |
|
89 |
apply (simp add: COMBC_def) |
|
90 |
done |
|
91 |
||
38047 | 92 |
use "Tools/ATP/async_manager.ML" |
93 |
use "Tools/ATP/atp_problem.ML" |
|
94 |
use "Tools/ATP/atp_systems.ML" |
|
38025 | 95 |
setup ATP_Systems.setup |
96 |
||
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 | 99 |
use "Tools/Sledgehammer/meson_tactic.ML" |
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" |
38988 | 106 |
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
|
107 |
use "Tools/Sledgehammer/sledgehammer_translate.ML" |
38988 | 108 |
use "Tools/Sledgehammer/sledgehammer_reconstruct.ML" |
38023 | 109 |
use "Tools/Sledgehammer/sledgehammer.ML" |
110 |
setup Sledgehammer.setup |
|
38988 | 111 |
use "Tools/Sledgehammer/sledgehammer_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 | 113 |
setup Metis_Tactics.setup |
23444 | 114 |
|
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
115 |
end |