author  paulson 
Wed, 09 Nov 2005 18:01:33 +0100  
changeset 18141  89e2e8bed08f 
parent 18009  df077e122064 
child 18144  4edcb5fdc3b0 
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) = 
17412  304 
(case Symtab.lookup (!clause_cache) name of 
16009  305 
NONE => 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

306 
(case skolem thy (name, Thm.transfer thy th) of 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

307 
NONE => thy 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

308 
 SOME (thy',cls) => 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

309 
(change clause_cache (Symtab.update (name, (th, cls))); thy')) 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

310 
 SOME _ => thy); 
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

311 

16009  312 

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

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

314 
fun cnf_axiom_g cnf (name,th) = 
15956  315 
case name of 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

316 
"" => cnf th (*no name, so can't cache*) 
17412  317 
 s => case Symtab.lookup (!clause_cache) s of 
15955
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset

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

319 
let val cls = cnf th 
17412  320 
in change clause_cache (Symtab.update (s, (th, cls))); cls end 
15955
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset

321 
 SOME(th',cls) => 
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset

322 
if eq_thm(th,th') then cls 
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset

323 
else (*New theorem stored under the same name? Possible??*) 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

324 
let val cls = cnf th 
17412  325 
in change clause_cache (Symtab.update (s, (th, cls))); cls end; 
15347  326 

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

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

328 

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

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

330 

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

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

332 

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

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

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

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

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

337 

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

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

339 

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

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

341 
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

342 

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

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

344 

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

345 
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

346 

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

347 

15956  348 
fun meta_cnf_axiom th = 
349 
map Meson.make_meta_clause (cnf_axiom (pairname th)); 

15499  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 
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

352 
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

353 

15347  354 

355 

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

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

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

359 
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

360 

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

361 
(*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

362 
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

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

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

365 

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

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

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

368 

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

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

370 
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

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

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

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

374 
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

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

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

377 
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

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

379 
end; 
15347  380 

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

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

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

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

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

385 
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

386 
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

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

388 

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

389 
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

390 
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

391 

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

392 
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

393 
fun simpset_rules_of_ctxt ctxt = rules_of_simpset (local_simpset_of ctxt); 
15347  394 

395 

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

398 
(* 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

399 
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

400 
 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

401 
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

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

404 

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 
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

406 
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

407 

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

408 

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

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

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

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

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

414 
(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

415 

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

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

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

419 
(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

420 

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

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

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

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

424 
(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

425 

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

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

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

428 
(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

429 

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

430 

17829  431 
fun clausify_rules_pairs_aux result [] = result 
432 
 clausify_rules_pairs_aux result ((name,th)::ths) = 

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

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

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

436 
clausify_rules_pairs_aux result ths) 

437 
 ResClause.CLAUSE (msg,t) => 

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

439 
": " ^ TermLib.string_of_term t); 

440 
clausify_rules_pairs_aux result ths) 

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

441 

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

442 

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

443 
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

444 
 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

445 
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

446 
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

447 
(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

448 
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

449 
 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

450 
(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

451 
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

452 

15347  453 

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

454 

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 
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

456 

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 
val clausify_rules_pairsH = clausify_rules_pairs_auxH []; 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

458 

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

461 
fun clause_cache_setup thy = 

462 
let val simps = simpset_rules_of_thy thy 

463 
and clas = claset_rules_of_thy thy 

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

464 
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

465 
(*Could be duplicate theorem names, due to multiple attributes*) 
16009  466 

16563  467 
val clause_setup = [clause_cache_setup]; 
468 

469 

470 
(*** meson proof methods ***) 

471 

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

473 

474 
fun meson_meth ths ctxt = 

475 
Method.SIMPLE_METHOD' HEADGOAL 

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

477 

478 
val meson_method_setup = 

479 
[Method.add_methods 

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

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

15347  482 

483 
end; 