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