Email Gateway (Aug 19 2022 at 15:14): Email Gateway (Aug 19 2022 at 15:14):From: Adamu Sani YAHAYA <adamusaniyahaya@gmail.com>
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
Email Gateway (Aug 19 2022 at 15:14):From: Manuel Eberl <eberlm@in.tum.de>
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
Email Gateway (Aug 19 2022 at 15:16):From: Makarius <makarius@sketis.net>
Side remark: you should always import at least theory "Main", not anything
below it like "Datatype" or "Nat" above.
Makarius
Last updated: Apr 20 2024 at 04:19 UTC