Re: [isabelle] Help



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.