src/HOL/ex/Qsort.thy
author paulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153 e534c4c32d54
parent 1476 608483c2122a
child 8414 5983668cac15
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
     1 (*  Title:      HOL/ex/qsort.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1994 TU Muenchen
     5 
     6 Quicksort
     7 *)
     8 
     9 Qsort = Sorting +
    10 consts
    11   qsort  :: [['a,'a] => bool, 'a list] => 'a list
    12 
    13 rules
    14 
    15 qsort_Nil  "qsort le [] = []"
    16 qsort_Cons "qsort le (x#xs) = qsort le [y:xs . ~le x y] @ 
    17                             (x# qsort le [y:xs . le x y])"
    18 
    19 (* computational induction.
    20    The dependence of p on x but not xs is intentional.
    21 *)
    22 qsort_ind
    23  "[| P([]); 
    24     !!x xs. [| P([y:xs . ~p x y]); P([y:xs . p x y]) |] ==> 
    25             P(x#xs) |] 
    26  ==> P(xs)"
    27 end