Re: [isabelle] beginner question: why isn't my lemma applied?



On Tuesday 04 October 2005 02:49, Andrew Pimlott wrote:
>  1. !!a list.
>        [| ~ haskey (list @ (k, v) # qs) a; uniquekeys (list @ (k, v) # qs);
>           uniquekeys (list @ (k, v') # qs);
>           haskey (list @ (k, v') # qs) a |]
>        ==> False
>
> This is where I was stuck before, but thanks to your help, I tried
> applying samekeys2:
>
>     apply (simp add: samekeys2);
>
> I get warnings about exceeding the simplification depth, but eventually
> "No subgoals!".  Probably not ideal, but hopefully I'll be able to reach
> my destination in this manner, then come back when I'm wiser and find a
> better way.

If you want to avoid the warning, you can use

	apply (erule notE)
	apply (erule samekeys2[rule_format])

instead of apply (simp add: samekeys2) to prove your lemma.

Best regards,
Tjark





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