# HG changeset patch
# User kleing
# Date 1111791716 -3600
# Node ID cbee04ce413b61a2188ebc0addd42e263a89dda8
# Parent  cc3776f004e298e8d04f78e7cc531a6eb2051e65
use Library/Multiset instead of own definition

diff -r cc3776f004e2 -r cbee04ce413b src/HOL/ex/InSort.thy
--- a/src/HOL/ex/InSort.thy	Sat Mar 26 00:00:56 2005 +0100
+++ b/src/HOL/ex/InSort.thy	Sat Mar 26 00:01:56 2005 +0100
@@ -22,15 +22,15 @@
 
 
 lemma multiset_ins[simp]:
- "\<And>y. multiset(ins le x xs) y = multiset (x#xs) y"
-by (induct "xs") auto
+ "\<And>y. multiset_of (ins le x xs) = multiset_of (x#xs)"
+  by (induct xs) (auto simp: union_ac)
 
 lemma insort_permutes[simp]:
- "\<And>x. multiset(insort le xs) x = multiset xs x";
-by (induct "xs") auto
+ "\<And>x. multiset_of (insort le xs) = multiset_of xs"
+  by (induct "xs") auto
 
 lemma set_ins[simp]: "set(ins le x xs) = insert x (set xs)"
-by (simp add: set_via_multiset) fast
+  by (simp add: set_count_greater_0) fast
 
 lemma sorted_ins[simp]:
  "\<lbrakk> total le; transf le \<rbrakk> \<Longrightarrow> sorted le (ins le x xs) = sorted le xs";
diff -r cc3776f004e2 -r cbee04ce413b src/HOL/ex/MergeSort.thy
--- a/src/HOL/ex/MergeSort.thy	Sat Mar 26 00:00:56 2005 +0100
+++ b/src/HOL/ex/MergeSort.thy	Sat Mar 26 00:01:56 2005 +0100
@@ -16,9 +16,9 @@
 "merge(xs,[]) = xs"
 "merge([],ys) = ys"
 
-lemma [simp]: "multiset(merge(xs,ys)) x = multiset xs x + multiset ys x"
+lemma [simp]: "multiset_of (merge(xs,ys)) = multiset_of xs + multiset_of ys"
 apply(induct xs ys rule: merge.induct)
-apply auto
+apply (auto simp: union_ac)
 done
 
 lemma [simp]: "set(merge(xs,ys)) = set xs \<union> set ys"
@@ -43,11 +43,14 @@
 lemma "sorted op <= (msort xs)"
 by (induct xs rule: msort.induct) simp_all
 
-lemma "multiset(msort xs) x = multiset xs x"
+lemma "multiset_of (msort xs) = multiset_of xs"
 apply (induct xs rule: msort.induct)
   apply simp
  apply simp
-apply (simp del:multiset_append add:multiset_append[symmetric])
+apply simp
+apply (subst union_commute)
+apply (simp del:multiset_of_append add:multiset_of_append[symmetric] union_assoc)
+apply (simp add: union_ac)
 done
 
 end
diff -r cc3776f004e2 -r cbee04ce413b src/HOL/ex/Qsort.thy
--- a/src/HOL/ex/Qsort.thy	Sat Mar 26 00:00:56 2005 +0100
+++ b/src/HOL/ex/Qsort.thy	Sat Mar 26 00:01:56 2005 +0100
@@ -18,13 +18,12 @@
 (hints recdef_simp: length_filter_le[THEN le_less_trans])
 
 lemma qsort_permutes[simp]:
- "multiset (qsort(le,xs)) x = multiset xs x"
-by (induct le xs rule: qsort.induct, auto)
-
+ "multiset_of (qsort(le,xs)) = multiset_of xs"
+by (induct le xs rule: qsort.induct) (auto simp: union_ac)
 
 (*Also provable by induction*)
 lemma set_qsort[simp]: "set (qsort(le,xs)) = set xs";
-by(simp add: set_via_multiset)
+by(simp add: set_count_greater_0)
 
 lemma sorted_qsort:
  "total(le) ==> transf(le) ==> sorted le (qsort(le,xs))"
@@ -46,12 +45,12 @@
 (hints recdef_simp: length_filter_le[THEN le_less_trans])
 
 lemma quickSort_permutes[simp]:
- "multiset (quickSort xs) z = multiset xs z"
-by (induct xs rule: quickSort.induct) auto
+ "multiset_of (quickSort xs) = multiset_of xs"
+by (induct xs rule: quickSort.induct) (auto simp: union_ac)
 
 (*Also provable by induction*)
 lemma set_quickSort[simp]: "set (quickSort xs) = set xs"
-by(simp add: set_via_multiset)
+by(simp add: set_count_greater_0)
 
 lemma sorted_quickSort: "sorted (op <=) (quickSort xs)"
 apply (induct xs rule: quickSort.induct)
diff -r cc3776f004e2 -r cbee04ce413b src/HOL/ex/Sorting.thy
--- a/src/HOL/ex/Sorting.thy	Sat Mar 26 00:00:56 2005 +0100
+++ b/src/HOL/ex/Sorting.thy	Sat Mar 26 00:01:56 2005 +0100
@@ -6,12 +6,11 @@
 Specification of sorting
 *)
 
-theory Sorting = Main:
+theory Sorting = Main + Multiset:
 
 consts
   sorted1:: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
   sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
-  multiset   :: "'a list => ('a => nat)"
 
 primrec
   "sorted1 le [] = True"
@@ -22,9 +21,6 @@
   "sorted le [] = True"
   "sorted le (x#xs) = ((!y:set xs. le x y) & sorted le xs)"
 
-primrec
-  "multiset [] y = 0"
-  "multiset (x#xs) y = (if x=y then Suc(multiset xs y) else multiset xs y)"
 
 constdefs
   total  :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool"
@@ -33,18 +29,7 @@
   transf :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool"
    "transf f == (ALL x y z. f x y & f y z --> f x z)"
 
-(* Some general lemmas *)
 
-lemma multiset_append[simp]:
- "multiset (xs@ys) x = multiset xs x + multiset ys x"
-by (induct xs, auto)
-
-lemma multiset_compl_add[simp]:
- "multiset [x:xs. ~p(x)] z + multiset [x:xs. p(x)] z = multiset xs z";
-by (induct xs, auto)
-
-lemma set_via_multiset: "set xs = {x. multiset xs x ~= 0}";
-by (induct xs, auto)
 
 (* Equivalence of two definitions of `sorted' *)