1 (* use"test-inssort.sml";
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 *)
8 "--------------- sort [1,4,3,2] by rewrite_set ----------------";
10 val ct = "sort [1,4,3,2]";
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";
18 "---------------- sort [1,3,2] by rewrite stepwise ----------------";
20 val ct = "sort [1,3,2]";
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] []"*)
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)"*)
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]"*)
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)"*)
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])"*)
43 val (ct,_) = the (calculate thy' op_ ct);
44 (*val ct = "foldr ins [#2] (if True then #1 # ins [] #3 else [#3, #1])"*)
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)"*)
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]"*)
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)"*)
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])"*)
63 val (ct,_) = the (calculate thy' op_ ct);
64 (*val ct = "foldr ins [] (if True then #1 # ins [#3] #2 else [#2, #1, #3])"*)
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)"*)
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]))"*)
75 val (ct,_) = the (calculate thy' op_ ct);
76 (*val ct = "foldr ins [] (#1 # (if False then #3 # ins [] #2 else [#2, #3]))"*)
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]"*)
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";
89 "---------------- sort [1,3,2] from script ----------------";
90 val fmz = ["unsorted [1,3,2]", "sorted S"];
92 ("InsSort", ["inssort","functional"], ("InsSort","inssort"));
93 val p = e_pos'; val c = [];
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_");
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_ \
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_; \
136 atomty (term_of (the scr));