remdups_adj lemma

gistfile1.thy

lemma remdups_adj_distinction:
  assumes "length xs > 0"
  shows "⋀i. i + 1 < length (remdups_adj xs) ⟹ (remdups_adj xs) ! i ≠ (remdups_adj xs) ! (i + 1)"
using assms proof (induction xs)
  case Nil
  hence "False" by simp
  thus "remdups_adj [] ! i ≠ remdups_adj [] ! (i + 1)"..
next
  case (Cons x xs)
  hence "xs ≠ []" by (metis Divides.div_less Suc_eq_plus1 Zero_not_Suc div_eq_dividend_iff list.size(3,4) plus_nat.add_0 remdups_adj.simps(2))
  then obtain y xs' where xs:"xs = y # xs'" by (metis list.exhaust)
  from `xs ≠ []` have lenxs:"length xs > 0" by simp
  from xs have rem:"remdups_adj (x # xs) = (if x = y then remdups_adj (y # xs') else x # remdups_adj (y # xs'))" using remdups_adj.simps(3) by auto
  show "remdups_adj (x # xs) ! i ≠ remdups_adj (x # xs) ! (i + 1)"
  proof (cases "x = y")
    case True 
    with rem xs have "remdups_adj (x # xs) = remdups_adj xs" by auto
    moreover from lenxs have "remdups_adj xs ! i ≠ remdups_adj xs ! (i + 1)" by (metis Cons.IH Cons.prems(1) calculation)
    ultimately show ?thesis by auto
  next
    case False
    with rem xs have rem2:"remdups_adj (x # xs) = x # remdups_adj xs" by auto
    show ?thesis
    proof (cases i)
      case 0
      with rem2 have isx:"remdups_adj (x # xs) ! i = x" by auto
      from 0 rem2 have "remdups_adj (x # xs) ! (i + 1) = remdups_adj xs ! 0"
        by (metis One_nat_def Suc_eq_plus1 diff_Suc_less less_Suc0 nth_Cons_pos)
      also have "… = remdups_adj (y # xs') ! 0" using xs by auto
      also have "… = (y # remdups_adj (y # xs')) ! 0" by (metis nth_Cons' remdups_adj_Cons_alt)
      also have "… = y" by simp
      finally have "remdups_adj (x # xs) ! (i + 1) = y".
      with False isx show "remdups_adj (x # xs) ! i ≠ remdups_adj (x # xs) ! (i + 1)" by auto
    next
      case (Suc j)
      with rem2 have "remdups_adj (x # xs) ! i = (remdups_adj xs) ! j" by auto
      from Cons(2) `i = Suc j` have "j + 1 < length (remdups_adj (x # xs)) - 1" by auto
      also have "… ≤ length (remdups_adj xs) + 1 - 1" by (metis One_nat_def le_refl list.size(4) rem2)
      also have "… = length (remdups_adj xs)" by simp
      finally have "j + 1 < length (remdups_adj xs)".
      with Cons.IH lenxs have "(remdups_adj xs) ! j ≠ (remdups_adj xs) ! (j + 1)" by auto
      with rem2 `i = Suc j` show "remdups_adj (x # xs) ! i ≠ remdups_adj (x # xs) ! (i + 1)" by (metis Suc_eq_plus1 nth_Cons_Suc)
    qed
  qed
qed