374 |
374 |
375 (*Rewrite subgoal i only *) |
375 (*Rewrite subgoal i only *) |
376 fun asm_rewrite_goal_tac prover_tac mss i = |
376 fun asm_rewrite_goal_tac prover_tac mss i = |
377 PRIMITIVE(rewrite_goal_rule (result1 prover_tac) mss i); |
377 PRIMITIVE(rewrite_goal_rule (result1 prover_tac) mss i); |
378 |
378 |
379 (*Rewrite or fold throughout proof state. *) |
379 (*Rewrite throughout proof state. *) |
380 fun rewrite_tac thms = PRIMITIVE(rewrite_rule thms); |
380 fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs); |
381 fun fold_tac rths = rewrite_tac (map symmetric rths); |
|
382 |
381 |
383 (*Rewrite subgoals only, not main goal. *) |
382 (*Rewrite subgoals only, not main goal. *) |
384 fun rewrite_goals_tac thms = PRIMITIVE (rewrite_goals_rule thms); |
383 fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs); |
385 fun fold_goals_tac rths = rewrite_goals_tac (map symmetric rths); |
384 |
386 |
385 fun rewtac def = rewrite_goals_tac [def]; |
387 fun rewtac rth = rewrite_goals_tac [rth]; |
386 |
388 |
387 |
389 |
388 (*** Tactic for folding definitions, handling critical pairs ***) |
390 (** Renaming of parameters in a subgoal |
389 |
391 Names may contain letters, digits or primes and must be |
390 (*The depth of nesting in a term*) |
392 separated by blanks **) |
391 fun term_depth (Abs(a,T,t)) = 1 + term_depth t |
|
392 | term_depth (f$t) = 1 + max [term_depth f, term_depth t] |
|
393 | term_depth _ = 0; |
|
394 |
|
395 val lhs_of_thm = #1 o Logic.dest_equals o #prop o rep_thm; |
|
396 |
|
397 (*folding should handle critical pairs! E.g. K == Inl(0), S == Inr(Inl(0)) |
|
398 Returns longest lhs first to avoid folding its subexpressions.*) |
|
399 fun sort_lhs_depths defs = |
|
400 let val keylist = make_keylist (term_depth o lhs_of_thm) defs |
|
401 val keys = distinct (sort op> (map #2 keylist)) |
|
402 in map (keyfilter keylist) keys end; |
|
403 |
|
404 fun fold_tac defs = EVERY |
|
405 (map rewrite_tac (sort_lhs_depths (map symmetric defs))); |
|
406 |
|
407 fun fold_goals_tac defs = EVERY |
|
408 (map rewrite_goals_tac (sort_lhs_depths (map symmetric defs))); |
|
409 |
|
410 |
|
411 (*** Renaming of parameters in a subgoal |
|
412 Names may contain letters, digits or primes and must be |
|
413 separated by blanks ***) |
393 |
414 |
394 (*Calling this will generate the warning "Same as previous level" since |
415 (*Calling this will generate the warning "Same as previous level" since |
395 it affects nothing but the names of bound variables!*) |
416 it affects nothing but the names of bound variables!*) |
396 fun rename_tac str i = |
417 fun rename_tac str i = |
397 let val cs = explode str |
418 let val cs = explode str |