author | paulson |
Mon, 20 Mar 2000 18:24:11 +0100 | |
changeset 8528 | 6c48043ccd0e |
parent 8422 | 6c6a5410a9bd |
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 |
||
8422 | 9 |
Goal "!y. multiset(ins le x xs) y = multiset (x#xs) y"; |
5184 | 10 |
by (induct_tac "xs" 1); |
8422 | 11 |
by Auto_tac; |
12 |
qed_spec_mp "multiset_ins"; |
|
13 |
Addsimps [multiset_ins]; |
|
2517 | 14 |
|
8422 | 15 |
Goal "!x. multiset(insort le xs) x = multiset xs x"; |
5184 | 16 |
by (induct_tac "xs" 1); |
8422 | 17 |
by Auto_tac; |
18 |
qed_spec_mp "insort_permutes"; |
|
2517 | 19 |
|
8422 | 20 |
Goal "set(ins le x xs) = insert x (set xs)"; |
21 |
by (asm_simp_tac (simpset() addsimps [set_via_multiset]) 1); |
|
2031 | 22 |
by (Fast_tac 1); |
3647
a64c8fbcd98f
Renamed theorems of the form set_of_list_XXX to set_XXX
paulson
parents:
3465
diff
changeset
|
23 |
qed "set_ins"; |
a64c8fbcd98f
Renamed theorems of the form set_of_list_XXX to set_XXX
paulson
parents:
3465
diff
changeset
|
24 |
Addsimps [set_ins]; |
969 | 25 |
|
8422 | 26 |
Goal "total(le) --> transf(le) --> sorted le (ins le x xs) = sorted le xs"; |
5184 | 27 |
by (induct_tac "xs" 1); |
4686 | 28 |
by (ALLGOALS Asm_simp_tac); |
8422 | 29 |
by (rewrite_goals_tac [Sorting.total_def, Sorting.transf_def]); |
30 |
by (Blast_tac 1); |
|
31 |
qed_spec_mp "sorted_ins"; |
|
2511 | 32 |
Addsimps [sorted_ins]; |
969 | 33 |
|
8422 | 34 |
Goal "[| total(le); transf(le) |] ==> sorted le (insort le xs)"; |
5184 | 35 |
by (induct_tac "xs" 1); |
8422 | 36 |
by Auto_tac; |
1750
817a34a54fb0
replaced result() by qed "sorted_insort" in last proof
berghofe
parents:
1465
diff
changeset
|
37 |
qed "sorted_insort"; |