simproc_setup fun_upd2;
authorwenzelm
Sat Jul 28 20:40:19 2007 +0200 (2007-07-28)
changeset 24017363287741ebe
parent 24016 cf022cc710ae
child 24018 edd20fe274b5
simproc_setup fun_upd2;
src/HOL/Fun.thy
     1.1 --- a/src/HOL/Fun.thy	Sat Jul 28 20:40:18 2007 +0200
     1.2 +++ b/src/HOL/Fun.thy	Sat Jul 28 20:40:19 2007 +0200
     1.3 @@ -465,10 +465,10 @@
     1.4  text {* simplifies terms of the form
     1.5    f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *}
     1.6  
     1.7 -ML {*
     1.8 +simproc_setup fun_upd2 ("f(v := w, x := y)") = {* fn _ =>
     1.9  let
    1.10    fun gen_fun_upd NONE T _ _ = NONE
    1.11 -    | gen_fun_upd (SOME f) T x y = SOME (Const (@{const_name fun_upd},T) $ f $ x $ y)
    1.12 +    | gen_fun_upd (SOME f) T x y = SOME (Const (@{const_name fun_upd}, T) $ f $ x $ y)
    1.13    fun dest_fun_T1 (Type (_, T :: Ts)) = T
    1.14    fun find_double (t as Const (@{const_name fun_upd},T) $ f $ x $ y) =
    1.15      let
    1.16 @@ -476,20 +476,22 @@
    1.17              if v aconv x then SOME g else gen_fun_upd (find g) T v w
    1.18          | find t = NONE
    1.19      in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end
    1.20 -  fun fun_upd_prover ss =
    1.21 -    rtac eq_reflection 1 THEN rtac ext 1 THEN
    1.22 -    simp_tac (Simplifier.inherit_context ss @{simpset}) 1
    1.23 -  val fun_upd2_simproc =
    1.24 -    Simplifier.simproc @{theory}
    1.25 -      "fun_upd2" ["f(v := w, x := y)"]
    1.26 -      (fn _ => fn ss => fn t =>
    1.27 -        case find_double t of (T, NONE) => NONE
    1.28 -        | (T, SOME rhs) =>
    1.29 -            SOME (Goal.prove (Simplifier.the_context ss) [] []
    1.30 -              (Term.equals T $ t $ rhs) (K (fun_upd_prover ss))))
    1.31 -in
    1.32 -  Addsimprocs [fun_upd2_simproc]
    1.33 -end;
    1.34 +
    1.35 +  fun proc ss ct =
    1.36 +    let
    1.37 +      val ctxt = Simplifier.the_context ss
    1.38 +      val t = Thm.term_of ct
    1.39 +    in
    1.40 +      case find_double t of
    1.41 +        (T, NONE) => NONE
    1.42 +      | (T, SOME rhs) =>
    1.43 +          SOME (Goal.prove ctxt [] [] (Term.equals T $ t $ rhs)
    1.44 +            (fn _ =>
    1.45 +              rtac eq_reflection 1 THEN
    1.46 +              rtac ext 1 THEN
    1.47 +              simp_tac (Simplifier.inherit_context ss @{simpset}) 1))
    1.48 +    end
    1.49 +in proc end
    1.50  *}
    1.51  
    1.52