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



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

-- 
Joachim Breitner
  e-Mail: mail at joachim-breitner.de
  Homepage: http://www.joachim-breitner.de
  ICQ#: 74513189
  Jabber-ID: nomeata at joachim-breitner.de

Attachment: signature.asc
Description: This is a digitally signed message part



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