author | berghofe |
Tue, 25 Jun 1996 13:11:29 +0200 | |
changeset 1824 | 44254696843a |
parent 1820 | e381e1c51689 |
child 2031 | 03a843f0f447 |
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 |
||
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); |
1673
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1465
diff
changeset
|
26 |
val alls_lemma=result(); |
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1465
diff
changeset
|
27 |
Addsimps [alls_lemma]; |
969 | 28 |
|
1673
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1465
diff
changeset
|
29 |
goal HOL.thy "((P --> Q) & (~P --> Q)) = Q"; |
1820 | 30 |
by(Fast_tac 1); |
1266 | 31 |
val lemma = result(); |
969 | 32 |
|
33 |
goal Qsort.thy "(Alls x:qsort le xs.P(x)) = (Alls x:xs.P(x))"; |
|
34 |
by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); |
|
1673
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1465
diff
changeset
|
35 |
by(Asm_simp_tac 1); |
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1465
diff
changeset
|
36 |
by(asm_simp_tac (!simpset delsimps [alls_lemma, list_all_Cons])1); |
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1465
diff
changeset
|
37 |
by(asm_simp_tac (!simpset addsimps [lemma]) 1); |
1266 | 38 |
Addsimps [result()]; |
969 | 39 |
|
40 |
goal Qsort.thy |
|
41 |
"sorted le (xs@ys) = (sorted le xs & sorted le ys & \ |
|
42 |
\ (Alls x:xs. Alls y:ys. le x y))"; |
|
43 |
by(list.induct_tac "xs" 1); |
|
1673
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1465
diff
changeset
|
44 |
by(Asm_simp_tac 1); |
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1465
diff
changeset
|
45 |
by(asm_simp_tac (!simpset delsimps [alls_lemma]) 1); |
1266 | 46 |
Addsimps [result()]; |
969 | 47 |
|
1673
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1465
diff
changeset
|
48 |
|
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1465
diff
changeset
|
49 |
|
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1465
diff
changeset
|
50 |
|
969 | 51 |
goal Qsort.thy |
52 |
"!!le. [| total(le); transf(le) |] ==> sorted le (qsort le xs)"; |
|
53 |
by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); |
|
1673
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1465
diff
changeset
|
54 |
by(Asm_simp_tac 1); |
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1465
diff
changeset
|
55 |
by(asm_full_simp_tac (!simpset addsimps []) 1); |
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1465
diff
changeset
|
56 |
by(asm_full_simp_tac (!simpset addsimps [list_all_mem_conv]) 1); |
969 | 57 |
by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]); |
1820 | 58 |
by(Fast_tac 1); |
969 | 59 |
result(); |
60 |
||
61 |
(* A verification based on predicate calculus rather than combinators *) |
|
62 |
||
63 |
val sorted_Cons = |
|
64 |
rewrite_rule [list_all_mem_conv RS eq_reflection] Sorting.sorted_Cons; |
|
65 |
||
1266 | 66 |
Addsimps [sorted_Cons]; |
969 | 67 |
|
68 |
||
69 |
goal Qsort.thy "x mem qsort le xs = x mem xs"; |
|
70 |
by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); |
|
1266 | 71 |
by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
1820 | 72 |
by(Fast_tac 1); |
1266 | 73 |
Addsimps [result()]; |
969 | 74 |
|
75 |
goal Qsort.thy |
|
76 |
"sorted le (xs@ys) = (sorted le xs & sorted le ys & \ |
|
77 |
\ (!x. x mem xs --> (!y. y mem ys --> le x y)))"; |
|
78 |
by(list.induct_tac "xs" 1); |
|
1673
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1465
diff
changeset
|
79 |
by(Asm_simp_tac 1); |
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1465
diff
changeset
|
80 |
by(asm_simp_tac (!simpset setloop (split_tac [expand_if]) |
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1465
diff
changeset
|
81 |
delsimps [list_all_conj] |
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1465
diff
changeset
|
82 |
addsimps [list_all_mem_conv]) 1); |
1820 | 83 |
by(Fast_tac 1); |
1266 | 84 |
Addsimps [result()]; |
969 | 85 |
|
86 |
goal Qsort.thy |
|
87 |
"!!xs. [| total(le); transf(le) |] ==> sorted le (qsort le xs)"; |
|
88 |
by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); |
|
1266 | 89 |
by(Simp_tac 1); |
1673
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1465
diff
changeset
|
90 |
by(asm_simp_tac (!simpset setloop (split_tac [expand_if]) |
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1465
diff
changeset
|
91 |
delsimps [list_all_conj] |
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1465
diff
changeset
|
92 |
addsimps [list_all_mem_conv]) 1); |
969 | 93 |
by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]); |
1820 | 94 |
by(Fast_tac 1); |
969 | 95 |
result(); |
1673
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1465
diff
changeset
|
96 |
|
d22110ddd0af
repaired critical proofs depending on the order inside non-confluent SimpSets
oheimb
parents:
1465
diff
changeset
|
97 |