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

 *)

 theory InsSort imports "../ProgLang/Script" begin

 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 []"

 ML {*

 (** problem type **)

 store_pbt

  (prep_pbt @{theory "InsSort"}

  (["functional"]:pblID,

   [("#Given" ,["unsorted u_"]),

    ("#Find"  ,["sorted s_"])

   ],

   []));

 store_pbt

  (prep_pbt @{theory "InsSort"}

  (["inssort","functional"]:pblID,

   [("#Given" ,["unsorted u_"]),

    ("#Find"  ,["sorted s_"])

   ],

   []));

 *}

 setup {* KEStore_Elems.add_pbts

   [(prep_pbt @{theory "InsSort"}

       (["functional"]:pblID,

         [("#Given" ,["unsorted u_"]), ("#Find"  ,["sorted s_"])], [])),

     (prep_pbt @{theory "InsSort"}

       (["inssort","functional"]:pblID,

         [("#Given" ,["unsorted u_"]), ("#Find"  ,["sorted s_"])], []))] *}

 ML {*

 (** method, 

     todo: implementation needs extra object-level lists **)

 store_met

  (prep_met @{theory "Diff"}

  (["InsSort"],

    [],

    {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,

     crls = Atools_rls, errpats = [], nrls = norm_Rational

     (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));

 store_met

  (prep_met @{theory "InsSort"} (*test-version for [#1,#3,#2] only: see *.sml*)

  (["InsSort","sort"]:metID,

    [("#Given" ,["unsorted u_"]),

     ("#Find"  ,["sorted s_"])

     ],

    {rew_ord'="tless_true",rls'=eval_rls,calc = [], srls = e_rls, prls=e_rls,

     crls = eval_rls, errpats = [], nrls = norm_Rational},

    "Script Sort (u_::'a list) = (Rewrite_Set ins_sort False) u_"

   ));

 *}

 setup {* KEStore_Elems.add_rlss [("ins_sort", (Context.theory_name @{theory}, ins_sort))] *}

 end