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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and