|
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 (* insertion sort, would need lists different from script-lists WN.11.00 |
|
11 WN.7.5.03: -"- started with someList :: 'a list => unl, fun dest_list |
|
12 WN.8.5.03: error (@@@) remained with outcommenting foldr ?!? |
|
13 |
|
14 use_thy_only"Knowledge/InsSort"; |
|
15 |
|
16 *) |
|
17 |
|
18 InsSort = Script + |
|
19 |
|
20 consts |
|
21 |
|
22 (*foldr :: [['a,'b] => 'a, 'b list, 'a] => 'a |
|
23 WN.8.5.03: already defined in Isabelle2002 (instantiated by Typefix): |
|
24 "[[real, real] => real, real list, real] => real") : term |
|
25 |
|
26 val t = str2term "foldr"; |
|
27 val t = |
|
28 Const |
|
29 ("List.foldr", |
|
30 "[[RealDef.real, RealDef.real] => RealDef.real, RealDef.real List.list, |
|
31 RealDef.real] => RealDef.real") : term |
|
32 *) |
|
33 ins :: ['a list,'a] => 'a list |
|
34 sort :: 'a list => 'a list |
|
35 |
|
36 (*descriptions, script-id*) |
|
37 unsorted :: 'a list => unl |
|
38 sorted :: 'a list => unl |
|
39 |
|
40 (*subproblem and script-name*) |
|
41 Ins'_sort :: "['a list, \ |
|
42 \ 'a list] => 'a list" |
|
43 ("((Script Ins'_sort (_ =))// \ |
|
44 \ (_))" 9) |
|
45 Sort :: "['a list, \ |
|
46 \ 'a list] => 'a list" |
|
47 ("((Script Sort (_ =))// \ |
|
48 \ (_))" 9) |
|
49 |
|
50 (*primrec |
|
51 foldr_base "foldr f [] a = a" |
|
52 foldr_rec "foldr f (x#xs) a = foldr f xs (f a x)" |
|
53 *) |
|
54 |
|
55 rules |
|
56 |
|
57 (*primrec .. outcommented analoguous to ListC.thy*) |
|
58 ins_base "ins [] a = [a]" |
|
59 ins_rec "ins (x#xs) a = (if x < a then x#(ins xs a) else a#(x#xs))" |
|
60 |
|
61 sort_def "sort ls = foldr ins ls []" |
|
62 |
|
63 end |