# HG changeset patch # User wenzelm # Date 898781610 -7200 # Node ID e03460289797bbc8624618b2bc23910274a1f2c4 # Parent 7274f7d101ee5f04a2df3694fb655eaef4352340 added XX_YY_rewrite: simpset -> cterm -> thm; diff -r 7274f7d101ee -r e03460289797 src/Provers/simplifier.ML --- a/src/Provers/simplifier.ML Thu Jun 25 15:32:41 1998 +0200 +++ b/src/Provers/simplifier.ML Thu Jun 25 15:33:30 1998 +0200 @@ -78,6 +78,10 @@ signature SIMPLIFIER = sig include BASIC_SIMPLIFIER + val rewrite: simpset -> cterm -> thm + val asm_rewrite: simpset -> cterm -> thm + val full_rewrite: simpset -> cterm -> thm + val asm_full_rewrite: simpset -> cterm -> thm val setup: (theory -> theory) list val get_local_simpset: local_theory -> simpset val put_local_simpset: simpset -> local_theory -> local_theory @@ -404,20 +408,26 @@ -(** simplification meta rules **) +(** simplification rules and conversions **) -fun simp mode (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac}) thm = +fun simp rew mode (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac}) thm = let val tacf = solve_all_tac (subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac); fun prover m th = apsome fst (Seq.pull (tacf m th)); - in - Drule.rewrite_thm mode prover mss thm - end; + in rew mode prover mss thm end; + +val simp_thm = simp Drule.rewrite_thm; +val simp_cterm = simp Drule.rewrite_cterm; -val simplify = simp (false, false, false); -val asm_simplify = simp (false, true, false); -val full_simplify = simp (true, false, false); -val asm_full_simplify = simp (true, true, false); +val simplify = simp_thm (false, false, false); +val asm_simplify = simp_thm (false, true, false); +val full_simplify = simp_thm (true, false, false); +val asm_full_simplify = simp_thm (true, true, false); + +val rewrite = simp_cterm (false, false, false); +val asm_rewrite = simp_cterm (false, true, false); +val full_rewrite = simp_cterm (true, false, false); +val asm_full_rewrite = simp_cterm (true, true, false);