Hi Thomas, thanks very much, now I see the possibility of changing whatever variable names I want! (I never knew nor needed ALPHA before, although alpha-conversion is familiar to me)
—Chun > Il giorno 03 ago 2018, alle ore 15:03, Thomas Tuerk <tho...@tuerk-brechen.de> > ha scritto: > > Hi Chun, > > the easiest way is using alpha-equivalence. If you really just want to rename > vars, you can state the new form explicitly and use apha-equivalence via e.g. > ALPHA directly. Tools like METIS_TAC should in theory be able to do it, but > in practice try to do too much and therefore time out, I fear. > > There are also tools for renaming bound vars. "rename_bvar" for example is a > conversion for renaming an outermost bound var. > Variables at subpositions can also be renamed using the quantifier heuristics > lib (see, e.g. INST_QUANT_CONV) > > Vaguely related are tools for renaming free vars during a tactical proof. > There are various related tactics for this, e.g. RENAME_TAC. However, since > these deal with free vars during a proof, this does not fit really here. > > So, there are plenty of options. Looking at your description, I expect using > ALPHA is the easiest and fasted possibility for your problem. I would use > something like > > fun ALPHA_RULE t thm = let > val t0 = concl thm > val thm1 = ALPHA t0 t > val thm2 = EQ_MP thm1 thm > in > thm2 > end > > > val t0 = ``?A. A \/ !B C. ?D. D B C`` > val t = ``?A'. A' \/ !B' C. ?DD. DD B' C`` > > val thm0 = METIS_PROVE [] t0 > val thm = ALPHA_RULE t thm0 > > Best > > Thomas > > > > On 03.08.2018 14:34, Chun Tian (binghe) wrote: >> 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 >> >> >> >> ------------------------------------------------------------------------------ >> Check out the vibrant tech community on one of the world's most >> engaging tech sites, Slashdot.org! http://sdm.link/slashdot >> <http://sdm.link/slashdot> >> >> _______________________________________________ >> hol-info mailing list >> hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net> >> https://lists.sourceforge.net/lists/listinfo/hol-info >> <https://lists.sourceforge.net/lists/listinfo/hol-info> > > ------------------------------------------------------------------------------ > 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
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
