author | paulson |
Mon, 27 Mar 2000 17:04:03 +0200 | |
changeset 8590 | 89675b444abe |
parent 8421 | 7156b8e26a17 |
child 8624 | 69619f870939 |
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 |
Addsimps qsort.rules; |
2511 | 12 |
|
8414 | 13 |
Goal "multiset (qsort(le,xs)) x = multiset xs x"; |
14 |
by (res_inst_tac [("v","xs"),("u","le")] qsort.induct 1); |
|
15 |
by Auto_tac; |
|
16 |
qed "qsort_permutes"; |
|
17 |
Addsimps [qsort_permutes]; |
|
969 | 18 |
|
8414 | 19 |
(*Also provable by induction*) |
20 |
Goal "set (qsort(le,xs)) = set xs"; |
|
21 |
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
|
22 |
qed "set_qsort"; |
a64c8fbcd98f
Renamed theorems of the form set_of_list_XXX to set_XXX
paulson
parents:
3465
diff
changeset
|
23 |
Addsimps [set_qsort]; |
969 | 24 |
|
8421 | 25 |
Goal "total(le) --> transf(le) --> sorted le (qsort(le,xs))"; |
8414 | 26 |
by (res_inst_tac [("v","xs"),("u","le")] qsort.induct 1); |
2511 | 27 |
by (ALLGOALS Asm_simp_tac); |
8414 | 28 |
by (rewrite_goals_tac [Sorting.total_def, Sorting.transf_def]); |
29 |
by (Blast_tac 1); |
|
30 |
qed_spec_mp "sorted_qsort"; |
|
8590 | 31 |
|
32 |
||
33 |
(*** Version two: type classes ***) |
|
34 |
||
35 |
Addsimps quickSort.rules; |
|
36 |
||
37 |
Goal "multiset (quickSort xs) z = multiset xs z"; |
|
38 |
by (res_inst_tac [("u","xs")] quickSort.induct 1); |
|
39 |
by Auto_tac; |
|
40 |
qed "quickSort_permutes"; |
|
41 |
Addsimps [quickSort_permutes]; |
|
42 |
||
43 |
(*Also provable by induction*) |
|
44 |
Goal "set (quickSort xs) = set xs"; |
|
45 |
by (simp_tac (simpset() addsimps [set_via_multiset]) 1); |
|
46 |
qed "set_quickSort"; |
|
47 |
Addsimps [set_quickSort]; |
|
48 |
||
49 |
Goal "sorted (op <=) (quickSort xs)"; |
|
50 |
by (res_inst_tac [("u","xs")] quickSort.induct 1); |
|
51 |
by (ALLGOALS Asm_simp_tac); |
|
52 |
by (blast_tac (claset() addIs [linorder_linear RS disjE, order_trans]) 1); |
|
53 |
qed_spec_mp "sorted_quickSort"; |