|
1 (* use"test-inssort.sml"; |
|
2 W.N.17.6.00 |
|
3 *) |
|
4 |
|
5 (* insertion sort, would need lists different from script-lists WN.11.00 |
|
6 WN.7.6.03: -"- started with someList :: 'a list => unl, fun dest_list *) |
|
7 |
|
8 "--------------- sort [1,4,3,2] by rewrite_set ----------------"; |
|
9 val thy' = "InsSort.thy"; |
|
10 val ct = "sort [1,4,3,2]"; |
|
11 "--- 1 ---"; |
|
12 val rls = "ins_sort"; |
|
13 val (ct,_) = the (rewrite_set thy' "eval_rls" false rls ct); |
|
14 if ct="[1, 2, 3, 4]" then "sort [1,4,3,2] OK" |
|
15 else raise error "sort [1,4,3,2] didn't work"; |
|
16 |
|
17 |
|
18 "---------------- sort [1,3,2] by rewrite stepwise ----------------"; |
|
19 val thy' = "InsSort.thy"; |
|
20 val ct = "sort [1,3,2]"; |
|
21 "--- 1 ---"; |
|
22 val thm = ("sort_def",""); |
|
23 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); |
|
24 (*val ct = "foldr ins [#1::real, #3::real, #2::real] []"*) |
|
25 "--- 2 ---"; |
|
26 val thm = ("foldr_rec",""); |
|
27 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); |
|
28 (*val ct = "foldr ins [#3, #2] (ins [] #1)"*) |
|
29 "--- 3 ---"; |
|
30 val thm = ("ins_base",""); |
|
31 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); |
|
32 (*val ct = "foldr ins [#3, #2] [#1]"*) |
|
33 "--- 4 ---"; |
|
34 val thm = ("foldr_rec",""); |
|
35 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); |
|
36 (*val ct = "foldr ins [#2] (ins [#1] #3)"*) |
|
37 "--- 5 ---"; |
|
38 val thm = ("ins_rec",""); |
|
39 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); |
|
40 (*val ct = "foldr ins [#2] (if #1 < #3 then #1 # ins [] #3 else [#3, #1])"*) |
|
41 "--- 6 ---"; |
|
42 val op_ = "le"; |
|
43 val (ct,_) = the (calculate thy' op_ ct); |
|
44 (*val ct = "foldr ins [#2] (if True then #1 # ins [] #3 else [#3, #1])"*) |
|
45 "--- 7 ---"; |
|
46 val thm = ("if_True",""); |
|
47 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); |
|
48 (*val ct = "foldr ins [#2] (#1 # ins [] #3)"*) |
|
49 "--- 8 ---"; |
|
50 val thm = ("ins_base",""); |
|
51 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); |
|
52 (*val ct = "foldr ins [#2] [#1, #3]"*) |
|
53 "--- 9 ---"; |
|
54 val thm = ("foldr_rec",""); |
|
55 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); |
|
56 (*val ct = "foldr ins [] (ins [#1, #3] #2)"*) |
|
57 "--- 10 ---"; |
|
58 val thm = ("ins_rec",""); |
|
59 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); |
|
60 (*val ct = "foldr ins [] (if #1 < #2 then #1 # ins [#3] #2 else [#2, #1, #3])"*) |
|
61 "--- 11 ---"; |
|
62 val op_ = "le"; |
|
63 val (ct,_) = the (calculate thy' op_ ct); |
|
64 (*val ct = "foldr ins [] (if True then #1 # ins [#3] #2 else [#2, #1, #3])"*) |
|
65 "--- 12 ---"; |
|
66 val thm = ("if_True",""); |
|
67 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); |
|
68 (*"foldr ins [] (#1 # ins [#3] #2)"*) |
|
69 "--- 13 ---"; |
|
70 val thm = ("ins_rec",""); |
|
71 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); |
|
72 (*"foldr ins [] (#1 # (if #3 < #2 then #3 # ins [] #2 else [#2, #3]))"*) |
|
73 "--- 14 ---"; |
|
74 val op_ = "le"; |
|
75 val (ct,_) = the (calculate thy' op_ ct); |
|
76 (*val ct = "foldr ins [] (#1 # (if False then #3 # ins [] #2 else [#2, #3]))"*) |
|
77 "--- 15 ---"; |
|
78 val thm = ("if_False",""); |
|
79 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); |
|
80 (*val ct = "foldr ins [] [#1, #2, #3]"*) |
|
81 "--- 16 ---"; |
|
82 val thm = ("foldr_base",""); |
|
83 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); |
|
84 (*val ct = "[#1, #2, #3]"*) |
|
85 if ct="[1, 2, 3]" then "sort [1,3,2] OK" |
|
86 else raise error "sort [1,3,2] didn't work"; |
|
87 |
|
88 |
|
89 "---------------- sort [1,3,2] from script ----------------"; |
|
90 val fmz = ["unsorted [1,3,2]", "sorted S"]; |
|
91 val (dI',pI',mI') = |
|
92 ("InsSort.thy", ["inssort","functional"], ("InsSort.thy","inssort")); |
|
93 val p = e_pos'; val c = []; |
|
94 |
|
95 |
|
96 |
|
97 (* ------- 17.6.00: mit kleinen problemen aufgegeben |
|
98 val scr=Script ((term_of o the o (parse thy)) |
|
99 "Script Sort (u_::'a list) = \ |
|
100 \ Rewrite_Set ins_sort False u_"); |
|
101 |
|
102 val scr=Script ((term_of o the o (parse thy)) |
|
103 "Script Ins_sort (u_::real list) = \ |
|
104 \ (let u_ = Rewrite sort_def False u_; \ |
|
105 \ u_ = Rewrite foldr_rec False u_; \ |
|
106 \ u_ = Rewrite ins_base False u_; \ |
|
107 \ u_ = Rewrite foldr_rec False u_; \ |
|
108 \ u_ = Rewrite ins_rec False u_; \ |
|
109 \ u_ = Calculate le u_; \ |
|
110 \ u_ = Rewrite if_True False u_; \ |
|
111 \ u_ = Rewrite ins_base False u_; \ |
|
112 \ u_ = Rewrite foldr_rec False u_; \ |
|
113 \ u_ = Rewrite ins_rec False u_; \ |
|
114 \ u_ = Calculate le u_; \ |
|
115 \ u_ = Rewrite if_True False u_; \ |
|
116 \ u_ = Rewrite ins_rec False u_; \ |
|
117 \ u_ = Calculate le u_; \ |
|
118 \ u_ = Rewrite if_False False u_; \ |
|
119 \ u_ = Rewrite foldr_base False u_ \ |
|
120 \ in u_)"); |
|
121 val scr=parse thy |
|
122 "Script Ins_sort (u_::real list) = \ |
|
123 \ (let u_ = Rewrite sort_def False u_; \ |
|
124 \ u_ = Rewrite foldr_rec False u_; \ |
|
125 \ u_ = Rewrite ins_base False u_; \ |
|
126 \ u_ = Rewrite foldr_rec False u_; \ |
|
127 \ u_ = Rewrite ins_rec False u_; \ |
|
128 \ u_ = Calculate le u_; \ |
|
129 \ u_ = Rewrite if_True False u_; \ |
|
130 \ u_ = Rewrite ins_base False u_; \ |
|
131 \ u_ = Rewrite foldr_rec False u_; \ |
|
132 \ u_ = Rewrite ins_rec False u_; \ |
|
133 \ u_ = u_ \ |
|
134 \ in u_)"; |
|
135 |
|
136 atomty (term_of (the scr)); |
|
137 |
|
138 ------- *) |