# HG changeset patch # User paulson # Date 1192196742 -7200 # Node ID cd497f6fe8d1a77b7a58efecb576d70104557bf0 # Parent fcf5a999d1c3f9fcf15b54d732dce3212ba12be5 trying to make it run faster diff -r fcf5a999d1c3 -r cd497f6fe8d1 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Fri Oct 12 15:45:13 2007 +0200 +++ b/src/HOL/Tools/res_axioms.ML Fri Oct 12 15:45:42 2007 +0200 @@ -10,7 +10,6 @@ val cnf_axiom: thm -> thm list val pairname: thm -> string * thm val multi_base_blacklist: string list - val skolem_thm: thm -> thm list val cnf_rules_pairs: (string * thm) list -> (thm * (string * int)) list val cnf_rules_of_ths: thm list -> thm list val neg_clausify: thm list -> thm list @@ -154,12 +153,6 @@ strip_lambdas (n-1) (freeze_thm (th RS xfun_cong x)) | _ => th; -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; - val lambda_free = not o Term.has_abs; val monomorphic = not o Term.exists_type (Term.exists_subtype Term.is_TVar); @@ -224,8 +217,7 @@ else case term_of ct of Abs _ => - let val _ = assert_eta_free ct; - val (cv,cta) = Thm.dest_abs NONE ct + let val (cv,cta) = Thm.dest_abs NONE ct val (v,Tv) = (dest_Free o term_of) cv val _ = Output.debug (fn()=>" recursion: " ^ string_of_cterm cta); val u_th = combinators_aux cta @@ -307,6 +299,30 @@ [] => () | ths' => error (msg ^ "\n" ^ cat_lines (map string_of_thm ths')); + +(*** Blacklisting (duplicated in ResAtp? ***) + +val max_lambda_nesting = 3; + +fun excessive_lambdas (f$t, k) = excessive_lambdas (f,k) orelse excessive_lambdas (t,k) + | excessive_lambdas (Abs(_,_,t), k) = k=0 orelse excessive_lambdas (t,k-1) + | excessive_lambdas _ = false; + +fun is_formula_type T = (T = HOLogic.boolT orelse T = propT); + +(*Don't count nested lambdas at the level of formulas, as they are quantifiers*) +fun excessive_lambdas_fm Ts (Abs(_,T,t)) = excessive_lambdas_fm (T::Ts) t + | excessive_lambdas_fm Ts t = + if is_formula_type (fastype_of1 (Ts, t)) + then exists (excessive_lambdas_fm Ts) (#2 (strip_comb t)) + else excessive_lambdas (t, max_lambda_nesting); + +fun too_complex t = + Meson.too_many_clauses t orelse excessive_lambdas_fm [] t; + +val multi_base_blacklist = + ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm"]; + (*Keep the full complexity of the original name*) fun flatten_name s = space_implode "_X" (NameSpace.explode s); @@ -318,14 +334,6 @@ if PureThy.has_name_hint th then PureThy.get_name_hint th else string_of_thm th; -(*Skolemize a named theorem, with Skolem functions as additional premises.*) -fun skolem_thm th = - let val ctxt0 = Variable.thm_context th - val (nnfth,ctxt1) = to_nnf th ctxt0 and s = fake_name th - val (cnfs,ctxt2) = Meson.make_cnf (assume_skolem_of_def s nnfth) nnfth ctxt1 - in cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |> Meson.finish_cnf end - handle THM _ => []; - (*Declare Skolem functions for a theorem, supplied in nnf and with its name. It returns a modified theory, unless skolemization fails.*) fun skolem thy th = @@ -371,13 +379,24 @@ (cls, ThmCache.map (Thmtab.update (th,cls)) thy'))) | SOME cls => (cls,thy); +(*Skolemize a named theorem, with Skolem functions as additional premises.*) +fun skolem_thm (s,th) = + if (Sign.base_name s) mem_string multi_base_blacklist orelse + PureThy.is_internal th orelse too_complex (prop_of th) then [] + else + let val ctxt0 = Variable.thm_context th + val (nnfth,ctxt1) = to_nnf th ctxt0 + val (cnfs,ctxt2) = Meson.make_cnf (assume_skolem_of_def s nnfth) nnfth ctxt1 + in cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |> Meson.finish_cnf end + handle THM _ => []; + (*Exported function to convert Isabelle theorems into axiom clauses*) fun cnf_axiom th = let val thy = Theory.merge (Theory.deref atp_linkup_thy_ref, Thm.theory_of_thm th) in case Thmtab.lookup (ThmCache.get thy) th of NONE => (Output.debug (fn () => "cnf_axiom: " ^ name_or_string th); - map Goal.close_result (skolem_thm th)) + map Goal.close_result (skolem_thm (fake_name th, th))) | SOME cls => cls end; @@ -411,12 +430,6 @@ (**** Translate a set of theorems into CNF ****) -(* classical rules: works for both FOL and HOL *) -fun cnf_rules [] err_list = ([],err_list) - | cnf_rules ((name,th) :: ths) err_list = - let val (ts,es) = cnf_rules ths err_list - in (cnf_axiom 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) @@ -436,27 +449,6 @@ val mark_skolemized = Sign.add_consts_i [("ResAxioms_endtheory", HOLogic.boolT, NoSyn)]; -val max_lambda_nesting = 3; - -fun excessive_lambdas (f$t, k) = excessive_lambdas (f,k) orelse excessive_lambdas (t,k) - | excessive_lambdas (Abs(_,_,t), k) = k=0 orelse excessive_lambdas (t,k-1) - | excessive_lambdas _ = false; - -fun is_formula_type T = (T = HOLogic.boolT orelse T = propT); - -(*Don't count nested lambdas at the level of formulas, as they are quantifiers*) -fun excessive_lambdas_fm Ts (Abs(_,T,t)) = excessive_lambdas_fm (T::Ts) t - | excessive_lambdas_fm Ts t = - if is_formula_type (fastype_of1 (Ts, t)) - then exists (excessive_lambdas_fm Ts) (#2 (strip_comb t)) - else excessive_lambdas (t, max_lambda_nesting); - -fun too_complex t = - Meson.too_many_clauses t orelse excessive_lambdas_fm [] t; - -val multi_base_blacklist = - ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm"]; - fun skolem_cache th thy = if PureThy.is_internal th orelse too_complex (prop_of th) then thy else #2 (skolem_cache_thm th thy);