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



On Sat, Sep 4, 2010 at 1:20 AM, Joachim Breitner
<mail at joachim-breitner.de> wrote:
> 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.

Yes, I think such cases would be rather unusual. But the simplifier
might still be able to handle some such cases automatically, since
there are simp rules that unfold Let in special circumstances (such as
when t is a numeral or a constant).

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

Right, this would make "intro cont2cont" get stuck.


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

If you defined bool::cpo with a *discrete* ordering, then you could
prove this rule:

"cont f ==> cont g ==> cont h ==> cont (%x. if f x then g x else h x)"

But as you point out, this rule is not provable with the bool::pcpo
instance you are using. With bool::pcpo, you can't do any better than
the current cont2cont_if -- if-then-else is simply not continuous in
its first argument. (This is one of the reasons why HOLCF doesn't
define bool::pcpo by default: besides conjunction and disjunction,
most operations on booleans would not be continuous.)

- Brian

PS: I've just added an instance list :: (cpo) cpo to the repository;
you can view the file here:

http://isabelle.in.tum.de/repos/isabelle/file/d80990d8b909/src/HOLCF/Library/List_Cpo.thy

The theory includes two cont2cont rules for list_case: The first one
(cont2cont_list_case') requires the list element type to be a cpo, and
allows the variable x to occur in the scrutinee. The second one
(cont2cont_list_case_simple) works with non-cpo list types, but does
not allow the list expression to mention x.





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