# HG changeset patch
# User haftmann
# Date 1748584975 -7200
# Node ID 779a25d9a807679d0e94e28270440fc75a1523ba
# Parent  eb51ca97b5a3737771957269b7fcfd5d3a960760
explicit abort for big lattice operations over non-empty sets

diff -r eb51ca97b5a3 -r 779a25d9a807 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri May 30 08:02:54 2025 +0200
+++ b/src/HOL/List.thy	Fri May 30 08:02:55 2025 +0200
@@ -3266,8 +3266,17 @@
   "A \<inter> List.coset xs = fold Set.remove xs A"
   by (simp add: Diff_eq [symmetric] minus_set_fold)
 
+definition abort_empty_set :: \<open>('a set \<Rightarrow> 'a) \<Rightarrow> 'a\<close>
+  where [simp]: \<open>abort_empty_set F = F {}\<close>
+
+declare [[code abort: abort_empty_set]]
+
+lemma (in semilattice_set) set_empty_abort [code]:
+  \<open>F (set []) = abort_empty_set F\<close>
+  by simp
+
 lemma (in semilattice_set) set_eq_fold [code]:
-  "F (set (x # xs)) = fold f xs x"
+  \<open>F (set (x # xs)) = fold f xs x\<close>
 proof -
   interpret comp_fun_idem f
     by standard (simp_all add: fun_eq_iff left_commute)