# HG changeset patch
# User nipkow
# Date 1020855700 -7200
# Node ID 6e1decd8a7a96019fd07a90c2c6c39fa59a5b383
# Parent  777db68dee1e9f230930cb32a84b1a8135ed9845
new thm distinct_conv_nth

diff -r 777db68dee1e -r 6e1decd8a7a9 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed May 08 12:21:42 2002 +0200
+++ b/src/HOL/List.thy	Wed May 08 13:01:40 2002 +0200
@@ -1163,6 +1163,33 @@
 lemma distinct_filter[simp]: "distinct xs ==> distinct (filter P xs)"
 by(induct xs, auto)
 
+(* It is best to avoid this indexed version of distinct,
+   but sometimes it is useful *)
+lemma distinct_conv_nth:
+ "distinct xs = (\<forall>i j. i < size xs \<and> j < size xs \<and> i \<noteq> j \<longrightarrow> xs!i \<noteq> xs!j)"
+apply(induct_tac xs)
+ apply simp
+apply simp
+apply(rule iffI)
+ apply(clarsimp)
+ apply(case_tac i)
+  apply(case_tac j)
+   apply simp
+  apply(simp add:set_conv_nth)
+ apply(case_tac j)
+  apply(clarsimp simp add:set_conv_nth)
+ apply simp
+apply(rule conjI)
+ apply(clarsimp simp add:set_conv_nth)
+ apply(erule_tac x = 0 in allE)
+ apply(erule_tac x = "Suc i" in allE)
+ apply simp
+apply clarsimp
+apply(erule_tac x = "Suc i" in allE)
+apply(erule_tac x = "Suc j" in allE)
+apply simp
+done
+
 (** replicate **)
 section "replicate"