*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] can't hack induction*From*: Andrei Borac <zerosum42 at gmail.com>*Date*: Tue, 13 Apr 2010 02:15:26 -0700*In-reply-to*: <4BC433B7.9000000@uibk.ac.at>*References*: <n2gce53b1121004121820r7930d8a0r11e7607f9c4734bd@mail.gmail.com> <4BC433B7.9000000@uibk.ac.at>

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, > > first of all, save your money :), answers on this list are for free. Your > example works with > > > 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: "add x (S y) = S (add x y)" > 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 >> 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 >> > >

**Follow-Ups**:**Re: [isabelle] can't hack induction***From:*Rafal Kolanski

**References**:**[isabelle] can't hack induction***From:*Andrei Borac

**Re: [isabelle] can't hack induction***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] can't hack induction
- Next by Date: [isabelle] question about locales and locale parameters
- Previous by Thread: Re: [isabelle] can't hack induction
- Next by Thread: Re: [isabelle] can't hack induction
- Cl-isabelle-users April 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list