Hi Waqar,
First of all thanks for the reply. Your answer is very helpful to me.
What I want to achieve is to remove the first n items of the list each time and
operate on them,
and then continue to perform the same operation on the rest of the list until
the list is empty.
So after reading your reply, this problem can be solved.
thank you
Shang
-----原始邮件-----
发件人:"Waqar Ahmad" <12phdwah...@seecs.edu.pk>
发送时间:2018-06-05 07:43:50 (星期二)
收件人: "尚亚龙" <2016210...@mail.buct.edu.cn>
抄送: hol-info <hol-info@lists.sourceforge.net>
主题: Re: [Hol-info] Loops in HOL4
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
