src/HOL/ex/Sorting.thy
author paulson
Tue, 16 Jul 1996 15:49:46 +0200
changeset 1868 836950047d85
parent 1476 608483c2122a
child 2511 282e9a9eae9d
permissions -rw-r--r--
Put in minimal simpset to avoid excessive simplification, just as in revision 1.9 of HOL/indrule.ML
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
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     9
Sorting = List +
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
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 969
diff changeset
    13
  mset   :: 'a list => ('a => nat)
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 969
diff changeset
    14
  total  :: (['a,'a] => bool) => bool
92f83b9d17e1 removed quotes from consts and syntax sections
clasohm
parents: 969
diff changeset
    15
  transf :: (['a,'a] => bool) => bool
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    16
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    17
rules
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    18
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    19
sorted1_Nil  "sorted1 f []"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    20
sorted1_One  "sorted1 f [x]"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    21
sorted1_Cons "sorted1 f (Cons x (y#zs)) = (f x y & sorted1 f (y#zs))"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    22
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    23
sorted_Nil "sorted le []"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    24
sorted_Cons "sorted le (x#xs) = ((Alls y:xs. le x y) & sorted le xs)"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    25
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    26
mset_Nil "mset [] y = 0"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    27
mset_Cons "mset (x#xs) y = (if x=y then Suc(mset xs y) else mset xs y)"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    28
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    29
total_def  "total r == (!x y. r x y | r y x)"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    30
transf_def "transf f == (!x y z. f x y & f y z --> f x z)"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    31
end