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.6  
     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.12  
    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.18  
    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.26  
    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.31  
    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.36  
    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.41  
    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.46  
    1.47  instantiation multiset :: (type) "{plus, minus, zero, size}" 
    1.48  begin
    1.49  
    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.54  
    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.59  
    1.60 -definition
    1.61 -  Zero_multiset_def [simp]: "0 = {#}"
    1.62 +definition Zero_multiset_def [simp]:
    1.63 +  "0 = {#}"
    1.64  
    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.69  
    1.70  instance ..
    1.71  
    1.72 @@ -207,10 +197,10 @@
    1.73  
    1.74  subsubsection {* Size *}
    1.75  
    1.76 -lemma size_empty [simp,code]: "size {#} = 0"
    1.77 +lemma size_empty [simp]: "size {#} = 0"
    1.78  by (simp add: size_def)
    1.79  
    1.80 -lemma size_single [simp,code]: "size {#b#} = 1"
    1.81 +lemma size_single [simp]: "size {#b#} = 1"
    1.82  by (simp add: size_def)
    1.83  
    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.88  
    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.95  
    1.96  subsubsection {* Comprehension (filter) *}
    1.97  
    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.102  
   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.108  
   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.115  
   1.116  subsubsection {* Well-foundedness *}
   1.117  
   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.125  
   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.130  
   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.135  
   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.140  
   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.145  
   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.149  
   1.150  subsection {* Pointwise ordering induced by count *}
   1.151  
   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.157  
   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.163  
   1.164  notation mset_le  (infix "\<subseteq>#" 50)
   1.165  notation mset_less  (infix "\<subset>#" 50)
   1.166 @@ -1448,22 +1433,23 @@
   1.167  
   1.168  subsection {* Image *}
   1.169  
   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.173  
   1.174  interpretation image_left_comm: left_commutative ["op + o single o f"]
   1.175  by (unfold_locales) (simp add:union_ac)
   1.176  
   1.177 -lemma image_mset_empty [simp, code]: "image_mset f {#} = {#}"
   1.178 +lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
   1.179  by (simp add: image_mset_def)
   1.180  
   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.183  by (simp add: image_mset_def)
   1.184  
   1.185  lemma image_mset_insert:
   1.186    "image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
   1.187  by (simp add: image_mset_def add_ac)
   1.188  
   1.189 -lemma image_mset_union[simp, code]:
   1.190 +lemma image_mset_union [simp]:
   1.191    "image_mset f (M+N) = image_mset f M + image_mset f N"
   1.192  apply (induct N)
   1.193   apply simp
   1.194 @@ -1476,7 +1462,6 @@
   1.195  lemma image_mset_is_empty_iff [simp]: "image_mset f M = {#} \<longleftrightarrow> M = {#}"
   1.196  by (cases M) auto
   1.197  
   1.198 -
   1.199  syntax
   1.200    comprehension1_mset :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
   1.201        ("({#_/. _ :# _#})")