changeset 24827 646bdc51eb7d parent 24819 7d8e0a47392e child 24943 5f5679e2ec2f
```--- a/src/HOL/ATP_Linkup.thy	Wed Oct 03 22:33:17 2007 +0200
+++ b/src/HOL/ATP_Linkup.thy	Thu Oct 04 12:32:58 2007 +0200
@@ -56,24 +56,6 @@
lemma equal_imp_fequal: "X=Y ==> fequal X Y"

-lemma K_simp: "COMBK P == (%Q. P)"
-apply (rule eq_reflection)
-apply (rule ext)
-done
-
-lemma I_simp: "COMBI == (%P. P)"
-apply (rule eq_reflection)
-apply (rule ext)
-done
-
-lemma B_simp: "COMBB P Q == %R. P (Q R)"
-apply (rule eq_reflection)
-apply (rule ext)
-done
-
text{*These two represent the equivalence between Boolean equality and iff.
They can't be converted to clauses automatically, as the iff would be
expanded...*}
@@ -84,8 +66,41 @@
lemma iff_negative: "~P | ~Q | P=Q"
by blast

+text{*Theorems for translation to combinators*}
+
+lemma abs_S: "(%x. (f x) (g x)) == COMBS f g"
+apply (rule eq_reflection)
+apply (rule ext)
+done
+
+lemma abs_I: "(%x. x) == COMBI"
+apply (rule eq_reflection)
+apply (rule ext)
+done
+
+lemma abs_K: "(%x. y) == COMBK y"
+apply (rule eq_reflection)
+apply (rule ext)
+done
+
+lemma abs_B: "(%x. a (g x)) == COMBB a g"
+apply (rule eq_reflection)
+apply (rule ext)
+done
+
+lemma abs_C: "(%x. (f x) b) == COMBC f b"
+apply (rule eq_reflection)
+apply (rule ext)
+done
+
+
use "Tools/res_axioms.ML"      --{*requires the combinators declared above*}
-use "Tools/res_hol_clause.ML"  --{*requires the combinators*}
+use "Tools/res_hol_clause.ML"
use "Tools/res_reconstruct.ML"
use "Tools/watcher.ML"
use "Tools/res_atp.ML"
@@ -102,17 +117,14 @@
oracle spass_oracle ("string * int") = {* ResAtpProvers.spass_o *}

use "Tools/res_atp_methods.ML"
-setup ResAtpMethods.setup
-
+setup ResAtpMethods.setup      --{*Oracle ATP methods: still useful?*}
+setup ResAxioms.setup          --{*Sledgehammer*}

subsection {* The Metis prover *}

use "Tools/metis_tools.ML"
setup MetisTools.setup

-(*Sledgehammer*)
-setup ResAxioms.setup
-
setup {*
Theory.at_end ResAxioms.clause_cache_endtheory
*}```