You need to define a helper function that has as its state not only the llist
that is being consumed but also a Boolean indicating whether or not to stop
(because a P-satisfying element has been seen).
- -
val until0_def =
new_specification ("until0_def", ["until0"],
ISPEC ``λbll. if FST bll then NONE
else if SND bll = [||] then NONE
else if P (THE (LHD (SND bll))) then
SOME ((T, THE (LTL (SND bll))), THE (LHD (SND bll)))
else SOME ((F, THE (LTL (SND bll))), THE (LHD (SND bll)))``
llist_Axiom_1 |> Q.GEN ‘P’ |> CONV_RULE (HO_REWR_CONV SKOLEM_THM));
val until0_T =
until0_def |> Q.SPEC `P` |> Q.SPEC ‘(T, ll)’ |> SIMP_RULE (srw_ss()) []
val until0_FCONS =
until0_def |> Q.SPEC `P` |> Q.SPEC ‘(F, h:::t)’ |> SIMP_RULE (srw_ss()) []
|> SIMP_RULE bool_ss [COND_RAND, Once COND_RATOR]
|> SIMP_RULE bool_ss [Once COND_RATOR]
|> SIMP_RULE (srw_ss()) [until0_T]
val until0_FNIL =
until0_def |> Q.SPEC `P` |> Q.SPEC ‘(F, [||])’ |> SIMP_RULE (srw_ss()) []
val until_def = Define‘until P ll = until0 P (F, ll)’
val until_thm = LIST_CONJ (map (SIMP_RULE bool_ss [GSYM until_def])
[until0_FNIL, until0_FCONS])
- -
Michael
From: Waqar Ahmad via hol-info <[email protected]>
Reply-To: Waqar Ahmad <[email protected]>
Date: Tuesday, 7 August 2018 at 03:26
To: hol-info <[email protected]>
Subject: [Hol-info] Partial Function on lazy list
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
