# HG changeset patch
# User nipkow
# Date 1738096924 -3600
# Node ID afae60d6ff1588b7752861e89a211a2e61fa4ff0
# Parent  dfde9a8296f525476846136e27eb572da3898fbc
extracted the ^^ subtheory for modularity reasons

diff -r dfde9a8296f5 -r afae60d6ff15 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Jan 28 17:30:00 2025 +0100
+++ b/src/HOL/List.thy	Tue Jan 28 21:42:04 2025 +0100
@@ -263,15 +263,6 @@
 replicate_0: "replicate 0 x = []" |
 replicate_Suc: "replicate (Suc n) x = x # replicate n x"
 
-overloading pow_list == "compow :: nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
-begin
-
-primrec pow_list :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"pow_list 0 xs = []" |
-"pow_list (Suc n) xs = xs @ pow_list n xs"
-
-end
-
 text \<open>
   Function \<open>size\<close> is overloaded for all datatypes. Users may
   refer to the list version as \<open>length\<close>.\<close>
@@ -4846,134 +4837,6 @@
 by (subst foldr_fold [symmetric]) simp_all
 
 
-subsubsection \<open>\<^term>\<open>xs ^^ n\<close>\<close>
-
-context
-begin
-
-interpretation monoid_mult "[]" "append"
-  rewrites "power u n = u ^^ n"
-proof-
-  show "class.monoid_mult [] (@)"
-    by (unfold_locales, simp_all)
-  show "power.power [] (@) u n = u ^^ n"
-    by(induction n) (auto simp add: power.power.simps)
-qed
-
-\<comment> \<open>inherited power properties\<close>
-
-lemmas pow_list_zero = power.power_0 and
-  pow_list_one = power_Suc0_right and
-  pow_list_1 = power_one_right and
-  pow_list_Nil = power_one and
-  pow_list_2 = power2_eq_square and
-  pow_list_Suc = power_Suc and
-  pow_list_Suc2 = power_Suc2 and
-  pow_list_comm = power_commutes and
-  pow_list_add = power_add and
-  pow_list_eq_if = power_eq_if and
-  pow_list_mult = power_mult and
-  pow_list_commuting_commutes = power_commuting_commutes
-
-end
-
-lemma pow_list_alt: "xs^^n = concat (replicate n xs)"
-by (induct n) auto
-
-lemma pow_list_single: "[a] ^^ m = replicate m a"
-by(simp add: pow_list_alt)
-
-lemma length_pow_list_single [simp]: "length([a] ^^ n) = n"
-by (simp add: pow_list_single)
-
-lemma nth_pow_list_single: "i < m \<Longrightarrow> ([a] ^^ m) ! i = a"
-by (simp add: pow_list_single)
-
-lemma pow_list_not_NilD: "xs ^^ m \<noteq> [] \<Longrightarrow> 0 < m"
-by (cases m) auto
-
-lemma length_pow_list:  "length(xs ^^ k) = k * length xs"
-by (induction k) simp+
-
-lemma pow_list_set: "set (w ^^ Suc k) = set w"
-by (induction k)(simp_all)
-
-lemma pow_list_slide: "xs @ (ys @ xs) ^^ n  @ ys = (xs @ ys)^^(Suc n)"
-by (induction n) simp+
-
-lemma hd_pow_list: "0 < n \<Longrightarrow> hd(xs ^^ n) = hd xs"
-by(auto simp: pow_list_alt hd_append gr0_conv_Suc)
-
-lemma rev_pow_list: "rev (xs ^^ m) = (rev xs) ^^ m"
-by (induction m)(auto simp: pow_list_comm)
-
-lemma eq_pow_list_iff_eq_exp[simp]: assumes "xs \<noteq> []" shows "xs ^^ k = xs ^^ m \<longleftrightarrow> k = m"
-proof
-  assume "k = m" thus "xs ^^ k = xs ^^ m" by simp
-next
-  assume "xs ^^ k = xs ^^ m"
-  thus "k = m" using \<open>xs \<noteq> []\<close>[folded length_0_conv]
-    by (metis length_pow_list mult_cancel2)
-qed
-
-lemma pow_list_Nil_iff_0: "xs \<noteq> [] \<Longrightarrow> xs ^^ m = [] \<longleftrightarrow> m = 0"
-by (simp add: pow_list_eq_if)
-
-lemma pow_list_Nil_iff_Nil: "0 < m \<Longrightarrow> xs ^^ m = [] \<longleftrightarrow>  xs = []"
-by (cases xs) (auto simp add: pow_list_Nil pow_list_Nil_iff_0)
-
-lemma pow_eq_eq:
-  assumes "xs ^^ k = ys ^^ k" and "0 < k"
-  shows "(xs::'a list) = ys"
-proof-
-  have "length xs = length ys"
-    using assms(1) length_pow_list by (metis nat_mult_eq_cancel1[OF \<open>0 < k\<close>])
-  thus ?thesis by (metis Suc_pred append_eq_append_conv assms(1,2) pow_list.simps(2))
-qed
-
-lemma map_pow_list[simp]: "map f (xs ^^ k) = (map f xs) ^^ k"
-by (induction k) simp_all
-
-lemma concat_pow_list: "concat (xs ^^ k) = (concat xs) ^^ k"
-by (induction k) simp_all
-
-lemma concat_pow_list_single[simp]: "concat ([a] ^^ k) = a ^^ k"
-by (simp add: pow_list_alt)
-
-lemma pow_list_single_Nil_iff: "[a] ^^ n = [] \<longleftrightarrow> n = 0"
-by (simp add: pow_list_single)
-
-lemma hd_pow_list_single: "k \<noteq> 0 \<Longrightarrow> hd ([a] ^^ k) = a"
-by (cases k) simp+
-
-lemma index_pow_mod: "i < length(xs ^^ k) \<Longrightarrow> (xs ^^ k)!i = xs!(i mod length xs)"
-proof(induction k)
-  have aux:  "length(xs ^^ Suc l) = length(xs ^^ l) + length xs" for l
-    by simp
-  have aux1: "length (xs ^^ l) \<le> i \<Longrightarrow> i < length(xs ^^ l) + length xs \<Longrightarrow>  i mod length xs = i -  length(xs^^l)" for l
-    unfolding length_pow_list[of l xs]
-     using less_diff_conv2[of "l * length xs" i "length xs", unfolded add.commute[of "length xs"  "l * length xs"]]
-       le_add_diff_inverse[of "l*length xs" i]
-    by (simp add: mod_nat_eqI)
-  case (Suc k)
-  show ?case
-    unfolding aux sym[OF pow_list_Suc2[symmetric]] nth_append le_mod_geq
-    using aux1[ OF _ Suc.prems[unfolded aux]]
-      Suc.IH pow_list_Suc2[symmetric] Suc.prems[unfolded aux] leI[of i "length(xs ^^ k)"] by presburger
-qed auto
-
-lemma unique_letter_word: assumes "\<And>c. c \<in> set w \<Longrightarrow> c = a" shows "w = [a] ^^ length w"
-  using assms proof (induction w)
-  case (Cons b w)
-  have "[a] ^^ length w = w" using Cons.IH[OF Cons.prems[OF list.set_intros(2)]]..
-  then show "b # w = [a] ^^ length(b # w)"
-    unfolding Cons.prems[OF list.set_intros(1)] by auto
-qed simp
-
-lemma count_list_pow_list: "count_list (w ^^ k) a = k * (count_list w a)"
-by (induction k) simp+
-
-
 subsubsection \<open>\<^const>\<open>enumerate\<close>\<close>
 
 lemma enumerate_simps [simp, code]:
@@ -6833,21 +6696,6 @@
 lemma replicate_in_lists: "a \<in> A \<Longrightarrow> replicate k a \<in> lists A"
 by (induction k) auto
 
-lemma sing_pow_lists: "a \<in> A \<Longrightarrow> [a] ^^ n \<in> lists A"
-by (induction n) auto
-
-lemma one_generated_list_power: "u \<in> lists {x} \<Longrightarrow> \<exists>k. concat u = x ^^ k"
-proof(induction u rule: lists.induct)
-  case Nil
-  then show ?case by (metis concat.simps(1) pow_list.simps(1))
-next
-  case Cons
-  then show ?case by (metis concat.simps(2) pow_list_Suc singletonD)
-qed
-
-lemma pow_list_in_lists: "0 < k \<Longrightarrow> u ^^ k \<in> lists B \<Longrightarrow> u \<in> lists B"
-by (metis Suc_pred in_lists_conv_set pow_list_set)
-
 
 subsubsection \<open>Inductive definition for membership\<close>