4 |
4 |
5 (* insertion sort, would need lists different from script-lists WN.11.00 |
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 *) |
6 WN.7.6.03: -"- started with someList :: 'a list => unl, fun dest_list *) |
7 |
7 |
8 "--------------- sort [1,4,3,2] by rewrite_set ----------------"; |
8 "--------------- sort [1,4,3,2] by rewrite_set ----------------"; |
9 val thy' = "InsSort.thy"; |
9 val thy' = "InsSort"; |
10 val ct = "sort [1,4,3,2]"; |
10 val ct = "sort [1,4,3,2]"; |
11 "--- 1 ---"; |
11 "--- 1 ---"; |
12 val rls = "ins_sort"; |
12 val rls = "ins_sort"; |
13 val (ct,_) = the (rewrite_set thy' "eval_rls" false rls ct); |
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" |
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"; |
15 else raise error "sort [1,4,3,2] didn't work"; |
16 |
16 |
17 |
17 |
18 "---------------- sort [1,3,2] by rewrite stepwise ----------------"; |
18 "---------------- sort [1,3,2] by rewrite stepwise ----------------"; |
19 val thy' = "InsSort.thy"; |
19 val thy' = "InsSort"; |
20 val ct = "sort [1,3,2]"; |
20 val ct = "sort [1,3,2]"; |
21 "--- 1 ---"; |
21 "--- 1 ---"; |
22 val thm = ("sort_def",""); |
22 val thm = ("sort_def",""); |
23 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); |
23 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); |
24 (*val ct = "foldr ins [#1::real, #3::real, #2::real] []"*) |
24 (*val ct = "foldr ins [#1::real, #3::real, #2::real] []"*) |
87 |
87 |
88 |
88 |
89 "---------------- sort [1,3,2] from script ----------------"; |
89 "---------------- sort [1,3,2] from script ----------------"; |
90 val fmz = ["unsorted [1,3,2]", "sorted S"]; |
90 val fmz = ["unsorted [1,3,2]", "sorted S"]; |
91 val (dI',pI',mI') = |
91 val (dI',pI',mI') = |
92 ("InsSort.thy", ["inssort","functional"], ("InsSort.thy","inssort")); |
92 ("InsSort", ["inssort","functional"], ("InsSort","inssort")); |
93 val p = e_pos'; val c = []; |
93 val p = e_pos'; val c = []; |
94 |
94 |
95 |
95 |
96 |
96 |
97 (* ------- 17.6.00: mit kleinen problemen aufgegeben |
97 (* ------- 17.6.00: mit kleinen problemen aufgegeben |