author | wenzelm |
Mon, 13 Oct 2008 14:04:53 +0200 | |
changeset 28573 | 6403f0e16269 |
parent 28483 | 9912ab2992f6 |
child 28585 | be3c44ac3e86 |
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 |
ID: $Id$ |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
4 |
Author: Jia Meng, NICTA |
28483 | 5 |
Author: Fabian Immler, TUM |
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 |
|
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28476
diff
changeset
|
8 |
header {* The Isabelle-ATP Linkup *} |
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
9 |
|
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
10 |
theory ATP_Linkup |
27368 | 11 |
imports Record Hilbert_Choice |
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
12 |
uses |
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
13 |
"Tools/polyhash.ML" |
21977 | 14 |
"Tools/res_clause.ML" |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28476
diff
changeset
|
15 |
("Tools/res_axioms.ML") |
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
16 |
("Tools/res_hol_clause.ML") |
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21977
diff
changeset
|
17 |
("Tools/res_reconstruct.ML") |
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
18 |
("Tools/res_atp.ML") |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28476
diff
changeset
|
19 |
("Tools/atp_manager.ML") |
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28476
diff
changeset
|
20 |
("Tools/atp_thread.ML") |
23444 | 21 |
"~~/src/Tools/Metis/metis.ML" |
22 |
("Tools/metis_tools.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 |
|
92 |
subsection {* Setup of Vampire, E prover and SPASS *} |
|
93 |
||
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28476
diff
changeset
|
94 |
use "Tools/res_axioms.ML" setup ResAxioms.setup |
24827 | 95 |
use "Tools/res_hol_clause.ML" |
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28476
diff
changeset
|
96 |
use "Tools/res_reconstruct.ML" setup ResReconstruct.setup |
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
97 |
use "Tools/res_atp.ML" |
28573 | 98 |
|
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28476
diff
changeset
|
99 |
use "Tools/atp_manager.ML" |
28483 | 100 |
use "Tools/atp_thread.ML" |
101 |
||
102 |
text {* basic provers *} |
|
103 |
setup {* AtpManager.add_prover "spass" AtpThread.spass *} |
|
104 |
setup {* AtpManager.add_prover "vampire" AtpThread.vampire *} |
|
105 |
setup {* AtpManager.add_prover "e" AtpThread.eprover *} |
|
106 |
||
107 |
text {* provers with stuctured output *} |
|
108 |
setup {* AtpManager.add_prover "vampire_full" AtpThread.vampire_full *} |
|
109 |
setup {* AtpManager.add_prover "e_full" AtpThread.eprover_full *} |
|
110 |
||
111 |
text {* on some problems better results *} |
|
112 |
setup {* AtpManager.add_prover "spass_no_tc" (AtpThread.spass_filter_opts 40 false) *} |
|
27182 | 113 |
|
28573 | 114 |
text {* remote provers via SystemOnTPTP *} |
115 |
setup {* AtpManager.add_prover "remote_vamp9" |
|
116 |
(AtpThread.remote_prover "Vampire---9.0" "jumpirefix --output_syntax tptp --mode casc -t 3600") *} |
|
117 |
setup {* AtpManager.add_prover "remote_vamp10" |
|
118 |
(AtpThread.remote_prover "Vampire---10.0" "drakosha.pl 60") *} |
|
119 |
||
23444 | 120 |
|
121 |
subsection {* The Metis prover *} |
|
122 |
||
123 |
use "Tools/metis_tools.ML" |
|
124 |
setup MetisTools.setup |
|
125 |
||
21254
d53f76357f41
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
wenzelm
parents:
diff
changeset
|
126 |
end |