# HG changeset patch # User wenzelm # Date 1157144682 -7200 # Node ID d689ad772b2cd263513c9463a9b1a1d38da6ea55 # Parent 351c63bb2704a7dc67446f2675d40f166c9d2bff skolem_cache_thm: Drule.close_derivation on clauses preserves some space; tuned skolem_cache operations: canonical argument order; tuned monomorphic test; diff -r 351c63bb2704 -r d689ad772b2c src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Fri Sep 01 20:44:16 2006 +0200 +++ b/src/HOL/Tools/res_axioms.ML Fri Sep 01 23:04:42 2006 +0200 @@ -2,7 +2,7 @@ ID: $Id$ Copyright 2004 University of Cambridge -Transformation of axiom rules (elim/intro/etc) into CNF forms. +Transformation of axiom rules (elim/intro/etc) into CNF forms. *) (*FIXME: does this signature serve any purpose?*) @@ -27,9 +27,9 @@ val atpset_rules_of_thy : theory -> (string * thm) list val atpset_rules_of_ctxt : Proof.context -> (string * thm) list end; - + structure ResAxioms = - + struct (*FIXME DELETE: For running the comparison between combinators and abstractions. @@ -54,7 +54,7 @@ | add_EX tm ((x,xtp)::xs) = add_EX (HOLogic.exists_const xtp $ Abs(x,xtp,tm)) xs; (*Checks for the premise ~P when the conclusion is P.*) -fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_))) +fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_))) (Const("Trueprop",_) $ Free(q,_)) = (p = q) | is_neg _ _ = false; @@ -64,50 +64,50 @@ premises, so the final consequent must be kept.*) fun strip_concl' prems bvs (Const ("==>",_) $ P $ Q) = strip_concl' (HOLogic.dest_Trueprop P :: prems) bvs Q - | strip_concl' prems bvs P = + | strip_concl' prems bvs P = let val P' = HOLogic.Not $ (HOLogic.dest_Trueprop P) in add_EX (foldr1 HOLogic.mk_conj (P'::prems)) bvs end; (*Recurrsion over the minor premise of an elimination rule. Final consequent is ignored, as it is the dummy "conclusion" variable.*) -fun strip_concl prems bvs concl (Const ("all", _) $ Abs (x,xtp,body)) = +fun strip_concl prems bvs concl (Const ("all", _) $ Abs (x,xtp,body)) = strip_concl prems ((x,xtp)::bvs) concl body | strip_concl prems bvs concl (Const ("==>",_) $ P $ Q) = if (is_neg P concl) then (strip_concl' prems bvs Q) else strip_concl (HOLogic.dest_Trueprop P::prems) bvs concl Q - | strip_concl prems bvs concl Q = + | strip_concl prems bvs concl Q = if concl aconv Q then add_EX (foldr1 HOLogic.mk_conj prems) bvs else raise ELIMR2FOL (*expected conclusion not found!*) - + fun trans_elim (major,[],_) = HOLogic.Not $ major | trans_elim (major,minors,concl) = let val disjs = foldr1 HOLogic.mk_disj (map (strip_concl [] [] concl) minors) in HOLogic.mk_imp (major, disjs) end; (* convert an elim rule into an equivalent formula, of type term. *) -fun elimR2Fol elimR = +fun elimR2Fol elimR = let val elimR' = #1 (Drule.freeze_thaw elimR) val (prems,concl) = (prems_of elimR', concl_of elimR') val cv = case concl of (*conclusion variable*) - Const("Trueprop",_) $ (v as Free(_,Type("bool",[]))) => v - | v as Free(_, Type("prop",[])) => v - | _ => raise ELIMR2FOL + Const("Trueprop",_) $ (v as Free(_,Type("bool",[]))) => v + | v as Free(_, Type("prop",[])) => v + | _ => raise ELIMR2FOL in case prems of [] => raise ELIMR2FOL - | (Const("Trueprop",_) $ major) :: minors => + | (Const("Trueprop",_) $ major) :: minors => if member (op aconv) (term_frees major) cv then raise ELIMR2FOL else (trans_elim (major, minors, concl) handle TERM _ => raise ELIMR2FOL) | _ => raise ELIMR2FOL end; -(* convert an elim-rule into an equivalent theorem that does not have the - predicate variable. Leave other theorems unchanged.*) +(* convert an elim-rule into an equivalent theorem that does not have the + predicate variable. Leave other theorems unchanged.*) fun transform_elim th = let val ctm = cterm_of (sign_of_thm th) (HOLogic.mk_Trueprop (elimR2Fol th)) in Goal.prove_raw [] ctm (fn _ => elimRule_tac th) end handle ELIMR2FOL => th (*not an elimination rule*) - | exn => (warning ("transform_elim failed: " ^ Toplevel.exn_message exn ^ - " for theorem " ^ string_of_thm th); th) + | exn => (warning ("transform_elim failed: " ^ Toplevel.exn_message exn ^ + " for theorem " ^ string_of_thm th); th) (**** Transformation of Clasets and Simpsets into First-Order Axioms ****) @@ -116,7 +116,7 @@ inside that theory -- because it's needed for Skolemization *) (*This will refer to the final version of theory Reconstruction.*) -val recon_thy_ref = Theory.self_ref (the_context ()); +val recon_thy_ref = Theory.self_ref (the_context ()); (*If called while Reconstruction is being created, it will transfer to the current version. If called afterward, it will transfer to the final version.*) @@ -130,63 +130,63 @@ (* remove tautologous clauses *) val rm_redundant_cls = List.filter (not o is_taut); - - + + (**** SKOLEMIZATION BY INFERENCE (lcp) ****) (*Traverse a theorem, declaring Skolem function definitions. String s is the suggested prefix for the Skolem constant. Result is a new theory*) fun declare_skofuns s th thy = let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (thy, axs) = - (*Existential: declare a Skolem function, then insert into body and continue*) - let val cname = gensym ("sko_" ^ s ^ "_") - val args = term_frees xtp (*get the formal parameter list*) - val Ts = map type_of args - val cT = Ts ---> T - val c = Const (Sign.full_name thy cname, cT) - val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp) - (*Forms a lambda-abstraction over the formal parameters*) - val thy' = Theory.add_consts_i [(cname, cT, NoSyn)] thy - (*Theory is augmented with the constant, then its def*) - val cdef = cname ^ "_def" - val thy'' = Theory.add_defs_i false false [(cdef, equals cT $ c $ rhs)] thy' - in dec_sko (subst_bound (list_comb(c,args), p)) - (thy'', get_axiom thy'' cdef :: axs) - end - | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) thx = - (*Universal quant: insert a free variable into body and continue*) - let val fname = Name.variant (add_term_names (p,[])) a - in dec_sko (subst_bound (Free(fname,T), p)) thx end - | dec_sko (Const ("op &", _) $ p $ q) thx = dec_sko q (dec_sko p thx) - | dec_sko (Const ("op |", _) $ p $ q) thx = dec_sko q (dec_sko p thx) - | dec_sko (Const ("Trueprop", _) $ p) thx = dec_sko p thx - | dec_sko t thx = thx (*Do nothing otherwise*) + (*Existential: declare a Skolem function, then insert into body and continue*) + let val cname = gensym ("sko_" ^ s ^ "_") + val args = term_frees xtp (*get the formal parameter list*) + val Ts = map type_of args + val cT = Ts ---> T + val c = Const (Sign.full_name thy cname, cT) + val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp) + (*Forms a lambda-abstraction over the formal parameters*) + val thy' = Theory.add_consts_i [(cname, cT, NoSyn)] thy + (*Theory is augmented with the constant, then its def*) + val cdef = cname ^ "_def" + val thy'' = Theory.add_defs_i false false [(cdef, equals cT $ c $ rhs)] thy' + in dec_sko (subst_bound (list_comb(c,args), p)) + (thy'', get_axiom thy'' cdef :: axs) + end + | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) thx = + (*Universal quant: insert a free variable into body and continue*) + let val fname = Name.variant (add_term_names (p,[])) a + in dec_sko (subst_bound (Free(fname,T), p)) thx end + | dec_sko (Const ("op &", _) $ p $ q) thx = dec_sko q (dec_sko p thx) + | dec_sko (Const ("op |", _) $ p $ q) thx = dec_sko q (dec_sko p thx) + | dec_sko (Const ("Trueprop", _) $ p) thx = dec_sko p thx + | dec_sko t thx = thx (*Do nothing otherwise*) in dec_sko (prop_of th) (thy,[]) end; (*Traverse a theorem, accumulating Skolem function definitions.*) fun assume_skofuns th = let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs = - (*Existential: declare a Skolem function, then insert into body and continue*) - let val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*) - val args = term_frees xtp \\ skos (*the formal parameters*) - val Ts = map type_of args - val cT = Ts ---> T - val c = Free (gensym "sko_", cT) - val rhs = list_abs_free (map dest_Free args, - HOLogic.choice_const T $ xtp) - (*Forms a lambda-abstraction over the formal parameters*) - val def = equals cT $ c $ rhs - in dec_sko (subst_bound (list_comb(c,args), p)) - (def :: defs) - end - | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) defs = - (*Universal quant: insert a free variable into body and continue*) - let val fname = Name.variant (add_term_names (p,[])) a - in dec_sko (subst_bound (Free(fname,T), p)) defs end - | dec_sko (Const ("op &", _) $ p $ q) defs = dec_sko q (dec_sko p defs) - | dec_sko (Const ("op |", _) $ p $ q) defs = dec_sko q (dec_sko p defs) - | dec_sko (Const ("Trueprop", _) $ p) defs = dec_sko p defs - | dec_sko t defs = defs (*Do nothing otherwise*) + (*Existential: declare a Skolem function, then insert into body and continue*) + let val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*) + val args = term_frees xtp \\ skos (*the formal parameters*) + val Ts = map type_of args + val cT = Ts ---> T + val c = Free (gensym "sko_", cT) + val rhs = list_abs_free (map dest_Free args, + HOLogic.choice_const T $ xtp) + (*Forms a lambda-abstraction over the formal parameters*) + val def = equals cT $ c $ rhs + in dec_sko (subst_bound (list_comb(c,args), p)) + (def :: defs) + end + | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) defs = + (*Universal quant: insert a free variable into body and continue*) + let val fname = Name.variant (add_term_names (p,[])) a + in dec_sko (subst_bound (Free(fname,T), p)) defs end + | dec_sko (Const ("op &", _) $ p $ q) defs = dec_sko q (dec_sko p defs) + | dec_sko (Const ("op |", _) $ p $ q) defs = dec_sko q (dec_sko p defs) + | dec_sko (Const ("Trueprop", _) $ p) defs = dec_sko p defs + | dec_sko t defs = defs (*Do nothing otherwise*) in dec_sko (prop_of th) [] end; @@ -208,27 +208,27 @@ end; (*Removes the lambdas from an equation of the form t = (%x. u)*) -fun strip_lambdas th = +fun strip_lambdas th = case prop_of th of - _ $ (Const ("op =", _) $ _ $ Abs (x,_,_)) => + _ $ (Const ("op =", _) $ _ $ Abs (x,_,_)) => strip_lambdas (#1 (Drule.freeze_thaw (th RS xfun_cong x))) | _ => th; -(*Convert meta- to object-equality. Fails for theorems like split_comp_eq, +(*Convert meta- to object-equality. Fails for theorems like split_comp_eq, where some types have the empty sort.*) -fun object_eq th = th RS def_imp_eq +fun object_eq th = th RS def_imp_eq handle THM _ => error ("Theorem contains empty sort: " ^ string_of_thm th); - + fun valid_name vs (Free(x,T)) = x mem_string vs | valid_name vs _ = false; (*Contract all eta-redexes in the theorem, lest they give rise to needless abstractions*) fun eta_conversion_rule th = equal_elim (eta_conversion (cprop_of th)) th; - + fun crhs_of th = case Drule.strip_comb (cprop_of th) of - (f, [_, rhs]) => + (f, [_, rhs]) => (case term_of f of Const ("==", _) => rhs | _ => raise THM ("crhs_of", 0, [th])) | _ => raise THM ("crhs_of", 1, [th]); @@ -250,71 +250,74 @@ fun list_cabs ([] , t) = t | list_cabs (v::vars, t) = Thm.cabs v (list_cabs(vars,t)); -fun assert_eta_free ct = - let val t = term_of ct - in if (t aconv Envir.eta_contract t) then () +fun assert_eta_free ct = + let val t = term_of ct + in if (t aconv Envir.eta_contract t) then () else error ("Eta redex in term: " ^ string_of_cterm ct) end; -fun eq_absdef (th1, th2) = +fun eq_absdef (th1, th2) = Context.joinable (theory_of_thm th1, theory_of_thm th2) andalso rhs_of th1 aconv rhs_of th2; fun lambda_free (Abs _) = false | lambda_free (t $ u) = lambda_free t andalso lambda_free u | lambda_free _ = true; - + +fun monomorphic t = + Term.fold_types (Term.fold_atyps (fn TVar _ => K false | _ => I)) t true; + (*Traverse a theorem, declaring abstraction function definitions. String s is the suggested prefix for the constants. Resulting theory is returned in the first theorem. *) fun declare_absfuns th = - let fun abstract thy ct = + let fun abstract thy ct = if lambda_free (term_of ct) then (transfer thy (reflexive ct), []) else case term_of ct of Abs (_,T,u) => - let val cname = gensym "abs_" - val _ = assert_eta_free ct; - val (cv,cta) = Thm.dest_abs NONE ct - val v = (#1 o dest_Free o term_of) cv - val (u'_th,defs) = abstract thy cta + let val cname = gensym "abs_" + val _ = assert_eta_free ct; + val (cv,cta) = Thm.dest_abs NONE ct + val v = (#1 o dest_Free o term_of) cv + val (u'_th,defs) = abstract thy cta val cu' = crhs_of u'_th - val abs_v_u = lambda (term_of cv) (term_of cu') - (*get the formal parameters: ALL variables free in the term*) - val args = term_frees abs_v_u - val rhs = list_abs_free (map dest_Free args, abs_v_u) - (*Forms a lambda-abstraction over the formal parameters*) - val v_rhs = Logic.varify rhs - val (ax,thy) = - case List.find (fn ax => v_rhs aconv rhs_of ax) - (Net.match_term (!abstraction_cache) v_rhs) of - SOME ax => (ax,thy) (*cached axiom, current theory*) - | NONE => - let val Ts = map type_of args - val cT = Ts ---> (T --> typ_of (ctyp_of_term cu')) - val thy = theory_of_thm u'_th - val c = Const (Sign.full_name thy cname, cT) - val thy = Theory.add_consts_i [(cname, cT, NoSyn)] thy - (*Theory is augmented with the constant, - then its definition*) - val cdef = cname ^ "_def" - val thy = Theory.add_defs_i false false - [(cdef, equals cT $ c $ rhs)] thy - val ax = get_axiom thy cdef - val _ = abstraction_cache := Net.insert_term eq_absdef (v_rhs,ax) - (!abstraction_cache) - handle Net.INSERT => - raise THM ("declare_absfuns: INSERT", 0, [th,u'_th,ax]) - in (ax,thy) end - val _ = assert (v_rhs aconv rhs_of ax) "declare_absfuns: rhs mismatch" - val def = #1 (Drule.freeze_thaw ax) - val def_args = list_combination def (map (cterm_of thy) args) - in (transitive (abstract_rule v cv u'_th) (symmetric def_args), - def :: defs) end - | (t1$t2) => - let val (ct1,ct2) = Thm.dest_comb ct - val (th1,defs1) = abstract thy ct1 - val (th2,defs2) = abstract (theory_of_thm th1) ct2 - in (combination th1 th2, defs1@defs2) end + val abs_v_u = lambda (term_of cv) (term_of cu') + (*get the formal parameters: ALL variables free in the term*) + val args = term_frees abs_v_u + val rhs = list_abs_free (map dest_Free args, abs_v_u) + (*Forms a lambda-abstraction over the formal parameters*) + val v_rhs = Logic.varify rhs + val (ax,thy) = + case List.find (fn ax => v_rhs aconv rhs_of ax) + (Net.match_term (!abstraction_cache) v_rhs) of + SOME ax => (ax,thy) (*cached axiom, current theory*) + | NONE => + let val Ts = map type_of args + val cT = Ts ---> (T --> typ_of (ctyp_of_term cu')) + val thy = theory_of_thm u'_th + val c = Const (Sign.full_name thy cname, cT) + val thy = Theory.add_consts_i [(cname, cT, NoSyn)] thy + (*Theory is augmented with the constant, + then its definition*) + val cdef = cname ^ "_def" + val thy = Theory.add_defs_i false false + [(cdef, equals cT $ c $ rhs)] thy + val ax = get_axiom thy cdef + val _ = abstraction_cache := Net.insert_term eq_absdef (v_rhs,ax) + (!abstraction_cache) + handle Net.INSERT => + raise THM ("declare_absfuns: INSERT", 0, [th,u'_th,ax]) + in (ax,thy) end + val _ = assert (v_rhs aconv rhs_of ax) "declare_absfuns: rhs mismatch" + val def = #1 (Drule.freeze_thaw ax) + val def_args = list_combination def (map (cterm_of thy) args) + in (transitive (abstract_rule v cv u'_th) (symmetric def_args), + def :: defs) end + | (t1$t2) => + let val (ct1,ct2) = Thm.dest_comb ct + val (th1,defs1) = abstract thy ct1 + val (th2,defs2) = abstract (theory_of_thm th1) ct2 + in (combination th1 th2, defs1@defs2) end val _ = if !trace_abs then warning (string_of_thm th) else (); val (eqth,defs) = abstract (theory_of_thm th) (cprop_of th) val ths = equal_elim eqth th :: @@ -324,46 +327,46 @@ fun assume_absfuns th = let val thy = theory_of_thm th val cterm = cterm_of thy - fun abstract vs ct = + fun abstract vs ct = if lambda_free (term_of ct) then (reflexive ct, []) else case term_of ct of Abs (_,T,u) => - let val (cv,cta) = Thm.dest_abs NONE ct - val _ = assert_eta_free ct; - val v = (#1 o dest_Free o term_of) cv - val (u'_th,defs) = abstract (v::vs) cta + let val (cv,cta) = Thm.dest_abs NONE ct + val _ = assert_eta_free ct; + val v = (#1 o dest_Free o term_of) cv + val (u'_th,defs) = abstract (v::vs) cta val cu' = crhs_of u'_th - val abs_v_u = Thm.cabs cv cu' - (*get the formal parameters: bound variables also present in the term*) - val args = filter (valid_name vs) (term_frees (term_of abs_v_u)) - val crhs = list_cabs (map cterm args, abs_v_u) - (*Forms a lambda-abstraction over the formal parameters*) - val rhs = term_of crhs - val def = (*FIXME: can we also use the const-abstractions?*) - case List.find (fn ax => rhs aconv rhs_of ax andalso - Context.joinable (thy, theory_of_thm ax)) - (Net.match_term (!abstraction_cache) rhs) of - SOME ax => ax - | NONE => - let val Ts = map type_of args - val const_ty = Ts ---> (T --> typ_of (ctyp_of_term cu')) - val c = Free (gensym "abs_", const_ty) - val ax = assume (Thm.capply (cterm (equals const_ty $ c)) crhs) - val _ = abstraction_cache := Net.insert_term eq_absdef (rhs,ax) - (!abstraction_cache) - handle Net.INSERT => - raise THM ("assume_absfuns: INSERT", 0, [th,u'_th,ax]) - in ax end - val _ = assert (rhs aconv rhs_of def) "assume_absfuns: rhs mismatch" - val def_args = list_combination def (map cterm args) - in (transitive (abstract_rule v cv u'_th) (symmetric def_args), - def :: defs) end - | (t1$t2) => - let val (ct1,ct2) = Thm.dest_comb ct - val (t1',defs1) = abstract vs ct1 - val (t2',defs2) = abstract vs ct2 - in (combination t1' t2', defs1@defs2) end + val abs_v_u = Thm.cabs cv cu' + (*get the formal parameters: bound variables also present in the term*) + val args = filter (valid_name vs) (term_frees (term_of abs_v_u)) + val crhs = list_cabs (map cterm args, abs_v_u) + (*Forms a lambda-abstraction over the formal parameters*) + val rhs = term_of crhs + val def = (*FIXME: can we also use the const-abstractions?*) + case List.find (fn ax => rhs aconv rhs_of ax andalso + Context.joinable (thy, theory_of_thm ax)) + (Net.match_term (!abstraction_cache) rhs) of + SOME ax => ax + | NONE => + let val Ts = map type_of args + val const_ty = Ts ---> (T --> typ_of (ctyp_of_term cu')) + val c = Free (gensym "abs_", const_ty) + val ax = assume (Thm.capply (cterm (equals const_ty $ c)) crhs) + val _ = abstraction_cache := Net.insert_term eq_absdef (rhs,ax) + (!abstraction_cache) + handle Net.INSERT => + raise THM ("assume_absfuns: INSERT", 0, [th,u'_th,ax]) + in ax end + val _ = assert (rhs aconv rhs_of def) "assume_absfuns: rhs mismatch" + val def_args = list_combination def (map cterm args) + in (transitive (abstract_rule v cv u'_th) (symmetric def_args), + def :: defs) end + | (t1$t2) => + let val (ct1,ct2) = Thm.dest_comb ct + val (t1',defs1) = abstract vs ct1 + val (t2',defs2) = abstract vs ct2 + in (combination t1' t2', defs1@defs2) end val (eqth,defs) = abstract [] (cprop_of th) in equal_elim eqth th :: map (forall_intr_vars o strip_lambdas o object_eq) defs @@ -378,15 +381,15 @@ (*Given an abstraction over n variables, replace the bound variables by free ones. Return the body, along with the list of free variables.*) -fun c_variant_abs_multi (ct0, vars) = +fun c_variant_abs_multi (ct0, vars) = let val (cv,ct) = Thm.dest_abs NONE ct0 in c_variant_abs_multi (ct, cv::vars) end handle CTERM _ => (ct0, rev vars); -(*Given the definition of a Skolem function, return a theorem to replace - an existential formula by a use of that function. +(*Given the definition of a Skolem function, return a theorem to replace + an existential formula by a use of that function. Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *) -fun skolem_of_def def = +fun skolem_of_def def = let val (c,rhs) = Drule.dest_equals (cprop_of (#1 (Drule.freeze_thaw def))) val (ch, frees) = c_variant_abs_multi (rhs, []) val (chilbert,cabs) = Thm.dest_comb ch @@ -397,7 +400,7 @@ val ex_tm = c_mkTrueprop (Thm.capply cex cabs) and conc = c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees))); fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS someI_ex) 1 - in Goal.prove_raw [ex_tm] conc tacf + in Goal.prove_raw [ex_tm] conc tacf |> forall_intr_list frees |> forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*) |> Thm.varifyT @@ -405,13 +408,13 @@ (*Converts an Isabelle theorem (intro, elim or simp format) into nnf.*) (*It now works for HOL too. *) -fun to_nnf th = +fun to_nnf th = th |> transfer_to_Reconstruction |> transform_elim |> zero_var_indexes |> Drule.freeze_thaw |> #1 |> ObjectLogic.atomize_thm |> make_nnf; -(*The cache prevents repeated clausification of a theorem, - and also repeated declaration of Skolem functions*) +(*The cache prevents repeated clausification of a theorem, + and also repeated declaration of Skolem functions*) (* FIXME better use Termtab!? No, we MUST use theory data!!*) val clause_cache = ref (Symtab.empty : (thm * thm list) Symtab.table) @@ -424,7 +427,7 @@ fun assume_abstract th = if lambda_free (prop_of th) then [th] - else th |> eta_conversion_rule |> assume_absfuns + else th |> eta_conversion_rule |> assume_absfuns |> tap (fn ths => assert_lambda_free ths "assume_abstract: lambdas") (*Replace lambdas by assumed function definitions in the theorems*) @@ -435,13 +438,13 @@ (*Replace lambdas by declared function definitions in the theorems*) fun declare_abstract' (thy, []) = (thy, []) | declare_abstract' (thy, th::ths) = - let val (thy', th_defs) = + let val (thy', th_defs) = if lambda_free (prop_of th) then (thy, [th]) else - th |> zero_var_indexes |> Drule.freeze_thaw |> #1 - |> eta_conversion_rule |> transfer thy |> declare_absfuns - val _ = assert_lambda_free th_defs "declare_abstract: lambdas" - val (thy'', ths') = declare_abstract' (thy', ths) + th |> zero_var_indexes |> Drule.freeze_thaw |> #1 + |> eta_conversion_rule |> transfer thy |> declare_absfuns + val _ = assert_lambda_free th_defs "declare_abstract: lambdas" + val (thy'', ths') = declare_abstract' (thy', ths) in (thy'', th_defs @ ths') end; (*FIXME DELETE if we decide to switch to abstractions*) @@ -450,8 +453,8 @@ else (thy, map eta_conversion_rule ths); (*Skolemize a named theorem, with Skolem functions as additional premises.*) -(*also works for HOL*) -fun skolem_thm th = +(*also works for HOL*) +fun skolem_thm th = let val nnfth = to_nnf th in Meson.make_cnf (skolem_of_nnf nnfth) nnfth |> assume_abstract_list |> Meson.finish_cnf |> rm_redundant_cls @@ -463,53 +466,53 @@ fun skolem thy (name,th) = let val cname = (case name of "" => gensym "" | s => Sign.base_name s) val _ = Output.debug ("skolemizing " ^ name ^ ": ") - in Option.map - (fn nnfth => + in Option.map + (fn nnfth => let val (thy',defs) = declare_skofuns cname nnfth thy val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth val (thy'',cnfs') = declare_abstract (thy',cnfs) in (thy'', rm_redundant_cls (Meson.finish_cnf cnfs')) end) - (SOME (to_nnf th) handle THM _ => NONE) + (SOME (to_nnf th) handle THM _ => NONE) end; (*Populate the clause cache using the supplied theorem. Return the clausal form and modified theory.*) -fun skolem_cache_thm ((name,th), thy) = +fun skolem_cache_thm (name,th) thy = case Symtab.lookup (!clause_cache) name of - NONE => - (case skolem thy (name, Thm.transfer thy th) of - NONE => ([th],thy) - | SOME (thy',cls) => - (if null cls then warning ("skolem_cache: empty clause set for " ^ name) - else (); - change clause_cache (Symtab.update (name, (th, cls))); - (cls,thy'))) + NONE => + (case skolem thy (name, Thm.transfer thy th) of + NONE => ([th],thy) + | SOME (thy',cls) => + (if null cls then warning ("skolem_cache: empty clause set for " ^ name) + else (); + change clause_cache (Symtab.update (name, (th, map Drule.close_derivation cls))); + (cls,thy'))) | SOME (th',cls) => if eq_thm(th,th') then (cls,thy) - else (Output.debug ("skolem_cache: Ignoring variant of theorem " ^ name); - Output.debug (string_of_thm th); - Output.debug (string_of_thm th'); - ([th],thy)); - -(*Exported function to convert Isabelle theorems into axiom clauses*) + else (Output.debug ("skolem_cache: Ignoring variant of theorem " ^ name); + Output.debug (string_of_thm th); + Output.debug (string_of_thm th'); + ([th],thy)); + +(*Exported function to convert Isabelle theorems into axiom clauses*) fun cnf_axiom (name,th) = case name of - "" => skolem_thm th (*no name, so can't cache*) + "" => skolem_thm th (*no name, so can't cache*) | s => case Symtab.lookup (!clause_cache) s of - NONE => - let val cls = skolem_thm th - in change clause_cache (Symtab.update (s, (th, cls))); cls end - | SOME(th',cls) => - if eq_thm(th,th') then cls - else (Output.debug ("cnf_axiom: duplicate or variant of theorem " ^ name); - Output.debug (string_of_thm th); - Output.debug (string_of_thm th'); - cls); + NONE => + let val cls = skolem_thm th + in change clause_cache (Symtab.update (s, (th, cls))); cls end + | SOME(th',cls) => + if eq_thm(th,th') then cls + else (Output.debug ("cnf_axiom: duplicate or variant of theorem " ^ name); + Output.debug (string_of_thm th); + Output.debug (string_of_thm th'); + cls); fun pairname th = (Thm.name_of_thm th, th); -fun meta_cnf_axiom th = +fun meta_cnf_axiom th = map Meson.make_meta_clause (cnf_axiom (pairname th)); @@ -523,7 +526,7 @@ val intros = safeIs @ hazIs val elims = map Classical.classical_rule (safeEs @ hazEs) in - Output.debug ("rules_of_claset intros: " ^ Int.toString(length intros) ^ + Output.debug ("rules_of_claset intros: " ^ Int.toString(length intros) ^ " elims: " ^ Int.toString(length elims)); map pairname (intros @ elims) end; @@ -531,7 +534,7 @@ fun rules_of_simpset ss = let val ({rules,...}, _) = rep_ss ss val simps = Net.entries rules - in + in Output.debug ("rules_of_simpset: " ^ Int.toString(length simps)); map (fn r => (#name r, #thm r)) simps end; @@ -551,20 +554,20 @@ (* classical rules: works for both FOL and HOL *) fun cnf_rules [] err_list = ([],err_list) - | cnf_rules ((name,th) :: ths) err_list = + | cnf_rules ((name,th) :: ths) err_list = let val (ts,es) = cnf_rules ths err_list - in (cnf_axiom (name,th) :: ts,es) handle _ => (ts, (th::es)) end; + in (cnf_axiom (name,th) :: ts,es) handle _ => (ts, (th::es)) end; fun pair_name_cls k (n, []) = [] | pair_name_cls k (n, cls::clss) = (cls, (n,k)) :: pair_name_cls (k+1) (n, clss) - + fun cnf_rules_pairs_aux pairs [] = pairs | cnf_rules_pairs_aux pairs ((name,th)::ths) = let val pairs' = (pair_name_cls 0 (name, cnf_axiom(name,th))) @ pairs - handle THM _ => pairs | ResClause.CLAUSE _ => pairs - | ResHolClause.LAM2COMB _ => pairs + handle THM _ => pairs | ResClause.CLAUSE _ => pairs + | ResHolClause.LAM2COMB _ => pairs in cnf_rules_pairs_aux pairs' ths end; - + val cnf_rules_pairs = cnf_rules_pairs_aux []; @@ -572,16 +575,16 @@ (*Setup function: takes a theory and installs ALL known theorems into the clause cache*) -fun skolem_cache ((name,th), thy) = - let val prop = prop_of th +fun skolem_cache (name,th) thy = + let val prop = Thm.prop_of th in - if lambda_free prop orelse null (term_tvars prop) + if lambda_free prop orelse monomorphic prop then thy (*monomorphic theorems can be Skolemized on demand*) - else #2 (skolem_cache_thm ((name,th), thy)) + else #2 (skolem_cache_thm (name,th) thy) end; -fun clause_cache_setup thy = List.foldl skolem_cache thy (PureThy.all_thms_of thy); - +fun clause_cache_setup thy = fold skolem_cache (PureThy.all_thms_of thy) thy; + (*** meson proof methods ***) @@ -593,7 +596,7 @@ val meson_method_setup = Method.add_methods - [("meson", Method.thms_ctxt_args meson_meth, + [("meson", Method.thms_ctxt_args meson_meth, "MESON resolution proof procedure")]; @@ -608,7 +611,7 @@ fun skolem_attr (Context.Theory thy, th) = let val name = Thm.name_of_thm th - val (cls, thy') = skolem_cache_thm ((name, th), thy) + val (cls, thy') = skolem_cache_thm (name, th) thy in (Context.Theory thy', conj_rule cls) end | skolem_attr (context, th) = (context, conj_rule (skolem_thm th)); @@ -617,4 +620,4 @@ val setup = clause_cache_setup #> setup_attrs; -end; +end;