Thanks for the exercise, John! Konrad's tips were very helpful, and here's a
awkward-looking miz3 solution below (using the default timeout of 1). As
Konrad said, this is really an exercise in sets.ml, and CARD is a part of
sets.ml I didn't know anything about. Miz3Tips, which as you noted needs a
lot of work, is now distributed in the latest subversion of HOL Light, in the
dir RichterHilbertAxiomGeometry. As Konrad said, much of sets.ml can indeed
be reproved using miz3 and BETA_THM of theorems.ml, and that's a nice exercise.
--
Best,
Bill
let JohnCard0_THM = thm `;
(CARD ({}:A->bool)) = 0
by CARD_CLAUSES;
`;;
let JohnCard1_THM = thm `;
let x be A;
thus (CARD {x}) = 1
proof
FINITE ({}:A->bool) /\ (CARD ({}:A->bool)) = 0 by FINITE_RULES,
CARD_CLAUSES;
(CARD {x}) = SUC(0) by -, MEMBER_NOT_EMPTY, CARD_CLAUSES;
qed by -, ONE;
`;;
let JohnCard2_THM = thm `;
let x y be A;
assume ~(x = y) [not_xy];
thus (CARD {x, y}) = 2
proof
FINITE ({y}) /\ (CARD {y}) = 1 by FINITE_RULES, JohnCard1_THM;
(CARD {x, y}) = SUC(1) by -, not_xy, IN_SING, CARD_CLAUSES;
qed by -, TWO;
`;;
let JohnCard3_THM = thm `;
let x y z be A;
assume ~(x = y) /\ ~(x = z) /\ ~(y = z) [Distinct];
thus (CARD {x, y, z}) = 3
proof
FINITE ({x}) /\ (CARD {x}) = 1 [C1] by FINITE_RULES, JohnCard1_THM;
FINITE ({y, z}) /\ (CARD {y, z}) = 2 [C2] by FINITE_RULES, Distinct,
JohnCard2_THM;
{x} INTER {y, z} = {} [Disjoint] by Distinct, SET_RULE;
{x, y, z} = {x} UNION {y, z} by SET_RULE, INSERT_UNION_EQ;
(CARD {x, y, z}) = 1 + 2 by C1, C2, -, Disjoint, CARD_UNION;
qed by -, ARITH_RULE;
`;;
------------------------------------------------------------------------------
LogMeIn Central: Instant, anywhere, Remote PC access and management.
Stay in control, update software, and manage PCs from one command center
Diagnose problems and improve visibility into emerging IT issues
Automate, monitor and manage. Do more in less time with Central
http://p.sf.net/sfu/logmein12331_d2d
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
