equal
deleted
inserted
replaced
1 (* Title: HOL/ex/insort.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1994 TU Muenchen |
|
5 *) |
|
6 |
|
7 header{*Insertion Sort*} |
|
8 |
|
9 theory InSort |
|
10 imports Sorting |
|
11 begin |
|
12 |
|
13 consts |
|
14 ins :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
15 insort :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
16 |
|
17 primrec |
|
18 "ins le x [] = [x]" |
|
19 "ins le x (y#ys) = (if le x y then (x#y#ys) else y#(ins le x ys))" |
|
20 |
|
21 primrec |
|
22 "insort le [] = []" |
|
23 "insort le (x#xs) = ins le x (insort le xs)" |
|
24 |
|
25 |
|
26 lemma multiset_ins[simp]: |
|
27 "\<And>y. multiset_of (ins le x xs) = multiset_of (x#xs)" |
|
28 by (induct xs) (auto simp: union_ac) |
|
29 |
|
30 theorem insort_permutes[simp]: |
|
31 "\<And>x. multiset_of (insort le xs) = multiset_of xs" |
|
32 by (induct "xs") auto |
|
33 |
|
34 lemma set_ins [simp]: "set(ins le x xs) = insert x (set xs)" |
|
35 by (simp add: set_count_greater_0) fast |
|
36 |
|
37 lemma sorted_ins[simp]: |
|
38 "\<lbrakk> total le; transf le \<rbrakk> \<Longrightarrow> sorted le (ins le x xs) = sorted le xs"; |
|
39 apply (induct xs) |
|
40 apply simp_all |
|
41 apply (unfold Sorting.total_def Sorting.transf_def) |
|
42 apply blast |
|
43 done |
|
44 |
|
45 theorem sorted_insort: |
|
46 "[| total(le); transf(le) |] ==> sorted le (insort le xs)" |
|
47 by (induct xs) auto |
|
48 |
|
49 end |
|
50 |
|