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



On Fri, Sep 3, 2010 at 12:50 PM, Joachim Breitner
<mail at joachim-breitner.de> wrote:
...
> 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))".

Well spotted. Indeed, the current cont2cont rule for Let assumes that
the variable x can appear in the bound expression, and it also
requires that the type of the bound expression be a cpo type. (I can
tell from your example that you are using the pcpo instance for type
bool; otherwise cont2cont_Let' couldn't have been applied at all.)

> 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 shouldn't be a conflict with the existing cont2cont_Let'. Wherever
the cont2cont rules are used by HOLCF simprocs or tools like fixrec,
"intro cont2cont" is used as a terminal method, which means that if
more than one rule applies, it will do backtracking if necessary to
solve the goal. Adding more rules might slow down the search a bit,
but it shouldn't break anything.

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

It would definitely be nice to have a tool or package that could
automatically generate these kinds of lemmas for HOL datatypes. For
the kinds of cont2cont lemmas you've shown above, it might not be that
hard. You can query the datatype package's theory data to get
information about datatypes, their case combinators, etc.

>
> Thanks,
> Joachim
>
> PS: I wrote a "list :: cpo(cpo)" instance, relating lists of equal
> length piecewise and not relating lists of different lengths, at
> http://git.nomeata.de/?p=funcCF.git;a=blob;f=CFGraph/HOLCFList.thy;hb=HEAD
> If you think this is generally useful and know where to put it I’d
> happily share it (after make the proofs prettier).

I also have a theory that defines the same cpo instance for lists; now
that there is a HOLCF/Library directory, I should put it in there.
I'll have a look at your theory, and if it implements anything that my
theory doesn't, I'll combine the two and add them to HOLCF/Library.

It's a shame that it takes so much work just to add HOLCF support for
one more datatype... It would be really nice to have a package that
could automatically generate cpo instances for HOL datatypes, along
with cont2cont rules for the constructors, etc. I've thought about it,
and it seems like it's possible, but it would be an awful lot of work
to implement. Maybe after I finish my PhD ;)

- Brian





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