Further clean-ups, and resolved a duplicate name

Author: simondfoster

List_Extra.thy

@@ -1271,11 +1271,11 @@ lemma distinct_b_lists: "distinct xs \<Longrightarrow> distinct (b_lists n xs)"
   using length_n_lists_elem apply blast
   done
 
-definition blists :: "nat \<Rightarrow> 'a set \<Rightarrow> 'a list set" where
-  "blists n A = {xs\<in>lists A. length xs \<le> n}"
+definition bounded_lists :: "nat \<Rightarrow> 'a set \<Rightarrow> 'a list set" where
+  "bounded_lists n A = {xs\<in>lists A. length xs \<le> n}"
 
-lemma blists_b_lists [code]: "blists n (set xs) = set (b_lists n xs)"
-  apply (auto simp add: blists_def in_blistsI in_listsI)
+lemma bounded_lists_b_lists [code]: "bounded_lists n (set xs) = set (b_lists n xs)"
+  apply (auto simp add: bounded_lists_def in_blistsI in_listsI)
   apply (meson b_lists_in_lists in_lists_conv_set)
   apply (meson length_b_lists_elem)
   done

Relation_Lib.thy

@@ -4,7 +4,7 @@ theory Relation_Lib
   imports
     Countable_Set_Extra Positive Infinity Enum_Type Record_Default_Instance Def_Const
     Relation_Extra Partial_Fun Partial_Inj Finite_Fun Finite_Inj Total_Fun List_Extra
-    Tabulate_Command
+    Bounded_List Tabulate_Command
 begin 
 
 text \<open> This theory marks the boundary between reusable library utilities and the creation of the

Sequence_Toolkit.thy

@@ -79,7 +79,7 @@ lemma iseq_iff [simp]: "xs \<in> iseq(A) \<longleftrightarrow> (xs \<in> seq A \
 subsection \<open> Bounded sequences \<close>
 
 definition bseq :: "\<nat> \<Rightarrow> 'a set \<Rightarrow> 'a list set" ("bseq[_]") where
-"bseq n A = blists n A"
+"bseq n A = bounded_lists n A"
 
 (* Proof that this corresponds to the Z definition required *)