# HG changeset patch
# User noschinl
# Date 1415713586 -3600
# Node ID 5f179549c362cb7811eb023fc43b3755775a5379
# Parent  d09bbd2642e294806e7e3595679b3687618c09e1
added lemma

diff -r d09bbd2642e2 -r 5f179549c362 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Nov 11 12:30:37 2014 +0100
+++ b/src/HOL/List.thy	Tue Nov 11 14:46:26 2014 +0100
@@ -3361,6 +3361,175 @@
   "distinct (a # b # xs) \<longleftrightarrow> (a \<noteq> b \<and> distinct (a # xs) \<and> distinct (b # xs))"
 by force
 
+lemma remdups_adj_altdef: "(remdups_adj xs = ys) \<longleftrightarrow>
+  (\<exists>f::nat => nat. mono f & f ` {0 ..< size xs} = {0 ..< size ys}
+    \<and> (\<forall>i < size xs. xs!i = ys!(f i))
+    \<and> (\<forall>i. i + 1 < size xs \<longrightarrow> (xs!i = xs!(i+1) <-> f i = f(i+1))))" (is "?L \<longleftrightarrow> (\<exists>f. ?p f xs ys)")
+proof
+  assume ?L
+  then show "\<exists>f. ?p f xs ys"
+  proof (induct xs arbitrary: ys rule: remdups_adj.induct)
+    case (1 ys)
+    thus ?case by (intro exI[of _ id]) (auto simp: mono_def)
+  next
+    case (2 x ys)
+    thus ?case by (intro exI[of _ id]) (auto simp: mono_def)
+  next
+    case (3 x1 x2 xs ys)
+    let ?xs = "x1 # x2 # xs"
+    let ?cond = "x1 = x2"
+    def zs \<equiv> "remdups_adj (x2 # xs)"
+    from 3(1-2)[of zs]
+    obtain f where p: "?p f (x2 # xs) zs" unfolding zs_def by (cases ?cond) auto
+    then have f0: "f 0 = 0"
+      by (intro mono_image_least[where f=f]) blast+
+    from p have mono: "mono f" and f_xs_zs: "f ` {0..<length (x2 # xs)} = {0..<length zs}" by auto
+    have ys: "ys = (if x1 = x2 then zs else x1 # zs)"
+      unfolding 3(3)[symmetric] zs_def by auto
+    have zs0: "zs ! 0 = x2" unfolding zs_def by (induct xs) auto
+    have zsne: "zs \<noteq> []" unfolding zs_def by (induct xs) auto
+    let ?Succ = "if ?cond then id else Suc"
+    let ?x1 = "if ?cond then id else Cons x1"
+    let ?f = "\<lambda> i. if i = 0 then 0 else ?Succ (f (i - 1))"
+    have ys: "ys = ?x1 zs" unfolding ys by (cases ?cond, auto)
+    have mono: "mono ?f" using `mono f` unfolding mono_def by auto
+    show ?case unfolding ys
+    proof (intro exI[of _ ?f] conjI allI impI)
+      show "mono ?f" by fact
+    next
+      fix i assume i: "i < length ?xs"
+      with p show "?xs ! i = ?x1 zs ! (?f i)" using zs0 by auto
+    next
+      fix i assume i: "i + 1 < length ?xs"
+      with p show "(?xs ! i = ?xs ! (i + 1)) = (?f i = ?f (i + 1))"
+        by (cases i) (auto simp: f0)
+    next
+      have id: "{0 ..< length (?x1 zs)} = insert 0 (?Succ ` {0 ..< length zs})"
+        using zsne by (cases ?cond, auto)
+      { fix i  assume "i < Suc (length xs)"
+        hence "Suc i \<in> {0..<Suc (Suc (length xs))} \<inter> Collect (op < 0)" by auto
+        from imageI[OF this, of "\<lambda>i. ?Succ (f (i - Suc 0))"]
+        have "?Succ (f i) \<in> (\<lambda>i. ?Succ (f (i - Suc 0))) ` ({0..<Suc (Suc (length xs))} \<inter> Collect (op < 0))" by auto
+      }
+      then show "?f ` {0 ..< length ?xs} = {0 ..< length (?x1  zs)}"
+        unfolding id f_xs_zs[symmetric] by auto
+    qed
+  qed
+next
+  assume "\<exists> f. ?p f xs ys"
+  then show ?L
+  proof (induct xs arbitrary: ys rule: remdups_adj.induct)
+    case 1 then show ?case by auto
+  next
+    case (2 x) then obtain f where f_img: "f ` {0 ..< size [x]} = {0 ..< size ys}"
+        and f_nth: "\<And>i. i < size [x] \<Longrightarrow> [x]!i = ys!(f i)"
+      by blast
+
+    have "length ys = card (f ` {0 ..< size [x]})"
+      using f_img by auto
+    then have "length ys = 1" by auto
+    moreover
+    then have "f 0 = 0" using f_img by auto
+    ultimately show ?case using f_nth by (cases ys) auto
+  next
+    case (3 x1 x2 xs)
+    from "3.prems" obtain f where f_mono: "mono f"
+      and f_img: "f ` {0..<length (x1 # x2 # xs)} = {0..<length ys}"
+      and f_nth:
+        "\<And>i. i < length (x1 # x2 # xs) \<Longrightarrow> (x1 # x2 # xs) ! i = ys ! f i"
+        "\<And>i. i + 1 < length (x1 # x2 #xs) \<Longrightarrow>
+          ((x1 # x2 # xs) ! i = (x1 # x2 # xs) ! (i + 1)) = (f i = f (i + 1))"
+      by blast
+
+    show ?case
+    proof cases
+      assume "x1 = x2"
+
+      let ?f' = "f o Suc"
+
+      have "remdups_adj (x1 # xs) = ys"
+      proof (intro "3.hyps" exI conjI impI allI)
+        show "mono ?f'"
+          using f_mono by (simp add: mono_iff_le_Suc)
+      next
+        have "?f' ` {0 ..< length (x1 # xs)} = f ` {Suc 0 ..< length (x1 # x2 # xs)}"
+          by safe (fastforce, rename_tac x, case_tac x, auto)
+        also have "\<dots> = f ` {0 ..< length (x1 # x2 # xs)}"
+        proof -
+          have "f 0 = f (Suc 0)" using \<open>x1 = x2\<close> f_nth[of 0] by simp
+          then show ?thesis by safe (fastforce, rename_tac x, case_tac x, auto)
+        qed
+        also have "\<dots> = {0 ..< length ys}" by fact
+        finally show  "?f' ` {0 ..< length (x1 # xs)} = {0 ..< length ys}" .
+      qed (insert f_nth[of "Suc i" for i], auto simp: \<open>x1 = x2\<close>)
+      then show ?thesis using \<open>x1 = x2\<close> by simp
+    next
+      assume "x1 \<noteq> x2"
+
+      have "2 \<le> length ys"
+      proof -
+        have "2 = card {f 0, f 1}" using \<open>x1 \<noteq> x2\<close> f_nth[of 0] by auto
+        also have "\<dots> \<le> card (f ` {0..< length (x1 # x2 # xs)})"
+          by (rule card_mono) auto
+        finally show ?thesis using f_img by simp
+      qed
+
+      have "f 0 = 0" using f_mono f_img by (rule mono_image_least) simp
+
+      have "f (Suc 0) = Suc 0"
+      proof (rule ccontr)
+        assume "f (Suc 0) \<noteq> Suc 0"
+        then have "Suc 0 < f (Suc 0)" using f_nth[of 0] \<open>x1 \<noteq> x2\<close> \<open>f 0 = 0\<close> by auto
+        then have "\<And>i. Suc 0 < f (Suc i)"
+          using f_mono
+          by (meson Suc_le_mono le0 less_le_trans monoD)
+        then have "\<And>i. Suc 0 \<noteq> f i" using \<open>f 0 = 0\<close>
+          by (case_tac i) fastforce+
+        then have "Suc 0 \<notin> f ` {0 ..< length (x1 # x2 # xs)}" by auto
+        then show False using f_img \<open>2 \<le> length ys\<close> by auto
+      qed
+
+      obtain ys' where "ys = x1 # x2 # ys'"
+        using \<open>2 \<le> length ys\<close> f_nth[of 0] f_nth[of 1]
+        apply (cases ys)
+        apply (rename_tac [2] ys', case_tac [2] ys')
+        by (auto simp: \<open>f 0 = 0\<close> \<open>f (Suc 0) = Suc 0\<close>)
+
+      def f' \<equiv> "\<lambda>x. f (Suc x) - 1"
+
+      { fix i
+        have "Suc 0 \<le> f (Suc 0)" using f_nth[of 0] \<open>x1 \<noteq> x2\<close> \<open>f 0 = 0\<close>  by auto
+        also have "\<dots> \<le> f (Suc i)" using f_mono by (rule monoD) arith
+        finally have "Suc 0 \<le> f (Suc i)" .
+      } note Suc0_le_f_Suc = this
+
+      { fix i have "f (Suc i) = Suc (f' i)"
+          using Suc0_le_f_Suc[of i] by (auto simp: f'_def)
+      } note f_Suc = this
+
+      have "remdups_adj (x2 # xs) = (x2 # ys')"
+      proof (intro "3.hyps" exI conjI impI allI)
+        show "mono f'"
+          using Suc0_le_f_Suc f_mono by (auto simp: f'_def mono_iff_le_Suc le_diff_iff)
+      next
+        have "f' ` {0 ..< length (x2 # xs)} = (\<lambda>x. f x - 1) ` {0 ..< length (x1 # x2 #xs)}"
+          apply safe
+          apply (rename_tac [!] n,  case_tac [!] n)
+          apply (auto simp: f'_def \<open>f 0 = 0\<close> \<open>f (Suc 0) = Suc 0\<close> intro: rev_image_eqI)
+          done
+        also have "\<dots> = (\<lambda>x. x - 1) ` f ` {0 ..< length (x1 # x2 #xs)}"
+          by (auto simp: image_comp)
+        also have "\<dots> = (\<lambda>x. x - 1) ` {0 ..< length ys}"
+          by (simp only: f_img)
+        also have "\<dots> = {0 ..< length (x2 # ys')}"
+          using \<open>ys = _\<close> by (fastforce intro: rev_image_eqI)
+        finally show  "f' ` {0 ..< length (x2 # xs)} = {0 ..< length (x2 # ys')}" .
+      qed (insert f_nth[of "Suc i" for i] \<open>x1 \<noteq> x2\<close>, auto simp add: f_Suc \<open>ys = _\<close>)
+      then show ?case using \<open>ys = _\<close> \<open>x1 \<noteq> x2\<close> by simp
+    qed
+  qed
+qed
+
 lemma hd_remdups_adj[simp]: "hd (remdups_adj xs) = hd xs"
 by (induction xs rule: remdups_adj.induct) simp_all