changing more definitions to quotient_definition
Wed, 28 Mar 2012 10:16:02 +0200
changeset 47179 54b38de0620e
parent 47178 2ae2b6fa9c84
child 47180 c14fda8fee38
changing more definitions to quotient_definition
--- a/src/HOL/Library/Multiset.thy	Wed Mar 28 10:02:22 2012 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed Mar 28 10:16:02 2012 +0200
@@ -1109,23 +1109,17 @@
 using assms
 unfolding subtract_entries_raw_def by (induct ys) (auto simp add: distinct_map_entry)
-text {* Operations on alists *}
-definition join
-  "join f xs ys = DAList.Alist (join_raw f (DAList.impl_of xs) (DAList.impl_of ys))" 
+text {* Operations on alists with distinct keys *}
-lemma [code abstract]:
-  "DAList.impl_of (join f xs ys) = join_raw f (DAList.impl_of xs) (DAList.impl_of ys)"
-unfolding join_def by (simp add: Alist_inverse distinct_join_raw)
-definition subtract_entries
+quotient_definition join :: "('a \<Rightarrow> 'b \<times> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist" 
-  "subtract_entries xs ys = DAList.Alist (subtract_entries_raw (DAList.impl_of xs) (DAList.impl_of ys))"
+  "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"
+by (simp add: distinct_join_raw)
-lemma [code abstract]:
-  "DAList.impl_of (subtract_entries xs ys) = subtract_entries_raw (DAList.impl_of xs) (DAList.impl_of ys)"
-unfolding subtract_entries_def by (simp add: Alist_inverse distinct_subtract_entries_raw)
+quotient_definition subtract_entries :: "('a, ('b :: minus)) alist \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist"
+  "subtract_entries" is "subtract_entries_raw :: ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b) list" 
+by (simp add: distinct_subtract_entries_raw)
 text {* Implementing multisets by means of association lists *}