author | oheimb |
Fri, 20 Feb 1998 16:00:18 +0100 | |
changeset 4637 | bac998af6ea2 |
parent 4423 | a129b817b58a |
child 4686 | 74a12e86b20b |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/ex/qsort.ML |
969 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Tobias Nipkow |
969 | 4 |
Copyright 1994 TU Muenchen |
5 |
||
6 |
Two verifications of Quicksort |
|
7 |
*) |
|
8 |
||
2526 | 9 |
Addsimps [ball_Un]; |
2511 | 10 |
|
11 |
(* Towards a proof of qsort_ind |
|
12 |
||
13 |
A short proof of Konrad's wf_minimal in WF1.ML: |
|
14 |
||
15 |
val [p1] = goalw WF.thy [wf_def] |
|
16 |
"wf(R) ==> (!Q. (? x. Q x) --> (? min. Q min & (!b. (b,min):R --> (~ Q b))))"; |
|
17 |
by (rtac allI 1); |
|
4423 | 18 |
by (cut_inst_tac[("x","%u.~Q u")](p1 RS spec) 1); |
2511 | 19 |
by (fast_tac HOL_cs 1); |
20 |
val wf_minimal = result(); |
|
21 |
||
22 |
*) |
|
23 |
||
24 |
||
1266 | 25 |
Addsimps ([Qsort.qsort_Nil,Qsort.qsort_Cons]@conj_comms); |
969 | 26 |
|
27 |
goal Qsort.thy "!x. mset (qsort le xs) x = mset xs x"; |
|
2031 | 28 |
by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); |
4089 | 29 |
by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if]))); |
2511 | 30 |
qed "qsort_permutes"; |
969 | 31 |
|
3465 | 32 |
goal Qsort.thy "set(qsort le xs) = set xs"; |
4423 | 33 |
by (simp_tac (simpset() addsimps [set_via_mset,qsort_permutes]) 1); |
3647
a64c8fbcd98f
Renamed theorems of the form set_of_list_XXX to set_XXX
paulson
parents:
3465
diff
changeset
|
34 |
qed "set_qsort"; |
a64c8fbcd98f
Renamed theorems of the form set_of_list_XXX to set_XXX
paulson
parents:
3465
diff
changeset
|
35 |
Addsimps [set_qsort]; |
969 | 36 |
|
2511 | 37 |
goal List.thy |
3842 | 38 |
"(!x:set[x:xs. P(x)].Q(x)) = (!x:set xs. P(x)-->Q(x))"; |
2511 | 39 |
by (list.induct_tac "xs" 1); |
4089 | 40 |
by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if]))); |
3647
a64c8fbcd98f
Renamed theorems of the form set_of_list_XXX to set_XXX
paulson
parents:
3465
diff
changeset
|
41 |
qed"Ball_set_filter"; |
a64c8fbcd98f
Renamed theorems of the form set_of_list_XXX to set_XXX
paulson
parents:
3465
diff
changeset
|
42 |
Addsimps [Ball_set_filter]; |
969 | 43 |
|
44 |
goal Qsort.thy |
|
45 |
"sorted le (xs@ys) = (sorted le xs & sorted le ys & \ |
|
3465 | 46 |
\ (!x:set xs. !y:set ys. le x y))"; |
2031 | 47 |
by (list.induct_tac "xs" 1); |
2511 | 48 |
by (ALLGOALS Asm_simp_tac); |
49 |
qed "sorted_append"; |
|
50 |
Addsimps [sorted_append]; |
|
1673
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1465
diff
changeset
|
51 |
|
969 | 52 |
goal Qsort.thy |
53 |
"!!le. [| total(le); transf(le) |] ==> sorted le (qsort le xs)"; |
|
2031 | 54 |
by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); |
2511 | 55 |
by (ALLGOALS Asm_simp_tac); |
2031 | 56 |
by (rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]); |
57 |
by (Fast_tac 1); |
|
2511 | 58 |
qed "sorted_qsort"; |