Hi Haitao,
You can introduce the conjunction among the antecedents as:
val GEN_IMP_TRANS_conj = (REWRITE_RULE [GSYM satTheory.AND_IMP]
GEN_IMP_TRANS);
val GEN_IMP_TRANS_conj =
⊢ ∀P Q R S. (∀x. P x ⇒ Q (R x)) ∧ (∀x. Q x ⇒ S x) ⇒ ∀x. P x ⇒ S (R x):
thm
On Tue, Mar 19, 2019 at 5:30 AM Haitao Zhang <zhtp...@gmail.com> wrote:
> 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
>
--
Waqar Ahmad, Ph.D.
Post Doc at Hardware Verification Group (HVG)
Department of Electrical and Computer Engineering
Concordia University, QC, Canada
Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
