[isabelle-dev] HOLCF lists

[Brian Huffman]

On Tue, Jul 17, 2012 at 11:04 AM, Christian Sternagel
<c-sterna at jaist.ac.jp> wrote:
> Dear all,
>
> I put together some functions on lists (that I use in some small proof) in
> Data_List.thy. While doing so and thinking about functions and proofs I
> would need in the future, I stumbled across the following points:
>
> 1) how to name HOLCF functions for which similar functions already exist in
> HOL. As you can see from my example thy-file, I tried to be as close to
> Haskell as possible and therefore hid existing HOL-names. My thinking was
> that when having a HOLCF type of lazy lists one would never want to use the
> HOL datatype list again. Maybe this was oversimplified. What do you think?

I think it is a good idea to use the Haskell names for the HOLCF list functions.

As for name-hiding, ideally this is something that users, not library
writers, should decide. Eventually I hope to see a feature like
"import qualified" for Isabelle. I wouldn't spend too much time
worrying about this for now.

> 2) I think at some point something like "set :: 'a list => 'a set" for HOLCF
> lists would be useful...

What for? Is it meant to be an abstraction of some kind of executable
function, or is it only useful for writing logical specifications?

> however, I did not manage to define it, since I was
> not able to prove continuity for the following specification
>
> "set $ Nil = {}" |
> "set $ (Cons$x$xs) = insert$x$(set$xs)"
>
> Maybe such a function is not a good idea at all in the HOLCF setting and we
> should find something different.

For "set" to have a continuous function type, you must be using a cpo
instance for 'a set, but which one?

If you want "set" to correspond to an executable type of thing, then
probably some kind of powerdomain would serve better as the result
type. But if you only want to use "set" for writing specifications,
then it probably shouldn't be defined as a continuous function; an
inductive definition would make more sense.

> 3) also if properties only hold for "defined" instances of lists (there are
> some differences in how defined they have to be... only xs not bottom, or
> additional no element of xs is bottom, ...), I am currently missing a
> convenient way of expressing this... (first I was thinking about "set" from
> above... but then again, if "set" is a continuous function also "set$xs" can
> be undefined... so maybe there is a nicer way?)

My suggestion: If a property is executable, then define it as a
continuous function; if it is not executable, then define it as an
ordinary HOL predicate.

> 4) How to nicely integrate natural numbers? I don't really want to mix =>
> and ->, e.g., the "list"-function "take" should have type "nat lift -> 'a
> list -> 'a list" (or something similar), rather than "nat => 'a list -> 'a
> list" I guess.

HOLCF/Library/{Nat,Int}_Discrete.thy define cpo instances for types
nat and int, so you can write types like "nat -> 'a list" or
"nat\<^sub>\<bottom> -> 'a list". Decisions about which types to use
should probably follow Haskell: "Integer" should be modeled as
"int\<^sub>\<bottom>" or "int lift", and for unboxed Haskell types
(e.g. Int#) you can use "int".

- Brian


>
> I am sure some of you have already considered the above points ;), so please
> let me know your conclusions.
>
> cheers
>
> chris
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>