# Re: [isabelle] newbie question

In general it is much better to use the "induct" method insead of the induct_tac. In your case you need to generalize over ys, since in the recursive call ys is modified by revH.
```
The following works for me:

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

If you insist on induct_tac:

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

Amine.

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"

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

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

lemma rev_rev2: "rev xs = revH xs []"
apply(induct_tac xs)
apply(auto)
done
--- 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
http://www.thenewsh.com/~newsham/
```
```

```

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