# HG changeset patch
# User blanchet
# Date 1314875907 -7200
# Node ID 3d046864ebe645abd6f3dc5f889cc92d7c312bd6
# Parent  2ac4ff398bc39ccc2e2b58f28d958f01d17ce2c7
added two lemmas about "distinct" to help Sledgehammer

diff -r 2ac4ff398bc3 -r 3d046864ebe6 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Sep 01 13:18:27 2011 +0200
+++ b/src/HOL/List.thy	Thu Sep 01 13:18:27 2011 +0200
@@ -2929,6 +2929,14 @@
     by (induct xs' ys' rule: list_induct2) (auto elim: in_set_zipE)
 qed
 
+(* The next two lemmas help Sledgehammer. *)
+
+lemma distinct_singleton: "distinct [x]" by simp
+
+lemma distinct_length_2_or_more:
+"distinct (a # b # xs) \<longleftrightarrow> (a \<noteq> b \<and> distinct (a # xs) \<and> distinct (b # xs))"
+by (metis distinct.simps(2) hd.simps hd_in_set list.simps(2) set_ConsD set_rev_mp set_subset_Cons)
+
 
 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}