src/HOL/Library/Multiset.thy
 changeset 61955 e96292f32c3c parent 61890 f6ded81f5690 child 62082 614ef6d7a6b6
1.1 --- a/src/HOL/Library/Multiset.thy	Mon Dec 28 19:23:15 2015 +0100
1.2 +++ b/src/HOL/Library/Multiset.thy	Mon Dec 28 21:47:32 2015 +0100
1.3 @@ -25,11 +25,11 @@
1.5  setup_lifting type_definition_multiset
1.7 -abbreviation Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool"  ("(_/ :# _)" [50, 51] 50) where
1.8 -  "a :# M == 0 < count M a"
1.9 -
1.10 -notation (xsymbols)
1.11 -  Melem (infix "\<in>#" 50)
1.12 +abbreviation Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<in>#" 50)
1.13 +  where "a \<in># M \<equiv> 0 < count M a"
1.14 +
1.15 +notation (ASCII)
1.16 +  Melem  ("(_/ :# _)" [50, 51] 50)  (* FIXME !? *)
1.18  lemma multiset_eq_iff: "M = N \<longleftrightarrow> (\<forall>a. count M a = count N a)"
1.19    by (simp only: count_inject [symmetric] fun_eq_iff)
1.20 @@ -265,16 +265,18 @@
1.22  subsubsection \<open>Pointwise ordering induced by count\<close>
1.24 -definition subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<=#" 50) where
1.25 -"subseteq_mset A B = (\<forall>a. count A a \<le> count B a)"
1.26 -
1.27 -definition subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<#" 50) where
1.28 -"subset_mset A B = (A <=# B \<and> A \<noteq> B)"
1.29 -
1.30 -notation subseteq_mset (infix "\<le>#" 50)
1.31 -notation (xsymbols) subseteq_mset (infix "\<subseteq>#" 50)
1.32 -
1.33 -notation (xsymbols) subset_mset (infix "\<subset>#" 50)
1.34 +definition subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<subseteq>#" 50)
1.35 +  where "A \<subseteq># B = (\<forall>a. count A a \<le> count B a)"
1.36 +
1.37 +definition subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subset>#" 50)
1.38 +  where "A \<subset># B = (A \<subseteq># B \<and> A \<noteq> B)"
1.39 +
1.40 +notation (input)
1.41 +  subseteq_mset  (infix "\<le>#" 50)
1.42 +
1.43 +notation (ASCII)
1.44 +  subseteq_mset  (infix "<=#" 50) and
1.45 +  subset_mset  (infix "<#" 50)
1.47  interpretation subset_mset: ordered_ab_semigroup_add_imp_le "op +" "op -" "op \<subseteq>#" "op \<subset>#"
1.48    by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)
1.49 @@ -504,9 +506,9 @@
1.50    show ?thesis unfolding B by auto
1.51  qed
1.53 -syntax
1.54 +syntax (ASCII)
1.55    "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"    ("(1{# _ :# _./ _#})")
1.56 -syntax (xsymbol)
1.57 +syntax
1.58    "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"    ("(1{# _ \<in># _./ _#})")
1.59  translations
1.60    "{#x \<in># M. P#}" == "CONST filter_mset (\<lambda>x. P) M"
1.61 @@ -855,27 +857,17 @@
1.62  lemma image_mset_is_empty_iff [simp]: "image_mset f M = {#} \<longleftrightarrow> M = {#}"
1.63    by (cases M) auto
1.65 +syntax (ASCII)
1.66 +  "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"  ("({#_/. _ :# _#})")
1.67  syntax
1.68 -  "_comprehension1_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
1.69 -      ("({#_/. _ :# _#})")
1.70 -translations
1.71 -  "{#e. x:#M#}" == "CONST image_mset (\<lambda>x. e) M"
1.72 -
1.73 -syntax (xsymbols)
1.74 -  "_comprehension2_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
1.75 -      ("({#_/. _ \<in># _#})")
1.76 +  "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"  ("({#_/. _ \<in># _#})")
1.77  translations
1.78 -  "{#e. x \<in># M#}" == "CONST image_mset (\<lambda>x. e) M"
1.79 -
1.80 +  "{#e. x \<in># M#}" \<rightleftharpoons> "CONST image_mset (\<lambda>x. e) M"
1.81 +
1.82 +syntax (ASCII)
1.83 +  "_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"  ("({#_/ | _ :# _./ _#})")
1.84  syntax
1.85 -  "_comprehension3_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
1.86 -      ("({#_/ | _ :# _./ _#})")
1.87 -translations
1.88 -  "{#e | x:#M. P#}" \<rightharpoonup> "{#e. x :# {# x:#M. P#}#}"
1.89 -
1.90 -syntax
1.91 -  "_comprehension4_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
1.92 -      ("({#_/ | _ \<in># _./ _#})")
1.93 +  "_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"  ("({#_/ | _ \<in># _./ _#})")
1.94  translations
1.95    "{#e | x\<in>#M. P#}" \<rightharpoonup> "{#e. x \<in># {# x\<in>#M. P#}#}"
1.97 @@ -1235,10 +1227,8 @@
1.98  qed
1.101 -abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset" where
1.102 -  "Union_mset MM \<equiv> msetsum MM"
1.104 -notation (xsymbols) Union_mset ("\<Union>#_" [900] 900)
1.105 +abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset"  ("\<Union>#_" [900] 900)
1.106 +  where "\<Union># MM \<equiv> msetsum MM"
1.108  lemma set_mset_Union_mset[simp]: "set_mset (\<Union># MM) = (\<Union>M \<in> set_mset MM. set_mset M)"
1.109    by (induct MM) auto
1.110 @@ -1246,14 +1236,12 @@
1.111  lemma in_Union_mset_iff[iff]: "x \<in># \<Union># MM \<longleftrightarrow> (\<exists>M. M \<in># MM \<and> x \<in># M)"
1.112    by (induct MM) auto
1.114 +syntax (ASCII)
1.115 +  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"  ("(3SUM _:#_. _)" [0, 51, 10] 10)
1.116  syntax
1.117 -  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
1.118 -      ("(3SUM _:#_. _)" [0, 51, 10] 10)
1.119 -syntax (xsymbols)
1.120 -  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
1.121 -      ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
1.122 +  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"  ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
1.123  translations
1.124 -  "SUM i :# A. b" == "CONST msetsum (CONST image_mset (\<lambda>i. b) A)"
1.125 +  "\<Sum>i \<in># A. b" \<rightleftharpoons> "CONST msetsum (CONST image_mset (\<lambda>i. b) A)"
1.127  context comm_monoid_mult
1.128  begin
1.129 @@ -1287,14 +1275,12 @@
1.131  end
1.133 +syntax (ASCII)
1.134 +  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  ("(3PROD _:#_. _)" [0, 51, 10] 10)
1.135  syntax
1.136 -  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
1.137 -      ("(3PROD _:#_. _)" [0, 51, 10] 10)
1.138 -syntax (xsymbols)
1.139 -  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
1.140 -      ("(3\<Prod>_\<in>#_. _)" [0, 51, 10] 10)
1.141 +  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  ("(3\<Prod>_\<in>#_. _)" [0, 51, 10] 10)
1.142  translations
1.143 -  "PROD i :# A. b" == "CONST msetprod (CONST image_mset (\<lambda>i. b) A)"
1.144 +  "\<Prod>i \<in># A. b" \<rightleftharpoons> "CONST msetprod (CONST image_mset (\<lambda>i. b) A)"
1.146  lemma (in comm_semiring_1) dvd_msetprod:
1.147    assumes "x \<in># A"
1.148 @@ -1718,14 +1704,15 @@
1.150  subsubsection \<open>Partial-order properties\<close>
1.152 -definition less_multiset :: "'a::order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "#<#" 50) where
1.153 -  "M' #<# M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
1.155 -definition le_multiset :: "'a::order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "#<=#" 50) where
1.156 -  "M' #<=# M \<longleftrightarrow> M' #<# M \<or> M' = M"
1.158 -notation (xsymbols) less_multiset (infix "#\<subset>#" 50)
1.159 -notation (xsymbols) le_multiset (infix "#\<subseteq>#" 50)
1.160 +definition less_multiset :: "'a::order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "#\<subset>#" 50)
1.161 +  where "M' #\<subset># M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
1.163 +definition le_multiset :: "'a::order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "#\<subseteq>#" 50)
1.164 +  where "M' #\<subseteq># M \<longleftrightarrow> M' #\<subset># M \<or> M' = M"
1.166 +notation (ASCII)
1.167 +  less_multiset (infix "#<#" 50) and
1.168 +  le_multiset (infix "#<=#" 50)
1.170  interpretation multiset_order: order le_multiset less_multiset
1.171  proof -