*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] HOLCF's continuity with partially defined operators*From*: Joachim Breitner <breitner at kit.edu>*Date*: Wed, 25 Jul 2012 16:44:40 +0200*In-reply-to*: <1343217287.4148.17.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>*Sender*: Joachim Breitner <msg at joachim-breitner.de>

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. I’m having a hard time showing that there are meets for my data type. For the inductive proof of ∃ u. {Value__take i ⋅ x | x . x ∈ S } >>| u in the case where I know that all elements of S have the form "Fn⋅_", I need to show the existence of a meet of the image of set of continuous functions ("S :: (Value_ d → Value_ d) set"), under cfun_map⋅f⋅g (where f and g involve "Value__take i"). By induction, I know that "⨅ (g ` S')" exists for any S' of type "Value_ d set", so pointwise, the meet exists. My hope was to show the following lemma, which would then give me the existence of the meet of the set of function: lemma has_glb_cfunI: assumes "(!! x. ∃ l. (λ f. f⋅x) ` S >>| l)" shows "(∃ l. S >>| l)" I did not manage to proof that, though, and I am worried that it might not hold. By analogy from analysis, the set of functions on [0,2] given by {x^n | n ∈ [1..∞]} has pointwise infimums, but itself none. 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 -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.info.uni-karlsruhe.de/~breitner

**Attachment:
signature.asc**

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

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

- Previous by Date: [isabelle] Uniqueness quantification
- 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