# HG changeset patch # User paulson # Date 864642510 -7200 # Node ID c81c7f8ad333e56730f80ef4794df3db29beb2ba # Parent ab7161e593c87eb60db858dfd885cb1bd3bc42a8 Now checks the name of the function being defined diff -r ab7161e593c8 -r c81c7f8ad333 TFL/post.sml --- a/TFL/post.sml Mon May 26 12:27:58 1997 +0200 +++ b/TFL/post.sml Mon May 26 12:28:30 1997 +0200 @@ -27,8 +27,11 @@ -> {induction:thm, rules:thm, TCs:term list list} -> {induction:thm, rules:thm, nested_tcs:thm list} - val define_i : theory -> term -> term -> theory * (thm * Prim.pattern list) - val define : theory -> string -> string list -> theory * Prim.pattern list + val define_i : theory -> string -> term -> term + -> theory * (thm * Prim.pattern list) + + val define : theory -> string -> string -> string list + -> theory * Prim.pattern list val simplify_defn : theory * (string * Prim.pattern list) -> {rules:thm list, induct:thm, tcs:term list} @@ -74,9 +77,9 @@ *--------------------------------------------------------------------------*) fun WF_TAC thms = REPEAT(FIRST1(map rtac thms)) val WFtac = WF_TAC[wf_measure, wf_inv_image, wf_lex_prod, wf_less_than, - wf_pred_list, wf_trancl]; + wf_trancl]; - val terminator = simp_tac(!simpset addsimps [less_Suc_eq, pred_list_def]) 1 + val terminator = simp_tac(!simpset addsimps [less_Suc_eq]) 1 THEN TRY(best_tac (!claset addSDs [not0_implies_Suc] addss (!simpset)) 1); @@ -105,20 +108,19 @@ (*--------------------------------------------------------------------------- * Defining a function with an associated termination relation. *---------------------------------------------------------------------------*) -fun define_i thy R eqs = - let val dummy = require_thy thy "WF_Rel" "recursive function definitions"; - +fun define_i thy fid R eqs = + let val dummy = require_thy thy "WF_Rel" "recursive function definitions" val {functional,pats} = Prim.mk_functional thy eqs - val (thm,thry) = Prim.wfrec_definition0 thy R functional + val (thm,thry) = Prim.wfrec_definition0 thy fid R functional in (thry,(thm,pats)) end; (*lcp's version: takes strings; doesn't return "thm" (whose signature is a draft and therefore useless) *) -fun define thy R eqs = +fun define thy fid R eqs = let fun read thy = readtm (sign_of thy) (TVar(("DUMMY",0),[])) val (thy',(_,pats)) = - define_i thy (read thy R) + define_i thy fid (read thy R) (fold_bal (app Ind_Syntax.conj) (map (read thy) eqs)) in (thy',pats) end handle Utils.ERR {mesg,...} => error mesg;