Thanks.
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.
>
This is exactly what I'm doing for mimic the Isabelle definitions like
primcorec flat where
"shd (flat ws) = hd (shd ws)"
| "stl (flat ws) = flat (if tl (shd ws) = [] then stl ws else tl (shd ws)
## stl ws)"
!L. sflat L = LFLATTEN (fromList L)
where sflat is lifted from the ordinary list to lazylists. Since, there is
not function available for reversing the lazy list so I've to define it
from scratch. I prefer axiomatic characterization of reverse in this case
>
> 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.
>
Thanks. I modified the reverse function definition to incorporate the
effect of finite lazy lists as
?reverse.
(reverse [||] = [||]) /\
!xs.
reverse xs =
if LFINITE xs then
LAPPEND (reverse (THE (LTL xs))) [|THE (LHD xs)|]
else xs
from LLIST_BISIMULATION, I need to assign an instance of relation R between
the characterizations as
?R.
R (g xs)
(if LFINITE xs then LAPPEND (g (THE (LTL xs))) [|THE (LHD xs)|]
else xs) /\
!ll3 ll4.
R ll3 ll4 ==>
(ll3 = [||]) /\ (ll4 = [||]) \/
(LHD ll3 = LHD ll4) /\ R (THE (LTL ll3)) (THE (LTL ll4))
------------------------------------
0. !x.
LHD (g x) =
OPTION_MAP SND
((\ll.
if LFINITE ll then
if ll = [||] then NONE
else
SOME
(fromList (FRONT (THE (toList ll))),
LAST (THE (toList ll)))
else SOME (ll,ARB)) x)
1. !x.
LTL (g x) =
OPTION_MAP (g o FST)
((\ll.
if LFINITE ll then
if ll = [||] then NONE
else
SOME
(fromList (FRONT (THE (toList ll))),
LAST (THE (toList ll)))
else SOME (ll,ARB)) x)
I've tried several options, one of them is
`\ll1 ll2. ?xs. (ll1 = g xs) /\
(ll2 = (if LFINITE xs then LAPPEND (g (THE (LTL xs))) [|THE
(LHD xs)|]
else xs))`
but at some point in proof I cannot reason it further. Any suggestion or
comments?
>
> 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
>
>
--
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
