*To*: Joachim Breitner <breitner at kit.edu>*Subject*: Re: [isabelle] HOLCF's continuity with partially defined operators*From*: Brian Huffman <huffman at in.tum.de>*Date*: Thu, 26 Jul 2012 07:39:44 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1343227480.4148.32.camel@kirk>*References*: <1343033044.4224.22.camel@kirk> <CAAMXsiYgpvXL=+yWkh78sZrbJavWgz700eVA9FjBLMoQJsi21A@mail.gmail.com> <1343040279.4224.38.camel@kirk> <CAAMXsiahLz3wyUsjGfP9eU5hKBmD=Ymsm+R7wmR1BGc4F5x=qw@mail.gmail.com> <1343217287.4148.17.camel@kirk> <1343227480.4148.32.camel@kirk>

On Wed, Jul 25, 2012 at 4:44 PM, Joachim Breitner <breitner at kit.edu> wrote: > Dear Brian, > > Am Mittwoch, den 25.07.2012, 13:54 +0200 schrieb Joachim Breitner: >> Then I defined >> domain Value_ = Fn (lazy "Value_ d → Value_ d") >> type_synonym Value = "Value_ d" >> and it seems that instantiating Nonempty_Meet_cpo for Value_ is what is >> left to do. >> >> Morally, things look clear to me: Either the set has a bottom, the the >> meet is bottom, or all elements are of the form "Fn _", then I take the >> meet pointwise. But this recurses, so I’m not sure how to define it. >> >> Because of the indirect recursion in the definition of Value_, no >> “normal” induction rules are available. My first approach would be to >> show that for every nonempty S, I find a meet of "Value__take i ` >> S" (and I am hoping that I can show this by induction on i, but I’m not >> sure yet). Then the lub of these seems to be the meet of M. I am a bit >> worried about the use of cfun_map in Value__take and whether it behaves >> well in the inductive step of the proof. [...] > You know the domains better than me: Do you still expect that is > possible to show the existence of arbitrary meets for such a data type, > and if so, how? > > Thanks a lot in advance, > Joachim Hi Joachim, Your idea of finding the meet of set M by taking the lub of a sequence of meets of (take i ` M) is on the right track. I think you should be able to show that any bifinite domain with binary meets has arbitrary nonempty meets. First, note that if you have binary meets then you have all nonempty finite meets. Then from bifiniteness, there exists a chain of approx functions: Like take functions, these have their lub = ID, but more importantly each one also has a finite range, so (approx i ` M) is always a finite set. Finally, LUB i. Meet (approx i ` M) should give you the meet for M. - Brian

**Follow-Ups**:**Re: [isabelle] HOLCF's continuity with partially defined operators***From:*Joachim Breitner

**References**:**[isabelle] HOLCF's continuity with partially defined operators***From:*Joachim Breitner

**Re: [isabelle] HOLCF's continuity with partially defined operators***From:*Brian Huffman

**Re: [isabelle] HOLCF's continuity with partially defined operators***From:*Joachim Breitner

**Re: [isabelle] HOLCF's continuity with partially defined operators***From:*Brian Huffman

**Re: [isabelle] HOLCF's continuity with partially defined operators***From:*Joachim Breitner

**Re: [isabelle] HOLCF's continuity with partially defined operators***From:*Joachim Breitner

- Previous by Date: Re: [isabelle] HOLCF equality type class
- Next by Date: Re: [isabelle] Simple question about theory parameter
- Previous by Thread: Re: [isabelle] HOLCF's continuity with partially defined operators
- Next by Thread: Re: [isabelle] HOLCF's continuity with partially defined operators
- Cl-isabelle-users July 2012 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