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 |
|
1266
|
9 |
Addsimps ([Qsort.qsort_Nil,Qsort.qsort_Cons]@conj_comms);
|
969
|
10 |
|
|
11 |
goal Qsort.thy "!x. mset (qsort le xs) x = mset xs x";
|
|
12 |
by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
|
1266
|
13 |
by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
|
969
|
14 |
result();
|
|
15 |
|
|
16 |
|
|
17 |
goal Qsort.thy "(Alls x:[x:xs.P(x)].Q(x)) = (Alls x:xs. P(x)-->Q(x))";
|
|
18 |
by(list.induct_tac "xs" 1);
|
1266
|
19 |
by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
|
|
20 |
Addsimps [result()];
|
969
|
21 |
|
|
22 |
goal Qsort.thy
|
|
23 |
"((Alls x:xs.P(x)) & (Alls x:xs.Q(x))) = (Alls x:xs. P(x)&Q(x))";
|
|
24 |
by(list.induct_tac "xs" 1);
|
1266
|
25 |
by(ALLGOALS Asm_simp_tac);
|
|
26 |
Addsimps [result()];
|
969
|
27 |
|
|
28 |
goal HOL.thy "((~P --> Q) & (P --> Q)) = Q";
|
|
29 |
by(fast_tac HOL_cs 1);
|
1266
|
30 |
val lemma = result();
|
969
|
31 |
|
|
32 |
goal Qsort.thy "(Alls x:qsort le xs.P(x)) = (Alls x:xs.P(x))";
|
|
33 |
by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
|
1266
|
34 |
by(ALLGOALS(asm_simp_tac (!simpset addsimps [lemma])));
|
|
35 |
Addsimps [result()];
|
969
|
36 |
|
|
37 |
goal Qsort.thy
|
|
38 |
"sorted le (xs@ys) = (sorted le xs & sorted le ys & \
|
|
39 |
\ (Alls x:xs. Alls y:ys. le x y))";
|
|
40 |
by(list.induct_tac "xs" 1);
|
1266
|
41 |
by(ALLGOALS Asm_simp_tac);
|
|
42 |
Addsimps [result()];
|
969
|
43 |
|
|
44 |
goal Qsort.thy
|
|
45 |
"!!le. [| total(le); transf(le) |] ==> sorted le (qsort le xs)";
|
|
46 |
by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
|
1266
|
47 |
by(ALLGOALS(asm_full_simp_tac (!simpset addsimps [list_all_mem_conv]) ));
|
969
|
48 |
by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);
|
|
49 |
by(fast_tac HOL_cs 1);
|
|
50 |
result();
|
|
51 |
|
|
52 |
|
|
53 |
(* A verification based on predicate calculus rather than combinators *)
|
|
54 |
|
|
55 |
val sorted_Cons =
|
|
56 |
rewrite_rule [list_all_mem_conv RS eq_reflection] Sorting.sorted_Cons;
|
|
57 |
|
1266
|
58 |
Addsimps [sorted_Cons];
|
969
|
59 |
|
|
60 |
|
|
61 |
goal Qsort.thy "x mem qsort le xs = x mem xs";
|
|
62 |
by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
|
1266
|
63 |
by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
|
969
|
64 |
by(fast_tac HOL_cs 1);
|
1266
|
65 |
Addsimps [result()];
|
969
|
66 |
|
|
67 |
goal Qsort.thy
|
|
68 |
"sorted le (xs@ys) = (sorted le xs & sorted le ys & \
|
|
69 |
\ (!x. x mem xs --> (!y. y mem ys --> le x y)))";
|
|
70 |
by(list.induct_tac "xs" 1);
|
1266
|
71 |
by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
|
969
|
72 |
by(fast_tac HOL_cs 1);
|
1266
|
73 |
Addsimps [result()];
|
969
|
74 |
|
|
75 |
goal Qsort.thy
|
|
76 |
"!!xs. [| total(le); transf(le) |] ==> sorted le (qsort le xs)";
|
|
77 |
by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
|
1266
|
78 |
by(Simp_tac 1);
|
|
79 |
by(asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
|
969
|
80 |
by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);
|
|
81 |
by(fast_tac HOL_cs 1);
|
|
82 |
result();
|