Thanks, John! Here's a better version of my miz3 code and an exercise for you.
I think Konrad gave you excellent advice, especially considering that HOL4
does not yet have anything like miz3. I thought Konrad said that writing
declarative proofs in miz3 is a very good way to actually learn HOL Light,
because instead of just heaving tactics at the wall to see if anything sticks,
you have to understand why the tactics work. Well, I used a powerful tactic
myself, SET_RULE, which was very helpful in shortening my Geometry code. So
here's a version of my code which doesn't use SET_RULE, and has many fewer
parentheses, but it comes at the prices of a high timeout, and a MESON "solved
at" number of 558,115, and I think that's all just proving
{x} INTER {y, z} = {} [Disjoint] by Distinct, IN_INTER, IN_SING,
IN_INSERT, MEMBER_NOT_EMPTY;
Can you prove this with a much lower timeout? Preferable the default timeout
:= 1;;. I think the way to do that is to understand the meaning of IN_INTER in
terms of !, perhaps using SUBSET_ANTISYM, and it would make sense to call this
a separate thm, at least until it works.
--
Best,
Bill
horizon := 0;;
timeout := 50;;
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} INTER {y, z} = {} [Disjoint] by Distinct, IN_INTER, IN_SING,
IN_INSERT, MEMBER_NOT_EMPTY;
:: {x, y, z} = {x} UNION {y, z} by SET_RULE, INSERT_UNION_EQ;
{x, y, z} = {x} UNION {y, z} by INSERT_UNION_EQ, UNION_EMPTY;
(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
