author | haftmann |
Wed, 21 Jan 2009 23:42:37 +0100 | |
changeset 29611 | 9891e3646809 |
parent 29600 | 0182b65e4ad0 |
parent 29609 | a010aab5bed0 |
child 29654 | 24e73987bfe2 |
permissions | -rw-r--r-- |
wenzelm@21254 | 1 |
(* Title: HOL/ATP_Linkup.thy |
wenzelm@21254 | 2 |
Author: Lawrence C Paulson |
wenzelm@21254 | 3 |
Author: Jia Meng, NICTA |
wenzelm@28483 | 4 |
Author: Fabian Immler, TUM |
wenzelm@21254 | 5 |
*) |
wenzelm@21254 | 6 |
|
wenzelm@28477 | 7 |
header {* The Isabelle-ATP Linkup *} |
wenzelm@21254 | 8 |
|
wenzelm@21254 | 9 |
theory ATP_Linkup |
haftmann@29609 | 10 |
imports Divides Record Hilbert_Choice |
wenzelm@21254 | 11 |
uses |
wenzelm@21254 | 12 |
"Tools/polyhash.ML" |
paulson@21977 | 13 |
"Tools/res_clause.ML" |
wenzelm@28477 | 14 |
("Tools/res_axioms.ML") |
wenzelm@21254 | 15 |
("Tools/res_hol_clause.ML") |
paulson@21999 | 16 |
("Tools/res_reconstruct.ML") |
wenzelm@21254 | 17 |
("Tools/res_atp.ML") |
wenzelm@28477 | 18 |
("Tools/atp_manager.ML") |
wenzelm@28592 | 19 |
("Tools/atp_wrapper.ML") |
wenzelm@23444 | 20 |
"~~/src/Tools/Metis/metis.ML" |
wenzelm@23444 | 21 |
("Tools/metis_tools.ML") |
wenzelm@21254 | 22 |
begin |
wenzelm@21254 | 23 |
|
wenzelm@24819 | 24 |
definition COMBI :: "'a => 'a" |
wenzelm@24819 | 25 |
where "COMBI P == P" |
wenzelm@21254 | 26 |
|
wenzelm@24819 | 27 |
definition COMBK :: "'a => 'b => 'a" |
wenzelm@24819 | 28 |
where "COMBK P Q == P" |
wenzelm@21254 | 29 |
|
wenzelm@24819 | 30 |
definition COMBB :: "('b => 'c) => ('a => 'b) => 'a => 'c" |
wenzelm@24819 | 31 |
where "COMBB P Q R == P (Q R)" |
wenzelm@21254 | 32 |
|
wenzelm@24819 | 33 |
definition COMBC :: "('a => 'b => 'c) => 'b => 'a => 'c" |
wenzelm@24819 | 34 |
where "COMBC P Q R == P R Q" |
wenzelm@21254 | 35 |
|
wenzelm@24819 | 36 |
definition COMBS :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c" |
wenzelm@24819 | 37 |
where "COMBS P Q R == P R (Q R)" |
wenzelm@21254 | 38 |
|
wenzelm@24819 | 39 |
definition fequal :: "'a => 'a => bool" |
wenzelm@24819 | 40 |
where "fequal X Y == (X=Y)" |
wenzelm@21254 | 41 |
|
wenzelm@21254 | 42 |
lemma fequal_imp_equal: "fequal X Y ==> X=Y" |
wenzelm@21254 | 43 |
by (simp add: fequal_def) |
wenzelm@21254 | 44 |
|
wenzelm@21254 | 45 |
lemma equal_imp_fequal: "X=Y ==> fequal X Y" |
wenzelm@21254 | 46 |
by (simp add: fequal_def) |
wenzelm@21254 | 47 |
|
wenzelm@21254 | 48 |
text{*These two represent the equivalence between Boolean equality and iff. |
wenzelm@21254 | 49 |
They can't be converted to clauses automatically, as the iff would be |
wenzelm@21254 | 50 |
expanded...*} |
wenzelm@21254 | 51 |
|
wenzelm@21254 | 52 |
lemma iff_positive: "P | Q | P=Q" |
wenzelm@21254 | 53 |
by blast |
wenzelm@21254 | 54 |
|
wenzelm@21254 | 55 |
lemma iff_negative: "~P | ~Q | P=Q" |
wenzelm@21254 | 56 |
by blast |
wenzelm@21254 | 57 |
|
paulson@24827 | 58 |
text{*Theorems for translation to combinators*} |
paulson@24827 | 59 |
|
paulson@24827 | 60 |
lemma abs_S: "(%x. (f x) (g x)) == COMBS f g" |
paulson@24827 | 61 |
apply (rule eq_reflection) |
paulson@24827 | 62 |
apply (rule ext) |
paulson@24827 | 63 |
apply (simp add: COMBS_def) |
paulson@24827 | 64 |
done |
paulson@24827 | 65 |
|
paulson@24827 | 66 |
lemma abs_I: "(%x. x) == COMBI" |
paulson@24827 | 67 |
apply (rule eq_reflection) |
paulson@24827 | 68 |
apply (rule ext) |
paulson@24827 | 69 |
apply (simp add: COMBI_def) |
paulson@24827 | 70 |
done |
paulson@24827 | 71 |
|
paulson@24827 | 72 |
lemma abs_K: "(%x. y) == COMBK y" |
paulson@24827 | 73 |
apply (rule eq_reflection) |
paulson@24827 | 74 |
apply (rule ext) |
paulson@24827 | 75 |
apply (simp add: COMBK_def) |
paulson@24827 | 76 |
done |
paulson@24827 | 77 |
|
paulson@24827 | 78 |
lemma abs_B: "(%x. a (g x)) == COMBB a g" |
paulson@24827 | 79 |
apply (rule eq_reflection) |
paulson@24827 | 80 |
apply (rule ext) |
paulson@24827 | 81 |
apply (simp add: COMBB_def) |
paulson@24827 | 82 |
done |
paulson@24827 | 83 |
|
paulson@24827 | 84 |
lemma abs_C: "(%x. (f x) b) == COMBC f b" |
paulson@24827 | 85 |
apply (rule eq_reflection) |
paulson@24827 | 86 |
apply (rule ext) |
paulson@24827 | 87 |
apply (simp add: COMBC_def) |
paulson@24827 | 88 |
done |
paulson@24827 | 89 |
|
haftmann@27368 | 90 |
|
wenzelm@28585 | 91 |
subsection {* Setup of external ATPs *} |
haftmann@27368 | 92 |
|
wenzelm@28477 | 93 |
use "Tools/res_axioms.ML" setup ResAxioms.setup |
paulson@24827 | 94 |
use "Tools/res_hol_clause.ML" |
wenzelm@28477 | 95 |
use "Tools/res_reconstruct.ML" setup ResReconstruct.setup |
wenzelm@21254 | 96 |
use "Tools/res_atp.ML" |
wenzelm@28573 | 97 |
|
wenzelm@28477 | 98 |
use "Tools/atp_manager.ML" |
wenzelm@28592 | 99 |
use "Tools/atp_wrapper.ML" |
wenzelm@28483 | 100 |
|
wenzelm@28483 | 101 |
text {* basic provers *} |
wenzelm@28592 | 102 |
setup {* AtpManager.add_prover "spass" AtpWrapper.spass *} |
wenzelm@28592 | 103 |
setup {* AtpManager.add_prover "vampire" AtpWrapper.vampire *} |
wenzelm@28592 | 104 |
setup {* AtpManager.add_prover "e" AtpWrapper.eprover *} |
wenzelm@28483 | 105 |
|
wenzelm@28483 | 106 |
text {* provers with stuctured output *} |
wenzelm@28592 | 107 |
setup {* AtpManager.add_prover "vampire_full" AtpWrapper.vampire_full *} |
wenzelm@28592 | 108 |
setup {* AtpManager.add_prover "e_full" AtpWrapper.eprover_full *} |
wenzelm@28483 | 109 |
|
wenzelm@28483 | 110 |
text {* on some problems better results *} |
wenzelm@28594 | 111 |
setup {* AtpManager.add_prover "spass_no_tc" (AtpWrapper.spass_opts 40 false) *} |
wenzelm@27182 | 112 |
|
wenzelm@28573 | 113 |
text {* remote provers via SystemOnTPTP *} |
immler@29590 | 114 |
setup {* AtpManager.add_prover "remote_vampire" |
immler@29593 | 115 |
(AtpWrapper.remote_prover "-s Vampire---9.0") *} |
immler@29587 | 116 |
setup {* AtpManager.add_prover "remote_spass" |
immler@29593 | 117 |
(AtpWrapper.remote_prover "-s SPASS---3.01") *} |
immler@29587 | 118 |
setup {* AtpManager.add_prover "remote_e" |
immler@29593 | 119 |
(AtpWrapper.remote_prover "-s EP---1.0") *} |
immler@29587 | 120 |
|
wenzelm@28573 | 121 |
|
wenzelm@23444 | 122 |
|
wenzelm@23444 | 123 |
subsection {* The Metis prover *} |
wenzelm@23444 | 124 |
|
wenzelm@23444 | 125 |
use "Tools/metis_tools.ML" |
wenzelm@23444 | 126 |
setup MetisTools.setup |
wenzelm@23444 | 127 |
|
wenzelm@21254 | 128 |
end |