Hi Bill,
There are a few points which you may or may not already realise. Sorry if
these are obvious, but I haven't been following the (very lengthy!) thread
in detail.
1. Just checking you understand this: In HOL Light and HOL4 (but not
ProofPower HOL), sets are represented as functions to booleans, so a set
with elements of type A is represented as a function from A to bool. Enter
the following in a HOL Light session to confirm this:
type_of ` { 10 }`;;
> 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 ...
2. `{A,B}` is a set enumeration, not a set abstraction, so I'm not sure why
you are pointing to the definition of "INSERT" (which is used in the
representation of set enumerations) and then talking about set abstractions.
But anyway, any set enumeration or set abstraction is of course a set, and,
in HOL Light, any set is a function (as explained by 1.), which is what a
lambda is, so there should be no surprise that a set abstraction/enumeration
can be expressed as a lambda in HOL Light.
> ... 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,
3. Lambdas are used in the representation of set abstractions, but the
representation is quite complicated and also involves a few other things,
and presumably it is these other things that MESON is not so good at.
Hope this helps.
Mark.
on 12/8/12 3:45 AM, Bill Richter <rich...@math.northwestern.edu> wrote:
> 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-LightMiz3HilbertAxiomGe
> ometry.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
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
>
------------------------------------------------------------------------------
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
