Thanks for the suggestion! I can use satTheory.AND_IMP to renormalize the
intermediate resolution back to an implicative form, which should work.
The reason that this issue came up is that asm_simp_tac seems to be
sensitive to the ordering of antecedents/assumptions. I was trying to do a
step deduction in a more controlled way to help it along. In this
particular case using fs [] also solves my problem.
Thanks,
Haitao
On Tue, Mar 19, 2019 at 11:10 AM Waqar Ahmad <12phdwah...@seecs.edu.pk>
wrote:
> 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 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
