# Re: [isabelle] Automating proofs involving function updates

The problem is that "r = r..." cannot be used as a rewrite rule because it would
not terminate. The simplifier recognises that and ignores that rule. However,
you can apply it by hand via "subst". Here is your proof in compact form:
proof -
from assms(1) show False
apply(subst (asm) assms(2))
by simp
qed
This is not automate matters but may help you a little.
Something else that may help is to turn equalities between records into
equalities between fields. In your case the lemma
lemma R_ext: "((r1::R) = r2) = (f r1 = f r2)"
by auto
can be given to the simplifier and turns your second assumption into
f r = (f r)(x := One)
and lemma fun_eq_iff can lower that one step further. But the difficulty remains
that you may have recursive equations that the simplifier will not use.
I suspect that your problem is actually automatable but requires more work at
the ML level.
Tobias
Am 21/06/2013 17:57, schrieb Giuliano Losa:
> 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.*