diff -r 518a1464f1ac -r 791c44b1d130 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Sun Nov 02 20:01:43 2025 +0100
+++ b/src/HOL/Library/Word.thy	Sun Nov 02 20:36:24 2025 +0100
@@ -4609,203 +4609,12 @@
   by (simp add: word_cat_eq)
 
 
-subsection \<open>Computation on ranges\<close>
-
-context
-begin
-
-qualified definition range :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word list\<close> \<comment> \<open>only for code generation\<close>
-  where range_eq: \<open>range a b = sorted_list_of_set {a..<b}\<close>
-
-qualified lemma set_range_eq [simp]:
-  \<open>set (range a b) = {a..<b}\<close>
-  using finite_atLeastLessThan by (simp add: range_eq)
-
-qualified lemma distinct_range [simp]:
-  \<open>distinct (range a b)\<close>
-  by (simp add: range_eq)
-
-qualified lemma range_code [code]:
-  \<open>range a b = (if a < b then a # range (a + 1) b else [])\<close>
-proof (cases \<open>a < b\<close>)
-  case True
-  then have \<open>{a..<b} = insert a {a + 1..<b}\<close>
-    apply (auto simp add: not_le)
-     apply (metis inc_le leD word_le_less_eq)
-    apply (metis dual_order.strict_implies_order inc_less_eq_iff word_not_simps(3))
-    done
-  then show ?thesis
-    apply (auto simp add: range_eq finite_atLeastLessThan intro!: insort_is_Cons)
-    apply (subst insort_is_Cons)
-     apply auto
-    apply (metis Diff_insert Diff_insert0 atLeastAtMost_iff
-        atLeastLessThan_eq_atLeastAtMost_diff inc_less_eq_triv_imp
-        word_not_simps(3))
-    done
-next
-  case False
-  then show ?thesis
-    by (simp add: range_eq)
-qed
-
-qualified lemma atLeast_eq_range [code_unfold]:
-  \<open>{a..} = insert (- 1) (set (range a (- 1)))\<close>
-  by (auto simp add: not_less word_order.extremum_unique)
-
-qualified lemma greaterThan_eq_range [code_unfold]:
-  \<open>{a<..} = (if a = - 1 then {} else insert (- 1) (set (range (a + 1) (- 1))))\<close>
-  apply (auto simp add: not_less not_le word_order.extremum_unique inc_less_eq_iff)
-  apply (simp add: order_neq_le_trans)
-  done
-
-qualified lemma lessThan_eq_range [code_unfold]:
-  \<open>{..<b} = set (range 0 b)\<close>
-  by auto
-
-qualified lemma atMost_eq_range [code_unfold]:
-  \<open>{..b} = insert b (set (range 0 b))\<close> for b :: \<open>'a::len word\<close>
-  by auto
-
-qualified lemma atLeastLessThan_eq_range [code_unfold]:
-  \<open>{a..<b} = set (range a b)\<close>
-  by simp
-
-qualified lemma atLeastAtMost_eq_range [code_unfold]:
-  \<open>{a..b} = (if b = - 1 then {a..} else set (range a (b + 1)))\<close>
-  apply auto
-  using inc_less_eq_iff linorder_not_le apply blast
-  using inc_le linorder_not_less apply blast
-  done
-
-qualified lemma greaterThanLessThan_eq_range [code_unfold]:
-  \<open>{a<..<b} = (if a = - 1 then {} else set (range (a + 1) b))\<close>
-  by (auto simp add: inc_less_eq_iff)
-
-qualified lemma greaterThanAtMost_eq_range [code_unfold]:
-  \<open>{a<..b} = (if b = - 1 then {a<..} else if a = - 1 then {} else set (range (a + 1) (b + 1)))\<close>
-  apply (auto simp add: inc_less_eq_iff)
-   apply (metis add_diff_cancel add_eq_0_iff2 less_eq_dec_iff)
-  using inc_le linorder_not_less apply blast
-  done
-
-qualified definition all_range :: \<open>('a::len word \<Rightarrow> bool) \<Rightarrow> 'a word \<Rightarrow> 'a word \<Rightarrow> bool\<close> \<comment> \<open>only for code generation\<close>
-  where all_range_iff [code_abbrev, simp]: \<open>all_range P a b \<longleftrightarrow> (\<forall>n\<in>{a..<b}. P n)\<close>
-
-qualified lemma all_range_code [code]:
-  \<open>all_range P a b \<longleftrightarrow> (a < b \<longrightarrow> P a \<and> all_range P (a + 1) b)\<close>
-  apply (auto simp add: Ball_def simp flip: less_iff_succ_less_eq)
-   apply (metis inc_less_eq_iff order_le_less word_not_simps(3))
-  apply (metis antisym_conv2 inc_le)
-  done
-
-qualified lemma forall_atLeast_iff [code_unfold]:
-  \<open>(\<forall>n\<in>{a..}. P n) \<longleftrightarrow> all_range P a (- 1) \<and> P (- 1)\<close>
-  apply auto
-  using atLeastLessThan_iff word_order.not_eq_extremum apply blast
-  done
-
-qualified lemma forall_greater_eq_iff [code_unfold]:
-  \<open>(\<forall>n\<ge>a. P n) \<longleftrightarrow> (\<forall>n\<in>{a..}. P n)\<close>
-  by auto
-
-qualified lemma forall_greaterThan_iff [code_unfold]:
-  \<open>(\<forall>n\<in>{a<..}. P n) \<longleftrightarrow> a = - 1 \<or> all_range P (a + 1) (- 1) \<and> P (- 1)\<close>
-  apply (auto simp add: inc_less_eq_iff word_order.not_eq_extremum)
-  apply (metis atLeastLessThan_iff inc_le word_order.not_eq_extremum)
-  done
-
-qualified lemma forall_greater_iff [code_unfold]:
-  \<open>(\<forall>n>a. P n) \<longleftrightarrow> (\<forall>n\<in>{a<..}. P n)\<close>
-  by auto
-
-qualified lemma forall_lessThan_iff [code_unfold]:
-  \<open>(\<forall>n\<in>{..<b}. P n) \<longleftrightarrow> all_range P 0 b\<close>
-  by auto
-
-qualified lemma forall_less_iff [code_unfold]:
-  \<open>(\<forall>n<b. P n) \<longleftrightarrow> (\<forall>n\<in>{..<b}. P n)\<close>
-  by auto
-
-qualified lemma forall_atMost_iff [code_unfold]:
-  \<open>(\<forall>n\<in>{..b}. P n) \<longleftrightarrow> P b \<and> all_range P 0 b\<close>
-  by auto
-
-qualified lemma forall_less_eq_iff [code_unfold]:
-  \<open>(\<forall>n\<le>b. P n) \<longleftrightarrow> (\<forall>n\<in>{..b}. P n)\<close>
-  by auto
-
-qualified lemma forall_atLeastLessThan_iff [code_unfold]:
-  \<open>(\<forall>n\<in>{a..<b}. P n) \<longleftrightarrow> all_range P a b\<close>
-  by simp
-
-qualified lemma forall_atLeastAtMost_iff [code_unfold]:
-  \<open>(\<forall>n\<in>{a..b}. P n) \<longleftrightarrow> (if b = - 1 then (\<forall>n\<in>{a..}. P n) else all_range P a (b + 1))\<close>
-  apply auto
-   apply (metis atLeastAtMost_iff inc_le not_less_iff_gr_or_eq order_le_less)
-  apply (metis (no_types, lifting) antisym_conv2 atLeastLessThan_iff dual_order.trans inc_less_eq_triv_imp
-      nle_le)
-  done
-
-qualified lemma forall_greaterThanLessThan_iff [code_unfold]:
-  \<open>(\<forall>n\<in>{a<..<b}. P n) \<longleftrightarrow> a = - 1 \<or> all_range P (a + 1) b\<close>
-  by (auto simp add: inc_less_eq_iff)
-
-qualified lemma forall_greaterThanAtMost_iff [code_unfold]:
-  \<open>(\<forall>n\<in>{a<..b}. P n) \<longleftrightarrow> (if b = - 1 then (\<forall>n\<in>{a<..}. P n) else a = - 1 \<or> all_range P (a + 1) (b + 1))\<close>
-  apply auto
-   apply (metis greaterThanAtMost_iff inc_less_eq_iff linorder_not_less)
-  apply (meson atLeastLessThan_iff inc_less_eq_iff order_le_less_trans word_le_less_eq)
-  done
-
-qualified lemma exists_atLeast_iff [code_unfold]:
-  \<open>(\<exists>n\<in>{a..}. P n) \<longleftrightarrow> \<not> all_range (Not \<circ> P) a (- 1) \<or> P (- 1)\<close>
-  using forall_atLeast_iff [of a \<open>Not \<circ> P\<close>] by auto
-
-qualified lemma exists_greater_eq_iff [code_unfold]:
-  \<open>(\<exists>n\<ge>a. P n) \<longleftrightarrow> (\<exists>n\<in>{a..}. P n)\<close>
-  by auto
-
-qualified lemma exists_greaterThan_iff [code_unfold]:
-  \<open>(\<exists>n\<in>{a<..}. P n) \<longleftrightarrow> a \<noteq> - 1 \<and> (\<not> all_range (Not \<circ> P) (a + 1) (- 1) \<or> P (- 1))\<close>
-  using forall_greaterThan_iff [of a \<open>Not \<circ> P\<close>] by auto
-
-qualified lemma exists_greater_iff [code_unfold]:
-  \<open>(\<exists>n>a. P n) \<longleftrightarrow> (\<exists>n\<in>{a<..}. P n)\<close>
-  by auto
-
-qualified lemma exists_lessThan_iff [code_unfold]:
-  \<open>(\<exists>n\<in>{..<b}. P n) \<longleftrightarrow> \<not> all_range (Not \<circ> P) 0 b\<close>
-  using forall_lessThan_iff [of b \<open>Not \<circ> P\<close>] by auto
-
-qualified lemma exists_less_iff [code_unfold]:
-  \<open>(\<exists>n<b. P n) \<longleftrightarrow> (\<exists>n\<in>{..<b}. P n)\<close>
-  by auto
-
-qualified lemma exists_atMost_iff [code_unfold]:
-  \<open>(\<exists>n\<in>{..b}. P n) \<longleftrightarrow> P b \<or> \<not> all_range (Not \<circ> P) 0 b\<close>
-  using forall_atMost_iff [of b \<open>Not \<circ> P\<close>] by auto
-
-qualified lemma exists_less_eq_iff [code_unfold]:
-  \<open>(\<exists>n\<le>b. P n) \<longleftrightarrow> (\<exists>n\<in>{..b}. P n)\<close>
-  by auto
-
-qualified lemma exists_atLeastLessThan_iff [code_unfold]:
-  \<open>(\<exists>n\<in>{a..<b}. P n) \<longleftrightarrow> \<not> all_range (Not \<circ> P) a b\<close>
-  using forall_atLeastLessThan_iff [of a b \<open>Not \<circ> P\<close>] by simp
-
-qualified lemma exists_atLeastAtMost_iff [code_unfold]:
-  \<open>(\<exists>n\<in>{a..b}. P n) \<longleftrightarrow> (if b = - 1 then \<exists>n\<in>{a..}. P n else \<not> all_range (Not \<circ> P) a (b + 1))\<close>
-  using forall_atLeastAtMost_iff [of a b \<open>Not \<circ> P\<close>] by auto
-
-qualified lemma exists_greaterThanLessThan_iff [code_unfold]:
-  \<open>(\<exists>n\<in>{a<..<b}. P n) \<longleftrightarrow> a \<noteq> - 1 \<and> \<not> all_range (Not \<circ> P) (a + 1) b\<close>
-  using forall_greaterThanLessThan_iff [of a b \<open>Not \<circ> P\<close>] by auto
-
-qualified lemma exists_greaterThanAtMost_iff [code_unfold]:
-  \<open>(\<exists>n\<in>{a<..b}. P n) \<longleftrightarrow> (if b = - 1 then \<exists>n\<in>{a<..}. P n else a \<noteq> - 1 \<and> \<not> all_range (Not \<circ> P) (a + 1) (b + 1))\<close>
-  using forall_greaterThanAtMost_iff [of a b \<open>Not \<circ> P\<close>] by auto
-
-end
+subsection \<open>Executable intervals\<close>
+
+instance word :: (len) \<open>{interval_top, interval_bot}\<close>
+  by standard
+    (simp_all add: less_eq_dec_self_iff_eq inc_less_eq_self_iff_eq less_inc_imp_less_eq dec_less_imp_less_eq)
+
 
 subsection \<open>Tool support\<close>