[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.