Hi,
Great!. This really helps alot...:) However, I may be interested in
defining it for [image: \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> 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>
> Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk>
> Date: Tuesday, 7 August 2018 at 03:26
> To: hol-info <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
> 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
