[isabelle] Automating proofs involving function updates

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

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.


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