match_mp_tac is indeed causing an error because it is not applicable in the
other subgoals.
Michael
From: Waqar Ahmad via hol-info <hol-info@lists.sourceforge.net>
Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Friday, 21 September 2018 at 08:39
To: "konrad.sl...@gmail.com" <konrad.sl...@gmail.com>
Cc: hol-info <hol-info@lists.sourceforge.net>
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 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
<konrad.sl...@gmail.com<mailto:konrad.sl...@gmail.com>> 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
<hol-info@lists.sourceforge.net<mailto: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<mailto: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
