src/HOL/Library/Multiset.thy
changeset 51599 1559e9266280
parent 51548 757fa47af981
child 51600 197e25f13f0c
     1.1 --- a/src/HOL/Library/Multiset.thy	Wed Apr 03 10:15:43 2013 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Wed Apr 03 22:26:04 2013 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* (Finite) multisets *}
     1.5  
     1.6  theory Multiset
     1.7 -imports Main DAList (* FIXME too specific dependency for a generic theory *)
     1.8 +imports Main
     1.9  begin
    1.10  
    1.11  subsection {* The type of multisets *}
    1.12 @@ -1371,232 +1371,6 @@
    1.13    by (cases "i = j") (simp_all add: multiset_of_update nth_mem_multiset_of)
    1.14  
    1.15  
    1.16 -subsubsection {* Association lists -- including code generation *}
    1.17 -
    1.18 -text {* Preliminaries *}
    1.19 -
    1.20 -text {* Raw operations on lists *}
    1.21 -
    1.22 -definition join_raw :: "('key \<Rightarrow> 'val \<times> 'val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.23 -where
    1.24 -  "join_raw f xs ys = foldr (\<lambda>(k, v). map_default k v (%v'. f k (v', v))) ys xs"
    1.25 -
    1.26 -lemma join_raw_Nil [simp]:
    1.27 -  "join_raw f xs [] = xs"
    1.28 -by (simp add: join_raw_def)
    1.29 -
    1.30 -lemma join_raw_Cons [simp]:
    1.31 -  "join_raw f xs ((k, v) # ys) = map_default k v (%v'. f k (v', v)) (join_raw f xs ys)"
    1.32 -by (simp add: join_raw_def)
    1.33 -
    1.34 -lemma map_of_join_raw:
    1.35 -  assumes "distinct (map fst ys)"
    1.36 -  shows "map_of (join_raw f xs ys) x = (case map_of xs x of None => map_of ys x | Some v =>
    1.37 -    (case map_of ys x of None => Some v | Some v' => Some (f x (v, v'))))"
    1.38 -using assms
    1.39 -apply (induct ys)
    1.40 -apply (auto simp add: map_of_map_default split: option.split)
    1.41 -apply (metis map_of_eq_None_iff option.simps(2) weak_map_of_SomeI)
    1.42 -by (metis Some_eq_map_of_iff map_of_eq_None_iff option.simps(2))
    1.43 -
    1.44 -lemma distinct_join_raw:
    1.45 -  assumes "distinct (map fst xs)"
    1.46 -  shows "distinct (map fst (join_raw f xs ys))"
    1.47 -using assms
    1.48 -proof (induct ys)
    1.49 -  case (Cons y ys)
    1.50 -  thus ?case by (cases y) (simp add: distinct_map_default)
    1.51 -qed auto
    1.52 -
    1.53 -definition
    1.54 -  "subtract_entries_raw xs ys = foldr (%(k, v). AList.map_entry k (%v'. v' - v)) ys xs"
    1.55 -
    1.56 -lemma map_of_subtract_entries_raw:
    1.57 -  assumes "distinct (map fst ys)"
    1.58 -  shows "map_of (subtract_entries_raw xs ys) x = (case map_of xs x of None => None | Some v =>
    1.59 -    (case map_of ys x of None => Some v | Some v' => Some (v - v')))"
    1.60 -using assms unfolding subtract_entries_raw_def
    1.61 -apply (induct ys)
    1.62 -apply auto
    1.63 -apply (simp split: option.split)
    1.64 -apply (simp add: map_of_map_entry)
    1.65 -apply (auto split: option.split)
    1.66 -apply (metis map_of_eq_None_iff option.simps(3) option.simps(4))
    1.67 -by (metis map_of_eq_None_iff option.simps(4) option.simps(5))
    1.68 -
    1.69 -lemma distinct_subtract_entries_raw:
    1.70 -  assumes "distinct (map fst xs)"
    1.71 -  shows "distinct (map fst (subtract_entries_raw xs ys))"
    1.72 -using assms
    1.73 -unfolding subtract_entries_raw_def by (induct ys) (auto simp add: distinct_map_entry)
    1.74 -
    1.75 -text {* Operations on alists with distinct keys *}
    1.76 -
    1.77 -lift_definition join :: "('a \<Rightarrow> 'b \<times> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist" 
    1.78 -is join_raw
    1.79 -by (simp add: distinct_join_raw)
    1.80 -
    1.81 -lift_definition subtract_entries :: "('a, ('b :: minus)) alist \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist"
    1.82 -is subtract_entries_raw 
    1.83 -by (simp add: distinct_subtract_entries_raw)
    1.84 -
    1.85 -text {* Implementing multisets by means of association lists *}
    1.86 -
    1.87 -definition count_of :: "('a \<times> nat) list \<Rightarrow> 'a \<Rightarrow> nat" where
    1.88 -  "count_of xs x = (case map_of xs x of None \<Rightarrow> 0 | Some n \<Rightarrow> n)"
    1.89 -
    1.90 -lemma count_of_multiset:
    1.91 -  "count_of xs \<in> multiset"
    1.92 -proof -
    1.93 -  let ?A = "{x::'a. 0 < (case map_of xs x of None \<Rightarrow> 0\<Colon>nat | Some (n\<Colon>nat) \<Rightarrow> n)}"
    1.94 -  have "?A \<subseteq> dom (map_of xs)"
    1.95 -  proof
    1.96 -    fix x
    1.97 -    assume "x \<in> ?A"
    1.98 -    then have "0 < (case map_of xs x of None \<Rightarrow> 0\<Colon>nat | Some (n\<Colon>nat) \<Rightarrow> n)" by simp
    1.99 -    then have "map_of xs x \<noteq> None" by (cases "map_of xs x") auto
   1.100 -    then show "x \<in> dom (map_of xs)" by auto
   1.101 -  qed
   1.102 -  with finite_dom_map_of [of xs] have "finite ?A"
   1.103 -    by (auto intro: finite_subset)
   1.104 -  then show ?thesis
   1.105 -    by (simp add: count_of_def fun_eq_iff multiset_def)
   1.106 -qed
   1.107 -
   1.108 -lemma count_simps [simp]:
   1.109 -  "count_of [] = (\<lambda>_. 0)"
   1.110 -  "count_of ((x, n) # xs) = (\<lambda>y. if x = y then n else count_of xs y)"
   1.111 -  by (simp_all add: count_of_def fun_eq_iff)
   1.112 -
   1.113 -lemma count_of_empty:
   1.114 -  "x \<notin> fst ` set xs \<Longrightarrow> count_of xs x = 0"
   1.115 -  by (induct xs) (simp_all add: count_of_def)
   1.116 -
   1.117 -lemma count_of_filter:
   1.118 -  "count_of (List.filter (P \<circ> fst) xs) x = (if P x then count_of xs x else 0)"
   1.119 -  by (induct xs) auto
   1.120 -
   1.121 -lemma count_of_map_default [simp]:
   1.122 -  "count_of (map_default x b (%x. x + b) xs) y = (if x = y then count_of xs x + b else count_of xs y)"
   1.123 -unfolding count_of_def by (simp add: map_of_map_default split: option.split)
   1.124 -
   1.125 -lemma count_of_join_raw:
   1.126 -  "distinct (map fst ys) ==> count_of xs x + count_of ys x = count_of (join_raw (%x (x, y). x + y) xs ys) x"
   1.127 -unfolding count_of_def by (simp add: map_of_join_raw split: option.split)
   1.128 -
   1.129 -lemma count_of_subtract_entries_raw:
   1.130 -  "distinct (map fst ys) ==> count_of xs x - count_of ys x = count_of (subtract_entries_raw xs ys) x"
   1.131 -unfolding count_of_def by (simp add: map_of_subtract_entries_raw split: option.split)
   1.132 -
   1.133 -text {* Code equations for multiset operations *}
   1.134 -
   1.135 -definition Bag :: "('a, nat) alist \<Rightarrow> 'a multiset" where
   1.136 -  "Bag xs = Abs_multiset (count_of (DAList.impl_of xs))"
   1.137 -
   1.138 -code_datatype Bag
   1.139 -
   1.140 -lemma count_Bag [simp, code]:
   1.141 -  "count (Bag xs) = count_of (DAList.impl_of xs)"
   1.142 -  by (simp add: Bag_def count_of_multiset Abs_multiset_inverse)
   1.143 -
   1.144 -lemma Mempty_Bag [code]:
   1.145 -  "{#} = Bag (DAList.empty)"
   1.146 -  by (simp add: multiset_eq_iff alist.Alist_inverse DAList.empty_def)
   1.147 -
   1.148 -lemma single_Bag [code]:
   1.149 -  "{#x#} = Bag (DAList.update x 1 DAList.empty)"
   1.150 -  by (simp add: multiset_eq_iff alist.Alist_inverse update.rep_eq empty.rep_eq)
   1.151 -
   1.152 -lemma union_Bag [code]:
   1.153 -  "Bag xs + Bag ys = Bag (join (\<lambda>x (n1, n2). n1 + n2) xs ys)"
   1.154 -by (rule multiset_eqI) (simp add: count_of_join_raw alist.Alist_inverse distinct_join_raw join_def)
   1.155 -
   1.156 -lemma minus_Bag [code]:
   1.157 -  "Bag xs - Bag ys = Bag (subtract_entries xs ys)"
   1.158 -by (rule multiset_eqI)
   1.159 -  (simp add: count_of_subtract_entries_raw alist.Alist_inverse distinct_subtract_entries_raw subtract_entries_def)
   1.160 -
   1.161 -lemma filter_Bag [code]:
   1.162 -  "Multiset.filter P (Bag xs) = Bag (DAList.filter (P \<circ> fst) xs)"
   1.163 -by (rule multiset_eqI) (simp add: count_of_filter DAList.filter.rep_eq)
   1.164 -
   1.165 -lemma mset_less_eq_Bag [code]:
   1.166 -  "Bag xs \<le> A \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). count_of (DAList.impl_of xs) x \<le> count A x)"
   1.167 -    (is "?lhs \<longleftrightarrow> ?rhs")
   1.168 -proof
   1.169 -  assume ?lhs then show ?rhs
   1.170 -    by (auto simp add: mset_le_def)
   1.171 -next
   1.172 -  assume ?rhs
   1.173 -  show ?lhs
   1.174 -  proof (rule mset_less_eqI)
   1.175 -    fix x
   1.176 -    from `?rhs` have "count_of (DAList.impl_of xs) x \<le> count A x"
   1.177 -      by (cases "x \<in> fst ` set (DAList.impl_of xs)") (auto simp add: count_of_empty)
   1.178 -    then show "count (Bag xs) x \<le> count A x"
   1.179 -      by (simp add: mset_le_def)
   1.180 -  qed
   1.181 -qed
   1.182 -
   1.183 -instantiation multiset :: (equal) equal
   1.184 -begin
   1.185 -
   1.186 -definition
   1.187 -  [code]: "HOL.equal A B \<longleftrightarrow> (A::'a multiset) \<le> B \<and> B \<le> A"
   1.188 -
   1.189 -instance
   1.190 -  by default (simp add: equal_multiset_def eq_iff)
   1.191 -
   1.192 -end
   1.193 -
   1.194 -text {* Quickcheck generators *}
   1.195 -
   1.196 -definition (in term_syntax)
   1.197 -  bagify :: "('a\<Colon>typerep, nat) alist \<times> (unit \<Rightarrow> Code_Evaluation.term)
   1.198 -    \<Rightarrow> 'a multiset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
   1.199 -  [code_unfold]: "bagify xs = Code_Evaluation.valtermify Bag {\<cdot>} xs"
   1.200 -
   1.201 -notation fcomp (infixl "\<circ>>" 60)
   1.202 -notation scomp (infixl "\<circ>\<rightarrow>" 60)
   1.203 -
   1.204 -instantiation multiset :: (random) random
   1.205 -begin
   1.206 -
   1.207 -definition
   1.208 -  "Quickcheck_Random.random i = Quickcheck_Random.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (bagify xs))"
   1.209 -
   1.210 -instance ..
   1.211 -
   1.212 -end
   1.213 -
   1.214 -no_notation fcomp (infixl "\<circ>>" 60)
   1.215 -no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
   1.216 -
   1.217 -instantiation multiset :: (exhaustive) exhaustive
   1.218 -begin
   1.219 -
   1.220 -definition exhaustive_multiset :: "('a multiset => (bool * term list) option) => natural => (bool * term list) option"
   1.221 -where
   1.222 -  "exhaustive_multiset f i = Quickcheck_Exhaustive.exhaustive (%xs. f (Bag xs)) i"
   1.223 -
   1.224 -instance ..
   1.225 -
   1.226 -end
   1.227 -
   1.228 -instantiation multiset :: (full_exhaustive) full_exhaustive
   1.229 -begin
   1.230 -
   1.231 -definition full_exhaustive_multiset :: "('a multiset * (unit => term) => (bool * term list) option) => natural => (bool * term list) option"
   1.232 -where
   1.233 -  "full_exhaustive_multiset f i = Quickcheck_Exhaustive.full_exhaustive (%xs. f (bagify xs)) i"
   1.234 -
   1.235 -instance ..
   1.236 -
   1.237 -end
   1.238 -
   1.239 -hide_const (open) bagify
   1.240 -
   1.241 -
   1.242  subsection {* The multiset order *}
   1.243  
   1.244  subsubsection {* Well-foundedness *}