21 |
21 |
22 goal Qsort.thy |
22 goal Qsort.thy |
23 "((Alls x:xs.P(x)) & (Alls x:xs.Q(x))) = (Alls x:xs. P(x)&Q(x))"; |
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); |
24 by(list.induct_tac "xs" 1); |
25 by(ALLGOALS Asm_simp_tac); |
25 by(ALLGOALS Asm_simp_tac); |
26 Addsimps [result()]; |
26 val alls_lemma=result(); |
|
27 Addsimps [alls_lemma]; |
27 |
28 |
28 goal HOL.thy "((~P --> Q) & (P --> Q)) = Q"; |
29 goal HOL.thy "((P --> Q) & (~P --> Q)) = Q"; |
29 by(fast_tac HOL_cs 1); |
30 by(fast_tac HOL_cs 1); |
30 val lemma = result(); |
31 val lemma = result(); |
31 |
32 |
32 goal Qsort.thy "(Alls x:qsort le xs.P(x)) = (Alls x:xs.P(x))"; |
33 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(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); |
34 by(ALLGOALS(asm_simp_tac (!simpset addsimps [lemma]))); |
35 by(Asm_simp_tac 1); |
|
36 by(asm_simp_tac (!simpset delsimps [alls_lemma, list_all_Cons])1); |
|
37 by(asm_simp_tac (!simpset addsimps [lemma]) 1); |
35 Addsimps [result()]; |
38 Addsimps [result()]; |
36 |
39 |
37 goal Qsort.thy |
40 goal Qsort.thy |
38 "sorted le (xs@ys) = (sorted le xs & sorted le ys & \ |
41 "sorted le (xs@ys) = (sorted le xs & sorted le ys & \ |
39 \ (Alls x:xs. Alls y:ys. le x y))"; |
42 \ (Alls x:xs. Alls y:ys. le x y))"; |
40 by(list.induct_tac "xs" 1); |
43 by(list.induct_tac "xs" 1); |
41 by(ALLGOALS Asm_simp_tac); |
44 by(Asm_simp_tac 1); |
|
45 by(asm_simp_tac (!simpset delsimps [alls_lemma]) 1); |
42 Addsimps [result()]; |
46 Addsimps [result()]; |
|
47 |
|
48 |
|
49 |
43 |
50 |
44 goal Qsort.thy |
51 goal Qsort.thy |
45 "!!le. [| total(le); transf(le) |] ==> sorted le (qsort le xs)"; |
52 "!!le. [| total(le); transf(le) |] ==> sorted le (qsort le xs)"; |
46 by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); |
53 by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); |
47 by(ALLGOALS(asm_full_simp_tac (!simpset addsimps [list_all_mem_conv]) )); |
54 by(Asm_simp_tac 1); |
|
55 by(asm_full_simp_tac (!simpset addsimps []) 1); |
|
56 by(asm_full_simp_tac (!simpset addsimps [list_all_mem_conv]) 1); |
48 by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]); |
57 by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]); |
49 by(fast_tac HOL_cs 1); |
58 by(fast_tac HOL_cs 1); |
50 result(); |
59 result(); |
51 |
|
52 |
60 |
53 (* A verification based on predicate calculus rather than combinators *) |
61 (* A verification based on predicate calculus rather than combinators *) |
54 |
62 |
55 val sorted_Cons = |
63 val sorted_Cons = |
56 rewrite_rule [list_all_mem_conv RS eq_reflection] Sorting.sorted_Cons; |
64 rewrite_rule [list_all_mem_conv RS eq_reflection] Sorting.sorted_Cons; |
66 |
74 |
67 goal Qsort.thy |
75 goal Qsort.thy |
68 "sorted le (xs@ys) = (sorted le xs & sorted le ys & \ |
76 "sorted le (xs@ys) = (sorted le xs & sorted le ys & \ |
69 \ (!x. x mem xs --> (!y. y mem ys --> le x y)))"; |
77 \ (!x. x mem xs --> (!y. y mem ys --> le x y)))"; |
70 by(list.induct_tac "xs" 1); |
78 by(list.induct_tac "xs" 1); |
71 by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
79 by(Asm_simp_tac 1); |
|
80 by(asm_simp_tac (!simpset setloop (split_tac [expand_if]) |
|
81 delsimps [list_all_conj] |
|
82 addsimps [list_all_mem_conv]) 1); |
72 by(fast_tac HOL_cs 1); |
83 by(fast_tac HOL_cs 1); |
73 Addsimps [result()]; |
84 Addsimps [result()]; |
74 |
85 |
75 goal Qsort.thy |
86 goal Qsort.thy |
76 "!!xs. [| total(le); transf(le) |] ==> sorted le (qsort le xs)"; |
87 "!!xs. [| total(le); transf(le) |] ==> sorted le (qsort le xs)"; |
77 by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); |
88 by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); |
78 by(Simp_tac 1); |
89 by(Simp_tac 1); |
79 by(asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
90 by(asm_simp_tac (!simpset setloop (split_tac [expand_if]) |
|
91 delsimps [list_all_conj] |
|
92 addsimps [list_all_mem_conv]) 1); |
80 by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]); |
93 by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]); |
81 by(fast_tac HOL_cs 1); |
94 by(fast_tac HOL_cs 1); |
82 result(); |
95 result(); |
|
96 |
|
97 |