*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] fixrec’s demand for continuity proofs*From*: Joachim Breitner <mail at joachim-breitner.de>*Date*: Sat, 04 Sep 2010 10:20:04 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <AANLkTimm0y6Krcbes=ZtHme8XF2pLge2jvK8HrScmGw7@mail.gmail.com>*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>*Sender*: Joachim Breitner <msg at joachim-breitner.de>

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? Thanks, Joachim -- Joachim "nomeata" Breitner mail: mail at joachim-breitner.de | ICQ# 74513189 | GPG-Key: 4743206C JID: nomeata at joachim-breitner.de | http://www.joachim-breitner.de/ Debian Developer: nomeata at debian.org

**Attachment:
signature.asc**

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

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

- Previous by Date: Re: [isabelle] fixrec’s demand for continuity proofs
- Next by Date: Re: [isabelle] fixrec’s demand for continuity proofs
- Previous by Thread: Re: [isabelle] fixrec’s demand for continuity proofs
- Next by Thread: Re: [isabelle] fixrec’s demand for continuity proofs
- 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