Actually, something similar to your alternative characterisation is available
but in a hard to know about way.
Try boolLib.EXISTS_UNIQUE_ALT:
``!P:'a->bool. (?!x. P x) <=> ?x. !y. P y <=> (x = y)``,
Also, as the simplifier does beta-reduction “for free”, I’d change what you had
to
pop_assum (qx_choose_tac `f12` o SIMP_RULE bool_ss [EXISTS_UNIQUE_ALT])
You could also accept the system’s choice of name and/or rename it later, and
just use fs[EXISTS_UNIQUE_ALT].
Note that all three of the suggestions will do slightly different things, and
this difference can be significant in various situations. You might like to
try to figure what those differences are, and decide if they matter to you in
general and/or in your specific goal
Michael
From: Haitao Zhang <zhtp...@gmail.com>
Date: Wednesday, 27 February 2019 at 16:02
To: hol-info <hol-info@lists.sourceforge.net>
Subject: [Hol-info] Exists unique quantifier
I have trouble figuring out the best way to deal with exists unique quantifers.
The existing theorems rewrite it in a way that does not work with CHOOSE_TAC or
X_CHOOSE_TAC:
EXISTS_UNIQUE_DEF;
|val it = ⊢ $?! = (λP. $? P ∧ ∀x y.
P x ∧ P y ⇒ (x = y)): thm
The top level connective is a conjunction not an exists.
So I proved a version that I thought would be better with a top level exists
connective:
EXISTS_UNIQUE_EXISTS;
|val it = ⊢ $?! = (λP. ∃x. P x ∧
∀y. P y ⇒ (y = x)): thm
``?! = \P:'a->bool. (?x. P x /\ !y. P y ==> (y=x))``
Now I can do choose:
e (POP_ASSUM (Q.X_CHOOSE_TAC `f12` o BETA_RULE o (PURE_REWRITE_RULE
[EXISTS_UNIQUE_EXISTS])));
Is this a good way to deal with exists unique? I am surprised that I couldn't
find a shrink-wrap way of doing it.
Thanks,
Haitao
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
