diff -r 91a91790899a -r 2cccd0e3e9ea TFL/post.sml --- a/TFL/post.sml Thu Jun 05 13:26:09 1997 +0200 +++ b/TFL/post.sml Thu Jun 05 13:27:28 1997 +0200 @@ -6,13 +6,6 @@ Postprocessing of TFL definitions *) -(*------------------------------------------------------------------------- -Three postprocessors are applied to the definition: - - a wellfoundedness prover (WF_TAC) - - a simplifier (tries to eliminate the language of termination expressions) - - a termination prover -*-------------------------------------------------------------------------*) - signature TFL = sig structure Prim : TFL_sig @@ -20,20 +13,17 @@ val tgoalw : theory -> thm list -> thm list -> thm list val tgoal: theory -> thm list -> thm list - val WF_TAC : thm list -> tactic - - val simplifier : thm -> thm - val std_postprocessor : theory + val std_postprocessor : simpset -> theory -> {induction:thm, rules:thm, TCs:term list list} -> {induction:thm, rules:thm, nested_tcs:thm list} val define_i : theory -> string -> term -> term list - -> theory * (thm * Prim.pattern list) + -> theory * Prim.pattern list val define : theory -> string -> string -> string list -> theory * Prim.pattern list - val simplify_defn : theory * (string * Prim.pattern list) + val simplify_defn : simpset -> theory * (string * Prim.pattern list) -> {rules:thm list, induct:thm, tcs:term list} (*------------------------------------------------------------------------- @@ -56,51 +46,38 @@ * have a tactic directly applied to them. *--------------------------------------------------------------------------*) fun termination_goals rules = - map (Logic.freeze_vars o HOLogic.dest_Trueprop) + map (#1 o Type.freeze_thaw o HOLogic.dest_Trueprop) (foldr (fn (th,A) => union_term (prems_of th, A)) (rules, [])); - (*--------------------------------------------------------------------------- - * Finds the termination conditions in (highly massaged) definition and - * puts them into a goalstack. - *--------------------------------------------------------------------------*) - fun tgoalw thy defs rules = - let val L = termination_goals rules - open USyntax - val g = cterm_of (sign_of thy) (HOLogic.mk_Trueprop(list_mk_conj L)) - in goalw_cterm defs g - end; +(*--------------------------------------------------------------------------- + * Finds the termination conditions in (highly massaged) definition and + * puts them into a goalstack. + *--------------------------------------------------------------------------*) +fun tgoalw thy defs rules = + let val L = termination_goals rules + open USyntax + val g = cterm_of (sign_of thy) (HOLogic.mk_Trueprop(list_mk_conj L)) + in goalw_cterm defs g + end; - fun tgoal thy = tgoalw thy []; - - (*--------------------------------------------------------------------------- - * Simple wellfoundedness prover. - *--------------------------------------------------------------------------*) - 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_trancl]; +fun tgoal thy = tgoalw thy []; - val terminator = simp_tac(!simpset addsimps [less_Suc_eq]) 1 - THEN TRY(best_tac - (!claset addSDs [not0_implies_Suc] - addss (!simpset)) 1); - - val simpls = [less_eq RS eq_reflection, - lex_prod_def, measure_def, inv_image_def]; +(*--------------------------------------------------------------------------- +* Three postprocessors are applied to the definition. It +* attempts to prove wellfoundedness of the given relation, simplifies the +* non-proved termination conditions, and finally attempts to prove the +* simplified termination conditions. +*--------------------------------------------------------------------------*) +fun std_postprocessor ss = + Prim.postprocess + {WFtac = REPEAT (ares_tac [wf_measure, wf_inv_image, wf_lex_prod, + wf_less_than, wf_trancl] 1), + terminator = asm_simp_tac ss 1 + THEN TRY(best_tac + (!claset addSDs [not0_implies_Suc] addss ss) 1), + simplifier = Rules.simpl_conv ss []}; - (*--------------------------------------------------------------------------- - * Does some standard things with the termination conditions of a definition: - * attempts to prove wellfoundedness of the given relation; simplifies the - * non-proven termination conditions; and finally attempts to prove the - * simplified termination conditions. - *--------------------------------------------------------------------------*) - val std_postprocessor = Prim.postprocess{WFtac = WFtac, - terminator = terminator, - simplifier = Rules.simpl_conv simpls}; - - val simplifier = rewrite_rule (simpls @ #simps(rep_ss (!simpset)) @ - [pred_list_def]); - - fun tflcongs thy = Prim.Context.read() @ (#case_congs(Thry.extract_info thy)); +fun tflcongs thy = Prim.Context.read() @ (#case_congs(Thry.extract_info thy)); val concl = #2 o Rules.dest_thm; @@ -111,17 +88,14 @@ 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 fid R functional - in (thry,(thm,pats)) + in (Prim.wfrec_definition0 thy fid R functional, pats) end; (*lcp's version: takes strings; doesn't return "thm" (whose signature is a draft and therefore useless) *) fun define thy fid R eqs = let fun read thy = readtm (sign_of thy) (TVar(("DUMMY",0),[])) - val (thy',(_,pats)) = - define_i thy fid (read thy R) (map (read thy) eqs) - in (thy',pats) end + in define_i thy fid (read thy R) (map (read thy) eqs) end handle Utils.ERR {mesg,...} => error mesg; (*--------------------------------------------------------------------------- @@ -147,8 +121,9 @@ Const("==",_)$_$_ => r | _$(Const("op =",_)$_$_) => r RS eq_reflection | _ => r RS P_imp_P_eq_True + +(*Is this the best way to invoke the simplifier??*) fun rewrite L = rewrite_rule (map mk_meta_eq (filter(not o id_thm) L)) -fun reducer thl = rewrite (map standard thl @ #simps(rep_ss (!simpset))) fun join_assums th = let val {sign,...} = rep_thm th @@ -164,17 +139,12 @@ end val gen_all = S.gen_all in -(*--------------------------------------------------------------------------- - * The "reducer" argument is - * (fn thl => rewrite (map standard thl @ #simps(rep_ss (!simpset)))); - *---------------------------------------------------------------------------*) -fun proof_stage theory reducer {f, R, rules, full_pats_TCs, TCs} = +fun proof_stage ss theory {f, R, rules, full_pats_TCs, TCs} = let val dummy = prs "Proving induction theorem.. " val ind = Prim.mk_induction theory f R full_pats_TCs - val dummy = writeln "Proved induction theorem." - val pp = std_postprocessor theory - val dummy = prs "Postprocessing.. " - val {rules,induction,nested_tcs} = pp{rules=rules,induction=ind,TCs=TCs} + val dummy = prs "Proved induction theorem.\nPostprocessing.. " + val {rules, induction, nested_tcs} = + std_postprocessor ss theory {rules=rules, induction=ind, TCs=TCs} in case nested_tcs of [] => (writeln "Postprocessing done."; @@ -186,8 +156,9 @@ if (solved th) then (th::So, Si, St) else (So, th::Si, St)) nested_tcs ([],[],[]) val simplified' = map join_assums simplified - val induction' = reducer (solved@simplified') induction - val rules' = reducer (solved@simplified') rules + val rewr = rewrite (solved @ simplified' @ #simps(rep_ss ss)) + val induction' = rewr induction + and rules' = rewr rules val dummy = writeln "Postprocessing done." in {induction = induction', @@ -212,18 +183,20 @@ (*Strip off the outer !P*) val spec'= read_instantiate [("x","P::?'b=>bool")] spec; +val wf_rel_defs = [lex_prod_def, measure_def, inv_image_def]; -fun simplify_defn (thy,(id,pats)) = +fun simplify_defn ss (thy,(id,pats)) = let val dummy = deny (id mem map ! (stamps_of_thy thy)) ("Recursive definition " ^ id ^ " would clash with the theory of the same name!") - val def = freezeT(get_def thy id RS meta_eq_to_obj_eq) + val def = freezeT(get_def thy id) RS meta_eq_to_obj_eq + val ss' = ss addsimps ((less_Suc_eq RS iffD2) :: wf_rel_defs) val {theory,rules,TCs,full_pats_TCs,patterns} = - Prim.post_definition (thy,(def,pats)) + Prim.post_definition ss' (thy,(def,pats)) val {lhs=f,rhs} = S.dest_eq(concl def) val (_,[R,_]) = S.strip_comb rhs val {induction, rules, tcs} = - proof_stage theory reducer + proof_stage ss' theory {f = f, R = R, rules = rules, full_pats_TCs = full_pats_TCs, TCs = TCs} @@ -235,8 +208,7 @@ end handle Utils.ERR {mesg,func,module} => error (mesg ^ - "\n (In TFL function " ^ module ^ "." ^ func ^ ")") - | e => print_exn e; + "\n (In TFL function " ^ module ^ "." ^ func ^ ")"); end; (*--------------------------------------------------------------------------- @@ -260,7 +232,6 @@ in {theory = theory, eq_ind = standard (induction RS (rules RS conjI))} end - handle e => print_exn e end;