Email Gateway (Aug 19 2022 at 11:18): Email Gateway (Aug 19 2022 at 11:18):From: Giuliano Losa <giuliano.losa@epfl.ch>
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
Email Gateway (Aug 19 2022 at 11:18):From: Tobias Nipkow <nipkow@in.tum.de>
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
Last updated: May 06 2024 at 16:21 UTC