Re: [Hol-info] proof replay?

Hi Dan, So, in a nutshell, you've got N proof scripts in HOL Light that you want to fit together as one coherent proof in a single session, but that would take far too much processing to do so in practice. So you want to execute these in N parallel HOL Light sessions, recording the

Re: [Hol-info] Visualizing subgoals in a proof script

Hi Mario, Yes, as Freek says, Tactician would do the sort of thing you need, but is only for HOL Light. It works on the vast majority of tactic proofs as they are typically written in HOL Light, say perhaps 1 in every 1,000 proof script lines might trip it up. It could be ported to HOL4,

Re: [Hol-info] grammar for HOL Light terms

And for HOL Zero there is Appendix C of the User Manual that gives a formal grammar of the HOL Zero concrete syntax. Again, this is fairly similar to HOL Light's and HOL4's, but there are numerous small differences. Note that the formal grammar hasn't actually been checked (as far as I'm

Re: [Hol-info] 0 / 0 = 0 ???

I think there is definitely an advantage in keeping ``x/y`` undefined (even granted that it will always be possible to prove ``?y. x/0 = y``), namely that it means that your proofs are much more likely to directly translate to other formalisms of real numbers where '/' is not total. Of course

Re: [Hol-info] String of term with type information?

Hi, I don't know of any function in HOL Light (although I'm don't know about most recent versions). To write your own, a simple approach would be to print primitive term syntax, with all constants and variables annotated with their type, and to put parentheses around everything at every

Re: [Hol-info] INST

Hi Michael, Yes, Konrad's right about how types are determined in term quotations, and I too don't know of an INST in HOL Light that unifies the types of its arguments. To get a listing of the types of the free variables in 'th', you can do: map dest_var (frees th);; or to return the type

Re: [Hol-info] Genesis of Church's simple theory of types, Wiedijk's criticism concerning the (current) HOL family

billion primitive inference steps. Another intended role is a pedagogical example of a basic HOL system, with a simple coding style and lots of code comments explaining what is going on, which also helps trustworthiness. Mark Adams. On 22/10/2016 03:41, Ken Kubota wrote: > … I have now ad

Re: [Hol-info] Type checking issue

Hello Abid, The term quotation fails type checking simply because the types of LHS and RHS of the equality are different: `:real^((N,P)finite_sum,Q)finite_sum^M` (with type vars N, P, Q, M) `:real^(N,(P,Q)finite_sum)finite_sum^M` (with type vars N, P, Q, M) As I understand it (I may be

Re: [Hol-info] A question about the theorem in HOL4?

It's a bit confusing. The expressions you enter in the session are not actually in HOL - they are in the functional programming language ML. This is the language used to implement HOL4. You are in an ML toplevel (also called "read-eval-print loop" or "REPL"), with HOL4 already incorporated. ML

Re: [Hol-info] Fwd: Re: HOL-Light Beginner Questions

you should get what you intend by transforming it to something logically equivalent, i.e. change "A ==> B ==> C" to "A /\ B ==> C". The error messages could be much better here. Mark. On 17/06/2016 10:51, Heiko Becker wrote: > Hello, > On 06/16/2016 01:45 PM

Re: [Hol-info] Fwd: Re: HOL-Light Beginner Questions

Hi Heiko, That's strange, your corrected version goes through fine on my computer. Do you still get the same problem if you restart HOL Light and enter the corrected script? What version of HOL Light are you using? Mark. On 16/06/2016 10:01, Heiko Becker wrote: > Forwarded Message

Re: [Hol-info] How to transform the proof form

For HOL Light I've got a tool called Tactician that would be ideal for that: http://www.proof-technologies.com/tactician/ but it doesn't work for HOL4. One day I hope to port it, but that's unlikely to be done in the near future. Mark. on 27/11/15 8:20 AM, Ada wrote: >

Re: [Hol-info] proof structure in Coq

it looks like perl.) >> >> Of course in Flyspeck many (most?) proofs are the other >> way around, where there is just a list of tactics that is >> processed like you would successively "e" them interactively. >> I think Mark Adams tactician is exactly

Re: [Hol-info] Question about camlp5

Hi Robert, Could you provide more information about the circumstances when it fails? Specifically, which versions of OCaml and Camlp5 are you using? Execute the following in a terminal window: ocaml -version camlp5 -v Does this error arise when building HOL Light from source in an OCaml

Re: [Hol-info] Theorems Produced by Type Definitions

Seems a good idea to me. Given ETA_AX, it's easy to show equivalence with current HOL Light, and it's always better to have closed formulae coming out of definition commands. One small point: the formulae as written in the linked message do not have the intended syntactic form (due to

Re: [Hol-info] advice on installing Ocaml, camlp5 HOL Light on Mac OS X 10.8.5?

...@math.unifi.it] Sent: 17 September 2014 08:15 To: Mark Adams Cc: Nela Cicmil; hol-info@lists.sourceforge.net Subject: Re: [Hol-info] advice on installing Ocaml, camlp5 HOL Light on Mac OS X 10.8.5? Hi Nela, I use the Nix package manager (http://nixos.org/nix/) and it works well for me

Re: [Hol-info] Learning HOL Light

Hi Bill, Have you tried looking at the HOL Zero source code? I think you will find it illustrative for your purposes. It has a simple core like HOL Light, but the source code explains more of what is going on. In file 'corethy.ml' I try to motivate the axioms and constant definitions used in

Re: [Hol-info] Learning HOL Light

Hi Bill, on 21/3/14 6:19 AM, Bill Richter rich...@math.northwestern.edu wrote: ... T = ((λxbool . x) = (λxbool . x)) So it looks to me that HOL Light is defining Tom's primitive = in terms of the Ocaml =. Is that correct? And maybe that just means that the HOL Light primitive = is

Re: [Hol-info] Learning HOL Light

I should have said '@' instead of '?' here. The constant '?' is actually defined in these axiomatisations (using '@'). Mark. on 21/3/14 9:10 AM, Mark Adams m...@proof-technologies.com wrote: ... In HOL Light's axiomatisation, the only such entities are the 'bool' and 'fun' type constants

Re: [Hol-info] Learning HOL Light

Hi Bill, on 21/3/14 4:28 PM, Bill Richter rich...@math.northwestern.edu wrote: ... BTW where is the constant = defined in HOL Light? I see now that the line in bool.ml override_interface (=,`(=):bool-bool-bool`);; just means that = is being defined as a synonym for = in this special case.

Re: [Hol-info] More on set comprehensions

Not wanting to be too picky here (because I very much agree with the thrust of what Rob is saying), but isn't ProofPower term quotation parsing sensitive to the subgoal package state (specifically, free variables in term quotations pick up the types of existing free variables in the subgoal

Re: [Hol-info] Trouble building HOL light

Oops. That last email contains an error in the detail. The HOL Light adaption of 'plexer.ml' and 'pa_o.ml' is called 'pa_j.ml'. Mark. on 15/10/13 2:29 PM, Mark Adams m...@proof-technologies.com wrote: Hi Rob, Yes, you not only need a sufficiently recent version of Camlp5 for your version

[Hol-info] HOL glossary

to suggestions for improvement and/or debate about appropriate choice of names/descriptions/scope. Mark Adams -- Benefiting from Server Virtualization: Beyond Initial Workload Consolidation -- Increasing the use