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