Email Gateway (Aug 18 2022 at 10:45): Email Gateway (Aug 18 2022 at 10:45):From: Lucas Cavalcante <thesupervisar@gmail.com>
Hello all,
Consider the usual datatype for lists and the list's append function. Given
the fallowing funcion to reverse a list, I was trying to prove the lemma
"rev_suf" (down):
datatype 'a list = Vazio ("[]")
| Lista 'a "'a list" (infixr "#" 65)
consts suf :: "'a list => 'a list => 'a list" (infixr "@" 65)
primrec
"[] @ ys = ys"
"(x # xs) @ ys = x # (xs @ ys)"
consts rev :: "'a list => 'a list"
primrec
"rev [] = []"
"rev (x # xs) = (rev xs) @ (x # [])"
lemma suf_vazio: "xs = xs @ []"
apply(induct_tac xs)
apply simp
apply simp
done
lemma suf_assoc: "(xs @ ys) @ zs = xs @ (ys @ zs)"
apply(induct_tac xs)
apply simp
apply simp
done
lemma rev_suf: "rev(xs @ ys) = (rev ys) @ (rev xs)"
apply(induct_tac xs)
apply simp
apply (rule suf_vazio)
apply simp
apply (rule suf_assoc)
done
It goes ok, but just becouse lemma "suc_vazio" is: "xs = xs @ []". How to
proceed (manually, thus not using "auto" command) if the lemma "suc_vazio"
was written this way: "xs @ [] = xs"?
The problem is I can't use "rule suf_vazio" in lemma "rev_suf". The subgoal
is "rev ys = rev ys @ []".
Regards,
Lucas Cavalcante
Email Gateway (Aug 18 2022 at 10:45):From: Peter Lammich <peter.lammich@uni-muenster.de>
Lucas Cavalcante wrote:
You could write (rule suc_vazio[symmetric]). The symmetric-attribute
will swap the sides of the equality
Last updated: Nov 21 2024 at 12:39 UTC