author | paulson |
Wed, 05 Nov 1997 13:23:46 +0100 | |
changeset 4153 | e534c4c32d54 |
parent 4089 | 96fba19bcbe2 |
child 4686 | 74a12e86b20b |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/ex/insort.ML |
969 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Tobias Nipkow |
969 | 4 |
Copyright 1994 TU Muenchen |
5 |
||
6 |
Correctness proof of insertion sort. |
|
7 |
*) |
|
8 |
||
2517 | 9 |
goal thy "!y. mset(ins f x xs) y = mset (x#xs) y"; |
2031 | 10 |
by (list.induct_tac "xs" 1); |
11 |
by (Asm_simp_tac 1); |
|
4089 | 12 |
by (asm_simp_tac (simpset() addsplits [expand_if]) 1); |
2517 | 13 |
qed "mset_ins"; |
14 |
Addsimps [mset_ins]; |
|
15 |
||
16 |
goal thy "!x. mset(insort f xs) x = mset xs x"; |
|
17 |
by (list.induct_tac "xs" 1); |
|
18 |
by (ALLGOALS Asm_simp_tac); |
|
19 |
qed "insort_permutes"; |
|
20 |
||
3465 | 21 |
goal thy "set(ins f x xs) = insert x (set xs)"; |
4089 | 22 |
by (asm_simp_tac (simpset() addsimps [set_via_mset] |
3919 | 23 |
addsplits [expand_if]) 1); |
2031 | 24 |
by (Fast_tac 1); |
3647
a64c8fbcd98f
Renamed theorems of the form set_of_list_XXX to set_XXX
paulson
parents:
3465
diff
changeset
|
25 |
qed "set_ins"; |
a64c8fbcd98f
Renamed theorems of the form set_of_list_XXX to set_XXX
paulson
parents:
3465
diff
changeset
|
26 |
Addsimps [set_ins]; |
969 | 27 |
|
2517 | 28 |
val prems = goalw InSort.thy [total_def,transf_def] |
969 | 29 |
"[| total(f); transf(f) |] ==> sorted f (ins f x xs) = sorted f xs"; |
2031 | 30 |
by (list.induct_tac "xs" 1); |
4089 | 31 |
by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if]))); |
2031 | 32 |
by (cut_facts_tac prems 1); |
2517 | 33 |
by (Fast_tac 1); |
2511 | 34 |
qed "sorted_ins"; |
35 |
Addsimps [sorted_ins]; |
|
969 | 36 |
|
37 |
goal InSort.thy "!!f. [| total(f); transf(f) |] ==> sorted f (insort f xs)"; |
|
2031 | 38 |
by (list.induct_tac "xs" 1); |
39 |
by (ALLGOALS Asm_simp_tac); |
|
1750
817a34a54fb0
replaced result() by qed "sorted_insort" in last proof
berghofe
parents:
1465
diff
changeset
|
40 |
qed "sorted_insort"; |