use Library/Multiset instead of own definition
authorkleing
Sat Mar 26 00:01:56 2005 +0100 (2005-03-26 ago)
changeset 15631cbee04ce413b
parent 15630 cc3776f004e2
child 15632 bb178a7a69c1
use Library/Multiset instead of own definition
src/HOL/ex/InSort.thy
src/HOL/ex/MergeSort.thy
src/HOL/ex/Qsort.thy
src/HOL/ex/Sorting.thy
     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.24 -apply (simp del:multiset_append add:multiset_append[symmetric])
    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.28 +apply (simp add: union_ac)
    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.15 -by(simp add: set_via_multiset)
    3.16 +by(simp add: set_count_greater_0)
    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.31 -by(simp add: set_via_multiset)
    3.32 +by(simp add: set_count_greater_0)
    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.37 -lemma multiset_compl_add[simp]:
    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