I have two assumptions both in implicative forms with universal
quantification. I would like to obtain an MP in the spirit of the following
theorem:
val GEN_IMP_TRANS = store_thm("GEN_IMP_TRANS",
``!P Q R S. (!x. P x ==> Q (R x)) ==> (!x. Q x ==> S x) ==> (!x. P x
==> S (R x))``,
metis_tac []);
However if I use drule with the theorem the antecedent of the resolution is
put into a conjunction (the last forall is moved left and the antecedent
becomes (!x. Q x ==> S x) /\ P x') and can not be used to resolve against
the second assumption. Any suggestions?
Thanks,
Haitao
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
