See also Conv.RENAME_VARS_CONV
On Fri, Aug 3, 2018 at 9:00 AM Chun Tian (binghe) <binghe.l...@gmail.com>
wrote:
> 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://slashdot.org>!
> http://sdm.link/slashdot
>
>
>
> _______________________________________________
> hol-info mailing
> listhol-info@lists.sourceforge.nethttps://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://slashdot.org>!
> http://sdm.link/slashdot_______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> 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
>
------------------------------------------------------------------------------
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
