src/HOL/Library/Multiset.thy
changeset 51600 197e25f13f0c
parent 51599 1559e9266280
child 51623 1194b438426a
     1.1 --- a/src/HOL/Library/Multiset.thy	Wed Apr 03 22:26:04 2013 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Wed Apr 03 22:26:04 2013 +0200
     1.3 @@ -257,6 +257,10 @@
     1.4      (M = N \<and> a = b \<or> (\<exists>K. M = K + {#b#} \<and> N = K + {#a#}))"
     1.5    by (auto simp add: add_eq_conv_diff)
     1.6  
     1.7 +lemma multi_member_split:
     1.8 +  "x \<in># M \<Longrightarrow> \<exists>A. M = A + {#x#}"
     1.9 +  by (rule_tac x = "M - {#x#}" in exI, simp)
    1.10 +
    1.11  
    1.12  subsubsection {* Pointwise ordering induced by count *}
    1.13  
    1.14 @@ -409,6 +413,30 @@
    1.15      by auto
    1.16  qed
    1.17  
    1.18 +lemma empty_inter [simp]:
    1.19 +  "{#} #\<inter> M = {#}"
    1.20 +  by (simp add: multiset_eq_iff)
    1.21 +
    1.22 +lemma inter_empty [simp]:
    1.23 +  "M #\<inter> {#} = {#}"
    1.24 +  by (simp add: multiset_eq_iff)
    1.25 +
    1.26 +lemma inter_add_left1:
    1.27 +  "\<not> x \<in># N \<Longrightarrow> (M + {#x#}) #\<inter> N = M #\<inter> N"
    1.28 +  by (simp add: multiset_eq_iff)
    1.29 +
    1.30 +lemma inter_add_left2:
    1.31 +  "x \<in># N \<Longrightarrow> (M + {#x#}) #\<inter> N = (M #\<inter> (N - {#x#})) + {#x#}"
    1.32 +  by (simp add: multiset_eq_iff)
    1.33 +
    1.34 +lemma inter_add_right1:
    1.35 +  "\<not> x \<in># N \<Longrightarrow> N #\<inter> (M + {#x#}) = N #\<inter> M"
    1.36 +  by (simp add: multiset_eq_iff)
    1.37 +
    1.38 +lemma inter_add_right2:
    1.39 +  "x \<in># N \<Longrightarrow> N #\<inter> (M + {#x#}) = ((N - {#x#}) #\<inter> M) + {#x#}"
    1.40 +  by (simp add: multiset_eq_iff)
    1.41 +
    1.42  
    1.43  subsubsection {* Filter (with comprehension syntax) *}
    1.44  
    1.45 @@ -563,9 +591,6 @@
    1.46  shows "P"
    1.47  using assms by (induct M) simp_all
    1.48  
    1.49 -lemma multi_member_split: "x \<in># M \<Longrightarrow> \<exists>A. M = A + {#x#}"
    1.50 -by (rule_tac x="M - {#x#}" in exI, simp)
    1.51 -
    1.52  lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B - {#c#} \<noteq> B"
    1.53  by (cases "B = {#}") (auto dest: multi_member_split)
    1.54  
    1.55 @@ -952,6 +977,14 @@
    1.56    "multiset_of (insort x xs) = multiset_of xs + {#x#}"
    1.57    by (induct xs) (simp_all add: ac_simps)
    1.58  
    1.59 +lemma in_multiset_of:
    1.60 +  "x \<in># multiset_of xs \<longleftrightarrow> x \<in> set xs"
    1.61 +  by (induct xs) simp_all
    1.62 +
    1.63 +lemma multiset_of_map:
    1.64 +  "multiset_of (map f xs) = image_mset f (multiset_of xs)"
    1.65 +  by (induct xs) simp_all
    1.66 +
    1.67  definition multiset_of_set :: "'a set \<Rightarrow> 'a multiset"
    1.68  where
    1.69    "multiset_of_set = folding.F (\<lambda>x M. {#x#} + M) {#}"
    1.70 @@ -965,6 +998,24 @@
    1.71    from multiset_of_set_def show "folding.F (\<lambda>x M. {#x#} + M) {#} = multiset_of_set" ..
    1.72  qed
    1.73  
    1.74 +lemma count_multiset_of_set [simp]:
    1.75 +  "finite A \<Longrightarrow> x \<in> A \<Longrightarrow> count (multiset_of_set A) x = 1" (is "PROP ?P")
    1.76 +  "\<not> finite A \<Longrightarrow> count (multiset_of_set A) x = 0" (is "PROP ?Q")
    1.77 +  "x \<notin> A \<Longrightarrow> count (multiset_of_set A) x = 0" (is "PROP ?R")
    1.78 +proof -
    1.79 +  { fix A
    1.80 +    assume "x \<notin> A"
    1.81 +    have "count (multiset_of_set A) x = 0"
    1.82 +    proof (cases "finite A")
    1.83 +      case False then show ?thesis by simp
    1.84 +    next
    1.85 +      case True from True `x \<notin> A` show ?thesis by (induct A) auto
    1.86 +    qed
    1.87 +  } note * = this
    1.88 +  then show "PROP ?P" "PROP ?Q" "PROP ?R"
    1.89 +  by (auto elim!: Set.set_insert)
    1.90 +qed -- {* TODO: maybe define @{const multiset_of_set} also in terms of @{const Abs_multiset} *}
    1.91 +
    1.92  context linorder
    1.93  begin
    1.94  
    1.95 @@ -1194,6 +1245,14 @@
    1.96        (simp_all del: mem_set_of_iff add: setsum.distrib setsum.delta' insert_absorb, simp)
    1.97  qed
    1.98  
    1.99 +lemma size_eq_mcard:
   1.100 +  "size = mcard"
   1.101 +  by (simp add: fun_eq_iff size_def mcard_unfold_setsum)
   1.102 +
   1.103 +lemma mcard_multiset_of:
   1.104 +  "mcard (multiset_of xs) = length xs"
   1.105 +  by (induct xs) simp_all
   1.106 +
   1.107  
   1.108  subsection {* Alternative representations *}
   1.109  
   1.110 @@ -1886,5 +1945,155 @@
   1.111  
   1.112  hide_const (open) fold
   1.113  
   1.114 +
   1.115 +subsection {* Naive implementation using lists *}
   1.116 +
   1.117 +code_datatype multiset_of
   1.118 +
   1.119 +lemma [code]:
   1.120 +  "{#} = multiset_of []"
   1.121 +  by simp
   1.122 +
   1.123 +lemma [code]:
   1.124 +  "{#x#} = multiset_of [x]"
   1.125 +  by simp
   1.126 +
   1.127 +lemma union_code [code]:
   1.128 +  "multiset_of xs + multiset_of ys = multiset_of (xs @ ys)"
   1.129 +  by simp
   1.130 +
   1.131 +lemma [code]:
   1.132 +  "image_mset f (multiset_of xs) = multiset_of (map f xs)"
   1.133 +  by (simp add: multiset_of_map)
   1.134 +
   1.135 +lemma [code]:
   1.136 +  "Multiset.filter f (multiset_of xs) = multiset_of (filter f xs)"
   1.137 +  by (simp add: multiset_of_filter)
   1.138 +
   1.139 +lemma [code]:
   1.140 +  "multiset_of xs - multiset_of ys = multiset_of (fold remove1 ys xs)"
   1.141 +  by (rule sym, induct ys arbitrary: xs) (simp_all add: diff_add diff_right_commute)
   1.142 +
   1.143 +lemma [code]:
   1.144 +  "multiset_of xs #\<inter> multiset_of ys =
   1.145 +    multiset_of (snd (fold (\<lambda>x (ys, zs).
   1.146 +      if x \<in> set ys then (remove1 x ys, x # zs) else (ys, zs)) xs (ys, [])))"
   1.147 +proof -
   1.148 +  have "\<And>zs. multiset_of (snd (fold (\<lambda>x (ys, zs).
   1.149 +    if x \<in> set ys then (remove1 x ys, x # zs) else (ys, zs)) xs (ys, zs))) =
   1.150 +      (multiset_of xs #\<inter> multiset_of ys) + multiset_of zs"
   1.151 +  by (induct xs arbitrary: ys)
   1.152 +    (auto simp add: mem_set_multiset_eq inter_add_right1 inter_add_right2 ac_simps)
   1.153 +  then show ?thesis by simp
   1.154 +qed
   1.155 +
   1.156 +lemma [code_unfold]:
   1.157 +  "x \<in># multiset_of xs \<longleftrightarrow> x \<in> set xs"
   1.158 +  by (simp add: in_multiset_of)
   1.159 +
   1.160 +lemma [code]:
   1.161 +  "count (multiset_of xs) x = fold (\<lambda>y. if x = y then Suc else id) xs 0"
   1.162 +proof -
   1.163 +  have "\<And>n. fold (\<lambda>y. if x = y then Suc else id) xs n = count (multiset_of xs) x + n"
   1.164 +    by (induct xs) simp_all
   1.165 +  then show ?thesis by simp
   1.166 +qed
   1.167 +
   1.168 +lemma [code]:
   1.169 +  "set_of (multiset_of xs) = set xs"
   1.170 +  by simp
   1.171 +
   1.172 +lemma [code]:
   1.173 +  "sorted_list_of_multiset (multiset_of xs) = sort xs"
   1.174 +  by (induct xs) simp_all
   1.175 +
   1.176 +lemma [code]: -- {* not very efficient, but representation-ignorant! *}
   1.177 +  "multiset_of_set A = multiset_of (sorted_list_of_set A)"
   1.178 +  apply (cases "finite A")
   1.179 +  apply simp_all
   1.180 +  apply (induct A rule: finite_induct)
   1.181 +  apply (simp_all add: union_commute)
   1.182 +  done
   1.183 +
   1.184 +lemma [code]:
   1.185 +  "mcard (multiset_of xs) = length xs"
   1.186 +  by (simp add: mcard_multiset_of)
   1.187 +
   1.188 +lemma [code]:
   1.189 +  "A \<le> B \<longleftrightarrow> A #\<inter> B = A" 
   1.190 +  by (auto simp add: inf.order_iff)
   1.191 +
   1.192 +instantiation multiset :: (equal) equal
   1.193 +begin
   1.194 +
   1.195 +definition
   1.196 +  [code]: "HOL.equal A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
   1.197 +
   1.198 +instance
   1.199 +  by default (simp add: equal_multiset_def eq_iff)
   1.200 +
   1.201  end
   1.202  
   1.203 +lemma [code]:
   1.204 +  "(A::'a multiset) < B \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
   1.205 +  by auto
   1.206 +
   1.207 +lemma [code]:
   1.208 +  "msetsum (multiset_of xs) = listsum xs"
   1.209 +  by (induct xs) (simp_all add: add.commute)
   1.210 +
   1.211 +lemma [code]:
   1.212 +  "msetprod (multiset_of xs) = fold times xs 1"
   1.213 +proof -
   1.214 +  have "\<And>x. fold times xs x = msetprod (multiset_of xs) * x"
   1.215 +    by (induct xs) (simp_all add: mult.assoc)
   1.216 +  then show ?thesis by simp
   1.217 +qed
   1.218 +
   1.219 +lemma [code]:
   1.220 +  "size = mcard"
   1.221 +  by (fact size_eq_mcard)
   1.222 +
   1.223 +text {*
   1.224 +  Exercise for the casual reader: add implementations for @{const le_multiset}
   1.225 +  and @{const less_multiset} (multiset order).
   1.226 +*}
   1.227 +
   1.228 +text {* Quickcheck generators *}
   1.229 +
   1.230 +definition (in term_syntax)
   1.231 +  msetify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
   1.232 +    \<Rightarrow> 'a multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
   1.233 +  [code_unfold]: "msetify xs = Code_Evaluation.valtermify multiset_of {\<cdot>} xs"
   1.234 +
   1.235 +notation fcomp (infixl "\<circ>>" 60)
   1.236 +notation scomp (infixl "\<circ>\<rightarrow>" 60)
   1.237 +
   1.238 +instantiation multiset :: (random) random
   1.239 +begin
   1.240 +
   1.241 +definition
   1.242 +  "Quickcheck_Random.random i = Quickcheck_Random.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (msetify xs))"
   1.243 +
   1.244 +instance ..
   1.245 +
   1.246 +end
   1.247 +
   1.248 +no_notation fcomp (infixl "\<circ>>" 60)
   1.249 +no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
   1.250 +
   1.251 +instantiation multiset :: (full_exhaustive) full_exhaustive
   1.252 +begin
   1.253 +
   1.254 +definition full_exhaustive_multiset :: "('a multiset \<times> (unit \<Rightarrow> term) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
   1.255 +where
   1.256 +  "full_exhaustive_multiset f i = Quickcheck_Exhaustive.full_exhaustive (\<lambda>xs. f (msetify xs)) i"
   1.257 +
   1.258 +instance ..
   1.259 +
   1.260 +end
   1.261 +
   1.262 +hide_const (open) msetify
   1.263 +
   1.264 +end
   1.265 +