[isabelle] Automating proofs involving function updates
I would like to automate some proofs that involve non-recursive data
types, records, and function updates.
datatype B = Zero | One
record R =
f :: "T ⇒ B"
fixes r::R and x::T
assumes "f r x = Zero"
and "r = r⦇f := (f r)(x := One)⦈"
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and