The function is already ready for use with any P; the final until_thm looks like
val until_thm =
⊢ (until P [||] = [||]) ∧
(until P (h:::t) = if P h then [|h|] else h:::until P t): thm
meaning that one can write things like
until (\x. x MOD 3 = 0) ll
for example. This seems like a suitably polymorphic function.
To tweak it to put your example element Q into the list instead of the actual
elements, change the core definition to also refer to Q. You will then need to
generalise Q as well as P, and to then skolemize twice.
Incidentally, Q is a bad name for an element; it looks too much like a name for
a predicate. You should use a name like ‘e’ instead.
Michael
From: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Thursday, 9 August 2018 at 06:08
To: "Norrish, Michael (Data61, Acton)" <michael.norr...@data61.csiro.au>
Cc: hol-info <hol-info@lists.sourceforge.net>
Subject: Re: [Hol-info] Partial Function on lazy list
Hi,
Great!. This really helps alot...:) However, I may be interested in defining it
for [\forall P] so that I don't need to instantiate every time with a specific
instance of P. I tried this by myself but every time I lost in connecting my
definition in llist form to its corresponding option theory form...:( Also,
what change should be made if I change my definition a little
val recur_llist_fn1_def = Define
`recur_llist_fn1 P Q w =
if (w = [||]) then [||]
else if P (THE (LHD w)) then
THE (LHD w) ::: (recur_llist_fn1 P Q (THE (LTL w)))
else Q:::(recur_llist_fn1 P Q (THE (LTL w)))`;
Any suggestions or thoughts?
On Mon, Aug 6, 2018 at 8:52 PM
<michael.norr...@data61.csiro.au<mailto:michael.norr...@data61.csiro.au>> wrote:
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
<hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>>
Reply-To: Waqar Ahmad
<12phdwah...@seecs.edu.pk<mailto:12phdwah...@seecs.edu.pk>>
Date: Tuesday, 7 August 2018 at 03:26
To: hol-info
<hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>>
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
hol-info@lists.sourceforge.net<mailto: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
