[isabelle] 2 sides of an equality
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
datatype 'a list = Vazio ("")
| Lista 'a "'a list" (infixr "#" 65)
consts suf :: "'a list => 'a list => 'a list" (infixr "@" 65)
" @ ys = ys"
"(x # xs) @ ys = x # (xs @ ys)"
consts rev :: "'a list => 'a list"
"rev  = "
"rev (x # xs) = (rev xs) @ (x # )"
lemma suf_vazio: "xs = xs @ "
lemma suf_assoc: "(xs @ ys) @ zs = xs @ (ys @ zs)"
lemma rev_suf: "rev(xs @ ys) = (rev ys) @ (rev xs)"
apply (rule suf_vazio)
apply (rule suf_assoc)
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 @ ".
This archive was generated by a fusion of
Pipermail (Mailman edition) and