# HG changeset patch
# User nipkow
# Date 1587568937 -7200
# Node ID 3ab4b989f8c8621f2302cd148a60ca9aa2e073ff
# Parent  ad91684444d717a457b5c06c9679d742d98ddc07
new funs successive and distinct_adj

diff -r ad91684444d7 -r 3ab4b989f8c8 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Apr 22 11:50:23 2020 +0200
+++ b/src/HOL/List.thy	Wed Apr 22 17:22:17 2020 +0200
@@ -215,6 +215,14 @@
 "distinct [] \<longleftrightarrow> True" |
 "distinct (x # xs) \<longleftrightarrow> x \<notin> set xs \<and> distinct xs"
 
+fun successively :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
+"successively P []  = True" |
+"successively P [x] = True" |
+"successively P (x # y # xs) = (P x y \<and> successively P (y#xs))"
+
+definition distinct_adj where
+"distinct_adj = successively (\<noteq>)"
+
 primrec remdups :: "'a list \<Rightarrow> 'a list" where
 "remdups [] = []" |
 "remdups (x # xs) = (if x \<in> set xs then remdups xs else x # remdups xs)"
@@ -300,6 +308,7 @@
 @{lemma "fold f [a,b,c] x = f c (f b (f a x))" by simp}\\
 @{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by simp}\\
 @{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\
+@{lemma "successively (\<noteq>) [True,False,True,False]" by simp}\\
 @{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\
 @{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\
 @{lemma "enumerate 3 [a,b,c] = [(3,a),(4,b),(5,c)]" by normalization}\\
@@ -347,7 +356,7 @@
 that should give an intuitive understanding of the above functions.
 \<close>
 
-text\<open>The following simple sort functions are intended for proofs,
+text\<open>The following simple sort(ed) functions are intended for proofs,
 not for efficient implementations.\<close>
 
 text \<open>A sorted predicate w.r.t. a relation:\<close>
@@ -3452,6 +3461,83 @@
 by(simp add: upto_aux_def)
 
 
+
+subsubsection \<open>\<^const>\<open>successively\<close>\<close>
+
+lemma successively_Cons:
+  "successively P (x # xs) \<longleftrightarrow> xs = [] \<or> P x (hd xs) \<and> successively P xs"
+by (cases xs) auto
+
+lemma successively_cong [cong]:
+  assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> P x y \<longleftrightarrow> Q x y" "xs = ys"
+  shows   "successively P xs \<longleftrightarrow> successively Q ys"
+  unfolding assms(2) [symmetric] using assms(1)
+  by (induction xs) (auto simp: successively_Cons)
+
+
+lemma successively_append_iff:
+  "successively P (xs @ ys) \<longleftrightarrow>
+     successively P xs \<and> successively P ys \<and> 
+     (xs = [] \<or> ys = [] \<or> P (last xs) (hd ys))"
+by (induction xs) (auto simp: successively_Cons)
+
+lemma successively_if_sorted_wrt: "sorted_wrt P xs \<Longrightarrow> successively P xs"
+by (induction xs rule: induct_list012) auto
+
+
+lemma successively_iff_sorted_wrt_strong:
+  assumes "\<And>x y z. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> z \<in> set xs \<Longrightarrow>
+                     P x y \<Longrightarrow> P y z \<Longrightarrow> P x z"
+  shows   "successively P xs \<longleftrightarrow> sorted_wrt P xs"
+proof
+  assume "successively P xs"
+  from this and assms show "sorted_wrt P xs"
+  proof (induction xs rule: induct_list012)
+    case (3 x y xs)
+    from "3.prems" have "P x y"
+      by auto
+    have IH: "sorted_wrt P (y # xs)"
+      using "3.prems"
+      by(intro "3.IH"(2) list.set_intros(2))(simp, blast intro: list.set_intros(2))
+    have "P x z" if asm: "z \<in> set xs" for z
+    proof -
+      from IH and asm have "P y z"
+        by auto
+      with \<open>P x y\<close> show "P x z"
+        using "3.prems" asm by auto
+    qed
+    with IH and \<open>P x y\<close> show ?case by auto
+  qed auto
+qed (use successively_if_sorted_wrt in blast)
+
+lemma successively_conv_sorted_wrt:
+  assumes "transp P"
+  shows   "successively P xs \<longleftrightarrow> sorted_wrt P xs"
+  using assms unfolding transp_def
+  by (intro successively_iff_sorted_wrt_strong) blast
+
+lemma successively_rev [simp]: "successively P (rev xs) \<longleftrightarrow> successively (\<lambda>x y. P y x) xs"
+  by (induction xs rule: remdups_adj.induct)
+     (auto simp: successively_append_iff successively_Cons)
+
+lemma successively_map: "successively P (map f xs) \<longleftrightarrow> successively (\<lambda>x y. P (f x) (f y)) xs"
+  by (induction xs rule: induct_list012) auto
+
+lemma successively_mono:
+  assumes "successively P xs"
+  assumes "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> P x y \<Longrightarrow> Q x y"
+  shows   "successively Q xs"
+  using assms by (induction Q xs rule: successively.induct) auto
+
+lemma successively_altdef:
+  "successively = (\<lambda>P. rec_list True (\<lambda>x xs b. case xs of [] \<Rightarrow> True | y # _ \<Rightarrow> P x y \<and> b))"
+proof (intro ext)
+  fix P and xs :: "'a list"
+  show "successively P xs = rec_list True (\<lambda>x xs b. case xs of [] \<Rightarrow> True | y # _ \<Rightarrow> P x y \<and> b) xs"
+    by (induction xs) (auto simp: successively_Cons split: list.splits)
+qed
+
+
 subsubsection \<open>\<^const>\<open>distinct\<close> and \<^const>\<open>remdups\<close> and \<^const>\<open>remdups_adj\<close>\<close>
 
 lemma distinct_tl: "distinct xs \<Longrightarrow> distinct (tl xs)"
@@ -3976,6 +4062,65 @@
   ultimately show ?thesis by simp
 qed
 
+lemma successively_remdups_adjI:
+  "successively P xs \<Longrightarrow> successively P (remdups_adj xs)"
+by (induction xs rule: remdups_adj.induct) (auto simp: successively_Cons)
+
+lemma successively_remdups_adj_iff:
+  "(\<And>x. x \<in> set xs \<Longrightarrow> P x x) \<Longrightarrow>
+  successively P (remdups_adj xs) \<longleftrightarrow> successively P xs"
+by (induction xs rule: remdups_adj.induct)(auto simp: successively_Cons)
+
+
+subsection \<open>@{const distinct_adj}\<close>
+
+lemma distinct_adj_Nil [simp]: "distinct_adj []"
+  and distinct_adj_singleton [simp]: "distinct_adj [x]"
+  and distinct_adj_Cons_Cons [simp]: "distinct_adj (x # y # xs) \<longleftrightarrow> x \<noteq> y \<and> distinct_adj (y # xs)"
+by (auto simp: distinct_adj_def)
+
+lemma distinct_adj_Cons: "distinct_adj (x # xs) \<longleftrightarrow> xs = [] \<or> x \<noteq> hd xs \<and> distinct_adj xs"
+by (cases xs) auto
+
+lemma distinct_adj_ConsD: "distinct_adj (x # xs) \<Longrightarrow> distinct_adj xs"
+by (cases xs) auto
+
+lemma distinct_adj_remdups_adj[simp]: "distinct_adj (remdups_adj xs)"
+by (induction xs rule: remdups_adj.induct) (auto simp: distinct_adj_Cons)
+
+lemma distinct_adj_altdef: "distinct_adj xs \<longleftrightarrow> remdups_adj xs = xs"
+proof
+  assume "remdups_adj xs = xs"
+  with distinct_adj_remdups_adj[of xs] show "distinct_adj xs"
+    by simp
+next
+  assume "distinct_adj xs"
+  thus "remdups_adj xs = xs"
+    by (induction xs rule: induct_list012) auto
+qed
+
+lemma distinct_adj_rev [simp]: "distinct_adj (rev xs) \<longleftrightarrow> distinct_adj xs"
+by (simp add: distinct_adj_def eq_commute)
+
+lemma distinct_adj_append_iff:
+  "distinct_adj (xs @ ys) \<longleftrightarrow>
+     distinct_adj xs \<and> distinct_adj ys \<and> (xs = [] \<or> ys = [] \<or> last xs \<noteq> hd ys)"
+by (auto simp: distinct_adj_def successively_append_iff)
+
+lemma distinct_adj_appendD1 [dest]: "distinct_adj (xs @ ys) \<Longrightarrow> distinct_adj xs"
+  and distinct_adj_appendD2 [dest]: "distinct_adj (xs @ ys) \<Longrightarrow> distinct_adj ys"
+  by (auto simp: distinct_adj_append_iff)
+
+lemma distinct_adj_mapI: "distinct_adj xs \<Longrightarrow> inj_on f (set xs) \<Longrightarrow> distinct_adj (map f xs)"
+  unfolding distinct_adj_def successively_map
+  by (erule successively_mono) (auto simp: inj_on_def)
+
+lemma distinct_adj_mapD: "distinct_adj (map f xs) \<Longrightarrow> distinct_adj xs"
+unfolding distinct_adj_def successively_map by (erule successively_mono) auto
+
+lemma distinct_adj_map_iff: "inj_on f (set xs) \<Longrightarrow> distinct_adj (map f xs) \<longleftrightarrow> distinct_adj xs"
+using distinct_adj_mapD distinct_adj_mapI by blast
+
 
 subsubsection \<open>\<^const>\<open>insert\<close>\<close>
 
@@ -7606,11 +7751,36 @@
   shows "(A ===> list_all2 A ===> list_all2 A) removeAll removeAll"
   unfolding removeAll_def by transfer_prover
 
+lemma successively_transfer [transfer_rule]:
+  "((A ===> A ===> (=)) ===> list_all2 A ===> (=)) successively successively"
+  unfolding successively_altdef by transfer_prover
+
 lemma distinct_transfer [transfer_rule]:
   assumes [transfer_rule]: "bi_unique A"
   shows "(list_all2 A ===> (=)) distinct distinct"
   unfolding distinct_def by transfer_prover
 
+lemma distinct_adj_transfer [transfer_rule]:
+  assumes "bi_unique A"
+  shows "(list_all2 A ===> (=)) distinct_adj distinct_adj"
+  unfolding rel_fun_def
+proof (intro allI impI)
+  fix xs ys assume "list_all2 A xs ys"
+  thus "distinct_adj xs \<longleftrightarrow> distinct_adj ys"
+  proof (induction rule: list_all2_induct)
+    case (Cons x xs y ys)
+    note * = this
+    show ?case
+    proof (cases xs)
+      case [simp]: (Cons x' xs')
+      with * obtain y' ys' where [simp]: "ys = y' # ys'"
+        by (cases ys) auto
+      from * show ?thesis
+        using assms by (auto simp: distinct_adj_Cons bi_unique_def)
+    qed (use * in auto)
+  qed auto
+qed
+
 lemma remdups_transfer [transfer_rule]:
   assumes [transfer_rule]: "bi_unique A"
   shows "(list_all2 A ===> list_all2 A) remdups remdups"