Improvement to classrel clauses: now outputs the minimum needed.
Theorem names: trying to minimize the number of multiple theorem names presented
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.
8 (*unused during debugging*)
11 val elimRule_tac : thm -> Tactical.tactic
12 val elimR2Fol : thm -> term
13 val transform_elim : thm -> thm
14 val cnf_axiom : (string * thm) -> thm list
15 val cnf_name : string -> thm list
16 val meta_cnf_axiom : thm -> thm list
17 val claset_rules_of_thy : theory -> (string * thm) list
18 val simpset_rules_of_thy : theory -> (string * thm) list
19 val claset_rules_of_ctxt: Proof.context -> (string * thm) list
20 val simpset_rules_of_ctxt : Proof.context -> (string * thm) list
21 val pairname : thm -> (string * thm)
22 val skolem_thm : thm -> thm list
23 val to_nnf : thm -> thm
24 val cnf_rules_pairs : (string * Thm.thm) list -> (Thm.thm * (string * int)) list list;
25 val meson_method_setup : theory -> theory
26 val setup : theory -> theory
28 val atpset_rules_of_thy : theory -> (string * thm) list
29 val atpset_rules_of_ctxt : Proof.context -> (string * thm) list
36 (*For running the comparison between combinators and abstractions.
37 CANNOT be a ref, as the setting is used while Isabelle is built.
38 Currently FALSE, i.e. all the "abstraction" code below is unused, but so far
39 it seems to be inferior to combinators...*)
40 val abstract_lambdas = false;
42 val trace_abs = ref false;
45 fun freeze_thm th = #1 (Drule.freeze_thaw th);
47 val lhs_of = #1 o Logic.dest_equals o Thm.prop_of;
48 val rhs_of = #2 o Logic.dest_equals o Thm.prop_of;
51 (*Store definitions of abstraction functions, ensuring that identical right-hand
52 sides are denoted by the same functions and thereby reducing the need for
53 extensionality in proofs.
54 FIXME! Store in theory data!!*)
56 (*Populate the abstraction cache with common combinators.*)
58 let val (_,ct) = Thm.dest_abs NONE (Drule.rhs_of th)
59 val t = Logic.legacy_varify (term_of ct)
60 in Net.insert_term eq_thm (t, th) net end;
62 val abstraction_cache = ref
63 (seed (thm"ATP_Linkup.I_simp")
64 (seed (thm"ATP_Linkup.B_simp")
65 (seed (thm"ATP_Linkup.K_simp") Net.empty)));
68 (**** Transformation of Elimination Rules into First-Order Formulas****)
70 (* a tactic used to prove an elim-rule. *)
72 (resolve_tac [impI,notI] 1) THEN (etac th 1) THEN REPEAT(fast_tac HOL_cs 1);
75 | add_EX tm ((x,xtp)::xs) = add_EX (HOLogic.exists_const xtp $ Abs(x,xtp,tm)) xs;
77 (*Checks for the premise ~P when the conclusion is P.*)
78 fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_)))
79 (Const("Trueprop",_) $ Free(q,_)) = (p = q)
84 (*Handles the case where the dummy "conclusion" variable appears negated in the
85 premises, so the final consequent must be kept.*)
86 fun strip_concl' prems bvs (Const ("==>",_) $ P $ Q) =
87 strip_concl' (HOLogic.dest_Trueprop P :: prems) bvs Q
88 | strip_concl' prems bvs P =
89 let val P' = HOLogic.Not $ (HOLogic.dest_Trueprop P)
90 in add_EX (foldr1 HOLogic.mk_conj (P'::prems)) bvs end;
92 (*Recurrsion over the minor premise of an elimination rule. Final consequent
93 is ignored, as it is the dummy "conclusion" variable.*)
94 fun strip_concl prems bvs concl (Const ("all", _) $ Abs (x,xtp,body)) =
95 strip_concl prems ((x,xtp)::bvs) concl body
96 | strip_concl prems bvs concl (Const ("==>",_) $ P $ Q) =
97 if (is_neg P concl) then (strip_concl' prems bvs Q)
98 else strip_concl (HOLogic.dest_Trueprop P::prems) bvs concl Q
99 | strip_concl prems bvs concl Q =
100 if concl aconv Q andalso not (null prems)
101 then add_EX (foldr1 HOLogic.mk_conj prems) bvs
102 else raise ELIMR2FOL (*expected conclusion not found!*)
104 fun trans_elim (major,[],_) = HOLogic.Not $ major
105 | trans_elim (major,minors,concl) =
106 let val disjs = foldr1 HOLogic.mk_disj (map (strip_concl [] [] concl) minors)
107 in HOLogic.mk_imp (major, disjs) end;
109 (* convert an elim rule into an equivalent formula, of type term. *)
110 fun elimR2Fol elimR =
111 let val elimR' = freeze_thm elimR
112 val (prems,concl) = (prems_of elimR', concl_of elimR')
113 val cv = case concl of (*conclusion variable*)
114 Const("Trueprop",_) $ (v as Free(_,Type("bool",[]))) => v
115 | v as Free(_, Type("prop",[])) => v
116 | _ => raise ELIMR2FOL
118 [] => raise ELIMR2FOL
119 | (Const("Trueprop",_) $ major) :: minors =>
120 if member (op aconv) (term_frees major) cv then raise ELIMR2FOL
121 else (trans_elim (major, minors, concl) handle TERM _ => raise ELIMR2FOL)
122 | _ => raise ELIMR2FOL
125 (* convert an elim-rule into an equivalent theorem that does not have the
126 predicate variable. Leave other theorems unchanged.*)
127 fun transform_elim th =
128 let val t = HOLogic.mk_Trueprop (elimR2Fol th)
130 if Meson.too_many_clauses t then TrueI
131 else Goal.prove_raw [] (cterm_of (sign_of_thm th) t) (fn _ => elimRule_tac th)
133 handle ELIMR2FOL => th (*not an elimination rule*)
134 | exn => (warning ("transform_elim failed: " ^ Toplevel.exn_message exn ^
135 " for theorem " ^ Thm.name_of_thm th ^ ": " ^ string_of_thm th); th)
138 (**** Transformation of Clasets and Simpsets into First-Order Axioms ****)
140 (*Transfer a theorem into theory ATP_Linkup.thy if it is not already
141 inside that theory -- because it's needed for Skolemization *)
143 (*This will refer to the final version of theory ATP_Linkup.*)
144 val recon_thy_ref = Theory.self_ref (the_context ());
146 (*If called while ATP_Linkup is being created, it will transfer to the
147 current version. If called afterward, it will transfer to the final version.*)
148 fun transfer_to_ATP_Linkup th =
149 transfer (Theory.deref recon_thy_ref) th handle THM _ => th;
153 (Const ("Trueprop", _) $ Const ("True", _)) => true
156 (* remove tautologous clauses *)
157 val rm_redundant_cls = List.filter (not o is_taut);
160 (**** SKOLEMIZATION BY INFERENCE (lcp) ****)
162 (*Traverse a theorem, declaring Skolem function definitions. String s is the suggested
163 prefix for the Skolem constant. Result is a new theory*)
164 fun declare_skofuns s th thy =
166 fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (thy, axs) =
167 (*Existential: declare a Skolem function, then insert into body and continue*)
168 let val cname = Name.internal (s ^ "_sko" ^ Int.toString (inc nref))
169 val args = term_frees xtp (*get the formal parameter list*)
170 val Ts = map type_of args
172 val c = Const (Sign.full_name thy cname, cT)
173 val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
174 (*Forms a lambda-abstraction over the formal parameters*)
175 val thy' = Sign.add_consts_authentic [(cname, cT, NoSyn)] thy
176 (*Theory is augmented with the constant, then its def*)
177 val cdef = cname ^ "_def"
178 val thy'' = Theory.add_defs_i false false [(cdef, equals cT $ c $ rhs)] thy'
179 in dec_sko (subst_bound (list_comb(c,args), p))
180 (thy'', get_axiom thy'' cdef :: axs)
182 | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) thx =
183 (*Universal quant: insert a free variable into body and continue*)
184 let val fname = Name.variant (add_term_names (p,[])) a
185 in dec_sko (subst_bound (Free(fname,T), p)) thx end
186 | dec_sko (Const ("op &", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
187 | dec_sko (Const ("op |", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
188 | dec_sko (Const ("Trueprop", _) $ p) thx = dec_sko p thx
189 | dec_sko t thx = thx (*Do nothing otherwise*)
190 in dec_sko (prop_of th) (thy,[]) end;
192 (*Traverse a theorem, accumulating Skolem function definitions.*)
193 fun assume_skofuns th =
194 let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs =
195 (*Existential: declare a Skolem function, then insert into body and continue*)
196 let val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*)
197 val args = term_frees xtp \\ skos (*the formal parameters*)
198 val Ts = map type_of args
200 val c = Free (gensym "sko_", cT)
201 val rhs = list_abs_free (map dest_Free args,
202 HOLogic.choice_const T $ xtp)
203 (*Forms a lambda-abstraction over the formal parameters*)
204 val def = equals cT $ c $ rhs
205 in dec_sko (subst_bound (list_comb(c,args), p))
208 | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) defs =
209 (*Universal quant: insert a free variable into body and continue*)
210 let val fname = Name.variant (add_term_names (p,[])) a
211 in dec_sko (subst_bound (Free(fname,T), p)) defs end
212 | dec_sko (Const ("op &", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
213 | dec_sko (Const ("op |", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
214 | dec_sko (Const ("Trueprop", _) $ p) defs = dec_sko p defs
215 | dec_sko t defs = defs (*Do nothing otherwise*)
216 in dec_sko (prop_of th) [] end;
219 (**** REPLACING ABSTRACTIONS BY FUNCTION DEFINITIONS ****)
221 (*Returns the vars of a theorem*)
223 map (Thm.cterm_of (theory_of_thm th) o Var) (Drule.fold_terms Term.add_vars th []);
225 (*Make a version of fun_cong with a given variable name*)
227 val fun_cong' = fun_cong RS asm_rl; (*renumber f, g to prevent clashes with (a,0)*)
228 val cx = hd (vars_of_thm fun_cong');
229 val ty = typ_of (ctyp_of_term cx);
230 val thy = theory_of_thm fun_cong;
231 fun mkvar a = cterm_of thy (Var((a,0),ty));
233 fun xfun_cong x = Thm.instantiate ([], [(cx, mkvar x)]) fun_cong'
236 (*Removes the lambdas from an equation of the form t = (%x. u). A non-negative n,
237 serves as an upper bound on how many to remove.*)
238 fun strip_lambdas 0 th = th
239 | strip_lambdas n th =
241 _ $ (Const ("op =", _) $ _ $ Abs (x,_,_)) =>
242 strip_lambdas (n-1) (freeze_thm (th RS xfun_cong x))
245 (*Convert meta- to object-equality. Fails for theorems like split_comp_eq,
246 where some types have the empty sort.*)
247 fun mk_object_eq th = th RS def_imp_eq
248 handle THM _ => error ("Theorem contains empty sort: " ^ string_of_thm th);
250 (*Apply a function definition to an argument, beta-reducing the result.*)
252 let val th1 = combination cf (reflexive x)
253 val th2 = beta_conversion false (Drule.rhs_of th1)
254 in transitive th1 th2 end;
256 (*Apply a function definition to arguments, beta-reducing along the way.*)
257 fun list_combination cf [] = cf
258 | list_combination cf (x::xs) = list_combination (beta_comb cf x) xs;
260 fun list_cabs ([] , t) = t
261 | list_cabs (v::vars, t) = Thm.cabs v (list_cabs(vars,t));
263 fun assert_eta_free ct =
264 let val t = term_of ct
265 in if (t aconv Envir.eta_contract t) then ()
266 else error ("Eta redex in term: " ^ string_of_cterm ct)
269 fun eq_absdef (th1, th2) =
270 Context.joinable (theory_of_thm th1, theory_of_thm th2) andalso
271 rhs_of th1 aconv rhs_of th2;
273 fun lambda_free (Abs _) = false
274 | lambda_free (t $ u) = lambda_free t andalso lambda_free u
275 | lambda_free _ = true;
278 Term.fold_types (Term.fold_atyps (fn TVar _ => K false | _ => I)) t true;
280 fun dest_abs_list ct =
281 let val (cv,ct') = Thm.dest_abs NONE ct
282 val (cvs,cu) = dest_abs_list ct'
284 handle CTERM _ => ([],ct);
286 fun lambda_list [] u = u
287 | lambda_list (v::vs) u = lambda v (lambda_list vs u);
289 fun abstract_rule_list [] [] th = th
290 | abstract_rule_list (v::vs) (ct::cts) th = abstract_rule v ct (abstract_rule_list vs cts th)
291 | abstract_rule_list _ _ th = raise THM ("abstract_rule_list", 0, [th]);
294 val Envir.Envir {asol = tenv0, iTs = tyenv0, ...} = Envir.empty 0
296 (*Does an existing abstraction definition have an RHS that matches the one we need now?
297 thy is the current theory, which must extend that of theorem th.*)
298 fun match_rhs thy t th =
299 let val _ = if !trace_abs then warning ("match_rhs: " ^ string_of_cterm (cterm_of thy t) ^
300 " against\n" ^ string_of_thm th) else ();
301 val (tyenv,tenv) = Pattern.first_order_match thy (rhs_of th, t) (tyenv0,tenv0)
302 val term_insts = map Meson.term_pair_of (Vartab.dest tenv)
303 val ct_pairs = if subthy (theory_of_thm th, thy) andalso
304 forall lambda_free (map #2 term_insts)
305 then map (pairself (cterm_of thy)) term_insts
306 else raise Pattern.MATCH (*Cannot allow lambdas in the instantiation*)
307 fun ctyp2 (ixn, (S, T)) = (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T)
308 val th' = cterm_instantiate ct_pairs th
309 in SOME (th, instantiate (map ctyp2 (Vartab.dest tyenv), []) th') end
312 (*Traverse a theorem, declaring abstraction function definitions. String s is the suggested
313 prefix for the constants. Resulting theory is returned in the first theorem. *)
314 fun declare_absfuns th =
315 let fun abstract thy ct =
316 if lambda_free (term_of ct) then (transfer thy (reflexive ct), [])
320 let val cname = Name.internal (gensym "abs_");
321 val _ = assert_eta_free ct;
322 val (cvs,cta) = dest_abs_list ct
323 val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs)
324 val _ = if !trace_abs then warning ("Nested lambda: " ^ string_of_cterm cta) else ();
325 val (u'_th,defs) = abstract thy cta
326 val _ = if !trace_abs then warning ("Returned " ^ string_of_thm u'_th) else ();
327 val cu' = Drule.rhs_of u'_th
329 val abs_v_u = lambda_list (map term_of cvs) u'
330 (*get the formal parameters: ALL variables free in the term*)
331 val args = term_frees abs_v_u
332 val _ = if !trace_abs then warning (Int.toString (length args) ^ " arguments") else ();
333 val rhs = list_abs_free (map dest_Free args, abs_v_u)
334 (*Forms a lambda-abstraction over the formal parameters*)
335 val _ = if !trace_abs then warning ("Looking up " ^ string_of_cterm cu') else ();
336 val thy = theory_of_thm u'_th
338 case List.mapPartial (match_rhs thy abs_v_u)
339 (Net.match_term (!abstraction_cache) u') of
341 (if !trace_abs then warning ("Re-using axiom " ^ string_of_thm ax) else ();
344 let val _ = if !trace_abs then warning "Lookup was empty" else ();
345 val Ts = map type_of args
346 val cT = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu'))
347 val c = Const (Sign.full_name thy cname, cT)
348 val thy = Sign.add_consts_authentic [(cname, cT, NoSyn)] thy
349 (*Theory is augmented with the constant,
350 then its definition*)
351 val cdef = cname ^ "_def"
352 val thy = Theory.add_defs_i false false
353 [(cdef, equals cT $ c $ rhs)] thy
354 val _ = if !trace_abs then (warning ("Definition is " ^
355 string_of_thm (get_axiom thy cdef)))
357 val ax = get_axiom thy cdef |> freeze_thm
358 |> mk_object_eq |> strip_lambdas (length args)
359 |> mk_meta_eq |> Meson.generalize
360 val (_,ax') = Option.valOf (match_rhs thy abs_v_u ax)
361 val _ = if !trace_abs then
362 (warning ("Declaring: " ^ string_of_thm ax);
363 warning ("Instance: " ^ string_of_thm ax'))
365 val _ = abstraction_cache := Net.insert_term eq_absdef
366 ((Logic.varify u'), ax) (!abstraction_cache)
368 raise THM ("declare_absfuns: INSERT", 0, [th,u'_th,ax])
370 in if !trace_abs then warning ("Lookup result: " ^ string_of_thm ax') else ();
371 (transitive (abstract_rule_list vs cvs u'_th) (symmetric ax'), ax::defs) end
373 let val (ct1,ct2) = Thm.dest_comb ct
374 val (th1,defs1) = abstract thy ct1
375 val (th2,defs2) = abstract (theory_of_thm th1) ct2
376 in (combination th1 th2, defs1@defs2) end
377 val _ = if !trace_abs then warning ("declare_absfuns, Abstracting: " ^ string_of_thm th) else ();
378 val (eqth,defs) = abstract (theory_of_thm th) (cprop_of th)
379 val ths = equal_elim eqth th :: map (strip_lambdas ~1 o mk_object_eq o freeze_thm) defs
380 val _ = if !trace_abs then warning ("declare_absfuns, Result: " ^ string_of_thm (hd ths)) else ();
381 in (theory_of_thm eqth, map Drule.eta_contraction_rule ths) end;
383 fun name_of def = try (#1 o dest_Free o lhs_of) def;
385 (*A name is valid provided it isn't the name of a defined abstraction.*)
386 fun valid_name defs (Free(x,T)) = not (x mem_string (List.mapPartial name_of defs))
387 | valid_name defs _ = false;
389 fun assume_absfuns th =
390 let val thy = theory_of_thm th
391 val cterm = cterm_of thy
393 if lambda_free (term_of ct) then (reflexive ct, [])
397 let val _ = assert_eta_free ct;
398 val (cvs,cta) = dest_abs_list ct
399 val (vs,Tvs) = ListPair.unzip (map (dest_Free o term_of) cvs)
400 val (u'_th,defs) = abstract cta
401 val cu' = Drule.rhs_of u'_th
403 (*Could use Thm.cabs instead of lambda to work at level of cterms*)
404 val abs_v_u = lambda_list (map term_of cvs) (term_of cu')
405 (*get the formal parameters: free variables not present in the defs
406 (to avoid taking abstraction function names as parameters) *)
407 val args = filter (valid_name defs) (term_frees abs_v_u)
408 val crhs = list_cabs (map cterm args, cterm abs_v_u)
409 (*Forms a lambda-abstraction over the formal parameters*)
410 val rhs = term_of crhs
412 case List.mapPartial (match_rhs thy abs_v_u)
413 (Net.match_term (!abstraction_cache) u') of
415 (if !trace_abs then warning ("Re-using axiom " ^ string_of_thm ax) else ();
418 let val Ts = map type_of args
419 val const_ty = Ts ---> (Tvs ---> typ_of (ctyp_of_term cu'))
420 val c = Free (gensym "abs_", const_ty)
421 val ax = assume (Thm.capply (cterm (equals const_ty $ c)) crhs)
422 |> mk_object_eq |> strip_lambdas (length args)
423 |> mk_meta_eq |> Meson.generalize
424 val (_,ax') = Option.valOf (match_rhs thy abs_v_u ax)
425 val _ = abstraction_cache := Net.insert_term eq_absdef (rhs,ax)
428 raise THM ("assume_absfuns: INSERT", 0, [th,u'_th,ax])
430 in if !trace_abs then warning ("Lookup result: " ^ string_of_thm ax') else ();
431 (transitive (abstract_rule_list vs cvs u'_th) (symmetric ax'), ax::defs) end
433 let val (ct1,ct2) = Thm.dest_comb ct
434 val (t1',defs1) = abstract ct1
435 val (t2',defs2) = abstract ct2
436 in (combination t1' t2', defs1@defs2) end
437 val _ = if !trace_abs then warning ("assume_absfuns, Abstracting: " ^ string_of_thm th) else ();
438 val (eqth,defs) = abstract (cprop_of th)
439 val ths = equal_elim eqth th :: map (strip_lambdas ~1 o mk_object_eq o freeze_thm) defs
440 val _ = if !trace_abs then warning ("assume_absfuns, Result: " ^ string_of_thm (hd ths)) else ();
441 in map Drule.eta_contraction_rule ths end;
444 (*cterms are used throughout for efficiency*)
445 val cTrueprop = Thm.cterm_of HOL.thy HOLogic.Trueprop;
447 (*cterm version of mk_cTrueprop*)
448 fun c_mkTrueprop A = Thm.capply cTrueprop A;
450 (*Given an abstraction over n variables, replace the bound variables by free
451 ones. Return the body, along with the list of free variables.*)
452 fun c_variant_abs_multi (ct0, vars) =
453 let val (cv,ct) = Thm.dest_abs NONE ct0
454 in c_variant_abs_multi (ct, cv::vars) end
455 handle CTERM _ => (ct0, rev vars);
457 (*Given the definition of a Skolem function, return a theorem to replace
458 an existential formula by a use of that function.
459 Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *)
460 fun skolem_of_def def =
461 let val (c,rhs) = Drule.dest_equals (cprop_of (freeze_thm def))
462 val (ch, frees) = c_variant_abs_multi (rhs, [])
463 val (chilbert,cabs) = Thm.dest_comb ch
464 val {sign,t, ...} = rep_cterm chilbert
465 val T = case t of Const ("Hilbert_Choice.Eps", Type("fun",[_,T])) => T
466 | _ => raise THM ("skolem_of_def: expected Eps", 0, [def])
467 val cex = Thm.cterm_of sign (HOLogic.exists_const T)
468 val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
469 and conc = c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees)));
470 fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS someI_ex) 1
471 in Goal.prove_raw [ex_tm] conc tacf
472 |> forall_intr_list frees
473 |> forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*)
477 (*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
479 th |> transfer_to_ATP_Linkup
480 |> transform_elim |> zero_var_indexes |> freeze_thm
481 |> ObjectLogic.atomize_thm |> make_nnf |> strip_lambdas ~1;
483 (*The cache prevents repeated clausification of a theorem,
484 and also repeated declaration of Skolem functions*)
485 (* FIXME better use Termtab!? No, we MUST use theory data!!*)
486 val clause_cache = ref (Symtab.empty : (thm * thm list) Symtab.table)
489 (*Generate Skolem functions for a theorem supplied in nnf*)
490 fun skolem_of_nnf th =
491 map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns th);
493 fun assert_lambda_free ths msg =
494 case filter (not o lambda_free o prop_of) ths of
496 | ths' => error (msg ^ "\n" ^ space_implode "\n" (map string_of_thm ths'));
498 fun assume_abstract th =
499 if lambda_free (prop_of th) then [th]
500 else th |> Drule.eta_contraction_rule |> assume_absfuns
501 |> tap (fn ths => assert_lambda_free ths "assume_abstract: lambdas")
503 (*Replace lambdas by assumed function definitions in the theorems*)
504 fun assume_abstract_list ths =
505 if abstract_lambdas then List.concat (map assume_abstract ths)
506 else map Drule.eta_contraction_rule ths;
508 (*Replace lambdas by declared function definitions in the theorems*)
509 fun declare_abstract' (thy, []) = (thy, [])
510 | declare_abstract' (thy, th::ths) =
511 let val (thy', th_defs) =
512 if lambda_free (prop_of th) then (thy, [th])
514 th |> zero_var_indexes |> freeze_thm
515 |> Drule.eta_contraction_rule |> transfer thy |> declare_absfuns
516 val _ = assert_lambda_free th_defs "declare_abstract: lambdas"
517 val (thy'', ths') = declare_abstract' (thy', ths)
518 in (thy'', th_defs @ ths') end;
520 fun declare_abstract (thy, ths) =
521 if abstract_lambdas then declare_abstract' (thy, ths)
522 else (thy, map Drule.eta_contraction_rule ths);
524 (*Skolemize a named theorem, with Skolem functions as additional premises.*)
526 let val nnfth = to_nnf th
527 in Meson.make_cnf (skolem_of_nnf nnfth) nnfth
528 |> assume_abstract_list |> Meson.finish_cnf |> rm_redundant_cls
532 (*Keep the full complexity of the original name*)
533 fun flatten_name s = space_implode "_X" (NameSpace.unpack s);
535 (*Declare Skolem functions for a theorem, supplied in nnf and with its name.
536 It returns a modified theory, unless skolemization fails.*)
537 fun skolem thy (name,th) =
538 let val cname = (case name of "" => gensym "" | s => flatten_name s)
539 val _ = Output.debug ("skolemizing " ^ name ^ ": ")
542 let val (thy',defs) = declare_skofuns cname nnfth thy
543 val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth
544 val (thy'',cnfs') = declare_abstract (thy',cnfs)
545 in (thy'', rm_redundant_cls (Meson.finish_cnf cnfs'))
547 (SOME (to_nnf th) handle THM _ => NONE)
550 (*Populate the clause cache using the supplied theorem. Return the clausal form
551 and modified theory.*)
552 fun skolem_cache_thm (name,th) thy =
553 case Symtab.lookup (!clause_cache) name of
555 (case skolem thy (name, Thm.transfer thy th) of
558 let val cls = map Drule.local_standard cls
560 if null cls then warning ("skolem_cache: empty clause set for " ^ name)
562 change clause_cache (Symtab.update (name, (th, cls)));
566 if eq_thm(th,th') then (cls,thy)
567 else (Output.debug ("skolem_cache: Ignoring variant of theorem " ^ name);
568 Output.debug (string_of_thm th);
569 Output.debug (string_of_thm th');
572 (*Exported function to convert Isabelle theorems into axiom clauses*)
573 fun cnf_axiom (name,th) =
574 (Output.debug ("cnf_axiom called, theorem name = " ^ name);
576 "" => skolem_thm th (*no name, so can't cache*)
577 | s => case Symtab.lookup (!clause_cache) s of
579 let val cls = map Drule.local_standard (skolem_thm th)
580 in Output.debug "inserted into cache";
581 change clause_cache (Symtab.update (s, (th, cls))); cls
584 if eq_thm(th,th') then cls
585 else (Output.debug ("cnf_axiom: duplicate or variant of theorem " ^ name);
586 Output.debug (string_of_thm th);
587 Output.debug (string_of_thm th');
591 fun pairname th = (Thm.name_of_thm th, th);
593 (*Principally for debugging*)
596 in cnf_axiom (Thm.name_of_thm th, th) end;
598 (**** Extract and Clausify theorems from a theory's claset and simpset ****)
600 (*Preserve the name of "th" after the transformation "f"*)
601 fun preserve_name f th = Thm.name_thm (Thm.name_of_thm th, f th);
603 fun rules_of_claset cs =
604 let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs
605 val intros = safeIs @ hazIs
606 val elims = map Classical.classical_rule (safeEs @ hazEs)
608 Output.debug ("rules_of_claset intros: " ^ Int.toString(length intros) ^
609 " elims: " ^ Int.toString(length elims));
610 map pairname (intros @ elims)
613 fun rules_of_simpset ss =
614 let val ({rules,...}, _) = rep_ss ss
615 val simps = Net.entries rules
617 Output.debug ("rules_of_simpset: " ^ Int.toString(length simps));
618 map (fn r => (#name r, #thm r)) simps
621 fun claset_rules_of_thy thy = rules_of_claset (claset_of thy);
622 fun simpset_rules_of_thy thy = rules_of_simpset (simpset_of thy);
624 fun atpset_rules_of_thy thy = map pairname (ResAtpset.get_atpset (Context.Theory thy));
627 fun claset_rules_of_ctxt ctxt = rules_of_claset (local_claset_of ctxt);
628 fun simpset_rules_of_ctxt ctxt = rules_of_simpset (local_simpset_of ctxt);
630 fun atpset_rules_of_ctxt ctxt = map pairname (ResAtpset.get_atpset (Context.Proof ctxt));
633 (**** Translate a set of classical/simplifier rules into CNF (still as type "thm") ****)
635 (* classical rules: works for both FOL and HOL *)
636 fun cnf_rules [] err_list = ([],err_list)
637 | cnf_rules ((name,th) :: ths) err_list =
638 let val (ts,es) = cnf_rules ths err_list
639 in (cnf_axiom (name,th) :: ts,es) handle _ => (ts, (th::es)) end;
641 fun pair_name_cls k (n, []) = []
642 | pair_name_cls k (n, cls::clss) = (cls, (n,k)) :: pair_name_cls (k+1) (n, clss)
644 fun cnf_rules_pairs_aux pairs [] = pairs
645 | cnf_rules_pairs_aux pairs ((name,th)::ths) =
646 let val pairs' = (pair_name_cls 0 (name, cnf_axiom(name,th))) @ pairs
647 handle THM _ => pairs | ResClause.CLAUSE _ => pairs
648 in cnf_rules_pairs_aux pairs' ths end;
650 (*The combination of rev and tail recursion preserves the original order*)
651 fun cnf_rules_pairs l = cnf_rules_pairs_aux [] (rev l);
654 (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)
656 (*Setup function: takes a theory and installs ALL known theorems into the clause cache*)
658 fun skolem_cache (name,th) thy =
659 let val prop = Thm.prop_of th
662 (*Monomorphic theorems can be Skolemized on demand,
663 but there are problems with re-use of abstraction functions if we don't
664 do them now, even for monomorphic theorems.*)
666 else #2 (skolem_cache_thm (name,th) thy)
669 (*The cache can be kept smaller by augmenting the condition above with
670 orelse (not abstract_lambdas andalso monomorphic prop).
671 However, while this step does not reduce the time needed to build HOL,
672 it doubles the time taken by the first call to the ATP link-up.*)
674 fun clause_cache_setup thy = fold skolem_cache (PureThy.all_thms_of thy) thy;
677 (*** meson proof methods ***)
679 fun skolem_use_cache_thm th =
680 case Symtab.lookup (!clause_cache) (Thm.name_of_thm th) of
681 NONE => skolem_thm th
683 if eq_thm(th,th') then cls else skolem_thm th;
685 fun cnf_rules_of_ths ths = List.concat (map skolem_use_cache_thm ths);
687 fun meson_meth ths ctxt =
688 Method.SIMPLE_METHOD' HEADGOAL
689 (CHANGED_PROP o Meson.meson_claset_tac (cnf_rules_of_ths ths) HOL_cs);
691 val meson_method_setup =
693 [("meson", Method.thms_ctxt_args meson_meth,
694 "MESON resolution proof procedure")];
696 (** Attribute for converting a theorem into clauses **)
698 fun meta_cnf_axiom th = map Meson.make_meta_clause (cnf_axiom (pairname th));
700 fun clausify_rule (th,i) = List.nth (meta_cnf_axiom th, i)
702 val clausify = Attrib.syntax (Scan.lift Args.nat
703 >> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i))));
705 (** The Skolemization attribute **)
707 fun conj2_rule (th1,th2) = conjI OF [th1,th2];
709 (*Conjoin a list of theorems to form a single theorem*)
710 fun conj_rule [] = TrueI
711 | conj_rule ths = foldr1 conj2_rule ths;
713 fun skolem_attr (Context.Theory thy, th) =
714 let val name = Thm.name_of_thm th
715 val (cls, thy') = skolem_cache_thm (name, th) thy
716 in (Context.Theory thy', conj_rule cls) end
717 | skolem_attr (context, th) = (context, conj_rule (skolem_use_cache_thm th));
719 val setup_attrs = Attrib.add_attributes
720 [("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem"),
721 ("clausify", clausify, "conversion to clauses")];
723 val setup = clause_cache_setup #> setup_attrs;