changing more definitions to quotient_definition
authorbulwahn
Wed Mar 28 10:16:02 2012 +0200 (2012-03-28)
changeset 4717954b38de0620e
parent 47178 2ae2b6fa9c84
child 47180 c14fda8fee38
changing more definitions to quotient_definition
src/HOL/Library/Multiset.thy
     1.1 --- a/src/HOL/Library/Multiset.thy	Wed Mar 28 10:02:22 2012 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Wed Mar 28 10:16:02 2012 +0200
     1.3 @@ -1109,23 +1109,17 @@
     1.4  using assms
     1.5  unfolding subtract_entries_raw_def by (induct ys) (auto simp add: distinct_map_entry)
     1.6  
     1.7 -text {* Operations on alists *}
     1.8 -
     1.9 -definition join
    1.10 -where
    1.11 -  "join f xs ys = DAList.Alist (join_raw f (DAList.impl_of xs) (DAList.impl_of ys))" 
    1.12 +text {* Operations on alists with distinct keys *}
    1.13  
    1.14 -lemma [code abstract]:
    1.15 -  "DAList.impl_of (join f xs ys) = join_raw f (DAList.impl_of xs) (DAList.impl_of ys)"
    1.16 -unfolding join_def by (simp add: Alist_inverse distinct_join_raw)
    1.17 -
    1.18 -definition subtract_entries
    1.19 +quotient_definition join :: "('a \<Rightarrow> 'b \<times> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist" 
    1.20  where
    1.21 -  "subtract_entries xs ys = DAList.Alist (subtract_entries_raw (DAList.impl_of xs) (DAList.impl_of ys))"
    1.22 +  "join" is "join_raw :: ('a \<Rightarrow> 'b \<times> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b) list"
    1.23 +by (simp add: distinct_join_raw)
    1.24  
    1.25 -lemma [code abstract]:
    1.26 -  "DAList.impl_of (subtract_entries xs ys) = subtract_entries_raw (DAList.impl_of xs) (DAList.impl_of ys)"
    1.27 -unfolding subtract_entries_def by (simp add: Alist_inverse distinct_subtract_entries_raw)
    1.28 +quotient_definition subtract_entries :: "('a, ('b :: minus)) alist \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist"
    1.29 +where
    1.30 +  "subtract_entries" is "subtract_entries_raw :: ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b) list" 
    1.31 +by (simp add: distinct_subtract_entries_raw)
    1.32  
    1.33  text {* Implementing multisets by means of association lists *}
    1.34