|
1 (* 6.8.02 change to Isabelle2002 caused error -- thy excluded ! |
|
2 |
|
3 Proving equations for primrec function(s) "InsSort.foldr" ... |
|
4 GC #1.17.30.54.345.21479: (10 ms) |
|
5 *** Definition of InsSort.ins :: "['a::ord list, 'a::ord] => 'a::ord list" |
|
6 *** imposes additional sort constraints on the declared type of the constant |
|
7 *** The error(s) above occurred in definition "InsSort.ins.ins_list_def" |
|
8 *) |
|
9 |
|
10 (* tools for insertion sort |
|
11 use"Knowledge/InsSort.ML"; |
|
12 *) |
|
13 |
|
14 (** interface isabelle -- isac **) |
|
15 |
|
16 theory' := (!theory') @ [("InsSort.thy",InsSort.thy)]; |
|
17 |
|
18 (** rule set **) |
|
19 |
|
20 val ins_sort = prep_rls( |
|
21 Rls{preconds = [], rew_ord = ("tless_true",tless_true), |
|
22 rules = [Thm ("foldr_base",(*num_str*) foldr_base), |
|
23 Thm ("foldr_rec",foldr_rec), |
|
24 Thm ("ins_base",ins_base), |
|
25 Thm ("ins_rec",ins_rec), |
|
26 Thm ("sort_def",sort_def), |
|
27 |
|
28 Calc ("op <",eval_equ "#less_"), |
|
29 Thm ("if_True", if_True), |
|
30 Thm ("if_False", if_False) |
|
31 ], |
|
32 scr = Script ((term_of o the o (parse thy)) |
|
33 "empty_script") |
|
34 }:rls); |
|
35 |
|
36 (** problem type **) |
|
37 |
|
38 store_pbt |
|
39 (prep_pbt InsSort.thy |
|
40 (["functional"]:pblID, |
|
41 [("#Given" ,["unsorted u_"]), |
|
42 ("#Find" ,["sorted s_"]) |
|
43 ], |
|
44 [])); |
|
45 |
|
46 store_pbt |
|
47 (prep_pbt InsSort.thy |
|
48 (["inssort","functional"]:pblID, |
|
49 [("#Given" ,["unsorted u_"]), |
|
50 ("#Find" ,["sorted s_"]) |
|
51 ], |
|
52 [])); |
|
53 |
|
54 (** method, |
|
55 todo: implementation needs extra object-level lists **) |
|
56 |
|
57 store_met |
|
58 (prep_met Diff.thy |
|
59 (["InsSort"], |
|
60 [], |
|
61 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls, |
|
62 crls = Atools_rls, nrls=norm_Rational |
|
63 (*, asm_rls=[],asm_thm=[]*)}, "empty_script")); |
|
64 store_met |
|
65 (prep_met InsSort.thy (*test-version for [#1,#3,#2] only: see *.sml*) |
|
66 (["InsSort""sort"]:metID, |
|
67 [("#Given" ,["unsorted u_"]), |
|
68 ("#Find" ,["sorted s_"]) |
|
69 ], |
|
70 {rew_ord'="tless_true",rls'=eval_rls,calc = [], srls = e_rls, prls=e_rls, |
|
71 crls = eval_rls, nrls=norm_Rational(*,asm_rls=[],asm_thm=[]*)}, |
|
72 "Script Sort (u_::'a list) = (Rewrite_Set ins_sort False) u_" |
|
73 )); |
|
74 |
|
75 ruleset' := overwritelthy thy (!ruleset', |
|
76 [(*("ins_sort",ins_sort) overwrites a Isa fun!!*) |
|
77 ]:(string * rls) list); |