Re: [isabelle] can't hack induction

Well, I have solved this particular problem. Still looking for someone
to answer questions (starting with "what is the difference between
induct and induct_tac" ...).


datatype n =
| S n

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

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

On Mon, Apr 12, 2010 at 6:20 PM, Andrei Borac <zerosum42 at> 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
> 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.