diff --git a/thys/Fixed_Length_Vector/Fixed_Length_Vector.thy b/thys/Fixed_Length_Vector/Fixed_Length_Vector.thy
new file mode 100644
--- /dev/null
+++ b/thys/Fixed_Length_Vector/Fixed_Length_Vector.thy
@@ -0,0 +1,586 @@
+theory Fixed_Length_Vector
+  imports "HOL-Library.Numeral_Type" "HOL-Library.Code_Cardinality"
+begin
+
+text \<open>
+  This theory introduces a type constructor for lists with known length, also known as \<^emph>\<open>vectors\<close>.
+  Those vectors are indexed with a numeral type that represent their length.
+
+  This can be employed to avoid carrying around length constraints on lists. Instead, those
+  constraints are discharged by the type checker.
+
+  As compared to the vectors defined in the distribution, this definition can easily work with unit
+  vectors. We exploit the fact that the cardinality of an infinite type is defined to be \<open>0\<close>: thus
+  any infinite length index type represents a unit vector.
+
+  Furthermore, we set up automation and BNF support.
+\<close>
+
+lemma zip_map_same: \<open>zip (map f xs) (map g xs) = map (\<lambda>x. (f x, g x)) xs\<close>
+  by (induction xs) auto
+
+section \<open>Type class for indexing\<close>
+
+text \<open>
+  The \<open>index\<close> class is used to define an isomorphism between some index types with fixed cardinality
+  and a subset of the natural numbers. Crucially, infinite types can be made instance of this class
+  too, since Isabelle defines infinite cardinality to be equal to zero.
+
+  The \<open>index1\<close> class then adds more properties, such as injectivity, which can only be satisfied for
+  finite index types.
+
+  This class is roughly similar to the \<^class>\<open>enum\<close> class defined in the Isabelle library, which is
+  proved at a later point. However, \<^class>\<open>enum\<close> does not admit infinite types.
+\<close>
+
+class index =
+  fixes from_index :: \<open>'a \<Rightarrow> nat\<close>
+    and to_index :: \<open>nat \<Rightarrow> 'a\<close>
+  assumes to_from_index: \<open>n < CARD('a) \<Longrightarrow> from_index (to_index n) = n\<close>
+  assumes from_index_surj: \<open>n < CARD('a) \<Longrightarrow> \<exists>a. from_index a = n\<close>
+begin
+
+text \<open>A list of all possible indexes.\<close>
+
+definition indexes :: \<open>'a list\<close> where
+\<open>indexes = map to_index [0..<CARD('a)]\<close>
+
+text \<open>There are as many indexes as the cardinality of type \<^typ>\<open>'a\<close>.\<close>
+
+lemma indexes_length[simp]: \<open>length indexes = CARD('a)\<close>
+  unfolding indexes_def by auto
+
+lemma list_cong_index:
+  assumes \<open>length xs = CARD('a)\<close> \<open>length ys = CARD('a)\<close>
+  assumes \<open>\<And>i. xs ! from_index i = ys ! from_index i\<close>
+  shows \<open>xs = ys\<close>
+  apply (rule nth_equalityI)
+  using assms from_index_surj by auto
+
+lemma from_indexE:
+  assumes \<open>n < CARD('a)\<close>
+  obtains a where \<open>from_index a = n\<close>
+  using assms by (metis from_index_surj)
+
+end
+
+text \<open>Restrict \<^class>\<open>index\<close> to only admit finite types.\<close>
+
+class index1 = index +
+  assumes from_index_bound[simp]: \<open>from_index a < CARD('a)\<close>
+  assumes from_index_inj: \<open>inj from_index\<close>
+begin
+
+text \<open>Finiteness follows from the class assumptions.\<close>
+
+lemma card_nonzero[simp]: \<open>0 < CARD('a)\<close>
+  by (metis less_nat_zero_code from_index_bound neq0_conv)
+
+lemma finite_type[simp]: \<open>finite (UNIV :: 'a set)\<close>
+  by (metis card_nonzero  card.infinite less_irrefl)
+
+sublocale finite
+  by standard simp
+
+text \<open>\<^const>\<open>to_index\<close> and \<^const>\<open>from_index\<close> form a bijection.\<close>
+
+lemma from_to_index[simp]: \<open>to_index (from_index i) = i\<close>
+  by (meson injD from_index_bound from_index_inj to_from_index)
+
+lemma indexes_from_index[simp]: \<open>indexes ! from_index i = i\<close>
+  unfolding indexes_def by auto
+
+lemma to_index_inj_on: \<open>inj_on to_index {0..<CARD('a)}\<close>
+
+  apply rule
+  apply auto
+  apply (erule from_indexE)+
+  by (metis from_to_index)
+
+
+end
+
+text \<open>Finally, we instantiate the class for the pre-defined numeral types.\<close>
+
+instantiation num0 :: index
+begin
+
+definition from_index_num0 :: \<open>num0 \<Rightarrow> nat\<close> where \<open>from_index_num0 _ = undefined\<close>
+definition to_index_num0 :: \<open>nat \<Rightarrow> num0\<close> where \<open>to_index_num0 _ = undefined\<close>
+
+instance
+  by standard auto
+
+end
+
+
+lemma indexes_zero[simp]: \<open>indexes = ([] :: 0 list)\<close>
+  by (auto simp: indexes_def)
+
+instantiation num1 :: index1
+begin
+
+definition from_index_num1 :: \<open>num1 \<Rightarrow> nat\<close> where [simp]: \<open>from_index_num1 _ = 0\<close>
+definition to_index_num1 :: \<open>nat \<Rightarrow> num1\<close> where [simp]: \<open>to_index_num1 _ = 1\<close>
+
+instance
+  by standard (auto simp: inj_on_def)
+
+end
+
+
+lemma indexes_one[simp]: \<open>indexes = [1 :: 1]\<close>
+  by (auto simp: indexes_def)
+
+instantiation bit0 :: (finite) index1
+begin
+
+definition from_index_bit0 :: \<open>'a bit0 \<Rightarrow> nat\<close> where \<open>from_index_bit0 x = nat (Rep_bit0 x)\<close>
+
+definition to_index_bit0 :: \<open>nat \<Rightarrow> 'a bit0\<close> where \<open>to_index_bit0 \<equiv> of_nat\<close>
+
+instance
+  apply standard
+  subgoal
+    by (simp add: to_index_bit0_def from_index_bit0_def bit0.of_nat_eq Abs_bit0_inverse)
+  subgoal for n
+    unfolding from_index_bit0_def apply auto
+    apply (rule exI[where x = \<open>Abs_bit0 (int n)\<close>])
+    apply (subst Abs_bit0_inverse)
+    by auto
+  subgoal
+    apply (simp add: from_index_bit0_def)
+    by (metis Rep_bit0 atLeastLessThan_iff bit0.Rep_less_n card_bit0 nat_less_iff)
+  subgoal
+    unfolding from_index_bit0_def inj_on_def
+    by (metis Rep_bit0 Rep_bit0_inverse atLeastLessThan_iff int_nat_eq)
+  done
+
+end
+
+instantiation bit1 :: (finite) index1
+begin
+
+definition from_index_bit1 :: \<open>'a bit1 \<Rightarrow> nat\<close> where \<open>from_index_bit1 x = nat (Rep_bit1 x)\<close>
+
+definition to_index_bit1 :: \<open>nat \<Rightarrow> 'a bit1\<close> where \<open>to_index_bit1 \<equiv> of_nat\<close>
+
+instance
+  apply standard
+  subgoal
+    by (simp add: to_index_bit1_def from_index_bit1_def bit1.of_nat_eq Abs_bit1_inverse)
+  subgoal for n
+    unfolding from_index_bit1_def apply auto
+    apply (rule exI[where x = \<open>Abs_bit1 (int n)\<close>])
+    apply (subst Abs_bit1_inverse)
+    by auto
+  subgoal
+    apply (simp add: from_index_bit1_def)
+    by (metis Rep_bit1 atLeastLessThan_iff bit1.Rep_less_n card_bit1 nat_less_iff)
+  subgoal
+    unfolding from_index_bit1_def inj_on_def
+    by (metis Rep_bit1 Rep_bit1_inverse atLeastLessThan_iff eq_nat_nat_iff)
+  done
+
+end
+
+lemma indexes_bit_simps:
+  \<open>(indexes :: 'a :: finite bit0 list) = map of_nat [0..<2 * CARD('a)]\<close>
+  \<open>(indexes :: 'b :: finite bit1 list) = map of_nat [0..<2 * CARD('b) + 1]\<close>
+  unfolding indexes_def to_index_bit0_def to_index_bit1_def
+  by simp+
+
+text \<open>The following class and instance definitions connect \<^const>\<open>indexes\<close> to \<^const>\<open>enum_class.enum\<close>.\<close>
+
+class index_enum = index1 + enum +
+  assumes indexes_eq_enum: \<open>indexes = enum_class.enum\<close>
+
+instance num1 :: index_enum
+  by standard (auto simp: indexes_def enum_num1_def)
+
+instance bit0 :: (finite) index_enum
+  apply standard
+  apply (auto simp: indexes_def to_index_bit0_def enum_bit0_def)
+  by (metis Abs_bit0'_def bit0.of_nat_eq)
+
+
+instance bit1 :: (finite) index_enum
+  apply standard
+  apply (auto simp: indexes_def to_index_bit1_def enum_bit1_def)
+  apply (metis Abs_bit1'_def bit1.of_nat_eq)
+  by (metis Abs_bit1'_def bit1.of_nat_eq of_nat_mult of_nat_numeral)
+
+section \<open>Type definition and BNF setup\<close>
+
+text \<open>
+  A vector is a list with a fixed length, where the length is given by the cardinality of the second
+  type parameter. To obtain the unit vector, we can choose an infinite type. There is no reason to
+  restrict the index type to a particular sort constraint at this point, even though later on,
+  \<^class>\<open>index\<close> is frequently used.
+\<close>
+
+typedef ('a, 'b) vec = "{xs. length xs = CARD('b)} :: 'a list set"
+  morphisms list_of_vec vec_of_list
+  by (rule exI[where x = \<open>replicate CARD('b) undefined\<close>]) simp
+
+declare vec.list_of_vec_inverse[simp]
+
+type_notation vec (infixl "^" 15)
+
+setup_lifting type_definition_vec
+
+lift_definition map_vec :: \<open>('a \<Rightarrow> 'b) \<Rightarrow> 'a ^ 'c \<Rightarrow> 'b ^ 'c\<close> is map by auto
+
+lift_definition set_vec :: \<open>'a ^ 'b \<Rightarrow> 'a set\<close> is set .
+
+lift_definition rel_vec :: \<open>('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a ^ 'c \<Rightarrow> 'b ^ 'c \<Rightarrow> bool\<close> is list_all2 .
+
+lift_definition pred_vec :: \<open>('a \<Rightarrow> bool) \<Rightarrow> 'a ^ 'b \<Rightarrow> bool\<close> is list_all .
+
+lift_definition zip_vec :: \<open>'a ^ 'c \<Rightarrow> 'b ^ 'c \<Rightarrow> ('a \<times> 'b) ^ 'c\<close> is zip by auto
+
+lift_definition replicate_vec :: \<open>'a \<Rightarrow> 'a ^ 'b\<close> is \<open>replicate CARD('b)\<close> by auto
+
+bnf \<open>('a, 'b) vec\<close>
+  map: map_vec
+  sets: set_vec
+  bd: natLeq
+  wits: replicate_vec
+  rel: rel_vec
+  pred: pred_vec
+  subgoal
+    apply (rule ext)
+    by transfer' auto
+  subgoal
+    apply (rule ext)
+    by transfer' auto
+  subgoal
+    by transfer' auto
+  subgoal
+    apply (rule ext)
+    by transfer' auto
+  subgoal by (fact natLeq_card_order)
+  subgoal by (fact natLeq_cinfinite)
+  subgoal by (fact regularCard_natLeq)
+  subgoal
+    apply transfer'
+    apply (tactic \<open>resolve_tac @{context} (BNF_Def.bnf_of @{context} "List.list" |> the |> BNF_Def.set_bd_of_bnf) 1\<close>)
+    done
+  subgoal
+    apply auto
+    apply transfer'
+    by (smt (verit) list_all2_trans relcompp.relcompI)
+  subgoal
+    apply (rule ext)+
+    apply transfer
+    by (auto simp: list.in_rel)
+  subgoal
+    apply (rule ext)
+    apply transfer'
+    by (auto simp: list_all_iff)
+  subgoal
+    by transfer' auto
+  done
+
+section \<open>Indexing\<close>
+
+lift_definition nth_vec' :: \<open>'a ^ 'b \<Rightarrow> nat \<Rightarrow> 'a\<close> is nth .
+
+lift_definition nth_vec :: \<open>'a ^ 'b \<Rightarrow> 'b :: index1 \<Rightarrow> 'a\<close> (infixl "$" 90)
+  \<comment> \<open>We fix this to \<^class>\<open>index1\<close> because indexing a unit vector makes no sense.\<close>
+  is \<open>\<lambda>xs. nth xs \<circ> from_index\<close> .
+
+lemma nth_vec_alt_def: \<open>nth_vec v = nth_vec' v \<circ> from_index\<close>
+  by transfer' auto
+
+text \<open>
+  We additionally define a notion of converting a function into a vector, by mapping over all
+  \<^const>\<open>indexes\<close>.
+\<close>
+
+lift_definition vec_lambda :: \<open>('b :: index \<Rightarrow> 'a) \<Rightarrow> 'a ^ 'b\<close> (binder "\<chi>" 10)
+  is \<open>\<lambda>f. map f indexes\<close> by simp
+
+lemma vec_lambda_nth[simp]: \<open>vec_lambda f $ i = f i\<close>
+  by transfer auto
+
+section \<open>Unit vector\<close>
+
+text \<open>
+  The \<^emph>\<open>unit vector\<close> is the unique vector of length zero. We use \<^typ>\<open>0\<close> as index type, but
+  \<^typ>\<open>nat\<close> or any other infinite type would work just as well.
+\<close>
+
+lift_definition unit_vec :: \<open>'a ^ 0\<close> is \<open>[]\<close> by simp
+
+lemma unit_vec_unique: \<open>v = unit_vec\<close>
+  by transfer auto
+
+lemma unit_vec_unique_simp[simp]: \<open>NO_MATCH v unit_vec \<Longrightarrow> v = unit_vec\<close>
+  by (rule unit_vec_unique)
+
+lemma set_unit_vec[simp]: \<open>set_vec (v :: 'a ^ 0) = {}\<close>
+  by transfer auto
+
+lemma map_unit_vec[simp]: \<open>map_vec f v = unit_vec\<close>
+  by simp
+
+lemma zip_unit_vec[simp]: \<open>zip_vec u v = unit_vec\<close>
+  by simp
+
+lemma rel_unit_vec[simp]: \<open>rel_vec R (u :: 'a ^ 0) v \<longleftrightarrow> True\<close>
+  by transfer auto
+
+lemma pred_unit_vec[simp]: \<open>pred_vec P (v :: 'a ^ 0)\<close>
+  by (simp add: vec.pred_set)
+
+
+section \<open>General lemmas\<close>
+
+lemmas vec_simps[simp] =
+  map_vec.rep_eq
+  zip_vec.rep_eq
+  replicate_vec.rep_eq
+
+lemmas map_vec_cong[fundef_cong] = map_cong[Transfer.transferred]
+
+lemmas rel_vec_cong = list.rel_cong[Transfer.transferred]
+
+lemmas pred_vec_cong = list.pred_cong[Transfer.transferred]
+
+lemma vec_eq_if: "list_of_vec f = list_of_vec g \<Longrightarrow> f = g"
+  by (metis list_of_vec_inverse)
+
+lemma vec_cong: "(\<And>i. f $ i = g $ i) \<Longrightarrow> f = g"
+  apply transfer
+  apply simp
+  apply (rule list_cong_index; assumption)
+  done
+
+lemma finite_set_vec[intro, simp]: \<open>finite (set_vec v)\<close>
+  by transfer' auto
+
+lemma set_vec_in[intro, simp]: \<open>v $ i \<in> set_vec v\<close>
+  by transfer auto
+
+lemma set_vecE[elim]:
+  assumes \<open>x \<in> set_vec v\<close>
+  obtains i where \<open>x = v $ i\<close>
+  using assms
+  by transfer (auto simp: in_set_conv_nth elim: from_indexE)
+
+lemma map_nth_vec[simp]: \<open>map_vec f v $ i = f (v $ i)\<close>
+  by transfer auto
+
+lemma replicate_nth_vec[simp]: \<open>replicate_vec a $ i = a\<close>
+  by transfer auto
+
+lemma replicate_set_vec[simp]: \<open>set_vec (replicate_vec a :: 'a ^ 'b :: index1) = {a}\<close>
+  by transfer simp
+
+lemma vec_explode: \<open>v = (\<chi> i. v $ i)\<close>
+  by (rule vec_cong) auto
+
+lemma vec_explode1:
+  fixes v :: \<open>'a ^ 1\<close>
+  obtains a where \<open>v = (\<chi> _. a)\<close>
+  apply (rule that[of \<open>v $ 1\<close>])
+  apply (subst vec_explode[of v])
+  apply (rule arg_cong[where f = vec_lambda])
+  apply (rule ext)
+  apply (subst num1_eq1)
+  by (rule refl)
+
+lemma zip_nth_vec[simp]: \<open>zip_vec u v $ i = (u $ i, v $ i)\<close>
+  by transfer auto
+
+lemma zip_vec_fst[simp]: \<open>map_vec fst (zip_vec u v) = u\<close>
+  by transfer auto
+
+lemma zip_vec_snd[simp]: \<open>map_vec snd (zip_vec u v) = v\<close>
+  by transfer auto
+
+lemma zip_lambda_vec[simp]: \<open>zip_vec (vec_lambda f) (vec_lambda g) = (\<chi> i. (f i, g i))\<close>
+  by transfer' (simp add: zip_map_same)
+
+lemma zip_map_vec: \<open>zip_vec (map_vec f u) (map_vec g v) = map_vec (\<lambda>(x, y). (f x, g y)) (zip_vec u v)\<close>
+  by transfer' (auto simp: zip_map1 zip_map2)
+
+lemma list_of_vec_length[simp]: \<open>length (list_of_vec (v :: 'a ^ 'b)) = CARD('b)\<close>
+  using list_of_vec by blast
+
+lemma list_vec_list: \<open>length xs = CARD('n) \<Longrightarrow> list_of_vec (vec_of_list xs :: 'a ^ 'n) = xs\<close>
+  by (subst vec.vec_of_list_inverse) auto
+
+lemma map_vec_list: \<open>length xs = CARD('n) \<Longrightarrow> map_vec f (vec_of_list xs :: 'a ^ 'n) = vec_of_list (map f xs)\<close>
+  by (rule map_vec.abs_eq) (auto simp: eq_onp_def)
+
+lemma set_vec_list: \<open>length xs = CARD('n) \<Longrightarrow> set_vec (vec_of_list xs :: 'a ^ 'n) = set xs\<close>
+  by (rule set_vec.abs_eq) (auto simp: eq_onp_def)
+
+lemma list_all_zip: \<open>length xs = length ys \<Longrightarrow> list_all P (zip xs ys) \<longleftrightarrow> list_all2 (\<lambda>x y. P (x, y)) xs ys\<close>
+  by (erule list_induct2) auto
+
+lemma pred_vec_zip: \<open>pred_vec P (zip_vec xs ys) \<longleftrightarrow> rel_vec (\<lambda>x y. P (x, y)) xs ys\<close>
+  by transfer (simp add: list_all_zip)
+
+lemma list_all2_left: \<open>length xs = length ys \<Longrightarrow> list_all2 (\<lambda>x y. P x) xs ys \<longleftrightarrow> list_all P xs\<close>
+  by (erule list_induct2) auto
+
+lemma list_all2_right: \<open>length xs = length ys \<Longrightarrow> list_all2 (\<lambda>_. P) xs ys \<longleftrightarrow> list_all P ys\<close>
+  by (erule list_induct2) auto
+
+lemma rel_vec_left: \<open>rel_vec (\<lambda>x y. P x) xs ys \<longleftrightarrow> pred_vec P xs\<close>
+  by transfer (simp add: list_all2_left)
+
+lemma rel_vec_right: \<open>rel_vec (\<lambda>_. P) xs ys \<longleftrightarrow> pred_vec P ys\<close>
+  by transfer (simp add: list_all2_right)
+
+
+section \<open>Instances\<close>
+
+definition bounded_lists :: \<open>nat \<Rightarrow> 'a set \<Rightarrow> 'a list set\<close> where
+\<open>bounded_lists n A = {xs. length xs = n \<and> list_all (\<lambda>x. x \<in> A) xs}\<close>
+
+lemma bounded_lists_finite:
+  assumes \<open>finite A\<close>
+  shows \<open>finite (bounded_lists n A)\<close>
+proof (induction n)
+  case (Suc n)
+  moreover have \<open>bounded_lists (Suc n) A \<subseteq> (\<lambda>(x, xs). x # xs) ` (A \<times> bounded_lists n A)\<close>
+    unfolding bounded_lists_def
+    by (auto intro!: image_eqI simp: length_Suc_conv split_beta)
+  ultimately show ?case
+    using assms by (meson finite_SigmaI finite_imageI finite_subset)
+qed (simp add: bounded_lists_def)
+
+lemma bounded_lists_bij: \<open>bij_betw list_of_vec (UNIV :: ('a ^ 'b) set) (bounded_lists CARD('b) UNIV)\<close>
+  unfolding bij_betw_def bounded_lists_def
+  by (metis (no_types, lifting) Ball_set Collect_cong UNIV_I inj_def type_definition.Rep_range type_definition_vec vec_eq_if)
+
+
+text \<open>If the base type is \<^class>\<open>finite\<close>, so is the vector type.\<close>
+
+instance vec :: (finite, type) finite
+  apply standard
+  apply (subst bij_betw_finite[OF bounded_lists_bij])
+  apply (rule bounded_lists_finite)
+  by simp
+
+text \<open>The \<^const>\<open>size\<close> of the vector is the \<^const>\<open>length\<close> of the underlying list.\<close>
+
+instantiation vec :: (type, type) size
+begin
+
+lift_definition size_vec :: \<open>'a ^ 'b \<Rightarrow> nat\<close> is length .
+
+instance ..
+
+end
+
+lemma size_vec_alt_def[simp]: \<open>size (v :: 'a ^ 'b) = CARD('b)\<close>
+  by transfer simp
+
+text \<open>Vectors can be compared for equality.\<close>
+
+instantiation vec :: (equal, type) equal
+begin
+
+lift_definition equal_vec :: \<open>'a ^ 'b \<Rightarrow> 'a ^ 'b \<Rightarrow> bool\<close> is \<open>equal_class.equal\<close> .
+
+instance
+  apply standard
+  apply transfer'
+  by (simp add: equal_list_def)
+
+end
+
+section \<open>Further operations\<close>
+
+subsection \<open>Distinctness\<close>
+
+lift_definition distinct_vec :: \<open>'a ^ 'n \<Rightarrow> bool\<close> is \<open>distinct\<close> .
+
+lemma distinct_vec_alt_def: \<open>distinct_vec v \<longleftrightarrow> (\<forall>i j. i \<noteq> j \<longrightarrow> v $ i \<noteq> v $ j)\<close>
+  apply transfer
+  unfolding distinct_conv_nth comp_apply
+  by (metis from_index_bound from_to_index to_from_index)
+
+lemma distinct_vecI:
+  assumes \<open>\<And>i j. i \<noteq> j \<Longrightarrow> v $ i \<noteq> v $ j\<close>
+  shows \<open>distinct_vec v\<close>
+  using assms unfolding distinct_vec_alt_def by simp
+
+lemma distinct_vec_mapI: \<open>distinct_vec xs \<Longrightarrow> inj_on f (set_vec xs) \<Longrightarrow> distinct_vec (map_vec f xs)\<close>
+  by transfer' (metis distinct_map)
+
+lemma distinct_vec_zip_fst: \<open>distinct_vec u \<Longrightarrow> distinct_vec (zip_vec u v)\<close>
+  by transfer' (metis distinct_zipI1)
+
+lemma distinct_vec_zip_snd: \<open>distinct_vec v \<Longrightarrow> distinct_vec (zip_vec u v)\<close>
+  by transfer' (metis distinct_zipI2)
+
+lemma inj_set_of_vec: \<open>distinct_vec (map_vec f v) \<Longrightarrow> inj_on f (set_vec v)\<close>
+  by transfer' (metis distinct_map)
+
+lemma distinct_vec_list: \<open>length xs = CARD('n) \<Longrightarrow> distinct_vec (vec_of_list xs :: 'a ^ 'n) \<longleftrightarrow> distinct xs\<close>
+  by (subst distinct_vec.rep_eq) (simp add: list_vec_list)
+
+subsection \<open>Summing\<close>
+
+lift_definition sum_vec :: \<open>'b::comm_monoid_add ^ 'a \<Rightarrow> 'b\<close> is sum_list .
+
+lemma sum_vec_lambda: \<open>sum_vec (vec_lambda v) = sum_list (map v indexes)\<close>
+  by transfer simp
+
+lemma elem_le_sum_vec:
+  fixes f :: \<open>'a :: canonically_ordered_monoid_add ^ 'b :: index1\<close>
+  shows "f $ i \<le> sum_vec f"
+  apply transfer
+  apply simp
+  apply (rule elem_le_sum_list)
+  by auto
+
+
+section \<open>Code setup\<close>
+
+text \<open>
+  Since \<^const>\<open>vec_of_list\<close> cannot be directly used in code generation, we defined a convenience
+  wrapper that checks the length and aborts if necessary.
+\<close>
+
+definition replicate' where \<open>replicate' n = replicate n undefined\<close>
+
+declare [[code abort: replicate']]
+
+lift_definition vec_of_list' :: \<open>'a list \<Rightarrow> 'a ^ 'n\<close>
+  is \<open>\<lambda>xs. if length xs \<noteq> CARD('n) then replicate' CARD('n) else xs\<close>
+  by (auto simp: replicate'_def)
+
+
+experiment begin
+
+proposition
+  \<open>sum_vec (\<chi> (i::2). (3::nat)) = 6\<close>
+  \<open>distinct_vec (vec_of_list' [1::nat, 2] :: nat ^ 2)\<close>
+  \<open>\<not> distinct_vec (vec_of_list' [1::nat, 1] :: nat ^ 2)\<close>
+  by eval+
+
+end
+
+export_code
+  sum_vec
+  map_vec
+  rel_vec
+  pred_vec
+  set_vec
+  zip_vec
+  distinct_vec
+  list_of_vec
+  vec_of_list'
+  checking SML
+
+lifting_update vec.lifting
+lifting_forget vec.lifting
+
+end
\ No newline at end of file
diff --git a/thys/Fixed_Length_Vector/ROOT b/thys/Fixed_Length_Vector/ROOT
new file mode 100644
--- /dev/null
+++ b/thys/Fixed_Length_Vector/ROOT
@@ -0,0 +1,10 @@
+chapter AFP
+
+session Fixed_Length_Vector (AFP) = HOL +
+  options [timeout = 600]
+  sessions
+    "HOL-Library"
+  theories
+    Fixed_Length_Vector
+  document_files
+    "root.tex"
diff --git a/thys/Fixed_Length_Vector/document/root.tex b/thys/Fixed_Length_Vector/document/root.tex
new file mode 100644
--- /dev/null
+++ b/thys/Fixed_Length_Vector/document/root.tex
@@ -0,0 +1,22 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
+\usepackage{isabelle,isabellesym}
+
+\usepackage{pdfsetup}
+
+\urlstyle{rm}
+\isabellestyle{it}
+
+\begin{document}
+
+\title{Fixed-length vectors}
+\author{Lars Hupel}
+\maketitle
+
+\tableofcontents
+
+\parindent 0pt\parskip 0.5ex
+
+\input{session}
+
+\end{document}
\ No newline at end of file
diff --git a/thys/ROOTS b/thys/ROOTS
--- a/thys/ROOTS
+++ b/thys/ROOTS
@@ -1,761 +1,762 @@
 ABY3_Protocols
 ADS_Functor
 AI_Planning_Languages_Semantics
 AODV
 AOT
 AVL-Trees
 AWN
 Abortable_Linearizable_Modules
 Abs_Int_ITP2012
 Abstract-Hoare-Logics
 Abstract-Rewriting
 Abstract_Completeness
 Abstract_Soundness
 Ackermanns_not_PR
 Actuarial_Mathematics
 Adaptive_State_Counting
 Affine_Arithmetic
 Aggregation_Algebras
 Akra_Bazzi
 Algebraic_Numbers
 Algebraic_VCs
 Allen_Calculus
 Amicable_Numbers
 Amortized_Complexity
 AnselmGod
 Applicative_Lifting
 Approximation_Algorithms
 Architectural_Design_Patterns
 Aristotles_Assertoric_Syllogistic
 Arith_Prog_Rel_Primes
 ArrowImpossibilityGS
 Attack_Trees
 Auto2_HOL
 Auto2_Imperative_HOL
 AutoFocus-Stream
 Automated_Stateful_Protocol_Verification
 Automatic_Refinement
 AxiomaticCategoryTheory
 BDD
 BD_Security_Compositional
 BNF_CC
 BNF_Operations
 BTree
 Balog_Szemeredi_Gowers
 Banach_Steinhaus
 Belief_Revision
 Bell_Numbers_Spivey
 BenOr_Kozen_Reif
 Berlekamp_Zassenhaus
 Bernoulli
 Bertrands_Postulate
 Bicategory
 BinarySearchTree
 Binary_Code_Imprimitive
 Binding_Syntax_Theory
 Binomial-Heaps
 Binomial-Queues
 BirdKMP
 Birkhoff_Finite_Distributive_Lattices
 Blue_Eyes
 Bondy
 Boolean_Expression_Checkers
 Boolos_Curious_Inference
 Boolos_Curious_Inference_Automated
 Bounded_Deducibility_Security
 Buchi_Complementation
 Budan_Fourier
 Buffons_Needle
 Buildings
 BytecodeLogicJmlTypes
 C2KA_DistributedSystems
 CAVA_Automata
 CAVA_LTL_Modelchecker
 CCS
 CHERI-C_Memory_Model
 CISC-Kernel
 CRDT
 CRYSTALS-Kyber
 CSP_RefTK
 CVP_Hardness
 CYK
 CZH_Elementary_Categories
 CZH_Foundations
 CZH_Universal_Constructions
 CakeML
 CakeML_Codegen
 Call_Arity
 Card_Equiv_Relations
 Card_Multisets
 Card_Number_Partitions
 Card_Partitions
 Cartan_FP
 Case_Labeling
 Catalan_Numbers
 Category
 Category2
 Category3
 Catoids
 Cauchy
 Cayley_Hamilton
 Certification_Monads
 Ceva
 Chandy_Lamport
 Chord_Segments
 Circus
 Clean
 Clique_and_Monotone_Circuits
 ClockSynchInst
 Closest_Pair_Points
 CoCon
 CoSMeDis
 CoSMed
 CofGroups
 Coinductive
 Coinductive_Languages
 Collections
 Combinable_Wands
 Combinatorial_Enumeration_Algorithms
 Combinatorics_Words
 Combinatorics_Words_Graph_Lemma
 Combinatorics_Words_Lyndon
 CommCSL
 Commuting_Hermitian
 Comparison_Sort_Lower_Bound
 Compiling-Exceptions-Correctly
 Complete_Non_Orders
 Completeness
 Complex_Bounded_Operators
 Complex_Geometry
 Complx
 ComponentDependencies
 ConcurrentGC
 ConcurrentIMP
 Concurrent_Ref_Alg
 Concurrent_Revisions
 Conditional_Simplification
 Conditional_Transfer_Rule
 Consensus_Refined
 Constructive_Cryptography
 Constructive_Cryptography_CM
 Constructor_Funs
 Containers
 Cook_Levin
 CoreC++
 Core_DOM
 Core_SC_DOM
 Correctness_Algebras
 Cotangent_PFD_Formula
 Count_Complex_Roots
 CryptHOL
 CryptoBasedCompositionalProperties
 Crypto_Standards
 Cubic_Quartic_Equations
 DCR-ExecutionEquivalence
 DFS_Framework
 DOM_Components
 DPRM_Theorem
 DPT-SAT-Solver
 DataRefinementIBP
 Datatype_Order_Generator
 Decl_Sem_Fun_PL
 Decreasing-Diagrams
 Decreasing-Diagrams-II
 Dedekind_Real
 Deep_Learning
 Delta_System_Lemma
 Density_Compiler
 Dependent_SIFUM_Refinement
 Dependent_SIFUM_Type_Systems
 Depth-First-Search
 Derangements
 Deriving
 Descartes_Sign_Rule
 Design_Theory
 Dict_Construction
 Differential_Dynamic_Logic
 Differential_Game_Logic
 DigitsInBase
 Digit_Expansions
 Dijkstra_Shortest_Path
 Diophantine_Eqns_Lin_Hom
 Dirichlet_L
 Dirichlet_Series
 DiscretePricing
 Discrete_Summation
 DiskPaxos
 Distributed_Distinct_Elements
 Dominance_CHK
 DynamicArchitectures
 Dynamic_Tables
 E_Transcendental
 Earley_Parser
 Echelon_Form
 EdmondsKarp_Maxflow
 Edwards_Elliptic_Curves_Group
 Efficient-Mergesort
 Efficient_Weighted_Path_Order
 Elliptic_Curves_Group_Law
 Encodability_Process_Calculi
 Epistemic_Logic
 Equivalence_Relation_Enumeration
 Ergodic_Theory
 Error_Function
 Euler_MacLaurin
 Euler_Partition
 Eval_FO
 Example-Submission
 Executable_Randomized_Algorithms
 Expander_Graphs
 Extended_Finite_State_Machine_Inference
 Extended_Finite_State_Machines
 FFT
 FLP
 FOL-Fitting
 FOL_Axiomatic
 FOL_Harrison
 FOL_Seq_Calc1
 FOL_Seq_Calc2
 FOL_Seq_Calc3
 FO_Theory_Rewriting
 FSM_Tests
 Factor_Algebraic_Polynomial
 Factored_Transition_System_Bounding
 Falling_Factorial_Sum
 Farkas
 FeatherweightJava
 Featherweight_OCL
 Fermat3_4
 FileRefinement
 FinFun
 Finger-Trees
 Finite-Map-Extras
 Finite_Automata_HF
 Finite_Fields
 Finitely_Generated_Abelian_Groups
 First_Order_Terms
 First_Welfare_Theorem
 Fishburn_Impossibility
 Fisher_Yates
 Fishers_Inequality
+Fixed_Length_Vector
 Flow_Networks
 Floyd_Warshall
 Flyspeck-Tame
 FocusStreamsCaseStudies
 Forcing
 Formal_Puiseux_Series
 Formal_SSA
 Formula_Derivatives
 Foundation_of_geometry
 Fourier
 Free-Boolean-Algebra
 Free-Groups
 Frequency_Moments
 Fresh_Identifiers
 FunWithFunctions
 FunWithTilings
 Functional-Automata
 Functional_Ordered_Resolution_Prover
 Furstenberg_Topology
 GPU_Kernel_PL
 Gabow_SCC
 GaleStewart_Games
 Gale_Shapley
 Game_Based_Crypto
 Gauss-Jordan-Elim-Fun
 Gauss_Jordan
 Gauss_Sums
 Gaussian_Integers
 GenClock
 General-Triangle
 Generalized_Counting_Sort
 Generic_Deriving
 Generic_Join
 GewirthPGCProof
 Girth_Chromatic
 Given_Clause_Loops
 GoedelGod
 Goedel_HFSet_Semantic
 Goedel_HFSet_Semanticless
 Goedel_Incompleteness
 Goodstein_Lambda
 GraphMarkingIBP
 Graph_Saturation
 Graph_Theory
 Gray_Codes
 Green
 Groebner_Bases
 Groebner_Macaulay
 Gromov_Hyperbolicity
 Grothendieck_Schemes
 Group-Ring-Module
 HOL-CSP
 HOLCF-Prelude
 HRB-Slicing
 Hahn_Jordan_Decomposition
 Hales_Jewett
 Heard_Of
 Hello_World
 HereditarilyFinite
 Hermite
 Hermite_Lindemann
 Hidden_Markov_Models
 Higher_Order_Terms
 HoareForDivergence
 Hoare_Time
 Hood_Melville_Queue
 HotelKeyCards
 Huffman
 Hybrid_Logic
 Hybrid_Multi_Lane_Spatial_Logic
 Hybrid_Systems_VCs
 HyperCTL
 HyperHoareLogic
 Hyperdual
 IEEE_Floating_Point
 IFC_Tracking
 IMAP-CRDT
 IMO2019
 IMP2
 IMP2_Binary_Heap
 IMP_Compiler
 IMP_Compiler_Reuse
 IP_Addresses
 Imperative_Insertion_Sort
 Implicational_Logic
 Impossible_Geometry
 Incompleteness
 Incredible_Proof_Machine
 Independence_CH
 Inductive_Confidentiality
 Inductive_Inference
 InfPathElimination
 InformationFlowSlicing
 InformationFlowSlicing_Inter
 Integration
 Interpolation_Polynomials_HOL_Algebra
 Interpreter_Optimizations
 Interval_Arithmetic_Word32
 Intro_Dest_Elim
 Involutions2Squares
 Iptables_Semantics
 Irrational_Series_Erdos_Straus
 Irrationality_J_Hancl
 Irrationals_From_THEBOOK
 IsaGeoCoq
 IsaNet
 Isabelle_C
 Isabelle_Marries_Dirac
 Isabelle_Meta_Model
 Jacobson_Basic_Algebra
 Jinja
 JinjaDCI
 JinjaThreads
 JiveDataStoreModel
 Jordan_Hoelder
 Jordan_Normal_Form
 KAD
 KAT_and_DRA
 KBPs
 KD_Tree
 Key_Agreement_Strong_Adversaries
 Khovanskii_Theorem
 Kleene_Algebra
 Kneser_Cauchy_Davenport
 Knights_Tour
 Knot_Theory
 Knuth_Bendix_Order
 Knuth_Morris_Pratt
 Koenigsberg_Friendship
 Kruskal
 Kuratowski_Closure_Complement
 LLL_Basis_Reduction
 LLL_Factorization
 LOFT
 LP_Duality
 LTL
 LTL_Master_Theorem
 LTL_Normal_Form
 LTL_to_DRA
 LTL_to_GBA
 Lam-ml-Normalization
 LambdaAuth
 LambdaMu
 Lambda_Free_EPO
 Lambda_Free_KBOs
 Lambda_Free_RPOs
 Lambert_W
 Landau_Symbols
 Laplace_Transform
 Latin_Square
 LatticeProperties
 Launchbury
 Laws_of_Large_Numbers
 Lazy-Lists-II
 Lazy_Case
 Lehmer
 Lifting_Definition_Option
 Lifting_the_Exponent
 LightweightJava
 LinearQuantifierElim
 Linear_Inequalities
 Linear_Programming
 Linear_Recurrences
 Liouville_Numbers
 List-Index
 List-Infinite
 List_Interleaving
 List_Inversions
 List_Update
 LocalLexing
 Localization_Ring
 Locally-Nameless-Sigma
 Logging_Independent_Anonymity
 Lowe_Ontological_Argument
 Lower_Semicontinuous
 Lp
 Lucas_Theorem
 MDP-Algorithms
 MDP-Rewards
 MFMC_Countable
 MFODL_Monitor_Optimized
 MFOTL_Monitor
 MSO_Regex_Equivalence
 Markov_Models
 Marriage
 Mason_Stothers
 Matrices_for_ODEs
 Matrix
 Matrix_Tensor
 Matroids
 Max-Card-Matching
 Maximum_Segment_Sum
 Median_Method
 Median_Of_Medians_Selection
 Menger
 Mereology
 Mersenne_Primes
 Metalogic_ProofChecker
 MHComputation
 MiniML
 MiniSail
 Minimal_SSA
 Minkowskis_Theorem
 Minsky_Machines
 MLSS_Decision_Proc
 Modal_Logics_for_NTS
 Modular_Assembly_Kit_Security
 Modular_arithmetic_LLL_and_HNF_algorithms
 Monad_Memo_DP
 Monad_Normalisation
 MonoBoolTranAlgebra
 MonoidalCategory
 Monomorphic_Monad
 MuchAdoAboutTwo
 Multi_Party_Computation
 Multirelations
 Multirelations_Heterogeneous
 Multiset_Ordering_NPC
 Multitape_To_Singletape_TM
 Myhill-Nerode
 Name_Carrying_Type_Inference
 Nano_JSON
 Nash_Williams
 Nat-Interval-Logic
 Native_Word
 Nested_Multisets_Ordinals
 Network_Security_Policy_Verification
 Neumann_Morgenstern_Utility
 No_FTL_observers
 No_FTL_observers_Gen_Rel
 Nominal2
 Noninterference_CSP
 Noninterference_Concurrent_Composition
 Noninterference_Generic_Unwinding
 Noninterference_Inductive_Unwinding
 Noninterference_Ipurge_Unwinding
 Noninterference_Sequential_Composition
 NormByEval
 Nullstellensatz
 Number_Theoretic_Transform
 Octonions
 OpSets
 Open_Induction
 Optics
 Optimal_BST
 Orbit_Stabiliser
 Order_Lattice_Props
 Ordered_Resolution_Prover
 Ordinal
 Ordinal_Partitions
 Ordinals_and_Cardinals
 Ordinary_Differential_Equations
 PAC_Checker
 PAL
 PAPP_Impossibility
 PCF
 PLM
 POPLmark-deBruijn
 PSemigroupsConvolution
 Package_logic
 Padic_Field
 Padic_Ints
 Pairing_Heap
 Paraconsistency
 Parity_Game
 Partial_Function_MR
 Partial_Order_Reduction
 Password_Authentication_Protocol
 Pell
 Perfect-Number-Thm
 Perron_Frobenius
 Physical_Quantities
 Pi_Calculus
 Pi_Transcendental
 Planarity_Certificates
 Pluennecke_Ruzsa_Inequality
 Poincare_Bendixson
 Poincare_Disc
 Polygonal_Number_Theorem
 Polynomial_Factorization
 Polynomial_Interpolation
 Polynomials
 Pop_Refinement
 Posix-Lexing
 Possibilistic_Noninterference
 Power_Sum_Polynomials
 Pratt_Certificate
 Prefix_Free_Code_Combinators
 Presburger-Automata
 Prim_Dijkstra_Simple
 Prime_Distribution_Elementary
 Prime_Harmonic_Series
 Prime_Number_Theorem
 Priority_Queue_Braun
 Priority_Search_Trees
 Probabilistic_Noninterference
 Probabilistic_Prime_Tests
 Probabilistic_System_Zoo
 Probabilistic_Timed_Automata
 Probabilistic_While
 Probability_Inequality_Completeness
 Program-Conflict-Analysis
 Progress_Tracking
 Projective_Geometry
 Projective_Measurements
 Promela
 Proof_Strategy_Language
 PropResPI
 Propositional_Logic_Class
 Propositional_Proof_Systems
 Prpu_Maxflow
 PseudoHoops
 Psi_Calculi
 Ptolemys_Theorem
 Public_Announcement_Logic
 QHLProver
 QR_Decomposition
 Quantales
 Quantales_Converse
 Quantifier_Elimination_Hybrid
 Quasi_Borel_Spaces
 Quaternions
 Query_Optimization
 Quick_Sort_Cost
 RIPEMD-160-SPARK
 ROBDD
 RSAPSS
 Ramsey-Infinite
 Random_BSTs
 Random_Graph_Subgraph_Threshold
 Randomised_BSTs
 Randomised_Social_Choice
 Rank_Nullity_Theorem
 Real_Impl
 Real_Power
 Real_Time_Deque
 Recursion-Addition
 Recursion-Theory-I
 Refine_Imperative_HOL
 Refine_Monadic
 RefinementReactive
 Regex_Equivalence
 Registers
 Regression_Test_Selection
 Regular-Sets
 Regular_Algebras
 Regular_Tree_Relations
 Relation_Algebra
 Relational-Incorrectness-Logic
 Relational_Disjoint_Set_Forests
 Relational_Forests
 Relational_Method
 Relational_Minimum_Spanning_Trees
 Relational_Paths
 Rensets
 Rep_Fin_Groups
 ResiduatedTransitionSystem
 Residuated_Lattices
 Resolution_FOL
 Rewrite_Properties_Reduction
 Rewriting_Z
 Ribbon_Proofs
 Risk_Free_Lending
 Robbins-Conjecture
 Robinson_Arithmetic
 Root_Balanced_Tree
 Roth_Arithmetic_Progressions
 Routing
 Roy_Floyd_Warshall
 SATSolverVerification
 SCC_Bloemen_Sequential
 SC_DOM_Components
 SDS_Impossibility
 SIFPL
 SIFUM_Type_Systems
 SPARCv8
 Safe_Distance
 Safe_OCL
 Safe_Range_RC
 Saturation_Framework
 Saturation_Framework_Extensions
 Sauer_Shelah_Lemma
 Schutz_Spacetime
 Schwartz_Zippel
 Secondary_Sylow
 Security_Protocol_Refinement
 Selection_Heap_Sort
 SenSocialChoice
 Separata
 Separation_Algebra
 Separation_Logic_Imperative_HOL
 Separation_Logic_Unbounded
 SequentInvertibility
 Shadow_DOM
 Shadow_SC_DOM
 Shivers-CFA
 ShortestPath
 Show
 Sigma_Commit_Crypto
 Signature_Groebner
 Simpl
 Simple_Clause_Learning
 Simple_Firewall
 Simplex
 Simplicial_complexes_and_boolean_functions
 SimplifiedOntologicalArgument
 Skew_Heap
 Skip_Lists
 Slicing
 Sliding_Window_Algorithm
 Smith_Normal_Form
 Smooth_Manifolds
 Solidity
 Sophomores_Dream
 Sort_Encodings
 Source_Coding_Theorem
 SpecCheck
 Special_Function_Bounds
 Splay_Tree
 Sqrt_Babylonian
 Stable_Matching
 Stalnaker_Logic
 Statecharts
 Stateful_Protocol_Composition_and_Typing
 Stellar_Quorums
 Stern_Brocot
 Stewart_Apollonius
 Stirling_Formula
 Stochastic_Matrices
 Stone_Algebras
 Stone_Kleene_Relation_Algebras
 Stone_Relation_Algebras
 Store_Buffer_Reduction
 Stream-Fusion
 Stream_Fusion_Code
 StrictOmegaCategories
 Strong_Security
 Sturm_Sequences
 Sturm_Tarski
 Stuttering_Equivalence
 Subresultants
 Subset_Boolean_Algebras
 SumSquares
 Sunflowers
 SuperCalc
 Suppes_Theorem
 Surprise_Paradox
 Symmetric_Polynomials
 Syntax_Independent_Logic
 Synthetic_Completeness
 Szemeredi_Regularity
 Szpilrajn
 TESL_Language
 TLA
 Tail_Recursive_Functions
 Tarskis_Geometry
 Taylor_Models
 Three_Circles
 Three_Squares
 Timed_Automata
 Topological_Semantics
 Topology
 TortoiseHare
 TsirelsonBound
 Transcendence_Series_Hancl_Rucki
 Transformer_Semantics
 Transition_Systems_and_Automata
 Transitive-Closure
 Transitive-Closure-II
 Transitive_Models
 Treaps
 Tree-Automata
 Tree_Decomposition
 Tree_Enumeration
 Triangle
 Trie
 Turans_Graph_Theorem
 Twelvefold_Way
 Two_Generated_Word_Monoids_Intersection
 Tycon
 Types_Tableaus_and_Goedels_God
 Types_To_Sets_Extension
 UPF
 UPF_Firewall
 UTP
 Undirected_Graph_Theory
 Universal_Hash_Families
 Universal_Turing_Machine
 UpDown_Scheme
 VYDRA_MDL
 Valuation
 Van_Emde_Boas_Trees
 Van_der_Waerden
 VectorSpace
 VeriComp
 Verified-Prover
 Verified_SAT_Based_AI_Planning
 VerifyThis2018
 VerifyThis2019
 Vickrey_Clarke_Groves
 Virtual_Substitution
 VolpanoSmith
 WHATandWHERE_Security
 WOOT_Strong_Eventual_Consistency
 WebAssembly
 Weight_Balanced_Trees
 Weighted_Arithmetic_Geometric_Mean
 Weighted_Path_Order
 Well_Quasi_Orders
 Wetzels_Problem
 Winding_Number_Eval
 Word_Lib
 WorkerWrapper
 X86_Semantics
 XML
 Youngs_Inequality
 ZFC_in_HOL
 Zeckendorf
 Zeta_3_Irrational
 Zeta_Function
 pGCL