src/HOL/ex/Sorting.thy

lucas - fixed bug with name capture variables bound outside redex could (previously)conflict with scheme variables that occur in the conditions of an equation, and which were renamed to avoid conflict with another instantiation. This has now been fixed.

(*  Title:      HOL/ex/sorting.thy
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   1994 TU Muenchen

Specification of sorting
*)

theory Sorting = Main:

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";
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