# [isabelle] Automating proofs involving function updates

Hello,
I would like to automate some proofs that involve non-recursive data
types, records, and function updates.
For example:
typedecl T
datatype B = Zero | One
record R =
f :: "T ⇒ B"
lemma test:
fixes r::R and x::T
assumes "f r x = Zero"
and "r = r⦇f := (f r)(x := One)⦈"
shows False
proof -
from assms(2) have "f r x = ((f r)(x := One)) x" by (cases r, simp)
hence "f r x = One" by simp
with assms(1) show ?thesis by simp
qed
Is there an easy way to enable simp or auto to solve this kind of goal?
Sledgehammer can solve this goal but fails as soon as the example gets a
little bigger.
Thanks,
Giuliano

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*