1.1 --- a/src/HOL/List.thy	Thu Apr 28 12:02:49 2005 +0200
     1.2 +++ b/src/HOL/List.thy	Thu Apr 28 12:04:34 2005 +0200
     1.3 @@ -566,12 +566,21 @@
     1.4  lemma rev_rev_ident [simp]: "rev (rev xs) = xs"
     1.5  by (induct xs) auto
     1.6  
     1.7 +lemma rev_swap: "(rev xs = ys) = (xs = rev ys)"
     1.8 +by auto
     1.9 +
    1.10  lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])"
    1.11  by (induct xs) auto
    1.12  
    1.13  lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])"
    1.14  by (induct xs) auto
    1.15  
    1.16 +lemma rev_singleton_conv [simp]: "(rev xs = [x]) = (xs = [x])"
    1.17 +by (cases xs) auto
    1.18 +
    1.19 +lemma singleton_rev_conv [simp]: "([x] = rev xs) = (xs = [x])"
    1.20 +by (cases xs) auto
    1.21 +
    1.22  lemma rev_is_rev_conv [iff]: "!!ys. (rev xs = rev ys) = (xs = ys)"
    1.23  apply (induct xs, force)
    1.24  apply (case_tac ys, simp, force)