As reverse on llist only really works when the argument is finite, the easiest
definition would be
Lrev ll = fromList (REVERSE (toList ll))
You could lift this to infinite lists by having
~LFINITE ll ==> (Lrev ll = infinite-list-of something)
Or similar. As it happens, I believe such a definition then satisfies your
desired characterisation.
One f you could instantiate the axiom with to get this effect would be
f ll = if LFINITE ll then if ll = [||] then NONE else SOME (fromList (FRONT
(toList ll)), LAST (toList ll))
else SOME (ll, ARB)
Your characterisation should follow from a bisimulation argument.
Michael
From: Waqar Ahmad via hol-info <hol-info@lists.sourceforge.net>
Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Wednesday, 23 May 2018 at 15:21
To: hol-info <hol-info@lists.sourceforge.net>
Subject: [Hol-info] Reverse Function on LazyLists
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
