# HG changeset patch
# User nipkow
# Date 1698424026 -7200
# Node ID 7482c023b37bdd7272b91e01ba1dc7356ee73b85
# Parent  35b2282fbc7737056d66146538dd623218981087
added lemma

diff -r 35b2282fbc77 -r 7482c023b37b src/HOL/Library/NList.thy
--- 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