src/HOL/ex/Sorting.thy

     Copyright   1994 TU Muenchen
 
 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"
   "sorted1 le (x#xs) = ((case xs of [] => True | y#ys => le x y) &
                         sorted1 le xs)"
 
 primrec
   "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"
    "total r == (ALL x y. r x y | r y x)"
   
   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' *)
 
 lemma sorted1_is_sorted:
  "transf(le) ==> sorted1 le xs = sorted le xs";