# HG changeset patch # User nipkow # Date 1660205481 -7200 # Node ID 40e16228405e1ff4cd7b76ce2720d8f814856354 # Parent 2a049b402e535c8048bc945675b59c054a84d882 new lemma diff -r 2a049b402e53 -r 40e16228405e NEWS --- a/NEWS Thu Aug 11 05:50:48 2022 +0200 +++ b/NEWS Thu Aug 11 10:11:21 2022 +0200 @@ -41,6 +41,8 @@ integers, sacrificing pattern patching in exchange for dramatically increased performance for comparisions. +* New theory HOL-Library.NList of fixed length lists + * Rule split_of_bool_asm is not split any longer, analogously to split_if_asm. INCOMPATIBILITY. diff -r 2a049b402e53 -r 40e16228405e src/HOL/Library/NList.thy --- a/src/HOL/Library/NList.thy Thu Aug 11 05:50:48 2022 +0200 +++ b/src/HOL/Library/NList.thy Thu Aug 11 10:11:21 2022 +0200 @@ -95,4 +95,7 @@ lemma nlists_replicateI [intro]: "x \ A \ replicate n x \ 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) + end