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.4  
     1.5  setup_lifting type_definition_multiset
     1.6  
     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.17  
    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.21  
    1.22  subsubsection \<open>Pointwise ordering induced by count\<close>
    1.23  
    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.46  
    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.52  
    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.64  
    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.96  
    1.97 @@ -1235,10 +1227,8 @@
    1.98  qed
    1.99  
   1.100  
   1.101 -abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset" where
   1.102 -  "Union_mset MM \<equiv> msetsum MM"
   1.103 -
   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.107  
   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.113  
   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.126  
   1.127  context comm_monoid_mult
   1.128  begin
   1.129 @@ -1287,14 +1275,12 @@
   1.130  
   1.131  end
   1.132  
   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.145  
   1.146  lemma (in comm_semiring_1) dvd_msetprod:
   1.147    assumes "x \<in># A"
   1.148 @@ -1718,14 +1704,15 @@
   1.149  
   1.150  subsubsection \<open>Partial-order properties\<close>
   1.151  
   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.154 -
   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.157 -
   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.162 +
   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.165 +
   1.166 +notation (ASCII)
   1.167 +  less_multiset (infix "#<#" 50) and
   1.168 +  le_multiset (infix "#<=#" 50)
   1.169  
   1.170  interpretation multiset_order: order le_multiset less_multiset
   1.171  proof -