author bulwahn Thu Apr 12 10:13:33 2012 +0200 (2012-04-12) changeset 47429 ec64d94cbf9c parent 47428 45b58fec9024 child 47430 b254fdaf1973 child 47436 d8fad618a67a
multiset operations are defined with lift_definitions;
tuned proofs;
```     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)"
```