--- a/src/HOL/Library/NList.thy Fri Oct 27 08:16:16 2023 +0200
+++ b/src/HOL/Library/NList.thy Fri Oct 27 18:27:06 2023 +0200
@@ -35,6 +35,9 @@
with size show "xs \<in> nlists n B" by(clarsimp intro!: nlistsI)
qed
+lemma nlists_singleton: "nlists n {a} = {replicate n a}"
+unfolding nlists_def by(auto simp: replicate_length_same dest!: subset_singletonD)
+
lemma nlists_n_0 [simp]: "nlists 0 A = {[]}"
unfolding nlists_def by (auto)
@@ -50,7 +53,6 @@
lemma nlists_not_empty: "A\<noteq>{} \<Longrightarrow> \<exists>xs. xs \<in> nlists n A"
by (induct "n") (auto simp: in_nlists_Suc_iff)
-
lemma nlistsE_nth_in: "\<lbrakk> xs \<in> nlists n A; i < n \<rbrakk> \<Longrightarrow> xs!i \<in> A"
unfolding nlists_def by (auto)
@@ -101,7 +103,8 @@
lemma nlists_replicateI [intro]: "x \<in> A \<Longrightarrow> replicate n x \<in> nlists n A"
by (induct n) auto
-lemma nlists_set[code]: "nlists n (set xs) = set (List.n_lists n xs)"
-unfolding nlists_def by (rule sym, induct n) (auto simp: image_iff length_Suc_conv)
+text \<open>Link to an executable version on lists in List.\<close>
+lemma nlists_set[code]: "nlists n (set xs) = set(List.n_lists n xs)"
+by (metis nlists_def set_n_lists)
end