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
SG2
------------------------------------
A1 ==> B1
(A1 ==> B1) ==> B1
3 subgoals
: proof
On Thu, Sep 20, 2018 at 6:21 PM Konrad Slind <[email protected]> wrote:
> 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 <
> [email protected]> 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
>> [email protected]
>> 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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
