1476
|
1 |
(* Title: HOL/ex/sorting.thy
|
969
|
2 |
ID: $Id$
|
1476
|
3 |
Author: Tobias Nipkow
|
969
|
4 |
Copyright 1994 TU Muenchen
|
|
5 |
*)
|
|
6 |
|
15815
|
7 |
header{*Sorting: Basic Theory*}
|
|
8 |
|
|
9 |
theory Sorting
|
|
10 |
imports Main Multiset
|
|
11 |
begin
|
13159
|
12 |
|
969
|
13 |
consts
|
13159
|
14 |
sorted1:: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
|
|
15 |
sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
|
969
|
16 |
|
5184
|
17 |
primrec
|
2517
|
18 |
"sorted1 le [] = True"
|
|
19 |
"sorted1 le (x#xs) = ((case xs of [] => True | y#ys => le x y) &
|
|
20 |
sorted1 le xs)"
|
969
|
21 |
|
5184
|
22 |
primrec
|
2517
|
23 |
"sorted le [] = True"
|
15815
|
24 |
"sorted le (x#xs) = ((\<forall>y \<in> set xs. le x y) & sorted le xs)"
|
969
|
25 |
|
|
26 |
|
19736
|
27 |
definition
|
13159
|
28 |
total :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool"
|
19736
|
29 |
"total r = (\<forall>x y. r x y | r y x)"
|
8415
|
30 |
|
13159
|
31 |
transf :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool"
|
19736
|
32 |
"transf f = (\<forall>x y z. f x y & f y z --> f x z)"
|
8415
|
33 |
|
13159
|
34 |
|
|
35 |
|
|
36 |
(* Equivalence of two definitions of `sorted' *)
|
|
37 |
|
15815
|
38 |
lemma sorted1_is_sorted: "transf(le) ==> sorted1 le xs = sorted le xs";
|
13159
|
39 |
apply(induct xs)
|
|
40 |
apply simp
|
|
41 |
apply(simp split: list.split)
|
|
42 |
apply(unfold transf_def);
|
|
43 |
apply(blast)
|
|
44 |
done
|
|
45 |
|
15815
|
46 |
lemma sorted_append [simp]:
|
19736
|
47 |
"sorted le (xs@ys) =
|
|
48 |
(sorted le xs & sorted le ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. le x y))"
|
|
49 |
by (induct xs) auto
|
13159
|
50 |
|
969
|
51 |
end
|