Hi Bill,
| John, using your new axiom framework, with help from Freek, I ported my
| Tarski geometry Mizar code up to Gupta's theorem (code below). Thanks again
| for your three frameworks!
That's great, I'm glad it's working out so well! I just loaded your
code and it worked smoothly for me to. It is indeed a tribute to
Freek's miz3 more than to my own work, I think :-)
| Can you look at the top of my
| code? I could not see how to define the predicates
| ORDERED a,b,c,d
| x on_line a,b
| I failed to modify your `parse_as_infix' defs of === and cong.
Although there is a notion of a "prefix" in HOL Light, this only
forces right-associativity of unary function applications, whereas
binary ones like "," still have lower precedence. So for ORDERED, I
recommend just parenthesizing the quadruples, as I did with "Between".
let ORDERED_DEF = new_definition
`ORDERED (a,b,c,d) <=>
Between (a,b,c) /\ Between (a,b,d) /\ Between (a,c,d) /\ Between (b,c,d)`;;
I think your on_line definition should basically work more or less
as written, using the parse_as_infix and Line_DEF calls you have. But
you have some special character in your definition that may be left
over from the Mizar version. I guess it's meant to be /\ or ==>. If
you replace it by its HOL ASCII counterpart, I think it will work
fine.
Just a comment on comments from the other thread: you can always put
comments in miz3 proofs by using the native HOL Light convention,
which is a BCPL-style "//" one-line comment.
let EquivReflexive = thm `;
!a b. a,b === a,b
// This is a really easy proof
proof
let a b be point; // point is the type of a and b
b,a === a,b by A1; // A1 is our first axiom
qed by -, A2 // Note that we use the previous line here`;;
But as far as I can see the native Mizar style :: is supposed to work
in miz3 too, so I'll defer to Freek on that.
| I just read Harrison's talk and the first thing that comes to my
| mind is to get started on algebraic topology in a systematic way.
| Let's forget proving just the big theorems and build the whole
| thing.
|
| I wish I had the time to say I am volunteering, but I cannot right
| now. Of course, I guess you first need to build some algebra and
| either topological spaces or simplicial sets.
Yes, I agree completely that doing algebraic topology systematically
would be more satisfying than these ad hoc tours de force. I know
several people have expressed an interest in this, but I don't know
if anyone has worked on it seriously. HOL Light does have some
rudimentary results on homotopy of paths in R^n and quite a lot of
useful lemmas about polyhedra, with even a definition of simplicial
complex (see Multivariate/polytope.ml):
|- simplicial_complex c <=>
FINITE c /\
(!s. s IN c ==> ?n. n simplex s) /\
(!f s. s IN c /\ f face_of s ==> f IN c) /\
(!s s'. s IN c /\ s' IN c
==> (s INTER s') face_of s /\ (s INTER s') face_of s')
I am hopeful that these might represent some sort of starting point
for serious algebraic topology, but I don't think I'll have the time
to work on this myself any time soon either!
John.
------------------------------------------------------------------------------
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
