(* 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_"])

  ],

  []));

(** 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, 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, nrls=norm_Rational(*,asm_rls=[],asm_thm=[]*)},

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

  ));

ruleset' := overwritelthy @{theory} (!ruleset',

			[(*("ins_sort",ins_sort) overwrites a Isa fun!!*)

			 ]:(string * rls) list);

*}

end