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



Andrew,

On Saturday 01 October 2005 03:35, Andrew Pimlott wrote:
> lemma samekeys:
> "haskey (ps @ (k,v) # qs) k' = haskey (ps @ (k,v') # qs) k'";

> lemma "haskey (ps @ (k, v) # qs) k' --> haskey (ps @ (k, v') # qs) k'";
> -- ???

maybe someone else is going to write more about the simplifier, but the 
following proof should solve your goal:

  apply (subst samekeys)
  apply auto
done

Best regards,
Tjark





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