Hi all,
Is there any easy way to define the following partial function on lazy list
val recur_llist_fn_def = Define
`recur_llist_fn P w =
if P (THE (LHD w)) then [|THE (LHD w)|]
else (THE (LHD w)):::(recur_llist_fn P (THE (LTL w)))`;
Otherwise, I can also include the LNIL case as
val recur_llist_fn_def = Define
`recur_llist_fn P w = if (w = [||]) then [||] else
if P (THE (LHD w)) then [|THE (LHD w)|]
else (THE (LHD w)):::(recur_llist_fn P (THE (LTL w)))`;
but I'm having issue to write its corresponding axiomatic form for
llist_Axiom_1:
!f. ?g. !x. g x = case f x of NONE => [||] | SOME (a,b) => b:::g a
Particularly for P (THE (LHD w)) what will be SOME (?)....
Any suggestion or thoughts?
--
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
