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