src/HOL/Library/Multiset.thy

--- a/src/HOL/Library/Multiset.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Library/Multiset.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -21,20 +21,23 @@
   and [simp] = Rep_multiset_inject [symmetric]
 
 definition
-  Mempty :: "'a multiset"    ("{#}")
+  Mempty :: "'a multiset"  ("{#}") where
   "{#} = Abs_multiset (\<lambda>a. 0)"
 
-  single :: "'a => 'a multiset"    ("{#_#}")
+definition
+  single :: "'a => 'a multiset"  ("{#_#}") where
   "{#a#} = Abs_multiset (\<lambda>b. if b = a then 1 else 0)"
 
-  count :: "'a multiset => 'a => nat"
+definition
+  count :: "'a multiset => 'a => nat" where
   "count = Rep_multiset"
 
-  MCollect :: "'a multiset => ('a => bool) => 'a multiset"
+definition
+  MCollect :: "'a multiset => ('a => bool) => 'a multiset" where
   "MCollect M P = Abs_multiset (\<lambda>x. if P x then Rep_multiset M x else 0)"
 
 abbreviation
-  Melem :: "'a => 'a multiset => bool"    ("(_/ :# _)" [50, 51] 50)
+  Melem :: "'a => 'a multiset => bool"  ("(_/ :# _)" [50, 51] 50) where
   "a :# M == 0 < count M a"
 
 syntax
@@ -43,7 +46,7 @@
   "{#x:M. P#}" == "CONST MCollect M (\<lambda>x. P)"
 
 definition
-  set_of :: "'a multiset => 'a set"
+  set_of :: "'a multiset => 'a set" where
   "set_of M = {x. x :# M}"
 
 instance multiset :: (type) "{plus, minus, zero}" ..
@@ -55,7 +58,7 @@
   size_def: "size M == setsum (count M) (set_of M)"
 
 definition
-  multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70)
+  multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"  (infixl "#\<inter>" 70) where
   "multiset_inter A B = A - (A - B)"
 
 
@@ -380,12 +383,13 @@
 subsubsection {* Well-foundedness *}
 
 definition
-  mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set"
+  mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
   "mult1 r =
     {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
       (\<forall>b. b :# K --> (b, a) \<in> r)}"
 
-  mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set"
+definition
+  mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
   "mult r = (mult1 r)\<^sup>+"
 
 lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
@@ -796,7 +800,7 @@
 subsection {* Pointwise ordering induced by count *}
 
 definition
-  mset_le :: "['a multiset, 'a multiset] \<Rightarrow> bool"   ("_ \<le># _"  [50,51] 50)
+  mset_le :: "['a multiset, 'a multiset] \<Rightarrow> bool"  ("_ \<le># _"  [50,51] 50) where
   "(xs \<le># ys) = (\<forall>a. count xs a \<le> count ys a)"
 
 lemma mset_le_refl[simp]: "xs \<le># xs"