match_mp_tac is indeed causing an error because it is not applicable in the other subgoals.
Michael From: Waqar Ahmad via hol-info <[email protected]> Reply-To: Waqar Ahmad <[email protected]> Date: Friday, 21 September 2018 at 08:39 To: "[email protected]" <[email protected]> Cc: hol-info <[email protected]> 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 <[email protected]<mailto:[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]<mailto:[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]<mailto:[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
