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

On Sun, Oct 02, 2005 at 04:12:41PM +0200, nipkow at wrote:
> >    lemma samekeys:
> >      "haskey (ps @ (k,v) # qs) k' = haskey (ps @ (k,v') # qs) k'";
> >
> > However, I could not get samekeys to be used to simplify it.
> The simplifier cannot guess what v' is supposed to be. Hence it cannot be
> used as a rewrite rule. Only the more restrictive version
> "(haskey (ps @ (k,v) # qs) k' = haskey (ps @ (k,v') # qs) k') = True";
> is used, which doesn't help here.
>     lemma
>       "haskey (ps @ (k, v) # qs) k' --> haskey (ps @ (k, v') # qs) k'";
> This one can be used by the simplifier: although it is equally unclear what v
> is supposed to be when the simplifier starts proving the precondition of the
> rule, this is a special case: if the precondition is directly present as an
> assumption, v is found by matching with that assumption.

Thank you to everyone who replied.  Continuing along the train that led
to my posting, I proved the lemma with implication above, which I called
samekeys2.  (I can either prove it from the lemma with equality by
applying subst, as others suggested, or prove it directly by induction.)
I then tried to prove a lemma about a related function, uniquekeys
(again, full code is below):

    lemma samekeys3[simp]:
      "uniquekeys (ps @ (k,v) # qs) --> uniquekeys (ps @ (k,v') # qs)";
    apply (induct_tac ps);
    apply (auto);

At this point, I had:

 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.


theory Assoc = Main:

consts haskey :: "('key * 'val)list => 'key => bool"
       uniquekeys :: "('key * 'val)list => bool";

"haskey [] k = False"
"haskey (p#ps) k = (let (k',v') = p in k=k' | haskey ps k)";

"uniquekeys [] = True"
"uniquekeys (p#ps) = (let (k,v) = p in ~(haskey ps k) & uniquekeys ps)";

declare Let_def[simp];

lemma samekeys: "haskey (ps @ (k,v) # qs) k' = haskey (ps @ (k,v') # qs) k'";
apply (induct_tac ps);
apply (auto);

lemma samekeys2:
  "haskey (ps @ (k, v) # qs) k' --> haskey (ps @ (k, v') # qs) k'";
apply (subst samekeys);
apply (auto);

lemma samekeys3[simp]:
  "uniquekeys (ps @ (k,v) # qs) --> uniquekeys (ps @ (k,v') # qs)";
apply (induct_tac ps);
apply (auto);
apply (simp add: samekeys2);  -- goes into a loop, but finally works!

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