# HG changeset patch
# User Andreas Lochbihler
# Date 1339507913 -7200
# Node ID 0122ba071e1a6dbc7a1518b2087d8f48a52f8c42
# Parent  d7864276bca8938fba936cb155678da403567e66
add lemma to FinFun

diff -r d7864276bca8 -r 0122ba071e1a src/HOL/Library/FinFun.thy
--- 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)