Rob, you seem to understand Hilbert axioms pretty well:
> let Line_DEF = new_definition
> `!A B. Line(A, B) = {X | ~(A = B) /\ (Collinear(X, A, B) \/ Collinear(A, X,
> B) \/ Collinear(A, B, X))}`;;
Yeah, that looks simpler than my Hilibert-choice operator (@), but
again it didn't work. Maybe John's let expansion will fix it.
John, thanks for the message, and handling Binyameen's question, which
was beyond me! I'm having problems even without let, as you'll see
from the script I just posted. I would have thought that
let Bool_DEF = new_definition
`!A, B, C. boolean-function(A, B, P) <=> alpha`;;
used in the proof as
boolean-function(A, B, P) by ... Bool_DEF;
would be the same as using
P IN set-function(A, B) by ... Set_DEF;
with the definition
let Set_DEF = new_definition
`!A, B, C. set-function(A, B) = {P | alpha}`;;
Without seeing the exact script I can't be absolutely sure, but I
think it's very likely that the default prover is failing to expand
or otherwise take account of the "let" construct. Can you try it
with the lets manually expanded? For example, do
let InteriorAngle_ALT =
CONV_RULE(TOP_DEPTH_CONV let_CONV) InteriorAngle_DEF;;
I tried it and I get the same error message. I just posted my code
(sorry I didn't see that you & Rob had written), and maybe I'll say
the problems I'm having can probably all be circumvented, as in this
case I replaced a {P | ... } definition by a boolean function. But it
would be nice to do exactly what I want as an exercise to show that
HOL Light is very flexible and can handle the set-theoretic
constructions that come up naturally in math.
Here's another thing I couldn't do. Let's define Line(A, B) to be the
(unique if A <> B) line through the points A and B. Well, then I'd
like to say in my miz3 code
let a = Line(A, B);
I can't get anything like that to work. You ought to be able to do
that, right? I see that Freek in lagrange1.ml did this:
set coset = \a. {b | b IN g /\ ?x. x IN h /\ b = a**x} [coset];
!a. coset a = {b' | b' IN g /\ ?x. x IN h /\ b' = a**x} [13];
So maybe it's set and not let, but that didn't work for me.
BTW Makarius seemed to say on the Isabelle group that Mizar is exactly
FOL with some automation to relieve the tedious parts of FOL. And
that's exactly what I want! That would explain why Mizar (and miz3)
is such a good thing. Does that sound right? I may have
misunderstood Makarius. I certainly don't understand how FOL relates
to the Isabelle frameworks Pure & Isar.
--
Best,
Bill
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
