src/HOL/ex/Sorting.thy
 author wenzelm Fri, 17 Nov 2006 02:20:03 +0100 changeset 21404 eb85850d3eb7 parent 19736 d8d0f8f51d69 child 41413 64cd30d6b0b8 permissions -rw-r--r--
more robust syntax for definition/abbreviation/notation;
```
(*  Title:      HOL/ex/sorting.thy
ID:         \$Id\$
Author:     Tobias Nipkow
*)

theory Sorting
imports Main Multiset
begin

consts
sorted1:: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"

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) = ((\<forall>y \<in> set xs. le x y) & sorted le xs)"

definition
total  :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool" where
"total r = (\<forall>x y. r x y | r y x)"

definition
transf :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool" where
"transf f = (\<forall>x y z. f x y & f y z --> f x z)"

(* 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 & sorted le ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. le x y))"
by (induct xs) auto

end
```