src/HOL/ex/Qsort.thy
author clasohm
Wed, 22 Mar 1995 12:42:34 +0100
changeset 969 b051e2fc2e34
child 1151 c820b3cc3df0
permissions -rw-r--r--
converted ex with curried function application
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 [] = []"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    16
qsort_Cons "qsort le (x#xs) = qsort le [y:xs . ~le x y] @ \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    17
\                            (x# qsort le [y:xs . le x y])"
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
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    23
 "[| P([]); \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    24
\    !!x xs. [| P([y:xs . ~p x y]); P([y:xs . p x y]) |] ==> \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    25
\            P(x#xs) |] \
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    26
\ ==> P(xs)"
b051e2fc2e34 converted ex with curried function application
clasohm
parents:
diff changeset
    27
end