Hi, I found that, if I call SPEC_ALL on the theorem with qualified variables, and then call GEN_ALL on the resulting theorem, the order of qualified variables may get changed:
> GEN_ALL (SPEC_ALL (ASSUME ``!A B C. B + C = A``));
val it =
[.] |- ∀C B A. B + C = A:
thm
most of time, variables appearing first will also come first in the results of
GEN_ALL, but in above example, the variable C appears before B maybe because of
specialities of “+”. Any way, this is not what I concerned most.
In my developing theory, I often need to convert an equation theorem in weaker
implication forms. For this purpose I have the following functions:
fun EQ_IMP_LR thm = (GEN_ALL o fst o EQ_IMP_RULE o SPEC_ALL) thm;
fun EQ_IMP_RL thm = (GEN_ALL o snd o EQ_IMP_RULE o SPEC_ALL) thm;
But they’re not perfect: the resulting theorems usually have different orders
for the qualified variables. And this may result into failures when actually
using these theorems in other proofs in which some tacticals apply to only the
first several qualified variables. As a result, I have to create the following
partial versions and then do the GEN_ALL by a series of GEN calls manually.
fun EQ_IMP_LR' thm = (fst (EQ_IMP_RULE (SPEC_ALL thm)));
fun EQ_IMP_RL' thm = (snd (EQ_IMP_RULE (SPEC_ALL thm)));
So instead of having
val TRANS_REC = save_thm ("TRANS_REC",
(EQ_IMP_LR TRANS_REC_EQ);
Now I have to write this instead: (and I must know and supply the name and type
of each qualified variable)
val TRANS_REC = save_thm ("TRANS_REC",
((GEN ``X :string``) o
(GEN ``E :CCS``) o
(GEN ``u :Action``) o
(GEN ``E' :CCS``))
(EQ_IMP_LR' TRANS_REC_EQ));
What I want to know is, does anyone know (or have ever implemented) a general
tools function, which can apply an arbitrary function of type (thm -> thm)
between SPEC_ALL and things like a GEN_ALL, but the resulting theorems doesn’t
change the orders of all qualified variables? (just first level would be enough
for me)
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
