If you're working with a conversion (term -> thm), from which you produce
your thm -> thm function via CONV_RULE, then I suggest looking at
STRIP_QUANT_CONV.
To avoid having to specify the types of variables explicitly, I suggest
looking at Q.GEN and Q.SPEC (and Q.ISPEC). To deal with lists of variables
at once, I suggest Q.GENL and Q.SPECL.
The specific functionality you asked for could be implemented as follows:
fun strip_forall_rule f th =
let val (vs,_) = strip_forall(concl th)
val th' = f (SPECL vs th)
in GENL vs th' end
e.g.,
val f = fst o EQ_IMP_RULE
val th = ASSUME``∀x y. (f x y ⇔ g y x)``
val th' = strip_forall_rule f th
[.] |- ∀x y. f x y ⇒ g y x
On 7 May 2017 at 03:09, Chun Tian (binghe) <binghe.l...@gmail.com> wrote:
> 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
>
>
>
> ------------------------------------------------------------
> ------------------
> 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
