If you want to build HOL with Poly/ML, you should run
poly < tools/smart-configure.sml
before running bin/build.
On 2 March 2016 at 13:18, 康漫 <956066...@qq.com> wrote:
> Thank you for your reply!
> My version of HOL4 is HOL-4 [Kananaskis 10 (stdknl, built Mon Nov 10
> 14:27:30 2014)], where Moscow ML version 2.01 (January 2004). Then from
> https://hol-theorem-prover.org/#get, I installed PolyML5.6-32bit, and
> pointed ""bin/build". Then I got HOL-4 [Kananaskis 10 (stdknl, built Mon
> Feb 29 21:47:05 2016)],where Moscow ML version 2.01 (January 2004).
> I Opened HOL4, print"open listTheory;", I still can't use LENGTH_TAKE_EQ,
> it responed "Unbound value component: listTheory.LENGTH_TAKE_EQ". I had
> downloaded the files in https://github.com/HOL-Theorem-Prover/HOL. How to
> add it to HOL4's directory? After that ,I could print "open listTheory;"
> in HOL4, and use LENGTH_TAKE_EQ.
>
> Thanks.
>
>
>
> ------------------ Original ------------------
> *From: * "hol-info-request";<hol-info-requ...@lists.sourceforge.net>;
> *Date: * Wed, Mar 2, 2016 06:31 AM
> *To: * "hol-info"<hol-info@lists.sourceforge.net>;
> *Subject: * hol-info Digest, Vol 118, Issue 1
>
> Send hol-info mailing list submissions to
> hol-info@lists.sourceforge.net
>
> To subscribe or unsubscribe via the World Wide Web, visit
> https://lists.sourceforge.net/lists/listinfo/hol-info
> or, via email, send a message with subject or body 'help' to
> hol-info-requ...@lists.sourceforge.net
>
> You can reach the person managing the list at
> hol-info-ow...@lists.sourceforge.net
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of hol-info digest..."
>
>
> Today's Topics:
>
> 1. Re: How to transform list format from "(cx l q p)" to "l"
> (Anthony Fox)
> 2. Re: Existential quantifier length (Michael Norrish)
> 3. ? Summer School on Real-World Crypto and Privacy, June 5-10,
> Croatia (Veelasha)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Mon, 29 Feb 2016 10:25:51 +0000
> From: Anthony Fox <ac...@cam.ac.uk>
> Subject: Re: [Hol-info] How to transform list format from "(cx l q p)"
> to "l"
> To: ?? <956066...@qq.com>
> Cc: hol-info <hol-info@lists.sourceforge.net>
> Message-ID: <6c0cb742-6c45-45b0-80bd-78737f4cd...@cam.ac.uk>
> Content-Type: text/plain; charset=utf-8
>
> Which version of HOL4 are you using? The definitions of TAKE and DROP were
> altered in Jan 2008 (around about the time of kananaskis-5).
>
> With the latest version of HOL4 Jeremy Dawson?s suggestion works fine for
> me. The proof seems to be trivial. (I?ve not tried it with older versions
> of HOL4.) How exactly did you define ?cx??
>
> With
>
> val cx_def = Define`
> (cx [] p q = p) /\
> (cx (h :: t) p q = TAKE h (cx t p q) ++ DROP h (cx t q p))`
>
> we have
>
> val th = Q.prove(
> `!p q l. (LENGTH p = LENGTH q) ==> (LENGTH (cx l p q) = LENGTH p)`,
> Induct_on `l` THEN RW_TAC list_ss [cx_def, listTheory.LENGTH_TAKE_EQ])
>
> To get something closer to your definition of ?cx? I did
>
> val cx_def = tDefine "cx" `
> (cx [] p q = p) /\
> (cx (h :: t) p q =
> TAKE (HD (h :: t)) (cx (TL (h :: t)) p q) ++
> DROP (HD (h :: t)) (cx (TL (h :: t)) q p))`
> (WF_REL_TAC `measure (\(x,y,z). LENGTH x)` THEN simp [])
>
> but the proof worked without modification.
>
> Regards,
> Anthony
>
> > On 29 Feb 2016, at 07:38, ?? <956066...@qq.com> wrote:
> >
> > Hi,Jeremy
> > Thank you for your reply!
> > I tried. But it can't work.
> > It responsed:
> > - e (RW_TAC list_ss [LENGRH_DROP]);
> > OK..
> > Exception raised at Tactical.VALID:
> > Invalid tactic
> > ! Uncaught exception:
> > ! HOL_ERR
> > I think the reason is that the format of "(cx l q p)" is not equal to
> "l", though they are the same type "bool list".
> > Thank you!
> >
> > ------------------ Original ------------------
> > From: "hol-info-request";<hol-info-requ...@lists.sourceforge.net>;
> > Date: Mon, Feb 29, 2016 01:08 PM
> > To: "hol-info"<hol-info@lists.sourceforge.net>;
> > Subject: hol-info Digest, Vol 117, Issue 9
> >
> > Send hol-info mailing list submissions to
> > hol-info@lists.sourceforge.net
> >
> > To subscribe or unsubscribe via the World Wide Web, visit
> > https://lists.sourceforge.net/lists/listinfo/hol-info
> > or, via email, send a message with subject or body 'help' to
> > hol-info-requ...@lists.sourceforge.net
> >
> > You can reach the person managing the list at
> > hol-info-ow...@lists.sourceforge.net
> >
> > When replying, please edit your Subject line so it is more specific
> > than "Re: Contents of hol-info digest..."
> >
> >
> > Today's Topics:
> >
> > 1. How to transform list format from "(cx l q p)" to "l" ( Ada )
> > 2. Re: How to transform list format from "(cx l q p)" to "l"
> > (Jeremy Dawson)
> > 3. Two postdoc positions - Reasoning about concurrency and
> > distribution - Imperial College London (Petar Maksimovic)
> >
> >
> > ----------------------------------------------------------------------
> >
> > Message: 1
> > Date: Sun, 28 Feb 2016 19:48:56 +0800
> > From: " Ada " <ada.k...@qq.com>
> > Subject: [Hol-info] How to transform list format from "(cx l q p)" to
> > "l"
> > To: " hol-info " <hol-info@lists.sourceforge.net>
> > Message-ID: <tencent_6526cfdf05ecaae746588...@qq.com>
> > Content-Type: text/plain; charset="gb18030"
> >
> > Hey,guys
> >
> > I am learning to use HOL4. Here are some questions about my proving:
> >
> >
> >
> > g`!p q:bool list l:num list. (LENGTH p = LENGTH q) ==> (LENGTH (cx l p
> q) = LENGTH p) `;
> >
> > e (Induct_on `l`);
> >
> > e (RW_TAC list_ss [cx_defn]);
> >
> > - e (RW_TAC list_ss [cx_defn]);
> >
> > OK..
> >
> > 1 subgoal:
> >
> > > val it =
> >
> >
> >
> > LENGTH (DROP h (cx l q p)) +
> >
> > LENGTH (TAKE h (cx l p q)) =
> >
> > LENGTH q
> >
> > ------------------------------------
> >
> > 0. !p q.
> >
> > (LENGTH p = LENGTH q) ==> (LENGTH (cx l p q) = LENGTH p)
> >
> > 1. LENGTH p = LENGTH q
> >
> > : proof
> >
> >
> >
> > The definition of ?cx? is following:
> >
> >
> >
> > |- (!q p. cx [] p q = p) /\
> >
> > !v5 v4 q p.
> >
> > cx (v4::v5) p q =
> >
> > TAKE (HD (v4::v5)) (cx (TL (v4::v5)) p q) ++
> >
> > DROP (HD (v4::v5)) (cx (TL (v4::v5)) q p) : thm
> >
> >
> >
> > Where, ?TAKE? is in listtheory in HOL4. It means that get firs n
> elements, ?DROP? is in listtheory in HOL4. It means that get after n
> elements,
> >
> >
> >
> > I have proved that ?!p q:bool list n:num. (LENGTH p = LENGTH q) ==>
> (LENGTH (DROP n q) + LENGTH (TAKE n p) = LENGTH q)?, named
> ?TAKE_DROP_LENGTH?.
> >
> >
> >
> > But I can?t prove the initial goal g`!p q:bool list l:num list. (LENGTH
> p = LENGTH q) ==> (LENGTH (cx l p q) = LENGTH p) `. I think that, the
> problem is that in the goal the form is ?DROP h (cx l q p)?, but the actual
> form is ?DROP h l?, where the format of ?(cx l q p)? is not equal to ?l?.
> But I can?t find a good transform between them.
> >
> >
> >
> > Could anyone give me some advices?
> >
> > Thank you!
> > -------------- next part --------------
> > An HTML attachment was scrubbed...
> >
> > ------------------------------
> >
> > Message: 2
> > Date: Mon, 29 Feb 2016 00:49:29 +1100
> > From: Jeremy Dawson <jeremy.daw...@anu.edu.au>
> > Subject: Re: [Hol-info] How to transform list format from "(cx l q p)"
> > to "l"
> > To: <hol-info@lists.sourceforge.net>
> > Message-ID: <56d2fae9.2080...@anu.edu.au>
> > Content-Type: text/plain; charset="windows-1252"; format=flowed
> >
> >
> > It might be easier to avoid using TAKE_DROP_LENGTH
> > but instead try to simplify your subgoal using
> > LENGTH_TAKE_EQ and LENGTH_DROP
> >
> > Then I think you'll have to instantiate your subgoal 0 once with p,q
> > and once with q,p
> >
> > Cheers,
> >
> > Jeremy
> >
> > On 28/02/16 22:48, Ada wrote:
> > > Hey,guys
> > >
> > > I am learning to use HOL4. Here are some questions about my proving:
> > >
> > > g`!p q:bool list l:num list. (LENGTH p = LENGTH q) ==> (LENGTH (cx l p
> > > q) = LENGTH p) `;
> > >
> > > e (Induct_on `l`);
> > >
> > > e (RW_TAC list_ss [cx_defn]);
> > >
> > > - e (RW_TAC list_ss [cx_defn]);
> > >
> > > OK..
> > >
> > > 1 subgoal:
> > >
> > >> val it =
> > >
> > > LENGTH (DROP h (cx l q p)) +
> > >
> > > LENGTH (TAKE h (cx l p q)) =
> > >
> > > LENGTH q
> > >
> > > ------------------------------------
> > >
> > > 0.!p q.
> > >
> > > (LENGTH p = LENGTH q) ==> (LENGTH (cx l p q) = LENGTH p)
> > >
> > > 1.LENGTH p = LENGTH q
> > >
> > > : proof
> > >
> > > The definition of ?cx? is following:
> > >
> > > |- (!q p. cx [] p q = p) /\
> > >
> > > !v5 v4 q p.
> > >
> > > cx (v4::v5) p q =
> > >
> > > TAKE (HD (v4::v5)) (cx (TL (v4::v5)) p q) ++
> > >
> > > DROP (HD (v4::v5)) (cx (TL (v4::v5)) q p) : thm
> > >
> > > Where,?TAKE? is in listtheory in HOL4. It means that get firs n
> > > elements,?DROP? is in listtheory in HOL4. It means that get after n
> > > elements,
> > >
> > > I have proved that ?!p q:bool list n:num. (LENGTH p = LENGTH q) ==>
> > > (LENGTH (DROP n q) + LENGTH (TAKE n p) = LENGTH q)?, named
> > > ?TAKE_DROP_LENGTH?.
> > >
> > > But I can?t prove the initial goal g`!p q:bool list l:num list. (LENGTH
> > > p = LENGTH q) ==> (LENGTH (cx l p q) = LENGTH p) `. I think that, the
> > > problem is that in the goal the form is ?DROP h (cx l q p)?, but the
> > > actual form is ?DROP h l?, where the format of ?(cx l q p)? is not
> equal
> > > to ?l?. But I can?t find a good transform between them.
> > >
> > > Could anyone give me some advices?
> > >
> > > Thank you!
> > >
> > >
> > >
> > >
> ------------------------------------------------------------------------------
> > > Site24x7 APM Insight: Get Deep Visibility into Application Performance
> > > APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
> > > Monitor end-to-end web transactions and take corrective actions now
> > > Troubleshoot faster and improve end-user experience. Signup Now!
> > > http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140
> > >
> > >
> > >
> > > _______________________________________________
> > > hol-info mailing list
> > > hol-info@lists.sourceforge.net
> > > https://lists.sourceforge.net/lists/listinfo/hol-info
> > >
>
>
>
>
> ------------------------------
>
> Message: 2
> Date: Mon, 29 Feb 2016 23:30:30 +0000
> From: Michael Norrish <michael.norr...@nicta.com.au>
> Subject: Re: [Hol-info] Existential quantifier length
> To: hol-info <hol-info@lists.sourceforge.net>
> Message-ID: <e632870e-78db-4885-bbe8-282d2d6a1...@nicta.com.au>
> Content-Type: text/plain; charset="us-ascii"
>
> I agree: your theorem is hard to prove because you don't have enough
> information about FA etc. Can you prove that
>
> mux_list_imp a b sel y ==> (LENGTH y = something)
>
> If you can't, why not adjust mux_list_imp's definition so that you can?
> Similarly, it would seem reasonable to have the same property be true of
> the _spec version.
>
> Michael
>
> On 25 Feb 2016, at 20:53, Sumayya Shiraz <sumayya.shi...@seecs.edu.pk
> <mailto:sumayya.shi...@seecs.edu.pk>> wrote:
>
>
> Dear all
>
> Is it possible to specify length of bool list of the existential
> quantifier.
>
> I have following proof
>
> (?FA FB FC.
>
> mux_list_imp (TL (num_BV_f (SUC (LENGTH y)) (BV_n (not_0 a) + 1)))
> a F FA /\
>
> mux_list_imp (TL (num_BV_f (SUC (LENGTH y)) (BV_n (not_0 b) + 1)))
> b F FB /\
>
> mux_list_imp (TL (num_BV_f (SUC (LENGTH y)) (BV_n (not_0 c) + 1)))
> c F FC /\
>
> Adder_imp_n (LENGTH y + LENGTH y)
>
> (num_BV_f (LENGTH FA + LENGTH FB) (BV_n FA * BV_n FB))
>
> (make_list_F (LENGTH y) ++ FC) F y co) <=>
>
> (co :: y =
>
> (num_BV_f (SUC (LENGTH y + LENGTH y)) (BV_n a * BV_n b + BV_n c)))
>
> ------------------------------------
>
> 0. LENGTH a = LENGTH y
>
> 1. LENGTH b = LENGTH y
>
> 2. LENGTH c = LENGTH y
>
> 3. !n a.
>
> num_BV_f (SUC n) a =
>
> HD (num_BV_f (SUC n) a)::TL (num_BV_f (SUC n) a)
>
> : proof
>
>
> In above code, i want to apply the verified theorem
>
> mux_list_thm;
> > val it =
> |- !a b sel y.
> (LENGTH b = LENGTH a) /\ (LENGTH y = LENGTH a) ==>
> (mux_list_imp a b sel y <=> mux_list_spec a b sel y) : thm
>
> Now the problem is that i dont know length of FA. FB and FC in the above
> goal to apply the mux_lixt_thm.
> How can i find or describe its length and apply the above theorem to
> simplify my goal
>
> kindly reply me soon.
> thanks a lot
>
> ------------------------------------------------------------------------------
> Site24x7 APM Insight: Get Deep Visibility into Application Performance
> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
> Monitor end-to-end web transactions and take corrective actions now
> Troubleshoot faster and improve end-user experience. Signup Now!
>
> http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140_______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
> ________________________________
>
> The information in this e-mail may be confidential and subject to legal
> professional privilege and/or copyright. National ICT Australia Limited
> accepts no liability for any damage caused by this email or its attachments.
> -------------- next part --------------
> An HTML attachment was scrubbed...
>
> ------------------------------
>
> Message: 3
> Date: Tue, 1 Mar 2016 14:51:01 +0100
> From: Veelasha <veelasha2...@gmail.com>
> Subject: [Hol-info] ? Summer School on Real-World Crypto and Privacy,
> June 5-10, Croatia
> To: undisclosed-recipients:;
> Message-ID:
> <CAPYFFjpOzZEVPqvDLzKfiR=z0Kv=Hrn9Tua9v3=_nemeghl...@mail.gmail.com>
> Content-Type: text/plain; charset="utf-8"
>
> [Apologies to those who receive multiple copies of this announcement]
>
>
> ****************************************************************************
>
>
> ? ?
> ? ?
> Call for Participation
>
>
> ??
> Summer School on Real-World Crypto and Privacy
>
>
> ? ?
> June 5-10, 2016, Sibenik (Croatia)
>
> http://summerschool-croatia.cs.ru.nl/2016/
>
>
> ****************************************************************************
>
> After the big success of the Summer School on Real-World Crypto and
> Privacy in 2015, we are planning the next edition for June 5-10, 2016 in
> Sibenik, Croatia.
>
> The purpose of the School is to attract not only Ph.D. students and
> postdocs, but also people from industry who are interested in recent
> developments in cryptography. The program will start with 2 days of
> plenary talks followed by an excursion to the Kornati National Park on
> June 8. The last 2 days will include more advanced talks on recent
> topics organized in two parallel sessions.
>
> List of confirmed invited speakers:
>
> - Lejla Batina, Radboud University, The Netherlands and KU Leuven, Belgium
> - Gilles Barthe, IMDEA Software Institute, Spain
> - David Basin, ETH Zurich, Switzerland
> - Daniel J. Bernstein, Technische Universiteit Eindhoven, The
> Netherlands and University of Illinois at Chicago, USA
> - Joppe Bos, NXP Semiconductors, Belgium
> - Srdjan Capkun, ETH Zurich, Switzerland
> - Joan Daemen, STMicroelectronics and Radboud University
> - Claudia Diaz, KU Leuven, Belgium
> - Roger Dingledine, The Tor Project, USA
> - Rachel Greenstadt, Drexel University, USA
> - J. Alex Halderman, University of Michigan, USA
> - Nadia Heninger, University of Pennsylvania, USA
> - Ari Juels, Cornell University, USA
> - Tanja Lange, Technische Universiteit Eindhoven, The Netherlands
> - Nele Mentens, KU Leuven, Belgium
> - Guevara Noubir, Northeastern University, USA
> - Kenny Paterson, RHUL, UK
> - Adrian Perrig, ETH Zurich, Switzerland
> - Bart Preneel, KU Leuven, Belgium
> - Phillip Rogaway, University of California, Davis, USA
> - Peter Schwabe, Radboud University, The Netherlands
> - Benjamin Smith, INRIA and ?cole Polytechnique, France
> - Martijn Stam, University of Bristol, UK
> - Fran?ois-Xavier Standaert, Universit? catholique de Louvain, Belgium
> - Carmela Troncoso, IMDEA Software Institute, Spain
> - Ingrid Verbauwhede, KU Leuven, Belgium
>
>
> Early registration is open until May 01.
> Stipends for students are also available.
>
> For more information, see http://summerschool-croatia.cs.ru.nl/2016/
> -------------- next part --------------
> An HTML attachment was scrubbed...
>
> ------------------------------
>
>
> ------------------------------------------------------------------------------
> Site24x7 APM Insight: Get Deep Visibility into Application Performance
> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
> Monitor end-to-end web transactions and take corrective actions now
> Troubleshoot faster and improve end-user experience. Signup Now!
> http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140
>
> ------------------------------
>
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
> End of hol-info Digest, Vol 118, Issue 1
> ****************************************
>
>
> ------------------------------------------------------------------------------
>
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
Transform Data into Opportunity.
Accelerate data analysis in your applications with
Intel Data Analytics Acceleration Library.
Click to learn more.
http://makebettercode.com/inteldaal-eval
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
