*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 13:24:43 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1343294705.4221.25.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> <CAAMXsibTcvy=kJfM2VtgooxmKep-ckVm25UjsFy=jYTTAzvyYQ@mail.gmail.com> <1343294705.4221.25.camel@kirk>

On Thu, Jul 26, 2012 at 11:25 AM, Joachim Breitner <breitner at kit.edu> wrote: > Dear Brian, > > Am Donnerstag, den 26.07.2012, 07:39 +0200 schrieb Brian Huffman: >> > 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. > > thanks for the hint, here is my progress so far: I was able to define > and proof the following class relations: > > class Finite_Meet_cpo = cpo + > assumes binary_meet_exists: "∃ l. l ⊑ x ∧ l ⊑ y ∧ (∀ z. (z ⊑ x ∧ z ⊑ y) ⟶ z ⊑ l)" > > class Finite_Meet_bifinite_cpo = Finite_Meet_cpo + bifinite > > instance Finite_Meet_bifinite_cpo ⊆ Nonempty_Meet_cpo > > So indeed all I need to do is to give an > > instance Value_ :: Finite_Meet_cpo > > but it seems I am stuck at the same problem as before. To show the > existence the meet of two values of the form "Fn f" and "Fn g" (while, > by induction, knowing that their images have pairwise meets), I can > define that as "Fn (Λ x . f x ⨅ g x)" but I have trouble showing that it > is continuous. You should try constructing the witness for the binary meet directly as a continuous function, e.g. fixrec meet :: "Value_ → Value_ → Value_" where "meet⋅(Fn⋅f)⋅(Fn⋅g) = Fn⋅(Λ x. (Λ (up⋅a) (up⋅b). up⋅(meet⋅a⋅b))⋅(f⋅x)⋅(g⋅x))" Using this definition, I was able to prove "(t ⊑ meet⋅u⋅v) = (t ⊑ u ∧ t ⊑ v)" by take induction on t. [...] > It seems that I don’t take the right approach to define the meet of two > function values. Is there some more magic required to define the meet? No magic should be necessary; binary meets of (continuous) functions are defined pointwise. - Brian

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

**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: Re: [isabelle] Simple question about theory parameter
- Next by Date: Re: [isabelle] Uniqueness quantification
- Previous by Thread: Re: [isabelle] HOLCF's continuity with partially defined operators
- Next by Thread: [isabelle] Simple question about theory parameter
- 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