(* 6.8.02 change to Isabelle2002 caused error -- thy excluded !

Proving equations for primrec function(s) "InsSort.foldr" ...

GC #1.17.30.54.345.21479:   (10 ms)

*** Definition of InsSort.ins :: "['a::ord list, 'a::ord] => 'a::ord list"

*** imposes additional sort constraints on the declared type of the constant

*** The error(s) above occurred in definition "InsSort.ins.ins_list_def (@@@)"

*)

(* insertion sort, would need lists different from script-lists WN.11.00

WN.7.5.03: -"- started with someList :: 'a list => unl, fun dest_list

WN.8.5.03: error (@@@) remained with outcommenting foldr ?!?

 use_thy_only"Knowledge/InsSort";

*)

InsSort = Script +

consts

(*foldr      :: [['a,'b] => 'a, 'b list, 'a] => 'a

WN.8.5.03: already defined in Isabelle2002 (instantiated by Typefix):

     "[[real, real] => real, real list, real] => real") : term

 val t = str2term "foldr";

val t =

  Const

    ("List.foldr",

     "[[RealDef.real, RealDef.real] => RealDef.real, RealDef.real List.list,

      RealDef.real] => RealDef.real") : term

 *)

  ins        :: ['a list,'a] => 'a list

  sort       :: 'a list => 'a list

(*descriptions, script-id*)

  unsorted   :: 'a list => unl

  sorted     :: 'a list => unl

(*subproblem and script-name*)

  Ins'_sort  :: "['a list, \

		  \ 'a list] => 'a list"

               ("((Script Ins'_sort (_ =))// \

		  \ (_))" 9)

  Sort       :: "['a list, \

		  \ 'a list] => 'a list"

               ("((Script Sort (_ =))// \

		  \ (_))" 9)

(*primrec

  foldr_base "foldr f [] a = a"

  foldr_rec  "foldr f (x#xs) a = foldr f xs (f a x)"

*)

rules

(*primrec .. outcommented analoguous to ListC.thy*)

  ins_base   "ins [] a = [a]"

  ins_rec    "ins (x#xs) a = (if x < a then x#(ins xs a) else a#(x#xs))" 

  sort_def   "sort ls = foldr ins ls []"

end