src/HOL/ex/InSort.thy
 author obua Mon Apr 10 16:00:34 2006 +0200 (2006-04-10) changeset 19404 9bf2cdc9e8e8 parent 15815 62854cac5410 permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
```     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
```