[isabelle] Help



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.