1 |
|
2 |
|
3 (*-------------------------from InsSort.thy 8.3.01----------------------*) |
|
4 (*List.thy: |
|
5 foldl :: [['b,'a] => 'b, 'b, 'a list] => 'b |
|
6 primrec |
|
7 foldl_Nil "foldl f a [] = a" |
|
8 foldl_Cons "foldl f a (x#xs) = foldl f (f a x) xs" |
|
9 |
|
10 above in sml: |
|
11 fun foldr f [] a = a |
|
12 | foldr f (x::xs) a = foldr f xs (f a x); |
|
13 (*val fold = fn : ('a -> 'b -> 'a) -> 'b list -> 'a -> 'a*) |
|
14 fun ins [] a = [a] |
|
15 | ins (x::xs) a = if x < a then x::(ins xs a) else a::(x::xs); |
|
16 fun sort xs = foldr ins xs []; |
|
17 *) |
|
18 (*-------------------------from InsSort.thy 8.3.01----------------------*) |
|
19 |
|
20 |
|
21 (*-------------------------from InsSort.ML 8.3.01----------------------*) |
|
22 |
|
23 theory' := (!theory') @ [("InsSort.thy",InsSort.thy)]; |
|
24 |
|
25 val ins_sort = |
|
26 Rls{preconds = [], rew_ord = ("tless_true",tless_true), |
|
27 rules = [Thm ("foldr_base",(*num_str*) foldr_base), |
|
28 Thm ("foldr_rec",foldr_rec), |
|
29 Thm ("ins_base",ins_base), |
|
30 Thm ("ins_rec",ins_rec), |
|
31 Thm ("sort_def",sort_def), |
|
32 |
|
33 Calc ("op <",eval_equ "#less_"), |
|
34 Thm ("if_True", if_True), |
|
35 Thm ("if_False", if_False) |
|
36 ], |
|
37 scr = Script ((term_of o the o (parse thy)) |
|
38 "empty_script") |
|
39 }:rls; |
|
40 |
|
41 |
|
42 |
|
43 |
|
44 (* |
|
45 > get_pbt ["Script.thy","squareroot","univariate","equation"]; |
|
46 > get_met ("Script.thy","max_on_interval_by_calculus"); |
|
47 *) |
|
48 pbltypes:= (!pbltypes) @ |
|
49 [ |
|
50 prep_pbt InsSort.thy |
|
51 (["InsSort.thy","inssort"]:pblID, |
|
52 [("#Given" ,"unsorted u_"), |
|
53 ("#Find" ,"sorted s_") |
|
54 ]) |
|
55 ]; |
|
56 |
|
57 methods:= (!methods) @ |
|
58 [ |
|
59 (*, -------17.6.00, |
|
60 (("InsSort.thy","inssort"):metID, |
|
61 {ppc = prep_met |
|
62 [("#Given" ,"unsorted u_"), |
|
63 ("#Find" ,"sorted s_") |
|
64 ], |
|
65 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
|
66 scr=Script (((inst_abs (assoc_thm "InsSort.thy")) |
|
67 o term_of o the o (parse thy)) (*for [#1,#3,#2] only*) |
|
68 "Script Ins_sort (u_::'a list) = \ |
|
69 \ (let u_ = Rewrite sort_def False u_; \ |
|
70 \ u_ = Rewrite foldr_rec False u_; \ |
|
71 \ u_ = Rewrite ins_base False u_; \ |
|
72 \ u_ = Rewrite foldr_rec False u_; \ |
|
73 \ u_ = Rewrite ins_rec False u_; \ |
|
74 \ u_ = Calculate le u_; \ |
|
75 \ u_ = Rewrite if_True False u_; \ |
|
76 \ u_ = Rewrite ins_base False u_; \ |
|
77 \ u_ = Rewrite foldr_rec False u_; \ |
|
78 \ u_ = Rewrite ins_rec False u_; \ |
|
79 \ u_ = Calculate le u_; \ |
|
80 \ u_ = Rewrite if_True False u_; \ |
|
81 \ u_ = Rewrite ins_rec False u_; \ |
|
82 \ u_ = Calculate le u_; \ |
|
83 \ u_ = Rewrite if_False False u_; \ |
|
84 \ u_ = Rewrite foldr_base False u_ \ |
|
85 \ in u_)") |
|
86 } : met), |
|
87 |
|
88 (("InsSort.thy","sort"):metID, |
|
89 {ppc = prep_met |
|
90 [("#Given" ,"unsorted u_"), |
|
91 ("#Find" ,"sorted s_") |
|
92 ], |
|
93 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
|
94 scr=Script ((inst_abs o term_of o the o (parse thy)) |
|
95 "Script Sort (u_::'a list) = \ |
|
96 \ Rewrite_Set ins_sort False u_") |
|
97 } : met) |
|
98 ------- *) |
|
99 (*, |
|
100 |
|
101 (("",""):metID, |
|
102 {ppc = prep_met |
|
103 [("#Given" ,""), |
|
104 ("#Find" ,""), |
|
105 ("#Relate","") |
|
106 ], |
|
107 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
|
108 scr=EmptyScr} : met), |
|
109 *) |
|
110 ]; |
|
111 (*-------------------------from InsSort.ML 8.3.01----------------------*) |
|
112 |
|
113 |
|
114 (*------------------------- nipkow ----------------------*) |
|
115 consts |
|
116 sort :: 'a list => 'a list |
|
117 ins :: ['a,'a list] => 'a list |
|
118 (*foldl :: [['a,'b] => 'a, 'a, 'b list] => 'a |
|
119 *) |
|
120 rules |
|
121 ins_base "ins e [] = [e]" |
|
122 ins_rec "ins e (l#ls) = (if l < e then l#(ins e ls) else e#(l#ls))" |
|
123 |
|
124 rules |
|
125 sort_def "sort ls = (foldl ins ls [])" |
|
126 end |
|
127 |
|
128 |
|
129 (** swp: ..L **) |
|
130 (* fn : ('a * 'b -> 'b) -> 'a list -> 'b -> 'b *) |
|
131 fun foldL f [] e = e |
|
132 | foldL f (l::ls) e = f(l,foldL f ls e); |
|
133 |
|
134 (* fn : int * int list -> int list *) |
|
135 fun insL (e,[]) = [e] |
|
136 | insL (e,l::ls) = if l < e then l::(insL(e,ls)) else e::(l::ls); |
|
137 |
|
138 fun sortL ls = foldL insL ls []; |
|
139 |
|
140 sortL [2,3,1]; (* [1,2,3] *) |
|
141 |
|
142 |
|
143 (** swp, curried: ..LC **) |
|
144 (* fn : ('a * 'b -> 'b) -> 'a list -> 'b -> 'b *) |
|
145 fun foldLC f [] e = e |
|
146 | foldLC f (x::xs) e = f x (foldLC f xs e); |
|
147 |
|
148 (* fn : int * int list -> int list *) |
|
149 fun insLC e [] = [e] |
|
150 | insLC e (l::ls) = if l < e then l::(insLC e ls) else e::(l::ls); |
|
151 |
|
152 fun sortLC ls = foldLC insLC ls []; |
|
153 |
|
154 sortLC [2,3,1]; (* [1,2,3] *) |
|
155 |
|
156 |
|
157 (** sml110: ..l **) |
|
158 (* fn : ('a * 'b -> 'b) -> 'b -> 'a list -> 'b *) |
|
159 foldl; |
|
160 (* fn : ('a * 'a -> 'a) -> 'a * 'b list -> 'a : ANDERS !!! |
|
161 fun foldl f e [] = e |
|
162 | foldl f e (l::ls) = f e (foldl f (e,ls)); 0+...+0+0 |
|
163 |
|
164 foldl op+ (0,[100,11,1]); |
|
165 val it = 0 : int ... GEHT NICHT !!! *) |
|
166 |
|
167 fun insl (e,[]) = [e] |
|
168 | insl (e,l::ls) = if l < e then l::(insl(e,ls)) else e::(l::ls); |
|
169 |
|
170 fun sortl ls = foldl insl [] ls; |
|
171 |
|
172 sortl [2,3,1]; (* [1,2,3] *) |
|
173 |
|
174 |
|
175 (** sml110, curried: ..lC **) |
|
176 (* fn : ('a -> 'a -> 'a) -> 'a -> 'b list -> 'a *) |
|
177 fun foldlC f e [] = e |
|
178 | foldlC f e (l::ls) = f e (foldlC f e ls); |
|
179 |
|
180 (* fn : int -> int list -> int list *) |
|
181 fun inslC e [] = [e] |
|
182 | inslC e (l::ls) = if l < e then l::(inslC e ls) else e::(l::ls); |
|
183 |
|
184 fun sortlC ls = foldlC inslC [] ls; |
|
185 |
|
186 sortlC [2,3,1]; |
|
187 |
|
188 (*--- 15.6.00 ---*) |
|
189 |
|
190 |
|
191 fun Foldl f a [] = a |
|
192 | Foldl f a (x::xs) = Foldl f (f a x) xs; |
|
193 (*val Foldl = fn : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a*) |
|
194 |
|
195 fun add a b = a+b:int; |
|
196 |
|
197 Foldl add 0 [1,2,3]; |
|
198 |
|
199 fun ins0 a [] = [a] |
|
200 | ins0 a (x::xs) = if x < a then x::(ins0 a xs) else a::(x::xs); |
|
201 (*val ins = fn : int -> int list -> int list*) |
|
202 |
|
203 fun ins [] a = [a] |
|
204 | ins (x::xs) a = if x < a then x::(ins xs a) else a::(x::xs); |
|
205 (*val ins = fn : int -> int list -> int list*) |
|
206 |
|
207 ins 3 [1,2,4]; |
|
208 |
|
209 fun sort xs = Foldl ins0 xs []; |
|
210 (*operator domain: int -> int list -> int |
|
211 operand: int -> int list -> int list |
|
212 in expression: |
|
213 Foldl ins |
|
214 *) |
|
215 fun sort xs = Foldl ins xs []; |
|
216 |
|
217 |
|
218 |
|
219 (*--- 17.6.00 ---*) |
|
220 |
|
221 |
|
222 fun foldr f [] a = a |
|
223 | foldr f (x::xs) a = foldr f xs (f a x); |
|
224 (*val fold = fn : ('a -> 'b -> 'a) -> 'b list -> 'a -> 'a*) |
|
225 |
|
226 fun add a b = a+b:int; |
|
227 |
|
228 fold add [1,2,3] 0; |
|
229 |
|
230 fun ins [] a = [a] |
|
231 | ins (x::xs) a = if x < a then x::(ins xs a) else a::(x::xs); |
|
232 (*val ins = fn : int list -> int -> int list*) |
|
233 |
|
234 ins [1,2,4] 3; |
|
235 |
|
236 fun sort xs = foldr ins xs []; |
|
237 |
|
238 sort [3,1,4,2]; |
|
239 |
|
240 |
|
241 |
|
242 (*--- 17.6.00 II ---*) |
|
243 |
|
244 fun foldl f a [] = a |
|
245 | foldl f a (x::xs) = foldl f (f a x) xs; |
|
246 |
|
247 fun ins [] a = [a] |
|
248 | ins (x::xs) a = if x < a then x::(ins xs a) else a::(x::xs); |
|
249 |
|
250 fun sort xs = foldl ins xs []; |
|
251 |
|
252 sort [3,1,4,2]; |
|
253 (*val it = [3,1,4,2] : int list !?!?!?!?!?!?!?!?!?!?!?!?!?!?!?*) |
|
254 |
|
255 (*------------------------- nipkow ----------------------*) |
|
256 consts |
|
257 sort :: 'a list => 'a list |
|
258 ins :: ['a,'a list] => 'a list |
|
259 (*foldl :: [['a,'b] => 'a, 'a, 'b list] => 'a |
|
260 *) |
|
261 rules |
|
262 ins_base "ins e [] = [e]" |
|
263 ins_rec "ins e (l#ls) = (if l < e then l#(ins e ls) else e#(l#ls))" |
|
264 |
|
265 rules |
|
266 sort_def "sort ls = (foldl ins ls [])" |
|
267 end |
|
268 |
|
269 |
|
270 (** swp: ..L **) |
|
271 (* fn : ('a * 'b -> 'b) -> 'a list -> 'b -> 'b *) |
|
272 fun foldL f [] e = e |
|
273 | foldL f (l::ls) e = f(l,foldL f ls e); |
|
274 |
|
275 (* fn : int * int list -> int list *) |
|
276 fun insL (e,[]) = [e] |
|
277 | insL (e,l::ls) = if l < e then l::(insL(e,ls)) else e::(l::ls); |
|
278 |
|
279 fun sortL ls = foldL insL ls []; |
|
280 |
|
281 sortL [2,3,1]; (* [1,2,3] *) |
|
282 |
|
283 |
|
284 (** swp, curried: ..LC **) |
|
285 (* fn : ('a * 'b -> 'b) -> 'a list -> 'b -> 'b *) |
|
286 fun foldLC f [] e = e |
|
287 | foldLC f (x::xs) e = f x (foldLC f xs e); |
|
288 |
|
289 (* fn : int * int list -> int list *) |
|
290 fun insLC e [] = [e] |
|
291 | insLC e (l::ls) = if l < e then l::(insLC e ls) else e::(l::ls); |
|
292 |
|
293 fun sortLC ls = foldLC insLC ls []; |
|
294 |
|
295 sortLC [2,3,1]; (* [1,2,3] *) |
|
296 |
|
297 |
|
298 (** sml110: ..l **) |
|
299 (* fn : ('a * 'b -> 'b) -> 'b -> 'a list -> 'b *) |
|
300 foldl; |
|
301 (* fn : ('a * 'a -> 'a) -> 'a * 'b list -> 'a : ANDERS !!! |
|
302 fun foldl f e [] = e |
|
303 | foldl f e (l::ls) = f e (foldl f (e,ls)); 0+...+0+0 |
|
304 |
|
305 foldl op+ (0,[100,11,1]); |
|
306 val it = 0 : int ... GEHT NICHT !!! *) |
|
307 |
|
308 fun insl (e,[]) = [e] |
|
309 | insl (e,l::ls) = if l < e then l::(insl(e,ls)) else e::(l::ls); |
|
310 |
|
311 fun sortl ls = foldl insl [] ls; |
|
312 |
|
313 sortl [2,3,1]; (* [1,2,3] *) |
|
314 |
|
315 |
|
316 (** sml110, curried: ..lC **) |
|
317 (* fn : ('a -> 'a -> 'a) -> 'a -> 'b list -> 'a *) |
|
318 fun foldlC f e [] = e |
|
319 | foldlC f e (l::ls) = f e (foldlC f e ls); |
|
320 |
|
321 (* fn : int -> int list -> int list *) |
|
322 fun inslC e [] = [e] |
|
323 | inslC e (l::ls) = if l < e then l::(inslC e ls) else e::(l::ls); |
|
324 |
|
325 fun sortlC ls = foldlC inslC [] ls; |
|
326 |
|
327 sortlC [2,3,1]; |
|
328 |
|
329 (*--- 15.6.00 ---*) |
|
330 |
|
331 |
|
332 fun Foldl f a [] = a |
|
333 | Foldl f a (x::xs) = Foldl f (f a x) xs; |
|
334 (*val Foldl = fn : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a*) |
|
335 |
|
336 fun add a b = a+b:int; |
|
337 |
|
338 Foldl add 0 [1,2,3]; |
|
339 |
|
340 fun ins0 a [] = [a] |
|
341 | ins0 a (x::xs) = if x < a then x::(ins0 a xs) else a::(x::xs); |
|
342 (*val ins = fn : int -> int list -> int list*) |
|
343 |
|
344 fun ins [] a = [a] |
|
345 | ins (x::xs) a = if x < a then x::(ins xs a) else a::(x::xs); |
|
346 (*val ins = fn : int -> int list -> int list*) |
|
347 |
|
348 ins 3 [1,2,4]; |
|
349 |
|
350 fun sort xs = Foldl ins0 xs []; |
|
351 (*operator domain: int -> int list -> int |
|
352 operand: int -> int list -> int list |
|
353 in expression: |
|
354 Foldl ins |
|
355 *) |
|
356 fun sort xs = Foldl ins xs []; |
|
357 |
|
358 |
|
359 |
|
360 (*--- 17.6.00 ---*) |
|
361 |
|
362 |
|
363 fun foldr f [] a = a |
|
364 | foldr f (x::xs) a = foldr f xs (f a x); |
|
365 (*val fold = fn : ('a -> 'b -> 'a) -> 'b list -> 'a -> 'a*) |
|
366 |
|
367 fun add a b = a+b:int; |
|
368 |
|
369 fold add [1,2,3] 0; |
|
370 |
|
371 fun ins [] a = [a] |
|
372 | ins (x::xs) a = if x < a then x::(ins xs a) else a::(x::xs); |
|
373 (*val ins = fn : int list -> int -> int list*) |
|
374 |
|
375 ins [1,2,4] 3; |
|
376 |
|
377 fun sort xs = foldr ins xs []; |
|
378 |
|
379 sort [3,1,4,2]; |
|
380 |
|
381 |
|
382 |
|
383 (*--- 17.6.00 II ---*) |
|
384 |
|
385 fun foldl f a [] = a |
|
386 | foldl f a (x::xs) = foldl f (f a x) xs; |
|
387 |
|
388 fun ins [] a = [a] |
|
389 | ins (x::xs) a = if x < a then x::(ins xs a) else a::(x::xs); |
|
390 |
|
391 fun sort xs = foldl ins xs []; |
|
392 |
|
393 sort [3,1,4,2]; |
|
394 (*val it = [3,1,4,2] : int list !?!?!?!?!?!?!?!?!?!?!?!?!?!?!?*) |
|
395 (*------------------------- nipkow ----------------------*) |
|