Now that the Platonism discussion has died down (didn't Russell's paradox show
the Platonic world of forms doesn't exist?), let me repeat two requests for
help, as I should be done in 2 or 3 weeks. I have 3700 lines of miz3 code
http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz
and I'm 2 pages away from formalizing the first 7 sections of my geometry paper
http://www.math.northwestern.edu/~richter/hilbert.pdf
I'm up to Euclid's Prop I.18, and I'll go no higher than Prop I.31. My paper
needs a lot of revision now.
My main problem is that I don't understand HOL, so I don't know what theorems
HOL Light is proving for me. The HOL4 Logic manual looks like a very
respectable CS document, but I haven't been able to read it yet, and it's not a
HOL Light document. With my Tarski code, I would be happy to say (though I
don't quite understand it) that HOL Light was verifying my FOL proofs using
Tarski's geometry axioms. But there's real HOL in my Hilbert code funneled
through sets.ml. Of course I know what results I meant to prove, and my
results use sets as mathematicians customarily use sets. I figure that's the
result that HOL Light proved for me, but I'm missing the translation. A simple
example of a result of mine I can't translate from math to HOL Light is
OriginInRay_THM below, which leads me into my next problem:
John promised to write some set theory that miz3 can't handle after I finished
formalizing my plane geometry. I can live without it, but it would be nice to
be able to fix something. In the following 75 lines of miz3 code, everything
works fine, including my set theoretic definition
Ram_DEF : thm =
|- !A B. ram A B = {X | ~(A = B) /\ Collinear A B X /\ A NOTIN open (X,B)}
except for a timeout error on my last thm. No problems arise with the funny
set theoretic definition
Ray_DEF : thm =
|- !A B X. ray A B X <=> ~(A = B) /\ Collinear A B X /\ A NOTIN open (X,B)
--
Best,
Bill
#load "unix.cma";;
loadt "miz3/miz3.ml";;
horizon := 0;;
timeout := 30;;
new_type("point",0);;
new_type_abbrev("point_set",`:point->bool`);;
new_constant("Between",`:point->point->point->bool`);;
new_constant("Line",`:point_set->bool`);;
parse_as_infix("NOTIN",(11, "right"));;
let NOTIN = new_definition
`!a:A l:A->bool. a NOTIN l <=> ~(a IN l)`;;
let Interval_DEF = new_definition
`! A B X. open (A,B) X <=> Between A X B`;;
let Collinear_DEF = new_definition
`Collinear A B C <=>
? l. Line l /\ A IN l /\ B IN l /\ C IN l`;;
let B1 = new_axiom
`! A B C. Between A B C ==> ~(A = B) /\ ~(A = C) /\ ~(B = C) /\
Between C B A /\ Collinear A B C`;;
let B1' = thm `;
! A B C. B IN open (A,C) ==> ~(A = B) /\ ~(A = C) /\ ~(B = C) /\
B IN open (C,A) /\ Collinear A B C
by IN, Interval_DEF, B1`;;
let I1 = new_axiom
`! A B. ~(A = B) ==> ?! l. Line l /\ A IN l /\ B IN l`;;
let Ray_DEF = new_definition
`! A B X. ray A B X <=> ~(A = B) /\ Collinear A B X /\ A NOTIN open (X,B)`;;
let OriginInRay_THM = thm `;
let O Q be point;
assume ~(Q = O) [H1];
thus O IN ray O Q
proof
O NOTIN open (O,Q) [OOQ] by B1', NOTIN;
consider l such that
Line l /\ O IN l /\ Q IN l by H1, I1;
Collinear O Q O by -, Collinear_DEF;
qed by H1, -, OOQ, IN, Ray_DEF`;;
let EndpointInRay_THM = thm `;
let O Q be point;
assume ~(Q = O) [H1];
thus Q IN ray O Q
proof
O NOTIN open (Q,Q) [notOQQ] by B1', NOTIN;
consider l such that
Line l /\ O IN l /\ Q IN l by H1, I1;
Collinear O Q Q by -, Collinear_DEF;
qed by H1, -, notOQQ, IN, Ray_DEF`;;
let Ram_DEF = new_definition
`! A B. ram A B = {X:point | ~(A = B) /\ Collinear A B X /\ A NOTIN open
(X,B)}`;;
let OriginInRam_THM = thm `;
let O Q be point;
assume ~(Q = O) [H1];
thus O IN ram O Q
proof
O NOTIN open (O,Q) [OOQ] by B1', NOTIN;
consider l such that
Line l /\ O IN l /\ Q IN l by H1, I1;
Collinear O Q O by -, Collinear_DEF;
qed by H1, -, OOQ, IN, Ram_DEF`;;
------------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
