author | paulson |
Thu, 21 Aug 1997 12:53:23 +0200 | |
changeset 3647 | a64c8fbcd98f |
parent 3465 | e85c24717cad |
child 3919 | c036caebfc75 |
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); |
|
12 |
by (asm_simp_tac (!simpset setloop (split_tac [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)"; |
3647
a64c8fbcd98f
Renamed theorems of the form set_of_list_XXX to set_XXX
paulson
parents:
3465
diff
changeset
|
22 |
by (asm_simp_tac (!simpset addsimps [set_via_mset] |
2517 | 23 |
setloop (split_tac [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); |
31 |
by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if])))); |
|
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"; |