1.1 --- a/src/HOL/Library/Multiset.thy	Thu Apr 12 07:33:14 2012 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Thu Apr 12 10:13:33 2012 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4    show "(\<lambda>x. 0::nat) \<in> {f. finite {x. f x > 0}}" by simp
     1.5  qed
     1.6  
     1.7 -lemmas multiset_typedef = Abs_multiset_inverse count_inverse count
     1.8 +setup_lifting type_definition_multiset
     1.9  
    1.10  abbreviation Melem :: "'a => 'a multiset => bool"  ("(_/ :# _)" [50, 51] 50) where
    1.11    "a :# M == 0 < count M a"
    1.12 @@ -82,21 +82,21 @@
    1.13  instantiation multiset :: (type) "{zero, plus}"
    1.14  begin
    1.15  
    1.16 -definition Mempty_def:
    1.17 -  "0 = Abs_multiset (\<lambda>a. 0)"
    1.18 +lift_definition zero_multiset :: "'a multiset" is "\<lambda>a. 0"
    1.19 +by (rule const0_in_multiset)
    1.20  
    1.21  abbreviation Mempty :: "'a multiset" ("{#}") where
    1.22    "Mempty \<equiv> 0"
    1.23  
    1.24 -definition union_def:
    1.25 -  "M + N = Abs_multiset (\<lambda>a. count M a + count N a)"
    1.26 +lift_definition plus_multiset :: "'a multiset => 'a multiset => 'a multiset" is "\<lambda>M N. (\<lambda>a. M a + N a)"
    1.27 +by (rule union_preserves_multiset)
    1.28  
    1.29  instance ..
    1.30  
    1.31  end
    1.32  
    1.33 -definition single :: "'a => 'a multiset" where
    1.34 -  "single a = Abs_multiset (\<lambda>b. if b = a then 1 else 0)"
    1.35 +lift_definition single :: "'a => 'a multiset" is "\<lambda>a b. if b = a then 1 else 0"
    1.36 +by (rule only1_in_multiset)
    1.37  
    1.38  syntax
    1.39    "_multiset" :: "args => 'a multiset"    ("{#(_)#}")
    1.40 @@ -105,10 +105,10 @@
    1.41    "{#x#}" == "CONST single x"
    1.42  
    1.43  lemma count_empty [simp]: "count {#} a = 0"
    1.44 -  by (simp add: Mempty_def in_multiset multiset_typedef)
    1.45 +  by (simp add: zero_multiset.rep_eq)
    1.46  
    1.47  lemma count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)"
    1.48 -  by (simp add: single_def in_multiset multiset_typedef)
    1.49 +  by (simp add: single.rep_eq)
    1.50  
    1.51  
    1.52  subsection {* Basic operations *}
    1.53 @@ -116,7 +116,7 @@
    1.54  subsubsection {* Union *}
    1.55  
    1.56  lemma count_union [simp]: "count (M + N) a = count M a + count N a"
    1.57 -  by (simp add: union_def in_multiset multiset_typedef)
    1.58 +  by (simp add: plus_multiset.rep_eq)
    1.59  
    1.60  instance multiset :: (type) cancel_comm_monoid_add
    1.61    by default (simp_all add: multiset_eq_iff)
    1.62 @@ -127,15 +127,15 @@
    1.63  instantiation multiset :: (type) minus
    1.64  begin
    1.65  
    1.66 -definition diff_def:
    1.67 -  "M - N = Abs_multiset (\<lambda>a. count M a - count N a)"
    1.68 -
    1.69 +lift_definition minus_multiset :: "'a multiset => 'a multiset => 'a multiset" is "\<lambda> M N. \<lambda>a. M a - N a"
    1.70 +by (rule diff_preserves_multiset)
    1.71 + 
    1.72  instance ..
    1.73  
    1.74  end
    1.75  
    1.76  lemma count_diff [simp]: "count (M - N) a = count M a - count N a"
    1.77 -  by (simp add: diff_def in_multiset multiset_typedef)
    1.78 +  by (simp add: minus_multiset.rep_eq)
    1.79  
    1.80  lemma diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
    1.81  by(simp add: multiset_eq_iff)
    1.82 @@ -264,8 +264,9 @@
    1.83  instantiation multiset :: (type) ordered_ab_semigroup_add_imp_le
    1.84  begin
    1.85  
    1.86 -definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
    1.87 -  mset_le_def: "A \<le> B \<longleftrightarrow> (\<forall>a. count A a \<le> count B a)"
    1.88 +lift_definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" is "\<lambda> A B. (\<forall>a. A a \<le> B a)"
    1.89 +by simp
    1.90 +lemmas mset_le_def = less_eq_multiset_def
    1.91  
    1.92  definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
    1.93    mset_less_def: "(A::'a multiset) < B \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
    1.94 @@ -391,7 +392,7 @@
    1.95  
    1.96  lemma multiset_inter_count [simp]:
    1.97    "count (A #\<inter> B) x = min (count A x) (count B x)"
    1.98 -  by (simp add: multiset_inter_def multiset_typedef)
    1.99 +  by (simp add: multiset_inter_def)
   1.100  
   1.101  lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
   1.102    by (rule multiset_eqI) auto
   1.103 @@ -414,14 +415,14 @@
   1.104  
   1.105  text {* Multiset comprehension *}
   1.106  
   1.107 -definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
   1.108 -  "filter P M = Abs_multiset (\<lambda>x. if P x then count M x else 0)"
   1.109 +lift_definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is "\<lambda>P M. \<lambda>x. if P x then M x else 0"
   1.110 +by (rule filter_preserves_multiset)
   1.111  
   1.112  hide_const (open) filter
   1.113  
   1.114  lemma count_filter [simp]:
   1.115    "count (Multiset.filter P M) a = (if P a then count M a else 0)"
   1.116 -  by (simp add: filter_def in_multiset multiset_typedef)
   1.117 +  by (simp add: filter.rep_eq)
   1.118  
   1.119  lemma filter_empty [simp]:
   1.120    "Multiset.filter P {#} = {#}"
   1.121 @@ -593,7 +594,7 @@
   1.122    and add: "!!M x. P M ==> P (M + {#x#})"
   1.123  shows "P M"
   1.124  proof -
   1.125 -  note defns = union_def single_def Mempty_def
   1.126 +  note defns = plus_multiset_def single_def zero_multiset_def
   1.127    note add' = add [unfolded defns, simplified]
   1.128    have aux: "\<And>a::'a. count (Abs_multiset (\<lambda>b. if b = a then 1 else 0)) =
   1.129      (\<lambda>b. if b = a then 1 else 0)" by (simp add: Abs_multiset_inverse in_multiset) 
   1.130 @@ -1073,7 +1074,8 @@
   1.131  
   1.132  lemma map_of_join_raw:
   1.133    assumes "distinct (map fst ys)"
   1.134 -  shows "map_of (join_raw f xs ys) x = (case map_of xs x of None => map_of ys x | Some v => (case map_of ys x of None => Some v | Some v' => Some (f x (v, v'))))"
   1.135 +  shows "map_of (join_raw f xs ys) x = (case map_of xs x of None => map_of ys x | Some v =>
   1.136 +    (case map_of ys x of None => Some v | Some v' => Some (f x (v, v'))))"
   1.137  using assms
   1.138  apply (induct ys)
   1.139  apply (auto simp add: map_of_map_default split: option.split)
   1.140 @@ -1093,8 +1095,10 @@
   1.141    "subtract_entries_raw xs ys = foldr (%(k, v). AList.map_entry k (%v'. v' - v)) ys xs"
   1.142  
   1.143  lemma map_of_subtract_entries_raw:
   1.144 -  "distinct (map fst ys) ==> map_of (subtract_entries_raw xs ys) x = (case map_of xs x of None => None | Some v => (case map_of ys x of None => Some v | Some v' => Some (v - v')))"
   1.145 -unfolding subtract_entries_raw_def
   1.146 +  assumes "distinct (map fst ys)"
   1.147 +  shows "map_of (subtract_entries_raw xs ys) x = (case map_of xs x of None => None | Some v =>
   1.148 +    (case map_of ys x of None => Some v | Some v' => Some (v - v')))"
   1.149 +using assms unfolding subtract_entries_raw_def
   1.150  apply (induct ys)
   1.151  apply auto
   1.152  apply (simp split: option.split)
   1.153 @@ -1197,7 +1201,7 @@
   1.154  
   1.155  lemma filter_Bag [code]:
   1.156    "Multiset.filter P (Bag xs) = Bag (DAList.filter (P \<circ> fst) xs)"
   1.157 -by (rule multiset_eqI) (simp add: count_of_filter filter.rep_eq)
   1.158 +by (rule multiset_eqI) (simp add: count_of_filter DAList.filter.rep_eq)
   1.159  
   1.160  lemma mset_less_eq_Bag [code]:
   1.161    "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)"