--- a/NEWS Sun Nov 02 20:01:43 2025 +0100
+++ b/NEWS Sun Nov 02 20:36:24 2025 +0100
@@ -144,7 +144,7 @@
thm null_def ~> List.null_iff [simp]
const List.all_interval_nat List.all_interval_int
- discontinued in favour of a generic List.all_range
+ discontinued in favour of a generic List.all_interval
const List.Bleast
discontinued in favour of more concise Lattices_Big.Least
--- a/src/HOL/Groups_List.thy Sun Nov 02 20:01:43 2025 +0100
+++ b/src/HOL/Groups_List.thy Sun Nov 02 20:36:24 2025 +0100
@@ -57,22 +57,30 @@
finally show ?thesis .
qed
+lemma atLeastAtMost_conv_list [code_unfold]:
+ \<open>set.F g {a..b} = list.F (map g (List.interval a b))\<close>
+ by (simp flip: List.set_interval_eq add: distinct_set_conv_list)
+
lemma atLeastLessThan_conv_list [code_unfold]:
- \<open>set.F g {a..<b} = list.F (map g (List.range a b))\<close>
- using List.atLeastLessThan_eq_range
- by (simp flip: List.set_range_eq add: distinct_set_conv_list)
+ \<open>set.F g {a..<b} = (let d = b - 1 in if d < b
+ then list.F (map g (List.interval a d))
+ else \<^bold>1)\<close>
+ using List.atLeastLessThan_eq_interval [of a b]
+ by (simp flip: List.set_interval_eq add: distinct_set_conv_list Let_def)
-lemma atLeastAtMost_conv_list [code_unfold]:
- \<open>set.F g {a..b} = list.F (map g (List.range a (b + 1)))\<close>
- by (simp flip: List.set_range_eq add: List.atLeastAtMost_eq_range distinct_set_conv_list)
+lemma greaterThanAtMost_conv_list [code_unfold]:
+ \<open>set.F g {a<..b} = (let c = a + 1 in if a < c
+ then list.F (map g (List.interval c b))
+ else \<^bold>1)\<close>
+ using List.greaterThanAtMost_eq_interval [of a b]
+ by (simp flip: List.set_interval_eq add: distinct_set_conv_list Let_def)
lemma greaterThanLessThan_conv_list [code_unfold]:
- \<open>set.F g {a<..<b} = list.F (map g (List.range (a + 1) b))\<close>
- by (simp flip: List.set_range_eq add: List.greaterThanLessThan_eq_range distinct_set_conv_list)
-
-lemma greaterThanAtMost_conv_list [code_unfold]:
- \<open>set.F g {a<..b} = list.F (map g (List.range (a + 1) (b + 1)))\<close>
- by (simp flip: List.set_range_eq add: List.greaterThanAtMost_eq_range distinct_set_conv_list)
+ \<open>set.F g {a<..<b} = (let c = a + 1; d = b - 1 in if a < c \<and> d < b
+ then list.F (map g (List.interval (a + 1) (b - 1)))
+ else \<^bold>1)\<close>
+ using List.greaterThanLessThan_eq_interval [of a b]
+ by (simp flip: List.set_interval_eq add: distinct_set_conv_list Let_def)
end
--- 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>
--- a/src/HOL/List.thy Sun Nov 02 20:01:43 2025 +0100
+++ b/src/HOL/List.thy Sun Nov 02 20:36:24 2025 +0100
@@ -8226,129 +8226,214 @@
by (simp_all add: add: lexordp_def)
-text \<open>Executable ranges\<close>
-
-class discrete_linordered_semidom_with_range = discrete_linordered_semidom +
- assumes finite_atLeastLessThan: \<open>finite {a..<b}\<close>
+text \<open>Executable intervals\<close>
+
+context preorder
+begin
+
+lemma forall_less_eq_iff [code_unfold]:
+ \<open>(\<forall>n\<le>b. P n) \<longleftrightarrow> (\<forall>n\<in>{..b}. P n)\<close>
+ by auto
+
+lemma exists_less_eq_iff [code_unfold]:
+ \<open>(\<exists>n\<le>b. P n) \<longleftrightarrow> (\<exists>n\<in>{..b}. P n)\<close>
+ by auto
+
+lemma forall_less_iff [code_unfold]:
+ \<open>(\<forall>n<b. P n) \<longleftrightarrow> (\<forall>n\<in>{..<b}. P n)\<close>
+ by auto
+
+lemma exists_less_iff [code_unfold]:
+ \<open>(\<exists>n<b. P n) \<longleftrightarrow> (\<exists>n\<in>{..<b}. P n)\<close>
+ by auto
+
+lemma forall_greater_eq_iff [code_unfold]:
+ \<open>(\<forall>n\<ge>a. P n) \<longleftrightarrow> (\<forall>n\<in>{a..}. P n)\<close>
+ by auto
+
+lemma exists_greater_eq_iff [code_unfold]:
+ \<open>(\<exists>n\<ge>a. P n) \<longleftrightarrow> (\<exists>n\<in>{a..}. P n)\<close>
+ by auto
+
+lemma forall_greater_iff [code_unfold]:
+ \<open>(\<forall>n>a. P n) \<longleftrightarrow> (\<forall>n\<in>{a<..}. P n)\<close>
+ by auto
+
+lemma exists_greater_iff [code_unfold]:
+ \<open>(\<exists>n>a. P n) \<longleftrightarrow> (\<exists>n\<in>{a<..}. P n)\<close>
+ by auto
+
+end
+
+class interval = linorder + comm_semiring_1_cancel +
+ assumes finite_atLeastAtMost: \<open>finite {a..b}\<close>
+ assumes dec_less_imp_less_eq: \<open>a - 1 < b \<Longrightarrow> a \<le> b\<close>
+ assumes less_inc_imp_less_eq: \<open>a < b + 1 \<Longrightarrow> a \<le> b\<close>
+ assumes dec_greater_eq_self_imp_bot: \<open>a \<le> a - 1 \<Longrightarrow> a \<le> c\<close>
+ assumes inc_less_eq_self_imp_top: \<open>b + 1 \<le> b \<Longrightarrow> d \<le> b\<close>
begin
context
begin
-qualified definition range :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a 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>
- by (auto simp flip: less_iff_succ_less_eq less_eq_iff_succ_less)
- then show ?thesis
- by (auto simp add: range_eq finite_atLeastLessThan intro!: insort_is_Cons)
-next
- case False
- then show ?thesis
- by (simp add: range_eq)
-qed
-
-qualified lemma atLeastLessThan_eq_range [code]:
- \<open>{a..<b} = set (range a b)\<close>
+qualified lemma less_imp_less_eq_dec:
+ \<open>c < b \<Longrightarrow> a < b \<Longrightarrow> a \<le> b - 1\<close>
+ using local.dec_less_imp_less_eq local.not_less by blast
+
+qualified lemma less_imp_in_less_eq:
+ \<open>a < c \<Longrightarrow> a < b \<Longrightarrow> a + 1 \<le> b\<close>
+ using local.less_inc_imp_less_eq local.not_less by blast
+
+qualified lemma less_eq_dec_imp_less:
+ \<open>c < b \<Longrightarrow> a \<le> b - 1 \<Longrightarrow> a < b\<close>
+ using local.dec_greater_eq_self_imp_bot local.dual_order.trans local.not_le by blast
+
+qualified lemma inc_less_eq_imp_less:
+ \<open>a < c \<Longrightarrow> a + 1 \<le> b \<Longrightarrow> a < b\<close>
+ using local.inc_less_eq_self_imp_top local.not_le local.order.strict_trans2 by blast
+
+qualified definition interval :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a list\<close> \<comment> \<open>only for code generation\<close>
+ where interval_eq: \<open>interval a b = sorted_list_of_set {a..b}\<close>
+
+qualified lemma set_interval_eq [simp]:
+ \<open>set (interval a b) = {a..b}\<close>
+ using finite_atLeastAtMost [of a b] by (simp add: interval_eq)
+
+qualified lemma distinct_interval [simp]:
+ \<open>distinct (interval a b)\<close>
+ by (simp add: interval_eq)
+
+qualified lemma interval_code [code]:
+ \<open>interval a b = (if a < b then a # interval (a + 1) b else if a = b then [a] else [])\<close>
+proof -
+ consider (less) \<open>a < b\<close> | (eq) \<open>a = b\<close> | (greater) \<open>a > b\<close>
+ using less_linear by blast
+ then show ?thesis proof cases
+ case less
+ then have \<open>{a..b} = insert a {a + 1..b}\<close>
+ by (auto simp add: not_le dest: less_imp_le local.inc_less_eq_imp_less dest!: less_inc_imp_less_eq)
+ moreover have \<open>{a + 1..b} - {a} = {a + 1..b}\<close>
+ using less by (auto dest: local.inc_less_eq_imp_less)
+ moreover have \<open>insort a (sorted_list_of_set {a + 1..b}) = a # sorted_list_of_set {a + 1..b}\<close>
+ using finite_atLeastAtMost [of \<open>a + 1\<close> b] less
+ by (auto intro!: insort_is_Cons dest: local.inc_less_eq_imp_less less_imp_le)
+ ultimately show ?thesis
+ using less finite_atLeastAtMost [of \<open>a + 1\<close> b]
+ by (simp add: interval_eq)
+ next
+ case eq
+ then show ?thesis
+ by (simp add: interval_eq)
+ next
+ case greater
+ then show ?thesis
+ by (auto simp add: interval_eq)
+ qed
+qed
+
+qualified lemma atLeastAtMost_eq_interval [code]:
+ \<open>{a..b} = set (interval a b)\<close>
by simp
-qualified lemma atLeastAtMost_eq_range [code]:
- \<open>{a..b} = set (range a (b + 1))\<close>
- by (auto simp flip: less_eq_iff_succ_less)
-
-qualified lemma greaterThanLessThan_eq_range [code]:
- \<open>{a<..<b} = set (range (a + 1) b)\<close>
- by (auto simp add: less_eq_iff_succ_less)
-
-qualified lemma greaterThanAtMost_eq_range [code]:
- \<open>{a<..b} = set (range (a + 1) (b + 1))\<close>
- by (auto simp add: less_eq_iff_succ_less)
-
-qualified definition all_range :: \<open>('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<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>
- by (auto simp add: Ball_def simp flip: less_iff_succ_less_eq)
- (auto simp add: le_less)
-
-lemma forall_atLeastAtMost_iff [code_unfold]:
- \<open>(\<forall>n\<in>{a..b}. P n) \<longleftrightarrow> all_range P a (b + 1)\<close>
- by (simp add: atLeastAtMost_eq_range)
-
-lemma forall_greaterThanLessThan_iff [code_unfold]:
- \<open>(\<forall>n\<in>{a<..<b}. P n) \<longleftrightarrow> all_range P (a + 1) b\<close>
- by (simp add: greaterThanLessThan_eq_range)
-
-lemma forall_greaterThanAtMost_iff [code_unfold]:
- \<open>(\<forall>n\<in>{a<..b}. P n) \<longleftrightarrow> all_range P (a + 1) (b + 1)\<close>
- by (simp add: greaterThanAtMost_eq_range)
-
-lemma exists_atLeastLessThan [code_unfold]:
- \<open>(\<exists>n\<in>{a..<b}. P n) \<longleftrightarrow> \<not> all_range (Not \<circ> P) a b\<close>
+qualified lemma atLeastLessThan_eq_interval [code]:
+ \<open>{a..<b} = (let d = b - 1 in if d < b then set (interval a d) else {})\<close>
+ by (auto simp add: Let_def not_less local.less_imp_less_eq_dec intro: dec_greater_eq_self_imp_bot)
+
+qualified lemma greaterThanAtMost_eq_interval [code]:
+ \<open>{a<..b} = (let c = a + 1 in if a < c then set (interval c b) else {})\<close>
+ by (auto simp add: Let_def not_less dec_less_imp_less_eq intro: inc_less_eq_self_imp_top)
+
+qualified lemma greaterThanLessThan_eq_interval [code]:
+ \<open>{a<..<b} = (let c = a + 1; d = b - 1 in if a < c \<and> d < b then set (interval c d) else {})\<close>
+ by (auto simp add: Let_def not_less dec_less_imp_less_eq
+ dest: local.less_imp_less_eq_dec local.inc_less_eq_imp_less local.less_eq_dec_imp_less)
+
+qualified definition all_interval :: \<open>('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool\<close> \<comment> \<open>only for code generation\<close>
+ where all_interval_iff [code_post, simp]: \<open>all_interval P a b \<longleftrightarrow> (\<forall>n\<in>{a..b}. P n)\<close>
+
+qualified lemma all_interval_code [code]:
+ \<open>all_interval P a b \<longleftrightarrow> ((a < b \<longrightarrow> P a \<and> all_interval P (a + 1) b) \<and> (a = b \<longrightarrow> P a))\<close>
+ by (simp only: all_interval_iff interval_code [of a b] flip: set_interval_eq) auto
+
+qualified lemma forall_atLeastAtMost_iff [code_unfold]:
+ \<open>(\<forall>n\<in>{a..b}. P n) \<longleftrightarrow> all_interval P a b\<close>
by simp
-lemma exists_atLeastAtMost_iff [code_unfold]:
- \<open>(\<exists>n\<in>{a..b}. P n) \<longleftrightarrow> \<not> all_range (Not \<circ> P) a (b + 1)\<close>
- by (simp add: atLeastAtMost_eq_range)
-
-lemma exists_greaterThanLessThan_iff [code_unfold]:
- \<open>(\<exists>n\<in>{a<..<b}. P n) \<longleftrightarrow> \<not> all_range (Not \<circ> P) (a + 1) b\<close>
- by (simp add: greaterThanLessThan_eq_range)
-
-lemma exists_greaterThanAtMost_iff [code_unfold]:
- \<open>(\<exists>n\<in>{a<..b}. P n) \<longleftrightarrow> \<not> all_range (Not \<circ> P) (a + 1) (b + 1)\<close>
- by (simp add: greaterThanAtMost_eq_range)
+qualified lemma exists_atLeastAtMost_iff [code_unfold]:
+ \<open>(\<exists>n\<in>{a..b}. P n) \<longleftrightarrow> \<not> all_interval (Not \<circ> P) a b\<close>
+ using forall_atLeastAtMost_iff [of a b \<open>Not \<circ> P\<close>] by simp
+
+qualified lemma forall_atLeastLessThan_iff [code_unfold]:
+ \<open>(\<forall>n\<in>{a..<b}. P n) \<longleftrightarrow> (let d = b - 1 in d < b \<longrightarrow> all_interval P a d)\<close>
+ by (auto simp add: not_less Let_def intro: local.less_eq_dec_imp_less local.less_imp_less_eq_dec elim!: bspec)
+
+qualified lemma exists_atLeastLessThan_iff [code_unfold]:
+ \<open>(\<exists>n\<in>{a..<b}. P n) \<longleftrightarrow> (let d = b - 1 in d < b \<and> \<not> all_interval (Not \<circ> P) a d)\<close>
+ using forall_atLeastLessThan_iff [of a b \<open>Not \<circ> P\<close>] by (auto simp add: Let_def)
+
+qualified lemma forall_greaterThanAtMost_iff [code_unfold]:
+ \<open>(\<forall>n\<in>{a<..b}. P n) \<longleftrightarrow> (let c = a + 1 in a < c \<longrightarrow> all_interval P c b)\<close>
+ by (auto simp add: Let_def not_less intro: local.less_imp_in_less_eq local.inc_less_eq_imp_less elim!: bspec)
+
+qualified lemma exists_greaterThanAtMost_iff [code_unfold]:
+ \<open>(\<exists>n\<in>{a<..b}. P n) \<longleftrightarrow> (let c = a + 1 in a < c \<and> \<not> all_interval (Not \<circ> P) c b)\<close>
+ using forall_greaterThanAtMost_iff [of a b \<open>Not \<circ> P\<close>] by (auto simp add: Let_def)
+
+qualified lemma forall_greaterThanLessThan_iff [code_unfold]:
+ \<open>(\<forall>n\<in>{a<..<b}. P n) \<longleftrightarrow> (let c = a + 1; d = b - 1 in a < c \<longrightarrow> d < b \<longrightarrow> all_interval P c d)\<close>
+ by (auto simp add: Let_def not_less local.less_imp_in_less_eq local.less_imp_less_eq_dec
+ intro: local.inc_less_eq_imp_less local.less_eq_dec_imp_less elim!: bspec)
+
+qualified lemma exists_greaterThanLessThan_iff [code_unfold]:
+ \<open>(\<exists>n\<in>{a<..<b}. P n) \<longleftrightarrow> (let c = a + 1; d = b - 1 in a < c \<and> d < b \<and> \<not> all_interval (Not \<circ> P) c d)\<close>
+ using forall_greaterThanLessThan_iff [of a b \<open>Not \<circ> P\<close>] by (auto simp add: Let_def)
end
end
-instance nat :: discrete_linordered_semidom_with_range
- by standard auto
-
-instance int :: discrete_linordered_semidom_with_range
- by standard auto
-
-lemma all_nat_less_eq [code_unfold]:
- "(\<forall>m<n. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)" for n :: nat
+class interval_top = interval + order_top
+begin
+
+lemma atLeast_eq_atLeastAtMost_top [code, code_unfold]:
+ \<open>{a..} = {a..top}\<close>
+ by auto
+
+lemma greaterThan_eq_greaterThanAtMost_top [code, code_unfold]:
+ \<open>{a<..} = {a<..top}\<close>
by auto
-lemma all_nat_less [code_unfold]:
- "(\<forall>m\<le>n. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)" for n :: nat
+end
+
+class interval_bot = interval + order_bot
+begin
+
+lemma atMost_eq_atLeastAtMost_bot [code, code_unfold]:
+ \<open>{..b} = {bot..b}\<close>
by auto
-lemma ex_nat_less_eq [code_unfold]:
- "(\<exists>m<n. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)" for n :: nat
+lemma lessThan_eq_atLeastLessThan_bot [code, code_unfold]:
+ \<open>{..<b} = {bot..<b}\<close>
by auto
-lemma ex_nat_less [code_unfold]:
- "(\<exists>m\<le>n. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)" for n :: nat
- by auto
+end
+
+instance nat :: interval_bot
+ by standard simp_all
+
+instance int :: interval
+ by standard simp_all
context
begin
-qualified lemma range_eq_upt [simp]:
- \<open>List.range m n = [m..<n]\<close>
- by (simp add: List.range_eq)
-
-qualified lemma range_eq_upto [simp]:
- \<open>List.range i k = [i..k - 1]\<close>
- using atLeastLessThanPlusOne_atLeastAtMost_int [of i \<open>k - 1\<close>]
- by (simp add: List.range_eq)
+qualified lemma interval_eq_upt [simp]:
+ \<open>List.interval m n = [m..<Suc n]\<close>
+ by (simp add: List.interval_eq flip: atLeastLessThanSuc_atLeastAtMost)
+
+qualified lemma interval_eq_upto [simp]:
+ \<open>List.interval i k = [i..k]\<close>
+ by (simp add: List.interval_eq)
end