--- a/src/HOL/Library/Multiset.thy Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Library/Multiset.thy Mon Dec 28 21:47:32 2015 +0100
@@ -25,11 +25,11 @@
setup_lifting type_definition_multiset
-abbreviation Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool" ("(_/ :# _)" [50, 51] 50) where
- "a :# M == 0 < count M a"
-
-notation (xsymbols)
- Melem (infix "\<in>#" 50)
+abbreviation Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<in>#" 50)
+ where "a \<in># M \<equiv> 0 < count M a"
+
+notation (ASCII)
+ Melem ("(_/ :# _)" [50, 51] 50) (* FIXME !? *)
lemma multiset_eq_iff: "M = N \<longleftrightarrow> (\<forall>a. count M a = count N a)"
by (simp only: count_inject [symmetric] fun_eq_iff)
@@ -265,16 +265,18 @@
subsubsection \<open>Pointwise ordering induced by count\<close>
-definition subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<=#" 50) where
-"subseteq_mset A B = (\<forall>a. count A a \<le> count B a)"
-
-definition subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<#" 50) where
-"subset_mset A B = (A <=# B \<and> A \<noteq> B)"
-
-notation subseteq_mset (infix "\<le>#" 50)
-notation (xsymbols) subseteq_mset (infix "\<subseteq>#" 50)
-
-notation (xsymbols) subset_mset (infix "\<subset>#" 50)
+definition subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subseteq>#" 50)
+ where "A \<subseteq># B = (\<forall>a. count A a \<le> count B a)"
+
+definition subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subset>#" 50)
+ where "A \<subset># B = (A \<subseteq># B \<and> A \<noteq> B)"
+
+notation (input)
+ subseteq_mset (infix "\<le>#" 50)
+
+notation (ASCII)
+ subseteq_mset (infix "<=#" 50) and
+ subset_mset (infix "<#" 50)
interpretation subset_mset: ordered_ab_semigroup_add_imp_le "op +" "op -" "op \<subseteq>#" "op \<subset>#"
by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)
@@ -504,9 +506,9 @@
show ?thesis unfolding B by auto
qed
-syntax
+syntax (ASCII)
"_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("(1{# _ :# _./ _#})")
-syntax (xsymbol)
+syntax
"_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("(1{# _ \<in># _./ _#})")
translations
"{#x \<in># M. P#}" == "CONST filter_mset (\<lambda>x. P) M"
@@ -855,27 +857,17 @@
lemma image_mset_is_empty_iff [simp]: "image_mset f M = {#} \<longleftrightarrow> M = {#}"
by (cases M) auto
+syntax (ASCII)
+ "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset" ("({#_/. _ :# _#})")
syntax
- "_comprehension1_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
- ("({#_/. _ :# _#})")
-translations
- "{#e. x:#M#}" == "CONST image_mset (\<lambda>x. e) M"
-
-syntax (xsymbols)
- "_comprehension2_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
- ("({#_/. _ \<in># _#})")
+ "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset" ("({#_/. _ \<in># _#})")
translations
- "{#e. x \<in># M#}" == "CONST image_mset (\<lambda>x. e) M"
-
+ "{#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" ("({#_/ | _ :# _./ _#})")
syntax
- "_comprehension3_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
- ("({#_/ | _ :# _./ _#})")
-translations
- "{#e | x:#M. P#}" \<rightharpoonup> "{#e. x :# {# x:#M. P#}#}"
-
-syntax
- "_comprehension4_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
- ("({#_/ | _ \<in># _./ _#})")
+ "_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset" ("({#_/ | _ \<in># _./ _#})")
translations
"{#e | x\<in>#M. P#}" \<rightharpoonup> "{#e. x \<in># {# x\<in>#M. P#}#}"
@@ -1235,10 +1227,8 @@
qed
-abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset" where
- "Union_mset MM \<equiv> msetsum MM"
-
-notation (xsymbols) Union_mset ("\<Union>#_" [900] 900)
+abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset" ("\<Union>#_" [900] 900)
+ where "\<Union># MM \<equiv> msetsum MM"
lemma set_mset_Union_mset[simp]: "set_mset (\<Union># MM) = (\<Union>M \<in> set_mset MM. set_mset M)"
by (induct MM) auto
@@ -1246,14 +1236,12 @@
lemma in_Union_mset_iff[iff]: "x \<in># \<Union># MM \<longleftrightarrow> (\<exists>M. M \<in># MM \<and> x \<in># M)"
by (induct MM) auto
+syntax (ASCII)
+ "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" ("(3SUM _:#_. _)" [0, 51, 10] 10)
syntax
- "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
- ("(3SUM _:#_. _)" [0, 51, 10] 10)
-syntax (xsymbols)
- "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
- ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
+ "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
translations
- "SUM i :# A. b" == "CONST msetsum (CONST image_mset (\<lambda>i. b) A)"
+ "\<Sum>i \<in># A. b" \<rightleftharpoons> "CONST msetsum (CONST image_mset (\<lambda>i. b) A)"
context comm_monoid_mult
begin
@@ -1287,14 +1275,12 @@
end
+syntax (ASCII)
+ "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" ("(3PROD _:#_. _)" [0, 51, 10] 10)
syntax
- "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
- ("(3PROD _:#_. _)" [0, 51, 10] 10)
-syntax (xsymbols)
- "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
- ("(3\<Prod>_\<in>#_. _)" [0, 51, 10] 10)
+ "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" ("(3\<Prod>_\<in>#_. _)" [0, 51, 10] 10)
translations
- "PROD i :# A. b" == "CONST msetprod (CONST image_mset (\<lambda>i. b) A)"
+ "\<Prod>i \<in># A. b" \<rightleftharpoons> "CONST msetprod (CONST image_mset (\<lambda>i. b) A)"
lemma (in comm_semiring_1) dvd_msetprod:
assumes "x \<in># A"
@@ -1718,14 +1704,15 @@
subsubsection \<open>Partial-order properties\<close>
-definition less_multiset :: "'a::order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "#<#" 50) where
- "M' #<# M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
-
-definition le_multiset :: "'a::order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "#<=#" 50) where
- "M' #<=# M \<longleftrightarrow> M' #<# M \<or> M' = M"
-
-notation (xsymbols) less_multiset (infix "#\<subset>#" 50)
-notation (xsymbols) le_multiset (infix "#\<subseteq>#" 50)
+definition less_multiset :: "'a::order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "#\<subset>#" 50)
+ where "M' #\<subset># M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
+
+definition le_multiset :: "'a::order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "#\<subseteq>#" 50)
+ where "M' #\<subseteq># M \<longleftrightarrow> M' #\<subset># M \<or> M' = M"
+
+notation (ASCII)
+ less_multiset (infix "#<#" 50) and
+ le_multiset (infix "#<=#" 50)
interpretation multiset_order: order le_multiset less_multiset
proof -