*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*: Fri, 03 Sep 2010 21:50:23 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <AANLkTiks9_nW7znhWgdRByPCfy8_n+7jx3045JV87z3K@mail.gmail.com>*References*: <1283436852.29045.36.camel@kirk> <1283437959.29045.42.camel@kirk> <AANLkTiks9_nW7znhWgdRByPCfy8_n+7jx3045JV87z3K@mail.gmail.com>*Sender*: Joachim Breitner <msg at joachim-breitner.de>

Dear Brian, thanks for your detailed response, I’m having a much clearer picture now and also managed to define my function using HOLCF. 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))". 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. 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. 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). -- Joachim Breitner e-Mail: mail at joachim-breitner.de Homepage: http://www.joachim-breitner.de ICQ#: 74513189 Jabber-ID: nomeata at joachim-breitner.de

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

- Previous by Date: Re: [isabelle] Two questions: one on "primrec hd" one on "value/normal_form"
- 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