Dear Shang,
reading your question, I was wondering, whether you really want to use a
WHILE loop. Usually you would rather use recursion in HOL. In higher
order logic you don't have a state that you can modify. Of course you
can mimic a state by passing it around explicitly. This is what the
WHILE function does. If you are new to HOL and have not done much
functional programming before, I recommend learning functional
programming first. Prof. Larry Paulson's book "ML for the working
programmer" is available online and a very good introduction
http://www.cl.cam.ac.uk/~lp15/MLbook/pub-details.html.
I'm also uncertain what you want to do exactly, but for me it sounds
like a combination of standard list functions like MAP, TAKE or FOLDL
might be what you really want. In HOL you talk about the value of
things, you don't have a global state to manipulate and there is nothing
like execution or an execution order. So - while it is a common thing to
say and people do it very frequently as a shortcut - strictly speaking
"removing the first n items of a list" is not something you can do. You
cannot modify an existing list. You talk about the first n elements of a
list (TAKE) or about the list you get by removing the first n elements
(DROP), but you don't have a concept of execution there and the original
list does not change. You talk about values and pass different lists
around explicitly. Similarly things like "operate on them" sounds like
doing something that modifies the global state (like e.g. printing
them). This is just nothing you can do in HOL. Timing is meaningless as
well. So things like first do something then "continue" to do something
else is meaningless. You talk about the value of a function, not how you
compute that value.
Best
Thomas
On 05.06.2018 04:23, 尚亚龙 wrote:
> 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
> <mailto: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
> <mailto:hol-info@lists.sourceforge.net>
> https://lists.sourceforge.net/lists/listinfo/hol-info
> <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
------------------------------------------------------------------------------
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
