author | wenzelm |
Wed, 08 Nov 2006 21:45:15 +0100 | |
changeset 21254 | d53f76357f41 |
child 21453 | 03ca07d478be |
permissions | -rw-r--r-- |
wenzelm@21254 | 1 |
(* Title: HOL/ATP_Linkup.thy |
wenzelm@21254 | 2 |
ID: $Id$ |
wenzelm@21254 | 3 |
Author: Lawrence C Paulson |
wenzelm@21254 | 4 |
Author: Jia Meng, NICTA |
wenzelm@21254 | 5 |
*) |
wenzelm@21254 | 6 |
|
wenzelm@21254 | 7 |
header{* The Isabelle-ATP Linkup *} |
wenzelm@21254 | 8 |
|
wenzelm@21254 | 9 |
theory ATP_Linkup |
wenzelm@21254 | 10 |
imports Hilbert_Choice Map Extraction |
wenzelm@21254 | 11 |
uses |
wenzelm@21254 | 12 |
"Tools/polyhash.ML" |
wenzelm@21254 | 13 |
"Tools/ATP/AtpCommunication.ML" |
wenzelm@21254 | 14 |
"Tools/ATP/watcher.ML" |
wenzelm@21254 | 15 |
"Tools/ATP/reduce_axiomsN.ML" |
wenzelm@21254 | 16 |
"Tools/res_clause.ML" |
wenzelm@21254 | 17 |
("Tools/res_hol_clause.ML") |
wenzelm@21254 | 18 |
("Tools/res_axioms.ML") |
wenzelm@21254 | 19 |
("Tools/res_atp.ML") |
wenzelm@21254 | 20 |
("Tools/res_atp_provers.ML") |
wenzelm@21254 | 21 |
("Tools/res_atp_methods.ML") |
wenzelm@21254 | 22 |
begin |
wenzelm@21254 | 23 |
|
wenzelm@21254 | 24 |
constdefs |
wenzelm@21254 | 25 |
COMBI :: "'a => 'a" |
wenzelm@21254 | 26 |
"COMBI P == P" |
wenzelm@21254 | 27 |
|
wenzelm@21254 | 28 |
COMBK :: "'a => 'b => 'a" |
wenzelm@21254 | 29 |
"COMBK P Q == P" |
wenzelm@21254 | 30 |
|
wenzelm@21254 | 31 |
COMBB :: "('b => 'c) => ('a => 'b) => 'a => 'c" |
wenzelm@21254 | 32 |
"COMBB P Q R == P (Q R)" |
wenzelm@21254 | 33 |
|
wenzelm@21254 | 34 |
COMBC :: "('a => 'b => 'c) => 'b => 'a => 'c" |
wenzelm@21254 | 35 |
"COMBC P Q R == P R Q" |
wenzelm@21254 | 36 |
|
wenzelm@21254 | 37 |
COMBS :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c" |
wenzelm@21254 | 38 |
"COMBS P Q R == P R (Q R)" |
wenzelm@21254 | 39 |
|
wenzelm@21254 | 40 |
COMBB' :: "('a => 'c) => ('b => 'a) => ('d => 'b) => 'd => 'c" |
wenzelm@21254 | 41 |
"COMBB' M P Q R == M (P (Q R))" |
wenzelm@21254 | 42 |
|
wenzelm@21254 | 43 |
COMBC' :: "('a => 'b => 'c) => ('d => 'a) => 'b => 'd => 'c" |
wenzelm@21254 | 44 |
"COMBC' M P Q R == M (P R) Q" |
wenzelm@21254 | 45 |
|
wenzelm@21254 | 46 |
COMBS' :: "('a => 'b => 'c) => ('d => 'a) => ('d => 'b) => 'd => 'c" |
wenzelm@21254 | 47 |
"COMBS' M P Q R == M (P R) (Q R)" |
wenzelm@21254 | 48 |
|
wenzelm@21254 | 49 |
fequal :: "'a => 'a => bool" |
wenzelm@21254 | 50 |
"fequal X Y == (X=Y)" |
wenzelm@21254 | 51 |
|
wenzelm@21254 | 52 |
lemma fequal_imp_equal: "fequal X Y ==> X=Y" |
wenzelm@21254 | 53 |
by (simp add: fequal_def) |
wenzelm@21254 | 54 |
|
wenzelm@21254 | 55 |
lemma equal_imp_fequal: "X=Y ==> fequal X Y" |
wenzelm@21254 | 56 |
by (simp add: fequal_def) |
wenzelm@21254 | 57 |
|
wenzelm@21254 | 58 |
lemma K_simp: "COMBK P == (%Q. P)" |
wenzelm@21254 | 59 |
apply (rule eq_reflection) |
wenzelm@21254 | 60 |
apply (rule ext) |
wenzelm@21254 | 61 |
apply (simp add: COMBK_def) |
wenzelm@21254 | 62 |
done |
wenzelm@21254 | 63 |
|
wenzelm@21254 | 64 |
lemma I_simp: "COMBI == (%P. P)" |
wenzelm@21254 | 65 |
apply (rule eq_reflection) |
wenzelm@21254 | 66 |
apply (rule ext) |
wenzelm@21254 | 67 |
apply (simp add: COMBI_def) |
wenzelm@21254 | 68 |
done |
wenzelm@21254 | 69 |
|
wenzelm@21254 | 70 |
lemma B_simp: "COMBB P Q == %R. P (Q R)" |
wenzelm@21254 | 71 |
apply (rule eq_reflection) |
wenzelm@21254 | 72 |
apply (rule ext) |
wenzelm@21254 | 73 |
apply (simp add: COMBB_def) |
wenzelm@21254 | 74 |
done |
wenzelm@21254 | 75 |
|
wenzelm@21254 | 76 |
text{*These two represent the equivalence between Boolean equality and iff. |
wenzelm@21254 | 77 |
They can't be converted to clauses automatically, as the iff would be |
wenzelm@21254 | 78 |
expanded...*} |
wenzelm@21254 | 79 |
|
wenzelm@21254 | 80 |
lemma iff_positive: "P | Q | P=Q" |
wenzelm@21254 | 81 |
by blast |
wenzelm@21254 | 82 |
|
wenzelm@21254 | 83 |
lemma iff_negative: "~P | ~Q | P=Q" |
wenzelm@21254 | 84 |
by blast |
wenzelm@21254 | 85 |
|
wenzelm@21254 | 86 |
use "Tools/res_axioms.ML" |
wenzelm@21254 | 87 |
use "Tools/res_hol_clause.ML" |
wenzelm@21254 | 88 |
use "Tools/res_atp.ML" |
wenzelm@21254 | 89 |
|
wenzelm@21254 | 90 |
setup ResAxioms.meson_method_setup |
wenzelm@21254 | 91 |
|
wenzelm@21254 | 92 |
|
wenzelm@21254 | 93 |
subsection {* Setup for Vampire, E prover and SPASS *} |
wenzelm@21254 | 94 |
|
wenzelm@21254 | 95 |
use "Tools/res_atp_provers.ML" |
wenzelm@21254 | 96 |
|
wenzelm@21254 | 97 |
oracle vampire_oracle ("string * int") = {* ResAtpProvers.vampire_o *} |
wenzelm@21254 | 98 |
oracle eprover_oracle ("string * int") = {* ResAtpProvers.eprover_o *} |
wenzelm@21254 | 99 |
oracle spass_oracle ("string * int") = {* ResAtpProvers.spass_o *} |
wenzelm@21254 | 100 |
|
wenzelm@21254 | 101 |
use "Tools/res_atp_methods.ML" |
wenzelm@21254 | 102 |
setup ResAtpMethods.ResAtps_setup |
wenzelm@21254 | 103 |
|
wenzelm@21254 | 104 |
end |