--- a/src/HOL/Library/RBT_Set.thy Sat Mar 23 07:59:53 2024 +0100
+++ b/src/HOL/Library/RBT_Set.thy Sat Mar 23 18:55:38 2024 +0100
@@ -31,7 +31,7 @@
Set.member Set.insert Set.remove UNIV Set.filter image
Set.subset_eq Ball Bex can_select Set.union minus_set_inst.minus_set Set.inter
card the_elem Pow sum prod Product_Type.product Id_on
- Image trancl relcomp wf Min Inf_fin Max Sup_fin
+ Image trancl relcomp wf_on wf_code Min Inf_fin Max Sup_fin
"(Inf :: 'a set set \<Rightarrow> 'a set)" "(Sup :: 'a set set \<Rightarrow> 'a set)"
sorted_list_of_set List.map_project List.Bleast]]
@@ -644,9 +644,11 @@
by (simp add: relcomp_fold finite_fold_fold_keys[OF *])
qed
-lemma wf_set [code]:
- "wf (Set t) = acyclic (Set t)"
-by (simp add: wf_iff_acyclic_if_finite)
+lemma wf_set: "wf (Set t) = acyclic (Set t)"
+ by (simp add: wf_iff_acyclic_if_finite)
+
+lemma wf_code_set[code]: "wf_code (Set t) = acyclic (Set t)"
+ unfolding wf_code_def using wf_set .
lemma Min_fin_set_fold [code]:
"Min (Set t) =