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> 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>
> *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>
> 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> 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
>
>
>
>
> --
>
> 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
>
--
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
