author | blanchet |
Wed, 17 Mar 2010 18:16:31 +0100 | |
changeset 35825 | a6aad5a70ed4 |
parent 33593 | ef54e2108b74 |
child 35826 | 1590abc3d42a |
permissions | -rw-r--r-- |
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOL/ATP_Linkup.thy |
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 |
28483 | 4 |
Author: Fabian Immler, TUM |
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
5 |
*) |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
6 |
|
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28476
diff
changeset
|
7 |
header {* The Isabelle-ATP Linkup *} |
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
8 |
|
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
9 |
theory ATP_Linkup |
33593 | 10 |
imports Plain Hilbert_Choice |
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
11 |
uses |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
12 |
"Tools/polyhash.ML" |
35825
a6aad5a70ed4
move Sledgehammer files in a directory of their own
blanchet
parents:
33593
diff
changeset
|
13 |
"Tools/Sledgehammer/sledgehammer_fol_clause.ML" |
a6aad5a70ed4
move Sledgehammer files in a directory of their own
blanchet
parents:
33593
diff
changeset
|
14 |
("Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML") |
a6aad5a70ed4
move Sledgehammer files in a directory of their own
blanchet
parents:
33593
diff
changeset
|
15 |
("Tools/Sledgehammer/sledgehammer_hol_clause.ML") |
a6aad5a70ed4
move Sledgehammer files in a directory of their own
blanchet
parents:
33593
diff
changeset
|
16 |
("Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML") |
a6aad5a70ed4
move Sledgehammer files in a directory of their own
blanchet
parents:
33593
diff
changeset
|
17 |
("Tools/Sledgehammer/sledgehammer_fact_filter.ML") |
32327
0971cc0b6a57
src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
wenzelm
parents:
31835
diff
changeset
|
18 |
("Tools/ATP_Manager/atp_manager.ML") |
0971cc0b6a57
src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
wenzelm
parents:
31835
diff
changeset
|
19 |
("Tools/ATP_Manager/atp_wrapper.ML") |
0971cc0b6a57
src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
wenzelm
parents:
31835
diff
changeset
|
20 |
("Tools/ATP_Manager/atp_minimal.ML") |
23444 | 21 |
"~~/src/Tools/Metis/metis.ML" |
35825
a6aad5a70ed4
move Sledgehammer files in a directory of their own
blanchet
parents:
33593
diff
changeset
|
22 |
("Tools/Sledgehammer/metis_tactics.ML") |
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
23 |
begin |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
24 |
|
24819 | 25 |
definition COMBI :: "'a => 'a" |
26 |
where "COMBI P == P" |
|
27 |
||
28 |
definition COMBK :: "'a => 'b => 'a" |
|
29 |
where "COMBK P Q == P" |
|
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
30 |
|
24819 | 31 |
definition COMBB :: "('b => 'c) => ('a => 'b) => 'a => 'c" |
32 |
where "COMBB P Q R == P (Q R)" |
|
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
33 |
|
24819 | 34 |
definition COMBC :: "('a => 'b => 'c) => 'b => 'a => 'c" |
35 |
where "COMBC P Q R == P R Q" |
|
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
36 |
|
24819 | 37 |
definition COMBS :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c" |
38 |
where "COMBS P Q R == P R (Q R)" |
|
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
39 |
|
24819 | 40 |
definition fequal :: "'a => 'a => bool" |
41 |
where "fequal X Y == (X=Y)" |
|
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
42 |
|
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
43 |
lemma fequal_imp_equal: "fequal X Y ==> X=Y" |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
44 |
by (simp add: fequal_def) |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
45 |
|
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
46 |
lemma equal_imp_fequal: "X=Y ==> fequal X Y" |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
47 |
by (simp add: fequal_def) |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
48 |
|
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
49 |
text{*These two represent the equivalence between Boolean equality and iff. |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
50 |
They can't be converted to clauses automatically, as the iff would be |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
51 |
expanded...*} |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
52 |
|
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
53 |
lemma iff_positive: "P | Q | P=Q" |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
54 |
by blast |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
55 |
|
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
56 |
lemma iff_negative: "~P | ~Q | P=Q" |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
57 |
by blast |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
58 |
|
24827 | 59 |
text{*Theorems for translation to combinators*} |
60 |
||
61 |
lemma abs_S: "(%x. (f x) (g x)) == COMBS f g" |
|
62 |
apply (rule eq_reflection) |
|
63 |
apply (rule ext) |
|
64 |
apply (simp add: COMBS_def) |
|
65 |
done |
|
66 |
||
67 |
lemma abs_I: "(%x. x) == COMBI" |
|
68 |
apply (rule eq_reflection) |
|
69 |
apply (rule ext) |
|
70 |
apply (simp add: COMBI_def) |
|
71 |
done |
|
72 |
||
73 |
lemma abs_K: "(%x. y) == COMBK y" |
|
74 |
apply (rule eq_reflection) |
|
75 |
apply (rule ext) |
|
76 |
apply (simp add: COMBK_def) |
|
77 |
done |
|
78 |
||
79 |
lemma abs_B: "(%x. a (g x)) == COMBB a g" |
|
80 |
apply (rule eq_reflection) |
|
81 |
apply (rule ext) |
|
82 |
apply (simp add: COMBB_def) |
|
83 |
done |
|
84 |
||
85 |
lemma abs_C: "(%x. (f x) b) == COMBC f b" |
|
86 |
apply (rule eq_reflection) |
|
87 |
apply (rule ext) |
|
88 |
apply (simp add: COMBC_def) |
|
89 |
done |
|
90 |
||
27368 | 91 |
|
28585 | 92 |
subsection {* Setup of external ATPs *} |
27368 | 93 |
|
35825
a6aad5a70ed4
move Sledgehammer files in a directory of their own
blanchet
parents:
33593
diff
changeset
|
94 |
use "Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML" |
a6aad5a70ed4
move Sledgehammer files in a directory of their own
blanchet
parents:
33593
diff
changeset
|
95 |
setup Res_Axioms.setup |
a6aad5a70ed4
move Sledgehammer files in a directory of their own
blanchet
parents:
33593
diff
changeset
|
96 |
use "Tools/Sledgehammer/sledgehammer_hol_clause.ML" |
a6aad5a70ed4
move Sledgehammer files in a directory of their own
blanchet
parents:
33593
diff
changeset
|
97 |
use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML" |
a6aad5a70ed4
move Sledgehammer files in a directory of their own
blanchet
parents:
33593
diff
changeset
|
98 |
setup Res_Reconstruct.setup |
a6aad5a70ed4
move Sledgehammer files in a directory of their own
blanchet
parents:
33593
diff
changeset
|
99 |
use "Tools/Sledgehammer/sledgehammer_fact_filter.ML" |
28573 | 100 |
|
35825
a6aad5a70ed4
move Sledgehammer files in a directory of their own
blanchet
parents:
33593
diff
changeset
|
101 |
use "Tools/ATP_Manager/atp_wrapper.ML" |
a6aad5a70ed4
move Sledgehammer files in a directory of their own
blanchet
parents:
33593
diff
changeset
|
102 |
setup ATP_Wrapper.setup |
32327
0971cc0b6a57
src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
wenzelm
parents:
31835
diff
changeset
|
103 |
use "Tools/ATP_Manager/atp_manager.ML" |
0971cc0b6a57
src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
wenzelm
parents:
31835
diff
changeset
|
104 |
use "Tools/ATP_Manager/atp_minimal.ML" |
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
29654
diff
changeset
|
105 |
|
28483 | 106 |
text {* basic provers *} |
32936 | 107 |
setup {* ATP_Manager.add_prover ATP_Wrapper.spass *} |
108 |
setup {* ATP_Manager.add_prover ATP_Wrapper.vampire *} |
|
109 |
setup {* ATP_Manager.add_prover ATP_Wrapper.eprover *} |
|
28483 | 110 |
|
111 |
text {* provers with stuctured output *} |
|
32936 | 112 |
setup {* ATP_Manager.add_prover ATP_Wrapper.vampire_full *} |
113 |
setup {* ATP_Manager.add_prover ATP_Wrapper.eprover_full *} |
|
28483 | 114 |
|
115 |
text {* on some problems better results *} |
|
32936 | 116 |
setup {* ATP_Manager.add_prover ATP_Wrapper.spass_no_tc *} |
27182 | 117 |
|
28573 | 118 |
text {* remote provers via SystemOnTPTP *} |
32936 | 119 |
setup {* ATP_Manager.add_prover ATP_Wrapper.remote_vampire *} |
120 |
setup {* ATP_Manager.add_prover ATP_Wrapper.remote_spass *} |
|
121 |
setup {* ATP_Manager.add_prover ATP_Wrapper.remote_eprover *} |
|
29587
96599d8d8268
simplified usage of remote-script; added compatible remote-atps
immler@in.tum.de
parents:
28594
diff
changeset
|
122 |
|
28573 | 123 |
|
23444 | 124 |
|
125 |
subsection {* The Metis prover *} |
|
126 |
||
35825
a6aad5a70ed4
move Sledgehammer files in a directory of their own
blanchet
parents:
33593
diff
changeset
|
127 |
use "Tools/Sledgehammer/metis_tactics.ML" |
23444 | 128 |
setup MetisTools.setup |
129 |
||
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
130 |
end |