Hi Ramana, Thanks very much. I’ve been using the following function STRIP_FORALL_RULE provided by Machael Norrish in private (now in HOL’s examples/CCS/CCSLib.sml)
(* provided by Michael Norrish *)
fun STRIP_FORALL_RULE f th =
let
val (vs, _) = strip_forall (concl th)
in
GENL vs (f (SPEC_ALL th))
end;
which is almost the same as your solutions. (SPEC_ALL = SPECL in this case)
Regards,
Chun Tian
> Il giorno 17 mag 2017, alle ore 23:40, Ramana Kumar
> <ramana.ku...@cl.cam.ac.uk> ha scritto:
>
> 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
>
>
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
