*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Help*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Tue, 08 Jul 2014 12:33:08 +0200*In-reply-to*: <CAHxd0bATfDpoHDTJEc5BM+BgOfPFDdRJ4KzSscN-2NeYd1TtmA@mail.gmail.com>*References*: <CAHxd0bATfDpoHDTJEc5BM+BgOfPFDdRJ4KzSscN-2NeYd1TtmA@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.6.0

Hallo, The problem is not associativity of plus, that gets applied automatically. The problem is that your induction does not work this way, because the second parameter of sum_list_compute is fixed to x; however, in the induction step, you change it to x + y. You therefore need to generalise over x using the “arbitrary” keyword: lemma sum_list_compute_relation: "sum_list_compute Ls x = sum_list' (x # Ls)" by (induct Ls arbitrary: x) simp_all Note that I also flipped the equation because it helps simp_all to figure out how to apply the induction hypothesis automatically, otherwise you would have had to instantiate it by hand. Also, your auxiliary lemmas don't really help, and if you do prove auxiliary lemmas, you should not put the HOL universal quantifier ∀ in front of it. Just state it as lemma help1: "(x + n ) + sum_list' L = sum_list' ((x + n)# L)" The free variables get generalised automatically by convention, and putting an explicit HOL universal quantifier in front of the lemma makes it more difficult to apply it. Cheers, Manuel On 08/07/14 00:37, Adamu Sani YAHAYA wrote: > Hello. > please can anyone help me to solve my problem. I want to apply plus > associativity but is not working. please what can I do. > the code is here: > theory Sumlist > imports Datatype Nat > begin > > datatype 'a list = Nil ("[]") > | cons 'a "'a list" (infixr "#" 65) > > primrec sum_list' :: "nat list => nat" where > "sum_list' [] = 0" > | "sum_list' (x#xs) = x + sum_list' xs " > > primrec sum_list_compute :: "nat list => nat => nat" where > "sum_list_compute [] y = y" > | "sum_list_compute (x#xs) y = sum_list_compute xs (y + x)" > > primrec sum_list :: "nat list => nat" where > "sum_list [] = 0" > | "sum_list (x#xs) = sum_list_compute xs x " > > > lemma help1:"\<forall> x n L. (x + n ) + sum_list' L = sum_list' ((x + n)# > L) " > apply simp > done > lemma help2 :" \<forall> x a L . x + (a + sum_list' L) = (x + a) + > sum_list' L " > apply simp > done > theorem sum_list_compute_relation:" sum_list'( x # Ls)= sum_list_compute Ls > x" > apply(induct_tac Ls) > apply(auto) > apply(rule help2) > done > Adamu sani yahaya > thanks

**References**:**[isabelle] Help***From:*Adamu Sani YAHAYA

- Previous by Date: Re: [isabelle] Isabelle2014-RC0: phantom theories
- Next by Date: [isabelle] some Isabelle/jEdit shortcuts
- Previous by Thread: [isabelle] Help
- Next by Thread: Re: [isabelle] Help
- Cl-isabelle-users July 2014 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