(* Title: HOL/ex/insort.thy ID: $Id: InSort.thy,v 1.9 2005/04/22 15:32:03 paulson Exp $ Author: Tobias Nipkow Copyright 1994 TU Muenchen *) header{*Insertion Sort*} theory InSort imports Sorting begin consts ins :: "('a => 'a => bool) => 'a => 'a list => 'a list" insort :: "('a => 'a => bool) => 'a list => '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]: "!!y. multiset_of (ins le x xs) = multiset_of (x#xs)" by (induct xs) (auto simp: union_ac) theorem insort_permutes[simp]: "!!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]: "[| total le; transf le |] ==> 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
lemma multiset_ins:
multiset_of (ins le x xs) = multiset_of (x # xs)
theorem insort_permutes:
multiset_of (insort le xs) = multiset_of xs
lemma set_ins:
set (ins le x xs) = insert x (set xs)
lemma sorted_ins:
[| total le; transf le |] ==> sorted le (ins le x xs) = sorted le xs
theorem sorted_insort:
[| total le; transf le |] ==> sorted le (insort le xs)