Re: [isabelle] HOLCF's continuity with partially defined operators

On Wed, Jul 25, 2012 at 4:44 PM, Joachim Breitner <breitner at> 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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.