1 (* Author: Jia Meng, Cambridge University Computer Laboratory
3 Copyright 2004 University of Cambridge
5 Transformation of axiom rules (elim/intro/etc) into CNF forms.
10 val trace_abs: bool ref
11 val cnf_axiom : string * thm -> thm list
12 val cnf_name : string -> thm list
13 val meta_cnf_axiom : thm -> thm list
14 val pairname : thm -> string * thm
15 val skolem_thm : thm -> thm list
16 val to_nnf : thm -> thm
17 val cnf_rules_pairs : (string * thm) list -> (thm * (string * int)) list
18 val meson_method_setup : theory -> theory
19 val setup : theory -> theory
20 val assume_abstract_list: thm list -> thm list
21 val neg_conjecture_clauses: thm -> int -> thm list * (string * typ) list
22 val claset_rules_of: Proof.context -> (string * thm) list (*FIXME DELETE*)
23 val simpset_rules_of: Proof.context -> (string * thm) list (*FIXME DELETE*)
24 val atpset_rules_of: Proof.context -> (string * thm) list
30 (*For running the comparison between combinators and abstractions.
31 CANNOT be a ref, as the setting is used while Isabelle is built.
32 Currently FALSE, i.e. all the "abstraction" code below is unused, but so far
33 it seems to be inferior to combinators...*)
34 val abstract_lambdas = true;
36 val trace_abs = ref false;
39 fun freeze_thm th = #1 (Drule.freeze_thaw th);
41 val lhs_of = #1 o Logic.dest_equals o Thm.prop_of;
42 val rhs_of = #2 o Logic.dest_equals o Thm.prop_of;
45 (*Store definitions of abstraction functions, ensuring that identical right-hand
46 sides are denoted by the same functions and thereby reducing the need for
47 extensionality in proofs.
48 FIXME! Store in theory data!!*)
50 (*Populate the abstraction cache with common combinators.*)
52 let val (_,ct) = Thm.dest_abs NONE (Drule.rhs_of th)
53 val t = Logic.legacy_varify (term_of ct)
54 in Net.insert_term Thm.eq_thm (t, th) net end;
56 val abstraction_cache = ref
57 (seed (thm"ATP_Linkup.I_simp")
58 (seed (thm"ATP_Linkup.B_simp")
59 (seed (thm"ATP_Linkup.K_simp") Net.empty)));
62 (**** Transformation of Elimination Rules into First-Order Formulas****)
64 val cfalse = cterm_of HOL.thy HOLogic.false_const;
65 val ctp_false = cterm_of HOL.thy (HOLogic.mk_Trueprop HOLogic.false_const);
67 (*Converts an elim-rule into an equivalent theorem that does not have the
68 predicate variable. Leaves other theorems unchanged. We simply instantiate the
69 conclusion variable to False.*)
70 fun transform_elim th =
71 case concl_of th of (*conclusion variable*)
72 Const("Trueprop",_) $ (v as Var(_,Type("bool",[]))) =>
73 Thm.instantiate ([], [(cterm_of HOL.thy v, cfalse)]) th
74 | v as Var(_, Type("prop",[])) =>
75 Thm.instantiate ([], [(cterm_of HOL.thy v, ctp_false)]) th
78 (**** Transformation of Clasets and Simpsets into First-Order Axioms ****)
80 (*Transfer a theorem into theory ATP_Linkup.thy if it is not already
81 inside that theory -- because it's needed for Skolemization *)
83 (*This will refer to the final version of theory ATP_Linkup.*)
84 val recon_thy_ref = Theory.self_ref (the_context ());
86 (*If called while ATP_Linkup is being created, it will transfer to the
87 current version. If called afterward, it will transfer to the final version.*)
88 fun transfer_to_ATP_Linkup th =
89 transfer (Theory.deref recon_thy_ref) th handle THM _ => th;
92 (**** SKOLEMIZATION BY INFERENCE (lcp) ****)
94 (*Traverse a theorem, declaring Skolem function definitions. String s is the suggested
95 prefix for the Skolem constant. Result is a new theory*)
96 fun declare_skofuns s th thy =
98 fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (thy, axs) =
99 (*Existential: declare a Skolem function, then insert into body and continue*)
100 let val cname = Name.internal (s ^ "_sko" ^ Int.toString (inc nref))
101 val args = term_frees xtp (*get the formal parameter list*)
102 val Ts = map type_of args
104 val c = Const (Sign.full_name thy cname, cT)
105 val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
106 (*Forms a lambda-abstraction over the formal parameters*)
107 val thy' = Sign.add_consts_authentic [(cname, cT, NoSyn)] thy
108 (*Theory is augmented with the constant, then its def*)
109 val cdef = cname ^ "_def"
110 val thy'' = Theory.add_defs_i false false [(cdef, equals cT $ c $ rhs)] thy'
111 in dec_sko (subst_bound (list_comb(c,args), p))
112 (thy'', get_axiom thy'' cdef :: axs)
114 | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) thx =
115 (*Universal quant: insert a free variable into body and continue*)
116 let val fname = Name.variant (add_term_names (p,[])) a
117 in dec_sko (subst_bound (Free(fname,T), p)) thx end
118 | dec_sko (Const ("op &", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
119 | dec_sko (Const ("op |", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
120 | dec_sko (Const ("Trueprop", _) $ p) thx = dec_sko p thx
121 | dec_sko t thx = thx (*Do nothing otherwise*)
122 in dec_sko (prop_of th) (thy,[]) end;
124 (*Traverse a theorem, accumulating Skolem function definitions.*)
125 fun assume_skofuns th =
126 let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs =
127 (*Existential: declare a Skolem function, then insert into body and continue*)
128 let val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*)
129 val args = term_frees xtp \\ skos (*the formal parameters*)
130 val Ts = map type_of args
132 val c = Free (gensym "sko_", cT)
133 val rhs = list_abs_free (map dest_Free args,
134 HOLogic.choice_const T $ xtp)
135 (*Forms a lambda-abstraction over the formal parameters*)
136 val def = equals cT $ c $ rhs
137 in dec_sko (subst_bound (list_comb(c,args), p))
140 | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) defs =
141 (*Universal quant: insert a free variable into body and continue*)
142 let val fname = Name.variant (add_term_names (p,[])) a
143 in dec_sko (subst_bound (Free(fname,T), p)) defs end
144 | dec_sko (Const ("op &", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
145 | dec_sko (Const ("op |", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
146 | dec_sko (Const ("Trueprop", _) $ p) defs = dec_sko p defs
147 | dec_sko t defs = defs (*Do nothing otherwise*)
148 in dec_sko (prop_of th) [] end;
151 (**** REPLACING ABSTRACTIONS BY FUNCTION DEFINITIONS ****)
153 (*Returns the vars of a theorem*)
155 map (Thm.cterm_of (theory_of_thm th) o Var) (Drule.fold_terms Term.add_vars th []);
157 (*Make a version of fun_cong with a given variable name*)
159 val fun_cong' = fun_cong RS asm_rl; (*renumber f, g to prevent clashes with (a,0)*)
160 val cx = hd (vars_of_thm fun_cong');
161 val ty = typ_of (ctyp_of_term cx);
162 val thy = theory_of_thm fun_cong;
163 fun mkvar a = cterm_of thy (Var((a,0),ty));
165 fun xfun_cong x = Thm.instantiate ([], [(cx, mkvar x)]) fun_cong'
168 (*Removes the lambdas from an equation of the form t = (%x. u). A non-negative n,
169 serves as an upper bound on how many to remove.*)
170 fun strip_lambdas 0 th = th
171 | strip_lambdas n th =
173 _ $ (Const ("op =", _) $ _ $ Abs (x,_,_)) =>
174 strip_lambdas (n-1) (freeze_thm (th RS xfun_cong x))
177 (*Convert meta- to object-equality. Fails for theorems like split_comp_eq,
178 where some types have the empty sort.*)
179 val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq";
180 fun mk_object_eq th = th RS meta_eq_to_obj_eq
181 handle THM _ => error ("Theorem contains empty sort: " ^ string_of_thm th);
183 (*Apply a function definition to an argument, beta-reducing the result.*)
185 let val th1 = combination cf (reflexive x)
186 val th2 = beta_conversion false (Drule.rhs_of th1)
187 in transitive th1 th2 end;
189 (*Apply a function definition to arguments, beta-reducing along the way.*)
190 fun list_combination cf [] = cf
191 | list_combination cf (x::xs) = list_combination (beta_comb cf x) xs;
193 fun list_cabs ([] , t) = t
194 | list_cabs (v::vars, t) = Thm.cabs v (list_cabs(vars,t));
196 fun assert_eta_free ct =
197 let val t = term_of ct
198 in if (t aconv Envir.eta_contract t) then ()
199 else error ("Eta redex in term: " ^ string_of_cterm ct)
202 fun eq_absdef (th1, th2) =
203 Context.joinable (theory_of_thm th1, theory_of_thm th2) andalso
204 rhs_of th1 aconv rhs_of th2;
206 fun lambda_free (Abs _) = false
207 | lambda_free (t $ u) = lambda_free t andalso lambda_free u
208 | lambda_free _ = true;
211 Term.fold_types (Term.fold_atyps (fn TVar _ => K false | _ => I)) t true;
213 fun dest_abs_list ct =
214 let val (cv,ct') = Thm.dest_abs NONE ct
215 val (cvs,cu) = dest_abs_list ct'
217 handle CTERM _ => ([],ct);
219 fun lambda_list [] u = u
220 | lambda_list (v::vs) u = lambda v (lambda_list vs u);
222 fun abstract_rule_list [] [] th = th
223 | abstract_rule_list (v::vs) (ct::cts) th = abstract_rule v ct (abstract_rule_list vs cts th)
224 | abstract_rule_list _ _ th = raise THM ("abstract_rule_list", 0, [th]);
227 val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0
229 (*Does an existing abstraction definition have an RHS that matches the one we need now?
230 thy is the current theory, which must extend that of theorem th.*)
231 fun match_rhs thy t th =
232 let val _ = if !trace_abs then warning ("match_rhs: " ^ string_of_cterm (cterm_of thy t) ^
233 " against\n" ^ string_of_thm th) else ();
234 val (tyenv,tenv) = Pattern.first_order_match thy (rhs_of th, t) (tyenv0,tenv0)
235 val term_insts = map Meson.term_pair_of (Vartab.dest tenv)
236 val ct_pairs = if subthy (theory_of_thm th, thy) andalso
237 forall lambda_free (map #2 term_insts)
238 then map (pairself (cterm_of thy)) term_insts
239 else raise Pattern.MATCH (*Cannot allow lambdas in the instantiation*)
240 fun ctyp2 (ixn, (S, T)) = (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T)
241 val th' = cterm_instantiate ct_pairs th
242 in SOME (th, instantiate (map ctyp2 (Vartab.dest tyenv), []) th') end
245 (*Traverse a theorem, declaring abstraction function definitions. String s is the suggested
246 prefix for the constants. Resulting theory is returned in the first theorem. *)
247 fun declare_absfuns th =
248 let fun abstract thy ct =
249 if lambda_free (term_of ct) then (transfer thy (reflexive ct), [])
253 let val cname = Name.internal (gensym "abs_");
254 val _ = assert_eta_free ct;
255 val (cvs,cta) = dest_abs_list ct
256 val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs)
257 val _ = if !trace_abs then warning ("Nested lambda: " ^ string_of_cterm cta) else ();
258 val (u'_th,defs) = abstract thy cta
259 val _ = if !trace_abs then warning ("Returned " ^ string_of_thm u'_th) else ();
260 val cu' = Drule.rhs_of u'_th
262 val abs_v_u = lambda_list (map term_of cvs) u'
263 (*get the formal parameters: ALL variables free in the term*)
264 val args = term_frees abs_v_u
265 val _ = if !trace_abs then warning (Int.toString (length args) ^ " arguments") else ();
266 val rhs = list_abs_free (map dest_Free args, abs_v_u)
267 (*Forms a lambda-abstraction over the formal parameters*)
268 val _ = if !trace_abs then warning ("Looking up " ^ string_of_cterm cu') else ();
269 val thy = theory_of_thm u'_th
271 case List.mapPartial (match_rhs thy abs_v_u)
272 (Net.match_term (!abstraction_cache) u') of
274 (if !trace_abs then warning ("Re-using axiom " ^ string_of_thm ax) else ();
277 let val _ = if !trace_abs then warning "Lookup was empty" else ();
278 val Ts = map type_of args
279 val cT = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu'))
280 val c = Const (Sign.full_name thy cname, cT)
281 val thy = Sign.add_consts_authentic [(cname, cT, NoSyn)] thy
282 (*Theory is augmented with the constant,
283 then its definition*)
284 val cdef = cname ^ "_def"
285 val thy = Theory.add_defs_i false false
286 [(cdef, equals cT $ c $ rhs)] thy
287 val _ = if !trace_abs then (warning ("Definition is " ^
288 string_of_thm (get_axiom thy cdef)))
290 val ax = get_axiom thy cdef |> freeze_thm
291 |> mk_object_eq |> strip_lambdas (length args)
292 |> mk_meta_eq |> Meson.generalize
293 val (_,ax') = Option.valOf (match_rhs thy abs_v_u ax)
294 val _ = if !trace_abs then
295 (warning ("Declaring: " ^ string_of_thm ax);
296 warning ("Instance: " ^ string_of_thm ax'))
298 val _ = abstraction_cache := Net.insert_term eq_absdef
299 ((Logic.varify u'), ax) (!abstraction_cache)
301 raise THM ("declare_absfuns: INSERT", 0, [th,u'_th,ax])
303 in if !trace_abs then warning ("Lookup result: " ^ string_of_thm ax') else ();
304 (transitive (abstract_rule_list vs cvs u'_th) (symmetric ax'), ax::defs) end
306 let val (ct1,ct2) = Thm.dest_comb ct
307 val (th1,defs1) = abstract thy ct1
308 val (th2,defs2) = abstract (theory_of_thm th1) ct2
309 in (combination th1 th2, defs1@defs2) end
310 val _ = if !trace_abs then warning ("declare_absfuns, Abstracting: " ^ string_of_thm th) else ();
311 val (eqth,defs) = abstract (theory_of_thm th) (cprop_of th)
312 val ths = equal_elim eqth th :: map (strip_lambdas ~1 o mk_object_eq o freeze_thm) defs
313 val _ = if !trace_abs then warning ("declare_absfuns, Result: " ^ string_of_thm (hd ths)) else ();
314 in (theory_of_thm eqth, map Drule.eta_contraction_rule ths) end;
316 fun name_of def = try (#1 o dest_Free o lhs_of) def;
318 (*A name is valid provided it isn't the name of a defined abstraction.*)
319 fun valid_name defs (Free(x,T)) = not (x mem_string (List.mapPartial name_of defs))
320 | valid_name defs _ = false;
322 fun assume_absfuns th =
323 let val thy = theory_of_thm th
324 val cterm = cterm_of thy
326 if lambda_free (term_of ct) then (reflexive ct, [])
330 let val _ = assert_eta_free ct;
331 val (cvs,cta) = dest_abs_list ct
332 val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs)
333 val (u'_th,defs) = abstract cta
334 val cu' = Drule.rhs_of u'_th
336 (*Could use Thm.cabs instead of lambda to work at level of cterms*)
337 val abs_v_u = lambda_list (map term_of cvs) (term_of cu')
338 (*get the formal parameters: free variables not present in the defs
339 (to avoid taking abstraction function names as parameters) *)
340 val args = filter (valid_name defs) (term_frees abs_v_u)
341 val crhs = list_cabs (map cterm args, cterm abs_v_u)
342 (*Forms a lambda-abstraction over the formal parameters*)
343 val rhs = term_of crhs
345 case List.mapPartial (match_rhs thy abs_v_u)
346 (Net.match_term (!abstraction_cache) u') of
348 (if !trace_abs then warning ("Re-using axiom " ^ string_of_thm ax) else ();
351 let val Ts = map type_of args
352 val const_ty = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu'))
353 val c = Free (gensym "abs_", const_ty)
354 val ax = assume (Thm.capply (cterm (equals const_ty $ c)) crhs)
355 |> mk_object_eq |> strip_lambdas (length args)
356 |> mk_meta_eq |> Meson.generalize
357 val (_,ax') = Option.valOf (match_rhs thy abs_v_u ax)
358 val _ = abstraction_cache := Net.insert_term eq_absdef (rhs,ax)
361 raise THM ("assume_absfuns: INSERT", 0, [th,u'_th,ax])
363 in if !trace_abs then warning ("Lookup result: " ^ string_of_thm ax') else ();
364 (transitive (abstract_rule_list vs cvs u'_th) (symmetric ax'), ax::defs) end
366 let val (ct1,ct2) = Thm.dest_comb ct
367 val (t1',defs1) = abstract ct1
368 val (t2',defs2) = abstract ct2
369 in (combination t1' t2', defs1@defs2) end
370 val _ = if !trace_abs then warning ("assume_absfuns, Abstracting: " ^ string_of_thm th) else ();
371 val (eqth,defs) = abstract (cprop_of th)
372 val ths = equal_elim eqth th :: map (strip_lambdas ~1 o mk_object_eq o freeze_thm) defs
373 val _ = if !trace_abs then warning ("assume_absfuns, Result: " ^ string_of_thm (hd ths)) else ();
374 in map Drule.eta_contraction_rule ths end;
377 (*cterms are used throughout for efficiency*)
378 val cTrueprop = Thm.cterm_of HOL.thy HOLogic.Trueprop;
380 (*cterm version of mk_cTrueprop*)
381 fun c_mkTrueprop A = Thm.capply cTrueprop A;
383 (*Given an abstraction over n variables, replace the bound variables by free
384 ones. Return the body, along with the list of free variables.*)
385 fun c_variant_abs_multi (ct0, vars) =
386 let val (cv,ct) = Thm.dest_abs NONE ct0
387 in c_variant_abs_multi (ct, cv::vars) end
388 handle CTERM _ => (ct0, rev vars);
390 (*Given the definition of a Skolem function, return a theorem to replace
391 an existential formula by a use of that function.
392 Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *)
393 fun skolem_of_def def =
394 let val (c,rhs) = Drule.dest_equals (cprop_of (freeze_thm def))
395 val (ch, frees) = c_variant_abs_multi (rhs, [])
396 val (chilbert,cabs) = Thm.dest_comb ch
397 val {sign,t, ...} = rep_cterm chilbert
398 val T = case t of Const ("Hilbert_Choice.Eps", Type("fun",[_,T])) => T
399 | _ => raise THM ("skolem_of_def: expected Eps", 0, [def])
400 val cex = Thm.cterm_of sign (HOLogic.exists_const T)
401 val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
402 and conc = c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees)));
403 fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS someI_ex) 1
404 in Goal.prove_raw [ex_tm] conc tacf
405 |> forall_intr_list frees
406 |> forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*)
410 (*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
412 th |> transfer_to_ATP_Linkup
413 |> transform_elim |> zero_var_indexes |> freeze_thm
414 |> ObjectLogic.atomize_thm |> make_nnf |> strip_lambdas ~1;
416 (*The cache prevents repeated clausification of a theorem,
417 and also repeated declaration of Skolem functions*)
418 (* FIXME use theory data!!*)
419 val clause_cache = ref (Thmtab.empty : thm list Thmtab.table)
422 (*Generate Skolem functions for a theorem supplied in nnf*)
423 fun skolem_of_nnf th =
424 map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns th);
426 fun assert_lambda_free ths msg =
427 case filter (not o lambda_free o prop_of) ths of
429 | ths' => error (msg ^ "\n" ^ space_implode "\n" (map string_of_thm ths'));
431 fun assume_abstract th =
432 if lambda_free (prop_of th) then [th]
433 else th |> Drule.eta_contraction_rule |> assume_absfuns
434 |> tap (fn ths => assert_lambda_free ths "assume_abstract: lambdas")
436 (*Replace lambdas by assumed function definitions in the theorems*)
437 fun assume_abstract_list ths =
438 if abstract_lambdas then List.concat (map assume_abstract ths)
439 else map Drule.eta_contraction_rule ths;
441 (*Replace lambdas by declared function definitions in the theorems*)
442 fun declare_abstract' (thy, []) = (thy, [])
443 | declare_abstract' (thy, th::ths) =
444 let val (thy', th_defs) =
445 if lambda_free (prop_of th) then (thy, [th])
447 th |> zero_var_indexes |> freeze_thm
448 |> Drule.eta_contraction_rule |> transfer thy |> declare_absfuns
449 val _ = assert_lambda_free th_defs "declare_abstract: lambdas"
450 val (thy'', ths') = declare_abstract' (thy', ths)
451 in (thy'', th_defs @ ths') end;
453 fun declare_abstract (thy, ths) =
454 if abstract_lambdas then declare_abstract' (thy, ths)
455 else (thy, map Drule.eta_contraction_rule ths);
457 (*Skolemize a named theorem, with Skolem functions as additional premises.*)
459 let val nnfth = to_nnf th
460 in Meson.make_cnf (skolem_of_nnf nnfth) nnfth |> assume_abstract_list |> Meson.finish_cnf
464 (*Keep the full complexity of the original name*)
465 fun flatten_name s = space_implode "_X" (NameSpace.explode s);
467 (*Declare Skolem functions for a theorem, supplied in nnf and with its name.
468 It returns a modified theory, unless skolemization fails.*)
470 let val cname = (case PureThy.get_name_hint th of "" => gensym "" | s => flatten_name s)
471 val _ = Output.debug (fn () => "skolemizing " ^ cname ^ ": ")
474 let val (thy',defs) = declare_skofuns cname nnfth thy
475 val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth
476 val (thy'',cnfs') = declare_abstract (thy',cnfs)
477 in (map Goal.close_result (Meson.finish_cnf cnfs'), thy'')
479 (SOME (to_nnf th) handle THM _ => NONE)
482 (*Populate the clause cache using the supplied theorem. Return the clausal form
483 and modified theory.*)
484 fun skolem_cache_thm th thy =
485 case Thmtab.lookup (!clause_cache) th of
487 (case skolem thy (Thm.transfer thy th) of
491 then warning ("skolem_cache: empty clause set for " ^ string_of_thm th)
493 change clause_cache (Thmtab.update (th, cls));
495 | SOME cls => (cls,thy);
497 (*Exported function to convert Isabelle theorems into axiom clauses*)
499 case Thmtab.lookup (!clause_cache) th of
501 let val cls = map Goal.close_result (skolem_thm th)
502 in Output.debug (fn () => "inserted into cache");
503 change clause_cache (Thmtab.update (th, cls)); cls
507 fun pairname th = (PureThy.get_name_hint th, th);
509 (**** Extract and Clausify theorems from a theory's claset and simpset ****)
511 fun rules_of_claset cs =
512 let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs
513 val intros = safeIs @ hazIs
514 val elims = map Classical.classical_rule (safeEs @ hazEs)
516 Output.debug (fn () => "rules_of_claset intros: " ^ Int.toString(length intros) ^
517 " elims: " ^ Int.toString(length elims));
518 map pairname (intros @ elims)
521 fun rules_of_simpset ss =
522 let val ({rules,...}, _) = rep_ss ss
523 val simps = Net.entries rules
525 Output.debug (fn () => "rules_of_simpset: " ^ Int.toString(length simps));
526 map (fn r => (#name r, #thm r)) simps
529 fun claset_rules_of ctxt = rules_of_claset (local_claset_of ctxt);
530 fun simpset_rules_of ctxt = rules_of_simpset (local_simpset_of ctxt);
532 fun atpset_rules_of ctxt = map pairname (ResAtpset.get_atpset ctxt);
535 (**** Translate a set of theorems into CNF ****)
537 (* classical rules: works for both FOL and HOL *)
538 fun cnf_rules [] err_list = ([],err_list)
539 | cnf_rules ((name,th) :: ths) err_list =
540 let val (ts,es) = cnf_rules ths err_list
541 in (cnf_axiom th :: ts,es) handle _ => (ts, (th::es)) end;
543 fun pair_name_cls k (n, []) = []
544 | pair_name_cls k (n, cls::clss) = (cls, (n,k)) :: pair_name_cls (k+1) (n, clss)
546 fun cnf_rules_pairs_aux pairs [] = pairs
547 | cnf_rules_pairs_aux pairs ((name,th)::ths) =
548 let val pairs' = (pair_name_cls 0 (name, cnf_axiom th)) @ pairs
549 handle THM _ => pairs | ResClause.CLAUSE _ => pairs
550 in cnf_rules_pairs_aux pairs' ths end;
552 (*The combination of rev and tail recursion preserves the original order*)
553 fun cnf_rules_pairs l = cnf_rules_pairs_aux [] (rev l);
556 (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)
558 (*Setup function: takes a theory and installs ALL known theorems into the clause cache*)
560 fun skolem_cache th thy =
561 let val prop = Thm.prop_of th
564 (*Monomorphic theorems can be Skolemized on demand,
565 but there are problems with re-use of abstraction functions if we don't
566 do them now, even for monomorphic theorems.*)
568 else #2 (skolem_cache_thm th thy)
571 (*The cache can be kept smaller by augmenting the condition above with
572 orelse (not abstract_lambdas andalso monomorphic prop).
573 However, while this step does not reduce the time needed to build HOL,
574 it doubles the time taken by the first call to the ATP link-up.*)
576 fun clause_cache_setup thy = fold skolem_cache (map #2 (PureThy.all_thms_of thy)) thy;
579 (*** meson proof methods ***)
581 fun skolem_use_cache_thm th =
582 case Thmtab.lookup (!clause_cache) th of
583 NONE => skolem_thm th
586 fun cnf_rules_of_ths ths = List.concat (map skolem_use_cache_thm ths);
588 val meson_method_setup = Method.add_methods
589 [("meson", Method.thms_args (fn ths =>
590 Method.SIMPLE_METHOD' (CHANGED_PROP o Meson.meson_claset_tac (cnf_rules_of_ths ths) HOL_cs)),
591 "MESON resolution proof procedure")];
593 (** Attribute for converting a theorem into clauses **)
595 fun meta_cnf_axiom th = map Meson.make_meta_clause (cnf_axiom th);
597 fun clausify_rule (th,i) = List.nth (meta_cnf_axiom th, i)
599 val clausify = Attrib.syntax (Scan.lift Args.nat
600 >> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i))));
603 (*** Converting a subgoal into negated conjecture clauses. ***)
605 val neg_skolemize_tac = EVERY' [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac];
607 (*finish_cnf removes tautologies and functional reflexivity axioms, but by calling Thm.varifyT
608 it can introduce TVars, which we don't want in conjecture clauses.*)
609 val neg_clausify = map Thm.freezeT o Meson.finish_cnf o assume_abstract_list o make_clauses;
611 fun neg_conjecture_clauses st0 n =
612 let val st = Seq.hd (neg_skolemize_tac n st0)
613 val (params,_,_) = strip_context (Logic.nth_prem (n, Thm.prop_of st))
614 in (neg_clausify (Option.valOf (metahyps_thms n st)), params) end;
616 (*Conversion of a subgoal to conjecture clauses. Each clause has
617 leading !!-bound universal variables, to express generality. *)
618 val neg_clausify_tac =
619 neg_skolemize_tac THEN'
622 let val ts = Logic.strip_assums_hyp prop
627 (map forall_intr_vars (neg_clausify hyps)) 1)),
628 REPEAT_DETERM_N (length ts) o (etac thin_rl)]
631 (** The Skolemization attribute **)
633 fun conj2_rule (th1,th2) = conjI OF [th1,th2];
635 (*Conjoin a list of theorems to form a single theorem*)
636 fun conj_rule [] = TrueI
637 | conj_rule ths = foldr1 conj2_rule ths;
639 fun skolem_attr (Context.Theory thy, th) =
640 let val (cls, thy') = skolem_cache_thm th thy
641 in (Context.Theory thy', conj_rule cls) end
642 | skolem_attr (context, th) = (context, conj_rule (skolem_use_cache_thm th));
644 val setup_attrs = Attrib.add_attributes
645 [("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem"),
646 ("clausify", clausify, "conversion of theorem to clauses")];
648 val setup_methods = Method.add_methods
649 [("neg_clausify", Method.no_args (Method.SIMPLE_METHOD' neg_clausify_tac),
650 "conversion of goal to conjecture clauses")];
652 val setup = clause_cache_setup #> setup_attrs #> setup_methods;