added material

--- a/src/HOL/List.thy	Thu Oct 23 14:49:21 2025 +0200
+++ b/src/HOL/List.thy	Sat Oct 25 09:48:45 2025 +0900
@@ -6987,6 +6987,63 @@
 "listset (A # As) = set_Cons A (listset As)"
 
 
+subsubsection \<open>Transitive Closure on Lists\<close>
+
+text \<open>Use \<open>\<^sup>+\<close> on binary relations if possible.
+Transitive closure on lists is useful for executable definitions on the list level.
+Is not efficient, naive closure computation.\<close>
+
+definition "trans_list_step ps = [(a,c). (a,b) \<leftarrow> ps, (b',c) \<leftarrow> ps, b=b']"
+
+lemma set_trans_list_step_subset_trancl: "set (trans_list_step ps) \<subseteq> (set ps)^+"
+unfolding trans_list_step_def by auto
+
+function trancl_list :: "('a * 'a) list \<Rightarrow> ('a * 'a) list" where 
+"trancl_list ps =
+  (let ps' = trans_list_step ps
+   in if set ps' \<subseteq>  set ps then ps else trancl_list (List.union ps' ps))"
+by pat_completeness auto
+
+termination
+proof
+  let ?r = "\<lambda>ps::('a * 'a) list. card ((set ps)^+ - set(ps))"
+
+  show "wf (measure ?r)" by blast
+
+  fix ps ps' :: "('a * 'a) list"
+  assume asms: "ps' = trans_list_step ps" "\<not> set ps' \<subseteq> set ps"
+  let ?P = "set ps" let ?P' = "set(trans_list_step ps)"
+  have "(?P' \<union> ?P)\<^sup>+ - (?P' \<union> ?P) = ?P\<^sup>+ - (?P' \<union> ?P)"
+    using trancl_absorb_subset_trancl[OF set_trans_list_step_subset_trancl] by (metis Un_commute)
+  also have "?P\<^sup>+ - (?P' \<union> ?P) < ?P\<^sup>+ - ?P"
+    using asms(1,2) set_trans_list_step_subset_trancl by fastforce
+  finally have "card((?P' \<union> ?P)\<^sup>+ - (?P' \<union> ?P)) < card (?P\<^sup>+ - ?P)"
+    by (meson List.finite_set finite_Diff finite_trancl psubset_card_mono)
+  with asms show "(List.union ps' ps, ps) \<in> measure ?r" by(simp)
+qed
+
+declare trancl_list.simps[code, simp del]
+
+lemma set_trancl_list: "set(trancl_list ps) = (set ps)^+"
+proof (induction ps rule: trancl_list.induct)
+  case (1 ps)
+  let ?P = "set ps" let ?P' = "set(trans_list_step ps)"
+  show ?case
+  proof (cases "?P' \<subseteq> ?P")
+    case True
+    then have "(a,b) \<in> set ps \<Longrightarrow> (b,c) \<in> set ps \<Longrightarrow> (a,c) \<in> set ps" for a b c
+      unfolding trans_list_step_def by fastforce
+    then show ?thesis using True trancl_id[OF transI, of ?P]
+      using [[simp_depth_limit=3]] by(simp add: Let_def trancl_list.simps[of ps])
+  next
+    case False
+    from 1[OF refl False] False
+     show ?thesis using trancl_absorb_subset_trancl[OF set_trans_list_step_subset_trancl]
+       by(auto simp add: Un_commute Let_def trancl_list.simps[of ps])
+  qed
+qed
+
+
 subsection \<open>Relations on Lists\<close>
 
 subsubsection \<open>Length Lexicographic Ordering\<close>

--- a/src/HOL/Transitive_Closure.thy	Thu Oct 23 14:49:21 2025 +0200
+++ b/src/HOL/Transitive_Closure.thy	Sat Oct 25 09:48:45 2025 +0900
@@ -50,6 +50,9 @@
 
 end
 
+lemma trancl_incr: "r \<subseteq> r\<^sup>+"
+by auto
+
 abbreviation reflcl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"  (\<open>(\<open>notation=\<open>postfix =\<close>\<close>_\<^sup>=)\<close> [1000] 999)
   where "r\<^sup>= \<equiv> r \<union> Id"
 
@@ -435,6 +438,9 @@
     by (cases p) force
 qed
 
+lemma trancl_mono_subset: "A \<subseteq> B \<Longrightarrow> A^+ \<subseteq> B^+"
+by (blast intro: trancl_mono)
+
 lemma r_into_trancl': "\<And>p. p \<in> r \<Longrightarrow> p \<in> r\<^sup>+"
   by (simp only: split_tupled_all) (erule r_into_trancl)
 
@@ -547,6 +553,19 @@
 
 lemmas trancl_into_trancl2 = tranclp_into_tranclp2 [to_set]
 
+lemma trancl_trancl_Un: "(A^+ \<union> B)^+ = (A \<union> B)^+"
+proof
+  show "(A\<^sup>+ \<union> B)\<^sup>+ \<subseteq> (A \<union> B)\<^sup>+"
+    using trancl_id[OF trans_trancl] trancl_incr[of "A \<union> B"]
+      trancl_mono_subset[of A "(A \<union> B)\<^sup>+"] trancl_mono_subset[of "A\<^sup>+ \<union> B" "(A \<union> B)\<^sup>+"]
+    by blast
+  show "(A \<union> B)\<^sup>+ \<subseteq> (A\<^sup>+ \<union> B)\<^sup>+"
+    using trancl_incr[of A] trancl_mono_subset[OF sup_mono] by blast
+qed
+
+lemma trancl_absorb_subset_trancl: "B \<subseteq> A^+ \<Longrightarrow> (A \<union> B)^+ = A^+"
+using trancl_trancl_Un[of A B] sup.order_iff[of B "A\<^sup>+"] by auto
+
 lemma tranclp_converseI:
   assumes "(r\<^sup>+\<^sup>+)\<inverse>\<inverse> x y" shows "(r\<inverse>\<inverse>)\<^sup>+\<^sup>+ x y"
   using conversepD [OF assms]