src/HOL/List.thy
changeset 13124 6e1decd8a7a9
parent 13122 c63612ffb186
child 13142 1ebd8ed5a1a0
     1.1 --- a/src/HOL/List.thy	Wed May 08 12:21:42 2002 +0200
     1.2 +++ b/src/HOL/List.thy	Wed May 08 13:01:40 2002 +0200
     1.3 @@ -1163,6 +1163,33 @@
     1.4  lemma distinct_filter[simp]: "distinct xs ==> distinct (filter P xs)"
     1.5  by(induct xs, auto)
     1.6  
     1.7 +(* It is best to avoid this indexed version of distinct,
     1.8 +   but sometimes it is useful *)
     1.9 +lemma distinct_conv_nth:
    1.10 + "distinct xs = (\<forall>i j. i < size xs \<and> j < size xs \<and> i \<noteq> j \<longrightarrow> xs!i \<noteq> xs!j)"
    1.11 +apply(induct_tac xs)
    1.12 + apply simp
    1.13 +apply simp
    1.14 +apply(rule iffI)
    1.15 + apply(clarsimp)
    1.16 + apply(case_tac i)
    1.17 +  apply(case_tac j)
    1.18 +   apply simp
    1.19 +  apply(simp add:set_conv_nth)
    1.20 + apply(case_tac j)
    1.21 +  apply(clarsimp simp add:set_conv_nth)
    1.22 + apply simp
    1.23 +apply(rule conjI)
    1.24 + apply(clarsimp simp add:set_conv_nth)
    1.25 + apply(erule_tac x = 0 in allE)
    1.26 + apply(erule_tac x = "Suc i" in allE)
    1.27 + apply simp
    1.28 +apply clarsimp
    1.29 +apply(erule_tac x = "Suc i" in allE)
    1.30 +apply(erule_tac x = "Suc j" in allE)
    1.31 +apply simp
    1.32 +done
    1.33 +
    1.34  (** replicate **)
    1.35  section "replicate"
    1.36