# HG changeset patch
# User nipkow
# Date 1665751192 -7200
# Node ID eb30869e72289fe05186d9f7067f9727d010a9fc
# Parent  f3e30ad850ba57810b74c5ada66bd501177da854# Parent  77e13a694cbedee6b53bdcf77418ab3f856aee47
merged

diff -r f3e30ad850ba -r eb30869e7228 CONTRIBUTORS
--- a/CONTRIBUTORS	Fri Oct 14 10:30:37 2022 +0100
+++ b/CONTRIBUTORS	Fri Oct 14 14:39:52 2022 +0200
@@ -6,6 +6,9 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* October 2022: Jeremy Sylvestre
+  Lemmas for Fun and List.
+
 
 Contributions to Isabelle2022
 -----------------------------
diff -r f3e30ad850ba -r eb30869e7228 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Oct 14 10:30:37 2022 +0100
+++ b/src/HOL/List.thy	Fri Oct 14 14:39:52 2022 +0200
@@ -4557,6 +4557,10 @@
 lemma in_set_replicate[simp]: "(x \<in> set (replicate n y)) = (x = y \<and> n \<noteq> 0)"
 by (simp add: set_replicate_conv_if)
 
+lemma card_set_1_iff_replicate:
+  "card(set xs) = Suc 0 \<longleftrightarrow> xs \<noteq> [] \<and> (\<exists>x. xs = replicate (length xs) x)"
+by (metis card_1_singleton_iff empty_iff insert_iff replicate_eqI set_empty2 set_replicate)      
+
 lemma Ball_set_replicate[simp]:
   "(\<forall>x \<in> set(replicate n a). P x) = (P a \<or> n=0)"
 by(simp add: set_replicate_conv_if)
@@ -4812,6 +4816,9 @@
 lemma set_rotate[simp]: "set(rotate n xs) = set xs"
   by (induct n) (simp_all add:rotate_def)
 
+lemma rotate1_replicate[simp]: "rotate1 (replicate n a) = replicate n a"
+by (cases n) (simp_all add: replicate_append_same)
+
 lemma rotate1_is_Nil_conv[simp]: "(rotate1 xs = []) = (xs = [])"
   by (cases xs) auto
 
@@ -4849,6 +4856,32 @@
   \<open>rotate1 xs ! n = xs ! (Suc n mod length xs)\<close> if \<open>n < length xs\<close>
   using that nth_rotate [of n xs 1] by simp
 
+lemma inj_rotate1: "inj rotate1"
+proof
+  fix xs ys :: "'a list" show "rotate1 xs = rotate1 ys \<Longrightarrow> xs = ys"
+    by (cases xs; cases ys; simp)
+qed
+
+lemma surj_rotate1: "surj rotate1"
+proof (safe, simp_all)
+  fix xs :: "'a list" show "xs \<in> range rotate1"
+  proof (cases xs rule: rev_exhaust)
+    case Nil
+    hence "xs = rotate1 []" by auto
+    thus ?thesis by fast
+  next
+    case (snoc as a)
+    hence "xs = rotate1 (a#as)" by force
+    thus ?thesis by fast
+  qed
+qed
+
+lemma bij_rotate1: "bij (rotate1 :: 'a list \<Rightarrow> 'a list)"
+using bijI inj_rotate1 surj_rotate1 by blast
+
+lemma rotate1_fixpoint_card: "rotate1 xs = xs \<Longrightarrow> xs = [] \<or> card(set xs) = 1"
+by(induction xs) (auto simp: card_insert_if[OF finite_set] append_eq_Cons_conv)
+
 
 subsubsection \<open>\<^const>\<open>nths\<close> --- a generalization of \<^const>\<open>nth\<close> to sets\<close>