1 (* Title: HOL/ATP_Linkup.thy
2 Author: Lawrence C Paulson
3 Author: Jia Meng, NICTA
4 Author: Fabian Immler, TUM
7 header {* The Isabelle-ATP Linkup *}
10 imports Record Hilbert_Choice
14 ("Tools/res_axioms.ML")
15 ("Tools/res_hol_clause.ML")
16 ("Tools/res_reconstruct.ML")
18 ("Tools/atp_manager.ML")
19 ("Tools/atp_wrapper.ML")
20 "~~/src/Tools/Metis/metis.ML"
21 ("Tools/metis_tools.ML")
24 definition COMBI :: "'a => 'a"
27 definition COMBK :: "'a => 'b => 'a"
28 where "COMBK P Q == P"
30 definition COMBB :: "('b => 'c) => ('a => 'b) => 'a => 'c"
31 where "COMBB P Q R == P (Q R)"
33 definition COMBC :: "('a => 'b => 'c) => 'b => 'a => 'c"
34 where "COMBC P Q R == P R Q"
36 definition COMBS :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c"
37 where "COMBS P Q R == P R (Q R)"
39 definition fequal :: "'a => 'a => bool"
40 where "fequal X Y == (X=Y)"
42 lemma fequal_imp_equal: "fequal X Y ==> X=Y"
43 by (simp add: fequal_def)
45 lemma equal_imp_fequal: "X=Y ==> fequal X Y"
46 by (simp add: fequal_def)
48 text{*These two represent the equivalence between Boolean equality and iff.
49 They can't be converted to clauses automatically, as the iff would be
52 lemma iff_positive: "P | Q | P=Q"
55 lemma iff_negative: "~P | ~Q | P=Q"
58 text{*Theorems for translation to combinators*}
60 lemma abs_S: "(%x. (f x) (g x)) == COMBS f g"
61 apply (rule eq_reflection)
63 apply (simp add: COMBS_def)
66 lemma abs_I: "(%x. x) == COMBI"
67 apply (rule eq_reflection)
69 apply (simp add: COMBI_def)
72 lemma abs_K: "(%x. y) == COMBK y"
73 apply (rule eq_reflection)
75 apply (simp add: COMBK_def)
78 lemma abs_B: "(%x. a (g x)) == COMBB a g"
79 apply (rule eq_reflection)
81 apply (simp add: COMBB_def)
84 lemma abs_C: "(%x. (f x) b) == COMBC f b"
85 apply (rule eq_reflection)
87 apply (simp add: COMBC_def)
91 subsection {* Setup of external ATPs *}
93 use "Tools/res_axioms.ML" setup ResAxioms.setup
94 use "Tools/res_hol_clause.ML"
95 use "Tools/res_reconstruct.ML" setup ResReconstruct.setup
96 use "Tools/res_atp.ML"
98 use "Tools/atp_manager.ML"
99 use "Tools/atp_wrapper.ML"
101 text {* basic provers *}
102 setup {* AtpManager.add_prover "spass" AtpWrapper.spass *}
103 setup {* AtpManager.add_prover "vampire" AtpWrapper.vampire *}
104 setup {* AtpManager.add_prover "e" AtpWrapper.eprover *}
106 text {* provers with stuctured output *}
107 setup {* AtpManager.add_prover "vampire_full" AtpWrapper.vampire_full *}
108 setup {* AtpManager.add_prover "e_full" AtpWrapper.eprover_full *}
110 text {* on some problems better results *}
111 setup {* AtpManager.add_prover "spass_no_tc" (AtpWrapper.spass_opts 40 false) *}
113 text {* remote provers via SystemOnTPTP *}
114 setup {* AtpManager.add_prover "remote_vampire"
115 (AtpWrapper.remote_prover "-s Vampire---9.0") *}
116 setup {* AtpManager.add_prover "remote_spass"
117 (AtpWrapper.remote_prover "-s SPASS---3.01") *}
118 setup {* AtpManager.add_prover "remote_e"
119 (AtpWrapper.remote_prover "-s EP---1.0") *}
123 subsection {* The Metis prover *}
125 use "Tools/metis_tools.ML"
126 setup MetisTools.setup