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