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})`;;
I don't know how to define the types of triples "S^3", but I can read
the reference manual to try to figure this out. I have another dumb
question below, but first let me explain why I need sets.
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. 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.
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))`;;
(* error message: Exception: Failure "typechecking error (initial type
assignment)". *)
new_constant("Twiddle6",`:line->point#point->bool`);;
parse_as_infix("Twiddle6",(12, "right"));;
let Twiddle6_DEF = new_definition
`l Twiddle6 A,B <=>
~(?X. (X on_line l) /\ Between(A, X, B))`;;
--
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
