Re: [Hol-info] Best way to conduct a generalized IMP_TRANS
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
Re: [Hol-info] Best way to conduct a generalized IMP_TRANS
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
[Hol-info] Best way to conduct a generalized IMP_TRANS
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