add lemma to FinFun

--- a/src/HOL/Library/FinFun.thy	Mon Jun 04 12:55:54 2012 +0200
+++ b/src/HOL/Library/FinFun.thy	Tue Jun 12 15:31:53 2012 +0200
@@ -906,6 +906,9 @@
 lemma expand_finfun_eq: "(f = g) = (op $ f = op $ g)"
 by(auto intro: finfun_ext)
 
+lemma finfun_upd_triv [simp]: "f(x $:= f $ x) = f"
+by(simp add: expand_finfun_eq fun_eq_iff finfun_upd_apply)
+
 lemma finfun_const_inject [simp]: "(K$ b) = (K$ b') \<equiv> b = b'"
 by(simp add: expand_finfun_eq fun_eq_iff)