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
