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



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
Description: This is a digitally signed message part



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