Hi Waqar,
Firstly (simplest),
SPLIT_LT 2 (ALLGOALS tac1, ALL_LT)
applies tac1 to the first two subgoals and does nothing to the
remainder. Then you can work on the remaining goal.
But you want to also apply EVERY [tac2, tac3, ...] to the third subgoal
(which is the only remaining one),
*Date: *Friday, 21 September 2018 at 08:39
> *To: *"konrad.sl...@gmail.com"
> *Cc: *hol-info
> *Subject: *Re: [Hol-info] assumption matching in SPLIT_LT
>
>
>
> Hi,
>
>
>
> Thanks for the reply. I think the match_mp_tac is causing the error since
> if
t: Re: [Hol-info] assumption matching in SPLIT_LT
Hi,
Thanks for the reply. I think the match_mp_tac is causing the error since if I
only pop the assumption the tactic works on first subgoal.
rw [] \\ (pop_assum (mp_tac)) THEN_LT SPLIT_LT 1 (ALL_LT, ALLGOALS (rw[]))
&g
Hi,
Thanks for the reply. I think the match_mp_tac is causing the error since
if I only pop the assumption the tactic works on first subgoal.
rw [] \\ (pop_assum (mp_tac)) THEN_LT SPLIT_LT 1 (ALL_LT, ALLGOALS (rw[]))
> val it =
SG3
A1 ==> B1
Seems like the rw[] is breaking the proof into 3 subgoals, and only on the
first one is the pop_assum match_mp_tac succeeding. So the proof is failing
before it gets to the THEN_LT.
Konrad.
On Thu, Sep 20, 2018 at 2:05 PM Waqar Ahmad via hol-info <
hol-info@lists.sourceforge.net> wrote:
> Hi,
Hi,
I'm trying to use the tactical SPLIT_LT to multiple subgoals. However, I'm
facing error with assumption matching. For instance, I've a proof goal of
this form:
`(A1 ==> B1) ==> (B1 /\ SG2 /\ SG3)`
rw []
\\ (pop_assum (fn th => match_mp_tac th)) THEN_LT SPLIT_LT 1 (ALL_LT,
ALLGOALS (rw[]))
