Re: [Hol-info] proof replay?

[Mark Adams]

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 
kernel-level steps as they happen, and export these, and replay them all 
in a single HOL Light session.


This is basically known as "proof recording", and an exported proof is 
known as a "proof object".  There have been various attempts at proof 
recording in HOL Systems over the years, including Wong (1990s), 
Skalberg & Obua (2000s), Kaliszyk & Krauss (2010s), Hurd's Open Theory 
project (2010s) and my Common HOL project (2010s).  Section 4.5 of my 
paper on proof auditing includes a brief overview of these.  As you say, 
most recording systems are designed for either porting proofs between 
two specific proof systems (either two proof assistants or a proof 
assistant and its sister proof checker), but Open Theory and Common HOL 
were designed for porting between any two HOL systems (including back 
into the same system).


You're absolutely right that the replay has potential to be much faster 
than executing the original proof scripts, given that search does not 
need to be replicated during replay.  But there are numerous challenges 
to overcome to make it tractable.  Even though a basic proof recording 
system can be written in a few hundred lines of ML, recording a large 
proof would probably use up huge amounts of RAM/diskspace, and probably 
not result in that much of a speed up during replay.  However, some 
recording systems do much better than that.  I'm not sure about the 
latest developments for other systems, but back in 2015 my recording 
system for Common HOL recorded the "text formalisation" part of Flyspeck 
in HOL Light (1.3bn primitive proof steps) using modest RAM/CPU, and 
managed to get replay in HOL Light down by a factor of 7, and I think 
that this could go down by another factor of 2 (so perhaps 15 in total) 
with a bit of extra work, but this is nowhere near the 100x speedup you 
envisage.  Would that meet your requirements?  May I ask what the 
application is?


Mark.


On 25/01/2021 13:40, D. J. Bernstein wrote:

I have another newbie question regarding HOL Light; again happy to hear
about other HOL variants if those have easier answers.

I'm in the typical post-human-proof situation where a program found a
"proof" that's too tedious for a human to verify (in the conventional
sense, not PCPs). For verification, I'm converting the "proof" into a
HOL Light proof: auto-generating the whole chain of intermediate steps
as definitions, and auto-generating all the theorems linking the
definitions. This works fine on scaled-down examples, and extrapolation
suggests that the CPU time for HOL Light will still be affordable when
scaled up to the full theorem, in the ballpark of 1 core-hours.

It's no problem to farm the separate proof steps out to separate cores,
each using its own subset of the relevant definitions, at which point I
have one instance of HOL Light printing out a theorem saying A implies
B, and a separate instance of HOL Light printing out a theorem saying B
implies C, and so on. This brings me to the question: how can I have 
HOL
Light printing out the combined theorem saying that A implies Z, 
without

waiting 1 hours for HOL Light on one core to serially run through
proving all the lemmas?

I'd guess that >99% of the CPU time I'm seeing comes from HOL Light
searching for proofs (e.g., the computation in REAL_LINEAR_PROVER), and
that far less is spent by the HOL Light kernel verifying the proofs. Is
there a generic mechanism to record merely what the kernel is doing---
i.e., to automatically write down a proof in the conventional sense---
and then replay this proof in another HOL Light instance that has the
same definitions?

The papers I've found on the problem of exporting libraries of theorems
from one system to another sound like that's only partially solved, but
that's also a conceptually more difficult problem than simply replaying
the lowest level of proof within a single system. I did various other
searches for answers and didn't find anything---sorry if I missed
something obvious. In general the small kernel makes me think that
tracing proofs wouldn't be touching many lines of code, but I haven't
studied the kernel closely enough to be confident about this.

In case this (1) doesn't exist and (2) is hard to build, my backup plan
is to modify the program printing out the proof tactics to do its own
searches for lower-level proof steps. Conceptually this would be 
copying

the searches implemented in HOL Light, so presumably the speed will end
up similar, but the searches would then be easily distributable
precomputation, which is the objective---I'd just like to reach this
without the waste of time of reimplementing something that HOL Light
already knows how to do!

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

[Mark Adams]

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, but 
this would not be easy to get working as well as it does for HOL Light, 
because it plays about with the innards of OCaml and equivalent tweaking 
of PolyML would be required.


Mark.

On 07/08/2020 10:02, Freek Wiedijk wrote:

Dear Mario,

Hello. In HOL4 is there a way to generate something like the entries 
in

Metamath proof explorer for the subgoals generated within a proof and
the tactics used to solve them? Example:



For HOL Light there is Mark Adams's "tactician" which
I expect would make something like this possible (even
though I expect it only would work on the majority of
proofs, and not be guaranteed to work on all of them).
But that's HOL Light, not HOL4.

Freek



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

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

[Mark Adams]

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 aware) by a parser generator.


  http://www.proof-technologies.com/holzero/

Mark.

On 09/11/2019 15:48, Petros Papapanagiotou wrote:

Hi Brando,

The HOL4 description manual has quite a bit of information, a lot of
which is shared with HOL Light:
http://sourceforge.net/projects/hol/files/hol/kananaskis-13/kananaskis-13-description.pdf/download

I am not sure if there is a similar document for HOL Light.

You can see the HOL Light term structure as it is defined here:
https://github.com/jrh13/hol-light/blob/a1ca1f31539c8e9bd40d324c14951e3c76836787/fusion.ml#L99

Hope this helps!

Regards,
Petros

On 08/11/2019 15:48, Miranda, Brando wrote:


Hi,

This is my first message to the HOL list so hope its not out of the
rules for the list (couldn’t find the rules).

I wanted to find the formal grammar for generating terms (formulas)
in HOL (Light). I was wondering were I could find such a
specification?

Thanks!

Brando

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


--
Dr. Petros Papapanagiotou
Chancellor's Fellow in Digital Technologies
CISA, School of Informatics, The University of Edinburgh

Academic Coordinator
IoT Research & Innovation Service

http://homepages.inf.ed.ac.uk/ppapapan/

---
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
___
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] 0 / 0 = 0 ???

[Mark Adams]

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 there is also a disadvantage, in that it makes proof harder.  
But then, arguably, being forced to justify that we are staying within 
the "normal" domain of the function is probably a good thing (in a 
similar way as being forced to conform to a type system is a good 
thing).  I understand that, historically, it is this disadvantage of 
harder proofs that was the reason for making ``0/0=0`` in HOL.  It's 
much easier for automated routines if they don't have to consider side 
conditions.


Mark.

On 15/02/2019 08:56, Chun Tian (binghe) wrote:

Thanks to all kindly answers.

Even I wanted ``0 / 0 = 0`` to be excluded from at least
"extreal_div_def" (in extrealTheory), I found no way to do that. All I
can do for now is to prevent ``0 / 0`` in all my proofs - whenever it's
going to happen, I do case analysis instead.

--Chun

Il 14/02/19 18:12, Konrad Slind ha scritto:

It's a deliberate choice. See the discussion in Section 1.2 of

http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=775DBF504F7EE4EE28CC5169488F4190?doi=10.1.1.56.4692=rep1=pdf



On Thu, Feb 14, 2019 at 10:40 AM Chun Tian (binghe)
mailto:binghe.l...@gmail.com>> wrote:

Hi,

in HOL's realTheory, division is defined by multiplication:

[real_div]  Definition

      ⊢ ∀x y. x / y = x * y⁻¹

and zero multiplies any other real number equals to zero, which is
definitely true:

   [REAL_MUL_LZERO]  Theorem

      ⊢ ∀x. 0 * x = 0

However, above two theorems together gives ``0 / 0 = 0``, as shown
below:

> REWRITE_RULE [REAL_MUL_LZERO] (Q.SPECL [`0`, `0`] real_div);
val it = ⊢ 0 / 0 = 0: thm

How do I understand this result? Is there anything "wrong"?

(The same problems happens also in extrealTheory, since the 
definition

of `*` finally reduces to `*` of real numbers)

Regards,

Chun Tian

___
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] String of term with type information?

[Mark Adams]

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 level.  This would be 
unreadable for anything but small terms, but would parse back in.


However, even this would have its problems:
(1) If you have generated type variables (e.g. `:?20147`) then HOL Light 
cannot parse these back in;
(2) Any irregular names of constants and variables would cause problems 
for the parser;

(3) Variables overloaded with constants would not get parsed properly.

But I suppose you are assuming that the original term was successfully 
parsed in by HOL Light's parser.  If so, then only (1) is a problem.


Mark.


But other if you are not concerned about type variables,

On 29/06/2018 15:26, Yaqing Jiang wrote:

Hi,

Anyone knows if there is a function in HOL Light that convert terms to
strings so that I can save the term and load it the next time?

If I do string_of_term `x:num` I only got "x", but I need "x:num". If
there's none I'll make one myself anyway.

Thanks


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

[Mark Adams]

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 of a given variable, where 'x' is the variable 
name:

   assoc x (map dest_var (frees th));;

Mark.

On 07/01/2018 17:36, Konrad Slind wrote:

Hi Michael,

  What I think is happening is that each quoted element is being
parsed separately.
This means that the type of the x in `x` is a type variable while the 
type

of `2` is :num. Since INST (I think) just fails if the two types
aren't identical,
you get the displayed behaviour. There may well be a version of INST in
Hol Light that normalizes the arguments but I don't know it.

Konrad.


On Thu, Jan 4, 2018 at 8:04 PM, Michael Beeson  
wrote:

an example from the tutorial

let th1 = REFL `x+1`;;

val th1 : thm = |- x + 1 = x + 1

# let th3 = INST [`2`,`x:num`] th1;;

val th3 : thm = |- 2 + 1 = 2 + 1

Fine.  But if we leave off the type information about x it doesn't 
work.


# let th3 = INST [`2`,`x`] th1;;

Warning: inventing type variables

Exception: Failure "vsubst: Bad substitution list".

I don't understand why this fails.   In general you might not
know what type x has in th1  (eg.,  has prioritize_real() or
prioritize_vector()  been done just before this?) .Is there
a command I can issue to ask for "the type of `x` in th1 " ?

Michael Beeson

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


--
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] Genesis of Church's simple theory of types, Wiedijk's criticism concerning the (current) HOL family

[Mark Adams]

Hello Ken,

Not wanting to crowd your diagram too much, but I think maybe HOL Zero 
(my system!) deserves a mention.  It is a bare bones implementation of 
the logic, and is designed to be highly trustworthy and robust.

   http://www.proof-technologies.com/holzero.html

It can be used to create simple natural deduction proofs, but is mainly 
intended as a proof checker to replay (via some proof recording 
mechanism) formal proofs performed on other systems.  It has 
successfully replayed two quarters of the Flyspeck Project, for example, 
that were originally performed in HOL Light in 1.4 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 added the quotes on the genesis of Church's simple theory 
> of types,
> and on the invention of λ-calculus and the origin of the λ-notation
> in the "Historical Notes" section at:
>   http://dx.doi.org/10./100.111
> 
> Also interesting might be Freek Wiedijk's criticism
> concerning the (current) HOL family quoted in the "Criticism" section.
> 
> Ken Kubota
> 
> 
> 
> Ken Kubota
> doi: 10./100
> http://dx.doi.org/10./100
> 
> 
> 
>> Anfang der weitergeleiteten Nachricht:
>> 
>> Von: Ken Kubota <m...@kenkubota.de>
> 
>> Concerning Roger Jones' remarks, let me first note that a legend 
>> ("significance of the shape of boxes")
>> can be found on top of the 2nd page, as it doesn't fit on the first 
>> anymore.
>> 
>> Please also note the arrow from lambda calculus (LC) to simple type 
>> theory (STT), narrowing the
>> interest to theories based on LC. The purpose is mainly to distinguish 
>> the logics based on LC
>> by their expressiveness in terms of their syntactic features, where 
>> STT is characterized by having no
>> type variables in their object language at all. From this perspective, 
>> the very early developments
>> prior to LC can be neglected, as Church's 1940 paper is the today's 
>> standard reference.
>> For me, even Church's 1940 logic is baroque, as I grew up with 
>> Andrews' Q0, which is much more
>> elegant, cleaner, and natural.
>> However, for historical accuracy, I already considered adding a quote 
>> mentioning Ramsey and Chwistek from
>>  
>> http://www.users.waitrose.com/~hindley/SomePapers_PDFs/2006CarHin,HistlamRp.pdf
>>  
>> (p. 12)
>> in the Historical Notes section. Note that Church mentions both, and 
>> Carnap, in the first footnote
>> of his 1940 article.
> 
> 
>>> Am 18.10.2016 um 15:34 schrieb Roger Bishop Jones <r...@rbjones.com>:
> 
>>> Credit for the Simple Theory of Types
>>> ===
>>> 
>>> Ken's diagram makes it look like this theory begins with Church.
>>> 
>>> Its not entirely uncontroversial as to who should have credit for 
>>> devising this system.
>>> Most frequently credit has been given to Ramsey, but though he seems 
>>> to have had the
>>> idea pretty early on, he never formulated the logical system in 
>>> detail (and one might think
>>> that the idea of simplifying Russell's ramified theory would have 
>>> occurred to others).
>>> 
>>> Recent scholarship suggests that the first fully detailed account of 
>>> STT as a formal
>>> system is due to Rudolf Carnap, who, in the course of writing a 
>>> logistics textbook
>>> to facilitate the application of formal logic in mathematics and 
>>> science, decided to
>>> base it around the simplified rather than the ramified type theory.
>>> I think this particular formulation may have escaped attention 
>>> because the book
>>> "Abriss der Logistik" was written in German and has never been 
>>> translated into
>>> English.
>>> Until recently the more widely know text by Hilbert and Ackermann was 
>>> thought
>>> to be the first formal account of the simple theory of types.
>>> STT appears I  believe, only in the second edition of their text, so 
>>> though the
>>> first edition (1928) precedes Carnap's (1929) text, he still was in 
>>> first with STT.
>>> There were many later textbooks which presented this version of STT
>>> (not based on the lambda-calculus and having "power set" as the 
>>> primitive
>>> type constructor), which was prob

Re: [Hol-info] Type checking issue

[Mark Adams]

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 wrong here), there is no way of getting the
HOL type system to let you express this associativity property about
'horz_conct1'.  If you want to express these kinds of properties, I
think you need to define your function in a different way, not using
types like this.

Mark.

On 02/07/2016 10:30, Abid Rauf wrote:

> Dear All, 
> 
> I am having the following type checking issue with a definition in the Matrix 
> theory of HOL-Light. It seems the double application of the function leads to 
> an unknown dimension of the matrix, which is causing the problem. I would 
> appreciate if someone can please help me out with us. 
> 
> let horz_conct1 = new_definition
> `(horz_conct1:real^N^M->real^P^M->real^((N,P)finite_sum)^M) A B = lambda a b 
> . 
> if (b<=dimindex(:N)) 
> then (A$a$b) else (B$a$(b-(dimindex(:N`;; 
> 
> Now if i want to prove that 
> 
> g`!(A:real^N^M) (B:real^P^M) (C:real^Q^M). horz_conct1 (horz_conct1 A B) (C)= 
> horz_conct1 (A) (horz_conct1 B C)`;; 
> 
> it gives following error 
> 
> Exception: Failure "typechecking error (initial type assignment)".
> 
> So the definition is accepted but the proof goal using the function gives the 
> problem. 
> 
> Best Regards, 
> 
> Abid Rauf 
> Ph.D Scholar (CS) & RA SAVe Labs,
> School of Electrical Engineering and Computer Science (SEECS),
> National University of Science and Technology (NUST), H-12, Islamabad, 
> Pakistan 
> --
> Attend Shape: An AT Tech Expo July 15-16. Meet us at AT Park in San
> Francisco, CA to explore cutting-edge tech and listen to tech luminaries
> present their vision of the future. This family event has something for
> everyone, including kids. Get more information and register today.
> http://sdm.link/attshape 
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info--
Attend Shape: An AT Tech Expo July 15-16. Meet us at AT Park in San
Francisco, CA to explore cutting-edge tech and listen to tech luminaries
present their vision of the future. This family event has something for
everyone, including kids. Get more information and register today.
http://sdm.link/attshape___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

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

[Mark Adams]

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 expressions that you enter in the session get
evaluated by the toplevel.  These may include standard library functions
that are provided by ML, or functions provided by HOL4, or a mixture of
both.  This is a very powerful paradigm, and allows the user to extend
the theorem prover as much as they like with their own facilities.

You are able to input HOL expressions (called "terms") by surrounding
them with two backquote characters at the start and end, like this:
`` FST (1,2) ``;
which results in:
val it = ``FST (1,2)``: term

  Inference rules are provided by HOL4 as ML functions that return
theorems, for example 'REWRITE_CONV':
REWRITE_CONV [pairTheory.FST] ``FST (1,2)``;
results in:
val it = |- FST (1,2) = 1: thm

As Ramana says, there happens to be an ML function called 'fst', which
directly corresponds to the HOL function 'FST'.  But when you enter the
following into the ML session:
fst (1,2);
to result in
val it = 1: int
you are not doing theorem proving, you are just doing functional
programming.

Hope this makes sense.

Mark.

On 22/06/2016 09:24, Ramana Kumar wrote:

> FST is a function in logic, not in ML.
> 
> In this case, there does happen to be a similar function, called fst, in ML.
> 
> Are you trying to specify/prove something in logic? Or are you trying to 
> write an ML program? 
> 
> On 22 June 2016 at 18:21, Ada <956066...@qq.com> wrote:
> 
>> Hi,guys 
>> I am working with HOL4.  
>> FST is in pairTheory, its definition is
>> 
>> [FST]  Theorem
>> 
>> |- ∀x y. FST (x,y) = x
>> 
>> But, When I use it  like following:
>> 
>> val n = FST (1,2);
>> 
>> It responses:
>> 
>> ! Toplevel input:
>> ! val n = FST (1,2);
>> ! ^^^
>> ! Type clash: expression of type
>> !   thm
>> ! cannot have type
>> !   'a -> 'b
>> 
>> What is the reason? Does anyone know how to use it?
>> 
>> Thanks! 
>> --
>> Attend Shape: An AT Tech Expo July 15-16. Meet us at AT Park in San
>> Francisco, CA to explore cutting-edge tech and listen to tech luminaries
>> present their vision of the future. This family event has something for
>> everyone, including kids. Get more information and register today.
>> http://sdm.link/attshape
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
> 
> --
> Attend Shape: An AT Tech Expo July 15-16. Meet us at AT Park in San
> Francisco, CA to explore cutting-edge tech and listen to tech luminaries
> present their vision of the future. This family event has something for
> everyone, including kids. Get more information and register today.
> http://sdm.link/attshape 
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info--
Attend Shape: An AT Tech Expo July 15-16. Meet us at AT Park in San
Francisco, CA to explore cutting-edge tech and listen to tech luminaries
present their vision of the future. This family event has something for
everyone, including kids. Get more information and register today.
http://sdm.link/attshape___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

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

[Mark Adams]

I think the problem now is that the syntactic form of the HOL term you
supply to 'new_inductive_definition' does not fit what is allowed by the
command, because you are not allowed to have compound implications (see
the HOL Light reference manual entry for 'new_inductive_definition'). 
So I think 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, Mark Adams wrote: 
> 
>> 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.
> 
> It turns out, that I accidentally loaded both commands. The sstep definition 
> and the next one. And the failure came from the next one. But I am unable to 
> fix it currently:
> 
> let bstep_RULES, bstep_INDUCT, bstep_CASES = new_inductive_definition
> `(!(x:num) (e:exp) (s1:cmd) (s2:cmd) (env:num->real) (v:real).
> exp_eval e env = v ==>
> bstep s1 (upd_env x v env) s2 ==>
> bstep (Ass x e s1) env s2) /\
> (!(c:bexp) (s1:cmd) (s2:cmd) (t:cmd) (env:num->real).
> bval c env = T ==>
> bstep s1 env s2 ==>
> bstep (Ite c s1 t) env s2) /\
> (!(c:bexp) (s:cmd) (t1:cmd) (t2:cmd) (env:num->real).
> bval c env = F ==>
> bstep t1 env t2 ==>
> bstep (Ite c s t1) env t2)`;;
> Exception: Failure "dest_var: not a variable".
> 
> I have tried removing some parts of the definition to see if I have an 
> undefined variable lying around but could not arrive at some obvious failure.
> 
> Best regards,
> 
> Heiko
> 
> On 16/06/2016 10:01, Heiko Becker wrote: 
> 
>  Forwarded Message  
> 
> SUBJECT:
> Re: [Hol-info] HOL-Light Beginner Questions
> 
> DATE:
> Thu, 16 Jun 2016 10:59:44 +0200
> 
> FROM:
> Heiko Becker <heikobecke...@gmail.com>
> 
> TO:
> Ramana Kumar <ramana.ku...@cl.cam.ac.uk>
> 
> CC:
> hol-info <hol-info@lists.sourceforge.net>
> 
> On 06/16/2016 01:57 AM, Ramana Kumar wrote: 
> I expect it could be because the Boolean constants are spelled "T" and "F" 
> rather than "true" and "false" in the logic, so the latter are being treated 
> as free variables. 
> 
> Thank you for your explanation. I am getting closer to getting my definition 
> working.
> I have changed it as follows:
> 
> let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition
> `(!x e s env v. exp_eval e env = v ==> sstep (Ass x e s) env s (upd_env x v 
> env)) /\
> (!c s t env. bval c env = T ==> sstep (Ite c s t) env s env) /\
> (!c s t env. bval c env = F ==> sstep (Ite c s t) env t env)`;;
> 
> But now HOL-Light complains about some construct not being a variable:
> Exception: Failure "dest_var: not a variable".
> 
> Can you maybe help me again?
> 
> Best regards,
> 
> Heiko
> 
> On 16 June 2016 at 01:09, Heiko Becker <heikobecke...@gmail.com> wrote:
> 
> My formalization:
> 
> let exp_INDUCT, exp_REC= define_type
> "exp = Var num
> | Const real
> | Plus exp exp
> | Sub exp exp
> | Mult exp exp
> | Div exp exp";;
> 
> let exp_eval_SIMPS = define
> `(exp_eval (Var x) E = E x) /\
> (exp_eval (Const r) E = r) /\
> (exp_eval (Plus e1 e2) E = (exp_eval e1) E + (exp_eval e2) E) /\
> (exp_eval (Sub e1 e2) E = (exp_eval e1) E - (exp_eval e2) E) /\
> (exp_eval (Mult e1 e2) E = (exp_eval e1) E * (exp_eval e2) E) /\
> (exp_eval (Div e1 e2) E = (exp_eval e1) E / (exp_eval e2) E)`;;
> 
> let bexp_INDUCT, bexp_REC = define_type
> "bexp = leq exp exp
> | less exp exp";;
> 
> let bval_SIMPS = define
> `(bval (leq e1 e2) (E:num->real) = (exp_eval e1 E) <= (exp_eval e2 E)) /\
> (bval (less e1 e2) E = (exp_eval e1 E) < (exp_eval e2 E))`;;
> 
> let cmd_INDUCT, cmd_REC = define_type
> "cmd = Ass num exp cmd
> | Ite bexp cmd cmd
> | Nop";;
> 
> let upd_env_simps1 = define
> `upd_env (x:num) (v:real) (E:num->real) =(\y. if y = x then v else E
> y)`;;
> 
> let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition
> `(!x e s E v. exp_eval e E = v ==> sstep (Ass x e s) E s (upd_env x v
> E)) /\
> (! c s t E. bval c E = true ==> sstep (Ite c s t) E s E) /\
> (! c s t E. bval c E = false ==> sstep (Ite c s t) E t E)`;;
> 
> When loading the sstep definitions I get the following failure:
> Exception: Failure "new_definiti

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

[Mark Adams]

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  
> 
> SUBJECT:
> Re: [Hol-info] HOL-Light Beginner Questions
> 
> DATE:
> Thu, 16 Jun 2016 10:59:44 +0200
> 
> FROM:
> Heiko Becker 
> 
> TO:
> Ramana Kumar 
> 
> CC:
> hol-info 
> 
> On 06/16/2016 01:57 AM, Ramana Kumar wrote: 
> 
>> I expect it could be because the Boolean constants are spelled "T" and "F" 
>> rather than "true" and "false" in the logic, so the latter are being treated 
>> as free variables.
> 
> Thank you for your explanation. I am getting closer to getting my definition 
> working.
> I have changed it as follows:
> 
> let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition
> `(!x e s env v. exp_eval e env = v ==> sstep (Ass x e s) env s (upd_env x v 
> env)) /\
> (!c s t env. bval c env = T ==> sstep (Ite c s t) env s env) /\
> (!c s t env. bval c env = F ==> sstep (Ite c s t) env t env)`;;
> 
> But now HOL-Light complains about some construct not being a variable:
> Exception: Failure "dest_var: not a variable".
> 
> Can you maybe help me again?
> 
> Best regards,
> 
> Heiko
> 
> On 16 June 2016 at 01:09, Heiko Becker  wrote:
> 
> My formalization:
> 
> let exp_INDUCT, exp_REC= define_type
> "exp = Var num
> | Const real
> | Plus exp exp
> | Sub exp exp
> | Mult exp exp
> | Div exp exp";;
> 
> let exp_eval_SIMPS = define
> `(exp_eval (Var x) E = E x) /\
> (exp_eval (Const r) E = r) /\
> (exp_eval (Plus e1 e2) E = (exp_eval e1) E + (exp_eval e2) E) /\
> (exp_eval (Sub e1 e2) E = (exp_eval e1) E - (exp_eval e2) E) /\
> (exp_eval (Mult e1 e2) E = (exp_eval e1) E * (exp_eval e2) E) /\
> (exp_eval (Div e1 e2) E = (exp_eval e1) E / (exp_eval e2) E)`;;
> 
> let bexp_INDUCT, bexp_REC = define_type
> "bexp = leq exp exp
> | less exp exp";;
> 
> let bval_SIMPS = define
> `(bval (leq e1 e2) (E:num->real) = (exp_eval e1 E) <= (exp_eval e2 E)) /\
> (bval (less e1 e2) E = (exp_eval e1 E) < (exp_eval e2 E))`;;
> 
> let cmd_INDUCT, cmd_REC = define_type
> "cmd = Ass num exp cmd
> | Ite bexp cmd cmd
> | Nop";;
> 
> let upd_env_simps1 = define
> `upd_env (x:num) (v:real) (E:num->real) =(\y. if y = x then v else E
> y)`;;
> 
> let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition
> `(!x e s E v. exp_eval e E = v ==> sstep (Ass x e s) E s (upd_env x v
> E)) /\
> (! c s t E. bval c E = true ==> sstep (Ite c s t) E s E) /\
> (! c s t E. bval c E = false ==> sstep (Ite c s t) E t E)`;;
> 
> When loading the sstep definitions I get the following failure:
> Exception: Failure "new_definition: term not closed".

Forwarding my message. Send from wrong mail account intially.

--
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.
http://pubads.g.doubleclick.net/gampad/clk?id=1444514421=/41014381 
___
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. http://pubads.g.doubleclick.net/gampad/clk?id=1444514421=/41014381___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

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

[Mark Adams]

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:

> Hey guys,
>
> I am learning to use HOL. Here is some code.
>
> load "abs_tools";
>
> open abs_tools;
> val _ = type_abbrev ("num_field", ``:complex -> bool``);
> (* -- *)
> (* Definition of number field.*)
> (* -- *)
>
> val s = ``s : num_field``;
>
> val nf_carrier = ``s SUBSET univ(:complex) /\ s <> {}:complex -> bool``;
> val nf_constant = ``0c IN s /\ 1c IN s``;
> val nf_operation = ``!a:complex b:complex.  a IN s /\ b IN s
> ==> (a+b IN s) /\ (a-b IN s) /\
> (a*b IN s)
> /\ (if a <> 0 then b/a IN s
> else a = 0c)``;
>
> val is_num_field_def = Define `
> num_field ^s =
> ^nf_carrier
> /\ ^nf_constant
> /\ ^nf_operation `;
> (* We work on an abstract number field s *)
>
> val _ = set_assums [ ``num_field ^s`` ];
>
> (* prove the coditions of number field *)
>
> val nf_proj_tac =
>
> POP_ASSUM MP_TAC THEN RW_TAC arith_ss [is_num_field_def] THEN STRIP_TAC;
> val carrier =
>
> asm_store_thm("carrier",nf_carrier,nf_proj_tac);
> val constant =
>
> asm_store_thm("constant",nf_constant,nf_proj_tac);
> val operation =
> asm_store_thm("operation",nf_operation,nf_proj_tac);
>
> Now, I want to write the prove in another way. For example, how to
> transform
>
> "val carrier =
>
> asm_store_thm("carrier",nf_carrier,nf_proj_tac); "
>
> into the form of
>
> "g(...)
> e(...)
> e(...)
> "
> Thanks! --Wish.
>
>
> 
>
>

> --
>
>
>
> 
> ___
> 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] proof structure in Coq

[Mark Adams]

Just to be clear, Tactician (only for HOL Light at the moment) goes between
the three styles:
 - g and e
 - prove with THEN/THENL/etc
 - Flyspeck's 'prove_by_refinement', which is a hybrid of the above two

Mark.

on 18/11/15 8:54 AM, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> wrote:

> I usually use ">>" instead of literally "THEN". Arguably that's still too
> much "shift".
>
> Yes I think you're right about tactician - it's for going back and forth
> between those styles.
>
> On 18 November 2015 at 08:41, Freek Wiedijk <fr...@cs.ru.nl> wrote:
>
>> Hi Ramana,
>>
>> >Apparently Coq somewhat recently gained the ability to be explicit about
>> >proof structure:
>>
>http://poleiro.info/posts/2013-06-27-structuring-proofs-with-bullets.html
>> >(Of course that comes naturally when using tacticals like THEN, THEN1,
>> etc.)
>>
>> Not _very_ recently.  It was introduced in 8.4, which is
>> from late 2011.  And maybe Ssreflect had it long before
>> that already?  (In my opinion Ssreflect is a much underrated
>> proof language, even if 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 about converting
>> a THEN-THEN proof to that format?
>>
>> But I agree that a more structured "bulleted" proof is nicer.
>> Even though ergonomically of course having to type THEN
>> is monstrous.
>>
>> Freek
>>
>
>
>
> 
>
>

> --
>
>
>
> 
> ___
> 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] Question about camlp5

[Mark Adams]

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
session?  Are you starting the session from scratch, or rebuilding HOL Light
on top of an existing session that had HOL Light already built?

Are you using a very recent download of HOL Light?  Do you know the SVN
release number, or roughly the date you downloaded?

Mark.

on 28/5/15 7:13 PM, Robert White ai.robert.wangsh...@gmail.com wrote:

 Dear all,

 I wonder if there is a way I can get rid of the error of :
 Error: Unbound value set_jrh_lexer

 Sometimes it is working sometimes it is not. I am very confused.
 Is there any advice?

 Thanks a lot!

 --
 Regards,
 Robert



 



 --



 
 ___
 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] Theorems Produced by Type Definitions

[Mark Adams]

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 bracketing), and should of course be
written as this:

   (\a. abs (rep a)) = \a. a
   P = (\r. rep (abs r) = r)

Mark.

on 16/10/14 5:19 PM, Ramana Kumar ramana.ku...@cl.cam.ac.uk wrote:

 Hi all,

 There has been an interesting discussion on the OpenTheory mailing list
 recently regarding how to simplify the two theorems produced by a type
 definition in HOL Light and remove their free variables. The latest
message
 in the thread, which shows the  suggestions by Mario Carneiro can be found
 here:
 http://www.gilith.com/pipermail/opentheory-users/2014-October/000415.html.

 I'm cross-posting to this list because I think using Mario's suggestions
 would be an improvement to both HOL Light and Opentheory. I hope the
 respective authors of those systems might agree and implement the changes,
 and that anyone else with an interest might voice their opinion.

 Cheers,
 Ramana



 



 --
 Comprehensive Server Monitoring with Site24x7.
 Monitor 10 servers for $9/Month.
 Get alerted through email, SMS, voice calls or mobile push notifications.
 Take corrective actions from your mobile device.
 http://p.sf.net/sfu/Zoho


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




--
Comprehensive Server Monitoring with Site24x7.
Monitor 10 servers for $9/Month.
Get alerted through email, SMS, voice calls or mobile push notifications.
Take corrective actions from your mobile device.
http://p.sf.net/sfu/Zoho
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

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

[Mark Adams]

Nela,

These versions should definitely work together.

Just realised - what you presumably did is first try the HOL Light 'make'
using other versions of OCaml or Camlp5.  So what you needed to do was first
do
make clean
before doing
make

I would be very surprised if this doesn't work.

Mark.

on 17/9/14 1:14 PM, Nela Cicmil nela.cic...@dpag.ox.ac.uk wrote:

 @ Mark:  I used the svn download command only this week so probably it has
 the most recent version of HOL Light. On svn download, I get the output
 Checked out revision 198, and the CHANGES document inside the hol_light
 directory is dated 9th Sept 2014. Here are my ocaml and camlp5 versions:

 hol_light nc$ ocaml -version
 The OCaml toplevel, version 4.01.0
 hol_light nc$ camlp5 -v
 Camlp5 version 6.11 (ocaml 4.01.0)

 @ Ramana: I'm looking into the pa_j*.ml files, but it's not clear to me
how
 to write one to work with the ocaml version 4.01.0/camlp5 v 6.11 combo.

 Thanks!

 Best wishes,
 Nela

 
 Nela Cicmil, D.Phil
 Dept. Physiology, Anatomy  Genetics,
 University of Oxford
 
 From: marco.magg...@gmail.com [marco.magg...@gmail.com] on behalf of Marco
 Maggesi [magg...@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.  I use Nix both on Max and on Linux.  It is nice because it makes the
 installation of HOL Light completely independent from the versions of
ocaml,
 camlp5 (or any other software indeed) installed in your machine.

 If you want to try, here is what you have to do:

 1. Install Nix.  Follow the instructions from the nix manual
 (http://nixos.org/nix/manual).  Basically you have to type the following
 four commands in a terminal:

 ​
 $ bash (curl https://nixos.org/nix/install)
 source /usr/local/etc/profile.d/nix.sh
 ​​
 ​​
 nix-channel --add http://nixos.org/channels/nixpkgs-unstable
 ​nix-channel --update​
 ​​
 ​2​
 .
 ​Then you can install HOL Light with a single command (no need to install
 OCaml or Camlp5)

 ​  ​
 nix-env -i hol_light

 ​For more serious work you probably need to use checkpointing which is
 available only on Linux.  For this I use a NixOS (http://nixos.org)
 VirtualBox appliance.  Do not esitate to ask for more details if you are
 interested.

 Best,
 Marco

 2014-09-17 5:50 GMT+02:00 Mark Adams
 m...@proof-technologies.commailto:m...@proof-technologies.com:
 Hi Nela,

 There have been various problems over the years, but I get no problems
with
 recent versions of HOL Light (downloaded since May 2014, including SVN
 version 197 downloaded in mid-August) with OCaml 4.01.0 and Camlp5 6.11
 running on Fedora 17.

 Do you know the HOL Light SVN version (or otherwise, what date did you
 download)?

 And can you please check your OCaml and Camlp5 versions by executing the
 following from the same terminal window from which you are trying the HOL
 Light make?:
 ocaml -version
 camlp5 -v

 Mark.

 on 16/9/14 4:45 PM, Nela Cicmil
 nela.cic...@dpag.ox.ac.ukmailto:nela.cic...@dpag.ox.ac.uk wrote:

 Dear HOL Light users,

 Would anyone be able to please advise me on how to install HOL Light on
my
 Mac? It's a MacBook Pro OS X 10.8.5 Intel core i5.

 My trouble is that I can't seem to get compatible versions of Ocaml,
 camlp5
 and HOL Light installed on my system, mainly because the Ocaml version
 that
 comes with OPAM, v 4.01.0, seems to be too recent to run with the
slighter
 older camlp5 versions compatible with HOL Light.

 Has anyone recently installed HOL Light on a Mac, and has advice on which
 versions of Ocaml and camlp5 to install, and which procedure to use to
 install them? In particular, is it possible to install an older version
of
 Ocaml, e.g. v 3.12, using OPAM?

 The specific issues I've encountered are detailed below. Any advice would
 be
 much appreciated.

 Thank you,

 Best wishes,
 Nela
 
 Nela Cicmil, D.Phil
 Dept. Physiology, Anatomy  Genetics,
 University of Oxford
 

 After various attempts to install Ocaml on the Mac, I installed (using
 homebrew) the latest version of OPAM, which comes with Ocaml version
 4.01.0.
 On basic testing at the terminal, Ocaml seemed to be working fine. I then
 installed camlp5 version 6.11, using ./configure --transitional mode, and
 that seemed to be running fine as well. When I then attempted to install
 HOL
 Light, using the svn checkout http://hol-light.googlecode.com/svn/trunk/
 hol_light procedure, and got the following error on make:

 File pa_j.mlhttp://pa_j.ml, line 112, characters 72-74:
 Error: This expression has type (string * MLast.ctyp) list
 but an expression was expected of type
 ('a * MLast.ctyp) list Ploc.vala
 make: *** [pa_j.cmo] Error 2

 - On reading various previous posts, it seemed that the latest versions
of
 camlp5 could be at fault. I

Re: [Hol-info] Learning HOL Light

[Mark Adams]

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 the
axiomatisation.  I try to use terminology as carefully as possible, and to
define everything precisely in the bundled HOL glossary, although I'm always
looking for suggestions for improvements (it's changed a lot over the years,
thanks to the suggestions of Rob, John and others).  And all derived
theorems and inference rules (e.g. in bool.ml') have annotations in comments
that explain what is going on in the derivation (although I've just spotted
a couple of theorems that don't).

HOL Zero has a different axiomatisation of the HOL logic than the one used
in HOL Light and the one used in HOL4 and ProofPower.  In a nutshell, it is
the same as HOL4 with the same primitive constants, except that it has 3
basic primitive inference rules (EQ_MP, INST and MK_COMB) in place of the
rather complicated SUBST (making it close to HOL Light's set of primitive
inference rules), and that it derives BOOL_CASES_AX (using the Beeson-like
proof) instead of IMP_ANTISYM_AX (whereas HOL Light derives both).  So it's
axiomatisation is between that of HOL4 and HOL Light, but somewhat closer to
HOL4's classic axiomatisation that HOL Light's.

Best,

Mark.


The source code comments explain a of what is going on.

on 21/3/14 6:19 AM, Bill Richter rich...@math.northwestern.edu wrote:

 Thanks, Konrad!  You seem to agree with me here, that the
 typed-LC-implies-FOL isn't actually important:

 My personal feelings on this foundational aspect are that the
 actual set of axioms isn't that important provided the usual
 introduction and elimination rules of predicate calculus can be
 derived from them.

 Now you're encouraging me to go read Church's typed LC paper more
carefully,
 and see if I can work out the apparent difference between Church and what
I
 quoted Andrews as saying about Church:

 My recollection (don't have citations to hand) is that Church
 originally wanted the untyped lambda calculus to serve as a
 foundation for logic, but that was discovered to be
 inconsistent. Something like Russell's paradox would be easy to
 code up in it. However, the simply typed lambda calculus worked
 better, i.e., it supports the derivation of the expected FOL-like
 rules, as we see in HOL theorem provers, and it is sound.

 Here's a some dumb questions about HOL4 and HOL Light.

 On p 29 of LOGIC, you write that there are constants
 Tbool, ∀(α→bool)→bool etc.  Why aren't there colons?  I would have written
 that as
 T:bool and ∀:(α→bool)→bool
 Are the apparent subscripts supposed to indicate colons, or does HOL4 not
 use colons for type annotations?

 I'm having trouble seeing your derivation of the expected FOL-like rules
in
 HOL Light.  Is there a paper where somebody explained these HOL
derivations,
 or is it perhaps easier to understand in HOL4?

 Tom Hales writes on p 6 of
 http://www.ams.org/notices/200811/tx081101370p.pdf

 The system [HOL Light] has only two primitive constants.  One of them is
the
 equality symbol (=) of type :A-A-bool.  So = is primitive, and p 5 lists
 the HOL Light axioms about the properties of =.  Let's try to find this in
 the HOL Light sources.  In
 hol_light/bool.ml
 it seems to me that first the type bool is defined,
 then = and = are defined to have type bool-bool-bool and to be the
same
 as each other,
 then T is defined as

 let T_DEF = new_basic_definition
 `T = ((\p:bool. p) = (\p:bool. p))`;;

 That's your first HOL axiom on p 29 (again without colons):

 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 represented in Ocaml as the ordinary =?

 --
 Best,
 Bill




 --
 Learn Graph Databases - Download FREE O'Reilly Book
 Graph Databases is the definitive new guide to graph databases and their
 applications. Written by three acclaimed leaders in the field,
 this first edition is now available. Download your free book today!
 http://p.sf.net/sfu/13534_NeoTech
 ___
 hol-info mailing list
 hol-info@lists.sourceforge.net
 https://lists.sourceforge.net/lists/listinfo/hol-info




--
Learn Graph Databases - Download FREE O'Reilly Book
Graph Databases is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!
http://p.sf.net/sfu/13534_NeoTech
___
hol-info mailing list
hol-info@lists.sourceforge.net

Re: [Hol-info] Learning HOL Light

[Mark Adams]

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 represented in Ocaml as the ordinary =?

No, not at all.  The above is defining the constant 'T'.  The constant '='
does not have a definition in HOL Light, or in any of the HOL
axiomatisations.  We have to start somewhere with entities that don't have
definitions but are just declared.  In HOL Light's axiomatisation, the only
such entities are the 'bool' and 'fun' type constants and the '=' constant
(the other axiomatisations also have the '==' and '?' constants).  In the
logic, the meaning of such entities is not captured in definitions, but
instead drops out from the aggregation of the axioms and primitive
inference rules.

Best,

Mark.

--
Learn Graph Databases - Download FREE O'Reilly Book
Graph Databases is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!
http://p.sf.net/sfu/13534_NeoTech
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Learning HOL Light

[Mark Adams]

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 and the '=' constant (the other axiomatisations also
 have the '==' and '?' constants)

--
Learn Graph Databases - Download FREE O'Reilly Book
Graph Databases is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!
http://p.sf.net/sfu/13534_NeoTech
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Learning HOL Light

[Mark Adams]

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.  In general = has type A-A-bool.

That's right, the line in bool.ml is just defining an alias.  The constant
'=' is *declared* (there is a difference in meaning between the words
declare and define) in fusion.ml, in the line that sets the ML binding
'the_term_constants' (approx line 206).  The type constants 'bool' and 'fun'
are declared similarly in fusion.ml in the line that sets
'the_type_constants' (approx line 114).

Mark.

--
Learn Graph Databases - Download FREE O'Reilly Book
Graph Databases is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!
http://p.sf.net/sfu/13534_NeoTech
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] More on set comprehensions

[Mark Adams]

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
package proof)?

Mark.

on 7/1/14 5:04 PM, Rob Arthan r...@lemma-one.com wrote:

 Bill,

 On 4 Jan 2014, at 05:17, Bill Richter wrote:
 ...

 On 7 Jan 2014, at 16:22, Rob Arthan wrote:
 I think we will just have to agree differ about this. Let me just make
two
 comments:


 Something very odd happened with my e-mail client which caused it to
discard
 the
 two comments. They were as follows:

 (a) Too much mathematical notation is explained away as short-hands, i.e.,
 as syntactic abbreviations. This is a consequence of the traditional
 pretence that mathematics is founded on first-order set theory and
 of the inexpressiveness of first-order languages. In a higher-order
 logic you can generally replace these short-hands by first class
 mathematical
 citizens that you can reason about in their own right. This often
 fits in well with a categorical way of thinking about what you are
 doing. In the case in point, the categorical account of set comprehensions
 would be in the category of sets and relations. Let me write R : X - Y
 to mean that R is a relation between the sets X and Y and let BOOL
 be the two-point set {F, T}. Given a relation R:X - BOOL, we
 associate the subset R^{-1}({T}). Given a function f : X - Y and
 a function p : X - BOOL, we get a relation R : Y - BOOL
 in the obvious way by defining R = p o f^{-1} and hence
 the associated subset R^{-1}({T}) of Y. Note there are no bound variables
 in this categorical description of {f x | p x}: they are all hidden in the
 definitions of relational composition, relational image and
 relational inverse. From what you say above you would
 presumably object to that.

 (b) My original objection was that something like
 `{x | x  0}` = `{x | x  0}` evaluates to false in HOL Light
 because the two terms use a different name for the
 hidden bound variable that you are so fond of. I now
 realise that things like `x` = `x` also evaluate false
 because you get different type variables. I can only conclude
 that the HOL Light parser does not share what I know was
 a design goal of the ProofPower-HOL parser which was that
 the same string of symbols should always parse to the same
 term in any given context. I suspect this is also a design goal
 of the HOL4 parser (which, like ProofPower-HOL, uses
 'a, 'b, 'c etc. for invented type variables).

 Regards,

 Rob.

--
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] Trouble building HOL light

[Mark Adams]

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 of OCaml, you also need to create a sufficiently recent
 adapted-for-HOL-Light version of pa_j.ml (adapted from Camlp5 source code
 files etc/).  You are right that you can work out what adaptions to do by
 diffing corresponding older versions of the unadapted and adapted Camlp5
 files.  These Camlp5 files are 'lib/lexer.ml' and 'etc/pa_o.ml', but the
 adaption for HOL Light is combined into one file called 'pa_o.ml'.  Note
 that Camlp5 6.07 or later is required for OCaml 4.00, and Camlp5 6.11 or
 later is required for OCaml 4.01.

 I think the warnings you get may be from superfluous #load directives in
 your adapted 'pa_j.ml' file, so comment out the following two lines in the
 adapted 'pa_o.ml' file and everything should go smoothly:
 #load pa_extend.cmo;;
 #load q_MLast.cmo;;

 Note that HOL Zero (also implemented in OCaml) does a similar thing to HOL
 Light, in that it uses Camlp5 to adjust the OCaml lexical syntax for HOL
 quotations (although in HOL Light there are also changes to the OCaml
 syntax).  Installation works smoothly for HOL Zero for all versions of
 OCaml.  Also, the HOL Zero distribution has relatively detailed comments
in
 Section 2 of INSTALL and Section 2 of 'etc/README', if you want to
 understand a little more about what is going on.

 Mark.

 on 14/10/13 2:07 PM, Rob Arthan r...@lemma-one.com wrote:


 On 14 Oct 2013, at 12:53, Rob Arthan r...@lemma-one.com wrote:

 Can anyone help me with building HOL light? I get the following when I
 run
 make:

 File pa_j.ml, line 1918, characters 35-43:
 While expanding quotation str_item:
 Parse error: antiquot _ or antiquot  or [ident] expected after
'type'
 (in
  [str_item])
 Error while running external preprocessor
 Command line: camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo 'pa_j.ml' 
 /var/folders/8_/t3z32dh14tzfb_4lvdq8q5frgn/T/ocamlppbd42df

 I am using ocaml version 4.01.0 and camlp5 version 6.11 and svn rev 174
 of
 the HOL light source.

 Regards,

 Rob.

 By comparing the camlp5 source with pa_j.ml, I got it and then HOL Light
 to
 compile. I can provide a patch if anyone wants it, but it still gives
 warnings,  so it really needs attention from someone who understands it.
 It
 seems a shame that this involves so much copy/paste/tweak re-use of the
 camlp5 source.

 Regards,

 Rob.




 --
 October Webinars: Code for Performance
 Free Intel webinars can help you accelerate application performance.
 Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most
 from
 the latest Intel processors and coprocessors. See abstracts and register



http://pubads.g.doubleclick.net/gampad/clk?id=60134071iu=/4140/ostg.clktrk
 ___
 hol-info mailing list
 hol-info@lists.sourceforge.net
 https://lists.sourceforge.net/lists/listinfo/hol-info







 --
 October Webinars: Code for Performance
 Free Intel webinars can help you accelerate application performance.
 Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most
 from
 the latest Intel processors and coprocessors. See abstracts and register 

http://pubads.g.doubleclick.net/gampad/clk?id=60135031iu=/4140/ostg.clktrk
 ___
 hol-info mailing list
 hol-info@lists.sourceforge.net
 https://lists.sourceforge.net/lists/listinfo/hol-info




--
October Webinars: Code for Performance
Free Intel webinars can help you accelerate application performance.
Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most from 
the latest Intel processors and coprocessors. See abstracts and register 
http://pubads.g.doubleclick.net/gampad/clk?id=60135031iu=/4140/ostg.clktrk
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] HOL glossary

[Mark Adams]

Dear HOL users,

An updated version of my glossary of HOL-related terminology is now
available from the Proof Technologies website at:

http://www.proof-technologies.com/Glossary

It significantly improves on the version of the glossary sent out on
the holinfo mailing list last October, by adding around 50 entries and
various links and improving many existing entries.  The biggest area
of change has been in adding various entries for background
mathematical logic concepts.

Please feel free to e-mail me with any comments or opinions.  I do not
consider the glossary as closed, and am open 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 of server virtualization is a top
priority.Virtualization can reduce costs, simplify management, and improve 
application availability and disaster protection. Learn more about boosting 
the value of server virtualization. http://p.sf.net/sfu/vmware-sfdev2dev
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info