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

Hi Brian,

Am Freitag, den 03.09.2010, 14:25 -0700 schrieb Brian Huffman:
> > 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
> > add it to HOLCF.
> It would be good to add this new rule to HOLCF, but I would make a
> small change to the "assumes" part:
> lemma cont2cont_Let_simple[simp,cont2cont]:
>  assumes "!!y. cont (λx. g x y)"
>  shows "cont (λx. let y = t in g x y)"
> unfolding Let_def using assms .
> In case "t" is a large term, and/or "y" occurs many times in the body
> of g, this might avoid a blow-up in term size.

it probably would not affect me at the moment, but are there no cases
where this would be too weak? What if "cont (λx. g x y)" does not hold
for all y, but only for y=t? But maybe such cases are only pathological
and do not occur in practice.

I guess the premise "let y = t in cont (λx. g x y)" would not allow the
other cont2cont rules to proceed.

> > Furthermore, I had to add these lemmas:
> > ______________________________________________________
> > 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.
> I see that these lemmas assume that the variable "x" doesn't occur in
> the scrutinee of the case expression; in practice it might be
> necessary to create both versions of cont2cont rules for each case
> combinator.

I used cont2cont_if as the template for these, and did not see a
cont2cont rule for if where x occurs in the condition. After all, it is
easy to create non-continuous functions then:
	cont (λx. if x then False else True)
using the bool:pcpo instance should be false (because it is not
monotonous), even though "cont (λx. x)", "cont (λx. False)" and "cont
(λx. True)" hold. What form would a cont2cont rule about if have, if x
appears in the condition?


Joachim "nomeata" Breitner
  mail: mail at | ICQ# 74513189 | GPG-Key: 4743206C
  JID: nomeata at |
  Debian Developer: nomeata at

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

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