src/HOL/ex/Sorting.thy

--- a/src/HOL/ex/Sorting.thy	Fri May 17 11:36:32 2002 +0200
+++ b/src/HOL/ex/Sorting.thy	Fri May 17 15:40:59 2002 +0200
@@ -6,11 +6,12 @@
 Specification of sorting
 *)
 
-Sorting = Main +
+theory Sorting = Main:
+
 consts
-  sorted1:: [['a,'a] => bool, 'a list] => bool
-  sorted :: [['a,'a] => bool, 'a list] => bool
-  multiset   :: 'a list => ('a => nat)
+  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"
@@ -26,10 +27,39 @@
   "multiset (x#xs) y = (if x=y then Suc(multiset xs y) else multiset xs y)"
 
 constdefs
-  total  :: (['a,'a] => bool) => bool
+  total  :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool"
    "total r == (ALL x y. r x y | r y x)"
   
-  transf :: (['a,'a] => bool) => bool
+  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";
+apply(induct xs)
+ apply simp
+apply(simp split: list.split)
+apply(unfold transf_def);
+apply(blast)
+done
+
+lemma sorted_append[simp]:
+ "sorted le (xs@ys) = (sorted le xs \<and> sorted le ys \<and>
+                       (\<forall>x \<in> set xs. \<forall>y \<in> set ys. le x y))"
+by (induct xs, auto)
+
 end