[isabelle] HOLCF's continuity with partially defined operators

```Hello,

I’m in the progress of formalizing Launchbury’s natural semantics for
lazy evaluation. For the denotational part, I use HOLCF machinery (which
was interesting to combine with Nominal, but it seems that I sailed
around that cliff).

The type of the semantic environments are a chain-complete partial order
(typeclass cpo). My current problem is that Launcbury uses the meet on
these, leaving it to the reader to believe that it is only used with
arguments where the least upper bound exists.

If I try to follow this path and define

definition meet :: "'a => 'a => 'a" (infixl "⊔" 70)
where "x ⊔ y = lub {x, y}"
definition have_meet :: "'a => 'a => bool"
where "have_meet x y = (∃ z. {x, y} <<| z)"

then maybe I will be able to show the have_meet property everywhere
where I use the meet.

But to be able to use HOLCF’s machinery, e.g. the lemmas from CFun.thy
and Fix.thy, I’d also have to show that the meet is continuous in both
its arguments, and that is currently not the case; it is not even
continuous, as x ⊔ y might exist, but x' ⊔ y for x' ⊒ x not.

What would be a sensible way to tackle this problem? Using the type
"'a => 'a => 'a option",
introducing a notion of continuous_if_defined and re-creating most of
HOLCF’s lemmas using this notation¹? Or maybe there is a way to extend
the meet continuously?

Thanks,
Joachim

¹ I already had to do that for the lemmas and definitions in Fix.thy, as
due to restrictions from Nominal, the environments need to have finite
support. But the type of maps with finite domain (which I introduced) is
not a pcpo, just a cpo, so I now have the notion of a least fixed point
“above a certain value”. If someone has use for that type, help yourself
at http://darcs.nomeata.de/isa-launchbury/, theories FMap, FMap-Nominal,
FMap-HOLCF and FMap-Nominal-HOLCF.

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