author | wenzelm |
Sat, 09 Jul 2011 21:53:27 +0200 | |
changeset 43721 | fad8634cee62 |
parent 41959 | b460124855b8 |
permissions | -rw-r--r-- |
41959 | 1 |
(* Title: HOL/ex/Sorting.thy |
1476 | 2 |
Author: Tobias Nipkow |
969 | 3 |
Copyright 1994 TU Muenchen |
4 |
*) |
|
5 |
||
15815 | 6 |
header{*Sorting: Basic Theory*} |
7 |
||
8 |
theory Sorting |
|
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
21404
diff
changeset
|
9 |
imports Main "~~/src/HOL/Library/Multiset" |
15815 | 10 |
begin |
13159 | 11 |
|
969 | 12 |
consts |
13159 | 13 |
sorted1:: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" |
14 |
sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" |
|
969 | 15 |
|
5184 | 16 |
primrec |
2517 | 17 |
"sorted1 le [] = True" |
18 |
"sorted1 le (x#xs) = ((case xs of [] => True | y#ys => le x y) & |
|
19 |
sorted1 le xs)" |
|
969 | 20 |
|
5184 | 21 |
primrec |
2517 | 22 |
"sorted le [] = True" |
15815 | 23 |
"sorted le (x#xs) = ((\<forall>y \<in> set xs. le x y) & sorted le xs)" |
969 | 24 |
|
25 |
||
19736 | 26 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset
|
27 |
total :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool" where |
19736 | 28 |
"total r = (\<forall>x y. r x y | r y x)" |
8415 | 29 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset
|
30 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19736
diff
changeset
|
31 |
transf :: "('a \<Rightarrow> 'a \<Rightarrow> bool) => bool" where |
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 |