author | nipkow |
Thu, 13 Apr 2000 10:30:28 +0200 | |
changeset 8698 | 8812dad6ef12 |
parent 8624 | 69619f870939 |
child 9736 | 332fab43628f |
permissions | -rw-r--r-- |
8590 | 1 |
(* Title: HOL/ex/Qsort.ML |
969 | 2 |
ID: $Id$ |
8414 | 3 |
Author: Tobias Nipkow (tidied by lcp) |
969 | 4 |
Copyright 1994 TU Muenchen |
5 |
||
8414 | 6 |
The verification of Quicksort |
969 | 7 |
*) |
8 |
||
8590 | 9 |
(*** Version one: higher-order ***) |
10 |
||
8414 | 11 |
Goal "multiset (qsort(le,xs)) x = multiset xs x"; |
12 |
by (res_inst_tac [("v","xs"),("u","le")] qsort.induct 1); |
|
13 |
by Auto_tac; |
|
14 |
qed "qsort_permutes"; |
|
15 |
Addsimps [qsort_permutes]; |
|
969 | 16 |
|
8414 | 17 |
(*Also provable by induction*) |
18 |
Goal "set (qsort(le,xs)) = set xs"; |
|
19 |
by (simp_tac (simpset() addsimps [set_via_multiset]) 1); |
|
3647
a64c8fbcd98f
Renamed theorems of the form set_of_list_XXX to set_XXX
paulson
parents:
3465
diff
changeset
|
20 |
qed "set_qsort"; |
a64c8fbcd98f
Renamed theorems of the form set_of_list_XXX to set_XXX
paulson
parents:
3465
diff
changeset
|
21 |
Addsimps [set_qsort]; |
969 | 22 |
|
8421 | 23 |
Goal "total(le) --> transf(le) --> sorted le (qsort(le,xs))"; |
8414 | 24 |
by (res_inst_tac [("v","xs"),("u","le")] qsort.induct 1); |
2511 | 25 |
by (ALLGOALS Asm_simp_tac); |
8414 | 26 |
by (rewrite_goals_tac [Sorting.total_def, Sorting.transf_def]); |
27 |
by (Blast_tac 1); |
|
28 |
qed_spec_mp "sorted_qsort"; |
|
8590 | 29 |
|
30 |
||
31 |
(*** Version two: type classes ***) |
|
32 |
||
33 |
Goal "multiset (quickSort xs) z = multiset xs z"; |
|
34 |
by (res_inst_tac [("u","xs")] quickSort.induct 1); |
|
35 |
by Auto_tac; |
|
36 |
qed "quickSort_permutes"; |
|
37 |
Addsimps [quickSort_permutes]; |
|
38 |
||
39 |
(*Also provable by induction*) |
|
40 |
Goal "set (quickSort xs) = set xs"; |
|
41 |
by (simp_tac (simpset() addsimps [set_via_multiset]) 1); |
|
42 |
qed "set_quickSort"; |
|
43 |
Addsimps [set_quickSort]; |
|
44 |
||
45 |
Goal "sorted (op <=) (quickSort xs)"; |
|
46 |
by (res_inst_tac [("u","xs")] quickSort.induct 1); |
|
47 |
by (ALLGOALS Asm_simp_tac); |
|
48 |
by (blast_tac (claset() addIs [linorder_linear RS disjE, order_trans]) 1); |
|
49 |
qed_spec_mp "sorted_quickSort"; |