Re: [isabelle] proof solution [ newbie question ]



Your goal is not provable. You need the assumptions that both xs and ys are non-empty --- see your own proof. If you have those, you can convert from xs ~= [] to EX a as. xs = a#as (similarly for ys) by simplifying with neq_Nil_conv. The rest is done by auto.

Tobias

Gregory Kulczycki schrieb:
I've been experimenting with the Isabelle prover and have reached a point in
a proof where I have the following subgoal:

/\ xs ys zs. [| hd xs = hd ys; tl xs @ zs = tl ys |] ==> xs @ zs = ys

This looks obvious to me (since xs @ zs = ys is equivalent to hd xs # tl xs
@ zs = hd ys # tl ys for non-empty xs) , but I don't know how to proceed.

Any suggestions?

Thanks,
Greg





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.