> Konrad, this is very interesting, because it's so much like sets.ml:
>
> There is also a description of sets in HOL4 in the manual. Start at
> p. 102 of the HOL4 Description document:
>
> Yours & Michael's Description manual starts pretty much like sets.ml which I
> cited above.
Not surprising. Those are the usual definitions of the standard
operations on sets. Also,
there is some overlap in naming styles between HOL4 and HOL Light. Many of the
theorems having to do with sets probably have the same name even,
because of the way these systems evolved from a common ancestor.
> What I don't see is anything like what I'm having trouble with, the IN_*
> theorems.
> Here are two from sets.ml I use constantly:
Those theorems are indeed present and heavily used in HOL4. Think of
it this way:
each basic set operation (union, intersection, complement, powerset,
difference, etc)
is defined via a set abstraction. These definitions tend to be
annoying to reason with,
so for each definition, a theorem with the name IN_<operation> is
proved. These theorems are rewrite rules that push the "IN" operator
deeper into whatever expression they are applied to. IN_INTER is a
typical example.
> Is your HOL4 set abstraction mechanism so simple that you don't need a
> big hammer like IN_ELIM_THM?
It's not simple, as a reading of section 3.5.1.1. in the HOL4
Description reveals.
When abstracting over multiple variables the representation becomes
unfortunately complex and hence expressions like
z IN {x + y | x * y > w}
do not easily reduce to something useful.
Konrad.
------------------------------------------------------------------------------
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
