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] 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] 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=/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=/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=/4140
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

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=/4140
___
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 tanji...@cmu.edu 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 ac...@cam.ac.uk 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 tanji...@cmu.edu 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] 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 ram...@member.fsf.org 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 tanji...@cmu.edu 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
 HOL message: Created theory prog_x64_extra
 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 jia...@andrew.cmu.edu 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 ac...@cam.ac.uk 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 ram...@member.fsf.org 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 tanji...@cmu.edu 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
  HOL message: Created theory prog_x64_extra
  Saved definition

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 ramana.ku...@cl.cam.ac.uk 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=121051231iu=/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 oschw...@kth.se 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=119420431iu=/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=119420431iu=/4140/ostg.clktrk
___
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 r...@lemma-one.com 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}``;
 HOL message: inventing new type variable names: 'a
 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=84349831iu=/4140/ostg.clktrk___
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 konrad.sl...@gmail.com 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. bsc.j@gmail.com 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] 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 hn_nemati1...@yahoo.com 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] 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 ramana.ku...@cl.cam.ac.uk 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] 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 hn_nemati1...@yahoo.com 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] 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 ramana.ku...@gmail.com 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] 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] 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] 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.


HOL message: inventing new type variable names: 'a


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] 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] 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 ``my BIG input``;

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 ``my BIG input``;
 
 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] 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] 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] 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