ex/qsort.thy
author nipkow
Mon, 24 Jan 1994 16:00:37 +0100
changeset 36 b503da67d2f7
child 37 65a546c2b8ed
permissions -rw-r--r--
Verification of quicksort
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
     1
Qsort = List +
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
     2
consts
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
     3
  sorted :: "[['a,'a] => bool, 'a list] => bool"
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
     4
  mset   :: "'a list => ('a => nat)"
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
     5
  qsort  :: "[['a,'a] => bool, 'a list] => 'a list"
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
     6
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
     7
rules
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
     8
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
     9
sorted_Nil "sorted(le,[])"
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    10
sorted_Cons "sorted(le,Cons(x,xs)) = ((Alls y:xs. le(x,y)) & sorted(le,xs))"
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    11
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    12
mset_Nil "mset([],y) = 0"
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    13
mset_Cons "mset(Cons(x,xs),y) = if(x=y, Suc(mset(xs,y)), mset(xs,y))"
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    14
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    15
qsort_Nil  "qsort(le,[]) = []"
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    16
qsort_Cons "qsort(le,Cons(x,xs)) = qsort(le,[y:xs . ~le(x,y)]) @ \
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    17
\                                  Cons(x, qsort(le,[y:xs . le(x,y)]))"
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    18
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    19
(* computational induction.
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    20
   The dependence of p on x but not xs is intentional.
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    21
*)
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    22
qsort_ind
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    23
 "[| P([]); \
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    24
\    !!x xs. [| P([y:xs . ~p(x,y)]); P([y:xs . p(x,y)]) |] ==> \
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    25
\            P(Cons(x,xs)) |] \
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    26
\ ==> P(xs)"
b503da67d2f7 Verification of quicksort
nipkow
parents:
diff changeset
    27
end