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
>
>
> _______________________________________________
> 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
