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