--- a/src/HOL/Set_Interval.thy Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Set_Interval.thy Mon Sep 23 21:09:23 2024 +0200
@@ -29,35 +29,35 @@
begin
definition
- lessThan :: "'a => 'a set" (\<open>(1{..<_})\<close>) where
+ lessThan :: "'a => 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{..<_})\<close>) where
"{..<u} == {x. x < u}"
definition
- atMost :: "'a => 'a set" (\<open>(1{.._})\<close>) where
+ atMost :: "'a => 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{.._})\<close>) where
"{..u} == {x. x \<le> u}"
definition
- greaterThan :: "'a => 'a set" (\<open>(1{_<..})\<close>) where
+ greaterThan :: "'a => 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{_<..})\<close>) where
"{l<..} == {x. l<x}"
definition
- atLeast :: "'a => 'a set" (\<open>(1{_..})\<close>) where
+ atLeast :: "'a => 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{_..})\<close>) where
"{l..} == {x. l\<le>x}"
definition
- greaterThanLessThan :: "'a => 'a => 'a set" (\<open>(1{_<..<_})\<close>) where
+ greaterThanLessThan :: "'a => 'a => 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{_<..<_})\<close>) where
"{l<..<u} == {l<..} Int {..<u}"
definition
- atLeastLessThan :: "'a => 'a => 'a set" (\<open>(1{_..<_})\<close>) where
+ atLeastLessThan :: "'a => 'a => 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{_..<_})\<close>) where
"{l..<u} == {l..} Int {..<u}"
definition
- greaterThanAtMost :: "'a => 'a => 'a set" (\<open>(1{_<.._})\<close>) where
+ greaterThanAtMost :: "'a => 'a => 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{_<.._})\<close>) where
"{l<..u} == {l<..} Int {..u}"
definition
- atLeastAtMost :: "'a => 'a => 'a set" (\<open>(1{_.._})\<close>) where
+ atLeastAtMost :: "'a => 'a => 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set interval\<close>\<close>{_.._})\<close>) where
"{l..u} == {l..} Int {..u}"
end
@@ -67,10 +67,10 @@
\<^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" (\<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)
+ "_UNION_le" :: "'a => 'a => 'b set => 'b set" (\<open>(\<open>indent=3 notation=\<open>binder UN\<close>\<close>UN _<=_./ _)\<close> [0, 0, 10] 10)
+ "_UNION_less" :: "'a => 'a => 'b set => 'b set" (\<open>(\<open>indent=3 notation=\<open>binder UN\<close>\<close>UN _<_./ _)\<close> [0, 0, 10] 10)
+ "_INTER_le" :: "'a => 'a => 'b set => 'b set" (\<open>(\<open>indent=3 notation=\<open>binder INT\<close>\<close>INT _<=_./ _)\<close> [0, 0, 10] 10)
+ "_INTER_less" :: "'a => 'a => 'b set => 'b set" (\<open>(\<open>indent=3 notation=\<open>binder INT\<close>\<close>INT _<_./ _)\<close> [0, 0, 10] 10)
syntax (latex output)
"_UNION_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" (\<open>(3\<Union>(\<open>unbreakable\<close>_ \<le> _)/ _)\<close> [0, 0, 10] 10)
@@ -79,10 +79,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" (\<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)
+ "_UNION_le" :: "'a => 'a => 'b set => 'b set" (\<open>(\<open>indent=3 notation=\<open>binder \<Union>\<close>\<close>\<Union>_\<le>_./ _)\<close> [0, 0, 10] 10)
+ "_UNION_less" :: "'a => 'a => 'b set => 'b set" (\<open>(\<open>indent=3 notation=\<open>binder \<Union>\<close>\<close>\<Union>_<_./ _)\<close> [0, 0, 10] 10)
+ "_INTER_le" :: "'a => 'a => 'b set => 'b set" (\<open>(\<open>indent=3 notation=\<open>binder \<Inter>\<close>\<close>\<Inter>_\<le>_./ _)\<close> [0, 0, 10] 10)
+ "_INTER_less" :: "'a => 'a => 'b set => 'b set" (\<open>(\<open>indent=3 notation=\<open>binder \<Inter>\<close>\<close>\<Inter>_<_./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_UNION_le" "_UNION_less" \<rightleftharpoons> Union and
@@ -1988,10 +1988,10 @@
subsection \<open>Summation indexed over intervals\<close>
syntax (ASCII)
- "_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)
+ "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>notation=\<open>binder SUM\<close>\<close>SUM _ = _.._./ _)\<close> [0,0,0,10] 10)
+ "_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>notation=\<open>binder SUM\<close>\<close>SUM _ = _..<_./ _)\<close> [0,0,0,10] 10)
+ "_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>notation=\<open>binder SUM\<close>\<close>SUM _<_./ _)\<close> [0,0,10] 10)
+ "_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>notation=\<open>binder SUM\<close>\<close>SUM _<=_./ _)\<close> [0,0,10] 10)
syntax (latex_sum output)
"_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
@@ -2004,10 +2004,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" (\<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)
+ "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Sum>\<close>\<close>\<Sum>_ = _.._./ _)\<close> [0,0,0,10] 10)
+ "_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Sum>\<close>\<close>\<Sum>_ = _..<_./ _)\<close> [0,0,0,10] 10)
+ "_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Sum>\<close>\<close>\<Sum>_<_./ _)\<close> [0,0,10] 10)
+ "_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Sum>\<close>\<close>\<Sum>_\<le>_./ _)\<close> [0,0,10] 10)
syntax_consts
"_from_to_sum" "_from_upto_sum" "_upt_sum" "_upto_sum" == sum
@@ -2681,10 +2681,10 @@
subsection \<open>Products indexed over intervals\<close>
syntax (ASCII)
- "_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)
+ "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>notation=\<open>binder PROD\<close>\<close>PROD _ = _.._./ _)\<close> [0,0,0,10] 10)
+ "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>notation=\<open>binder PROD\<close>\<close>PROD _ = _..<_./ _)\<close> [0,0,0,10] 10)
+ "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>notation=\<open>binder PROD\<close>\<close>PROD _<_./ _)\<close> [0,0,10] 10)
+ "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>notation=\<open>binder PROD\<close>\<close>PROD _<=_./ _)\<close> [0,0,10] 10)
syntax (latex_prod output)
"_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
@@ -2697,10 +2697,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" (\<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)
+ "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>_ = _.._./ _)\<close> [0,0,0,10] 10)
+ "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>_ = _..<_./ _)\<close> [0,0,0,10] 10)
+ "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>_<_./ _)\<close> [0,0,10] 10)
+ "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>_\<le>_./ _)\<close> [0,0,10] 10)
syntax_consts
"_from_to_prod" "_from_upto_prod" "_upt_prod" "_upto_prod" \<rightleftharpoons> prod