--- a/TFL/post.ML Thu Oct 16 12:13:43 2003 +0200
+++ b/TFL/post.ML Fri Oct 17 11:03:48 2003 +0200
@@ -138,9 +138,16 @@
if (solved th) then (th::So, Si, St)
else (So, th::Si, St)) nested_tcs ([],[],[])
val simplified' = map join_assums simplified
+ val dummy = (Prim.trace_thms "solved =" solved;
+ Prim.trace_thms "simplified' =" simplified')
val rewr = full_simplify (ss addsimps (solved @ simplified'));
+ val dummy = Prim.trace_thms "Simplifying the induction rule..."
+ [induction]
val induction' = rewr induction
- and rules' = rewr rules
+ val dummy = Prim.trace_thms "Simplifying the recursion rules..."
+ [rules]
+ val rules' = rewr rules
+ val _ = message "... Postprocessing finished";
in
{induction = induction',
rules = rules',
@@ -162,18 +169,25 @@
(*Strip off the outer !P*)
val spec'= read_instantiate [("x","P::?'b=>bool")] spec;
+fun tracing true _ = ()
+ | tracing false msg = writeln msg;
+
fun simplify_defn strict thy cs ss congs wfs id pats def0 =
let val def = freezeT def0 RS meta_eq_to_obj_eq
- val {theory,rules,rows,TCs,full_pats_TCs} = Prim.post_definition congs (thy, (def,pats))
+ val {theory,rules,rows,TCs,full_pats_TCs} =
+ Prim.post_definition congs (thy, (def,pats))
val {lhs=f,rhs} = S.dest_eq (concl def)
val (_,[R,_]) = S.strip_comb rhs
+ val dummy = Prim.trace_thms "congs =" congs
+ (*the next step has caused simplifier looping in some cases*)
val {induction, rules, tcs} =
proof_stage strict cs ss wfs theory
{f = f, R = R, rules = rules,
full_pats_TCs = full_pats_TCs,
TCs = TCs}
- val rules' = map (standard o ObjectLogic.rulify_no_asm) (R.CONJUNCTS rules)
- in {induct = meta_outer (ObjectLogic.rulify_no_asm (induction RS spec')),
+ val rules' = map (standard o ObjectLogic.rulify_no_asm)
+ (R.CONJUNCTS rules)
+ in {induct = meta_outer (ObjectLogic.rulify_no_asm (induction RS spec')),
rules = ListPair.zip(rules', rows),
tcs = (termination_goals rules') @ tcs}
end
--- a/TFL/tfl.ML Thu Oct 16 12:13:43 2003 +0200
+++ b/TFL/tfl.ML Fri Oct 17 11:03:48 2003 +0200
@@ -9,6 +9,8 @@
signature PRIM =
sig
val trace: bool ref
+ val trace_thms: string -> thm list -> unit
+ val trace_cterms: string -> cterm list -> unit
type pattern
val mk_functional: theory -> term list -> {functional: term, pats: pattern list}
val wfrec_definition0: theory -> string -> term -> term -> theory * thm
@@ -914,6 +916,15 @@
(R.MP rule tcthm, R.PROVE_HYP tcthm induction)
+fun trace_thms s L =
+ if !trace then writeln (cat_lines (s :: map string_of_thm L))
+ else ();
+
+fun trace_cterms s L =
+ if !trace then writeln (cat_lines (s :: map string_of_cterm L))
+ else ();;
+
+
fun postprocess strict {wf_tac, terminator, simplifier} theory {rules,induction,TCs} =
let val tych = Thry.typecheck theory
val prove = R.prove strict;
@@ -937,19 +948,11 @@
* 3. replace tc by tc' in both the rules and the induction theorem.
*---------------------------------------------------------------------*)
- fun print_thms s L =
- if !trace then writeln (cat_lines (s :: map string_of_thm L))
- else ();
-
- fun print_cterms s L =
- if !trace then writeln (cat_lines (s :: map string_of_cterm L))
- else ();;
-
fun simplify_tc tc (r,ind) =
let val tc1 = tych tc
- val _ = print_cterms "TC before simplification: " [tc1]
+ val _ = trace_cterms "TC before simplification: " [tc1]
val tc_eq = simplifier tc1
- val _ = print_thms "result: " [tc_eq]
+ val _ = trace_thms "result: " [tc_eq]
in
elim_tc (R.MATCH_MP Thms.eqT tc_eq) (r,ind)
handle U.ERR _ =>