src/HOL/ex/Sorting.thy
author wenzelm
Fri Nov 17 02:20:03 2006 +0100 (2006-11-17)
changeset 21404 eb85850d3eb7
parent 19736 d8d0f8f51d69
child 41413 64cd30d6b0b8
permissions -rw-r--r--
more robust syntax for definition/abbreviation/notation;
     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