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

*)

(* tools for insertion sort

   use"Knowledge/InsSort.ML";

*)

(** interface isabelle -- isac **)

theory' := (!theory') @ [("InsSort.thy",InsSort.thy)];

(** rule set **)

val ins_sort = prep_rls(

  Rls{preconds = [], rew_ord = ("tless_true",tless_true),

      rules = [Thm ("foldr_base",(*num_str*) foldr_base),

	       Thm ("foldr_rec",foldr_rec),

	       Thm ("ins_base",ins_base),

	       Thm ("ins_rec",ins_rec),

	       Thm ("sort_def",sort_def),

	       Calc ("op <",eval_equ "#less_"),

	       Thm ("if_True", if_True),

	       Thm ("if_False", if_False)

	       ],

      scr = Script ((term_of o the o (parse thy)) 

      "empty_script")

      }:rls);      

(** problem type **)

store_pbt

 (prep_pbt InsSort.thy

 (["functional"]:pblID,

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

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

  ],

  []));

store_pbt

 (prep_pbt InsSort.thy

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

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

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

  ],

  []));

(** method, 

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

store_met

 (prep_met Diff.thy

 (["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 InsSort.thy (*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 thy (!ruleset',

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

			 ]:(string * rls) list);