src/HOL/ex/Qsort.thy
author clasohm
Wed, 21 Jun 1995 15:47:10 +0200
changeset 1151 c820b3cc3df0
parent 969 b051e2fc2e34
child 1376 92f83b9d17e1
permissions -rw-r--r--
removed \...\ inside strings
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     1
(*  Title: 	HOL/ex/qsort.thy
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
     3
    Author: 	Tobias Nipkow
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
Quicksort
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
Qsort = Sorting +
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    10
consts
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    11
  qsort  :: "[['a,'a] => bool, 'a list] => 'a list"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    12
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    13
rules
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    14
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    15
qsort_Nil  "qsort le [] = []"
1151
c820b3cc3df0 removed \...\ inside strings
clasohm
parents: 969
diff changeset
    16
qsort_Cons "qsort le (x#xs) = qsort le [y:xs . ~le x y] @ 
c820b3cc3df0 removed \...\ inside strings
clasohm
parents: 969
diff changeset
    17
                            (x# qsort le [y:xs . le x y])"
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    18
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    19
(* computational induction.
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    20
   The dependence of p on x but not xs is intentional.
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    21
*)
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    22
qsort_ind
1151
c820b3cc3df0 removed \...\ inside strings
clasohm
parents: 969
diff changeset
    23
 "[| P([]); 
c820b3cc3df0 removed \...\ inside strings
clasohm
parents: 969
diff changeset
    24
    !!x xs. [| P([y:xs . ~p x y]); P([y:xs . p x y]) |] ==> 
c820b3cc3df0 removed \...\ inside strings
clasohm
parents: 969
diff changeset
    25
            P(x#xs) |] 
c820b3cc3df0 removed \...\ inside strings
clasohm
parents: 969
diff changeset
    26
 ==> P(xs)"
969
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    27
end