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
Hi John,
No it's not that hard. A calculation-like goal such as
CARD {3;4} = 2
is a one-liner in HOL4 and I'd be surprised if that wasn't also
true in HOL-Light. In HOL4 the one-liner is an invocation of the
simplifier, using the implicit set of rewrites, so
RW_TAC (srw_ss()) []
solves
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
Hello John,
On 04/11/2012 03:48, John Nicol wrote:
Never figured out why
real#real is a different type than real*real (they're both just tuples,
right?), but I digress.
Unless I'm missing something, real*real is the OCaml notation for a pair
of reals, whereas real#real is the HOL Light
Hi Konrad,
Thanks! I hope it turns out to be that easy in HOL Light :-)
Yes, I browsed sets.ml, which is how I found the various FINITE_* tactics
and theorems. I also did greps on the sources to look for uses of CARD and
HAS_SIZE and see how they were used. No dice.
{3,4} in HOL Light is set
Thanks Bill and Petros for the comments and the code!
Petros, now the need for the real#real type makes perfect sense to me. (I
originally wrote my definitions with OCaml type syntax, and it took me a
long time to figure out why it was failing.) So it's not just me that's
had difficulties with
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
Hi,
I know it is not really what John asked for, but, well, just for fun, I
developped a conversion and a tactic to deal with this kind of goals
(in some sense, it can thus be considered as an Easy button).
From my (basic) tests it should work quite well.
Please find them in the attached file.
