*To*: Andrei Borac <zerosum42 at gmail.com>*Subject*: Re: [isabelle] can't hack induction*From*: Rafal Kolanski <rafalk at cse.unsw.edu.au>*Date*: Wed, 14 Apr 2010 17:56:11 +1000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <h2sce53b1121004130215uf76be3eewb706a43a4517fe98@mail.gmail.com>*References*: <n2gce53b1121004121820r7930d8a0r11e7607f9c4734bd@mail.gmail.com> <4BC433B7.9000000@uibk.ac.at> <h2sce53b1121004130215uf76be3eewb706a43a4517fe98@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.24 (X11/20100317)

Anyway, I'm glad you got your problem sorted. 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, 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

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

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

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

- Previous by Date: Re: [isabelle] can't hack induction
- Next by Date: [isabelle] FLoC 2010: Student Travel Grants
- 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