# HG changeset patch
# User kleing
# Date 1114682674 -7200
# Node ID 4320bce5873f86b706fbaed37cc56a36dd7dd07a
# Parent  3aca7f05cd122631f202fd0da087c33a0b0c6abc
more on rev

diff -r 3aca7f05cd12 -r 4320bce5873f src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Apr 28 12:02:49 2005 +0200
+++ b/src/HOL/List.thy	Thu Apr 28 12:04:34 2005 +0200
@@ -566,12 +566,21 @@
 lemma rev_rev_ident [simp]: "rev (rev xs) = xs"
 by (induct xs) auto
 
+lemma rev_swap: "(rev xs = ys) = (xs = rev ys)"
+by auto
+
 lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])"
 by (induct xs) auto
 
 lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])"
 by (induct xs) auto
 
+lemma rev_singleton_conv [simp]: "(rev xs = [x]) = (xs = [x])"
+by (cases xs) auto
+
+lemma singleton_rev_conv [simp]: "([x] = rev xs) = (xs = [x])"
+by (cases xs) auto
+
 lemma rev_is_rev_conv [iff]: "!!ys. (rev xs = rev ys) = (xs = ys)"
 apply (induct xs, force)
 apply (case_tac ys, simp, force)