I made real progress on my set theory problem, but I'd like to do even better.
My 3860 lines of miz3 Hilbert axiomatic geometry code
http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz
now uses set abstraction to define rays:
let Ray_DEF = new_definition
`! A B. ray A B = {X:point | ~(A = B) /\ Collinear A B X /\ A NOTIN open
(X,B)}`;;
This works because of the theorem I then prove, following sets.ml
let IN_Ray = prove
(`! A B X:point. X IN ray A B <=> ~(A = B) /\ Collinear A B X /\ A NOTIN open
(X,B)`,
REWRITE_TAC[IN_ELIM_THM; Ray_DEF]);;
I then replaced every occurrence of `IN, Ray_DEF' with the sets.ml-friendly
`IN_Ray'. I have no idea why IN_Ray works, and I borrowed code from sets.ml:
let UNION = new_definition
`s UNION t = {x:A | x IN s \/ x IN t}`;;
let IN_UNION = prove
(`!s t (x:A). x IN (s UNION t) <=> x IN s \/ x IN t`,
REWRITE_TAC[IN_ELIM_THM; UNION]);;
This is partly explained on p 91--92 of the HOL Light tutorial:
In order to eliminate the set abstraction from a term of the form
x ∈ {t | p}, rewrite with the theorem IN_ELIM_THM [of sets.ml], which will
nicely eliminate the internal representation of set abstractions, e.g.
# REWRITE_CONV[IN_ELIM_THM]
‘z IN {3 * x + 5 * y | x IN (:num) /\ y IN (:num)}‘;;
val it : thm =
|- z IN {3 * x + 5 * y | x IN (:num) /\ y IN (:num)} <=>
(?x y. (x IN (:num) /\ y IN (:num)) /\ z = 3 * x + 5 * y)
The tutorial then explains {A, B} is syntactic sugar for A INSERT B INSERT {}.
INSERT is defined in sets.ml as
let INSERT_DEF = new_definition
`x INSERT s = \y:A. y IN s \/ (y = x)`;;
That kinda sounds like saying a set abstraction is a lambda, but that can't be,
because p 100 of the HOL Light tutorial says something I need to understand:
Since MESON’s handling of lambdas is a bit better than its handling
of set abstractions,
If anyone can explain any of these mysteries, I'd be happy to listen. But what
I'd really like is a way to prove IN_Ray in miz3.
--
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
