src/HOL/ex/Qsort.thy
changeset 8414 5983668cac15
parent 1476 608483c2122a
child 8524 f990040535c9
equal deleted inserted replaced
8413:09db77a084aa 8414:5983668cac15
     1 (*  Title:      HOL/ex/qsort.thy
     1 (*  Title:      HOL/ex/Qsort.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     3     Author:     Tobias Nipkow
     4     Copyright   1994 TU Muenchen
     4     Copyright   1994 TU Muenchen
     5 
     5 
     6 Quicksort
     6 Quicksort
     7 *)
     7 *)
     8 
     8 
     9 Qsort = Sorting +
     9 Qsort = Sorting +
    10 consts
    10 consts qsort :: "((['a,'a] => bool) * 'a list) => 'a list"
    11   qsort  :: [['a,'a] => bool, 'a list] => 'a list
       
    12 
    11 
    13 rules
    12 recdef qsort "measure (size o snd)"
       
    13     simpset "simpset() addsimps [less_Suc_eq_le]"
       
    14     
       
    15     "qsort(le, [])   = []"
       
    16     
       
    17     "qsort(le, x#xs) = qsort(le, [y:xs . ~ le x y])  
       
    18                        @ (x # qsort(le, [y:xs . le x y]))"
    14 
    19 
    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
    20 end