*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 01:27:03 -0700*In-reply-to*: <n2gce53b1121004121820r7930d8a0r11e7607f9c4734bd@mail.gmail.com>*References*: <n2gce53b1121004121820r7930d8a0r11e7607f9c4734bd@mail.gmail.com>

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" ...). -Andrei 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: "!!x. ((add x (S y)) = (S (add x y)))" apply(induct y) apply(auto) done On Mon, Apr 12, 2010 at 6:20 PM, Andrei Borac <zerosum42 at gmail.com> 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

- Previous by Date: [isabelle] can't hack induction
- Next by Date: Re: [isabelle] can't hack induction
- Previous by Thread: [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