Hi,
Thanks!. The tip is spot on..:) Now, I'm able to define it as
val recur_llist_fn1_thm =
(recur_llist_fn1 P e [||] = [||]) [image: \wedge]
(recur_llist_fn1 P e (h:::t) =
if P h then h:::recur_llist_fn1 P e t
else e:::recur_llist_fn1 P e t)
On Wed, Aug 8, 2018 at 7:20 PM <michael.norr...@data61.csiro.au> wrote:
> 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 [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
>
--
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
