[isabelle] Beginner question: Symmetry of equality in proofs?


I'm still very new to isabelle and I've been following the standard tutorial
from the isabelle website.

I was practicing proofs using my own definitions of rev and length.

Here is my theory:

theory RevLength
imports Datatype


datatype 'a list = Nil ("[]")
                 | Cons 'a "'a list" (infixr "#" 65)

primrec app :: "'a list => 'a list => 'a list" (infixr "++" 65)
"[] ++ ys       = ys" |
"(x # xs) ++ ys = x # (xs ++ ys)"

primrec rev :: "'a list => 'a list" where
"rev []       = []" |
"rev (x # xs) = (rev xs) ++ (x # [])"

primrec length :: "'a list => nat" where
"length [] = 0" |
"length (x # xs) = 1 + length xs"

lemma length_suc: "Suc (length list) = length (list ++ a # [])"
apply(induct_tac list)

lemma "length xs = length (rev xs)"
apply(induct_tac xs)
apply(simp, simp)
apply(rule length_suc)

lemma "length (rev xs) = length xs"
apply(induct_tac xs)
apply(simp, simp)
(* apply(simp add: length_suc)
done *)

What I noticed was that between the last two lemmas, the direction of the
equality makes a huge difference when proving the lemma.  The lemma "length
xs = length (rev xs)" is easy to prove but lemma "length (rev xs) = length
xs" is much harder to prove (for me at least).

I thought that maybe it was because the induction variable was inside a
function call on the LHS, but one of the first examples of induction in the
tutorial is theorem rev_rev[simp]: "(rev (rev xs)) = xs", which is easily
proven by induction on xs followed by auto.

I would expect "=" to be symmetric.  Is that not the case?  Is there
something else going on here?

On a side note, I tried to define Cons as ":" instead of "#", but I kept
getting ambiguous parses.  Why is that?  ":" doesn't seem to be used in the
grammar that I've seen thus far in the tutorial, but it's also a hard thing
to search for.


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