Re: [isabelle] 2 sides of an equality



Lucas Cavalcante wrote:
> 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 @ []".
>
>   
You could write (rule suc_vazio[symmetric]). The symmetric-attribute
will swap the sides of the equality






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