author  paulson 
Mon, 13 Mar 2000 12:42:05 +0100  
changeset 8421  7156b8e26a17 
parent 8414  5983668cac15 
child 8590  89675b444abe 
permissions  rwrr 
1465  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 

8414  9 
Addsimps qsort.rules; 
2511  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"; 