Here's an old-school solution:
fun locate P left [] = NONE
| locate P left (h::t) =
if P h then
SOME (rev left, h, t)
else
locate P (h::left) t;
fun ASM_CONJ_TAC (asl,c) =
case locate is_conj [] asl
of NONE => raise ERR "ASM_CONJ_TAC" "no conj in assums"
| SOME(left,conj,right) =>
let val (t1,t2) = dest_conj conj
val th = SPECL [t1,t2,c] AND_IMP_INTRO
in ([(left @ [t2,t1] @ right, c)],
fn [thm] => UNDISCH(EQ_MP th (DISCH t1 (DISCH t2 thm))))
end
Test.
g `a ==> b /\ c ==> d /\ e ==> k`;
e (rpt disch_tac);
e (rpt ASM_CONJ_TAC);
On Fri, Jun 29, 2018 at 2:27 AM Heiko Becker <hbec...@mpi-sws.org> wrote:
> Hello,
>
> On 06/28/2018 11:44 PM, Dylan Melville wrote:
> > Also, the version Im using is HOL - Light
> >
> >> On Jun 28, 2018, at 5:38 PM, Dylan Melville <dylanmelvi...@gmail.com>
> wrote:
> >>
> >> Is there a tactic for splitting conjoined assumptions into separate
> assumptions?
>
> In HOL-Light you can try using CONJ_PAIR[1] for an assumption of the
> form A /\ B and CONJUNCTS[2] for finitely many conjuncts. These can then
> be added back using ASSUME_TAC.
>
> Alternatively you can use CONJUNCTS_THEN[3] in combination with ASSUME_TAC.
>
>
> Hope this helps.
>
> Best regards,
>
>
> Heiko
>
>
> [1]: http://www.cl.cam.ac.uk/~jrh13/hol-light/HTML/CONJ_PAIR.html
>
> [2]:
> http://www.cl.cam.ac.uk/~jrh13/hol-light/HTML/CONJUNCTS_UPPERCASE.html
>
> [3]:http://www.cl.cam.ac.uk/~jrh13/hol-light/HTML/CONJUNCTS_THEN.html
>
>
>
> ------------------------------------------------------------------------------
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
