1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/Knowledge/InsSort.ML	Wed Aug 25 16:20:07 2010 +0200
     1.3 @@ -0,0 +1,77 @@
     1.4 +(* 6.8.02 change to Isabelle2002 caused error -- thy excluded !
     1.5 +
     1.6 +Proving equations for primrec function(s) "InsSort.foldr" ...
     1.7 +GC #1.17.30.54.345.21479:   (10 ms)
     1.8 +*** Definition of InsSort.ins :: "['a::ord list, 'a::ord] => 'a::ord list"
     1.9 +*** imposes additional sort constraints on the declared type of the constant
    1.10 +*** The error(s) above occurred in definition "InsSort.ins.ins_list_def"
    1.11 +*)
    1.12 +
    1.13 +(* tools for insertion sort
    1.14 +   use"Knowledge/InsSort.ML";
    1.15 +*)
    1.16 +
    1.17 +(** interface isabelle -- isac **)
    1.18 +
    1.19 +theory' := (!theory') @ [("InsSort.thy",InsSort.thy)];
    1.20 +
    1.21 +(** rule set **)
    1.22 +
    1.23 +val ins_sort = prep_rls(
    1.24 +  Rls{preconds = [], rew_ord = ("tless_true",tless_true),
    1.25 +      rules = [Thm ("foldr_base",(*num_str*) foldr_base),
    1.26 +	       Thm ("foldr_rec",foldr_rec),
    1.27 +	       Thm ("ins_base",ins_base),
    1.28 +	       Thm ("ins_rec",ins_rec),
    1.29 +	       Thm ("sort_def",sort_def),
    1.30 +
    1.31 +	       Calc ("op <",eval_equ "#less_"),
    1.32 +	       Thm ("if_True", if_True),
    1.33 +	       Thm ("if_False", if_False)
    1.34 +	       ],
    1.35 +      scr = Script ((term_of o the o (parse thy)) 
    1.36 +      "empty_script")
    1.37 +      }:rls);      
    1.38 +
    1.39 +(** problem type **)
    1.40 +
    1.41 +store_pbt
    1.42 + (prep_pbt InsSort.thy
    1.43 + (["functional"]:pblID,
    1.44 +  [("#Given" ,["unsorted u_"]),
    1.45 +   ("#Find"  ,["sorted s_"])
    1.46 +  ],
    1.47 +  []));
    1.48 +
    1.49 +store_pbt
    1.50 + (prep_pbt InsSort.thy
    1.51 + (["inssort","functional"]:pblID,
    1.52 +  [("#Given" ,["unsorted u_"]),
    1.53 +   ("#Find"  ,["sorted s_"])
    1.54 +  ],
    1.55 +  []));
    1.56 +
    1.57 +(** method, 
    1.58 +    todo: implementation needs extra object-level lists **)
    1.59 +
    1.60 +store_met
    1.61 + (prep_met Diff.thy
    1.62 + (["InsSort"],
    1.63 +   [],
    1.64 +   {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
    1.65 +    crls = Atools_rls, nrls=norm_Rational
    1.66 +    (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
    1.67 +store_met
    1.68 + (prep_met InsSort.thy (*test-version for [#1,#3,#2] only: see *.sml*)
    1.69 + (["InsSort""sort"]:metID,
    1.70 +   [("#Given" ,["unsorted u_"]),
    1.71 +    ("#Find"  ,["sorted s_"])
    1.72 +    ],
    1.73 +   {rew_ord'="tless_true",rls'=eval_rls,calc = [], srls = e_rls, prls=e_rls,
    1.74 +    crls = eval_rls, nrls=norm_Rational(*,asm_rls=[],asm_thm=[]*)},
    1.75 +   "Script Sort (u_::'a list) = (Rewrite_Set ins_sort False) u_"
    1.76 +  ));
    1.77 +
    1.78 +ruleset' := overwritelthy thy (!ruleset',
    1.79 +			[(*("ins_sort",ins_sort) overwrites a Isa fun!!*)
    1.80 +			 ]:(string * rls) list);