969
|
1 |
(* Title: HOL/ex/insort.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 1994 TU Muenchen
|
|
5 |
|
|
6 |
Correctness proof of insertion sort.
|
|
7 |
*)
|
|
8 |
|
|
9 |
goalw InSort.thy [Sorting.total_def]
|
|
10 |
"!!f. [| total(f); ~f x y |] ==> f y x";
|
|
11 |
by(fast_tac HOL_cs 1);
|
|
12 |
qed "totalD";
|
|
13 |
|
|
14 |
goalw InSort.thy [Sorting.transf_def]
|
|
15 |
"!!f. [| transf(f); f b a |] ==> !x. f a x --> f b x";
|
|
16 |
by(fast_tac HOL_cs 1);
|
|
17 |
qed "transfD";
|
|
18 |
|
|
19 |
goal InSort.thy "list_all p (ins f x xs) = (list_all p xs & p(x))";
|
|
20 |
by(list.induct_tac "xs" 1);
|
1266
|
21 |
by(Asm_simp_tac 1);
|
|
22 |
by(asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
|
969
|
23 |
by(fast_tac HOL_cs 1);
|
1266
|
24 |
Addsimps [result()];
|
969
|
25 |
|
|
26 |
goal InSort.thy "(!x. p(x) --> q(x)) --> list_all p xs --> list_all q xs";
|
|
27 |
by(list.induct_tac "xs" 1);
|
1266
|
28 |
by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
|
969
|
29 |
qed "list_all_imp";
|
|
30 |
|
|
31 |
val prems = goal InSort.thy
|
|
32 |
"[| total(f); transf(f) |] ==> sorted f (ins f x xs) = sorted f xs";
|
|
33 |
by(list.induct_tac "xs" 1);
|
1266
|
34 |
by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
|
969
|
35 |
by(cut_facts_tac prems 1);
|
|
36 |
by(cut_inst_tac [("p","f(a)"),("q","f(x)")] list_all_imp 1);
|
|
37 |
by(fast_tac (HOL_cs addDs [totalD,transfD]) 1);
|
1266
|
38 |
Addsimps [result()];
|
969
|
39 |
|
|
40 |
goal InSort.thy "!!f. [| total(f); transf(f) |] ==> sorted f (insort f xs)";
|
|
41 |
by(list.induct_tac "xs" 1);
|
1266
|
42 |
by(ALLGOALS Asm_simp_tac);
|
969
|
43 |
result();
|