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