Hi,
Lately, I've been exploring the HOL4 lazy list theory "llistTheory", which
is developed based on the co-algebraic datatype. I understand that the
datatype *'a llist *is derived as a subset of the option type *:num -> 'a
option. * Now, I want to define a new datatype based on datatype 'a llist.
For instance,
P of 'a llist
such that *P: 'a llist -> 'a stream*, where *'a stream* is essentially the
similar datatype as *'a llist* but having different properties. In shallow
embedding, I can define it by using filter function of llistTheory as:
val Stream = Define `Stream L = LFILTER (\n:'a. T) L`;
One way of defining the co-inductive datatype *stream* is to follow the
same procedure as described in "llistTheory", which is quite cumbersome. Is
there any alternate way similar to that of package "Hol_datatype"?
Secondly, Is it possible to define a co-inductive datatype that takes a set
type (:'a -> bool) and maps it to a set of type (:'a llist -> bool)? A
similar function, in shallow embedding, I can think of is:
val streams_def = Define
`streams A = IMAGE (\a. Stream a) {llist_abs x | x IN A} `;
where the function streams is of type (:num -> 'a option) ->bool -> 'a
llist-> bool
In some cases, the function *streams* doesn't suffice for modeling the
correct behavior of streams related properties..
Any suggestion or thoughts would be highly helpful...
--
Waqar Ahmad, Ph.D.
Post Doc at Hardware Verification Group (HVG)
Department of Electrical and Computer Engineering
Concordia University, QC, Canada
Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
