[isabelle] 2 sides of an equality



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




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