# Re: [isabelle] can't hack induction

Feel free to ask questions about it, it's only there to show you more internal steps of what's going on. The simple proof in my email is more than adequate for the task and is, in fact, identical to Christian's.
```
```
Christian's explanation is better than mine, I think. Less rambling, straight to the point. It's a shame we don't get to see each other's posts until the next round of moderation ;)
```

Sincerely,

Rafal Kolanski.

Andrei Borac wrote:
```
```Wow, thanks everyone, lots of good info. So far I am impressed with
proofgeneral/isabelle/hol (have just finished doing the commutativity
of add). Especially Rafal Kolanski's detailed proof I will have to go
over carefully. Might take a while ;-)

-Andrei

On Tue, Apr 13, 2010 at 2:04 AM, Christian Sternagel
<christian.sternagel at uibk.ac.at> wrote:
```
```Hi there,

example works with

datatype n = Z | S n

primrec add :: "n => n => n" where
"add x Z = x" |

by (induct y arbitrary: x) simp_all

The "trick" is generalization over x (otherwise the IH does only hold for
the specific x in the lemma and not for all x's). You could do the same
thing by stating your lemma as:

lemma desired: "ALL x. add x (S y) = S (add x y)"

And then doing an induction prove over y.

cheers

chris

On 04/13/2010 03:20 AM, Andrei Borac wrote:
```
```I am looking for someone who will answer these kinds of beginner
questions for pay. I am thinking something like \$10 / question,
payment would be over paypal or similar. This does not constitute an
offer to pay \$10 for an answer to this particular question. If you are
figure out some basic terms.

Ok, so I'm trying to get started. So far I've only been doing things
that can be proven by auto. Now I'm trying induction and things aren't
working. I'm trying to prove that "successor" can be "factored" out of

datatype n =
Z
| S n

primrec add :: "n =>  n =>  n"
where

lemma desired: "!!y. !!x. ((add x (S y)) = (S (add x y)))"

I can write out the steps of the induction I'm trying to do:

!!x. add x sz = add sx z = s (add x z) # this is the base case y=Z

So the general idea is to do a "forward step" (where an s is shifted
left), an "inductive step" and a "backward step" (where an s is
shifted right). The base case and the inductive step can be proven
with auto:

lemma bascase: "(!!x. (add x (S Z)) = (S (add x Z)))"
apply(auto)
done

lemma indstep [simp]: "(!!x. (add x (S y)) = (S (add x y))) ==>  (!!x.
apply(auto)
done

However, if I try to apply induct_tac on the desired lemma:

lemma desired: "!!y. !!x. ((add x (S y)) = (S (add x y)))"
apply(induct_tac y)
apply(auto)

I get:

proof (prove): step 2

goal (1 subgoal):
1. !!x n. add (S x) n = S (add x n) ==>  add (S (S x)) n = S (S (add x
n))

This is not what I want. My induction is based on !!y (!!x p(x,y)) ->
(!!x p'(x,y)) but what it is asking me to prove is !!y !!x (p(x,y) ->
p'(x,y)). How do I get back on track?

-Andrei

```
```
```
```

```

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