src/HOL/ex/InSort.thy

Tuned signature of Locale.add_locale(_i).

(*  Title:      HOL/ex/insort.thy
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   1994 TU Muenchen
*)

header{*Insertion Sort*}

theory InSort
imports Sorting
begin

consts
  ins    :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
  insort :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list"

primrec
  "ins le x [] = [x]"
  "ins le x (y#ys) = (if le x y then (x#y#ys) else y#(ins le x ys))"

primrec
  "insort le [] = []"
  "insort le (x#xs) = ins le x (insort le xs)"


lemma multiset_ins[simp]:
 "\<And>y. multiset_of (ins le x xs) = multiset_of (x#xs)"
  by (induct xs) (auto simp: union_ac)

theorem insort_permutes[simp]:
 "\<And>x. multiset_of (insort le xs) = multiset_of xs"
  by (induct "xs") auto

lemma set_ins [simp]: "set(ins le x xs) = insert x (set xs)"
  by (simp add: set_count_greater_0) fast

lemma sorted_ins[simp]:
 "\<lbrakk> total le; transf le \<rbrakk> \<Longrightarrow> sorted le (ins le x xs) = sorted le xs";
apply (induct xs)
apply simp_all
apply (unfold Sorting.total_def Sorting.transf_def)
apply blast
done

theorem sorted_insort:
 "[| total(le); transf(le) |] ==>  sorted le (insort le xs)"
by (induct xs) auto

end