*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*: Fri, 3 Sep 2010 14:25:13 -0700*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1283543423.2794.18.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>*Sender*: huffman.brian.c at gmail.com

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

**Follow-Ups**:**Re: [isabelle] fixrec’s demand for continuity proofs***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

- 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