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

```Dear Brian,

thanks for your detailed response, I’m having a much clearer picture now
and also managed to define my function using HOLCF.

I had some problems with the cont2cont_Let' rule in the cont2cont rule
set. Here is a minimal example:
______________________________________________________
lemma "cont (λx. x⋅(Discr True))"
by (intro cont2cont)
______________________________________________________
works as expected. But
______________________________________________________
lemma "cont (λx. let y = True in x⋅(Discr y))"
by (intro cont2cont)
______________________________________________________
does not. The goal that it is stuck on is
"cont (λp. Discr (snd p))".

It works after I added this lemma to the cont2cont set, which works for
let expressions where the variable x does not appear in the bound
expression:
______________________________________________________
lemma cont2cont_Let_simple[simp,cont2cont]:
assumes "cont (λx. g x t)"
shows "cont (λx. let y = t in g x y)"
unfolding Let_def using assms .
______________________________________________________

I’m not sure if this is a general solution and or it would somehow
conflict with cont2cont_Let'. If it is a general solution, feel free to

______________________________________________________
lemma cont2cont_list_case [simp, cont2cont]:
assumes "⋀y. cont (λx. f1 x)"
and  "⋀y z. cont (λx. f2 x y z)"
shows "cont (λx. list_case (f1 x) (f2 x) l)"
using assms
by (cases l) auto

lemma cont2cont_prod_case [simp, cont2cont]:
assumes "⋀y z. cont (λx. f x y z)"
shows "cont (λx. prod_case (f x) p)"
using assms
by (cases p) auto
______________________________________________________
plus similar ones for each algebraic data types that I am using. The
form of these lemmas is very static – do you think this can be
generalized somehow? I did not yet write any ML scripts in Isabelle, but
I’m eager to learn if there is a worthwhile goal.

Thanks,
Joachim

PS: I wrote a "list :: cpo(cpo)" instance, relating lists of equal
length piecewise and not relating lists of different lengths, at
If you think this is generally useful and know where to put it I’d
happily share it (after make the proofs prettier).

--
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.