equal
deleted
inserted
replaced
1 (* Author: Tobias Nipkow *) |
1 (* Author: Tobias Nipkow *) |
2 |
|
3 (* FIXME adjust List.sorted to work like below; [code] is different! *) |
|
4 |
2 |
5 theory Sorting |
3 theory Sorting |
6 imports |
4 imports |
7 Complex_Main |
5 Complex_Main |
8 "HOL-Library.Multiset" |
6 "HOL-Library.Multiset" |
9 begin |
7 begin |
10 |
8 |
11 hide_const List.sorted List.insort |
9 hide_const List.insort |
12 |
10 |
13 declare Let_def [simp] |
11 declare Let_def [simp] |
14 |
|
15 fun sorted :: "'a::linorder list \<Rightarrow> bool" where |
|
16 "sorted [] = True" | |
|
17 "sorted (x # xs) = ((\<forall>y\<in>set xs. x \<le> y) & sorted xs)" |
|
18 |
|
19 lemma sorted_append: |
|
20 "sorted (xs@ys) = (sorted xs & sorted ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))" |
|
21 by (induct xs) (auto) |
|
22 |
|
23 lemma sorted01: "length xs \<le> 1 \<Longrightarrow> sorted xs" |
|
24 by(auto simp: le_Suc_eq length_Suc_conv) |
|
25 |
12 |
26 |
13 |
27 subsection "Insertion Sort" |
14 subsection "Insertion Sort" |
28 |
15 |
29 fun insort :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
16 fun insort :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> 'a list" where |