# Theory InSort

Up to index of Isabelle/HOL/ex

theory InSort
imports Sorting
begin

    (*  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)