author kleing Sat Mar 26 00:01:56 2005 +0100 (2005-03-26) changeset 15631 cbee04ce413b parent 15630 cc3776f004e2 child 15632 bb178a7a69c1
use Library/Multiset instead of own definition
 src/HOL/ex/InSort.thy file | annotate | diff | revisions src/HOL/ex/MergeSort.thy file | annotate | diff | revisions src/HOL/ex/Qsort.thy file | annotate | diff | revisions src/HOL/ex/Sorting.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/ex/InSort.thy	Sat Mar 26 00:00:56 2005 +0100
1.2 +++ b/src/HOL/ex/InSort.thy	Sat Mar 26 00:01:56 2005 +0100
1.3 @@ -22,15 +22,15 @@
1.4
1.5
1.6  lemma multiset_ins[simp]:
1.7 - "\<And>y. multiset(ins le x xs) y = multiset (x#xs) y"
1.8 -by (induct "xs") auto
1.9 + "\<And>y. multiset_of (ins le x xs) = multiset_of (x#xs)"
1.10 +  by (induct xs) (auto simp: union_ac)
1.11
1.12  lemma insort_permutes[simp]:
1.13 - "\<And>x. multiset(insort le xs) x = multiset xs x";
1.14 -by (induct "xs") auto
1.15 + "\<And>x. multiset_of (insort le xs) = multiset_of xs"
1.16 +  by (induct "xs") auto
1.17
1.18  lemma set_ins[simp]: "set(ins le x xs) = insert x (set xs)"
1.19 -by (simp add: set_via_multiset) fast
1.20 +  by (simp add: set_count_greater_0) fast
1.21
1.22  lemma sorted_ins[simp]:
1.23   "\<lbrakk> total le; transf le \<rbrakk> \<Longrightarrow> sorted le (ins le x xs) = sorted le xs";
```
```     2.1 --- a/src/HOL/ex/MergeSort.thy	Sat Mar 26 00:00:56 2005 +0100
2.2 +++ b/src/HOL/ex/MergeSort.thy	Sat Mar 26 00:01:56 2005 +0100
2.3 @@ -16,9 +16,9 @@
2.4  "merge(xs,[]) = xs"
2.5  "merge([],ys) = ys"
2.6
2.7 -lemma [simp]: "multiset(merge(xs,ys)) x = multiset xs x + multiset ys x"
2.8 +lemma [simp]: "multiset_of (merge(xs,ys)) = multiset_of xs + multiset_of ys"
2.9  apply(induct xs ys rule: merge.induct)
2.10 -apply auto
2.11 +apply (auto simp: union_ac)
2.12  done
2.13
2.14  lemma [simp]: "set(merge(xs,ys)) = set xs \<union> set ys"
2.15 @@ -43,11 +43,14 @@
2.16  lemma "sorted op <= (msort xs)"
2.17  by (induct xs rule: msort.induct) simp_all
2.18
2.19 -lemma "multiset(msort xs) x = multiset xs x"
2.20 +lemma "multiset_of (msort xs) = multiset_of xs"
2.21  apply (induct xs rule: msort.induct)
2.22    apply simp
2.23   apply simp
2.25 +apply simp
2.26 +apply (subst union_commute)
2.27 +apply (simp del:multiset_of_append add:multiset_of_append[symmetric] union_assoc)
2.29  done
2.30
2.31  end
```
```     3.1 --- a/src/HOL/ex/Qsort.thy	Sat Mar 26 00:00:56 2005 +0100
3.2 +++ b/src/HOL/ex/Qsort.thy	Sat Mar 26 00:01:56 2005 +0100
3.3 @@ -18,13 +18,12 @@
3.4  (hints recdef_simp: length_filter_le[THEN le_less_trans])
3.5
3.6  lemma qsort_permutes[simp]:
3.7 - "multiset (qsort(le,xs)) x = multiset xs x"
3.8 -by (induct le xs rule: qsort.induct, auto)
3.9 -
3.10 + "multiset_of (qsort(le,xs)) = multiset_of xs"
3.11 +by (induct le xs rule: qsort.induct) (auto simp: union_ac)
3.12
3.13  (*Also provable by induction*)
3.14  lemma set_qsort[simp]: "set (qsort(le,xs)) = set xs";
3.17
3.18  lemma sorted_qsort:
3.19   "total(le) ==> transf(le) ==> sorted le (qsort(le,xs))"
3.20 @@ -46,12 +45,12 @@
3.21  (hints recdef_simp: length_filter_le[THEN le_less_trans])
3.22
3.23  lemma quickSort_permutes[simp]:
3.24 - "multiset (quickSort xs) z = multiset xs z"
3.25 -by (induct xs rule: quickSort.induct) auto
3.26 + "multiset_of (quickSort xs) = multiset_of xs"
3.27 +by (induct xs rule: quickSort.induct) (auto simp: union_ac)
3.28
3.29  (*Also provable by induction*)
3.30  lemma set_quickSort[simp]: "set (quickSort xs) = set xs"
3.33
3.34  lemma sorted_quickSort: "sorted (op <=) (quickSort xs)"
3.35  apply (induct xs rule: quickSort.induct)
```
```     4.1 --- a/src/HOL/ex/Sorting.thy	Sat Mar 26 00:00:56 2005 +0100
4.2 +++ b/src/HOL/ex/Sorting.thy	Sat Mar 26 00:01:56 2005 +0100
4.3 @@ -6,12 +6,11 @@
4.4  Specification of sorting
4.5  *)
4.6
4.7 -theory Sorting = Main:
4.8 +theory Sorting = Main + Multiset:
4.9
4.10  consts
4.11    sorted1:: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
4.12    sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
4.13 -  multiset   :: "'a list => ('a => nat)"
4.14
4.15  primrec
4.16    "sorted1 le [] = True"
4.17 @@ -22,9 +21,6 @@
4.18    "sorted le [] = True"
4.19    "sorted le (x#xs) = ((!y:set xs. le x y) & sorted le xs)"
4.20
4.21 -primrec
4.22 -  "multiset [] y = 0"
4.23 -  "multiset (x#xs) y = (if x=y then Suc(multiset xs y) else multiset xs y)"
4.24
4.25  constdefs
4.26    total  :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool"
4.27 @@ -33,18 +29,7 @@
4.28    transf :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool"
4.29     "transf f == (ALL x y z. f x y & f y z --> f x z)"
4.30
4.31 -(* Some general lemmas *)
4.32
4.33 -lemma multiset_append[simp]:
4.34 - "multiset (xs@ys) x = multiset xs x + multiset ys x"
4.35 -by (induct xs, auto)
4.36 -
4.38 - "multiset [x:xs. ~p(x)] z + multiset [x:xs. p(x)] z = multiset xs z";
4.39 -by (induct xs, auto)
4.40 -
4.41 -lemma set_via_multiset: "set xs = {x. multiset xs x ~= 0}";
4.42 -by (induct xs, auto)
4.43
4.44  (* Equivalence of two definitions of `sorted' *)
4.45
```