src/HOL/ex/Sorting.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 8415 852c63072334
child 13159 2af7b94892ce
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1376
diff changeset
     1
(*  Title:      HOL/ex/sorting.thy
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1376
diff changeset
     3
    Author:     Tobias Nipkow
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1994 TU Muenchen
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     5
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     6
Specification of sorting
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     7
*)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     8
8415
paulson
parents: 5184
diff changeset
     9
Sorting = Main +
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    10
consts
1376
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 969
diff changeset
    11
  sorted1:: [['a,'a] => bool, 'a list] => bool
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 969
diff changeset
    12
  sorted :: [['a,'a] => bool, 'a list] => bool
8415
paulson
parents: 5184
diff changeset
    13
  multiset   :: 'a list => ('a => nat)
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    14
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 3465
diff changeset
    15
primrec
2517
2af078382853 Modified some defs and shortened proofs.
nipkow
parents: 2511
diff changeset
    16
  "sorted1 le [] = True"
2af078382853 Modified some defs and shortened proofs.
nipkow
parents: 2511
diff changeset
    17
  "sorted1 le (x#xs) = ((case xs of [] => True | y#ys => le x y) &
2af078382853 Modified some defs and shortened proofs.
nipkow
parents: 2511
diff changeset
    18
                        sorted1 le xs)"
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    19
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 3465
diff changeset
    20
primrec
2517
2af078382853 Modified some defs and shortened proofs.
nipkow
parents: 2511
diff changeset
    21
  "sorted le [] = True"
3465
e85c24717cad set_of_list -> set
nipkow
parents: 2517
diff changeset
    22
  "sorted le (x#xs) = ((!y:set xs. le x y) & sorted le xs)"
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    23
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 3465
diff changeset
    24
primrec
8415
paulson
parents: 5184
diff changeset
    25
  "multiset [] y = 0"
paulson
parents: 5184
diff changeset
    26
  "multiset (x#xs) y = (if x=y then Suc(multiset xs y) else multiset xs y)"
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    27
8415
paulson
parents: 5184
diff changeset
    28
constdefs
paulson
parents: 5184
diff changeset
    29
  total  :: (['a,'a] => bool) => bool
paulson
parents: 5184
diff changeset
    30
   "total r == (ALL x y. r x y | r y x)"
paulson
parents: 5184
diff changeset
    31
  
paulson
parents: 5184
diff changeset
    32
  transf :: (['a,'a] => bool) => bool
paulson
parents: 5184
diff changeset
    33
   "transf f == (ALL x y z. f x y & f y z --> f x z)"
paulson
parents: 5184
diff changeset
    34
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    35
end