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