author  wenzelm 
Thu, 19 Jan 2006 21:22:08 +0100  
changeset 18708  4b3dadb4fe33 
parent 18680  677e2bdd75f0 
child 18728  6790126ab5f6 
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 
18 
val meta_cnf_axiom : thm > thm list 

19 
val claset_rules_of_thy : theory > (string * thm) list 

20 
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

21 
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

22 
val simpset_rules_of_ctxt : Proof.context > (string * thm) list 
17829  23 
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

24 
val clausify_rules_pairsH : (string*thm) list > (ResHolClause.clause*thm) list 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

25 
val pairname : thm > (string * thm) 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

26 
val skolem_thm : thm > thm list 
18274
bbca1d2da0e9
Added two functions for CNF translation, used by other files.
mengj
parents:
18198
diff
changeset

27 
val cnf_rules1 : (string * thm) list > string list > (string * thm list) list * string list 
bbca1d2da0e9
Added two functions for CNF translation, used by other files.
mengj
parents:
18198
diff
changeset

28 
val cnf_rules2 : (string * thm) list > string list > (string * term list) list * string list 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

29 

18708  30 
val meson_method_setup : theory > theory 
31 
val setup : theory > theory 

15997  32 
end; 
15347  33 

18198
95330fc0ea8d
 combined common CNF functions used by HOL and FOL axioms, the difference between conversion of HOL and FOL theorems only comes in when theorems are converted to ResClause.clause or ResHolClause.clause format.
mengj
parents:
18144
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 

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

15347  64 

65 
exception STRIP_CONCL; 

66 

67 

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

71 
in 

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

15371  77 
add_EX (make_conjs (P'::prems)) bvs 
15956  78 
end; 
15371  79 

80 

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

81 
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

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

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

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

88 

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

15347  91 
val disjs = make_disjs others' 
92 
in 

15956  93 
HOLogic.mk_imp (HOLogic.dest_Trueprop main, disjs) 
15347  94 
end; 
95 

96 

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

101 
in 

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

15956  106 

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

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

111 
in 

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

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

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

117 

118 

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

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

124 

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

16009  127 
fun transform_elim th = 
128 
if is_elimR th then 

129 
let val tm = elimR2Fol th 

130 
val ctm = cterm_of (sign_of_thm th) tm 

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

134 

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

136 

15347  137 

16563  138 
(*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

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

140 

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

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

143 

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

16009  146 
fun transfer_to_Reconstruction th = 
16563  147 
transfer (Theory.deref recon_thy_ref) th handle THM _ => th; 
15347  148 

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

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

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

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

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

153 

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

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

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

156 

15997  157 

16009  158 
(**** SKOLEMIZATION BY INFERENCE (lcp) ****) 
159 

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

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

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

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

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

16012  166 
val args = term_frees xtp (*get the formal parameter list*) 
16009  167 
val Ts = map type_of args 
168 
val cT = Ts > T 

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

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

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

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

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

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

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

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

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

183 
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

184 
 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

185 
 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

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

187 
 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

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

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

190 

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

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

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

193 
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

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

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

196 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

212 
 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

213 
 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

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

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

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

217 
in dec_sko (#prop (rep_thm th)) [] end; 
16009  218 

219 
(*cterms are used throughout for efficiency*) 

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

220 
val cTrueprop = Thm.cterm_of HOL.thy HOLogic.Trueprop; 
16009  221 

222 
(*cterm version of mk_cTrueprop*) 

223 
fun c_mkTrueprop A = Thm.capply cTrueprop A; 

224 

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

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

227 
fun c_variant_abs_multi (ct0, vars) = 

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

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

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

231 

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

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

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

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

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

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

240 
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

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

244 
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

245 
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

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

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

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

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

250 
end; 
16009  251 

18198
95330fc0ea8d
 combined common CNF functions used by HOL and FOL axioms, the difference between conversion of HOL and FOL theorems only comes in when theorems are converted to ResClause.clause or ResHolClause.clause format.
mengj
parents:
18144
diff
changeset

252 
(*Converts an Isabelle theorem (intro, elim or simp format) into nnf.*) 
95330fc0ea8d
 combined common CNF functions used by HOL and FOL axioms, the difference between conversion of HOL and FOL theorems only comes in when theorems are converted to ResClause.clause or ResHolClause.clause format.
mengj
parents:
18144
diff
changeset

253 
(*It now works for HOL too. *) 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

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

255 
th > transfer_to_Reconstruction 
16588  256 
> transform_elim > Drule.freeze_all 
257 
> ObjectLogic.atomize_thm > make_nnf; 

16009  258 

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

18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

260 
and also repeated declaration of Skolem functions*) 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

261 
(* FIXME better use Termtab!? No, we MUST use theory data!!*) 
15955
87cf2ce8ede8
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents:
15872
diff
changeset

262 
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

263 

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

264 

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

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

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

267 
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

268 

18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

269 
(*Skolemize a named theorem, with Skolem functions as additional premises.*) 
18198
95330fc0ea8d
 combined common CNF functions used by HOL and FOL axioms, the difference between conversion of HOL and FOL theorems only comes in when theorems are converted to ResClause.clause or ResHolClause.clause format.
mengj
parents:
18144
diff
changeset

270 
(*also works for HOL*) 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

271 
fun skolem_thm th = 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

272 
let val nnfth = to_nnf th 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

273 
in Meson.make_cnf (skolem_of_nnf nnfth) nnfth 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

274 
end 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

275 
handle THM _ => []; 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

276 

18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

277 
(*Declare Skolem functions for a theorem, supplied in nnf and with its name. 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

278 
It returns a modified theory, unless skolemization fails.*) 
16009  279 
fun skolem thy (name,th) = 
16588  280 
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

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

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

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

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

285 
in (thy', Meson.make_cnf skoths nnfth) end) 
18198
95330fc0ea8d
 combined common CNF functions used by HOL and FOL axioms, the difference between conversion of HOL and FOL theorems only comes in when theorems are converted to ResClause.clause or ResHolClause.clause format.
mengj
parents:
18144
diff
changeset

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

287 
end; 
16009  288 

18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

289 
(*Populate the clause cache using the supplied theorem. Return the clausal form 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

290 
and modified theory.*) 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

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

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

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

294 
(case skolem thy (name, Thm.transfer thy th) of 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

295 
NONE => ([th],thy) 
18144
4edcb5fdc3b0
duplicate axioms in ATP linkup, and general fixes
paulson
parents:
18141
diff
changeset

296 
 SOME (thy',cls) => 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

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

298 
 SOME (th',cls) => 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

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

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

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

302 
warning (string_of_thm th'); 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

303 
([th],thy)); 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

304 

0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

305 
fun skolem_cache ((name,th), thy) = #2 (skolem_cache_thm ((name,th), thy)); 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

306 

16009  307 

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

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

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

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

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

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

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

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

315 
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

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

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

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

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

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

321 
cls); 
15347  322 

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

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

324 

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

325 

18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

326 
val cnf_axiom = cnf_axiom_g skolem_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

327 

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

328 

15956  329 
fun meta_cnf_axiom th = 
330 
map Meson.make_meta_clause (cnf_axiom (pairname th)); 

15499  331 

15347  332 

333 

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

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

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

337 
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

338 

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

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

340 
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

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

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

343 

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

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

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

346 

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

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

348 
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

349 
val intros = safeIs @ hazIs 
18532  350 
val elims = map Classical.classical_rule (safeEs @ hazEs) 
17404
d16c3a62c396
the experimental tagging system, and the usual tidying
paulson
parents:
17279
diff
changeset

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

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

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

355 
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

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

357 
end; 
15347  358 

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

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

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

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

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

364 
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

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

366 

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

367 
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

368 
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

369 

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

370 
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

371 
fun simpset_rules_of_ctxt ctxt = rules_of_simpset (local_simpset_of ctxt); 
15347  372 

373 

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

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

377 
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

378 
 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

379 
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

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

382 

18198
95330fc0ea8d
 combined common CNF functions used by HOL and FOL axioms, the difference between conversion of HOL and FOL theorems only comes in when theorems are converted to ResClause.clause or ResHolClause.clause format.
mengj
parents:
18144
diff
changeset

383 
(*works for both FOL and HOL*) 
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

384 
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

385 

18274
bbca1d2da0e9
Added two functions for CNF translation, used by other files.
mengj
parents:
18198
diff
changeset

386 
fun cnf_rules1 [] err_list = ([],err_list) 
bbca1d2da0e9
Added two functions for CNF translation, used by other files.
mengj
parents:
18198
diff
changeset

387 
 cnf_rules1 ((name,th) :: ths) err_list = 
bbca1d2da0e9
Added two functions for CNF translation, used by other files.
mengj
parents:
18198
diff
changeset

388 
let val (ts,es) = cnf_rules1 ths err_list 
bbca1d2da0e9
Added two functions for CNF translation, used by other files.
mengj
parents:
18198
diff
changeset

389 
in 
bbca1d2da0e9
Added two functions for CNF translation, used by other files.
mengj
parents:
18198
diff
changeset

390 
((name,cnf_axiom (name,th)) :: ts,es) handle _ => (ts,(name::es)) end; 
bbca1d2da0e9
Added two functions for CNF translation, used by other files.
mengj
parents:
18198
diff
changeset

391 

bbca1d2da0e9
Added two functions for CNF translation, used by other files.
mengj
parents:
18198
diff
changeset

392 
fun cnf_rules2 [] err_list = ([],err_list) 
bbca1d2da0e9
Added two functions for CNF translation, used by other files.
mengj
parents:
18198
diff
changeset

393 
 cnf_rules2 ((name,th) :: ths) err_list = 
bbca1d2da0e9
Added two functions for CNF translation, used by other files.
mengj
parents:
18198
diff
changeset

394 
let val (ts,es) = cnf_rules2 ths err_list 
bbca1d2da0e9
Added two functions for CNF translation, used by other files.
mengj
parents:
18198
diff
changeset

395 
in 
bbca1d2da0e9
Added two functions for CNF translation, used by other files.
mengj
parents:
18198
diff
changeset

396 
((name,map prop_of (cnf_axiom (name,th))) :: ts,es) handle _ => (ts,(name::es)) end; 
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

397 

18198
95330fc0ea8d
 combined common CNF functions used by HOL and FOL axioms, the difference between conversion of HOL and FOL theorems only comes in when theorems are converted to ResClause.clause or ResHolClause.clause format.
mengj
parents:
18144
diff
changeset

398 
(**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****) 
15347  399 

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

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

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

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

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

404 

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

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

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

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

409 

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

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

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

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

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

414 

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

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

416 
filter (fn (c,th) => not (ResHolClause.isTaut c)) 
18198
95330fc0ea8d
 combined common CNF functions used by HOL and FOL axioms, the difference between conversion of HOL and FOL theorems only comes in when theorems are converted to ResClause.clause or ResHolClause.clause format.
mengj
parents:
18144
diff
changeset

417 
(make_axiom_clausesH 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

418 

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

419 

17829  420 
fun clausify_rules_pairs_aux result [] = result 
421 
 clausify_rules_pairs_aux result ((name,th)::ths) = 

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

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

18680  424 
(Output.debug ("Cannot clausify " ^ name ^ ": " ^ msg); 
17829  425 
clausify_rules_pairs_aux result ths) 
426 
 ResClause.CLAUSE (msg,t) => 

18680  427 
(Output.debug ("Cannot clausify " ^ name ^ ": " ^ msg ^ 
17829  428 
": " ^ TermLib.string_of_term t); 
429 
clausify_rules_pairs_aux result ths) 

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

430 

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 

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

432 
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

433 
 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

434 
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

435 
handle THM (msg,_,_) => 
18680  436 
(Output.debug ("Cannot clausify " ^ name ^ ": " ^ msg); 
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

437 
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

438 
 ResHolClause.LAM2COMB (t) => 
18680  439 
(Output.debug ("Cannot clausify " ^ TermLib.string_of_term t); 
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

440 
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

441 

15347  442 

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

443 

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

445 

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

447 

18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

448 
(*These should include any plausiblyuseful theorems, especially if they need 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

449 
Skolem functions. FIXME: this list is VERY INCOMPLETE*) 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

450 
val default_initial_thms = map pairname 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

451 
[refl_def, antisym_def, sym_def, trans_def, single_valued_def, 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

452 
subset_refl, Union_least, Inter_greatest]; 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

453 

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

456 
fun clause_cache_setup thy = 

457 
let val simps = simpset_rules_of_thy thy 

458 
and clas = claset_rules_of_thy thy 

18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

459 
and thy0 = List.foldl skolem_cache thy default_initial_thms 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

460 
val thy1 = List.foldl skolem_cache thy0 clas 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

461 
in List.foldl skolem_cache thy1 simps end; 
18141
89e2e8bed08f
Skolemization by inference, but not quite finished
paulson
parents:
18009
diff
changeset

462 
(*Could be duplicate theorem names, due to multiple attributes*) 
16009  463 

16563  464 

465 
(*** meson proof methods ***) 

466 

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

468 

469 
fun meson_meth ths ctxt = 

470 
Method.SIMPLE_METHOD' HEADGOAL 

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

472 

473 
val meson_method_setup = 

18708  474 
Method.add_methods 
475 
[("meson", Method.thms_ctxt_args meson_meth, 

476 
"The MESON resolution proof procedure")]; 

15347  477 

18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

478 

0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

479 

0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

480 
(*** The Skolemization attribute ***) 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

481 

0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

482 
fun conj2_rule (th1,th2) = conjI OF [th1,th2]; 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

483 

0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

484 
(*Conjoin a list of clauses to recreate a single theorem*) 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

485 
val conj_rule = foldr1 conj2_rule; 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

486 

0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

487 
fun skolem_global_fun (thy, th) = 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

488 
let val name = Thm.name_of_thm th 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

489 
val (cls,thy') = skolem_cache_thm ((name,th), thy) 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

490 
in (thy', conj_rule cls) end; 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

491 

0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

492 
val skolem_global = Attrib.no_args skolem_global_fun; 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

493 

18629  494 
fun skolem_local x = Attrib.no_args (Attrib.rule (K (conj_rule o skolem_thm))) x; 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

495 

0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

496 
val setup_attrs = Attrib.add_attributes 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

497 
[("skolem", (skolem_global, skolem_local), 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

498 
"skolemization of a theorem")]; 
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

499 

18708  500 
val setup = clause_cache_setup #> setup_attrs; 
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18404
diff
changeset

501 

15347  502 
end; 