Michael, here's a 1-line HOL Light proof of your exercise { x | x ∈ P ∧ x ∈ Q}
= λx. P x ∧ Q x:
let IntersectionAbstractionIsLambda = prove
(`!P Q :A->bool. {x | x IN P /\ x IN Q} = \x. x IN P /\ x IN Q`,
REWRITE_TAC[IN_ELIM_THM; EXTENSION]);;
If you can't do that in HOL4, that's evidence for my feeling that IN_ELIM_THM
is hard to understand. This clearly shows that John was right, that miz3 has
some problems with sets, as I couldn't quite prove this in miz3. The more
general result has the same 1-line proof:
let AbstractionIsLambda = prove
(`!P:A->bool. {x | P x} = \x. P x`,
REWRITE_TAC[IN_ELIM_THM; EXTENSION]);;
So you really taught me something: a set abstraction {...} is a lambda! That's
really cool, and I see no reason not to code up the parts of sets.ml using
lambdas. I'll get much simpler proofs at the meaningless cost of not seeing a
few nice {...} in the definitions. I got started already, and redid my 4000
lines of Hilbert axiomatic geometry miz3 code using lambda defs for INSERT,
EMPTY, SING, and union.
http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz
Each of these except UNION was already defined as a lambda in sets.ml, but I
think my proofs of the basic properties are simpler. At least, I can I
understand them. Here's an example of my union defs & thms being used:
let Angle_DEF = new_definition
` angle A O B = ray O A union ray O B `;;
let AngleSymmetry_THM = thm `;
! A O B. angle A O B = angle B O A
by Angle_DEF, union_COMM`;;
--
Best,
Bill
let IN_INSERT = thm `;
let x y be A;
let s be A->bool;
thus x IN (y INSERT s) <=> (x = y) \/ x IN s
by INSERT_DEF, IN, BETA_THM`;;
let NOT_IN_EMPTY = thm `;
let x be A;
thus ~(x IN {})
by EMPTY, IN, BETA_THM`;;
let IN_SING = thm `;
let x y be A;
thus x IN {y} <=> x = y
by NOT_IN_EMPTY, IN_INSERT, IN, BETA_THM`;;
let SING_SUBSET = thm `;
let x be A;
let s be A->bool;
thus {x} SUBSET s <=> x IN s
by IN_SING, SUBSET, IN, BETA_THM`;;
(* now define union as a lambda, not the set abstraction UNION from sets.ml *)
parse_as_infix("union",(16, "right"));;
let union = new_definition
`! s t:A->bool. s union t = \x. x IN s \/ x IN t`;;
let union_SUBSET = thm `;
let s t u be A->bool;
thus (s union t) SUBSET u <=> s SUBSET u /\ t SUBSET u
by union, SUBSET, IN, BETA_THM`;;
let IN_union = thm `;
let x be A;
let s t be A->bool;
thus x IN (s union t) <=> x IN s \/ x IN t
by union, IN, BETA_THM`;;
let union_COMM = thm `;
let s t be A->bool;
thus s union t = t union s
proof
! x. x IN s union t <=> x IN s \/ x IN t [union1] by IN, union;
! x. x IN t union s <=> x IN s \/ x IN t by IN, union;
! x. x IN s union t <=> x IN t union s by union1, -;
qed by -, EXTENSION`;;
------------------------------------------------------------------------------
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
