Re: [isabelle] fixrec’s demand for continuity proofs

On Thu, Sep 2, 2010 at 7:32 AM, Joachim Breitner
<mail at> wrote:
> Hi,
> I think I can answer one of the questions myself:
> Am Donnerstag, den 02.09.2010, 16:14 +0200 schrieb Joachim Breitner:
>> I’m also wondering why this works
>> ______________________________________________________
>> fixrec g :: "(int×int) discr → ((int×int) ⇒ one)" where
>>   "g⋅b = (case undiscr b of t ⇒ (g⋅(Discr t)) (t := ONE))"
>> ______________________________________________________
>> but this does not:
>> ______________________________________________________
>> fixrec g :: "(int×int) discr → ((int×int) ⇒ one)" where
>>   "g⋅b = (case undiscr b of (a,c) ⇒ (g⋅(Discr (a,c))) ((a,c) := ONE))"
>> ______________________________________________________
>> *** Continuity proof failed; please check that cont2cont rules
>> *** or simp rules are configured for all non-HOLCF constants.
>> *** The error occurred for the goal statement:
>> *** cont (λg. Λ a. case undiscr a of (a, c) ⇒ (g⋅(Discr (a, c)))((a, c) := ONE))
>> *** At command "fixrec".
> It works if I first show this lemma:
> ______________________________________________________
> lemma cont_prod_case [simp, cont2cont]:
>  "[|⋀ a b. cont (f a b)|] ==> cont (λx. prod_case (λa b. f a b x) p)"
> unfolding prod_case_unfold
> by (induct p) simp_all
> ______________________________________________________
> Does this mean that I have to show such a lemma for every function (or
> case expression) that contains a recursive call to the function I’m
> defining with fixrec? Or is there some automatism that I’m missing at
> the moment?
> Thanks again,
> Joachim

Hello again,

You are exactly right: Every function (or case combinator) that
contains a recursive call needs to have a corresponding continuity
lemma. Sometimes a shortcut might be possible (functions with a
discrete argument type are always continuous, for example) but in
general there is no way around this requirement.

The way fixrec tries to prove its continuity subgoals is really quite
simple. You get the continuity goal from the recursive definition:

cont (λg. Λ a. case undiscr a of (a, c) ⇒ (g⋅(Discr (a, c)))((a, c) := ONE))

First, fixrec tries to solve this goal by doing "apply (intro
cont2cont)". If that doesn't work, then it tries "apply simp". If that
doesn't work either, then you get the "Continuity proof failed"

If a subterm has no recursive calls, it can be solved instantly by
rule cont_const (which is in cont2cont); otherwise there must be a
cont2cont rule that matches the current subterm. A good way to debug
the continuity proof is to copy the subgoal from the error message and
try to prove it as a lemma using "apply (intro cont2cont)". If it gets
stuck at any point, then look at the top-level constant to see what
continuity rule you need.

Hope this helps,

- Brian

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.