|
1 val ss = list_ss addsimps |
|
2 [Qsort.mset_Nil,Qsort.mset_Cons, |
|
3 Qsort.sorted_Nil,Qsort.sorted_Cons, |
|
4 Qsort.qsort_Nil,Qsort.qsort_Cons]; |
|
5 |
|
6 |
|
7 goal Qsort.thy "!x.mset(xs@ys,x) = mset(xs,x)+mset(ys,x)"; |
|
8 by(list_ind_tac "xs" 1); |
|
9 by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if])))); |
|
10 val ss = ss addsimps [result()]; |
|
11 |
|
12 goal Qsort.thy "!x. mset([x:xs. ~p(x)], x) + mset([x:xs.p(x)], x) = \ |
|
13 \ mset(xs, x)"; |
|
14 by(list_ind_tac "xs" 1); |
|
15 by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if])))); |
|
16 val ss = ss addsimps [result()]; |
|
17 |
|
18 goal Qsort.thy "!x. mset(qsort(le,xs),x) = mset(xs,x)"; |
|
19 by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); |
|
20 by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if])))); |
|
21 result(); |
|
22 |
|
23 |
|
24 goal Qsort.thy "(Alls x:[x:xs.P(x)].Q(x)) = (Alls x:xs. P(x)-->Q(x))"; |
|
25 by(list_ind_tac "xs" 1); |
|
26 by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if])))); |
|
27 val ss = ss addsimps [result()]; |
|
28 |
|
29 goal Qsort.thy |
|
30 "((Alls x:xs.P(x)) & (Alls x:xs.Q(x))) = (Alls x:xs. P(x)&Q(x))"; |
|
31 by(list_ind_tac "xs" 1); |
|
32 by(ALLGOALS(asm_simp_tac ss)); |
|
33 by(fast_tac HOL_cs 1); |
|
34 val ss = ss addsimps [result()]; |
|
35 |
|
36 goal Qsort.thy "(list_all(p,xs) & Q & list_all(q,ys)) = \ |
|
37 \ (Q & list_all(p,xs) & list_all(q,ys))"; |
|
38 by(fast_tac HOL_cs 1); |
|
39 val lemma1 = result(); |
|
40 |
|
41 goal HOL.thy "((~P --> Q) & (P --> Q)) = Q"; |
|
42 by(fast_tac HOL_cs 1); |
|
43 val lemma2 = result(); |
|
44 |
|
45 goal Qsort.thy "(Alls x:qsort(le,xs).P(x)) = (Alls x:xs.P(x))"; |
|
46 by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); |
|
47 by(ALLGOALS(asm_simp_tac (ss addsimps [lemma1,lemma2]))); |
|
48 val ss = ss addsimps [result()]; |
|
49 |
|
50 goal Qsort.thy |
|
51 "sorted(le,xs@ys) = (sorted(le,xs) & sorted(le,ys) & \ |
|
52 \ (Alls x:xs. Alls y:ys. le(x,y)))"; |
|
53 by(list_ind_tac "xs" 1); |
|
54 by(ALLGOALS(asm_simp_tac ss)); |
|
55 by(fast_tac HOL_cs 1); |
|
56 val ss = ss addsimps [result()]; |
|
57 |
|
58 val prems = goal Qsort.thy |
|
59 "[| !x y. (~le(x,y)) = le(y,x); \ |
|
60 \ !x y z. le(x,y) & le(y,z) --> le(x,z) |] ==> \ |
|
61 \ sorted(le,qsort(le,xs))"; |
|
62 by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); |
|
63 by(ALLGOALS(asm_full_simp_tac (ss addsimps [hd prems,list_all_mem_conv]) )); |
|
64 by(cut_facts_tac (tl prems) 1); |
|
65 by(fast_tac HOL_cs 1); |
|
66 result(); |
|
67 |
|
68 |
|
69 (* A verification based on predicate calculus rather than combinators *) |
|
70 |
|
71 val sorted_Cons = |
|
72 rewrite_rule [list_all_mem_conv RS eq_reflection] Qsort.sorted_Cons; |
|
73 |
|
74 val ss = list_ss addsimps |
|
75 [Qsort.sorted_Nil,sorted_Cons, |
|
76 Qsort.qsort_Nil,Qsort.qsort_Cons]; |
|
77 |
|
78 |
|
79 goal List.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))"; |
|
80 by(list_ind_tac "xs" 1); |
|
81 by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if])))); |
|
82 val ss = ss addsimps [result()]; |
|
83 |
|
84 goal Qsort.thy "x mem qsort(le,xs) = x mem xs"; |
|
85 by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); |
|
86 by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if])))); |
|
87 by(fast_tac HOL_cs 1); |
|
88 val ss = ss addsimps [result()]; |
|
89 |
|
90 goal Qsort.thy |
|
91 "sorted(le,xs@ys) = (sorted(le,xs) & sorted(le,ys) & \ |
|
92 \ (!x. x mem xs --> (!y. y mem ys --> le(x,y))))"; |
|
93 by(list_ind_tac "xs" 1); |
|
94 by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if])))); |
|
95 by(fast_tac HOL_cs 1); |
|
96 val ss = ss addsimps [result()]; |
|
97 |
|
98 val prems = goal Qsort.thy |
|
99 "[| !x y. (~le(x,y)) = le(y,x); \ |
|
100 \ !x y z. le(x,y) & le(y,z) --> le(x,z) |] ==> \ |
|
101 \ sorted(le,qsort(le,xs))"; |
|
102 by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); |
|
103 by(simp_tac ss 1); |
|
104 by(asm_full_simp_tac (ss addsimps [hd prems] |
|
105 setloop (split_tac [expand_if])) 1); |
|
106 by(cut_facts_tac (tl prems) 1); |
|
107 by(fast_tac HOL_cs 1); |
|
108 result(); |