author  paulson 
Thu, 10 Nov 2005 17:33:14 +0100  
changeset 18144  4edcb5fdc3b0 
parent 18141  89e2e8bed08f 
child 18198  95330fc0ea8d 
permissions  rwrr 
15347  1 
(* Author: Jia Meng, Cambridge University Computer Laboratory 
2 
ID: $Id$ 

3 
Copyright 2004 University of Cambridge 

4 

5 
Transformation of axiom rules (elim/intro/etc) into CNF forms. 

6 
*) 

7 

15997  8 
signature RES_AXIOMS = 
9 
sig 

10 
exception ELIMR2FOL of string 

17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

11 
val tagging_enabled : bool 
15997  12 
val elimRule_tac : thm > Tactical.tactic 
16012  13 
val elimR2Fol : thm > term 
15997  14 
val transform_elim : thm > thm 
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
16012
diff
changeset

15 
val clausify_axiom_pairs : (string*thm) > (ResClause.clause*thm) list 
18000
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

16 
val clausify_axiom_pairsH : (string*thm) > (ResHolClause.clause*thm) list 
15997  17 
val cnf_axiom : (string * thm) > thm list 
18000
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

18 
val cnf_axiomH : (string * thm) > thm list 
15997  19 
val meta_cnf_axiom : thm > thm list 
18000
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

20 
val meta_cnf_axiomH : thm > thm list 
15997  21 
val claset_rules_of_thy : theory > (string * thm) list 
22 
val simpset_rules_of_thy : theory > (string * thm) list 

17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

23 
val claset_rules_of_ctxt: Proof.context > (string * thm) list 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

24 
val simpset_rules_of_ctxt : Proof.context > (string * thm) list 
17829  25 
val clausify_rules_pairs : (string*thm) list > (ResClause.clause*thm) list list 
18000
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

26 
val clausify_rules_pairsH : (string*thm) list > (ResHolClause.clause*thm) list list 
16563  27 
val clause_setup : (theory > theory) list 
28 
val meson_method_setup : (theory > theory) list 

17905
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
17829
diff
changeset

29 
val pairname : thm > (string * thm) 
18000
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

30 
val repeat_RS : thm > thm > thm 
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

31 

15997  32 
end; 
15347  33 

18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

34 
structure ResAxioms (*: RES_AXIOMS*) = 
15997  35 

36 
struct 

15347  37 

18000
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

38 

17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

39 
val tagging_enabled = false (*compile_time option*) 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

40 

15997  41 
(**** Transformation of Elimination Rules into FirstOrder Formulas****) 
15347  42 

15390  43 
(* a tactic used to prove an elimrule. *) 
16009  44 
fun elimRule_tac th = 
45 
((rtac impI 1) ORELSE (rtac notI 1)) THEN (etac th 1) THEN 

16588  46 
REPEAT(fast_tac HOL_cs 1); 
15347  47 

48 
exception ELIMR2FOL of string; 

49 

15390  50 
(* functions used to construct a formula *) 
51 

15347  52 
fun make_disjs [x] = x 
15956  53 
 make_disjs (x :: xs) = HOLogic.mk_disj(x, make_disjs xs) 
15347  54 

55 
fun make_conjs [x] = x 

15956  56 
 make_conjs (x :: xs) = HOLogic.mk_conj(x, make_conjs xs) 
57 

58 
fun add_EX tm [] = tm 

59 
 add_EX tm ((x,xtp)::xs) = add_EX (HOLogic.exists_const xtp $ Abs(x,xtp,tm)) xs; 

15347  60 

61 

62 

15956  63 
fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_))) (Const("Trueprop",_) $ Free(q,_)) = (p = q) 
15371  64 
 is_neg _ _ = false; 
65 

15347  66 

67 
exception STRIP_CONCL; 

68 

69 

15371  70 
fun strip_concl' prems bvs (Const ("==>",_) $ P $ Q) = 
15956  71 
let val P' = HOLogic.dest_Trueprop P 
72 
val prems' = P'::prems 

73 
in 

15371  74 
strip_concl' prems' bvs Q 
15956  75 
end 
15371  76 
 strip_concl' prems bvs P = 
15956  77 
let val P' = HOLogic.Not $ (HOLogic.dest_Trueprop P) 
78 
in 

15371  79 
add_EX (make_conjs (P'::prems)) bvs 
15956  80 
end; 
15371  81 

82 

18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

83 
fun strip_concl prems bvs concl (Const ("all", _) $ Abs (x,xtp,body)) = 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

84 
strip_concl prems ((x,xtp)::bvs) concl body 
15371  85 
 strip_concl prems bvs concl (Const ("==>",_) $ P $ Q) = 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

86 
if (is_neg P concl) then (strip_concl' prems bvs Q) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

87 
else strip_concl (HOLogic.dest_Trueprop P::prems) bvs concl Q 
15371  88 
 strip_concl prems bvs concl _ = add_EX (make_conjs prems) bvs; 
15347  89 

90 

15371  91 
fun trans_elim (main,others,concl) = 
92 
let val others' = map (strip_concl [] [] concl) others 

15347  93 
val disjs = make_disjs others' 
94 
in 

15956  95 
HOLogic.mk_imp (HOLogic.dest_Trueprop main, disjs) 
15347  96 
end; 
97 

98 

15390  99 
(* aux function of elim2Fol, take away predicate variable. *) 
15371  100 
fun elimR2Fol_aux prems concl = 
15347  101 
let val nprems = length prems 
102 
val main = hd prems 

103 
in 

15956  104 
if (nprems = 1) then HOLogic.Not $ (HOLogic.dest_Trueprop main) 
15371  105 
else trans_elim (main, tl prems, concl) 
15347  106 
end; 
107 

15956  108 

16012  109 
(* convert an elim rule into an equivalent formula, of type term. *) 
15347  110 
fun elimR2Fol elimR = 
111 
let val elimR' = Drule.freeze_all elimR 

112 
val (prems,concl) = (prems_of elimR', concl_of elimR') 

113 
in 

114 
case concl of Const("Trueprop",_) $ Free(_,Type("bool",[])) 

15956  115 
=> HOLogic.mk_Trueprop (elimR2Fol_aux prems concl) 
116 
 Free(x,Type("prop",[])) => HOLogic.mk_Trueprop(elimR2Fol_aux prems concl) 

15347  117 
 _ => raise ELIMR2FOL("Not an elimination rule!") 
118 
end; 

119 

120 

15390  121 
(* check if a rule is an elim rule *) 
16009  122 
fun is_elimR th = 
123 
case (concl_of th) of (Const ("Trueprop", _) $ Var (idx,_)) => true 

15347  124 
 Var(indx,Type("prop",[])) => true 
125 
 _ => false; 

126 

15997  127 
(* convert an elimrule into an equivalent theorem that does not have the 
128 
predicate variable. Leave other theorems unchanged.*) 

16009  129 
fun transform_elim th = 
130 
if is_elimR th then 

131 
let val tm = elimR2Fol th 

132 
val ctm = cterm_of (sign_of_thm th) tm 

18009  133 
in Goal.prove_raw [] ctm (fn _ => elimRule_tac th) end 
16563  134 
else th; 
15997  135 

136 

137 
(**** Transformation of Clasets and Simpsets into FirstOrder Axioms ****) 

138 

15390  139 
(* repeated resolution *) 
15347  140 
fun repeat_RS thm1 thm2 = 
141 
let val thm1' = thm1 RS thm2 handle THM _ => thm1 

142 
in 

143 
if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2) 

144 
end; 

145 

146 

16009  147 
(*Convert a theorem into NNF and also skolemize it. Original version, using 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

148 
Hilbert's epsilon in the resulting clauses. FIXME DELETE*) 
18000
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

149 
fun skolem_axiom_g mk_nnf th = 
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

150 
let val th' = (skolemize o mk_nnf o ObjectLogic.atomize_thm o Drule.freeze_all) th 
16588  151 
in repeat_RS th' someI_ex 
152 
end; 

15347  153 

154 

16563  155 
(*Transfer a theorem into theory Reconstruction.thy if it is not already 
15359
8bad1f42fec0
new CLAUSIFY attribute for proof reconstruction with lemmas
paulson
parents:
15347
diff
changeset

156 
inside that theory  because it's needed for Skolemization *) 
8bad1f42fec0
new CLAUSIFY attribute for proof reconstruction with lemmas
paulson
parents:
15347
diff
changeset

157 

16563  158 
(*This will refer to the final version of theory Reconstruction.*) 
159 
val recon_thy_ref = Theory.self_ref (the_context ()); 

15359
8bad1f42fec0
new CLAUSIFY attribute for proof reconstruction with lemmas
paulson
parents:
15347
diff
changeset

160 

16563  161 
(*If called while Reconstruction is being created, it will transfer to the 
162 
current version. If called afterward, it will transfer to the final version.*) 

16009  163 
fun transfer_to_Reconstruction th = 
16563  164 
transfer (Theory.deref recon_thy_ref) th handle THM _ => th; 
15347  165 

15955
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset

166 
fun is_taut th = 
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset

167 
case (prop_of th) of 
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset

168 
(Const ("Trueprop", _) $ Const ("True", _)) => true 
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset

169 
 _ => false; 
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset

170 

87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset

171 
(* remove tautologous clauses *) 
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset

172 
val rm_redundant_cls = List.filter (not o is_taut); 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

173 

15997  174 

16009  175 
(**** SKOLEMIZATION BY INFERENCE (lcp) ****) 
176 

18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

177 
(*Traverse a theorem, declaring Skolem function definitions. String s is the suggested 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

178 
prefix for the Skolem constant. Result is a new theory*) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

179 
fun declare_skofuns s th thy = 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

180 
let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (n, (thy, axs)) = 
16009  181 
(*Existential: declare a Skolem function, then insert into body and continue*) 
182 
let val cname = s ^ "_" ^ Int.toString n 

16012  183 
val args = term_frees xtp (*get the formal parameter list*) 
16009  184 
val Ts = map type_of args 
185 
val cT = Ts > T 

18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

186 
val c = Const (Sign.full_name thy cname, cT) 
16009  187 
val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp) 
16012  188 
(*Forms a lambdaabstraction over the formal parameters*) 
16009  189 
val def = equals cT $ c $ rhs 
190 
val thy' = Theory.add_consts_i [(cname, cT, NoSyn)] thy 

16012  191 
(*Theory is augmented with the constant, then its def*) 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

192 
val cdef = cname ^ "_def" 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

193 
val thy'' = Theory.add_defs_i false [(cdef, def)] thy' 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

194 
in dec_sko (subst_bound (list_comb(c,args), p)) 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

195 
(n+1, (thy'', get_axiom thy'' cdef :: axs)) 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

196 
end 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

197 
 dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) (n, thx) = 
16012  198 
(*Universal quant: insert a free variable into body and continue*) 
16009  199 
let val fname = variant (add_term_names (p,[])) a 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

200 
in dec_sko (subst_bound (Free(fname,T), p)) (n, thx) end 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

201 
 dec_sko (Const ("op &", _) $ p $ q) nthy = dec_sko q (dec_sko p nthy) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

202 
 dec_sko (Const ("op ", _) $ p $ q) nthy = dec_sko q (dec_sko p nthy) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

203 
 dec_sko (Const ("HOL.tag", _) $ p) nthy = dec_sko p nthy 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

204 
 dec_sko (Const ("Trueprop", _) $ p) nthy = dec_sko p nthy 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

205 
 dec_sko t nthx = nthx (*Do nothing otherwise*) 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

206 
in #2 (dec_sko (#prop (rep_thm th)) (1, (thy,[]))) end; 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

207 

89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

208 
(*Traverse a theorem, accumulating Skolem function definitions.*) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

209 
fun assume_skofuns th = 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

210 
let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs = 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

211 
(*Existential: declare a Skolem function, then insert into body and continue*) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

212 
let val name = variant (add_term_names (p,[])) (gensym "sko_") 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

213 
val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

214 
val args = term_frees xtp \\ skos (*the formal parameters*) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

215 
val Ts = map type_of args 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

216 
val cT = Ts > T 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

217 
val c = Free (name, cT) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

218 
val rhs = list_abs_free (map dest_Free args, 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

219 
HOLogic.choice_const T $ xtp) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

220 
(*Forms a lambdaabstraction over the formal parameters*) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

221 
val def = equals cT $ c $ rhs 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

222 
in dec_sko (subst_bound (list_comb(c,args), p)) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

223 
(def :: defs) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

224 
end 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

225 
 dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) defs = 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

226 
(*Universal quant: insert a free variable into body and continue*) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

227 
let val fname = variant (add_term_names (p,[])) a 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

228 
in dec_sko (subst_bound (Free(fname,T), p)) defs end 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

229 
 dec_sko (Const ("op &", _) $ p $ q) defs = dec_sko q (dec_sko p defs) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

230 
 dec_sko (Const ("op ", _) $ p $ q) defs = dec_sko q (dec_sko p defs) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

231 
 dec_sko (Const ("HOL.tag", _) $ p) defs = dec_sko p defs 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

232 
 dec_sko (Const ("Trueprop", _) $ p) defs = dec_sko p defs 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

233 
 dec_sko t defs = defs (*Do nothing otherwise*) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

234 
in dec_sko (#prop (rep_thm th)) [] end; 
16009  235 

236 
(*cterms are used throughout for efficiency*) 

18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

237 
val cTrueprop = Thm.cterm_of HOL.thy HOLogic.Trueprop; 
16009  238 

239 
(*cterm version of mk_cTrueprop*) 

240 
fun c_mkTrueprop A = Thm.capply cTrueprop A; 

241 

242 
(*Given an abstraction over n variables, replace the bound variables by free 

243 
ones. Return the body, along with the list of free variables.*) 

244 
fun c_variant_abs_multi (ct0, vars) = 

245 
let val (cv,ct) = Thm.dest_abs NONE ct0 

246 
in c_variant_abs_multi (ct, cv::vars) end 

247 
handle CTERM _ => (ct0, rev vars); 

248 

249 
(*Given the definition of a Skolem function, return a theorem to replace 

18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

250 
an existential formula by a use of that function. 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

251 
Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *) 
16588  252 
fun skolem_of_def def = 
16009  253 
let val (c,rhs) = Drule.dest_equals (cprop_of (Drule.freeze_all def)) 
254 
val (ch, frees) = c_variant_abs_multi (rhs, []) 

18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

255 
val (chilbert,cabs) = Thm.dest_comb ch 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

256 
val {sign,t, ...} = rep_cterm chilbert 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

257 
val T = case t of Const ("Hilbert_Choice.Eps", Type("fun",[_,T])) => T 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

258 
 _ => raise THM ("skolem_of_def: expected Eps", 0, [def]) 
16009  259 
val cex = Thm.cterm_of sign (HOLogic.exists_const T) 
260 
val ex_tm = c_mkTrueprop (Thm.capply cex cabs) 

261 
and conc = c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees))); 

18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

262 
fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS someI_ex) 1 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

263 
in Goal.prove_raw [ex_tm] conc tacf 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

264 
> forall_intr_list frees 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

265 
> forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

266 
> Thm.varifyT 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

267 
end; 
16009  268 

18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

269 
(*Converts an Isabelle theorem (intro, elim or simp format) into nnf. 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

270 
FIXME: generalize so that it works for HOL too!!*) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

271 
fun to_nnf th = 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

272 
th > transfer_to_Reconstruction 
16588  273 
> transform_elim > Drule.freeze_all 
274 
> ObjectLogic.atomize_thm > make_nnf; 

16009  275 

276 
(*The cache prevents repeated clausification of a theorem, 

16800  277 
and also repeated declaration of Skolem functions*) (* FIXME better use Termtab!? *) 
15955
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset

278 
val clause_cache = ref (Symtab.empty : (thm * thm list) Symtab.table) 
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset

279 

18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

280 

89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

281 
(*Generate Skolem functions for a theorem supplied in nnf*) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

282 
fun skolem_of_nnf th = 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

283 
map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns th); 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

284 

89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

285 
(*Skolemize a named theorem, returning a modified theory. NONE can occur if the 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

286 
theorem is not firstorder.*) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

287 
fun skolem_thm th = 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

288 
Option.map (fn nnfth => Meson.make_cnf (skolem_of_nnf nnfth) nnfth) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

289 
(SOME (to_nnf th) handle THM _ => NONE); 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

290 

16009  291 
(*Declare Skolem functions for a theorem, supplied in nnf and with its name*) 
292 
fun skolem thy (name,th) = 

16588  293 
let val cname = (case name of "" => gensym "sko"  s => Sign.base_name s) 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

294 
in Option.map 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

295 
(fn nnfth => 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

296 
let val (thy',defs) = declare_skofuns cname nnfth thy 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

297 
val skoths = map skolem_of_def defs 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

298 
in (thy', Meson.make_cnf skoths nnfth) end) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

299 
(SOME (to_nnf th) handle THM _ => NONE) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

300 
end; 
16009  301 

302 
(*Populate the clause cache using the supplied theorems*) 

18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

303 
fun skolem_cache ((name,th), thy) = 
18144
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

304 
case Symtab.lookup (!clause_cache) name of 
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

305 
NONE => 
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

306 
(case skolem thy (name, Thm.transfer thy th) of 
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

307 
NONE => thy 
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

308 
 SOME (thy',cls) => 
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

309 
(change clause_cache (Symtab.update (name, (th, cls))); thy')) 
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

310 
 SOME (th',cls) => 
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

311 
if eq_thm(th,th') then thy 
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

312 
else (warning ("skolem_cache: Ignoring variant of theorem " ^ name); 
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

313 
warning (string_of_thm th); 
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

314 
warning (string_of_thm th'); 
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

315 
thy); 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

316 

16009  317 

318 
(*Exported function to convert Isabelle theorems into axiom clauses*) 

18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

319 
fun cnf_axiom_g cnf (name,th) = 
18144
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

320 
case name of 
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

321 
"" => cnf th (*no name, so can't cache*) 
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

322 
 s => case Symtab.lookup (!clause_cache) s of 
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

323 
NONE => 
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

324 
let val cls = cnf th 
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

325 
in change clause_cache (Symtab.update (s, (th, cls))); cls end 
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

326 
 SOME(th',cls) => 
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

327 
if eq_thm(th,th') then cls 
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

328 
else (warning ("cnf_axiom: duplicate or variant of theorem " ^ name); 
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

329 
warning (string_of_thm th); 
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

330 
warning (string_of_thm th'); 
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

331 
cls); 
15347  332 

18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

333 
fun pairname th = (Thm.name_of_thm th, th); 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

334 

89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

335 
val skolem_axiomH = skolem_axiom_g make_nnf1; 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

336 

89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

337 
fun cnf_ruleH th = make_clauses [skolem_axiomH (transform_elim th)]; 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

338 

89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

339 
(* transform an Isabelle theorem into CNF *) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

340 
fun cnf_axiom_aux_g cnf_rule th = 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

341 
map zero_var_indexes 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

342 
(rm_redundant_cls (cnf_rule (transfer_to_Reconstruction th))); 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

343 

89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

344 
val cnf_axiom_auxH = cnf_axiom_aux_g cnf_ruleH; 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

345 

89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

346 
(*NONE can occur if th fails the firstorder check.*) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

347 
fun cnf_axiom_aux th = Option.getOpt (skolem_thm th, []); 
18000
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

348 

ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

349 
val cnf_axiom = cnf_axiom_g cnf_axiom_aux; 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

350 

18000
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

351 
val cnf_axiomH = cnf_axiom_g cnf_axiom_auxH; 
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

352 

ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

353 

15956  354 
fun meta_cnf_axiom th = 
355 
map Meson.make_meta_clause (cnf_axiom (pairname th)); 

15499  356 

18000
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

357 
fun meta_cnf_axiomH th = 
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

358 
map Meson.make_meta_clause (cnf_axiomH (pairname th)); 
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

359 

15347  360 

361 

15872  362 
(**** Extract and Clausify theorems from a theory's claset and simpset ****) 
15347  363 

17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

364 
(*Preserve the name of "th" after the transformation "f"*) 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

365 
fun preserve_name f th = Thm.name_thm (Thm.name_of_thm th, f th); 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

366 

d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

367 
(*Tags identify the major premise or conclusion, as hints to resolution provers. 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

368 
However, they don't appear to help in recent tests, and they complicate the code.*) 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

369 
val tagI = thm "tagI"; 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

370 
val tagD = thm "tagD"; 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

371 

d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

372 
val tag_intro = preserve_name (fn th => th RS tagI); 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

373 
val tag_elim = preserve_name (fn th => tagD RS th); 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

374 

17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

375 
fun rules_of_claset cs = 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

376 
let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

377 
val intros = safeIs @ hazIs 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

378 
val elims = safeEs @ hazEs 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

379 
in 
17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

380 
debug ("rules_of_claset intros: " ^ Int.toString(length intros) ^ 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

381 
" elims: " ^ Int.toString(length elims)); 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

382 
if tagging_enabled 
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

383 
then map pairname (map tag_intro intros @ map tag_elim elims) 
17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

384 
else map pairname (intros @ elims) 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

385 
end; 
15347  386 

17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

387 
fun rules_of_simpset ss = 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

388 
let val ({rules,...}, _) = rep_ss ss 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

389 
val simps = Net.entries rules 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

390 
in 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

391 
debug ("rules_of_simpset: " ^ Int.toString(length simps)); 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

392 
map (fn r => (#name r, #thm r)) simps 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

393 
end; 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

394 

f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

395 
fun claset_rules_of_thy thy = rules_of_claset (claset_of thy); 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

396 
fun simpset_rules_of_thy thy = rules_of_simpset (simpset_of thy); 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

397 

f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

398 
fun claset_rules_of_ctxt ctxt = rules_of_claset (local_claset_of ctxt); 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset

399 
fun simpset_rules_of_ctxt ctxt = rules_of_simpset (local_simpset_of ctxt); 
15347  400 

401 

15872  402 
(**** Translate a set of classical/simplifier rules into CNF (still as type "thm") ****) 
15347  403 

404 
(* classical rules *) 

18000
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

405 
fun cnf_rules_g cnf_axiom [] err_list = ([],err_list) 
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

406 
 cnf_rules_g cnf_axiom ((name,th) :: ths) err_list = 
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

407 
let val (ts,es) = cnf_rules_g cnf_axiom ths err_list 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

408 
in (cnf_axiom (name,th) :: ts,es) handle _ => (ts, (th::es)) end; 
15347  409 

410 

18000
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

411 
val cnf_rules = cnf_rules_g cnf_axiom; 
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

412 
val cnf_rulesH = cnf_rules_g cnf_axiomH; 
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

413 

ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

414 

15872  415 
(**** Convert all theorems of a claset/simpset into clauses (ResClause.clause) ****) 
15347  416 

18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

417 
fun make_axiom_clauses _ _ [] = [] 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

418 
 make_axiom_clauses name i (cls::clss) = 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

419 
(ResClause.make_axiom_clause (prop_of cls) (name,i), cls) :: 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

420 
(make_axiom_clauses name (i+1) clss) 
18000
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

421 

17829  422 
(* outputs a list of (clause,theorem) pairs *) 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

423 
fun clausify_axiom_pairs (name,th) = 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

424 
filter (fn (c,th) => not (ResClause.isTaut c)) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

425 
(make_axiom_clauses name 0 (cnf_axiom (name,th))); 
18000
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

426 

18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

427 
fun make_axiom_clausesH _ _ [] = [] 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

428 
 make_axiom_clausesH name i (cls::clss) = 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

429 
(ResHolClause.make_axiom_clause (prop_of cls) (name,i), cls) :: 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

430 
(make_axiom_clausesH name (i+1) clss) 
18000
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

431 

18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

432 
fun clausify_axiom_pairsH (name,th) = 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

433 
filter (fn (c,th) => not (ResHolClause.isTaut c)) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

434 
(make_axiom_clausesH name 0 (cnf_axiomH (name,th))); 
18000
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

435 

ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

436 

17829  437 
fun clausify_rules_pairs_aux result [] = result 
438 
 clausify_rules_pairs_aux result ((name,th)::ths) = 

439 
clausify_rules_pairs_aux (clausify_axiom_pairs (name,th) :: result) ths 

440 
handle THM (msg,_,_) => 

441 
(debug ("Cannot clausify " ^ name ^ ": " ^ msg); 

442 
clausify_rules_pairs_aux result ths) 

443 
 ResClause.CLAUSE (msg,t) => 

444 
(debug ("Cannot clausify " ^ name ^ ": " ^ msg ^ 

445 
": " ^ TermLib.string_of_term t); 

446 
clausify_rules_pairs_aux result ths) 

17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

447 

18000
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

448 

ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

449 
fun clausify_rules_pairs_auxH result [] = result 
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

450 
 clausify_rules_pairs_auxH result ((name,th)::ths) = 
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

451 
clausify_rules_pairs_auxH (clausify_axiom_pairsH (name,th) :: result) ths 
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

452 
handle THM (msg,_,_) => 
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

453 
(debug ("Cannot clausify " ^ name ^ ": " ^ msg); 
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

454 
clausify_rules_pairs_auxH result ths) 
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

455 
 ResHolClause.LAM2COMB (t) => 
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

456 
(debug ("Cannot clausify " ^ TermLib.string_of_term t); 
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

457 
clausify_rules_pairs_auxH result ths) 
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
16012
diff
changeset

458 

15347  459 

18000
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

460 

ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

461 
val clausify_rules_pairs = clausify_rules_pairs_aux []; 
ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

462 

ac059afd6b86
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
mengj
parents:
17959
diff
changeset

463 
val clausify_rules_pairsH = clausify_rules_pairs_auxH []; 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

464 

16009  465 
(*Setup function: takes a theory and installs ALL simprules and claset rules 
466 
into the clause cache*) 

467 
fun clause_cache_setup thy = 

468 
let val simps = simpset_rules_of_thy thy 

469 
and clas = claset_rules_of_thy thy 

18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

470 
in List.foldl skolem_cache (List.foldl skolem_cache thy clas) simps end; 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

471 
(*Could be duplicate theorem names, due to multiple attributes*) 
16009  472 

16563  473 
val clause_setup = [clause_cache_setup]; 
474 

475 

476 
(*** meson proof methods ***) 

477 

478 
fun cnf_rules_of_ths ths = List.concat (#1 (cnf_rules (map pairname ths) [])); 

479 

480 
fun meson_meth ths ctxt = 

481 
Method.SIMPLE_METHOD' HEADGOAL 

482 
(CHANGED_PROP o Meson.meson_claset_tac (cnf_rules_of_ths ths) (local_claset_of ctxt)); 

483 

484 
val meson_method_setup = 

485 
[Method.add_methods 

486 
[("meson", Method.thms_ctxt_args meson_meth, 

487 
"The MESON resolution proof procedure")]]; 

15347  488 

489 
end; 