John Nicol, you may not need this anymore, but a miz3 tip that I learned from
your CARD exercise. Miz3 solves this immediately:
let notXinterYZ_THM = thm `;
! x y z: A. ~(x = y) /\ ~(x = z) /\ ~(y = z) ==> {x} INTER {y, z} = {}
by SET_RULE;
`;;
(* But let's try to get rid of the powerful tactic SET_RULE. I would think the
right way to do this is *)
horizon := 0;;
timeout := 50;;
let notXintYZ_THM = thm `;
! x y z: A. ~(x = y) /\ ~(x = z) /\ ~(y = z) ==> {x} INTER {y, z} = {}
by IN_INTER, IN_SING, IN_INSERT, MEMBER_NOT_EMPTY;
`;;
(* The MESON solved at number is quite high, 558,115! Here's a proof with a
MESON solved at number 25: *)
timeout := 1;;
let XdisjointYZ = thm `;
let x y z be A;
assume ~(x = y) /\ ~(x = z) /\ ~(y = z) [Distinct];
thus {x} INTER {y, z} = {}
proof
! a. ~(a IN {x} INTER {y, z})
proof
let a be A;
~(a IN {x} INTER {y, z})
proof
~(a IN {x}) \/ ~(a IN {y, z})
proof
assume a IN {x};
a = x by -, IN_SING;
~(a = y) /\ ~(a = z) by -, Distinct;
~(a IN {y, z}) by -, IN_INSERT, IN_SING;
qed by -;
qed by -, IN_INTER;
qed by -;
qed by -, MEMBER_NOT_EMPTY;
`;;
Here's the sense in this proof. The first claim
! a. ~(a IN {x} INTER {y, z})
is equivalent to our theorem by MEMBER_NOT_EMPTY. In the proof of this claim,
the first two lines
let a be A;
~(a IN {x} INTER {y, z})
are obligatory. Now IN_INTER say that to prove that, it suffices to show
~(a IN {x}) \/ ~(a IN {y, z})
so that's our next statement to be proved.
This statement follows easily from IN_SING, Distinct & IN_INSERT.
Final tip: I didn't write this proof in this order. I first started with this
skeleton proof:
let XdisjointYZ = thm `;
let x y z be A;
assume ~(x = y) /\ ~(x = z) /\ ~(y = z) [Distinct];
thus {x} INTER {y, z} = {}
proof
! a. ~(a IN {x} INTER {y, z})
proof
qed by -;
qed by -, MEMBER_NOT_EMPTY;
`;;
I got only one error, a #1 inference error after the line
qed by -;
That shows that proof will be correct once we fill in the proof of
! a. ~(a IN {x} INTER {y, z}). And so on.
--
Best,
Bill
------------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
