--- a/src/HOL/Library/Multiset.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Multiset.thy Wed Oct 09 23:38:29 2024 +0200
@@ -133,22 +133,22 @@
notation
member_mset (\<open>'(\<in>#')\<close>) and
- member_mset (\<open>(_/ \<in># _)\<close> [50, 51] 50)
+ member_mset (\<open>(\<open>notation=\<open>infix \<in>#\<close>\<close>_/ \<in># _)\<close> [50, 51] 50)
notation (ASCII)
member_mset (\<open>'(:#')\<close>) and
- member_mset (\<open>(_/ :# _)\<close> [50, 51] 50)
+ member_mset (\<open>(\<open>notation=\<open>infix :#\<close>\<close>_/ :# _)\<close> [50, 51] 50)
abbreviation not_member_mset :: \<open>'a \<Rightarrow> 'a multiset \<Rightarrow> bool\<close>
where \<open>not_member_mset a M \<equiv> a \<notin> set_mset M\<close>
notation
not_member_mset (\<open>'(\<notin>#')\<close>) and
- not_member_mset (\<open>(_/ \<notin># _)\<close> [50, 51] 50)
+ not_member_mset (\<open>(\<open>notation=\<open>infix \<notin>#\<close>\<close>_/ \<notin># _)\<close> [50, 51] 50)
notation (ASCII)
not_member_mset (\<open>'(~:#')\<close>) and
- not_member_mset (\<open>(_/ ~:# _)\<close> [50, 51] 50)
+ not_member_mset (\<open>(\<open>notation=\<open>infix ~:#\<close>\<close>_/ ~:# _)\<close> [50, 51] 50)
context
begin
@@ -162,17 +162,18 @@
end
syntax
- "_MBall" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3\<forall>_\<in>#_./ _)\<close> [0, 0, 10] 10)
- "_MBex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3\<exists>_\<in>#_./ _)\<close> [0, 0, 10] 10)
-
+ "_MBall" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"
+ (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<close>\<close>\<forall>_\<in>#_./ _)\<close> [0, 0, 10] 10)
+ "_MBex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"
+ (\<open>(\<open>indent=3 notation=\<open>binder \<exists>\<close>\<close>\<exists>_\<in>#_./ _)\<close> [0, 0, 10] 10)
syntax (ASCII)
- "_MBall" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3\<forall>_:#_./ _)\<close> [0, 0, 10] 10)
- "_MBex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3\<exists>_:#_./ _)\<close> [0, 0, 10] 10)
-
+ "_MBall" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"
+ (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<close>\<close>\<forall>_:#_./ _)\<close> [0, 0, 10] 10)
+ "_MBex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"
+ (\<open>(\<open>indent=3 notation=\<open>binder \<exists>\<close>\<close>\<exists>_:#_./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_MBall" \<rightleftharpoons> Multiset.Ball and
"_MBex" \<rightleftharpoons> Multiset.Bex
-
translations
"\<forall>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Ball A (\<lambda>x. P)"
"\<exists>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Bex A (\<lambda>x. P)"
@@ -1249,9 +1250,11 @@
by (rule filter_preserves_multiset)
syntax (ASCII)
- "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" (\<open>(1{#_ :# _./ _#})\<close>)
+ "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
+ (\<open>(\<open>indent=1 notation=\<open>mixfix multiset comprehension\<close>\<close>{#_ :# _./ _#})\<close>)
syntax
- "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" (\<open>(1{#_ \<in># _./ _#})\<close>)
+ "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
+ (\<open>(\<open>indent=1 notation=\<open>mixfix multiset comprehension\<close>\<close>{#_ \<in># _./ _#})\<close>)
syntax_consts
"_MCollect" == filter_mset
translations
@@ -1824,18 +1827,22 @@
image_mset_subseteq_mono subset_mset.less_le_not_le)
syntax (ASCII)
- "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset" (\<open>({#_/. _ :# _#})\<close>)
+ "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
+ (\<open>(\<open>notation=\<open>mixfix multiset comprehension\<close>\<close>{#_/. _ :# _#})\<close>)
syntax
- "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset" (\<open>({#_/. _ \<in># _#})\<close>)
+ "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
+ (\<open>(\<open>notation=\<open>mixfix multiset comprehension\<close>\<close>{#_/. _ \<in># _#})\<close>)
syntax_consts
"_comprehension_mset" \<rightleftharpoons> image_mset
translations
"{#e. x \<in># M#}" \<rightleftharpoons> "CONST image_mset (\<lambda>x. e) M"
syntax (ASCII)
- "_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" (\<open>({#_/ | _ :# _./ _#})\<close>)
+ "_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
+ (\<open>(\<open>notation=\<open>mixfix multiset comprehension\<close>\<close>{#_/ | _ :# _./ _#})\<close>)
syntax
- "_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" (\<open>({#_/ | _ \<in># _./ _#})\<close>)
+ "_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
+ (\<open>(\<open>notation=\<open>mixfix multiset comprehension\<close>\<close>{#_/ | _ \<in># _./ _#})\<close>)
syntax_consts
"_comprehension_mset'" \<rightleftharpoons> image_mset
translations
@@ -2682,9 +2689,11 @@
notation sum_mset (\<open>\<Sum>\<^sub>#\<close>)
syntax (ASCII)
- "_sum_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" (\<open>(3SUM _:#_. _)\<close> [0, 51, 10] 10)
+ "_sum_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
+ (\<open>(\<open>indent=3 notation=\<open>binder SUM\<close>\<close>SUM _:#_. _)\<close> [0, 51, 10] 10)
syntax
- "_sum_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" (\<open>(3\<Sum>_\<in>#_. _)\<close> [0, 51, 10] 10)
+ "_sum_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
+ (\<open>(\<open>indent=3 notation=\<open>binder \<Sum>\<close>\<close>\<Sum>_\<in>#_. _)\<close> [0, 51, 10] 10)
syntax_consts
"_sum_mset_image" \<rightleftharpoons> sum_mset
translations
@@ -2863,9 +2872,11 @@
notation prod_mset (\<open>\<Prod>\<^sub>#\<close>)
syntax (ASCII)
- "_prod_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" (\<open>(3PROD _:#_. _)\<close> [0, 51, 10] 10)
+ "_prod_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
+ (\<open>(\<open>indent=3 notation=\<open>binder PROD\<close>\<close>PROD _:#_. _)\<close> [0, 51, 10] 10)
syntax
- "_prod_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" (\<open>(3\<Prod>_\<in>#_. _)\<close> [0, 51, 10] 10)
+ "_prod_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
+ (\<open>(\<open>indent=3 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>_\<in>#_. _)\<close> [0, 51, 10] 10)
syntax_consts
"_prod_mset_image" \<rightleftharpoons> prod_mset
translations