1 (* Title: HOL/ex/qsort.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1994 TU Muenchen |
|
5 |
|
6 Two verifications of Quicksort |
|
7 *) |
|
8 |
|
9 val ss = sorting_ss addsimps ([Qsort.qsort_Nil,Qsort.qsort_Cons]@conj_comms); |
|
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); |
|
13 by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if])))); |
|
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); |
|
19 by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if])))); |
|
20 val ss = ss addsimps [result()]; |
|
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); |
|
25 by(ALLGOALS(asm_simp_tac ss)); |
|
26 val ss = ss addsimps [result()]; |
|
27 |
|
28 goal HOL.thy "((~P --> Q) & (P --> Q)) = Q"; |
|
29 by(fast_tac HOL_cs 1); |
|
30 qed "lemma"; |
|
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); |
|
34 by(ALLGOALS(asm_simp_tac (ss addsimps [lemma]))); |
|
35 val ss = ss addsimps [result()]; |
|
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); |
|
41 by(ALLGOALS(asm_simp_tac ss)); |
|
42 val ss = ss addsimps [result()]; |
|
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); |
|
47 by(ALLGOALS(asm_full_simp_tac (ss addsimps [list_all_mem_conv]) )); |
|
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 |
|
58 val ss = list_ss addsimps |
|
59 [Sorting.sorted_Nil,sorted_Cons, |
|
60 Qsort.qsort_Nil,Qsort.qsort_Cons]; |
|
61 |
|
62 |
|
63 goal Qsort.thy "x mem qsort(le,xs) = x mem xs"; |
|
64 by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); |
|
65 by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if])))); |
|
66 by(fast_tac HOL_cs 1); |
|
67 val ss = ss addsimps [result()]; |
|
68 |
|
69 goal Qsort.thy |
|
70 "sorted(le,xs@ys) = (sorted(le,xs) & sorted(le,ys) & \ |
|
71 \ (!x. x mem xs --> (!y. y mem ys --> le(x,y))))"; |
|
72 by(list.induct_tac "xs" 1); |
|
73 by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if])))); |
|
74 by(fast_tac HOL_cs 1); |
|
75 val ss = ss addsimps [result()]; |
|
76 |
|
77 goal Qsort.thy |
|
78 "!!xs. [| total(le); transf(le) |] ==> sorted(le,qsort(le,xs))"; |
|
79 by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); |
|
80 by(simp_tac ss 1); |
|
81 by(asm_full_simp_tac (ss setloop (split_tac [expand_if])) 1); |
|
82 by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]); |
|
83 by(fast_tac HOL_cs 1); |
|
84 result(); |
|