added fun_upd2_simproc

--- a/src/HOL/Fun.ML	Fri Jul 14 16:27:37 2000 +0200
+++ b/src/HOL/Fun.ML	Fri Jul 14 16:27:42 2000 +0200
@@ -434,7 +434,8 @@
 qed "fun_upd_apply";
 Addsimps [fun_upd_apply];
 
-(*fun_upd_apply supersedes these two*)
+(* fun_upd_apply supersedes these two,   but they are useful 
+   if fun_upd_apply is intentionally removed from the simpset *)
 Goal "(f(x:=y)) x = y";
 by (Simp_tac 1);
 qed "fun_upd_same";
@@ -449,6 +450,27 @@
 qed "fun_upd_upd";
 Addsimps [fun_upd_upd];
 
+(* simplifies terms of the form f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *)
+local 
+  fun gen_fun_upd  None    T _ _ = None
+  |   gen_fun_upd (Some f) T x y = Some (Const ("Fun.fun_upd",T) $ f $ x $ y)
+  fun dest_fun_T1 (Type (_,T::Ts)) = T
+  fun find_double (t as Const ("Fun.fun_upd",T) $ f $ x $ y) = let
+      fun find         (Const ("Fun.fun_upd",T) $ g $ v $ w) = 
+          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
+  val fun_upd_prover = K [rtac eq_reflection 1, rtac ext 1, 
+                          simp_tac (simpset_of Fun.thy) 1]
+  fun mk_eq_cterm sg T l r = Thm.cterm_of sg (equals T $ l $ r)
+in 
+  val fun_upd2_simproc = Simplifier.mk_simproc "fun_upd2"
+   [Thm.read_cterm (sign_of Fun.thy) ("f(v:=w,x:=y)", HOLogic.termT)] 
+   (fn sg => (K (fn t => case find_double t of (T,None)=> None | (T,Some rhs)=> 
+       Some (prove_goalw_cterm [] (mk_eq_cterm sg T t rhs) fun_upd_prover))))
+end;
+Addsimprocs[fun_upd2_simproc];
+
 Goal "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)";
 by (rtac ext 1);
 by Auto_tac;

--- a/src/HOL/IMP/Examples.ML	Fri Jul 14 16:27:37 2000 +0200
+++ b/src/HOL/IMP/Examples.ML	Fri Jul 14 16:27:42 2000 +0200
@@ -4,13 +4,6 @@
     Copyright   2000 TUM
 *)
 
-(*###should go to Fun.ML*)
-Goal "f(x:=y,a:=b,x:=z) = f(a:=b,x:=z)";
-by (rtac ext 1);
-by (Simp_tac 1);
-qed "fun_upd_upd2";
-Addsimps [fun_upd_upd2];
-
 Addsimps[update_def];
 
 section "Examples";