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,
>
> 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[]))
>
> I'm getting following matching error...
>
> Exception raised at Tactic.MATCH_MP_TAC:
> No match
> Exception-
> HOL_ERR
> {message = "No match", origin_function = "MATCH_MP_TAC",
> origin_structure = "Tactic"} raised
>
> It works otherwise for handling them individually...
> --
> 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 mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
