On Tue, Jul 17, 2012 at 11:04 AM, Christian Sternagel
c-ste...@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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
