src/HOL/List.thy
changeset 25130 d91391a8705b
parent 25112 98824cc791c0
child 25134 3d4953e88449
equal deleted inserted replaced
25129:de54445dc82c 25130:d91391a8705b
  2150 apply (metis Zero_neq_Suc gr0_conv_Suc in_set_conv_nth lessI less_trans_Suc nth_Cons' nth_Cons_Suc)
  2150 apply (metis Zero_neq_Suc gr0_conv_Suc in_set_conv_nth lessI less_trans_Suc nth_Cons' nth_Cons_Suc)
  2151 *)
  2151 *)
  2152  apply (clarsimp simp add: set_conv_nth)
  2152  apply (clarsimp simp add: set_conv_nth)
  2153  apply (erule_tac x = 0 in allE, simp)
  2153  apply (erule_tac x = 0 in allE, simp)
  2154  apply (erule_tac x = "Suc i" in allE, simp, clarsimp)
  2154  apply (erule_tac x = "Suc i" in allE, simp, clarsimp)
       
  2155 (*TOO SLOW
  2155 apply (metis Suc_Suc_eq lessI less_trans_Suc nth_Cons_Suc)
  2156 apply (metis Suc_Suc_eq lessI less_trans_Suc nth_Cons_Suc)
       
  2157 *)
       
  2158 apply (erule_tac x = "Suc i" in allE, simp)
       
  2159 apply (erule_tac x = "Suc j" in allE, simp)
  2156 done
  2160 done
  2157 
  2161 
  2158 lemma nth_eq_iff_index_eq:
  2162 lemma nth_eq_iff_index_eq:
  2159  "\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
  2163  "\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
  2160 by(auto simp: distinct_conv_nth)
  2164 by(auto simp: distinct_conv_nth)