6 Correctness proof of insertion sort. |
6 Correctness proof of insertion sort. |
7 *) |
7 *) |
8 |
8 |
9 goalw InSort.thy [Sorting.total_def] |
9 goalw InSort.thy [Sorting.total_def] |
10 "!!f. [| total(f); ~f x y |] ==> f y x"; |
10 "!!f. [| total(f); ~f x y |] ==> f y x"; |
11 by(Fast_tac 1); |
11 by (Fast_tac 1); |
12 qed "totalD"; |
12 qed "totalD"; |
13 |
13 |
14 goalw InSort.thy [Sorting.transf_def] |
14 goalw InSort.thy [Sorting.transf_def] |
15 "!!f. [| transf(f); f b a |] ==> !x. f a x --> f b x"; |
15 "!!f. [| transf(f); f b a |] ==> !x. f a x --> f b x"; |
16 by(Fast_tac 1); |
16 by (Fast_tac 1); |
17 qed "transfD"; |
17 qed "transfD"; |
18 |
18 |
19 goal InSort.thy "list_all p (ins f x xs) = (list_all p xs & p(x))"; |
19 goal InSort.thy "list_all p (ins f x xs) = (list_all p xs & p(x))"; |
20 by(list.induct_tac "xs" 1); |
20 by (list.induct_tac "xs" 1); |
21 by(Asm_simp_tac 1); |
21 by (Asm_simp_tac 1); |
22 by(asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
22 by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1); |
23 by(Fast_tac 1); |
23 by (Fast_tac 1); |
24 Addsimps [result()]; |
24 Addsimps [result()]; |
25 |
25 |
26 goal InSort.thy "(!x. p(x) --> q(x)) --> list_all p xs --> list_all q xs"; |
26 goal InSort.thy "(!x. p(x) --> q(x)) --> list_all p xs --> list_all q xs"; |
27 by(list.induct_tac "xs" 1); |
27 by (list.induct_tac "xs" 1); |
28 by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
28 by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
29 qed "list_all_imp"; |
29 qed "list_all_imp"; |
30 |
30 |
31 val prems = goal InSort.thy |
31 val prems = goal InSort.thy |
32 "[| total(f); transf(f) |] ==> sorted f (ins f x xs) = sorted f xs"; |
32 "[| total(f); transf(f) |] ==> sorted f (ins f x xs) = sorted f xs"; |
33 by(list.induct_tac "xs" 1); |
33 by (list.induct_tac "xs" 1); |
34 by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
34 by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
35 by(cut_facts_tac prems 1); |
35 by (cut_facts_tac prems 1); |
36 by(cut_inst_tac [("p","f(a)"),("q","f(x)")] list_all_imp 1); |
36 by (cut_inst_tac [("p","f(a)"),("q","f(x)")] list_all_imp 1); |
37 by(fast_tac (!claset addDs [totalD,transfD]) 1); |
37 by (fast_tac (!claset addDs [totalD,transfD]) 1); |
38 Addsimps [result()]; |
38 Addsimps [result()]; |
39 |
39 |
40 goal InSort.thy "!!f. [| total(f); transf(f) |] ==> sorted f (insort f xs)"; |
40 goal InSort.thy "!!f. [| total(f); transf(f) |] ==> sorted f (insort f xs)"; |
41 by(list.induct_tac "xs" 1); |
41 by (list.induct_tac "xs" 1); |
42 by(ALLGOALS Asm_simp_tac); |
42 by (ALLGOALS Asm_simp_tac); |
43 qed "sorted_insort"; |
43 qed "sorted_insort"; |
44 |
44 |