*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Beginner question: Symmetry of equality in proofs?*From*: Jason Dagit <dagitj at gmail.com>*Date*: Sun, 12 Dec 2010 20:58:51 -0800

Hello, 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: \begin{code} theory RevLength imports Datatype begin datatype 'a list = Nil ("[]") | Cons 'a "'a list" (infixr "#" 65) primrec app :: "'a list => 'a list => 'a list" (infixr "++" 65) where "[] ++ 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) apply(auto) done lemma "length xs = length (rev xs)" apply(induct_tac xs) apply(simp, simp) apply(rule length_suc) done lemma "length (rev xs) = length xs" apply(induct_tac xs) apply(simp, simp) oops (* apply(simp add: length_suc) done *) \end{code} 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. Thanks, Jason

**Follow-Ups**:**Re: [isabelle] Beginner question: Symmetry of equality in proofs?***From:*Lars Noschinski

**Re: [isabelle] Beginner question: Symmetry of equality in proofs?***From:*Brian Huffman

- Previous by Date: Re: [isabelle] How to avoid x \<in> carrier G proofs
- Next by Date: Re: [isabelle] Beginner question: Symmetry of equality in proofs?
- Previous by Thread: Re: [isabelle] AFP modification policy (was: How to avoid x \<in> carrier G proofs)
- Next by Thread: Re: [isabelle] Beginner question: Symmetry of equality in proofs?
- Cl-isabelle-users December 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list