*To*: Joachim Breitner <mail at joachim-breitner.de>*Subject*: Re: [isabelle] fixrec’s demand for continuity proofs*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Sat, 4 Sep 2010 08:20:22 -0700*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1283588404.2560.7.camel@kirk>*References*: <1283436852.29045.36.camel@kirk> <1283437959.29045.42.camel@kirk> <AANLkTiks9_nW7znhWgdRByPCfy8_n+7jx3045JV87z3K@mail.gmail.com> <1283543423.2794.18.camel@kirk> <AANLkTimm0y6Krcbes=ZtHme8XF2pLge2jvK8HrScmGw7@mail.gmail.com> <1283588404.2560.7.camel@kirk>*Sender*: huffman.brian.c at gmail.com

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.

**Follow-Ups**:**[isabelle] adm and fixrec’s induct rules***From:*Joachim Breitner

**References**:**[isabelle] fixrec’s demand for continuity proofs***From:*Joachim Breitner

**Re: [isabelle] fixrec’s demand for continuity proofs***From:*Joachim Breitner

**Re: [isabelle] fixrec’s demand for continuity proofs***From:*Brian Huffman

**Re: [isabelle] fixrec’s demand for continuity proofs***From:*Joachim Breitner

**Re: [isabelle] fixrec’s demand for continuity proofs***From:*Brian Huffman

**Re: [isabelle] fixrec’s demand for continuity proofs***From:*Joachim Breitner

- Previous by Date: Re: [isabelle] fixrec’s demand for continuity proofs
- Next by Date: [isabelle] Congruence rule for Let
- Previous by Thread: Re: [isabelle] fixrec’s demand for continuity proofs
- Next by Thread: [isabelle] adm and fixrec’s induct rules
- Cl-isabelle-users September 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list