Re: [isabelle] newbie question

lemma rev_revH: "revH xs ys = rev xs @ ys"
 by (induct xs arbitrary: ys, auto)

when I try this I get
  *** Error in method "HOL.induct":
  *** method "induct": bad arguments
  ***   : ys
  *** At command "by".
using the FreeBSD packages isabelle-2005 and proofgeneral-xemacs-3.6.
(I also tried without the colon and got a different error).

If you insist on induct_tac:

lemma rev_revH: "ALL ys. revH xs ys = rev xs @ ys"
 apply (induct_tac xs)
 apply simp_all

It's not so much that I insist as I was unaware that there is a separate "induct" :) This worked fine for me and was what I was going for with my "strengthened proof" I mentioned earlier. I thought (incorrectly) that "!! ys ." would do what "ALL ys ." does. Its still not clear to me
what the difference is, and I guess I need to read up on this some more.


Tim Newsham wrote:
[possible duplicate, I jumped the gun on sending the first before I was properly subscribed].

I'm trying to prove a simple proof related to the "reverse" proof
in the tutorial (I have the rest of the tutorial theory here
as well including lemmas app_Nil2, app_assoc, rev_app and rev_rev):

--- snip ---
         revH :: "'a list => 'a list => 'a list"

  "revH [] ys = ys"
  "revH (x # xs) ys = revH xs (x # ys)"

  lemma rev_revH: "revH xs ys = rev xs @ ys"
  apply(induct_tac xs)

  lemma rev_rev2: "rev xs = revH xs []"
  apply(induct_tac xs)
--- snip ---

when I evaluate the first lemma it is able to automatically reduce the problem to the goal:

   forall a list.
       revH list ys = rev list @ ys ==>
       revH list (a # ys) = rev list @ a # ys

To me this seems to imply that this is solved, but I guess Isabelle doesn't see it that way. I tried to strengthen the proof by saying
"!! ys ." but that didn't seem to have any effect.  What do I need to
do here to complete this proof?

Tim Newsham

Tim Newsham

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