*To*: Joachim Breitner <mail at joachim-breitner.de>*Subject*: Re: [isabelle] fixrec’s demand for continuity proofs*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Thu, 2 Sep 2010 08:47:35 -0700*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1283437959.29045.42.camel@kirk>*References*: <1283436852.29045.36.camel@kirk> <1283437959.29045.42.camel@kirk>*Sender*: huffman.brian.c at gmail.com

On Thu, Sep 2, 2010 at 7:32 AM, Joachim Breitner <mail at joachim-breitner.de> 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" message. 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

**Follow-Ups**:**Re: [isabelle] fixrec’s demand for continuity proofs***From:*Joachim Breitner

**References**:**[isabelle] fixrec’s demand for continuity proofs***From:*Joachim Breitner

**Re: [isabelle] fixrec’s demand for continuity proofs***From:*Joachim Breitner

- Previous by Date: Re: [isabelle] sets in HOL/CF
- Next by Date: [isabelle] Two questions: one on "primrec hd" one on "value/normal_form"
- Previous by Thread: Re: [isabelle] fixrec’s demand for continuity proofs
- Next by Thread: Re: [isabelle] fixrec’s demand for continuity proofs
- Cl-isabelle-users September 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list