Michael, Konrad, Rob, Mark, Cris, thank you very much for all the messages!
This partly answers many questions that have puzzled me. Among other things,
I'm well on way to having to give you guys acknowledgments in my paper. I
think the point of an acknowledgment isn't to pay someone for help, but to tell
the audience that this person is a valuable resource. This was a valuable
advice I got today. I really had no idea what a type was, or the relationship
between HOL and ZFC. And John is back, with great looking photos that suggest
he recharged his soul climbing mountains in the Rockies! I'll mostly just ask
a technical question about sets.ml raised by Michael & Konrad.
Rob, your Andrews book looks good, and I grabbed the preface, and downloaded
the wiki Type_theory entry.
Michael, your comparison between the complicated { n + 1 | n > 6 } and the
simpler { x | P x } suggests that sets.ml doesn't need such a complicated
result as IN_ELIM_THM, that there should be a simpler proof of my first thm
# val IN_Interval : thm = |- !A B X. X IN open (A,B) <=>
Between A X B
that uses of course my first definition
# val Interval_DEF : thm = |- !A B. open (A,B) = {X | Between A X B}
but doesn't use IN_ELIM_THM. Maybe even a miz3 proof!
BTW the sets.ml defs of "HOL Light's GSPEC and SETSPEC" are very simple. Here
are the first 4 results of sets.ml:
let IN = new_definition
`!P:A->bool. !x. x IN P <=> P x`;;
let EXTENSION = prove
(`!s t. (s = t) <=> !x:A. x IN s <=> x IN t`,
REWRITE_TAC[IN; FUN_EQ_THM]);;
let GSPEC = new_definition
`GSPEC (p:A->bool) = p`;;
let SETSPEC = new_definition
`SETSPEC v P t <=> P /\ (v = t)`;;
Michael, I need clarification here, because Rob said that HOL ought to be
called "polymorphic typed set theory":
A type is a non-empty set. A term denotes a value in a type (i.e., an
element
of the non-empty set denoted by the type that term has).
(Simplifying slightly; the above is true as long as the type is not
polymorphic.)
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. 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:
let IN_INTER = prove
(`!s t (x:A). x IN (s INTER t) <=> x IN s /\ x IN t`,
REWRITE_TAC[IN_ELIM_THM; INTER]);;
let IN_DELETE = prove
(`!s. !x:A. !y. x IN (s DELETE y) <=> x IN s /\ ~(x = y)`,
REWRITE_TAC[IN_ELIM_THM; DELETE]);;
Is your HOL4 set abstraction mechanism so simple that you don't need a big
hammer like IN_ELIM_THM?
http://www.proof-technologies.com/misc/Glossary.txt
Thanks, Mark, I'll read it!
I prefer not to say that a type is a set, because the set of all
things having a type is expressible as \x. T (or {x | T}.
Cris, I'm tempted to go with Michael, who sorta disagreed with you above. Let
me try to resolve the semi-disagreement. My guess is that if you can really
write {x | T}, then that means that we're doing all our type theory in a
"universe" which in ZFC would actually be called a set. The model of ZFC isn't
going to be a set, by Russell's paradox, and that's a way in which HOL is
weaker than ZFC, a weakness that doesn't bother me at all.
--
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
