25 val rm_Eps |
23 val rm_Eps |
26 : (Term.term * Term.term) list -> thm list -> Term.term list |
24 : (Term.term * Term.term) list -> thm list -> Term.term list |
27 val claset_rules_of_thy : theory -> (string * thm) list |
25 val claset_rules_of_thy : theory -> (string * thm) list |
28 val simpset_rules_of_thy : theory -> (string * thm) list |
26 val simpset_rules_of_thy : theory -> (string * thm) list |
29 val clausify_rules : thm list -> thm list -> ResClause.clause list list * thm list |
27 val clausify_rules : thm list -> thm list -> ResClause.clause list list * thm list |
|
28 val setup : (theory -> theory) list |
30 end; |
29 end; |
31 |
30 |
32 structure ResAxioms : RES_AXIOMS = |
31 structure ResAxioms : RES_AXIOMS = |
33 |
32 |
34 struct |
33 struct |
35 |
34 |
36 (**** Transformation of Elimination Rules into First-Order Formulas****) |
35 (**** Transformation of Elimination Rules into First-Order Formulas****) |
37 |
36 |
38 (* a tactic used to prove an elim-rule. *) |
37 (* a tactic used to prove an elim-rule. *) |
39 fun elimRule_tac thm = |
38 fun elimRule_tac th = |
40 ((rtac impI 1) ORELSE (rtac notI 1)) THEN (etac thm 1) THEN |
39 ((rtac impI 1) ORELSE (rtac notI 1)) THEN (etac th 1) THEN |
41 REPEAT(Fast_tac 1); |
40 REPEAT(Fast_tac 1); |
42 |
41 |
43 |
42 |
44 (* This following version fails sometimes, need to investigate, do not use it now. *) |
43 (* This following version fails sometimes, need to investigate, do not use it now. *) |
45 fun elimRule_tac' thm = |
44 fun elimRule_tac' th = |
46 ((rtac impI 1) ORELSE (rtac notI 1)) THEN (etac thm 1) THEN |
45 ((rtac impI 1) ORELSE (rtac notI 1)) THEN (etac th 1) THEN |
47 REPEAT(SOLVE((etac exI 1) ORELSE (rtac conjI 1) ORELSE (rtac disjI1 1) ORELSE (rtac disjI2 1))); |
46 REPEAT(SOLVE((etac exI 1) ORELSE (rtac conjI 1) ORELSE (rtac disjI1 1) ORELSE (rtac disjI2 1))); |
48 |
47 |
49 |
48 |
50 exception ELIMR2FOL of string; |
49 exception ELIMR2FOL of string; |
51 |
50 |
153 in |
152 in |
154 if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2) |
153 if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2) |
155 end; |
154 end; |
156 |
155 |
157 |
156 |
158 (* convert a theorem into NNF and also skolemize it. *) |
157 (*Convert a theorem into NNF and also skolemize it. Original version, using |
159 fun skolem_axiom thm = |
158 Hilbert's epsilon in the resulting clauses.*) |
160 if Term.is_first_order (prop_of thm) then |
159 fun skolem_axiom th = |
161 let val thm' = (skolemize o make_nnf o ObjectLogic.atomize_thm o Drule.freeze_all) thm |
160 if Term.is_first_order (prop_of th) then |
|
161 let val th' = (skolemize o make_nnf o ObjectLogic.atomize_thm o Drule.freeze_all) th |
162 in |
162 in |
163 repeat_RS thm' someI_ex |
163 repeat_RS th' someI_ex |
164 end |
164 end |
165 else raise THM ("skolem_axiom: not first-order", 0, [thm]); |
165 else raise THM ("skolem_axiom: not first-order", 0, [th]); |
166 |
166 |
167 |
167 |
168 fun cnf_rule thm = make_clauses [skolem_axiom (transform_elim thm)]; |
168 fun cnf_rule th = make_clauses [skolem_axiom (transform_elim th)]; |
169 |
169 |
170 (*Transfer a theorem in to theory Reconstruction.thy if it is not already |
170 (*Transfer a theorem in to theory Reconstruction.thy if it is not already |
171 inside that theory -- because it's needed for Skolemization *) |
171 inside that theory -- because it's needed for Skolemization *) |
172 |
172 |
173 val recon_thy = ThyInfo.get_theory"Reconstruction"; |
173 val recon_thy = ThyInfo.get_theory"Reconstruction"; |
174 |
174 |
175 fun transfer_to_Reconstruction thm = |
175 fun transfer_to_Reconstruction th = |
176 transfer recon_thy thm handle THM _ => thm; |
176 transfer recon_thy th handle THM _ => th; |
177 |
177 |
178 fun is_taut th = |
178 fun is_taut th = |
179 case (prop_of th) of |
179 case (prop_of th) of |
180 (Const ("Trueprop", _) $ Const ("True", _)) => true |
180 (Const ("Trueprop", _) $ Const ("True", _)) => true |
181 | _ => false; |
181 | _ => false; |
182 |
182 |
183 (* remove tautologous clauses *) |
183 (* remove tautologous clauses *) |
184 val rm_redundant_cls = List.filter (not o is_taut); |
184 val rm_redundant_cls = List.filter (not o is_taut); |
185 |
185 |
186 (* transform an Isabelle thm into CNF *) |
186 (* transform an Isabelle thm into CNF *) |
187 fun cnf_axiom_aux thm = |
187 fun cnf_axiom_aux th = |
188 map (zero_var_indexes o Thm.varifyT) |
188 map (zero_var_indexes o Thm.varifyT) |
189 (rm_redundant_cls (cnf_rule (transfer_to_Reconstruction thm))); |
189 (rm_redundant_cls (cnf_rule (transfer_to_Reconstruction th))); |
190 |
190 |
191 |
191 |
192 (*Cache for clauses: could be a hash table if we provided them.*) |
192 (**** SKOLEMIZATION BY INFERENCE (lcp) ****) |
|
193 |
|
194 (*Traverse a term, accumulating Skolem function definitions.*) |
|
195 fun declare_skofuns s t thy = |
|
196 let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (n, thy) = |
|
197 (*Existential: declare a Skolem function, then insert into body and continue*) |
|
198 let val cname = s ^ "_" ^ Int.toString n |
|
199 val args = term_frees xtp |
|
200 val Ts = map type_of args |
|
201 val cT = Ts ---> T |
|
202 val c = Const(NameSpace.append (PureThy.get_name thy) cname, cT) |
|
203 val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp) |
|
204 val def = equals cT $ c $ rhs |
|
205 val thy' = Theory.add_consts_i [(cname, cT, NoSyn)] thy |
|
206 val thy'' = Theory.add_defs_i false [(cname ^ "_def", def)] thy' |
|
207 in dec_sko (subst_bound (list_comb(c,args), p)) (n+1, thy'') end |
|
208 | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) (n, thy) = |
|
209 (*Universal: insert a free variable into body and continue*) |
|
210 let val fname = variant (add_term_names (p,[])) a |
|
211 in dec_sko (subst_bound (Free(fname,T), p)) (n+1, thy) end |
|
212 | dec_sko (Const ("op &", _) $ p $ q) nthy = |
|
213 dec_sko q (dec_sko p nthy) |
|
214 | dec_sko (Const ("op |", _) $ p $ q) nthy = |
|
215 dec_sko q (dec_sko p nthy) |
|
216 | dec_sko (Const ("Trueprop", _) $ p) nthy = |
|
217 dec_sko p nthy |
|
218 | dec_sko t (n,thy) = (n,thy) (*Do nothing otherwise*) |
|
219 in #2 (dec_sko t (1,thy)) end; |
|
220 |
|
221 (*cterms are used throughout for efficiency*) |
|
222 val cTrueprop = Thm.cterm_of (Theory.sign_of HOL.thy) HOLogic.Trueprop; |
|
223 |
|
224 (*cterm version of mk_cTrueprop*) |
|
225 fun c_mkTrueprop A = Thm.capply cTrueprop A; |
|
226 |
|
227 (*Given an abstraction over n variables, replace the bound variables by free |
|
228 ones. Return the body, along with the list of free variables.*) |
|
229 fun c_variant_abs_multi (ct0, vars) = |
|
230 let val (cv,ct) = Thm.dest_abs NONE ct0 |
|
231 in c_variant_abs_multi (ct, cv::vars) end |
|
232 handle CTERM _ => (ct0, rev vars); |
|
233 |
|
234 (*Given the definition of a Skolem function, return a theorem to replace |
|
235 an existential formula by a use of that function.*) |
|
236 fun skolem_of_def def = |
|
237 let val (c,rhs) = Drule.dest_equals (cprop_of (Drule.freeze_all def)) |
|
238 val (ch, frees) = c_variant_abs_multi (rhs, []) |
|
239 val (chil,cabs) = Thm.dest_comb ch |
|
240 val {sign, t, ...} = rep_cterm chil |
|
241 val (Const ("Hilbert_Choice.Eps", Type("fun",[_,T]))) = t |
|
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))); |
|
245 in prove_goalw_cterm [def] (Drule.mk_implies (ex_tm, conc)) |
|
246 (fn [prem] => [ rtac (prem RS someI_ex) 1 ]) |
|
247 end; |
|
248 |
|
249 |
|
250 (*Converts an Isabelle theorem (intro, elim or simp format) into nnf.*) |
|
251 fun to_nnf thy th = |
|
252 if Term.is_first_order (prop_of th) then |
|
253 th |> Thm.transfer thy |> transform_elim |> Drule.freeze_all |
|
254 |> ObjectLogic.atomize_thm |> make_nnf |
|
255 else raise THM ("to_nnf: not first-order", 0, [th]); |
|
256 |
|
257 (*The cache prevents repeated clausification of a theorem, |
|
258 and also repeated declaration of Skolem functions*) |
193 val clause_cache = ref (Symtab.empty : (thm * thm list) Symtab.table) |
259 val clause_cache = ref (Symtab.empty : (thm * thm list) Symtab.table) |
194 |
260 |
|
261 (*Declare Skolem functions for a theorem, supplied in nnf and with its name*) |
|
262 fun skolem thy (name,th) = |
|
263 let val cname = (case name of |
|
264 "" => gensym "sko" | s => Sign.base_name s) |
|
265 val thy' = declare_skofuns cname (#prop (rep_thm th)) thy |
|
266 in (map (skolem_of_def o #2) (axioms_of thy'), thy') end; |
|
267 |
|
268 (*Populate the clause cache using the supplied theorems*) |
|
269 fun skolemlist [] thy = thy |
|
270 | skolemlist ((name,th)::nths) thy = |
|
271 (case Symtab.lookup (!clause_cache,name) of |
|
272 NONE => |
|
273 let val nnfth = to_nnf thy th |
|
274 val (skoths,thy') = skolem thy (name, nnfth) |
|
275 val cls = Meson.make_cnf skoths nnfth |
|
276 in clause_cache := Symtab.update ((name, (th,cls)), !clause_cache); |
|
277 skolemlist nths thy' |
|
278 end |
|
279 | SOME _ => skolemlist nths thy) (*FIXME: check for duplicate names?*) |
|
280 handle THM _ => skolemlist nths thy; |
|
281 |
|
282 (*Exported function to convert Isabelle theorems into axiom clauses*) |
195 fun cnf_axiom (name,th) = |
283 fun cnf_axiom (name,th) = |
196 case name of |
284 case name of |
197 "" => cnf_axiom_aux th (*no name, so can't cache*) |
285 "" => cnf_axiom_aux th (*no name, so can't cache*) |
198 | s => case Symtab.lookup (!clause_cache,s) of |
286 | s => case Symtab.lookup (!clause_cache,s) of |
199 NONE => |
287 NONE => |
244 fun get_skolem epss t = |
332 fun get_skolem epss t = |
245 case (sk_lookup epss t) of NONE => get_new_skolem epss t |
333 case (sk_lookup epss t) of NONE => get_new_skolem epss t |
246 | SOME sk => (sk,epss); |
334 | SOME sk => (sk,epss); |
247 |
335 |
248 |
336 |
249 fun rm_Eps_cls_aux epss (t as (Const ("Hilbert_Choice.Eps",_) $ Abs(_,_,_))) = get_skolem epss t |
337 fun rm_Eps_cls_aux epss (t as (Const ("Hilbert_Choice.Eps",_) $ Abs(_,_,_))) = |
|
338 get_skolem epss t |
250 | rm_Eps_cls_aux epss (P $ Q) = |
339 | rm_Eps_cls_aux epss (P $ Q) = |
251 let val (P',epss') = rm_Eps_cls_aux epss P |
340 let val (P',epss') = rm_Eps_cls_aux epss P |
252 val (Q',epss'') = rm_Eps_cls_aux epss' Q |
341 val (Q',epss'') = rm_Eps_cls_aux epss' Q |
253 in |
342 in (P' $ Q',epss'') end |
254 (P' $ Q',epss'') |
|
255 end |
|
256 | rm_Eps_cls_aux epss t = (t,epss); |
343 | rm_Eps_cls_aux epss t = (t,epss); |
257 |
344 |
258 |
345 |
259 fun rm_Eps_cls epss thm = rm_Eps_cls_aux epss (prop_of thm); |
346 fun rm_Eps_cls epss th = rm_Eps_cls_aux epss (prop_of th); |
260 |
347 |
261 |
348 |
262 (* remove the epsilon terms in a formula, by skolem terms. *) |
349 (* remove the epsilon terms in a formula, by skolem terms. *) |
263 fun rm_Eps _ [] = [] |
350 fun rm_Eps _ [] = [] |
264 | rm_Eps epss (thm::thms) = |
351 | rm_Eps epss (th::thms) = |
265 let val (thm',epss') = rm_Eps_cls epss thm |
352 let val (th',epss') = rm_Eps_cls epss th |
266 in |
353 in th' :: (rm_Eps epss' thms) end; |
267 thm' :: (rm_Eps epss' thms) |
|
268 end; |
|
269 |
354 |
270 |
355 |
271 (* convert a theorem into CNF and then into Clause.clause format. *) |
356 (* convert a theorem into CNF and then into Clause.clause format. *) |
272 fun clausify_axiom thm = |
357 fun clausify_axiom th = |
273 let val name = Thm.name_of_thm thm |
358 let val name = Thm.name_of_thm th |
274 val isa_clauses = cnf_axiom (name, thm) |
359 val isa_clauses = cnf_axiom (name, th) |
275 (*"isa_clauses" are already in "standard" form. *) |
360 (*"isa_clauses" are already in "standard" form. *) |
276 val isa_clauses' = rm_Eps [] isa_clauses |
361 val isa_clauses' = rm_Eps [] isa_clauses |
277 val clauses_n = length isa_clauses |
362 val clauses_n = length isa_clauses |
278 fun make_axiom_clauses _ [] = [] |
363 fun make_axiom_clauses _ [] = [] |
279 | make_axiom_clauses i (cls::clss) = |
364 | make_axiom_clauses i (cls::clss) = |
321 |
406 |
322 (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause) ****) |
407 (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause) ****) |
323 |
408 |
324 (* classical rules *) |
409 (* classical rules *) |
325 fun clausify_rules [] err_list = ([],err_list) |
410 fun clausify_rules [] err_list = ([],err_list) |
326 | clausify_rules (thm::thms) err_list = |
411 | clausify_rules (th::thms) err_list = |
327 let val (ts,es) = clausify_rules thms err_list |
412 let val (ts,es) = clausify_rules thms err_list |
328 in |
413 in |
329 ((clausify_axiom thm)::ts,es) handle _ => (ts,(thm::es)) |
414 ((clausify_axiom th)::ts,es) handle _ => (ts,(th::es)) |
330 end; |
415 end; |
331 |
|
332 |
416 |
333 (* convert all classical rules from a given theory into Clause.clause format. *) |
417 (* convert all classical rules from a given theory into Clause.clause format. *) |
334 fun clausify_classical_rules_thy thy = |
418 fun clausify_classical_rules_thy thy = |
335 clausify_rules (map #2 (claset_rules_of_thy thy)) []; |
419 clausify_rules (map #2 (claset_rules_of_thy thy)) []; |
336 |
420 |
337 (* convert all simplifier rules from a given theory into Clause.clause format. *) |
421 (* convert all simplifier rules from a given theory into Clause.clause format. *) |
338 fun clausify_simpset_rules_thy thy = |
422 fun clausify_simpset_rules_thy thy = |
339 clausify_rules (map #2 (simpset_rules_of_thy thy)) []; |
423 clausify_rules (map #2 (simpset_rules_of_thy thy)) []; |
340 |
424 |
|
425 (*Setup function: takes a theory and installs ALL simprules and claset rules |
|
426 into the clause cache*) |
|
427 fun clause_cache_setup thy = |
|
428 let val simps = simpset_rules_of_thy thy |
|
429 and clas = claset_rules_of_thy thy |
|
430 in skolemlist clas (skolemlist simps thy) end; |
|
431 |
|
432 val setup = [clause_cache_setup]; |
341 |
433 |
342 end; |
434 end; |