Michael, I'm really grateful to you, as you cleared up my main problem:
> Now is my interpretation of my own code correct?
Your interpretation of what you've written seems fine to me.
That's great. I have to tell my audience of mathematicians what theorems HOL
Light is verifying, even if I don't understand how. I'd like to understand HOL
better, and so let me ask some more baby questions. I think my first def & thm
let Interval_DEF = new_definition
`! A B. open (A,B) = {X | Between A X B}`;;
let IN_Interval = prove
(`! A B X. X IN open (A,B) <=> Between A X B`,
REWRITE_TAC[IN_ELIM_THM; Interval_DEF]);;
give a counterexample to what you wrote:
If you never use that [{ n + 1 | n > 6 }] notation, then it's
certainly fine to just view { x | P x } as a fancy way of writing
(λx. P x).
I'll give 3 reasons below to indicate this isn't true for me (I love your λ,
BTW, and I suppose you can use it in HOL4). Let me first say that I think you
understand this, as Konrad just posted something of this sort:
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.
Konrad must be referring to the annoying-to-reason-with properties of {...},
because the sets.ml definition of INTER is very simple:
let INTER = new_definition
`s INTER t = {x:A | x IN s /\ x IN t}`;;
Reason-1) I'll write a lambda version of this, with miz3 code that proves the
IN_<operation> result:
#load "unix.cma";;
loadt "miz3/miz3.ml";;
parse_as_infix("inter",(20, "right"));;
let inter_DEF = new_definition
`! s t:A->bool. s inter t = \x:A. x IN s /\ x IN t`;;
let IN_inter = thm `;
let x be A;
let s t be A->bool;
thus x IN s inter t <=> x IN s /\ x IN t
by inter_DEF, IN, BETA_THM`;;
This works fine, and my output is
# Warning: Benign redefinition
val inter_DEF : thm = |- !s t. s inter t = (\x. x IN s /\ x IN t)
# val IN_inter : thm = |- !x s t. x IN s inter t <=> x IN s /\ x
IN t
Reason-2) This miz3 code below seems to show that my {...} is not the obvious
lambda:
let AbstractionLambda = thm `;
let A B be point;
thus A = A
proof
open (A,B) = {X | Between A X B} by Interval_DEF;
open (A,B) = \X:point. Between A X B by Interval_DEF;
open (A,B) = (\X. Between A X B) by Interval_DEF;
qed`;;
Miz3 buys my first line (the definition), if I first run my Hilbert geometry
code
http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz
but I get a #1 inference error after the 2nd and 3rd lines.
Reason-3) Just to check, let's make sure that miz3 doesn't buy an
IN_<operation> proof similar to (1):
let IM_interval = thm `;
let A B X be point;
thus X IN open (A,B) <=> Between A X B
by Interval_DEF, IN, BETA_THM`;;
I get a #1 inference error. So that's 3 reasons why I think my set
abstractions {...} are not the obvious lambdas. And it raises the obvious
question: why don't I just rewrite sets.ml to use the obvious lambdas? What
will I miss, other than the beautiful {...} notation? Even if what you wrote
isn't technically true, it's true in spirit, right? We really think that given
a set X, we defined a subset of X by a boolean function on X, right?
Rob, I looked up your Axiom of Replacement, which I wasn't familiar with:
http://en.wikipedia.org/wiki/Axiom_schema_of_replacement
In particular, ZF proves the consistency of Z, as the set Vω·2 is a model of
Z constructible in ZF. [...]
The axiom schema of replacement is not necessary for the proofs of most
theorems of ordinary mathematics.
So I'm cool with HOL skipping the Axiom of Replacement, and I'll start saying
ZC here instead ZFC.
--
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
