Hi,
Lately, I've been trying to define the "reverse" function on lazy lists but
I'm facing some issues. I understand that, unlike lists, in order to define
recursive function over lazy lists every time I need to justify the
definition of (co-)recursive functions (reverse in my case) that map into
the llist type using
llist_Axiom;
val it =
|- !f.
?g.
(!x. LHD (g x) = OPTION_MAP SND (f x)) /\
!x. LTL (g x) = OPTION_MAP (g o FST) (f x):
thm
So I'm trying to prove the following reverse function definition over llist
type
`?reverse.
( reverse ([||]) = LNIL) /\
(!x xs. reverse (LCONS x xs) = LAPPEND ( reverse xs) [|x|])`
but could not find the appropriate instance of "f" in llist_Axiom to prove
both the base and the inductive cases...
Any suggestion or comments?
--
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
