Re: [isabelle] can't hack induction



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
interested in answering questions for pay, please contact me and we'll
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
add:

datatype n =
  Z
| S n

primrec add :: "n => n => n"
where
  "(add x Z) = x"
| "(add x (S y)) = (add (S x) y)"

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
!!x. add x ssz = add sx sz = s (add sx z) = s (add x sz)
!!x. add x sssz = add sx ssz = s (add sx sz) = s (add x ssz)

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.
(add x (S (S y))) = (S (S (add x y))))"
apply(auto)
done
I think this is not the right inductive step, but that you want
(add x (S (S y))) = (S (add x (S y)))

In any event, given this problem, you should have not declared your inductive step as [simp]. Then, after doing the induct_tac step, you would see what the required lemmas are.
Regards,

Jeremy







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