Hi Bill,
| Thanks, John! Yet again you were extremely helpful. Your fix works:
|
| let plane = new_definition
| `plane S Between Equiv <=>
| (Between SUBSET {(x,y,z) | x IN S /\ y IN S /\ z IN S} /\
| Equiv SUBSET {(x,y,z,w) | x IN S /\ y IN S /\ z IN S /\ w IN S})`;;
Yes, that seems to be the most general way of setting things up.
However, given the rather limited way in which HOL Light lets you
parse things as infix, you might consider setting up Equiv to be
a (curried) binary relation between S^2 and S^2 rather than a
subset of S^4, with a clause like this (assuming "Equiv" has been
declared infix):
(!x y z w. (x,y) Equiv (z,w) ==> x IN S /\ y IN S /\ z IN S /\ w IN S)
| The way I organized my Hilbert paper was to define a Hilbert plane S,
| a set whose elements we call points, with subsets called lines, which
| has Betweenness and relations satisfying 13 axioms. Then for solid
| geometry I say we have a set Space with certain subsets S which are
| Hilbert planes.
Yes, I like this approach. I would certainly very much support your
idea in another message of formalizing the whole paper, though of
course it would represent a lot of work. Not only would it give you
about as high a level of assurance as you could want, but it might be
a useful basis for analyzing, for example, just what set-theoretic
properties you actually end up using and hence clarify the
relationship with the other way of formalizing it using unanalyzed
concepts for "line" etc. instead of considering them as subsets of
points.
| These two alternatives seems unpleasant:
|
| 1) to go back and redefine one axioms, using the new term coplanar,
| and then reprove all the theorems (the fixes are all easy).
|
| 2) be doing solid geometry from the beginning: that's tough on a high
| school audience, who have enough trouble with plane geometry.
My own instinct would be be something like (1). You would have some
"space" with certain subsets that you call "lines" or "planes". Then
the 2-dimensional theorems would have some ambient plane P at the
beginning:
!P:point->bool. plane P ==> !x y. x IN P /\ Y IN P ==> ...
You would effectively relativize all quantifiers to this plane P
and then just assume in the first hypothesis that it is a plane.
And for axioms or theorems that are true in higher dimensions,
you might as well omit the "plane" hypothesis. The reason this
works nicely is precisely that you do model most other concepts
as sets of points with certain properties instead of some other
unanalyzed category.
| new_type("point",0);;
| new_type("line",0);;
| new_constant("on_line",`:point->line->bool`);;
| parse_as_infix("on_line",(12, "right"));;
| new_constant("Between",`:point#point#point->bool`);;
|
| new_constant("Twiddle",`:point->line->point->bool`);;
|
| let Twiddle_DEF = new_definition
| `Twiddle(A, l, B) <=>
| ~(?X. (X on_line l) /\ Between(A, X, B))`;;
First of all, there is the issue of currying versus uncurrying
again: if you want to write Twiddle(A, l, B) then you need to
make the type of Twiddle `:point#line#point->bool`, or if you
want to keep the type as ``:point->line->point->bool` you need
to write `Twiddle A l B`. Also, if you are going to make an
actual definition of Twiddle then you should delete the line
that declares the constant (since definitions already do that,
and will complain if the constant exists);
new_constant("Twiddle",`:point->line->point->bool`);;
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
