src/HOL/Library/Multiset.thy
 changeset 28708 a1a436f09ec6 parent 28562 4e74209f113e child 28823 dcbef866c9e2
1.1 --- a/src/HOL/Library/Multiset.thy	Tue Oct 28 17:53:46 2008 +0100
1.2 +++ b/src/HOL/Library/Multiset.thy	Wed Oct 29 11:33:40 2008 +0100
1.3 @@ -20,27 +20,19 @@
1.4      Abs_multiset_inverse Rep_multiset_inverse Rep_multiset
1.5    and [simp] = Rep_multiset_inject [symmetric]
1.7 -definition
1.8 -  Mempty :: "'a multiset"  ("{#}") where
1.9 -  "{#} = Abs_multiset (\<lambda>a. 0)"
1.10 +definition Mempty :: "'a multiset"  ("{#}") where
1.11 +  [code del]: "{#} = Abs_multiset (\<lambda>a. 0)"
1.13 -definition
1.14 -  single :: "'a => 'a multiset" where
1.15 -  "single a = Abs_multiset (\<lambda>b. if b = a then 1 else 0)"
1.16 +definition single :: "'a => 'a multiset" where
1.17 +  [code del]: "single a = Abs_multiset (\<lambda>b. if b = a then 1 else 0)"
1.19 -declare
1.20 -  Mempty_def[code del] single_def[code del]
1.21 -
1.22 -definition
1.23 -  count :: "'a multiset => 'a => nat" where
1.24 +definition count :: "'a multiset => 'a => nat" where
1.25    "count = Rep_multiset"
1.27 -definition
1.28 -  MCollect :: "'a multiset => ('a => bool) => 'a multiset" where
1.29 +definition MCollect :: "'a multiset => ('a => bool) => 'a multiset" where
1.30    "MCollect M P = Abs_multiset (\<lambda>x. if P x then Rep_multiset M x else 0)"
1.32 -abbreviation
1.33 -  Melem :: "'a => 'a multiset => bool"  ("(_/ :# _)" [50, 51] 50) where
1.34 +abbreviation Melem :: "'a => 'a multiset => bool"  ("(_/ :# _)" [50, 51] 50) where
1.35    "a :# M == 0 < count M a"
1.37  notation (xsymbols)
1.38 @@ -51,25 +43,23 @@
1.39  translations
1.40    "{#x :# M. P#}" == "CONST MCollect M (\<lambda>x. P)"
1.42 -definition
1.43 -  set_of :: "'a multiset => 'a set" where
1.44 +definition set_of :: "'a multiset => 'a set" where
1.45    "set_of M = {x. x :# M}"
1.47  instantiation multiset :: (type) "{plus, minus, zero, size}"
1.48  begin
1.50 -definition
1.51 -  union_def[code del]:
1.52 +definition union_def [code del]:
1.53    "M + N = Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
1.55 -definition
1.56 -  diff_def: "M - N = Abs_multiset (\<lambda>a. Rep_multiset M a - Rep_multiset N a)"
1.57 +definition diff_def [code del]:
1.58 +  "M - N = Abs_multiset (\<lambda>a. Rep_multiset M a - Rep_multiset N a)"
1.60 -definition
1.61 -  Zero_multiset_def [simp]: "0 = {#}"
1.62 +definition Zero_multiset_def [simp]:
1.63 +  "0 = {#}"
1.65 -definition
1.66 -  size_def[code del]: "size M = setsum (count M) (set_of M)"
1.67 +definition size_def:
1.68 +  "size M = setsum (count M) (set_of M)"
1.70  instance ..
1.72 @@ -207,10 +197,10 @@
1.74  subsubsection {* Size *}
1.76 -lemma size_empty [simp,code]: "size {#} = 0"
1.77 +lemma size_empty [simp]: "size {#} = 0"
1.80 -lemma size_single [simp,code]: "size {#b#} = 1"
1.81 +lemma size_single [simp]: "size {#b#} = 1"
1.84  lemma finite_set_of [iff]: "finite (set_of M)"
1.85 @@ -223,7 +213,7 @@
1.86  apply (simp add: Int_insert_left set_of_def)
1.87  done
1.89 -lemma size_union[simp,code]: "size (M + N::'a multiset) = size M + size N"
1.90 +lemma size_union [simp]: "size (M + N::'a multiset) = size M + size N"
1.91  apply (unfold size_def)
1.92  apply (subgoal_tac "count (M + N) = (\<lambda>a. count M a + count N a)")
1.93   prefer 2
1.94 @@ -376,16 +366,16 @@
1.96  subsubsection {* Comprehension (filter) *}
1.98 -lemma MCollect_empty[simp, code]: "MCollect {#} P = {#}"
1.99 +lemma MCollect_empty [simp]: "MCollect {#} P = {#}"
1.100  by (simp add: MCollect_def Mempty_def Abs_multiset_inject
1.101      in_multiset expand_fun_eq)
1.103 -lemma MCollect_single[simp, code]:
1.104 +lemma MCollect_single [simp]:
1.105    "MCollect {#x#} P = (if P x then {#x#} else {#})"
1.106  by (simp add: MCollect_def Mempty_def single_def Abs_multiset_inject
1.107      in_multiset expand_fun_eq)
1.109 -lemma MCollect_union[simp, code]:
1.110 +lemma MCollect_union [simp]:
1.111    "MCollect (M+N) f = MCollect M f + MCollect N f"
1.112  by (simp add: MCollect_def union_def Abs_multiset_inject
1.113      in_multiset expand_fun_eq)
1.114 @@ -498,14 +488,11 @@
1.116  subsubsection {* Well-foundedness *}
1.118 -definition
1.119 -  mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
1.120 -  [code del]:"mult1 r =
1.121 -    {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
1.122 +definition mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
1.123 +  [code del]: "mult1 r = {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
1.124        (\<forall>b. b :# K --> (b, a) \<in> r)}"
1.126 -definition
1.127 -  mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
1.128 +definition mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
1.129    "mult r = (mult1 r)\<^sup>+"
1.131  lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
1.132 @@ -715,11 +702,11 @@
1.133  instantiation multiset :: (order) order
1.134  begin
1.136 -definition
1.137 -  less_multiset_def [code del]: "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
1.138 +definition less_multiset_def [code del]:
1.139 +  "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
1.141 -definition
1.142 -  le_multiset_def [code del]: "M' <= M \<longleftrightarrow> M' = M \<or> M' < (M::'a multiset)"
1.143 +definition le_multiset_def [code del]:
1.144 +  "M' <= M \<longleftrightarrow> M' = M \<or> M' < (M::'a multiset)"
1.146  lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}"
1.147  unfolding trans_def by (blast intro: order_less_trans)
1.148 @@ -981,13 +968,11 @@
1.150  subsection {* Pointwise ordering induced by count *}
1.152 -definition
1.153 -  mset_le :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<le>#" 50) where
1.154 -  [code del]: "(A \<le># B) = (\<forall>a. count A a \<le> count B a)"
1.155 +definition mset_le :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<le>#" 50) where
1.156 +  [code del]: "A \<le># B \<longleftrightarrow> (\<forall>a. count A a \<le> count B a)"
1.158 -definition
1.159 -  mset_less :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "<#" 50) where
1.160 -  [code del]: "(A <# B) = (A \<le># B \<and> A \<noteq> B)"
1.161 +definition mset_less :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "<#" 50) where
1.162 +  [code del]: "A <# B \<longleftrightarrow> A \<le># B \<and> A \<noteq> B"
1.164  notation mset_le  (infix "\<subseteq>#" 50)
1.165  notation mset_less  (infix "\<subset>#" 50)
1.166 @@ -1448,22 +1433,23 @@
1.168  subsection {* Image *}
1.170 -definition [code del]: "image_mset f == fold_mset (op + o single o f) {#}"
1.171 +definition [code del]:
1.172 + "image_mset f = fold_mset (op + o single o f) {#}"
1.174  interpretation image_left_comm: left_commutative ["op + o single o f"]
1.177 -lemma image_mset_empty [simp, code]: "image_mset f {#} = {#}"
1.178 +lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
1.181 -lemma image_mset_single [simp, code]: "image_mset f {#x#} = {#f x#}"
1.182 +lemma image_mset_single [simp]: "image_mset f {#x#} = {#f x#}"
1.185  lemma image_mset_insert:
1.186    "image_mset f (M + {#a#}) = image_mset f M + {#f a#}"