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
     1 (*  Title:      HOL/ex/sorting.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1994 TU Muenchen
     5 
     6 Specification of sorting
     7 *)
     8 
     9 Sorting = List +
    10 consts
    11   sorted1:: [['a,'a] => bool, 'a list] => bool
    12   sorted :: [['a,'a] => bool, 'a list] => bool
    13   mset   :: 'a list => ('a => nat)
    14   total  :: (['a,'a] => bool) => bool
    15   transf :: (['a,'a] => bool) => bool
    16 
    17 primrec sorted1 list
    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 sorted list
    23   "sorted le [] = True"
    24   "sorted le (x#xs) = ((!y:set xs. le x y) & sorted le xs)"
    25 
    26 primrec mset list
    27   "mset [] y = 0"
    28   "mset (x#xs) y = (if x=y then Suc(mset xs y) else mset xs y)"
    29 
    30 defs
    31 total_def  "total r == (!x y. r x y | r y x)"
    32 transf_def "transf f == (!x y z. f x y & f y z --> f x z)"
    33 end