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.