# HG changeset patch # User paulson # Date 1156524538 -7200 # Node ID df257a9cf0e9d25c94961ebd22f3f0e52a595b50 # Parent 7c1aa787226618df3512fedcfcff11276437c59f abstraction of lambda-expressions diff -r 7c1aa7872266 -r df257a9cf0e9 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Fri Aug 25 18:48:09 2006 +0200 +++ b/src/HOL/Tools/res_atp.ML Fri Aug 25 18:48:58 2006 +0200 @@ -63,7 +63,7 @@ (*** background linkup ***) val call_atp = ref false; val hook_count = ref 0; -val time_limit = ref 30; +val time_limit = ref 80; val prover = ref "E"; (* use E as the default prover *) val custom_spass = (*specialized options for SPASS*) ref ["-Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub"]; @@ -735,7 +735,7 @@ let val st = Seq.hd (EVERY' [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac] n th) val negs = Option.valOf (metahyps_thms n st) - val negs_clauses = make_clauses negs + val negs_clauses = ResAxioms.assume_abstract (make_clauses negs) in negs_clauses :: get_neg_subgoals (n-1) end @@ -809,7 +809,7 @@ Pretty.string_of (ProofContext.pretty_term ctxt (Logic.mk_conjunction_list (Thm.prems_of goal)))); Output.debug ("current theory: " ^ Context.theory_name thy); - hook_count := !hook_count +1; + inc hook_count; Output.debug ("in hook for time: " ^ Int.toString (!hook_count)); ResClause.init thy; ResHolClause.init thy; diff -r 7c1aa7872266 -r df257a9cf0e9 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Fri Aug 25 18:48:09 2006 +0200 +++ b/src/HOL/Tools/res_axioms.ML Fri Aug 25 18:48:58 2006 +0200 @@ -18,6 +18,7 @@ val simpset_rules_of_ctxt : Proof.context -> (string * thm) list val pairname : thm -> (string * thm) val skolem_thm : thm -> thm list + val to_nnf : thm -> thm val cnf_rules_pairs : (string * Thm.thm) list -> (Thm.thm * (string * int)) list list; val meson_method_setup : theory -> theory val setup : theory -> theory @@ -25,17 +26,22 @@ val atpset_rules_of_thy : theory -> (string * thm) list val atpset_rules_of_ctxt : Proof.context -> (string * thm) list end; - -structure ResAxioms : RES_AXIOMS = + +structure ResAxioms = struct +(*FIXME DELETE: For running the comparison between combinators and abstractions. + CANNOT be a ref, as the setting is used while Isabelle is built.*) +val abstract_lambdas = true; + +val trace_abs = ref false; (**** Transformation of Elimination Rules into First-Order Formulas****) (* a tactic used to prove an elim-rule. *) fun elimRule_tac th = - (resolve_tac [impI,notI] 1) THEN (etac th 1) THEN REPEAT(blast_tac HOL_cs 1); + (resolve_tac [impI,notI] 1) THEN (etac th 1) THEN REPEAT(fast_tac HOL_cs 1); fun add_EX tm [] = tm | add_EX tm ((x,xtp)::xs) = add_EX (HOLogic.exists_const xtp $ Abs(x,xtp,tm)) xs; @@ -97,10 +103,8 @@ " for theorem " ^ string_of_thm th); th) - (**** Transformation of Clasets and Simpsets into First-Order Axioms ****) - (*Transfer a theorem into theory Reconstruction.thy if it is not already inside that theory -- because it's needed for Skolemization *) @@ -126,43 +130,41 @@ (*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))) (n, (thy, axs)) = + 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 = s ^ "_" ^ Int.toString n + 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 def = equals cT $ c $ rhs 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, def)] thy' + val thy'' = Theory.add_defs_i false false [(cdef, equals cT $ c $ rhs)] thy' in dec_sko (subst_bound (list_comb(c,args), p)) - (n+1, (thy'', get_axiom thy'' cdef :: axs)) + (thy'', get_axiom thy'' cdef :: axs) end - | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) (n, thx) = + | 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)) (n, thx) end - | dec_sko (Const ("op &", _) $ p $ q) nthy = dec_sko q (dec_sko p nthy) - | dec_sko (Const ("op |", _) $ p $ q) nthy = dec_sko q (dec_sko p nthy) - | dec_sko (Const ("Trueprop", _) $ p) nthy = dec_sko p nthy - | dec_sko t nthx = nthx (*Do nothing otherwise*) - in #2 (dec_sko (#prop (rep_thm th)) (1, (thy,[]))) end; + 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 name = Name.variant (add_term_names (p,[])) (gensym "sko_") - val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*) + 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 (name, cT) + 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*) @@ -178,7 +180,145 @@ | 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 (rep_thm th)) [] end; + in dec_sko (prop_of th) [] end; + + +(**** REPLACING ABSTRACTIONS BY FUNCTION DEFINITIONS ****) + +(*Returns the vars of a theorem*) +fun vars_of_thm th = + map (Thm.cterm_of (Thm.theory_of_thm th) o Var) (Drule.fold_terms Term.add_vars th []); + +(*Make a version of fun_cong with a given variable name*) +local + val fun_cong' = fun_cong RS asm_rl; (*renumber f, g to prevent clashes with (a,0)*) + val cx = hd (vars_of_thm fun_cong'); + val ty = typ_of (ctyp_of_term cx); + val thy = Thm.theory_of_thm fun_cong; + fun mkvar a = cterm_of thy (Var((a,0),ty)); +in +fun xfun_cong x = Thm.instantiate ([], [(cx, mkvar x)]) fun_cong' +end; + +(*Removes the lambdas from an equation of the form t = (%x. u)*) +fun strip_lambdas th = + case prop_of th of + _ $ (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, + where some types have the empty sort.*) +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 th = + case Drule.strip_comb (cprop_of th) of + (f, [_, rhs]) => + (case term_of f of + Const ("==", _) => rhs + | _ => raise THM ("crhs", 0, [th])) + | _ => raise THM ("crhs", 1, [th]); + +(*Apply a function definition to an argument, beta-reducing the result.*) +fun beta_comb cf x = + let val th1 = combination cf (reflexive x) + val th2 = beta_conversion false (crhs th1) + in transitive th1 th2 end; + +(*Apply a function definition to arguments, beta-reducing along the way.*) +fun list_combination cf [] = cf + | list_combination cf (x::xs) = list_combination (beta_comb cf x) xs; + +fun list_cabs ([] , t) = t + | list_cabs (v::vars, t) = Thm.cabs v (list_cabs(vars,t)); + +(*FIXME DELETE*) +fun check_eta 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; + +(*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 = case term_of ct of + Abs (_,T,u) => + let val cname = gensym "abs_" + val _ = check_eta 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 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 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 def*) + val rhs = list_abs_free (map dest_Free args, abs_v_u) + (*Forms a lambda-abstraction over the formal parameters*) + val cdef = cname ^ "_def" + val thy = Theory.add_defs_i false false [(cdef, equals cT $ c $ rhs)] thy + val def = #1 (Drule.freeze_thaw (get_axiom thy cdef)) + 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 + | _ => (transfer thy (reflexive ct), []) + 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 :: + map (forall_intr_vars o strip_lambdas o object_eq) defs + in (theory_of_thm eqth, ths) end; + +fun assume_absfuns th = + let val cterm = cterm_of (Thm.theory_of_thm th) + fun abstract vs ct = case term_of ct of + Abs (_,T,u) => + let val (cv,cta) = Thm.dest_abs NONE ct + val _ = check_eta ct; + val v = (#1 o dest_Free o term_of) cv + val (u'_th,defs) = abstract (v::vs) cta + val cu' = crhs 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 Ts = map type_of args + val const_ty = Ts ---> (T --> typ_of (ctyp_of_term cu')) + val c = Free (gensym "abs_", const_ty) + val rhs = list_cabs (map cterm args, abs_v_u) + (*Forms a lambda-abstraction over the formal parameters*) + val def = assume (Thm.capply (cterm (equals const_ty $ c)) rhs) + 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 + | _ => (reflexive ct, []) + val (eqth,defs) = abstract [] (cprop_of th) + in equal_elim eqth th :: + map (forall_intr_vars o strip_lambdas o object_eq) defs + end; + (*cterms are used throughout for efficiency*) val cTrueprop = Thm.cterm_of HOL.thy HOLogic.Trueprop; @@ -217,7 +357,7 @@ (*It now works for HOL too. *) fun to_nnf th = th |> transfer_to_Reconstruction - |> transform_elim |> Drule.freeze_thaw |> #1 + |> transform_elim |> zero_var_indexes |> Drule.freeze_thaw |> #1 |> ObjectLogic.atomize_thm |> make_nnf; (*The cache prevents repeated clausification of a theorem, @@ -230,23 +370,46 @@ fun skolem_of_nnf th = map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns th); +(*Replace lambdas by assumed function definitions in the theorems*) +fun assume_abstract ths = + if abstract_lambdas then List.concat (map (assume_absfuns o eta_conversion_rule) ths) + else map eta_conversion_rule ths; + +(*Replace lambdas by declared function definitions in the theorems*) +fun declare_abstract' (thy, []) = (thy, []) + | declare_abstract' (thy, th::ths) = + let val (thy', th_defs) = + th |> zero_var_indexes |> Drule.freeze_thaw |> #1 + |> eta_conversion_rule |> transfer thy |> declare_absfuns + val (thy'', ths') = declare_abstract' (thy', ths) + in (thy'', th_defs @ ths') end; + +(*FIXME DELETE*) +fun declare_abstract (thy, ths) = + if abstract_lambdas then declare_abstract' (thy, ths) + 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 = let val nnfth = to_nnf th - in rm_redundant_cls (Meson.make_cnf (skolem_of_nnf nnfth) nnfth) + in Meson.make_cnf (skolem_of_nnf nnfth) nnfth + |> assume_abstract |> Meson.finish_cnf |> rm_redundant_cls 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 (name,th) = - let val cname = (case name of "" => gensym "sko_" | s => Sign.base_name s) + let val cname = (case name of "" => gensym "" | s => Sign.base_name s) + val _ = Output.debug ("skolemizing " ^ name ^ ": ") in Option.map (fn nnfth => let val (thy',defs) = declare_skofuns cname nnfth thy - val skoths = map skolem_of_def defs - in (thy', rm_redundant_cls (Meson.make_cnf skoths nnfth)) end) + 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) end; @@ -347,14 +510,8 @@ (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****) -(*Setup function: takes a theory and installs ALL simprules and claset rules - into the clause cache*) -fun clause_cache_setup thy = - let val simps = simpset_rules_of_thy thy - and clas = claset_rules_of_thy thy - val thy1 = List.foldl skolem_cache thy clas - in List.foldl skolem_cache thy1 simps end; -(*Could be duplicate theorem names, due to multiple attributes*) +(*Setup function: takes a theory and installs ALL known theorems into the clause cache*) +fun clause_cache_setup thy = List.foldl skolem_cache thy (PureThy.all_thms_of thy); (*** meson proof methods ***) @@ -379,15 +536,14 @@ (*Conjoin a list of clauses to recreate a single theorem*) val conj_rule = foldr1 conj2_rule; -fun skolem (Context.Theory thy, th) = - let - val name = Thm.name_of_thm th - val (cls, thy') = skolem_cache_thm ((name, th), thy) +fun skolem_attr (Context.Theory thy, th) = + let val name = Thm.name_of_thm th + val (cls, thy') = skolem_cache_thm ((name, th), thy) in (Context.Theory thy', conj_rule cls) end - | skolem (context, th) = (context, conj_rule (skolem_thm th)); + | skolem_attr (context, th) = (context, conj_rule (skolem_thm th)); val setup_attrs = Attrib.add_attributes - [("skolem", Attrib.no_args skolem, "skolemization of a theorem")]; + [("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem")]; val setup = clause_cache_setup #> setup_attrs;