# HG changeset patch # User wenzelm # Date 1185648019 -7200 # Node ID 363287741ebe23ed843d4c77e6efd09afda0bd6b # Parent cf022cc710aeb5b99932b03fd12fe94a1eba79b4 simproc_setup fun_upd2; diff -r cf022cc710ae -r 363287741ebe src/HOL/Fun.thy --- a/src/HOL/Fun.thy Sat Jul 28 20:40:18 2007 +0200 +++ b/src/HOL/Fun.thy Sat Jul 28 20:40:19 2007 +0200 @@ -465,10 +465,10 @@ text {* simplifies terms of the form f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *} -ML {* +simproc_setup fun_upd2 ("f(v := w, x := y)") = {* fn _ => let fun gen_fun_upd NONE T _ _ = NONE - | gen_fun_upd (SOME f) T x y = SOME (Const (@{const_name fun_upd},T) $ f $ x $ y) + | gen_fun_upd (SOME f) T x y = SOME (Const (@{const_name fun_upd}, T) $ f $ x $ y) fun dest_fun_T1 (Type (_, T :: Ts)) = T fun find_double (t as Const (@{const_name fun_upd},T) $ f $ x $ y) = let @@ -476,20 +476,22 @@ if v aconv x then SOME g else gen_fun_upd (find g) T v w | find t = NONE in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end - fun fun_upd_prover ss = - rtac eq_reflection 1 THEN rtac ext 1 THEN - simp_tac (Simplifier.inherit_context ss @{simpset}) 1 - val fun_upd2_simproc = - Simplifier.simproc @{theory} - "fun_upd2" ["f(v := w, x := y)"] - (fn _ => fn ss => fn t => - case find_double t of (T, NONE) => NONE - | (T, SOME rhs) => - SOME (Goal.prove (Simplifier.the_context ss) [] [] - (Term.equals T $ t $ rhs) (K (fun_upd_prover ss)))) -in - Addsimprocs [fun_upd2_simproc] -end; + + fun proc ss ct = + let + val ctxt = Simplifier.the_context ss + val t = Thm.term_of ct + in + case find_double t of + (T, NONE) => NONE + | (T, SOME rhs) => + SOME (Goal.prove ctxt [] [] (Term.equals T $ t $ rhs) + (fn _ => + rtac eq_reflection 1 THEN + rtac ext 1 THEN + simp_tac (Simplifier.inherit_context ss @{simpset}) 1)) + end +in proc end *}