228 |
228 |
229 definition |
229 definition |
230 "rec_mult = PR Z (CN rec_add [Id 3 1, Id 3 2])" |
230 "rec_mult = PR Z (CN rec_add [Id 3 1, Id 3 2])" |
231 |
231 |
232 definition |
232 definition |
233 "rec_power_swap = PR (constn 1) (CN rec_mult [Id 3 1, Id 3 2])" |
233 "rec_power = rec_swap (PR (constn 1) (CN rec_mult [Id 3 1, Id 3 2]))" |
234 |
|
235 definition |
|
236 "rec_power = rec_swap rec_power_swap" |
|
237 |
234 |
238 definition |
235 definition |
239 "rec_fact = PR (constn 1) (CN rec_mult [CN S [Id 3 0], Id 3 1])" |
236 "rec_fact = PR (constn 1) (CN rec_mult [CN S [Id 3 0], Id 3 1])" |
240 |
237 |
241 definition |
238 definition |
242 "rec_pred = CN (PR Z (Id 3 0)) [Id 1 0, Id 1 0]" |
239 "rec_pred = CN (PR Z (Id 3 0)) [Id 1 0, Id 1 0]" |
243 |
240 |
244 definition |
241 definition |
245 "rec_minus_swap = (PR (Id 1 0) (CN rec_pred [Id 3 1]))" |
242 "rec_minus = rec_swap (PR (Id 1 0) (CN rec_pred [Id 3 1]))" |
246 |
243 |
247 definition |
|
248 "rec_minus = rec_swap rec_minus_swap" |
|
249 |
244 |
250 text {* Sign function returning 1 when the input argument is greater than @{text "0"}. *} |
245 text {* Sign function returning 1 when the input argument is greater than @{text "0"}. *} |
251 |
246 |
252 definition |
247 definition |
253 "rec_sign = CN rec_minus [constn 1, CN rec_minus [constn 1, Id 1 0]]" |
248 "rec_sign = CN rec_minus [constn 1, CN rec_minus [constn 1, Id 1 0]]" |
257 |
252 |
258 text {* |
253 text {* |
259 @{text "rec_eq"} compares two arguments: returns @{text "1"} |
254 @{text "rec_eq"} compares two arguments: returns @{text "1"} |
260 if they are equal; @{text "0"} otherwise. *} |
255 if they are equal; @{text "0"} otherwise. *} |
261 definition |
256 definition |
262 "rec_eq = CN rec_minus |
257 "rec_eq = CN rec_minus [constn 1, CN rec_add [rec_minus, rec_swap rec_minus]]" |
263 [CN (constn 1) [Id 2 0], |
|
264 CN rec_add [rec_minus, rec_swap rec_minus]]" |
|
265 |
258 |
266 definition |
259 definition |
267 "rec_noteq = CN rec_not [rec_eq]" |
260 "rec_noteq = CN rec_not [rec_eq]" |
268 |
261 |
269 definition |
262 definition |
275 definition |
268 definition |
276 "rec_imp = CN rec_disj [CN rec_not [Id 2 0], Id 2 1]" |
269 "rec_imp = CN rec_disj [CN rec_not [Id 2 0], Id 2 1]" |
277 |
270 |
278 text {* @{term "rec_ifz [z, x, y]"} returns x if z is zero, |
271 text {* @{term "rec_ifz [z, x, y]"} returns x if z is zero, |
279 y otherwise *} |
272 y otherwise *} |
|
273 |
280 definition |
274 definition |
281 "rec_ifz = PR (Id 2 0) (Id 4 3)" |
275 "rec_ifz = PR (Id 2 0) (Id 4 3)" |
282 |
276 |
283 text {* @{term "rec_if [z, x, y]"} returns x if z is *not* zero, |
277 text {* @{term "rec_if [z, x, y]"} returns x if z is *not* zero, |
284 y otherwise *} |
278 y otherwise *} |
324 "rec_ex2 f = CN rec_sign [rec_sigma2 f]" |
318 "rec_ex2 f = CN rec_sign [rec_sigma2 f]" |
325 |
319 |
326 text {* Dvd, Quotient, Reminder *} |
320 text {* Dvd, Quotient, Reminder *} |
327 |
321 |
328 definition |
322 definition |
329 "rec_dvd_swap = CN (rec_ex2 (CN rec_eq [Id 3 2, CN rec_mult [Id 3 1, Id 3 0]])) [Id 2 0, Id 2 1, Id 2 0]" |
323 "rec_dvd = |
330 |
324 rec_swap (CN (rec_ex2 (CN rec_eq [Id 3 2, CN rec_mult [Id 3 1, Id 3 0]])) [Id 2 0, Id 2 1, Id 2 0])" |
331 definition |
|
332 "rec_dvd = rec_swap rec_dvd_swap" |
|
333 |
325 |
334 definition |
326 definition |
335 "rec_quo = (let lhs = CN S [Id 3 0] in |
327 "rec_quo = (let lhs = CN S [Id 3 0] in |
336 let rhs = CN rec_mult [Id 3 2, CN S [Id 3 1]] in |
328 let rhs = CN rec_mult [Id 3 2, CN S [Id 3 1]] in |
337 let cond = CN rec_eq [lhs, rhs] in |
329 let cond = CN rec_eq [lhs, rhs] in |
357 |
349 |
358 lemma mult_lemma [simp]: |
350 lemma mult_lemma [simp]: |
359 "rec_eval rec_mult [x, y] = x * y" |
351 "rec_eval rec_mult [x, y] = x * y" |
360 by (induct x) (simp_all add: rec_mult_def) |
352 by (induct x) (simp_all add: rec_mult_def) |
361 |
353 |
362 lemma power_swap_lemma [simp]: |
|
363 "rec_eval rec_power_swap [y, x] = x ^ y" |
|
364 by (induct y) (simp_all add: rec_power_swap_def) |
|
365 |
|
366 lemma power_lemma [simp]: |
354 lemma power_lemma [simp]: |
367 "rec_eval rec_power [x, y] = x ^ y" |
355 "rec_eval rec_power [x, y] = x ^ y" |
368 by (simp add: rec_power_def) |
356 by (induct y) (simp_all add: rec_power_def) |
369 |
357 |
370 lemma fact_lemma [simp]: |
358 lemma fact_lemma [simp]: |
371 "rec_eval rec_fact [x] = fact x" |
359 "rec_eval rec_fact [x] = fact x" |
372 by (induct x) (simp_all add: rec_fact_def) |
360 by (induct x) (simp_all add: rec_fact_def) |
373 |
361 |
374 lemma pred_lemma [simp]: |
362 lemma pred_lemma [simp]: |
375 "rec_eval rec_pred [x] = x - 1" |
363 "rec_eval rec_pred [x] = x - 1" |
376 by (induct x) (simp_all add: rec_pred_def) |
364 by (induct x) (simp_all add: rec_pred_def) |
377 |
365 |
378 lemma minus_swap_lemma [simp]: |
|
379 "rec_eval rec_minus_swap [x, y] = y - x" |
|
380 by (induct x) (simp_all add: rec_minus_swap_def) |
|
381 |
|
382 lemma minus_lemma [simp]: |
366 lemma minus_lemma [simp]: |
383 "rec_eval rec_minus [x, y] = x - y" |
367 "rec_eval rec_minus [x, y] = x - y" |
384 by (simp add: rec_minus_def) |
368 by (induct y) (simp_all add: rec_minus_def) |
385 |
369 |
386 lemma sign_lemma [simp]: |
370 lemma sign_lemma [simp]: |
387 "rec_eval rec_sign [x] = (if x = 0 then 0 else 1)" |
371 "rec_eval rec_sign [x] = (if x = 0 then 0 else 1)" |
388 by (simp add: rec_sign_def) |
372 by (simp add: rec_sign_def) |
389 |
373 |
466 apply(auto simp add: dvd_def) |
450 apply(auto simp add: dvd_def) |
467 apply(case_tac x) |
451 apply(case_tac x) |
468 apply(auto) |
452 apply(auto) |
469 done |
453 done |
470 |
454 |
471 lemma dvd_swap_lemma [simp]: |
|
472 "rec_eval rec_dvd_swap [x, y] = (if y dvd x then 1 else 0)" |
|
473 unfolding dvd_alt_def |
|
474 by (auto simp add: rec_dvd_swap_def) |
|
475 |
|
476 lemma dvd_lemma [simp]: |
455 lemma dvd_lemma [simp]: |
477 "rec_eval rec_dvd [x, y] = (if x dvd y then 1 else 0)" |
456 "rec_eval rec_dvd [x, y] = (if x dvd y then 1 else 0)" |
478 by (simp add: rec_dvd_def) |
457 unfolding dvd_alt_def |
479 |
458 by (auto simp add: rec_dvd_def) |
480 |
459 |
481 fun Quo where |
460 fun Quo where |
482 "Quo x 0 = 0" |
461 "Quo x 0 = 0" |
483 | "Quo x (Suc y) = (if (Suc y = x * (Suc (Quo x y))) then Suc (Quo x y) else Quo x y)" |
462 | "Quo x (Suc y) = (if (Suc y = x * (Suc (Quo x y))) then Suc (Quo x y) else Quo x y)" |
484 |
463 |