--- a/src/HOL/Set_Interval.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Set_Interval.thy Mon Sep 23 13:32:38 2024 +0200
@@ -29,35 +29,35 @@
begin
definition
- lessThan :: "'a => 'a set" ("(1{..<_})") where
+ lessThan :: "'a => 'a set" (\<open>(1{..<_})\<close>) where
"{..<u} == {x. x < u}"
definition
- atMost :: "'a => 'a set" ("(1{.._})") where
+ atMost :: "'a => 'a set" (\<open>(1{.._})\<close>) where
"{..u} == {x. x \<le> u}"
definition
- greaterThan :: "'a => 'a set" ("(1{_<..})") where
+ greaterThan :: "'a => 'a set" (\<open>(1{_<..})\<close>) where
"{l<..} == {x. l<x}"
definition
- atLeast :: "'a => 'a set" ("(1{_..})") where
+ atLeast :: "'a => 'a set" (\<open>(1{_..})\<close>) where
"{l..} == {x. l\<le>x}"
definition
- greaterThanLessThan :: "'a => 'a => 'a set" ("(1{_<..<_})") where
+ greaterThanLessThan :: "'a => 'a => 'a set" (\<open>(1{_<..<_})\<close>) where
"{l<..<u} == {l<..} Int {..<u}"
definition
- atLeastLessThan :: "'a => 'a => 'a set" ("(1{_..<_})") where
+ atLeastLessThan :: "'a => 'a => 'a set" (\<open>(1{_..<_})\<close>) where
"{l..<u} == {l..} Int {..<u}"
definition
- greaterThanAtMost :: "'a => 'a => 'a set" ("(1{_<.._})") where
+ greaterThanAtMost :: "'a => 'a => 'a set" (\<open>(1{_<.._})\<close>) where
"{l<..u} == {l<..} Int {..u}"
definition
- atLeastAtMost :: "'a => 'a => 'a set" ("(1{_.._})") where
+ atLeastAtMost :: "'a => 'a => 'a set" (\<open>(1{_.._})\<close>) where
"{l..u} == {l..} Int {..u}"
end
@@ -67,22 +67,22 @@
\<^term>\<open>{m..<n}\<close> may not exist in \<^term>\<open>{..<n}\<close>-form as well.\<close>
syntax (ASCII)
- "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3UN _<=_./ _)" [0, 0, 10] 10)
- "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3UN _<_./ _)" [0, 0, 10] 10)
- "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3INT _<=_./ _)" [0, 0, 10] 10)
- "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3INT _<_./ _)" [0, 0, 10] 10)
+ "_UNION_le" :: "'a => 'a => 'b set => 'b set" (\<open>(3UN _<=_./ _)\<close> [0, 0, 10] 10)
+ "_UNION_less" :: "'a => 'a => 'b set => 'b set" (\<open>(3UN _<_./ _)\<close> [0, 0, 10] 10)
+ "_INTER_le" :: "'a => 'a => 'b set => 'b set" (\<open>(3INT _<=_./ _)\<close> [0, 0, 10] 10)
+ "_INTER_less" :: "'a => 'a => 'b set => 'b set" (\<open>(3INT _<_./ _)\<close> [0, 0, 10] 10)
syntax (latex output)
- "_UNION_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(\<open>unbreakable\<close>_ \<le> _)/ _)" [0, 0, 10] 10)
- "_UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(\<open>unbreakable\<close>_ < _)/ _)" [0, 0, 10] 10)
- "_INTER_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(\<open>unbreakable\<close>_ \<le> _)/ _)" [0, 0, 10] 10)
- "_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(\<open>unbreakable\<close>_ < _)/ _)" [0, 0, 10] 10)
+ "_UNION_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" (\<open>(3\<Union>(\<open>unbreakable\<close>_ \<le> _)/ _)\<close> [0, 0, 10] 10)
+ "_UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" (\<open>(3\<Union>(\<open>unbreakable\<close>_ < _)/ _)\<close> [0, 0, 10] 10)
+ "_INTER_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" (\<open>(3\<Inter>(\<open>unbreakable\<close>_ \<le> _)/ _)\<close> [0, 0, 10] 10)
+ "_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" (\<open>(3\<Inter>(\<open>unbreakable\<close>_ < _)/ _)\<close> [0, 0, 10] 10)
syntax
- "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Union>_\<le>_./ _)" [0, 0, 10] 10)
- "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Union>_<_./ _)" [0, 0, 10] 10)
- "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter>_\<le>_./ _)" [0, 0, 10] 10)
- "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter>_<_./ _)" [0, 0, 10] 10)
+ "_UNION_le" :: "'a => 'a => 'b set => 'b set" (\<open>(3\<Union>_\<le>_./ _)\<close> [0, 0, 10] 10)
+ "_UNION_less" :: "'a => 'a => 'b set => 'b set" (\<open>(3\<Union>_<_./ _)\<close> [0, 0, 10] 10)
+ "_INTER_le" :: "'a => 'a => 'b set => 'b set" (\<open>(3\<Inter>_\<le>_./ _)\<close> [0, 0, 10] 10)
+ "_INTER_less" :: "'a => 'a => 'b set => 'b set" (\<open>(3\<Inter>_<_./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_UNION_le" "_UNION_less" \<rightleftharpoons> Union and
@@ -1988,26 +1988,26 @@
subsection \<open>Summation indexed over intervals\<close>
syntax (ASCII)
- "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)
- "_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)
- "_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<_./ _)" [0,0,10] 10)
- "_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<=_./ _)" [0,0,10] 10)
+ "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(SUM _ = _.._./ _)\<close> [0,0,0,10] 10)
+ "_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(SUM _ = _..<_./ _)\<close> [0,0,0,10] 10)
+ "_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(SUM _<_./ _)\<close> [0,0,10] 10)
+ "_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(SUM _<=_./ _)\<close> [0,0,10] 10)
syntax (latex_sum output)
"_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^latex>\<open>$\\sum_{\<close>_ = _\<^latex>\<open>}^{\<close>_\<^latex>\<open>}$\<close> _)" [0,0,0,10] 10)
+ (\<open>(3\<^latex>\<open>$\sum_{\<close>_ = _\<^latex>\<open>}^{\<close>_\<^latex>\<open>}$\<close> _)\<close> [0,0,0,10] 10)
"_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^latex>\<open>$\\sum_{\<close>_ = _\<^latex>\<open>}^{<\<close>_\<^latex>\<open>}$\<close> _)" [0,0,0,10] 10)
+ (\<open>(3\<^latex>\<open>$\sum_{\<close>_ = _\<^latex>\<open>}^{<\<close>_\<^latex>\<open>}$\<close> _)\<close> [0,0,0,10] 10)
"_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^latex>\<open>$\\sum_{\<close>_ < _\<^latex>\<open>}$\<close> _)" [0,0,10] 10)
+ (\<open>(3\<^latex>\<open>$\sum_{\<close>_ < _\<^latex>\<open>}$\<close> _)\<close> [0,0,10] 10)
"_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^latex>\<open>$\\sum_{\<close>_ \<le> _\<^latex>\<open>}$\<close> _)" [0,0,10] 10)
+ (\<open>(3\<^latex>\<open>$\sum_{\<close>_ \<le> _\<^latex>\<open>}$\<close> _)\<close> [0,0,10] 10)
syntax
- "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
- "_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10)
- "_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10)
- "_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10)
+ "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Sum>_ = _.._./ _)\<close> [0,0,0,10] 10)
+ "_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Sum>_ = _..<_./ _)\<close> [0,0,0,10] 10)
+ "_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Sum>_<_./ _)\<close> [0,0,10] 10)
+ "_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Sum>_\<le>_./ _)\<close> [0,0,10] 10)
syntax_consts
"_from_to_sum" "_from_upto_sum" "_upt_sum" "_upto_sum" == sum
@@ -2681,26 +2681,26 @@
subsection \<open>Products indexed over intervals\<close>
syntax (ASCII)
- "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10)
- "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10)
- "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _<_./ _)" [0,0,10] 10)
- "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _<=_./ _)" [0,0,10] 10)
+ "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(PROD _ = _.._./ _)\<close> [0,0,0,10] 10)
+ "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(PROD _ = _..<_./ _)\<close> [0,0,0,10] 10)
+ "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(PROD _<_./ _)\<close> [0,0,10] 10)
+ "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(PROD _<=_./ _)\<close> [0,0,10] 10)
syntax (latex_prod output)
"_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^latex>\<open>$\\prod_{\<close>_ = _\<^latex>\<open>}^{\<close>_\<^latex>\<open>}$\<close> _)" [0,0,0,10] 10)
+ (\<open>(3\<^latex>\<open>$\prod_{\<close>_ = _\<^latex>\<open>}^{\<close>_\<^latex>\<open>}$\<close> _)\<close> [0,0,0,10] 10)
"_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^latex>\<open>$\\prod_{\<close>_ = _\<^latex>\<open>}^{<\<close>_\<^latex>\<open>}$\<close> _)" [0,0,0,10] 10)
+ (\<open>(3\<^latex>\<open>$\prod_{\<close>_ = _\<^latex>\<open>}^{<\<close>_\<^latex>\<open>}$\<close> _)\<close> [0,0,0,10] 10)
"_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^latex>\<open>$\\prod_{\<close>_ < _\<^latex>\<open>}$\<close> _)" [0,0,10] 10)
+ (\<open>(3\<^latex>\<open>$\prod_{\<close>_ < _\<^latex>\<open>}$\<close> _)\<close> [0,0,10] 10)
"_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^latex>\<open>$\\prod_{\<close>_ \<le> _\<^latex>\<open>}$\<close> _)" [0,0,10] 10)
+ (\<open>(3\<^latex>\<open>$\prod_{\<close>_ \<le> _\<^latex>\<open>}$\<close> _)\<close> [0,0,10] 10)
syntax
- "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10)
- "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10)
- "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_<_./ _)" [0,0,10] 10)
- "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10)
+ "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Prod>_ = _.._./ _)\<close> [0,0,0,10] 10)
+ "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Prod>_ = _..<_./ _)\<close> [0,0,0,10] 10)
+ "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Prod>_<_./ _)\<close> [0,0,10] 10)
+ "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Prod>_\<le>_./ _)\<close> [0,0,10] 10)
syntax_consts
"_from_to_prod" "_from_upto_prod" "_upt_prod" "_upto_prod" \<rightleftharpoons> prod