I'm not sure what actually you desired with WHILE function but I can
explain its functioning that might help you to define your function.
For instance, you can define a function that continue traversing over a
list until "P h" is true otherwise return the remaining part of the list.
!P L. dropWhile_new P L = WHILE (\a. P (HD a)) TL L
a trivial example could be
val dropWhile_eq = store_thm("dropWhile_eq",
``ALL_DISTINCT [a;b;c] ==> (dropWhile_new ($=a) [a;b;c] = [b;c])``,
rw[dropWhile_new_def]
\\ once_rewrite_tac[WHILE]
\\ rw[]
\\ once_rewrite_tac[WHILE]
\\ rw[]);
I hope this helps....
On Mon, Jun 4, 2018 at 10:08 AM, 尚亚龙 <2016210...@mail.buct.edu.cn> wrote:
> Hi everyone,
>
>
> I'm just beginning to learn HOL4. And I have a question.
>
>
>
> The problem is as follows: I have a list 'a',
>
> I want to use a loop to retrieve the number of 'num' in a each time until
> the list is empty,
>
> and I see WHILE theorems can be used in the HOL library, but I can not
> succeed,
>
> So I would like to ask how to implement the WHILE theorem,
>
> if you can, please attach an example to explain. Thank you!
>
>
>
> Shang
>
> ------------------------------------------------------------
> ------------------
> 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
