On Tue, Apr 29, 2014 at 5:51 AM, Bill Richter wrote:
>
> Here's a more substantive point that's always bothered me. Suppose if one
> is working in one's preferred logical framework (e.g. ZFC), and one engages
> in metamathematics. On what grounds to we believe the metamathematics?
> The poin
Thanks, Rob! I think we're in agreement on the substantive issues, after I
agree with your true correction:
If you replace “true” by “provable”, then this is how one would
state Andrews’ claim that the rules of N are admissible in FOL.
Yes, thanks for the correction. So we're just talkin
On 28 Apr 2014, at 00:57, Bill Richter wrote:
> Rob, I want to argue that Peter Andrews's book To Truth Through Proof
> supports my idea of informal mathematics documentation for HOL Light. I
> don't understand yet how the informal math compares to your HOL documentation
> http://www.lemma-
Rob, I want to argue that Peter Andrews's book To Truth Through Proof supports
my idea of informal mathematics documentation for HOL Light. I don't
understand yet how the informal math compares to your HOL documentation
http://www.lemma-one.com/ProofPower/specs/spc001.pdf
Mostly I'm going to
On 26 Mar 2014, at 07:58, Bill Richter wrote:
> Thanks, Konrad! The proof of SYM in the HOL4 manual Description (p 46) is
> fine because the HOL4 SUBST is much more powerful than the HOL Light INST.
> On p 26, SUBST is described by
>
> SUBST : (thm * term)list -> term -> thm -> thm
>
> t
Thanks, Rob! You seem to be correct about Andrews's book To Truth Through
Proof. His Chapter 5 Type Theory is 56 pages long, and it's mostly about Q_0
which is based on equality, which he calls Q:A->A->bool, and I notice that he
prove the only "truth table" result I was able to prove:
|- T ∧ T
Bill,
On 26 Mar 2014, at 23:01, Bill Richter wrote:
> Thanks, Rob! Then since I only technically have a model, I would say I'm
> working in your class (c):
>
> (c) Informal mathematical proofs that an assertion is provable in
> some agreed deductive system.
No. When I wrote "an assertion",
Thanks, Rob! Then since I only technically have a model, I would say I'm
working in your class (c):
(c) Informal mathematical proofs that an assertion is provable in
some agreed deductive system.
I still don't understand what you're saying about class (d), or why this is
true:
Your theorem
Bill,
On 26 Mar 2014, at 09:37, Bill Richter wrote:
> Rob, thanks for the excellent post! Let me more clearly tell you what I
> think I'm doing, using your terminology, and maybe we can discuss your
> classes a--e.
>
> Take HOL Light and possibly some extra types, constants and axioms create
Rob, thanks for the excellent post! Let me more clearly tell you what I think
I'm doing, using your terminology, and maybe we can discuss your classes a--e.
Take HOL Light and possibly some extra types, constants and axioms created by
commands like new_type, new_constant, and new_axiom. Let S
Thanks, Konrad! The proof of SYM in the HOL4 manual Description (p 46) is fine
because the HOL4 SUBST is much more powerful than the HOL Light INST. On p 26,
SUBST is described by
SUBST : (thm * term)list -> term -> thm -> thm
t[t1 , . . . , tn ] yields t[t1',...,tn']
. where t[t1 , . . .
Bill,
On 25 Mar 2014, at 07:27, Bill Richter wrote:
> So the similarity is that in both FOL and HOL,
> 1) You can define a set of statements to study (wffs and proto-sequents).
"Proto-sequent" and “sequent” are usually referred to as “sequent” and
“theorem” respectively. E.g., see the HOL4 Lo
> Konrad, I should definitely read Description's chapter Derived Inference
Rules, which seems to be doing much the same
> thing as I was attempting in my post. I noticed that Gordon & Melham's
book is only mentioned much later and is not in
> your bibliography. Could that be because Gordon wrote
Thanks, Rob and Konrad! I will read Andrews's book and the HOL4 Description
manual.
Rob, I'm guessing Andrews isn't too happy with the HOL->FOL derivation you've
argued must be in his book, as he advertised it so poorly. I'll agree with you
and Konrad that Tarski, Quine and Henkin are the o
> Osmosis. The original HOL documentation/code included schematic
derivations of the derived rules of inference (didn't that
> make it into Gordon and Melham?). However, the starting point for that is
the rather ad hoc collection of primitive rules and
> axioms that evolved into the ones currently
Bill,
On 24 Mar 2014, at 06:28, Bill Richter wrote:
> Thanks, Rob! You're right, I hadn't looked at Section 1.4 "A Formulation
> Based on Equality" of Andrew's link
>> http://plato.stanford.edu/entries/type-theory-church/ and more to the point,
>> I didn't read the longer version Andrew's wro
Mark, I tried to make your corrections, and here's my new draft, at just 500
lines:
I want to explain how to read the HOL Light basics from the source code in
several sections
0) informal math and HOL
1) the type bool and the constant =
2) sequents, new_basic_definition and the HOL Light infere
Thanks, Rob! You're right, I hadn't looked at Section 1.4 "A Formulation Based
on Equality" of Andrew's link
> http://plato.stanford.edu/entries/type-theory-church/ and more to the point,
> I didn't read the longer version Andrew's wrote in his book To Truth Through
> Proof:
More details ab
Thanks, Mark! My draft can use a lot of help from experts like you. I think I
decided that what I'm attempting is to describe, in the usual language of
mathematicians, the set of HOL Light sequents.
But I'm not sure your declare/define terminology is standard. The string
"declar" does not o
Bill,
On 23 Mar 2014, at 18:44, Bill Richter wrote:
>
> The claim (which you may not be making) that Hankin derived FOL from the
> basic LC axioms (e.g. the HOL axioms) seems to contradict Andrew's link
> http://plato.stanford.edu/entries/type-theory-church/
> which as I posted lists Prop Log
Hi Bill
These are nice explanations, but here are a few comments and
corrections:
> * 1) the definitions of type bool and the constant =
*
>
You're still using the terminology "definition" for 'bool'
and '=', whereas they are only *declared* in each of the HOL systems'
axiomatisati
Thanks, Mark! I figured out the constant = myself, but it would have saved me a
lot of time if I checked my mail yesterday when you explained it :)
I should have said '@' instead of '?' here. The constant '?' is
actually defined in these axiomatisations (using '@').
This is true for HO
I want to explain how to read the HOL Light basics from the source code in
several sections
0) colloquial (informal) math and HOL
1) the definitions of type bool and the constant =
2) sequents, new_basic_definition and the HOL Light inference rules
3) The BETA_CONV proof of general beta-conversio
Andrew,
On 21 Mar 2014, at 09:13, Andrew Butterfield
wrote:
>
> On 20 Mar 2014, at 16:50, Rob Arthan wrote:
>
>>
>> ProofPower is no different from HOL4 and HOL Light as regards substitution.
>> The ProofPower documentation does include a formal specification of the
>> logic and the proof
On 20 Mar 2014, at 16:50, Rob Arthan wrote:
>
> ProofPower is no different from HOL4 and HOL Light as regards substitution.
> The ProofPower documentation does include a formal specification of the logic
> and the proof system, but you would probably do better looking at the HOL4
> Logic Ma
On 20 Mar 2014, at 16:50, Rob Arthan wrote:
>
> ProofPower is no different from HOL4 and HOL Light as regards substitution.
> The ProofPower documentation does include a formal specification of the logic
> and the proof system, but you would probably do better looking at the HOL4
> Logic Ma
Hi Bill,
on 21/3/14 4:28 PM, Bill Richter 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 t
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 wrote:
> ... In HOL Light's axiomatisation, the only such entities are the 'bool'
and
> 'fun' type constants and the '=' constant (the oth
The constant = is not defined in HOL Light, but simply declared (as Mark
said). In fact, equality is even more basic than that: it's a built in
term. You can see, for example, the "safe_mk_eq" function in fusion.ml, and
also the "the_term_constants" reference (which starts with "=" built in).
I fe
Thanks for correcting me, Mark! I'll look at your HOL Zero source code,
especially corethy.ml. I see my error now. From bool.ml:
let T_DEF = new_basic_definition
`T = ((\p:bool. p) = (\p:bool. p))`;;
The first = is an Ocaml =, but the 2nd =, the one we care about, is the
primitive HOL Ligh
Thanks, Konrad! I'll read your proof of NOT_FORALL_THM, and try to find Gordon
and Melham's book. Two points:
I don't believe that Church ever explained how typed LC implies FOL. Church
certainly does not explain this in his paper
A Formulation of the Simple Theory of Types http://www.jstor.o
Bill:
> 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?
Throughout th
Hi Bill,
on 21/3/14 6:19 AM, Bill Richter 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 th
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 th
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
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.
My recollection (don't have citations to hand) is that Church originally
wanted the untyped
Thanks, Rob! I don't Andrew's book to hand either, but his on-line article is
causing me real trouble:
http://plato.stanford.edu/entries/type-theory-church/
1.3.2 Elementary Type Theory
We start by listing the axioms for what we shall call elementary type theory.
(1) [pο ∨ pο] ⊃ pο
Bill,
On 19 Mar 2014, at 07:02, Bill Richter wrote:
> work is. If I understood it, I'm sure I'd say it was elegant mathematics,
> and that it's good we're assuming the weakest possible set of axioms.
Have you looked at Peter Andrews’ book "An Introduction to Mathematical Logic
and Type The
2. The argument formerly used a direct port of the original
Diaconescu proof as presented in Beeson's "Foundations of
Constructive Mathematics". But in July 2009 I changed it to a
somewhat optimized variant shown to me by Mark Adams. This is
noted in the CHANGES fil
Thanks, John and Rob! The main problem I'm having is actually embarrassingly
simple: I don't understand the typed Lambda Calculus angle in Church's work or
HOL. Now I definitely see the point of having functions as well as sets, and
that means that the HOL type theory (sets are either types or
Konrad and Rob have already answered Bill very thoroughly, but I'll add
two additional comments:
1. I guess Bill was dicombobulated by the "..._AX" name, which does
suggest an axiom. This name is for historical reasons and compatibility
with other HOLs. BOOL_CASES_AX was traditionally a
On 17 Mar 2014, at 00:52, Konrad Slind wrote:
> RE: type bool. I think BOOL_CASES_AX can be derived from choice.
> There's a topos-flavoured proof (due to Diaconescu?) in Lambek and Scott,
> which I think John ported to HOL-Light.
Yes. I don’t know the right reference: the comment in the HOL Li
Thanks, Konrad! I see that the HOL light BOOL_CASES_AX is proved in class.ml
using the result I mentioned, EXCLUDED_MIDDLE, which class.ml says is derived
from Beeson's book:
let BOOL_CASES_AX = prove
(`!t. (t <=> T) \/ (t <=> F)`,
GEN_TAC THEN DISJ_CASES_TAC(SPEC `t:bool` EXCLUDED_MIDDLE)
RE: type bool. I think BOOL_CASES_AX can be derived from choice.
There's a topos-flavoured proof (due to Diaconescu?) in Lambek and Scott,
which I think John ported to HOL-Light.
Konrad.
On Sun, Mar 16, 2014 at 7:25 PM, Bill Richter wrote:
> I'm trying to understand Tom Hales's compact descri
I'm trying to understand Tom Hales's compact description of HOL Light in his
AMS Notices article www.ams.org/notices/200811/tx081101370p.pdf
The first things I don't understand are the type bool and the beta-conversion
inference rule.
Isn't there an axiom that there are exactly two term type boo
On 19.02.2014 14:41, Bill Richter wrote:
> - if you have existentials or disjunctions in the theorems you want to
> use or in the goal, use MESON_TAC
>
> By putting this after SIMP_TAC, I infer that SIMP_TAC will not handle
> existentials or disjunctions.
Indeed - most of the time.
Let me
Vince, thanks for improving my code! I've implemented Freek's 1-line "by"
proofs, so I can shorten your proof a bit:
let INTERIOR_EQ = theorem `;
∀s. interior s = s ⇔ open s
by simplify interior_DEF OPEN_IN SUBSET_UNIV TOPSPACE_EUCLIDEAN InteriorEq
EQ_SYM_EQ`;;
But why does this work? L
Hi Bill,
you're right. Indeed, part of the idea of automation tools is to
actually remove the burden of knowing precisely what's going on inside.
But they're not perfect so in practice, it turns out to actually be
useful to know about them. So knowing about the algorithms behind them
is still
Back to my other question, there's something about USE_THEN and type
annotations I don't understand. I get the same problem with FIRST_ASSUM. In
Multivariate/topology.ml there's a theorem
let FRONTIER_CLOSURES = prove
(`!s:real^N->bool. frontier s = (closure s) INTER (closure(UNIV DIFF s))`,
Thanks, Vince! I think we haven't quite gotten it right yet, as it's tricky to
talk about intentions. You correctly pointed out there was something wrong
with the way I used REWRITE_TAC[DIST_SYM]. John's proof uses ONCE_REWRITE_TAC
correctly, but he's using DIST_TRIANGLE_ALT, while I tried to
On 17.02.2014 12:49, Bill Richter wrote:
> Vince, this is very interesting:
>
> I would say what is bad coding is not to rely on features you don't
> understand but on features that are actually
> undocumented/unintended. Here, the ordering chosen is indeed
> ingenious to prevent s
Vince, this is very interesting:
I would say what is bad coding is not to rely on features you don't
understand but on features that are actually
undocumented/unintended. Here, the ordering chosen is indeed
ingenious to prevent some often-met looping situations. However,
as John p
On 14.02.2014 04:39, Bill Richter wrote:
> I guess I understood that REWRITE_TAC used a complicated algorithm in order
> to avoid infinite looping. So I think I didn't express my question very
> well. I tend to think that it's not good coding on my part to rely on
> features that I don't even
Thanks, John! I'll read p 34 more carefully. Your example shows the behavior
I'd want from REWRITE_TAC. You theorem is
# ADD_AC;;
val it : thm =
|- m + n = n + m /\ (m + n) + p = m + n + p /\ m + n + p = n + m + p
This is a good exercise for my right associativity skill. and that's what it
Hi Bill,
| I'm quite mystified that the REWRITE_TAC[DIST_SYM] only rewrote the
| middle dist term
Generally speaking, with constructs like REWRITE_TAC that apply
rewrites repeatedly, there are special heuristics to deal with those
that would obviously loop indefinitely. (This doesn't apply to mo
Here's a question about free variables and REWRITE_TAC (and other
thmlist->tactics). Almost every usage of USE_THEN in the HOL Light sources is
of the form
USE_THEN label MATCH_MP_TAC
Here's an example of a labeled assumption used in thmlist of MESON_TAC:
let NSQRT_2 = prove
(`!p q. p * p =
I have a question about REWRITE_TAC. I was invited to speak at the conference
https://ihp2014.pps.univ-paris-diderot.fr/doku.php?id=workshop_1
where John, Freek, Tobias Nipkow and Tom Hales are 4 of the 14 plenary
speakers, and I hope folks here will help answer various HOL Light questions I
sti
In my last post I should have said instead that HOL programmers have very good
concrete down-to-earth adjoint functors skills, which pure mathematicians tend
to have good theoretical adjoint functors skills, and maybe interfaces that
hides the adjoint functors calculations are good.
Today I'd a
I want to explain GEN_REWRITE_TAC, which I just understood (partly because of
Rob and Michael's advice here about is_comb etc), and to argue that
1) HOL programmers are very good at the pure math skill of adjoint functor, and
2) getting mathematicians to use HOL may require an interface that hide
John, I'm sorry it took me so long to respond to your MP_TAC vs MESON_TAC post
of Jun 1:
| What's the difference between MESON_TAC[th1; th2; th3];; and
| MP_TAC th3;;
| MESON_TAC[th1; th2];;
The difference is that after MP_TAC any free variables or free type
variables effectively
Mark, I now understand your HOLZero/print_exn idea, and it works pretty well:
exception Readable_fail of string;;
let PrintErrorFail s = raise(Readable_fail s);;
let print_exn e =
match e with
| Readable_fail s
-> print_string s
| _ -> print_string (Printexc.to_string e);;
#install
Mark, your update_database.ml idea worked great! My code simplified to
(* From update_database.ml: Execute any OCaml expression given as a string. *)
let exec = ignore o Toploop.execute_phrase false Format.std_formatter
o !Toploop.parse_toplevel_phrase o Lexing.from_string;;
(* exec and a re
>> HOL Light and HOL Zero don't use OCaml's lexing facilities, but
>> implement their own from scratch.
>
> Wow, I didn't know that! Where can I learn about HOL Light lexing
> facilities?
HOL Light's nice, simple and compact, but is a bit light on source code
comments. It's got a snappy little l
Mark, thank you very much! You gave me a good idea, to try to use the top of
update_database.ml directly:
(* Execute any OCaml expression given as a string. *)
let exec = ignore o Toploop.execute_phrase false Format.std_formatter
o !Toploop.parse_toplevel_phrase o Lexing.from_string;
Hi Bill,
> Let me try to explain. My only objection to my PrintErrorFail is minor:
> it prints Exception: Failure "". at the end, but arguably this is a good
> error message.
What you do is print out the message regardless of whether the exception
bubbles up to the toplevel. The solution I'm
Hi Bill,
> By grepping, I see occurrences of Format.print_string and
> Format.print_newline commands in e.g. make.ml, but isn't the Format
> prefix here unnecessary, because they're pervasive? Isn't that
> explained in section 20.2 Module Pervasives : The initially opened
> module of the ocaml re
Mark, I think you can write some good Light documentation, and maybe improve
the HOL Light code. Let me try to explain. My only objection to my
PrintErrorFail is minor: it prints
Exception: Failure "".
at the end, but arguably this is a good error message. Here's what I like
about my def:
1
Thanks, Mark! I see your include Format;; in printer.ml. By grepping, I see
occurrences of Format.print_string and Format.print_newline commands in e.g.
make.ml, but isn't the Format prefix here unnecessary, because they're
pervasive? Isn't that explained in section
20.2 Module Pervasives :
Hi Bill,
> Thanks, Mark! That sounds like a good tip, but can you be more specific?
I
> produce error message with this function
>
> let PrintErrorFail s =
> open_box 0; print_string s; close_box (); print_newline (); fail();;
>
>
> But I only want to change the OCaml exception printer for m
Thanks, Mark! That sounds like a good tip, but can you be more specific? I
produce error message with this function
let PrintErrorFail s =
open_box 0; print_string s; close_box (); print_newline (); fail();;
BTW I do not understand why this works, why I don't have to say
Format.open_box an
Hi Bill,
You can overwrite the OCaml exception printer if you want, like I do in HOL
Zero in 'exn.ml' and the main build file 'holzero.ml', where the error
message is part of the exception and gets printed out if/when the exception
bubbles to the top. You could do something like this:
let pri
Vince, I figured out how to print error messages without double-quotes and with
actual newlines! This and a lot more is explained in the ocaml doc in "Module
Format", which I got the idea to use after looking at Freek's miz3.ml. I'd like
to get rid of a trailing message Exception: Failure "".
I learned a number of basic facts thinking about Vince and Freek's ideas, and
now I have no "unused variable" warnings in
RichterHilbertAxiomGeometry/readable.ml. I have some questions.
I reworked Freek's code to get eliminate the "unused variable" warning I was
getting with `is_thm':
let
Vince, I tried your new `ignore' idea with your previous `get' idea, and I
think it works but doesn't suppress error messages. That is, it works fine if
I replace my definition of `is_thm' in RichterHilbertAxiomGeometry/readable.m,
with your
let is_thm s =
try ignore (exec_thm s); true
wi
Thanks, Vince! Your is_thm works fine, but I get a warning when I try to
extend your idea:
let is_thm s =
try ignore (exec_thm s); true
with _ -> false;;
let is_tactic s =
try ignore (exec_tactic s); true
with _ -> false;;
let is_thmtactic s =
try ignore (exec_thmtactic s); true
wi
Hi Bill,
Le 2013-07-02 à 00:00, Bill Richter a écrit :
> I hope folks can help me improve my code readable.ml, which in the new
> subversion 166 is in
> hol_light/RichterHilbertAxiomGeometry/
>
> 1) Can you pretty-print error messages in HOL Light? E.g. here:
>
> with Not_found -> failwith
I hope folks can help me improve my code readable.ml, which in the new
subversion 166 is in
hol_light/RichterHilbertAxiomGeometry/
1) Can you pretty-print error messages in HOL Light? E.g. here:
with Not_found -> failwith("missing initial \"proof\" or final \"qed;\" in "^ s)
It would be nice
Thanks for the great response, John! I'm sorry it took me so long to respond,
and I still don't have a good response, but:
l think I see what you're saying about MP_TAC, MESON_TAC and FREEZE_THEN, and
I'll have to do more experiments.
I ought to learn how parse_preterm works, and I would if
Hi Bill,
| Can someone explain the point of HOL Light parsers, as in the
| reference manual entry for many:
There is an approach to writing parsers in functional languages
where you can make functional code look almost like an abstract
grammar. These HOL Light functions are a pretty simple versi
Can someone explain the point of HOL Light parsers, as in the reference manual
entry for many:
This is one of a suite of combinators for manipulating
``parsers''. A parser is simply a function whose OCaml type is some
instance of :('a)list -> 'b * ('a)list. The function should take a
Vince and Freek, I was wrong and you were right! First I used Vince's
let get = Obj.magic o Toploop.getvalue;;
but then I switched over to Freek's much more complicated exec_thm, as I could
not see how to test for theorems with get, as I didn't know how to handle a get
exception.
My low-tec
Here's a reasonable version of a miz3 interface for HOL Light. Thanks to
Vince, Freek and Petros for helping me out!
I believe this is the end of this parser-based discussion, so allow me to
summarize. It's good for formal proofs to readable, especially if you want to
attract mathematician
Thanks, Ramana! I think it would be good to compare what I'm doing with how
things are in HOL4, because
1) John has always stressed the importance of readability in formal proofs, and
2) my code looks like it will be a lot simpler than John's mizar.ml or Freek's
miz.ml.
I know nothing of HOL4,
>
> Do such regexp issues arise in HOL4 and SML?
>
HOL4 does not have a separate tactic language. Proof scripts are written in
SML directly. (The SML implementation will have a parser etc. though.)
HOL4 does have a sophisticated parser for the object language of HOL terms
and types, which I thin
You can't detect matching braces with regular expressions.
(See e.g.
http://stackoverflow.com/questions/546433/regular-expression-to-match-outer-brackets
.)
What you probably need is to define your tactic language with a grammar and
write a parser for it.
You're going down a route that I think ma
Thanks, Ramana! I created my thmlist_tactics list in the same way that HOL
Light creates the theorems database in hol_light/database.ml:
needs "help.ml";;
theorems :=
[
"ABSORPTION",ABSORPTION;
"ABS_SIMP",ABS_SIMP;
"ADD",ADD;
[...]
"vector",vector
];;
That doesn't strike me as a painful solutio
On Sun, May 5, 2013 at 5:52 PM, Bill Richter
wrote:
> Did I show this wasn't true in this theorem biz here, and did Ramana show
> it wasn't true in HOL4 with DB.fetch?
>
Not quite. Using a database that maps strings to values is a way to solve
the problem of looking up a theorem by its name. But
Here's a toy version of the miz3 interface for HOL Light that I'm aiming for,
with 3 easy proofs. I've coded up quite a bit more (although not case_split),
but this is short enough to show the idea. This was really a lot of fun to
code up. Thanks again to Vince and Freek!
--
Best,
Bill
#l
Thanks, Freek, Ramana and Vincent! I think (assoc thm !theorems) gives a nicer
solution:
RK> In HOL Light I guess there's no database of theorems indexed by
RK> names? That would be one way to avoid having to use Obj.magic.
Yes! The database is an association listtheorems, which is 2212 lines
Am 2013-05-05 um 03:31 schrieb Ramana Kumar :
> On Sun, May 5, 2013 at 5:45 AM, Vincent Aravantinos
> wrote:
>> Hi Bill
>>
>> 2013/5/4 Bill Richter
>>> Question: given the string of a theorem "IN_ELIM_THM", how can I access the
>>> theorem IN_ELIM_THM? Or given a string of a thm_list->tact
On Sun, May 5, 2013 at 5:45 AM, Vincent Aravantinos <
vincent.aravanti...@gmail.com> wrote:
> Hi Bill
>
> 2013/5/4 Bill Richter
>
>> Question: given the string of a theorem "IN_ELIM_THM", how can I access
>> the theorem IN_ELIM_THM? Or given a string of a thm_list->tactic
>> "MESON_TAC", how can
Hi Bill
2013/5/4 Bill Richter
> Question: given the string of a theorem "IN_ELIM_THM", how can I access
> the theorem IN_ELIM_THM? Or given a string of a thm_list->tactic
> "MESON_TAC", how can I access MESON_TAC?
# let get = Obj.magic o Toploop.getvalue;;
val get : string -> 'a =
# ((get "I
Question: given the string of a theorem "IN_ELIM_THM", how can I access the
theorem IN_ELIM_THM? Or given a string of a thm_list->tactic "MESON_TAC", how
can I access MESON_TAC? This is a problem that Freek must have solved in
miz3.ml, but I can't figure out how. John did not seem to solve it
Thanks for explaining the ((asl,w) as g) of tactics.ml, Vince! I now see your
explanation is also in ocaml-4.00-refman.pdf, sec 6.6 Patterns. I know you
told me about your HOL-Light-Q, but you told me not to read it, and you did not
tell me how to get the nonempty environment we need. But it'
Le 01.05.13 00:29, Bill Richter a écrit :
> Thanks, Vince! It look like your q.ml and the HOL4 version are both
> counterexamples to what I've been posting, that the only place where
> retypecheck is used with a nonempty environment is in John & Freek's
> Mizar-like code. I'm really happy to h
Thanks, Vince! It look like your q.ml and the HOL4 version are both
counterexamples to what I've been posting, that the only place where
retypecheck is used with a nonempty environment is in John & Freek's Mizar-like
code. I'm really happy to have been wrong! I can definitely see some
simila
On 04/30/2013 10:24 AM, Bill Richter wrote:
> I wrote my type annotation reducing versions of EXISTS_TAC and X_GEN_TAC, and
> cleaned up the code, with
>
> let (make_env: goal -> (string * pretype) list) =
> fun (asl,w) -> map ((fun (s,ty) -> s,pretype_of_type ty) o dest_var)
>
I wrote my type annotation reducing versions of EXISTS_TAC and X_GEN_TAC, and
cleaned up the code, with
let (make_env: goal -> (string * pretype) list) =
fun (asl,w) -> map ((fun (s,ty) -> s,pretype_of_type ty) o dest_var)
(freesl (w::(map (concl o snd) asl)));;
Thanks, Konrad and Mark! I sorta understood what you posted on my own, by
thinking about John & Freek's Mizar-like code. And thanks to Vince, as I now
have the type annotation reduction I wanted, using retypecheck code from
Freek's function parse_context_term from Mizarlight/miz2a.ml, which is
> I bet the information that p, q, and m have type num is stored somewhere.
> I know we can infer the type num from the assumptions, but that's not
always true.
> Can you tell me where this type information is stored?
Every occurrence of a variable in HOL includes the type of the variable.
You ca
1 - 100 of 212 matches
Mail list logo
