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), together in the same step.
To package this as a list-tactic, you could do
val tac23 = EVERY [tac2, tac3, ...]
then val lt23 = ALLGOALS tac23
or val lt23 = TACS_TO_LT [tac23]
then what you ask would be achieved by
SPLIT_LT 2 (ALLGOALS tac1, lt23)
Cheers,
Jeremy
On 10/13/2018 03:38 AM, Waqar Ahmad via hol-info wrote:
Hi,
Suppose, I have 3 subgoals where first 2 subgoals can be proved by apply
tac1 and the third goal may takes some set of tacts, say tac2, tac3...
Is it possible that I can use SPLIT_LT in a way such that first two
subgoals are discharged by applying tac1 and I only end up proving the
third subgoal?
On Fri, Sep 21, 2018 at 3:00 AM <michael.norr...@data61.csiro.au
<mailto:michael.norr...@data61.csiro.au>> wrote:
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
<mailto:hol-info@lists.sourceforge.net>>
*Reply-To: *Waqar Ahmad <12phdwah...@seecs.edu.pk
<mailto:12phdwah...@seecs.edu.pk>>
*Date: *Friday, 21 September 2018 at 08:39
*To: *"konrad.sl...@gmail.com <mailto:konrad.sl...@gmail.com>"
<konrad.sl...@gmail.com <mailto:konrad.sl...@gmail.com>>
*Cc: *hol-info <hol-info@lists.sourceforge.net
<mailto: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 <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
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
