author nipkow Wed, 22 Apr 2020 17:22:17 +0200 changeset 71779 3ab4b989f8c8 parent 71778 ad91684444d7 child 71787 acfe72ff00c2
 src/HOL/List.thy file | annotate | diff | comparison | revisions
```--- 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))"
+
+
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 @@

+
+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

+  "successively P xs \<Longrightarrow> successively P (remdups_adj xs)"
+by (induction xs rule: remdups_adj.induct) (auto simp: successively_Cons)
+
+  "(\<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)
+
+
+
+  and distinct_adj_Cons_Cons [simp]: "distinct_adj (x # y # xs) \<longleftrightarrow> x \<noteq> y \<and> distinct_adj (y # xs)"
+
+lemma distinct_adj_Cons: "distinct_adj (x # xs) \<longleftrightarrow> xs = [] \<or> x \<noteq> hd xs \<and> distinct_adj xs"
+by (cases xs) auto
+
+by (cases xs) auto
+
+
+proof
+  assume "remdups_adj xs = xs"
+    by simp
+next
+  thus "remdups_adj xs = xs"
+    by (induction xs rule: induct_list012) auto
+qed
+
+
+  "distinct_adj (xs @ ys) \<longleftrightarrow>
+     distinct_adj xs \<and> distinct_adj ys \<and> (xs = [] \<or> ys = [] \<or> last xs \<noteq> hd ys)"
+
+
+  by (erule successively_mono) (auto simp: inj_on_def)
+
+unfolding distinct_adj_def successively_map by (erule successively_mono) auto
+
+

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

+  assumes "bi_unique A"
+  unfolding rel_fun_def
+proof (intro allI impI)
+  fix xs ys assume "list_all2 A xs 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"```