Re: [Hol-info] Holmake Problem

[Anthony Fox]

As an alternative workaround, you could edit the files in the 
src/floating-point directory to remove the dependency on PackRealBig. For 
example, you could try commenting out the lines

   val floatToReal : term -> real
   val wordToReal  : term -> real
   val realToFloat : real -> term
   val realToWord  : real -> term
   val native_ty   : hol_type

in binary_ieeeSyntax.sig, and the associated code at the end of 
binary_ieeeSyntax.sml. It’s likely that you would also have to remove the files 
binary_ieeeLib.{sml,sig}, as this depends on that code.

[This code supports evaluation (using EVAL) of floating-point operations via 
the native Real.real type. This gives you an “oracle” theorem with the tag 
“native_ieee”. By default this is turned off and evaluation uses Arbint 
instead, which gives you an untagged theorem - this is always the path that is 
used for non-native sizes. So a slightly cut-down version of binary_ieeeLib 
could be made to work under MoscowML.]

In any case, the ARM M0 model doesn’t actually have any floating-point - the 
dependency is there for other ISA models.

Anthony

> On 3 Dec 2015, at 23:35, Michael Norrish  wrote:
> 
> I guess you are using MoscowML (perhaps because you are on Windows).  Is this 
> right?
> 
> Unfortunately, the src/floating-point directory requires Poly/ML, and for the 
> moment that requires unix of some form.
> 
> If you want to use this directory, I'm afraid you must use Unix.  If you are 
> committed to a Windows machine, perhaps you can install Linux in a virtual 
> machine (VirtualBox, for example).
> 
> Michael
> 
> 
>> On 3 Dec 2015, at 21:23, Ali Abbassi  wrote:
>> 
>> Hello,
>> 
>> I am trying to Holmake some of the folders in examples folder (the ones 
>> related to ARM m0 processor), however, when I type ".../bin/Holmake -r", it 
>> requires machine_ieeeSyntax.ui, which I found the related sml file of that 
>> in "src/floating-point/" directory.
>> When I try to Holmake that, this error appears : "Cannot find file 
>> PackRealBig.ui", and I could not find the PackRealBig.sml in directories. I 
>> appreciate any kind of help.
>> 
>> Thanks in advance,
>> Ali


--
Go from Idea to Many App Stores Faster with Intel(R) XDK
Give your users amazing mobile app experiences with Intel(R) XDK.
Use one codebase in this all-in-one HTML5 development environment.
Design, debug & build mobile apps & 2D/3D high-impact games for multiple OSs.
http://pubads.g.doubleclick.net/gampad/clk?id=254741911&iu=/4140
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Tags: oracles, axioms

[Anthony Fox]

The axiom tag list only contains axioms that have been introduced within the 
“current theory segment”. All theorems from other theory segments (i.e. those 
previously stored to “disk”) will have an empty list of axioms, since they 
cannot have been derived using axioms from the current theory segment.

You can list all axioms introduced in ancestor theories with

List.map DB.axioms (Theory.ancestry "-“)

By contrast, oracle tags are sticky. The DISK_THM tag is used to show that a 
theorem has come from a stored theory, i.e. via export_theory.

So, if you have

val name = Theory.new_axiom (“name", ..)

in the current theory segment then (while that segment is still active) the 
“name” axiom tag will appear in all theorems derived using this axiom. However, 
once this theory is stored, only the existence of the axiom is recorded.

If you have

val name = Thm.mk_oracle_thm “name” (.., ..)

then the “name” oracle tag will always appear in the tags of all theorems 
derived with this theorem (even after storing the theorems to disk).



Things have recently become a bit more complicated with holyhammer, which uses 
special tags to keep track of all theorem dependencies. However, this 
information is not printed when showing the normal tags. For your example, you 
can see the connection with

> Tag.dep_of (Thm.tag boolTheory.AND_CLAUSES);
val it = DEP_SAVED (("bool", 51), [("bool", [0, 3, 26, 27, 39])]): Dep.dep

> Tag.dep_of (Thm.tag IMP_ANTISYM_AX);
val it = DEP_SAVED (("bool", 26), [("bool", [0, 4, 5, 13])]): Dep.dep

> Tag.dep_of (Thm.tag boolTheory.BOOL_CASES_AX);
val it = DEP_SAVED (("bool", 13), []): Dep.dep
>

i.e. theorem 51 (AND_CLAUSES) depends on theorem 26 (MP_ANTISYM_AX), which in 
turn depends on theorem 13 (BOOL_CASES_AX).

Anthony

> On 4 Dec 2015, at 13:44, Andrea Condoluci  wrote:
> 
> Hi all,
> 
> Let's consider any theorem that depends on the BOOL_CASES_AX. For example, 
> from the HOL Reference:
> 
> >  [AND_CLAUSES]  Theorem
> >
> >  [oracles: ] [axioms: BOOL_CASES_AX] []
> >  |- !t.
> >   (T /\ t <=> t) /\ (t /\ T <=> t) /\ (F /\ t <=> F) /\
> >   (t /\ F <=> F) /\ (t /\ t <=> t)
> 
> But if now I display in my HOL system the theorem, with the option "show_tags 
> := true", this is what I get:
> 
> >  val it = 
> >[oracles: DISK_THM] [axioms: ] []
> >|- ∀t.
> > (T ∧ t ⇔ t) ∧ (t ∧ T ⇔ t) ∧ (F ∧ t ⇔ F) ∧ (t ∧ F ⇔ F) ∧ (t ∧ t ⇔ t)
> 
> How comes the axiom is not displayed, and there is a "DISK_THM" oracle 
> instead?
> 
> Thank you,
> Andrea


--
Go from Idea to Many App Stores Faster with Intel(R) XDK
Give your users amazing mobile app experiences with Intel(R) XDK.
Use one codebase in this all-in-one HTML5 development environment.
Design, debug & build mobile apps & 2D/3D high-impact games for multiple OSs.
http://pubads.g.doubleclick.net/gampad/clk?id=254741911&iu=/4140
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Tags: oracles, axioms

[Anthony Fox]

This issue seems to be related to the fact that we had

val EXCLUDED_MIDDLE = save_thm(
  "EXCLUDED_MIDDLE”, ...)

followed by

val _ = save_thm("EXCLUDED_MIDDLE",EXCLUDED_MIDDLE)

in boolScript.sml.

This meant that the saved theorem “EXCLUDED_MIDDLE” (id 30) depended on an 
unsaved/overwritten theorem (id 29). NOT_CLAUSES also depended on id 29, so a 
lookup failed because this theorem wasn’t being saved with the theory. (The 
same sort of thing was happening throughout boolTheory.)

I’ve updated the script file to avoid instances of “val _ = save_thm”. This 
means that we now get

> boolTheory.NOT_CLAUSES |> Thm.tag |> Tag.dep_of |> Dep.depidl_of;
val it =
   [("bool", 25), ("bool", 26), ("bool", 27), ("bool", 29), ("bool", 46),
("bool", 47)]: Dep.depid list
> List.map hhWriter.thm_of_depid it
val it =
   [("TRUTH", |- T),
("IMP_ANTISYM_AX",
 |- ∀t1 t2. (t1 ⇒ t2) ⇒ (t2 ⇒ t1) ⇒ (t1 ⇔ t2)),
("FALSITY", |- ∀t. F ⇒ t),
("EXCLUDED_MIDDLE", |- ∀t. t ∨ ¬t),
("IMP_F", |- ∀t. (t ⇒ F) ⇒ ¬t),
("F_IMP", |- ∀t. ¬t ⇒ t ⇒ F)]:
   (string * thm) list

I’m not sure if it makes sense to think about exporting the theory in such a 
way that references to unsaved theorems are eliminated. Thibault Gauthier is 
better placed to discuss this issue.

Anthony

> On 6 Dec 2015, at 14:51, Andrea Condoluci  wrote:
> 
> I now have a problem w/ dependencies: some theorems depend on things that do 
> not appear to exist (?)
> For example:
> - boolTheory.NOT_CLAUSES |> Thm.tag |> Tag.dep_of |> Dep.depidl_of;
> > val it = [("bool", 0), ("bool", 6), ("bool", 26), ("bool", 27), ("bool", 
> > 29)]
> - hhWriter.thm_of_depid ("bool", 29);
> ! Uncaught exception: 
> ! HOL_ERR
> 
> Why this?
> 
> Andrea
> 


--
Go from Idea to Many App Stores Faster with Intel(R) XDK
Give your users amazing mobile app experiences with Intel(R) XDK.
Use one codebase in this all-in-one HTML5 development environment.
Design, debug & build mobile apps & 2D/3D high-impact games for multiple OSs.
http://pubads.g.doubleclick.net/gampad/clk?id=254741911&iu=/4140
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] About Binary Relations

[Anthony Fox]

Your original goal seemed to be just an instance of

pred_setTheory.SUBSET_REFL

  |- !s. s SUBSET s

Are you actually trying to prove:

!A. IMAGE FST (A CROSS A) SUBSET A

?

If so, you could have:

Q.prove(
  `!A. IMAGE FST (A CROSS A) SUBSET A`,
  simp [pred_setTheory.SUBSET_DEF]
  \\ metis_tac []
  )

However, it may be better to prove a lemma for this, as it could be useful 
elsewhere. For example:

val image_fst_cross = Q.prove(
  `!A B. IMAGE FST (A CROSS B) = if B = EMPTY then EMPTY else A`,
  rw [pred_setTheory.EXTENSION, pred_setTheory.IN_CROSS,
  pred_setTheory.IN_IMAGE]
  \\ eq_tac
  \\ rw [] >- metis_tac []
  \\ fs []
  \\ qexists_tac `(x, x')`
  \\ simp []
  )

(There’s probably a nicer way of proving the above lemma.)

With this, the following works

Q.prove(
  `!A. IMAGE FST (A CROSS A) SUBSET A`, rw [image_fst_cross])

Anthony

> On 5 Feb 2016, at 07:19, Ramana Kumar  wrote:
> 
> What's the problem/what is going wrong?
> 
> On 5 February 2016 at 17:48, Nadeem Iqbal  wrote:
> Yes, I want the set of first components of the pairs. I replaced S with A, 
> and used IMAGE FST (A CROSS A), but the problem is not solved.
> 
> 
> 
> On Fri, Feb 5, 2016 at 8:52 AM, Ramana Kumar  
> wrote:
> ``S CROSS S`` is a set of pairs. Although ``S`` is usually parsed as a 
> constant, so you might want to use a different letter, or use Parse.hide"S".
> 
> Do you want the set of first components of the pairs? That would be ``IMAGE 
> FST (S CROSS S)``, and should be equal to ``S``.
> 
> On 5 February 2016 at 14:42, Nadeem Iqbal  wrote:
> Hi,
> 
> Dear All,
> 
> I am working in HOL4. I want to extract the domain of the set of binary 
> relations.
> For example, when I tried this goal,
> 
> g `! S. (FST (S CROSS S)) SUBSET (FST (S CROSS S))`;
> 
> It could not run. Can any one guide me?
> 
> Regards,
> 
> Nadeem Iqbal
> HoD School of Computing and Information Sciences,
> Imperial College of Business Studies,
> Lahore, Pakistan.
> 
> 
> --
> 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
> 
> 
> 
> 
> --
> 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


--
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

Re: [Hol-info] word problem

[Anthony Fox]

Looks false to me, since `n2w a` can represent a negative number. The 
assumption `0 < a` doesn’t prevent this, you’d need `0w < n2w a` instead. Also, 
I think you’d need `a` to be strictly less than `m`. For example:

Q.prove(
  `0w < (n2w m : 'a word) /\ 0w < (n2w a : 'a word) /\ a < m /\
   m < dimword(:'a) ==> (n2w m - n2w a :'a word) < n2w m`,
  rpt strip_tac
  \\ match_mp_tac wordsTheory.WORD_LT_SUB_UPPER
  \\ lfs [wordsTheory.word_lt_n2w]
  )

The original formulation makes more sense for unsigned less than? For example:

Q.prove(
  `0 < a /\ a <= m /\ m < dimword(:'a) ==> (n2w m - n2w a :'a word) <+ n2w m`,
  rw_tac std_ss [GSYM wordsTheory.n2w_sub]
  \\ simp [wordsTheory.WORD_LO]
  )

Anthony

> On 9 Feb 2016, at 00:28, Ramana Kumar  wrote:
> 
> Scott informed me that it is likely false (e.g., take m = 1 and a = 2). I can 
> add additional assumptions that may help, though.
> 
> Alternatively, I have a variant of the problem that looks like this:
> 
> 0. m < dimword (:'a)
> 1. a <= m
> 2. 0 < m
> 3. 0 < a
> 
> n2w m - n2w a < n2w m
> 
> That one seems more likely to be true. But how to prove it?
> 
> On 9 February 2016 at 10:02, Ramana Kumar  wrote:
> Hi,
> 
> Does anyone know whether the following goal is true or false?
> 
> How would you prove it?
> 
> If it's false, under what reasonable additional assumptions would it be true?
> 
>   0.  m < dimword (:α)
>   1.  m < a
>   2.  0 < m
> 
> n2w m − n2w a < n2w m
> 
> Cheers,
> Ramana
> 
> --
> 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


--
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

Re: [Hol-info] How to transform list format from "(cx l q p)" to "l"

[Anthony Fox]

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";;
> Date:  Mon, Feb 29, 2016 01:08 PM
> To:  "hol-info";
> 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 " 
> Subject: [Hol-info] How to transform list format from "(cx l q p)" to
> "l"
> To: " hol-info " 
> Message-ID: 
> 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 
> Subject: Re: [Hol-info] How to transform list format from "(cx l q p)"
> to "l"
> To: 
> 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 

Re: [Hol-info] Problem installing HOL 4

[Anthony Fox]

You may find that the release version of PolyML 5.6 doesn’t work with the 
development version of HOL4. If you experience any problems then try the fixes 
branch of Poly/ML:

https://github.com/polyml/polyml/tree/fixes-5.6

For example, you can do

$ git checkout fixes-5.6

after cloning the Poly/ML repository.

Anthony

> On 24 May 2016, at 09:47, Ramana Kumar  wrote:
> 
> PolyML 5.6 is supported by the development version of HOL4 (i.e., the head of 
> the master branch), and has been for a while.
> 
> On 24 May 2016 at 18:39, Chun Tian (binghe)  wrote:
> Hi all,
> 
> But still, PolyML 5.6 is not supported yet, right? I have to use latest Poly 
> ML 5.5.x to build HOL4 (Git master) on Mac OS X.
> 
> Regards,
> 
> Chun Tian (binghe)
> University of Bologna
> 
> On 24 May 2016 at 07:29, Thomas Tuerk  wrote:
> Hi Michael,
> 
> thanks. That did the trick. The new libraries were installed there, but
> the old ones were still in there causing trouble. Anyhow, purging the
> old ones solved the issue.
> 
> Many thanks
> 
> Thomas
> 
> On 24/05/16 07:23, Michael Norrish wrote:
> > It looks to me as if you have a very old libpoly installed in 
> > /usr/local/lib (or perhaps somewhere else on your LD_LIBRARY_PATH).  I'd 
> > guess that you need to purge those files (and make sure that the 5.6 
> > library files end up there as well).
> >
> > Michael
> >
> >> On 24 May 2016, at 14:50, Thomas Tuerk  wrote:
> >>
> >> Hi all,
> >>
> >> I have a problem installing HOL 4, which is puzzling me. It would be
> >> great if someone had a idea how to help me.
> >>
> >> I wanted to update my HOL 4 installation. I had an old PolyML installed
> >> and got the error message that at least version 5.5.1 is needed. So, I
> >> installed the latest version 5.6 and then ran
> >>
> >> poly < tools/smart-configure.sml
> >>
> >> I got a strange error message. I also tried with versions 5.5.2, 5.5.1
> >> with same effect:
> >>
> >> -
> >> Poly/ML 5.5.1 Release
> >>
> >> HOL smart configuration.
> >>
> >> Determining configuration parameters: holdir OS poly polymllibdir
> >> OS: linux
> >> poly:   /usr/local/bin/poly
> >> polyc:  /usr/local/bin/polyc
> >> polymllibdir:   /usr/local/lib
> >> holdir: /home/thtuerk/HOL
> >> DOT_PATH:   /usr/bin/dot
> >>
> >> Configuration will begin with above values.  If they are wrong
> >> press Control-C.
> >>
> >> Will continue in 1 seconds.
> >>
> >> Loading system specific functions
> >> Compiling system specific functions (sml)
> >> Beginning configuration.
> >> Making mllex
> >> Making mlyacc
> >>
> >> The exported object file has version 5.51 but this library supports
> >> 5.10-5.50
> >> Failed to make mlyacc
> >> -
> >>
> >> Does anyone have an idea library this error message is about? I briefly
> >> started debugging, but have not put much time into it yet? Has anyone
> >> encountered this problem before.
> >>
> >> Best
> >>
> >> Thomas Tuerk
> >>
> >> --
> >> Mobile security can be enabling, not merely restricting. Employees who
> >> bring their own devices (BYOD) to work are irked by the imposition of MDM
> >> restrictions. Mobile Device Manager Plus allows you to control only the
> >> apps on BYO-devices by containerizing them, leaving personal data 
> >> untouched!
> >> https://ad.doubleclick.net/ddm/clk/304595813;131938128;j
> >> ___
> >> 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.
> >
> 
> --
> Mobile security can be enabling, not merely restricting. Employees who
> bring their own devices (BYOD) to work are irked by the imposition of MDM
> restrictions. Mobile Device Manager Plus allows you to control only the
> apps on BYO-devices by containerizing them, leaving personal data untouched!
> https://ad.doubleclick.net/ddm/clk/304595813;131938128;j
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
> 
> 
> 
> -- 
> Chun Tian (binghe)
> 
> --
> Mobile security can be enabling, not merely restricting. Employees who
> bring their own devices (BYOD) to work are irked by the imposition of MDM
> restrictions. Mobile Device Manager Plus allows you to control only the
> apps on BYO-devices by containerizing them, 

Re: [Hol-info] Translating HOL4 function to SML

[Anthony Fox]

A starting point might be to use the function real_to_arbrat in binary_ieeeLib.

https://github.com/HOL-Theorem-Prover/HOL/tree/master/src/floating-point

For example, the following is one method to get a result:

fun arbrat_to_math_real x =
  Real./ (Real.fromInt (Arbint.toInt (Arbrat.numerator x)),
  Real.fromInt (Arbnum.toInt (Arbrat.denominator x)))

val real_to_math_real = arbrat_to_math_real o real_to_arbrat

Math.exp (real_to_math_real ``0.4``)
> val it = 1.491824698: real

Anthony

> On 27 May 2016, at 07:56, Michael Norrish  
> wrote:
> 
> It depends on what term-structure you expect to see as the argument to exp.  
> If, for example, you were only going to see integer literals there, you could 
> just use realSyntax.int_of_term:
> 
> > realSyntax.int_of_term ``4:real``;
> val it = 4i: Arbint.int
> > realSyntax.int_of_term ``-5:real``;
> val it = -5i: Arbint.int
> 
> But if you expected to see fractions there too, you would have to combine the 
> above with realSyntax.dest_div:
> 
> > realSyntax.dest_div ``4 / 5 : real``;
> val it = (``4``, ``5``): term * term
> 
> Note that decimal numbers are really fractions:
> 
> > realSyntax.dest_div ``3.14``;
> val it = (``314``, ``100``): term * term
> 
> It would be nice to combine all of the above to give a 
> 
>   realLit_to_rat 
> 
> function of type term -> Arbrat.rat.
> 
> You could presumably special-case other interesting constants like pi and e, 
> though you'd have to then decide what precision you wanted in your rational 
> output. Note also that Arbrat.rat is not the same type as the SML 
> implementation's real type. 
> 
> Michael
> 
>> On 27 May 2016, at 15:14, Waqar Ahmad <12phdwah...@seecs.edu.pk 
>> > wrote:
>> 
>> Hi all,
>> 
>> I am trying to translate some defined HOL4 functions to their equivalent 
>> functions in SML. For instance, there is a function "exp ": real->real in a 
>> HOL4 'transcTheory' and I want to compute it using a similar SML function 
>> `Math.exp`.
>> 
>> So, I have written a translator function as follows:
>> 
>> fun sml_of_hol_real_exp t =
>> let val failstring = "Symbolic expression could not be translated in a 
>> number" in
>> if fst (dest_comb t) = ``exp:real->real`` then
>>   
>> Math.exp  (snd (dest_comb t))
>>else failwith failstring
>>   end;
>> 
>> A possible usage of above function can be  sml_of_hol_real_exp ``exp 0.4``;
>> 
>> Now, I need a kind of operator in place of   that can give an 
>> argument to Math.exp function for computation... Can anybody have an idea 
>> about this?
>> 
>> -- 
>> Thanks and best regards,
>> 
>> Waqar Ahmed
>> 
>> 
>> --
>> What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
>> patterns at an interface-level. Reveals which users, apps, and protocols are 
>> consuming the most bandwidth. Provides multi-vendor support for NetFlow, 
>> J-Flow, sFlow and other flows. Make informed decisions using capacity 
>> planning 
>> reports.https://ad.doubleclick.net/ddm/clk/305295220;132659582;e___
>>  
>> 
>> 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.
> --
> What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
> patterns at an interface-level. Reveals which users, apps, and protocols are 
> consuming the most bandwidth. Provides multi-vendor support for NetFlow, 
> J-Flow, sFlow and other flows. Make informed decisions using capacity 
> planning reports. 
> https://ad.doubleclick.net/ddm/clk/305295220;132659582;e___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info

--
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are 
consuming the most bandwidth. Provides multi-vendor support for NetFlow, 
J-Flow, sFlow and other flows. Make informed decisions using capacity 
planning reports. https://ad.doubleclick.net/ddm/clk/305295220;132659582;e___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Opening theories without output

[Anthony Fox]

I use Ramana’s HOL mode for Vim, shortcut “hl”. That makes use of

  HOL_Interactive.toggle_quietdec

For example, you can do

> HOL_Interactive.toggle_quietdec();
> open prim_recTheory pairTheory listTheory rich_listTheory;
> open ...
> HOL_Interactive.toggle_quietdec();

The advantage of the Vim shortcut is that it also loads all of the theories 
beforehand. I believe there is something similar for the Emacs mode.

Anthony

> On 31 May 2016, at 16:39, Peter Vincent Homeier 
>  wrote:
> 
> Very often I wish to work in an existing theory script file which begins with 
> a number of files being opened, e.g., 
> 
> open prim_recTheory pairTheory listTheory rich_listTheory;
> open combinTheory;
> open listLib;
> open pred_setTheory pred_setLib;
> open numTheory;
> open numLib;
> open arithmeticTheory;
> . . .
> 
> But for theories that contain hundreds or thousands of theorems, this prints 
> out each theorem in full, which can take tens of minutes of my time while I 
> am waiting to begin work, and theorems that I already know are just spilling 
> by.
> 
> Clearly this is not practical. What do other people do to speed this up, so 
> you can get into your theory and start work? Is there any way to enter the 
> defined names of an existing theory, like arithmeticTheory, to the current ML 
> session without printing all of them, which is what takes such a long time? 
> I'd like to use something like
> 
> open_silently arithmeticTheory;
> 
> which would be functionally equivalent to "open", but would print none of the 
> values it is introducing.
> 
> What do people do to get around this problem? Or do they just live with it? 
> Would "open_silently" have to be added to the Standard ML implementation?
> 
> Peter
> 
> 
> "In Your majesty ride prosperously 
> because of truth, humility, and righteousness;
> and Your right hand shall teach You awesome things." (Psalm 45:4)
> --
> What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
> patterns at an interface-level. Reveals which users, apps, and protocols are 
> consuming the most bandwidth. Provides multi-vendor support for NetFlow, 
> J-Flow, sFlow and other flows. Make informed decisions using capacity 
> planning reports. 
> https://ad.doubleclick.net/ddm/clk/305295220;132659582;e___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info


--
What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic
patterns at an interface-level. Reveals which users, apps, and protocols are 
consuming the most bandwidth. Provides multi-vendor support for NetFlow, 
J-Flow, sFlow and other flows. Make informed decisions using capacity 
planning reports. https://ad.doubleclick.net/ddm/clk/305295220;132659582;e
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Instantiating type variables

[Anthony Fox]

The theorem float_add_relative is of the form

  ∀(a :(τ, χ) float) (b :(τ, χ) float). ..

and

  SPEC ``(fp64_to_float v):(52, 11) float``  float_add_relative

will only try to specialise values and not types. What you need is Drule.ISPEC, 
i.e.

  Drule.ISPEC ``fp64_to_float v : (52, 11) float`` float_add_relative

Alternatively you could use SPEC after manually using Thm.INST_TYPE to 
instantiate the type of float_add_relative.

Anthony

> On 8 Sep 2017, at 08:01, Heiko Becker  wrote:
> 
> Hello everyone,
> 
> I am trying to prove a theorem using the IEEE floating-point formalizations 
> of HOL4. In a proof, I need to apply the lemma 
> lift_ieeeTheory.float_add_relative. However neither match_mp_tac nor irule 
> are able to unify the lemma with the conclusion I want to show.
> 
> I tried instantiating variables by hand to see what happens. Trying the below 
> code fails with an error complaining about mismatched types in the conclusion:
> 
> SPEC ``(fp64_to_float v):(52, 11) float``  float_add_relative
> 
> 
> Can someone tell me what I a doing wrong in this case, since (52,11) float 
> should be unifiable with (τ, χ) float.
> 
> 
> 
> Thanks,
> 
> Heiko
> 
> 
> 
> 
> --
> 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

Re: [Hol-info] EVAL not EVALing as expected

[Anthony Fox]

Your example can be handled with a bit of simplification.  For  
example, if you add


- open computeLib
- add_conv(``$COND:bool -> 'a -> 'a -> 'a``, 3, SIMP_CONV bool_ss [])  
the_compset;


you get

- EVAL ``update (update not T T) F F``;
> val it = |- update (update not T T) F F = (\z. z) : thm

However, it may be best to exclude the update definition from  
the_compset and write custom conversions for simplifying/evaluating  
update terms.


You can exclude a definition with:

- computeLib.auto_import_definitions := false;
- Define `update f x y = \z. if z=x then y else (f z)`;
- computeLib.auto_import_definitions := true;

You'll then need something like:

- add_conv(``$update:('a -> 'b) -> 'a -> 'b -> 'a -> 'b``, 3,  
SORT_UPDATE) the_compset;
- add_conv(``$update:('a -> 'b) -> 'a -> 'b -> 'a -> 'b``, 4,  
EVAL_UPDATE) the_compset;


SORT_UPDATE will depend on the finite domain and you could use  
CNV_CONV with some suitable rewrites.  In your example, I would aim  
for something like:


- EVAL ``update (update not T T) F F```;
>  |- update (update not T T) F F =  update (update not T T) F F
- EVAL ``update (update not F F) T T```;
>  |- update (update not F F) T T =  update (update not T T) F F
- EVAL ``(update (update not T T) F F) T```;
>  |- (update (update not T T) F F) T = T

Some examples of rewrites for sorting updates can be found in $HOLDIR/ 
examples/ARM/v4T/updateScript.sml.  These are used in arm_evalLib.sml.


Anthony Fox.

On 16 Nov 2007, at 16:01, Bingham, Jesse D wrote:

Thanks to Konrad and Michael for their responses to my previous  
question.


Here's another one.  I'm not sure if it is a question about EVAL or  
a pretty printing question.  If I EVAL a function that has a finite  
domain (especially a small one), I would like the function to be  
represented as a set of pairs.  However, EVAL tends to give  
unnecessarily complicated terms when dealing with functions.  For  
example,


Define `update f x y = \z. if z=x then y else (f z)`;
Define `not x = ~x`;

Now let's use update to morph not into the identity on bools.

EVAL ``update (update not T T) F F``;

I would like this to print the bool identity  in some succinct  
manner (something along the lines of [T |-> T, F |-> F])
Instead, EVAL gives the function as a nested if-then-else lambda  
expression:


 (\z. (if ~z then F else (if z then T else ~z)))

Things get worse if there are more updates.  I tried using  
finite_maps and |+ instead of update and got similar results,  
modulo notation.  How do I get EVAL to crunch a function with a  
finite domains down to a set of pairs?

Thanks

-Jesse
-- 
---

This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2005.
http://clk.atdmt.com/MRT/go/vse012070mrt/direct/01/ 
___

hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info


-
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2005.
http://clk.atdmt.com/MRT/go/vse012070mrt/direct/01/___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] HOL newbie question on lemma rewrites

[Anthony Fox]

The theorem n2w_w2n

|- !w. n2w (w2n w) = w

cannot be applied in

``n2w (w2n w) = v``

when w and v do not have the same length, which is the case in your  
goal.

For proving things about ``a @@ b``, I would recommend using the  
latest HOL snapshot.  I'm assuming that you're using the latest  
official release?   (The type ``:i2`` has since become ``:2``.)

I'm not sure what your original goal is but it may be provable using  
tools located in wordsLib.  For example:

- wordsLib.WORD_DECIDE ``!cv:word2. (cv = 0w) ==> (cv @@ cv =  
0w:word4)``;
 > val it = |- !cv. (cv = 0w) ==> (cv @@ cv = 0w) : thm

- Q.prove( `!cv:word2. (cv = 0w) ==> (cv @@ cv = 0w:word4)`,
   SRW_TAC [wordsLib.WORD_EXTRACT_ss] []);
 > val it = |- !cv. (cv = 0w) ==> (cv @@ cv = 0w) : thm

These tools work best when word lengths are ground i.e. when goal's  
don't contain an ``:'a word`` (``:bool['a]``).

Anthony.

On 29 Dec 2008, at 08:27, Nikhil Kikkeri wrote:

> Hi,
>
> My current proof obligation looks something like this
>
> 1 subgoal:
>> val it =
>w2n (n2w (w2n (cv << dimindex (:i2) !! cv))) = 0
>
>  0.  (1 -- 1) add_in = 0w
>  1.  (0 -- 0) add_in = 0w
>  2.  Abbrev (cv = w2w 0w)
> : goalstack
>
>
> Now I would assume that doing something like
>
> e (PURE_REWRITE_TAC[n2w_w2n]);
>
> should reduce the goal to
>
> w2n (cv << dimindex (:i2) !! cv) = 0
> ---
>  0.  (1 -- 1) add_in = 0w
>  1.  (0 -- 0) add_in = 0w
>  2.  Abbrev (cv = w2w 0w)
> : goalstack
>
> Now if I am seeing things correctly, the rewrite should happen  
> without a
> hitch. However that has not been the case, and that is gating me from
> discharging this goal, which looks trivial.
>
> Thank you in advance,
>
> Nikhil
>
> --
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info


--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] convert an SML int variable into a word32 term?

[Anthony Fox]

The second parameter is the word length.  For example:

wordsSyntax.mk_word (Arbnum.fromInt 0xA, Arbnum.fromInt 32)

For convenience, there is also

wordsSyntax.mk_wordi (Arbnum.fromInt 0xA, 32)

and

wordsSyntax.mk_wordii (0xA, 32)

Be aware that Mosml integers are 31 bits wide.  For example:

- mk_wordii (0x, 32);
! Toplevel input:
! mk_wordii (0x, 32);
!^^
! Lexical error: integer constant is too large.

However this is okay with PolyML:

 > mk_wordii (0x, 32);
val it = ``4294967295w`` : Abbrev.term

Anthony.

for the cases when the word length and value are integers.

On 15 Apr 2009, at 20:46, Lu Zhao wrote:

> Hey,
>
> Suppose there is a variable in SML:
>
> val v = 0xA
>
> How can I get a term which has the value of "v" in word32? I found
> mk_word in wordsSyntax, but I have no idea what the second parameter
> should be (I guess the first might be v)?
>
> Thanks.
> Lu


--
This SF.net email is sponsored by:
High Quality Requirements in a Collaborative Environment.
Download a free trial of Rational Requirements Composer Now!
http://p.sf.net/sfu/www-ibm-com
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] word inequality tac?

[Anthony Fox]

One option is

simpLib.SIMP_PROVE (srw_ss()++wordsLib.WORD_ARITH_EQ_ss) []
  ``(p:bool[32]) + 0x4w <> p + 0x8w``;

Anthony.

On 12 Dec 2009, at 00:21, Lu Zhao wrote:

> Hi,
> 
> I have an inequality proof:
> 
> ``(p:bool[32]) + 0x4w <> p + 0x8w``
> 
> How should I proceed to prove it?
> 
> Lu
> 
> 
> --
> Return on Information:
> Google Enterprise Search pays you back
> Get the facts.
> http://p.sf.net/sfu/google-dev2dev
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info


--
Return on Information:
Google Enterprise Search pays you back
Get the facts.
http://p.sf.net/sfu/google-dev2dev
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] HOL problem

[Anthony Fox]

You could use

Globals.max_print_depth := 10;

(try: help "max_print_depth").

You could also do

val _ = time defCNF.DEF_CNF_VECTOR_CONV ;

which will perform the computation, giving you the time, but then throw away 
the result.

Anthony.

On 11 Dec 2009, at 14:14, Khaza Anuarul Hoque wrote:

> I have a big file of DNF which has 500 clause, each clause has upto 50  
> literals. now i
> was trying to do the cnf conversion using HOL4 Kan4 release.
> 
> load "tautLib";
> open tautLib;
> load "defCNF";
> open defCNF;
> 
> time defCNF.DEF_CNF_VECTOR_CONV ;
> 
> Whenever i do this it returns me an exception "Ptetty Printer: out_of_memory".
> Seems like this is a problem because HOL is running out of memory  
> while printing the output on screen. So is there any way to do the  
> computation in background rather in printing on screen ?? All i need  
> is the time of that cnf computation, i dont need to see the output. I  
> am sure there is a way to do this... can anyone help me ?? Its more  
> than urgent
> 
> regards
> -- 
> Khaza Anuarul Hoque, B.Sc Engr
> M.A.Sc Student, Dept. of ECE
> Concordia University, Montreal, Canada
> Web: http://users.encs.concordia.ca/~k_hoque
> 
> 
> 
> 
> 
> 
> --
> Return on Information:
> Google Enterprise Search pays you back
> Get the facts.
> http://p.sf.net/sfu/google-dev2dev
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info


--
Return on Information:
Google Enterprise Search pays you back
Get the facts.
http://p.sf.net/sfu/google-dev2dev
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] word inequality tac?

[Anthony Fox]

wordsLib.WORD_ARITH_EQ_ss doesn't do very much.  It simply performs the 
conversion

x = y |-> x - y = 0w

but it does not simplify "x - y".  It is expected to be used in combination 
with wordsLib.WORD_ARITH_ss, which is included in the stateful simpset srw_ss() 
but not in std_ss.

The simpsets

wordsLib.WORD_ARITH_EQ_ss
wordsLib.WORD_BIT_EQ_ss
wordsLib.WORD_EXTRACT_ss

are not included in the stateful simpset, but they can help in some situations.

Anthony.

On 13 Dec 2009, at 04:06, Lu Zhao wrote:

> Hi Anthony and Magnus,
> 
> Thank you very much for the solution.
> 
> I have a question on srw_ss(). Before sending the email for help, I used
> 
> SIMP_TAC (std_ss++WORD_ARITH_EQ_ss) []
> 
> but it didn't work. Why does srw_ss() work and std_ss not? In what situations 
> should I use srw_ss()?
> 
> Lu


--
Return on Information:
Google Enterprise Search pays you back
Get the facts.
http://p.sf.net/sfu/google-dev2dev
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] the different between with type and datatype in HOL4

[Anthony Fox]

Another option is to use finite Cartesian products, which are defined in 
src/n-bit/.  This is very similar to Konrad's approach, except for the handling 
of the number of rows and columns, which is done through the type system.  For 
example, you would have

load "wordsLib";  (* loads finite Cartesian products and gets evaluation 
working *)

val vprod_def =
  Define
`vprod (v1:num['a]) (v2:num['a]) =
   Sigma 0 (dimindex(:'a)-1) ((FCP i. (v1 ' i) * (v2 ' i)):num['a])`;

val matrix_prod_def =
  Define
`matrix_prod (M1:num['a]['b]) (M2:num['c]['a]) =
   (FCP r c. vprod (M1 ' r) (FCP r. M2 ' r ' c)) : num['c]['b]`;

val fromLists_def =
  Define
 `fromLists lists = FCP r c. EL c (EL r lists)`;

val matA_def =
  Define
   `matA = fromLists [[1;2;3;4]; [2;3;5;7]; [9;8;7;2]] : num[4][3]`;

val matB_def =
  Define
   `matB = fromLists [[1;2]; [5;7]; [8;7]; [11;3]] : num[2][4]`;

EVAL ``(matrix_prod matA matB) ' 1 ' 1``;  (* Should be 81 *)

FCP is a binder, used to define finite Cartesian products -- the size is given 
by the function dimindex.  Type annotations are needed when using fromLists 
because the definition doesn't (can't) examine the lists to get the correct 
dimensions.

For a HOL beginner, I would expect proofs to be a little more tricky with this 
approach.  However, there is the advantage that side conditions are no longer 
required e.g. you would just prove

  matrix_prod A (matrix_prod B C) = matrix_prod (matrix_prod A B) C

Cheers,
Anthony.

On 12 Apr 2010, at 04:32, Konrad Slind wrote:

> Hi Amy,
> 
>   Matrices are an interesting modelling example, since there are  
> several
> viable approaches.  For extreme simplicity, I would use functions of  
> type
> 
>  num -> num -> 'a
> 
> to represent them. That makes many of the basic operations quite easy.
> You will also need to include the rows and columns. This leads to the
> idea of having a record hold the rows, columns, and indexing function:
> 
>   Hol_datatype
> `matrix = <| rows:num; cols:num; index:num->num->'a |>`;
> 
> To then define an operation like matrix multiplication, you need a  
> summation
> function:
> 
>   val Sigma_def =
> tDefine
>  "Sigma"
>   `Sigma lo hi f =
>   if lo > hi then 0 else f(lo) + Sigma (lo+1) hi f`
> (WF_REL_TAC `measure (\(lo,hi,f). (hi+1) - lo)`);
> 
> WIth that you can define the finite product of two vectors:
> 
>   val vprod_def =
> Define
>`vprod v1 v2 k = Sigma 0 (k-1) (\i. v1(i) * v2(i))`;
> 
> And then the matrix product is
> 
>   val matrix_prod_def =
> Define
>   `matrix_prod (M1:num matrix) (M2:num matrix) =
>  <|rows := M1.rows ;
>cols := M2.cols ;
>index := \r c. vprod (M1.index r) (\r. M2.index r c)  
> M1.cols |>`;
> 
> It also helps for testing to have something that makes a matrix from a
> list of lists:
> 
>   Define
>  `fromLists lists =
> <| rows := LENGTH lists;
>cols := LENGTH (HD lists);
>index := \r c. EL c (EL r lists) |>`;
> 
> A test:
> 
>   val matA_def =
> Define
>  `matA = fromLists [[1;2;3;4]; [2;3;5;7]; [9;8;7;2]]`;
> 
>val matB_def =
> Define
>  `matB = fromLists [[1;2]; [5;7]; [8;7]; [11;3]]`;
> 
>EVAL ``(matrix_prod matA matB).index 1 1``;  (* Should be 81 *)
> 
> Then you of course have to prove some theorems about the product.
> An obvious one would be associativity. Note that you have to constrain
> the matrices appropriately.
> 
> (A.cols = B.rows) /\ (B.cols = C.rows)
> ==>
> ( matrix_prod A (matrix_prod B C) = matrix_prod (matrix_prod A B) C
> 
> I haven't tried this proof, so there may be lurking problems with the  
> above
> formulation. But the general idea should be clear. I would be keen to  
> hear
> of other formalizations of matrices, since, as I mentioned, there are  
> multiple
> ways to skin this cat.
> 
> For example, another approach would be to use a list of equal-length  
> lists
> to represent the matrix, but my experience with that approach was  
> kind of
> negative: I got bogged down in relatively horrible inductions to prove
> even simple theorems.
> 
> Cheers,
> Konrad.
> 
> 
> 
> On Apr 11, 2010, at 9:42 AM, anythingroom wrote:
> 
>> Hi everyone，
>> 
>> 
>> 
>> Who know the different between with type and datatype in HOL4? I  
>> wanted to define a new type for matrix in HOL4, but I might be  
>> confusing type with datatype. I didn’t know how to start to define  
>> the type of matrix.
>> 
>> 
>> 
>> Who can help me ? Thank you very much. I’m looking for your reply.
>> 
>> 
>> 
>> Best wishes,
>> 
>> Amy
>> 
>> 
>> 
>> -- 
>> 
>> Download Intel® Parallel Studio Eval
>> Try the new software tools for yourself. Speed compiling, find bugs
>> proactively, and fine-tune applications for parallel performance.
>> See why Intel Parallel Studio got high marks during beta.
>> http://p.sf.net/sfu/intel-

Re: [Hol-info] How can I correct the type?

[Anthony Fox]

Hi,

My guess for the correct definition is:

val det = Define`
   det (A:('n ,'n) matrix) =
 sigma (\p. (sign (dimindex(:'n)) p) *
(product (1n, dimindex(:'n))
  (\(k:num). (A ' k ' (p (k:real))
   { (p:num -> num) | permutes (dimindex(:'n)) p}`;

This fixes a few things:

1. "prod_iter" wasn't defined, so replaced it with "product".
2. "sigma" requires a map as the first argument, so added "\p. ".
3. "dimindex(:'n)" needed to be surrounded by brackets.
4. "%%" syntax is not supported in the latest release, it has been  
replaced with '.  You can an overload if you like the old syntax.


Anthony

On 12 Oct 2010, at 13:28, anythingroom wrote:


Hi everyone,


I have to define the determinant definition in HOL4 and I define it  
as following:



val det =

Define ` det (A:('n ,'n) matrix) = sigma ( (sign (dimindex(:'n)) p)  
* ( prod_iter ( (1:num), dimindex(:'n) ) (\(k:num). (A %% k %% (p  
(k) ) ) ):real ) ) { (p:num -> num) | permutes dimindex(:'n) p}`;



But there are some errors on typecheck.


<>


Type inference failure: unable to infer a type for the application of


(sigma :('a -> real) -> ('a -> bool) -> real) :('a -> real) -> ('a - 
> bool) -> real



on line 50, characters 46-50


to


sign (dimindex ((:'n) :'n itself)) (p :num -> num) *

(prod_iter :num # num -> (num -> real) -> real)

  ((1 :num),dimindex ((:'n) :'n itself))

  (\(k :num). (A :('n, 'n) matrix) %% k %% p k)


on line 50, characters 54-160


which has type


:real


unification failure message: unify failed


Exception raised at Preterm.typecheck:

on line 50, characters 54-160:

failed

! Uncaught exception:

! HOL_ERR


Because the blue part has real type not “’a -> real” type?


How can I correct the definition of determinant?

Could anybody give me some hints?


I really appreciate your help!


The loaded libraries are listed here:

app  
load 
["HolKernel 
","bossLib 
","fcpTheory","listTheory","wordsLib","realTheory","realLib",


"simpLib 
","boolTheory 
","boolLib","mesonLib","Parse","fcpLib","pred_setTheory"];



open HolKernel bossLib fcpTheory listTheory wordsLib realTheory  
realLib simpLib boolTheory


boolLib mesonLib Parse fcpLib pred_setTheory;

val _ = type_abbrev ("matrix", ``:(real ** 'a) ** 'b``);


val permutes =

Define ` permutes (n:num) (p:num -> num) =(!i. (i = 0) ==> (p i =  
i)) /\ (!i. (i < SUC n) ==> (p i < SUC n)) /\ (!y. ?!i. p i = y)`;



val productc = Define ` (productc n 0 f = 1) /\ (productc n (SUC m)  
f = productc n m f * f(n+m))`;



val product = Define ` product(m,n) f = productc m n f`;


val prod_iter = store_thm("prod_iter", ``!f m n. (product(n,0) f =  
1) /\


(product(n, SUC m) f = product(n,m) f * f (n+m))``, REWRITE_TAC  
[productc,product]);



val nixu = Define` nixu (n:num) (p: num -> num) = {i:num ,j| ((i <  
j) /\(j < n)) /\ (p i > p j)}`;


val _ = overload_on ("nixu", ``nixu : num -> (num -> num) -> num #  
num ->bool``);



val evenperm = Define`evenperm n p = EVEN (CARD(nixu n p))`;

val _ = overload_on ("evenperm", ``evenperm : num -> (num -> num) ->  
bool``);



val sign = Define`sign n p = if evenperm n p then 1 else ~1`;

val _ = overload_on ("sign", ``sign : num -> (num -> num) -> real``);


val sum_image_real = Define`sigma (f :'a -> real) (s :'a -> bool) =  
ITSET (\(e :'a) (acc :real). f e + acc) s (0 :real)`;





Amy



全国最低价，天天在家冲照片，24小时发货上门！  
--

Beautiful is writing same markup. Internet Explorer 9 supports
standards for HTML5, CSS3, SVG 1.1,  ECMAScript5, and DOM L2 & L3.
Spend less time writing and  rewriting code and more time creating  
great

experiences on the web. Be a part of the beta today.
http://p.sf.net/sfu/beautyoftheweb___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info


--
Beautiful is writing same markup. Internet Explorer 9 supports
standards for HTML5, CSS3, SVG 1.1,  ECMAScript5, and DOM L2 & L3.
Spend less time writing and  rewriting code and more time creating great
experiences on the web. Be a part of the beta today.
http://p.sf.net/sfu/beautyoftheweb___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] How can I correct the definition about the submatrix?

[Anthony Fox]

Hi,

I'm not entirely sure I understand what you're trying to define.  If  
you're just after the matrix that is matrix A with row i and column j  
removed then you could define this as follows:

val dsyz_matrix = Define`
   dszy_matrix (A:('n,'n) matrix) (i:num) (j:num) : ('n sub1,'n sub1)  
matrix =
 FCP x y. let xi = if x < i then x else x + 1
  and yj = if y < j then y else y + 1
  in A ' xi ' yj`;

The "size" of ``:'n sub1`` is one less than the size of ``:'n``.   
Although note that ``dimindex(:1 sub1) = 1``, since all type must have  
at least one element.  One disadvantage of this sort of definition is  
that you can't really do arithmetic on types, e.g. ``:'a sub1 + 1`` is  
not the same as ``:'a``.  This could lead to unexpected type errors.   
To get around this you may need to define a casting function, e.g.  
something like

val cast_matrix = Define`
   cast_matrix pad (A:('a,'b) matrix) : ('m,'n) matrix =
  FCP x y. if x < dimindex (:'a) /\ y < dimindex (:'b) then
 A ' x ' y
   else
 pad`;

Note that if ``dimindex (:'a) = dimindex (:'m)`` and ``dimindex (:'b)  
= dimindex (:'n)`` then effectively this will be an identity map.

Note that this requirement comes from a fundamental limitation of  
HOL's simple, polymorphic type system.  Systems with dependent types  
(such as Coq and PVS) are better equipped for doing this sort of  
reasoning, with the caveat that type checking is more complicated (not  
always fully automatic) in these systems.

Anthony

On 26 Nov 2010, at 07:35, anythingroom wrote:

> hi everyone,
>
>
> I want to define a submatrix Mij is formed by throwing away row i  
> and column j :
>
> The initial matrix of order n, this splitting gives n smaller matrix  
> of order n-1.
>
>
> I define the definition of submatrix as follow:
>
>
> val dsyz_matrix = Define`dszy_matrix (A:('n,'n) matrix) (r:num)  
> (c:num) =
>
> (\i j. (FCP x y. if (i < r /\ j < c) then (A %% x %% y) else
>
> if (i < r /\ j > c) then (A %% x %% (y + 1)) else
>
> if(i > r /\ j > c) then (A %% (x + 1) %% (y + 1)) else
>
> (A %% (x + 1) %% y)))`;
>
>
> And the result is like this:
>
> val dsyz_matrix =
> |- !(A :('n, 'n) matrix) (r :num) (c :num).
>  (dszy_matrix A r c :num -> num -> ('a, 'b) matrix) =
>  (\(i :num) (j :num).
> FCP (x :num) (y :num).
>   (if i < r /\ j < c then
>  A %% x %% y
>else
>  (if i < r /\ j > c then
> A %% x %% (y + (1 :num))
>   else
> (if i > r /\ j > c then
>A %% (x + (1 :num)) %% (y + (1 :num))
>  else
>A %% (x + (1 :num)) %% y : thm
>
>
> But the submatrix of order is not n – 1.
>
> How can I correct the definition that limit the order n – 1 of  
> submatrix? Could anybody give me some hints about it?
>
>
> I appreciate your help.
>
>
> Best wishes,
>
>
> Amy
>
>
>
> 网易163/126邮箱百分百兼容iphone ipad邮件收发  
> --
> Increase Visibility of Your 3D Game App & Earn a Chance To Win $500!
> Tap into the largest installed PC base & get more eyes on your game by
> optimizing for Intel(R) Graphics Technology. Get started today with  
> the
> Intel(R) Software Partner Program. Five $500 cash prizes are up for  
> grabs.
> http://p.sf.net/sfu/intelisp-dev2dev___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info


--
Increase Visibility of Your 3D Game App & Earn a Chance To Win $500!
Tap into the largest installed PC base & get more eyes on your game by
optimizing for Intel(R) Graphics Technology. Get started today with the
Intel(R) Software Partner Program. Five $500 cash prizes are up for grabs.
http://p.sf.net/sfu/intelisp-dev2dev
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Inconsistencies in wordsTheory, or stupidity on my part?

[Anthony Fox]

Hi,

This appears to be a bug in METIS_TAC.  It should fail but it instead returns a 
legitimate theorem - just one with inconsistent hypotheses.  This appears to 
relate to the fact that METIS_TAC is at heart a first-order prover, which 
doesn't fit in with the types/theorems in wordsTheory.  Joe Hurd may like to 
take a look at this...

Using METIS_TAC in this way is fairly non-standard -- it's mostly applied to 
small goals using a few hand-picked theorems.

What sort of goals are you trying to prove?  You may like to consider using one 
of the standard procedures in wordsLib or blastLib.  If you're trying to prove 
arithmetic properties then you could try wordsLib.WORD_ARITH_PROVE, e.g.

> load "wordsLib";
> wordsLib.WORD_ARITH_PROVE
  ``(a * (b + c) + b = a * b) = (a * c = -b)``
val it =
   |- (a * (b + c) + b = a * b) ⇔ (a * c = -b):
   thm

(or as a tactic: CONV_TAC wordsLib.WORD_ARITH_CONV.)

Note that WORD_ARITH_PROVE has only just been added to the SourceForge 
repository.  wordsLib.WORD_DECIDE is similar but can't prove the goal above.

If you are working with *known* word sizes then blastLib.BBLAST_PROVE 
(BBLAST_TAC) is a good option, e.g.

> blastLib.BBLAST_PROVE
  ``(31 >< 2) (w2w (x:word30) << 2 + y:word32) = x + (31 >< 2) y``;
val it =
   |- (31 >< 2) (w2w x ≪ 2 + y) = x + (31 >< 2) y:
   thm

However, this isn't so suited to proving things about multiplication (by a 
non-literal) and division.

If these routines don't work then you may have to rely on user guidance or 
writing custom routines, e.g. using the simplifier and the various tools in 
wordsLib.   The help pages may be helpful there:

help "wordsLib";
help "WORD_ARITH_CONV";

Anthony

On 23 Jun 2011, at 12:33, Tom N wrote:

> Hello,
> 
> I have a set of hypotheses involving the words library that I would
> like to prove automatically. My first attempt at this was to ask HOL
> to prove them against the entirety of wordsTheory, using:
> 
>> prove(hypothesis, METIS_TAC(map snd (DB.theorems "words")));
> 
> While this appeared to work at first, it seems that it is able to
> 'prove' obviously-incorrect hypotheses, for example:
> 
>> load "wordsTheory"; open wordsTheory;
>> show_assums := true;
>> prove(``F``, METIS_TAC(map snd (DB.theorems "words")));
>  [%%genvar%%8939 = @m. dimindex (:'XXfolXX_40996) = SUC m,
>   %%genvar%%8939 = @m. dimindex (:2) = SUC m,
>   %%genvar%%8939 = @m. dimindex (:unit) = SUC m] |- F:
> thm
> 
> Is this more likely to indicate an inconsistency in wordsTheory, or me
> doing something wrong?  I've only started using HOL recently, so it's
> probably the latter ;)
> 
> 
> Thanks in advance,
> 
> Tom Nixon
> 
> --
> Simplify data backup and recovery for your virtual environment with vRanger.
> Installation's a snap, and flexible recovery options mean your data is safe,
> secure and there when you need it. Data protection magic?
> Nope - It's vRanger. Get your free trial download today.
> http://p.sf.net/sfu/quest-sfdev2dev
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info


--
All the data continuously generated in your IT infrastructure contains a 
definitive record of customers, application performance, security 
threats, fraudulent activity and more. Splunk takes this data and makes 
sense of it. Business sense. IT sense. Common sense.. 
http://p.sf.net/sfu/splunk-d2d-c1
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] emitLib

[Anthony Fox]

To reconstruct the datatype you can use EmitTeX.datatype_thm_to_string, which 
is documented.

Anthony

On 22 Mar 2012, at 09:14, Michael Norrish wrote:

> Unfortunately there isn't any documentation for emitLib.  If you figure 
> anything out, patches fixing this situation would be gratefully received.  
> There are a number of examples of probably useful uses of emitLib in the HOL 
> sources.  If you figure out who wrote those calls (git blame may help), feel 
> free to hassle those people for enlightenment. Indeed, those people may well 
> be in your building. 
> 
> Michael
> 
> On 22/03/2012, at 19:58, Ramana Kumar  wrote:
> 
>> Is EmitML documented somewhere? I don't think I saw it in the Description 
>> manual.
>> In particular, I'm wondering whether I need to repeat the quotation of a 
>> datatype for EmitML.DATATYPE (after having passed it once already to 
>> Hol_datatype) if I want to emit a datatype, or whether it can be 
>> reconstructed somehow based on whatever Hol_datatype stores.
> 


--
This SF email is sponsosred by:
Try Windows Azure free for 90 days Click Here 
http://p.sf.net/sfu/sfd2d-msazure
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] More efficient operations on finite sets and tabulated functions.

[Anthony Fox]

Hi,

Just for reference. The Patricia tree library works well for simple 
dictionary-style lookups (IN) but it’s not so suited to computing UNIONS.

For example, you can define constants as follows:

val s100_def = patriciaLib.Define_mk_ptree "s100"
  (patriciaLib.ptree_of_ints
 [0,1,2,3,4,5,6,7,8,9,10,19,18,17,16,15,14,13,12,11,
  20,22,24,26,28,30,29,27,25,23,21,39,38,37,36,35,34,33,32,31,
  40,41,42,43,44,45,56,57,48,49,50,59,58,57,56,55,54,53,52,51,
  60,63,66,69,61,64,67,62,65,68,79,75,71,78,74,70,77,73,76,72,
  99,98,96,93,89,84,80,82,85,88,92,95,97,81,83,87,92,91,90,94])

val s50_def = patriciaLib.Define_mk_ptree "s50"
  (patriciaLib.ptree_of_ints
 [10,19,18,17,16,15,14,13,12,11,
  40,41,42,43,44,45,56,57,48,49,50,59,58,57,56,55,54,53,52,51,
  99,98,96,93,89,84,80,82,85,88,92,95,97,81,83,87,92,91,90,94])

The operation KEYS converts this to a list:

val thm1 = Count.apply (DEPTH_CONV patriciaLib.PTREE_DEFN_CONV THENC EVAL)
   ``KEYS s100`;

runtime: 0.071s,gctime: 0.000s, systime: 0.003s.
Axioms: 0, Defs: 0, Disk: 0, Orcl: 0, Prims: 95675; Total: 95675
val thm1 =
   |- KEYS s100 =
   [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; 18;
19; 20; 21; 22; 23; 24; 25; 26; 27; 28; 29; 30; 31; 32; 33; 34; 35;
36; 37; 38; 39; 40; 41; 42; 43; 44; 45; 48; 49; 50; 51; 52; 53; 54;
55; 56; 57; 58; 59; 60; 61; 62; 63; 64; 65; 66; 67; 68; 69; 70; 71;
72; 73; 74; 75; 76; 77; 78; 79; 80; 81; 82; 83; 84; 85; 87; 88; 89;
90; 91; 92; 93; 94; 95; 96; 97; 98; 99]:
   thm

Lookup is fairly fast:

val thm2 = Count.apply EVAL ``35 IN_PTREE s100`;

runtime: 0.001s,gctime: 0.000s, systime: 0.000s.
Axioms: 0, Defs: 0, Disk: 0, Orcl: 0, Prims: 1170; Total: 1170
val thm2 = |- 35 IN_PTREE s100 ⇔ T: thm

This scales reasonably well to trees with thousands of elements.

UNION is more complicated but with effort lookup can be fast:

val union_s50_s100_CONV =
   REWRITE_CONV
 [MATCH_MP patriciaTheory.IN_PTREE_UNION_PTREE
   (CONJ (DB.theorem "s50_is_ptree_thm")
 (DB.theorem "s100_is_ptree_thm"))];

val thm3 = Count.apply (union_s50_s100_CONV THENC EVAL)
   ``35 IN_PTREE (s50 UNION_PTREE s100)``;

runtime: 0.003s,gctime: 0.000s, systime: 0.001s.
Axioms: 0, Defs: 0, Disk: 0, Orcl: 0, Prims: 2052; Total: 2052
val thm3 = |- 35 IN_PTREE s50 UNION_PTREE s100 ⇔ T: thm

Of course, it will be a bit quicker if the element is in the first tree:

val thm4 = Count.apply (union_s50_s100_CONV THENC EVAL)
   ``11 IN_PTREE (s50 UNION_PTREE s100)``;

runtime: 0.001s,gctime: 0.000s, systime: 0.001s.
Axioms: 0, Defs: 0, Disk: 0, Orcl: 0, Prims: 884; Total: 884
val thm4 = |- 11 IN_PTREE s50 UNION_PTREE s100 ⇔ T: thm

Cheers,
Anthony

On 13 Nov 2012, at 17:42, F.Lockwood Morris  wrote:

> Dear Ramana,
> 
> Thank you very much for your encouraging message. I will send you my files 
> and the documentary notes such as they are very
> shortly, as soon as I add a few paragraphs to the latter.
> 
> At present I am running HOL 4 Kanasaskis-6. Having glanced at Michael's 
> wellorderScript.sml in examples, I think I had better not
> try to hook up to it until I get Kanasaskis-8 installed here, which I have 
> put in to have done. My formalization of Halmos's proof of the
> well-ordering theorem will do perfectly well for the time being.
> 
> As soon as I can manage, I will follow the suggestion both you and Michael 
> made, to try how EVAL does with a the_compset enlarged by the necessary 
> rewrites from my theories. I think there can be no doubt that EVAL, 
> unaugmented, burns up linear time for IN and quadratic time for UNION just 
> based on how far away the set elements mostly are in the default INSERT - {} 
> (that is effectively
> linear list) representation for sets. Here is one data point:
> 
> val s100 = Term`{0;1;2;3;4;5;6;7;8;9;10;19;18;17;16;15;14;13;12;11;
>   20;22;24;26;28;30;29;27;25;23;21;39;38;37;36;35;34;33;32;31;
>   40;41;42;43;44;45;56;57;48;49;50;59;58;57;56;55;54;53;52;51;
>   60;63;66;69;61;64;67;62;65;68;79;75;71;78;74;70;77;73;76;72;
>   99;98;96;93;89;84;80;82;85;88;92;95;97;81;83;87;92;91;90;94}`;
> 
> val s50 = Term`{10;19;18;17;16;15;14;13;12;11;
>   40;41;42;43;44;45;56;57;48;49;50;59;58;57;56;55;54;53;52;51;
>   99;98;96;93;89;84;80;82;85;88;92;95;97;81;83;87;92;91;90;94}`;
> 
> Count.apply EVAL_CONV (Term`^s50 UNION ^s100`);
> 
> takes on my machine 33.7 seconds and 857842 inference steps (1154262 steps 
> for ^s100 UNION ^s50).
> 
> More cumbersomely, going around through my conversions:
> 
> val t50 = make_oset numto_CONV (Term`numto`) s50; (* 14276 infs. 2.4s *)
> val t100 = make_oset numto_CONV (Term`numto`) s100; (* 29374 infs. 5.6s *)
> 
> (These print out large trees you don't want to see. Most of the work so far 
> has gone into sorting.)
> 
> val beer1 = o_union_RULE numto_CONV t50 t100; (* 9539 inference steps, 1.25 
> seconds *) (another

Re: [Hol-info] HOL4's ARM model- Output Simplification.

[Anthony Fox]

Hi Hamed,

I’m assuming that your example comes from using the tool 
arm_random_testingLib.arm_step_updates.

If you wish to manipulate these terms then you can do so using HOL4’s 
collection of syntax functions (e.g. see Term, boolSyntax and wordsSyntax). 
These libraries can be used to destruct terms and to build new ones. For 
example, you can get a list of bytes as follows:

> val l = HolKernel.strip_binop (Lib.total wordsSyntax.dest_word_concat) tm;
val l =
   [``mem (r2 + 7w)``,
``mem (r2 + 6w)``,
``mem (r2 + 5w)``,
``mem (r2 + 4w)``]: term list

where tm is your original term. You can then build a term that is close to what 
you’re after as follows:

Term.mk_comb 
   (Term.mk_var ("mem", ``:word32 # 'a -> word32``),
pairSyntax.mk_pair
   (boolSyntax.rand (List.last l),
Term.mk_var ("e_little", Type.alpha)));
val it = ``mem (r2 + 4w,e_little)``:

However, note that this is definitely not "proper simplification” because the 
manipulations are not constrained by HOL’s logic. The manipulations are purely 
syntactic and there is no proof going on at all.

If you wish to do simplifications (proofs) then 
arm_random_testingLib.arm_step_updates is not the way to go; you should instead:

1. Use armLib.arm_step to give you a theorem.

2. Make definitions that correspond with BAP’s model, e.g. define a memory 
operation with the right semantics.

3. Use forward proof (e.g. REWRITE_RULE and SIMP_RULE) to translate the 
step-theorem into the required form.

Regards,
Anthony

On 28 Jan 2013, at 12:40, hamed nemati  wrote:

> 
> Dear developers,
> 
> I am a student working on formal verification of a middle-ware. In this 
> project as a part of this verification task, I have to convert the HOL4 step 
> theorem's output to a simplified intermediate language which can be processed 
> by another tool called BAP(http://bap.ece.cmu.edu/).
> 
> I already implemented a prototype version of such a converter module, which 
> is completely based on syntax analysis of the HOL4's output. Now, I am trying 
> to adopt a new approach to introduce this converter into the HOL4 structure, 
> but I do not know what is the best way to do this. I would appreciate if you 
> could help me with this by providing a guideline. As an example for 
> instructions which deal with memory like (ldr r1,[r2,#4]) , what the HOL4 
> model for ARM produces is as follows: (I attached the code snippet producing 
> the following output)
> 
> ((mem :u32 -> u8) ((r2 :u32) + (7w :u32)) @@
>((mem (r2 + (6w :u32)) @@
>((mem (r2 + (5w :u32)) @@ mem (r2 + (4w :u32))) :word16))
> :word24))
> 
> However the BAP's intermediate language syntax for this instruction is
> 
> mem:?u32[(R2:u32 + 0x4:u32),e_little]:u32
> 
> I was wondering if there is way to do this kind of simplification inside the 
> HOL4. Many thanks in advance.
> 
> Regards,
> 
> --
> Master Visual Studio, SharePoint, SQL, ASP.NET, C# 2012, HTML5, CSS,
> MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current
> with LearnDevNow - 3,200 step-by-step video tutorials by Microsoft
> MVPs and experts. ON SALE this month only -- learn more at:
> http://p.sf.net/sfu/learnnow-d2d___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info


--
Master Visual Studio, SharePoint, SQL, ASP.NET, C# 2012, HTML5, CSS,
MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current
with LearnDevNow - 3,200 step-by-step video tutorials by Microsoft
MVPs and experts. ON SALE this month only -- learn more at:
http://p.sf.net/sfu/learnnow-d2d
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] HOL4's ARM model- Output Simplification.

[Anthony Fox]

On 29 Jan 2013, at 09:57, hamed nemati  wrote:

> Dear Antony,
> 
> Thank you very much for this wonderful explanation! Is there any example of 
> such simplification inside the HOL4's ARM model?
> 
> Regards,
> Hamed


Hi Hamed,

You can find examples of using “conversions” and “rules” throughout the HOL 
distribution. These are often used to perform some sort of “simplification”. 
Typically these routines are defined in files with the name *Lib.sml. The ARM 
tools (e.g. arm_stepLib) are probably not particularly illustrative though. 
You’d be better off reading through some HOL4 documentation, e.g.

http://hol.sourceforge.net/kananaskis-8-helpdocs/help/Docfiles/HTML/bossLib.SIMP_CONV.html

As a very brief primer:

A “conversion” is any SML function with type

: Term.term -> Thm.thm

satisfying the requirement that

cnv ``x``

produces a theorem of the form

|- x = y

For example, the simplifier "SIMP_CONV simpset rwts" is such a conversion:

> SIMP_CONV (srw_ss()) [] ``12w * a + 4w * a: word32``;
val it =
   |- 12w * a + 4w * a = 16w * a: thm

Most conversions are suffixed with “_CONV” (but some aren’t, e.g. EVAL). 
Conversions can be sequenced using the THENC operator; for example:

> (SIMP_CONV (srw_ss()) [] THENC wordsLib.WORD_MUL_LSL_CONV) ``12w * a + 4w * 
> a: word32``;
val it =
   |- 12w * a + 4w * a = a ≪ 4: thm

Therefore, the most common way to define new “custom” conversions is to use 
existing conversions as building blocks (combining them together with operators 
such as THENC, ORELSEC, REPEATC, DEPTH_CONV, RATOR_CONV, ...).

A “rule” is any SML function with type

: Thm.thm -> Thm.thm

Most, but not all, rules are suffixed with “_RULE”. Rules can be built from 
conversions using Conv.CONV_RULE. For example:

> Conv.CONV_RULE (Conv.DEPTH_CONV wordsLib.WORD_MUL_LSL_CONV)
   (ASSUME ``b = 16w * a : word32``)
val it =  [.] |- b = a ≪ 4: thm

Here DEPTH_CONV ensures that the conversion is tried at all positions 
(bottom-up).

If you wish to introduce your own definitions then you can use Define. For 
example:

val LSL4_def = Define `LSL4 a = (a << 4) : word32`

These definitions can then be used as “rewrites”. For example:

(SIMP_CONV (srw_ss()) []
 THENC wordsLib.WORD_MUL_LSL_CONV
 THENC REWRITE_CONV [GSYM LSL4_def]) ``12w * a + 4w * a : word32``
val it = |- 12w * a + 4w * a = LSL4 a:

The rule GSYM reverses an equality — so here it ensures that the rewrite 
theorem LSL4_def is applied right-to-left.

Thus, given a term or theorem, it’s possible to introduce your own definitions 
through the use of conversions and rules.

Regards,
Anthony
--
Master Visual Studio, SharePoint, SQL, ASP.NET, C# 2012, HTML5, CSS,
MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current
with LearnDevNow - 3,200 step-by-step video tutorials by Microsoft
MVPs and experts. ON SALE this month only -- learn more at:
http://p.sf.net/sfu/learnnow-d2d
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] list computations

[Anthony Fox]

Note quite sure how you got to 48 lines. I think only a single call to SRW_TAC 
(or lcsymtacs.lrw) is needed.

val thm = Q.prove(
   `TAKE (LENGTH bvs + 1)
 (REVERSE bvs ++
  h::
  (blvs ++ [benv; x] ++ REVERSE args0 ++ [cl0] ++ st)) ++
   DROP (LENGTH args0 + (LENGTH blvs + (LENGTH bvs + 4)))
 (REVERSE bvs ++
  h::
  (blvs ++ [benv; x] ++ REVERSE args0 ++ [cl0] ++ st)) =
   TAKE (LENGTH bvs + 1)
 (REVERSE bvs ++
  h::
  (blvs ++ [benv; x] ++ REVERSE args0 ++ [cl0] ++ st)) ++ st`,
   lrw [listTheory.LIST_EQ_REWRITE, rich_listTheory.EL_DROP,
rich_listTheory.EL_APPEND2, rich_listTheory.EL_CONS,
arithmeticTheory.PRE_SUB1]
   )

Anthony

On 27 Feb 2013, at 17:58, Ramana Kumar  wrote:

> I just wrote a fairly manual 48-line proof of the following.
> Is there some decision procedure, simpset, or tactic I could use to automate 
> it that I'm not aware of?
> The theorems in srw_ss() seem not to play very well together on this kind of 
> stuff.
> 
> TAKE (LENGTH bvs + 1)
>   (REVERSE bvs ++
>Block 3 [CodePtr a; bve]::
>(blvs ++ [benv; CodePtr ret] ++ REVERSE args0 ++ [cl0] ++ st)) ++
> DROP (LENGTH args0 + (LENGTH blvs + (LENGTH bvs + 4)))
>   (REVERSE bvs ++
>Block 3 [CodePtr a; bve]::
>(blvs ++ [benv; CodePtr ret] ++ REVERSE args0 ++ [cl0] ++ st)) =
> TAKE (LENGTH bvs + 1)
>   (REVERSE bvs ++
>Block 3 [CodePtr a; bve]::
>(blvs ++ [benv; CodePtr ret] ++ REVERSE args0 ++ [cl0] ++ st)) ++
> st
> 
> --
> Everyone hates slow websites. So do we.
> Make your web apps faster with AppDynamics
> Download AppDynamics Lite for free today:
> http://p.sf.net/sfu/appdyn_d2d_feb___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info


--
Everyone hates slow websites. So do we.
Make your web apps faster with AppDynamics
Download AppDynamics Lite for free today:
http://p.sf.net/sfu/appdyn_d2d_feb
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Question about wordTheory

[Anthony Fox]

Hi Hamed,

Yes, the side-condition

n < dimindex (:α)

is redundant. I’ve updated this theorem accordingly.

To get a theorem with no side-conditions we can introduce a MOD:

 wordsTheory.n2w_DIV
 |> Q.SPEC `a MOD dimword(:'a)`
 |> SIMP_RULE (srw_ss()) [wordsTheory.n2w_mod]
 |> GEN_ALL

val it =
   |- ∀a n. n2w (a MOD dimword (:α) DIV 2 ** n) = n2w a ⋙ n:
   thm

It would also have been possible to get to this theorem using word_lsr_n2w as 
the starting point.

Regards,
Anthony

On 4 Mar 2013, at 19:48, hamed nemati  wrote:

> Hello all,
> For Theorems like the following one what is the corresponding theorem if 
> the guard conditions do not hold,  I mean what the n2w_DIV theorem would like 
> if a or n or
>  both of them are greater that dimword (:α).
>[n2w_DIV
> ]  Theorem
> 
>   |- ∀a n.
>n < dimindex (:α) ∧ a < dimword (:α) ⇒
> 
>(n2w (a DIV 2 ** n) = n2w a ⋙ n) 
> 
> do we have module to dimword(:'a) of these two numbers? if no what we can
> do in such a case? Thanks in advance.
> 
> Regards,
> Hamed Nemati
> --
> Everyone hates slow websites. So do we.
> Make your web apps faster with AppDynamics
> Download AppDynamics Lite for free today:
> http://p.sf.net/sfu/appdyn_d2d_feb___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info


--
Everyone hates slow websites. So do we.
Make your web apps faster with AppDynamics
Download AppDynamics Lite for free today:
http://p.sf.net/sfu/appdyn_d2d_feb
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Question about wordTheory

[Anthony Fox]

Hi Hamed,

Ideally there shouldn’t be any theorems with redundant side-conditions, so 
these are worth reporting/fixing, especially if they’re hampering progress. In 
general, side-conditions will be there because they’re needed.

You may be able to specialise other theorems to eliminate side-conditions, 
however this can make the resulting theorems less useful.

For example:

n2w (a MOD dimword (:α) DIV 2 ** n) = ...

is a less useful than the conditional rewrite

a < dimword(:’a) ==> (n2w (a DIV 2 ** n) = ...)

This is because with the latter we can do:

> SIMP_CONV (srw_ss()) [n2w_DIV] ``n2w (3 DIV 2 ** n) : word8``;
val it = |- n2w (3 DIV 2 ** n) = 3w ⋙ n: thm

which isn’t directly possible with the former.

Regards,
Anthony

On 4 Mar 2013, at 22:04, hamed nemati  wrote:

> Dear Anthony,
> 
> Thank you very much for your response. Is it a general case and we can do the 
> same for all the other theorems like the n2w_DIV or no? 
> 
> Regards,


--
Everyone hates slow websites. So do we.
Make your web apps faster with AppDynamics
Download AppDynamics Lite for free today:
http://p.sf.net/sfu/appdyn_d2d_feb
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Array's in proof

[Anthony Fox]

Just to add to Konrad’s e-mail.

There is a list “write" operation in listTheory — it is defined as follows:

(∀e n. LUPDATE e n [] = []) ∧
(∀e x l. LUPDATE e 0 (x::l) = e::l) ∧
 ∀e n x l. LUPDATE e (SUC n) (x::l) = x::LUPDATE e n l

Other representation choices include:

  - functions of type  : ‘a word -> ty
  - partial functions  : ‘a word |-> ty

This could make sense if your “int” type is actually a machine word, e.g. 
``:word32`` in HOL.

Anthony

On 11 Apr 2013, at 18:12, Konrad Slind  wrote:

> Hi J.J. :
> 
>   First you have to choose how arrays are modelled, i.e., which HOL type
> is going to be used to represent arrays. Choices:
> 
>   - functions of type  : num -> ty
>   - finite functions : num |-> ty
>   - lists: ty list
>   - finite products  : ty['dim]
> 
> Summary of the read (A[i]) and write (A[i] := e) operations on array A:
> 
>   A : num -> ty   
>  read operation: A i  
>  write operation: \j. if (i=j) then e else A j
>  Note: there is already a definition for update in combinTheory, using an 
> infix
> 
>   (i =+ e) A = \j. if (i=j) then e else A(j)
> 
>   A  : num |-> ty  (load finite_mapTheory)
>   read operation: A ' i 
>   write : A |+ (i,e)
> 
>   A  : ty list
>  read operation: EL i list
>  write operation: not sure an indexed write for lists is defined in HOL. 
> If not, the 
>  following is one version:
> 
> update (h::t) 0 e = e::t
> update (h::t) n e = h::update t (n-1) e;
> 
>   A : ty['dim]   (load fcpTheory)
>  read operation: A ' i
>  write operation: (i :+ e) A
> 
> I hope this helps,
> Konrad.
> 
> 
> 
> On Thu, Apr 11, 2013 at 6:10 AM, J. J. W.  wrote:
> Dear all,
> 
> I would like to model the following:
> 
> public replace_smaller(int[] A, int c, int d){
>   if (A[d] < A[c]){
>   A[c] = A[q]
>   }
>   return A;
> }
> 
> and I would like to prove that the resulting array is just like the code.
> 
> So I think I should define the following:
> 
> val replace_smaller_def = Define `replace_smaller a b (\a. if (nth (a, p) < 
> nth (a,q)) then ... else ...`;
> 
> However I have no idea how to continue with this since, I have no idea how to 
> access the array or anything like that.
> 
> Can someone give me some advice?
> 
> Kind regards,
> 
> Jun Jie
> 
> --
> Precog is a next-generation analytics platform capable of advanced
> analytics on semi-structured data. The platform includes APIs for building
> apps and a phenomenal toolset for data science. Developers can use
> our toolset for easy data analysis & visualization. Get a free account!
> http://www2.precog.com/precogplatform/slashdotnewsletter
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
> 
> 
> --
> Precog is a next-generation analytics platform capable of advanced
> analytics on semi-structured data. The platform includes APIs for building
> apps and a phenomenal toolset for data science. Developers can use
> our toolset for easy data analysis & visualization. Get a free account!
> http://www2.precog.com/precogplatform/slashdotnewsletter___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info


--
Precog is a next-generation analytics platform capable of advanced
analytics on semi-structured data. The platform includes APIs for building
apps and a phenomenal toolset for data science. Developers can use
our toolset for easy data analysis & visualization. Get a free account!
http://www2.precog.com/precogplatform/slashdotnewsletter
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] More on set comprehensions

[Anthony Fox]

Rob,

On 29 Dec 2013, at 21:26, Rob Arthan  wrote:

>>   The code for HOL4 set abstractions says that the bound variables
>> of a set abstraction {t | p} are the intersection of the free variables 
>> of t and p unless either side has no free vars, in which case the
>> bound variables are those of the other side. Also, if t has no free vars,
>> then fail.
> 
> Thanks - I couldn't find my way round the HOL4 parser code.  However,
> the last bit seems to be a bit more subtle: HOL4 doesn't fail the following
> example where t has no free vars:
> 
> > ``{0 | a = b}``;
> <>
> val it = ``{0 | a = b}``: term

The relevant bit of HOL4 code is “make_set_abs”, which can be found in

src/parse/Parse_support.sml (line 470).

The failure case comes into play when:

* Neither “t” nor “p” have free variables

e.g. {0 | T} fails.

* Both “t” and “p” have free variables and at least one of them intersects

e.g. {x /\ y | x /\ z} is fine but {x /\ y | w /\ z} fails.

Everything else seems to be accepted.

With regard to the {t | d | p} syntax, everything seems to be accepted, 
provided that “d” is a comma separated list of variable names. For example,

{0 | a, b, c | T}

is accepted — it’s the term

GSPEC (\(a, b, c). (0, T))

Anthony--
Rapidly troubleshoot problems before they affect your business. Most IT 
organizations don't have a clear picture of how application performance 
affects their revenue. With AppDynamics, you get 100% visibility into your 
Java,.NET, & PHP application. Start your 15-day FREE TRIAL of AppDynamics Pro!
http://pubads.g.doubleclick.net/gampad/clk?id=84349831&iu=/4140/ostg.clktrk___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Assigning functions/operations in L3

[Anthony Fox]

Hi Oliver,

Yes, the approach of the former ARMv7 model doesn’t translate naturally to the 
new L3 setting. That is, it’s not possible to call co-processor “hook” 
functions within the L3 specification itself.

I can think of two options:

1. If you want to model a specific co-processor then it’s probably a good idea 
to specify this directly in L3. By way of an example, this is how the 
floating-point co-processor is currently modelled. An “accept” function isn’t 
really needed in this case. Floating-point instructions are either successfully 
decoded and run, or they decode as “undefined” and a processor “undefined 
instruction” exception occurs.

2. If you’re after something more generic (similar to before) then the best 
approach is probably to extend the exiting model within HOL. That is, you can 
augment the L3 exported “next state” function

|- ∀state.
 Next state =
 (let (v,s) = Fetch state
  in
ITAdvance () (let (v,s) = Decode v s in SND (Run v s))):

with custom HOL4 code. As such you'd augment the state-space with additional 
co-processor components/hooks (as you see fit). You’d end up with something 
roughly like:

CP-Next (cp-state, state) =
  if is-co-processor-instruction (FST (Fetch state)) then
 do-something (cp-state, state)
  else
 (cp-state, Next state)

Hope this helps.

Anthony

On 13 Jan 2014, at 18:13, Oliver Schwarz  wrote:

> Dear L3-experts,
> 
> in the former model of ARMv7, coprocessors were defined in a placeholder
> fashion like
> 
> val _ = Hol_datatype `Coprocessors =
>  <| state : coproc_state;
> accept : CPinstruction -> coproc_state -> (bool # coproc_state);
> .
> .
> .
> 
> where the behavior of accept was originally not defined, but could be
> specified later on by assigning/initializing an implementation my_accept
> to state.coprocessors.accept.
> 
> I would like to achieve something similar in L3.
> However, from what I understand from the documentation and some
> experiments, assigning some function/operation to a record member is not
> possible in L3, since the language is first order. Did I get that right?
> 
> One workaround I can think of is to do the definition (of Coprocessors,
> possibly even of my_accept) in L3, but initialize/assign later in HOL4.
> 
> Now:
> 1. Do you see any reason why I should not use that workaround?
> 2. Is there something else I can consider?
> 
> 
> I hope I was able to make my chaotic thoughts clear and am thankful for
> any help.
> Thanks!
> 
> Oliver
> 
> 
> --
> CenturyLink Cloud: The Leader in Enterprise Cloud Services.
> Learn Why More Businesses Are Choosing CenturyLink Cloud For
> Critical Workloads, Development Environments & Everything In Between.
> Get a Quote or Start a Free Trial Today. 
> http://pubads.g.doubleclick.net/gampad/clk?id=119420431&iu=/4140/ostg.clktrk
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info


--
CenturyLink Cloud: The Leader in Enterprise Cloud Services.
Learn Why More Businesses Are Choosing CenturyLink Cloud For
Critical Workloads, Development Environments & Everything In Between.
Get a Quote or Start a Free Trial Today. 
http://pubads.g.doubleclick.net/gampad/clk?id=119420431&iu=/4140/ostg.clktrk
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Find the precedence and fixity

[Anthony Fox]

How about

term_grammar.get_precedence (Parse.term_grammar())

?

On 10 Feb 2014, at 09:35, Ramana Kumar  wrote:

> Is there a way to find the precedence/fixity information about a token in the 
> term grammar that is better than using Parse.term_grammar() and sifting 
> through the voluminous output? Sometimes I don't have enough scroll buffer to 
> catch what I need from that!


--
Managing the Performance of Cloud-Based Applications
Take advantage of what the Cloud has to offer - Avoid Common Pitfalls.
Read the Whitepaper.
http://pubads.g.doubleclick.net/gampad/clk?id=121051231&iu=/4140/ostg.clktrk
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] How long should it take to build examples/machine-code?

[Anthony Fox]

I think it’s more likely that there was a problem with building minisat under 
the latest Mac OS. To check that it is installed, try going to the directory

HOL/src/HolSat/sat_solvers/minisat

There should be a binary “minisat” there. Alternatively, to make sure it is 
working properly, you can try something like:

> load “blastLib”;
..
> blastLib.BBLAST_PROVE ``?x y. x + y = 12w : word8``;

If you see the warning

HolSat WARNING: SAT solver not found. Using slow internal prover.
To turn off this warning, type: set_trace "HolSatLib_warn" 0; RET

then that is the source of your problem.

I have a patch for the minisat sources, but it’s not been checked on other 
platforms yet.

Anthony

On 5 Apr 2014, at 08:09, Ramana Kumar  wrote:

> I believe it takes several hours. I haven't done it myself though.
> 
> 
> On Sat, Apr 5, 2014 at 3:23 AM, Jiaqi Tan  wrote:
> Hi,
> 
> I have downloaded the latest version of HOL from github, and my current build 
> of examples/machine-code is taking quite a long time, and the build has been 
> stuck in examples/machine-code/instruction-set-models/x86_64 for about an 
> hour. I'm wondering if that's normal.
> 
> I am using PolyML 5.5.1 on Mac OS X 10.9.2. I have built HOL (poly < 
> tools/smart-configure.sml followed by bin/build), and I am building 
> examples/machine-code using "bin/build -dir examples/machine-code".
> 
> The last couple of lines of console output are:
> 
> Exporting theory "prog_x64" ... done.
> Theory "prog_x64" took 13.609s to build
> Analysing prog_x64Theory.sig
> Analysing prog_x64Theory.sml
> Linking prog_x64_extraScript.uo to produce theory-builder executable
> Poly/ML 5.5.1 Release
> <>
> Saved definition __ "zCODE_HEAP_RAX_def"
>  [cache]Saved definition __ "IMM32_def"
> Saved definition __ "stack_list_def"
> Saved definition __ "stack_list_rev_def"
> Saved definition __ "stack_ok_def"
> Saved definition __ "zSTACK_def"
> Saved theorem _ "x64_pop_r0"
> Saved theorem _ "x64_pop_r1"
> Saved theorem _ "x64_pop_r2"
> Saved theorem _ "x64_pop_r3"
> Saved theorem _ "x64_pop_r6"
> Saved theorem _ "x64_pop_r7"
> Saved theorem _ "x64_pop_r8"
> Saved theorem _ "x64_pop_r9"
> Saved theorem _ "x64_pop_r10"
> Saved theorem _ "x64_pop_r11"
> Saved theorem _ "x64_pop_r12"
> Saved theorem _ "x64_pop_r13"
> Saved theorem _ "x64_pop_r14"
> Saved theorem _ "x64_pop_r15"
> 
> How long does it typically take to build examples/machine-code? Is it closer 
> to under an hour, or several hours?
> 
> Thanks!
> 
> Regards,
> Jiaqi
> 
> 
> --
> 
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
> 
> 
> --
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info


--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] How long should it take to build examples/machine-code?

[Anthony Fox]

Hi Jiaqi,

I get the same error if I do

bin/build -dir examples/machine-code

so I suspect this is problem with “build”. The more conventional thing to do 
would be:

$ cd HOL/examples/machine-code
$ Holmake

This should enable you to get a bit further. The machine-code example is pretty 
demanding — it helps to have a machine with lots of RAM.

Thanks,
Anthony

On 5 Apr 2014, at 19:31, Jiaqi Tan  wrote:

> Hi Anthony,
> 
> I checked my installation of HOL, minisat was successfully compiled and the 
> blastlib test did not use the internal prover.
> 
> I downloaded a clean version of HOL from github and recompiled it, and after 
> that, my compilation of examples/machine-code was not getting stuck anymore. 
> However, I encountered the compile error below:
> 
> /Users/jiaqi/code/HOL.latest/bin/Holmake: Finished recursive invocation in 
> /Users/jiaqi/code/HOL.latest/examples/machine-code/instruction-set-models/x86_64
> Analysing codegenLib.sig
> Trying to create directory .HOLMK for dependency files
> Analysing codegenLib.sml
> Analysing codegen_armLib.sig
> Analysing codegen_inputLib.sig
> Analysing codegen_ppcLib.sig
> Analysing codegen_x64Lib.sig
> Analysing codegen_x86Lib.sig
> Analysing codegen_armLib.sml
> Analysing codegen_inputLib.sml
> Analysing codegen_ppcLib.sml
> Analysing codegen_x64Lib.sml
> Analysing codegen_x86Lib.sml
> Analysing compilerLib.sig
> Analysing compilerLib.sml
> Analysing reg_allocLib.sig
> Analysing reg_allocLib.sml
> /Users/jiaqi/code/HOL.latest/bin/Holmake: Finished recursive invocation in 
> /Users/jiaqi/code/HOL.latest/examples/machine-code/compiler
> /Users/jiaqi/code/HOL.latest/bin/Holmake: Recursively calling Holmake in 
> /Users/jiaqi/code/HOL.latest/examples/machine-code/compiler/demo
> Analysing compiler_demoScript.sml
> Trying to create directory .HOLMK for dependency files
> /Users/jiaqi/code/HOL.latest/bin/buildheap -o local-hol-heap ../compilerLib
> Poly/ML 5.5.1 Release
> val heapname = "local-hol-heap": string
> 
> Loading ../compilerLib
> ld: warning: could not create compact unwind for _ffi_call_unix64: does not 
> use RBP or RSP based frame
> Linking compiler_demoScript.uo to produce theory-builder executable
> Poly/ML 5.5.1 Release
> Error- in 'poly/poly-init2.ML', line 156.
> Type error in function application.
>Function: Word.fromLargeWord : Word.largeword -> word
>Argument: (PolyWord8.toLargeWord w) : word
>Reason:
>   Can't unify Word.largeword (*Created from opaque signature*) with
>   word (*In Basis*) (Different type constructors)
> Found near Word.fromLargeWord (PolyWord8.toLargeWord w)
> Exception- Fail "Static Errors" raised
> Cannot find file compiler_demoScript.ui
> Cannot find file compiler_demoScript.ui
> /Users/jiaqi/code/HOL.latest/bin/Holmake: Failed script build for 
> compiler_demoScript - exited with code 1
> /Users/jiaqi/code/HOL.latest/bin/Holmake: Finished recursive invocation in 
> /Users/jiaqi/code/HOL.latest/examples/machine-code/compiler/demo
> Build failed in directory examples/machine-code/ (exited with code 1)
> 
> However, I do have compiler_demoScript.sml in 
> examples/machine-code/compiler/demo.
> 
> Thanks,
> Jiaqi
> 
> 
> 
> On Sat, Apr 5, 2014 at 5:29 AM, Anthony Fox  wrote:
> I think it’s more likely that there was a problem with building minisat under 
> the latest Mac OS. To check that it is installed, try going to the directory
> 
> HOL/src/HolSat/sat_solvers/minisat
> 
> There should be a binary “minisat” there. Alternatively, to make sure it is 
> working properly, you can try something like:
> 
> > load “blastLib”;
> ..
> > blastLib.BBLAST_PROVE ``?x y. x + y = 12w : word8``;
> 
> If you see the warning
> 
> HolSat WARNING: SAT solver not found. Using slow internal prover.
> To turn off this warning, type: set_trace "HolSatLib_warn" 0; RET
> 
> then that is the source of your problem.
> 
> I have a patch for the minisat sources, but it’s not been checked on other 
> platforms yet.
> 
> Anthony
> 
> On 5 Apr 2014, at 08:09, Ramana Kumar  wrote:
> 
> > I believe it takes several hours. I haven't done it myself though.
> >
> >
> > On Sat, Apr 5, 2014 at 3:23 AM, Jiaqi Tan  wrote:
> > Hi,
> >
> > I have downloaded the latest version of HOL from github, and my current 
> > build of examples/machine-code is taking quite a long time, and the build 
> > has been stuck in examples/machine-code/instruction-set-models/x86_64 for 
> > about an hour. I'm wondering if that's normal.
> >
> > I am using PolyML 5.5.1 on Mac OS X 10.9.2. I have built HOL (poly < 
> > tools/smart-conf

Re: [Hol-info] Proving with existentially quantified variable: Can witnesses be generated automatically for finite sets?

[Anthony Fox]

The tactic

  ACCEPT_TAC
(blastLib.BBLAST_PROVE
   ``?r:word8. 100w ≤₊ r + 251w ∧ r + 251w <₊ 200w``)

will prove your goal. If you’re doing this sort of thing a lot then you should 
consider wrapping this process up into a custom tactic.

- Anthony

On 27 Jun 2014, at 18:49, Jiaqi Tan  wrote:

> Hi,
> 
> Is it possible, using just the built-in HOL4 libraries/theorems, to 
> automatically generate witnesses for an existentially quantified theorem over 
> a finite set?
> 
> Specifically, I have theorems of the form:
> {r − 5w} ⊆ {a | 100w ≤₊ a ∧ a <₊ 200w}
> 
> Where the variable r is of type word8, and the set specification is also over 
> word8.
> 
> I tried simplifying using the following simplification sets:
> 
> SIMP_TAC (std_ss ++ ARITH_ss ++ wordsLib.WORD_ss ++ 
> pred_setSimps.PRED_SET_ss) []
> 
> And this yields the subgoal:
> val it =   [([],``∃r. 100w ≤₊ r + 251w ∧ r + 251w <₊ 200w``)]: goal list
> 
> Is it possible, using just the available theorems in the base HOL4 
> installation, to automatically discharge such existential goals of membership 
> in fixed size word sets?
> 
> Thank you!
> 
> Regards,
> Jiaqi Tan
> 
> 
> 
> --
> Open source business process management suite built on Java and Eclipse
> Turn processes into business applications with Bonita BPM Community Edition
> Quickly connect people, data, and systems into organized workflows
> Winner of BOSSIE, CODIE, OW2 and Gartner awards
> http://p.sf.net/sfu/Bonitasoft___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info


--
Open source business process management suite built on Java and Eclipse
Turn processes into business applications with Bonita BPM Community Edition
Quickly connect people, data, and systems into organized workflows
Winner of BOSSIE, CODIE, OW2 and Gartner awards
http://p.sf.net/sfu/Bonitasoft
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Proving with existentially quantified variable: Can witnesses be generated automatically for finite sets?

[Anthony Fox]

I’ve just added blastLib.BBLAST_PROVE_TAC, which calls blastLib.BBLAST_PROVE on 
the current goal.

If this bit-vector procedure succeeds in proving your goal then a witness 
(which is the one used for the proof) can be viewed by attempting to prove the 
goal’s negation. In this case:

> blastLib.BBLAST_PROVE ``!r:word8. ~(100w ≤₊ r + 251w ∧ r + 251w <₊ 200w)``;
Found counterexample:

r -> 112w

Exception-
   SAT_cex |- ¬(100w ≤₊ 112w + 251w ∧ 112w + 251w <₊ 200w) ⇔ F
   raised

This will work for ordinary propositional formula as well. For example:

> blastLib.BBLAST_PROVE ``a = b:bool``;

will give you “b" is F and “a" is T as the counterexample.

I’m not aware of other HOL4 decision procedures that can readily supply 
counterexamples, e.g. METIS_PROVE and numLib.ARITH_PROVE don’t.

Isabelle/HOL has much better support for this sort of thing:

http://www4.in.tum.de/~blanchet/nitpick.html

Others can probably comment on how well it does in producing counterexamples 
for arithmetic goals.

- Anthony

On 28 Jun 2014, at 02:56, Jiaqi Tan  wrote:

> Hi Anthony,
> 
> Thank you for the pointer! That works and I am able to prove the theorem.
> 
> Does blastLib (or any other HOL4 library) also support the generation of 
> witnesses for such theorems?
> 
> Thank you!
> 
> Regards,
> Jiaqi
> 
> 
> 
> On Fri, Jun 27, 2014 at 6:23 PM, Anthony Fox  wrote:
> The tactic
> 
>   ACCEPT_TAC
> (blastLib.BBLAST_PROVE
>``?r:word8. 100w ≤₊ r + 251w ∧ r + 251w <₊ 200w``)
> 
> will prove your goal. If you’re doing this sort of thing a lot then you 
> should consider wrapping this process up into a custom tactic.
> 
> - Anthony
> 
> On 27 Jun 2014, at 18:49, Jiaqi Tan  wrote:
> 
> > Hi,
> >
> > Is it possible, using just the built-in HOL4 libraries/theorems, to 
> > automatically generate witnesses for an existentially quantified theorem 
> > over a finite set?
> >
> > Specifically, I have theorems of the form:
> > {r − 5w} ⊆ {a | 100w ≤₊ a ∧ a <₊ 200w}
> >
> > Where the variable r is of type word8, and the set specification is also 
> > over word8.
> >
> > I tried simplifying using the following simplification sets:
> >
> > SIMP_TAC (std_ss ++ ARITH_ss ++ wordsLib.WORD_ss ++ 
> > pred_setSimps.PRED_SET_ss) []
> >
> > And this yields the subgoal:
> > val it =   [([],``∃r. 100w ≤₊ r + 251w ∧ r + 251w <₊ 200w``)]: goal list
> >
> > Is it possible, using just the available theorems in the base HOL4 
> > installation, to automatically discharge such existential goals of 
> > membership in fixed size word sets?
> >
> > Thank you!
> >
> > Regards,
> > Jiaqi Tan
> >
> >
> >
> > --
> > Open source business process management suite built on Java and Eclipse
> > Turn processes into business applications with Bonita BPM Community Edition
> > Quickly connect people, data, and systems into organized workflows
> > Winner of BOSSIE, CODIE, OW2 and Gartner awards
> > http://p.sf.net/sfu/Bonitasoft___
> > hol-info mailing list
> > hol-info@lists.sourceforge.net
> > https://lists.sourceforge.net/lists/listinfo/hol-info
> 
> 


--
Open source business process management suite built on Java and Eclipse
Turn processes into business applications with Bonita BPM Community Edition
Quickly connect people, data, and systems into organized workflows
Winner of BOSSIE, CODIE, OW2 and Gartner awards
http://p.sf.net/sfu/Bonitasoft
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] CROSS_applied thm.

[Anthony Fox]

The theorem comes from a custom version of store_thm, which was added in 
November 2012. See:

https://github.com/HOL-Theorem-Prover/HOL/commit/1de5add5520bcd6bc6b44258e5a3d881d5bb9a4c

It appears that this didn’t make it to the HOL4 K-8 release.

Anthony

> On 25 Oct 2014, at 17:09, Vincent Aravantinos 
>  wrote:
> 
> You might have an older version of HOL4. 
> I don't know when this theorem was introduced but if it was in HOL4 9 and you 
> have HOL4 8, that could explain it.
> If so, either switch to the latest version, or, if not possible, just copy 
> paste the proof in your own script (with potential dependencies).
> 
> --
> Vincent Aravantinos
> Analysis and Design of Dependable Systems
> fortiss GmbH 
> Guerickestrasse 25 | 80805 Munich | Germany
> 
> 
> Le 24 oct. 2014 à 18:16, Cvetan Dunchev  a écrit :
> 
>> Dear colleagues and friends,
>> 
>> I would like to inform you about the following problem: I want to use  
>> the CROSS_applied theorem from the pred_setTheory:
>> 
>> http://hol.sourceforge.net/kananaskis-9-helpdocs/help/src-sml/htmlsigs/pred_setTheory.html#CROSS_applied-val
>> 
>> Despite the fact that the theory is loaded, I got the following  
>> message in the console:
>> ! Toplevel input:
>> ! CROSS_applied;
>> ! ^
>> ! Unbound value identifier: CROSS_applied
>> 
>> and when I have a look at the corresponding source file, indeed such a  
>> theorem does not exist. Does anybody have an explanation about that?
>> 
>> Best regards,
>> Cvetan Dunchev
>> 
>> 
>> --
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
> --
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info


--
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info