src/HOL/ex/Sorting.thy
author paulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153 e534c4c32d54
parent 3465 e85c24717cad
child 5184 9b8547a9496a
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
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
Specification of sorting
clasohm@969
     7
*)
clasohm@969
     8
clasohm@969
     9
Sorting = List +
clasohm@969
    10
consts
clasohm@1376
    11
  sorted1:: [['a,'a] => bool, 'a list] => bool
clasohm@1376
    12
  sorted :: [['a,'a] => bool, 'a list] => bool
clasohm@1376
    13
  mset   :: 'a list => ('a => nat)
clasohm@1376
    14
  total  :: (['a,'a] => bool) => bool
clasohm@1376
    15
  transf :: (['a,'a] => bool) => bool
clasohm@969
    16
nipkow@2517
    17
primrec sorted1 list
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
nipkow@2517
    22
primrec sorted list
nipkow@2517
    23
  "sorted le [] = True"
nipkow@3465
    24
  "sorted le (x#xs) = ((!y:set xs. le x y) & sorted le xs)"
clasohm@969
    25
nipkow@2517
    26
primrec mset list
nipkow@2517
    27
  "mset [] y = 0"
nipkow@2517
    28
  "mset (x#xs) y = (if x=y then Suc(mset xs y) else mset xs y)"
clasohm@969
    29
nipkow@2517
    30
defs
clasohm@969
    31
total_def  "total r == (!x y. r x y | r y x)"
clasohm@969
    32
transf_def "transf f == (!x y z. f x y & f y z --> f x z)"
clasohm@969
    33
end