Hi, suppose I have proved (or generated) a theorem like this:
⊢ ∀a0 a1.
a0 ∼ a1 ⇔
∀u.
(∀E1. a0 --u-> E1 ⇒ ∃E2. a1 --u-> E2 ∧ E1 ∼ E2) ∧
∀E2. a1 --u-> E2 ⇒ ∃E1. a0 --u-> E1 ∧ E1 ∼ E2
but I don’t like the variables names (a0, a1, E1, E2), I want a new theorem,
essentially the same one, but with variables names same as in text book:
⊢ ∀P Q.
P ∼ Q ⇔
∀u.
(∀P'. P --u-> P' ⇒ ∃Q'. Q --u-> Q' ∧ P' ∼ Q') ∧
∀Q'. Q --u-> Q' ⇒ ∃P'. P --u-> P' ∧ P' ∼ Q’
if I understood HOL correctly, it is impossible to directly modify any theorem
(as first-class object), replacing its bound variables with different names (if
not conflicting others).
Actually, changing the outside universal quantifiers is easy, as I just need to
do a SPEC with new variables, then GEN them. On the other side, I don’t see any
automatic way to replace inner variables. I also tried to prove the new
theorem by PROVE_TAC or METIS_TAC with the old theorem, sometimes the theorem
can be directly proved, but most of time it fails, I think because of those
existential quantifiers.
Does anyone have such experiences? (it’s a painful process to go over all
proofs again, fixing almost every step with different variable names)
Regards,
Chun Tian
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
