308 "rec_accum1 f = PR (CN f [Z, Id 1 0]) (CN rec_mult [Id 3 1, CN f [S, Id 3 2]])" |
308 "rec_accum1 f = PR (CN f [Z, Id 1 0]) (CN rec_mult [Id 3 1, CN f [S, Id 3 2]])" |
309 |
309 |
310 definition |
310 definition |
311 "rec_accum2 f = PR (CN f [Z, Id 2 0, Id 2 1]) (CN rec_mult [Id 4 1, CN f [S, Id 4 2, Id 4 3]])" |
311 "rec_accum2 f = PR (CN f [Z, Id 2 0, Id 2 1]) (CN rec_mult [Id 4 1, CN f [S, Id 4 2, Id 4 3]])" |
312 |
312 |
|
313 definition |
|
314 "rec_accum3 f = PR (CN f [Z, Id 3 0, Id 3 1, Id 3 2]) |
|
315 (CN rec_mult [Id 5 1, CN f [S, Id 5 2, Id 5 3, Id 5 4]])" |
|
316 |
|
317 |
313 text {* Bounded quantifiers for one and two arguments *} |
318 text {* Bounded quantifiers for one and two arguments *} |
314 |
319 |
315 definition |
320 definition |
316 "rec_all1 f = CN rec_sign [rec_accum1 f]" |
321 "rec_all1 f = CN rec_sign [rec_accum1 f]" |
317 |
322 |
318 definition |
323 definition |
319 "rec_all2 f = CN rec_sign [rec_accum2 f]" |
324 "rec_all2 f = CN rec_sign [rec_accum2 f]" |
|
325 |
|
326 definition |
|
327 "rec_all3 f = CN rec_sign [rec_accum3 f]" |
|
328 |
|
329 definition |
|
330 "rec_all1_less f = (let f' = CN rec_disj [CN rec_eq [Id 3 0, Id 3 1], CN f [Id 3 0, Id 3 2]] |
|
331 in CN (rec_all2 f') [Id 2 0, Id 2 0, Id 2 1])" |
|
332 |
|
333 definition |
|
334 "rec_all2_less f = (let f' = CN rec_disj [CN rec_eq [Id 4 0, Id 4 1], CN f [Id 4 0, Id 4 2, Id 4 3]] |
|
335 in CN (rec_all3 f') [Id 3 0, Id 3 0, Id 3 1, Id 3 2])" |
320 |
336 |
321 definition |
337 definition |
322 "rec_ex1 f = CN rec_sign [rec_sigma1 f]" |
338 "rec_ex1 f = CN rec_sign [rec_sigma1 f]" |
323 |
339 |
324 definition |
340 definition |
450 |
466 |
451 lemma accum2_lemma [simp]: |
467 lemma accum2_lemma [simp]: |
452 shows "rec_eval (rec_accum2 f) [x, y1, y2] = (\<Prod> z \<le> x. (rec_eval f) [z, y1, y2])" |
468 shows "rec_eval (rec_accum2 f) [x, y1, y2] = (\<Prod> z \<le> x. (rec_eval f) [z, y1, y2])" |
453 by (induct x) (simp_all add: rec_accum2_def) |
469 by (induct x) (simp_all add: rec_accum2_def) |
454 |
470 |
|
471 lemma accum3_lemma [simp]: |
|
472 shows "rec_eval (rec_accum3 f) [x, y1, y2, y3] = (\<Prod> z \<le> x. (rec_eval f) [z, y1, y2, y3])" |
|
473 by (induct x) (simp_all add: rec_accum3_def) |
|
474 |
455 lemma ex1_lemma [simp]: |
475 lemma ex1_lemma [simp]: |
456 "rec_eval (rec_ex1 f) [x, y] = (if (\<exists>z \<le> x. 0 < rec_eval f [z, y]) then 1 else 0)" |
476 "rec_eval (rec_ex1 f) [x, y] = (if (\<exists>z \<le> x. 0 < rec_eval f [z, y]) then 1 else 0)" |
457 by (simp add: rec_ex1_def) |
477 by (simp add: rec_ex1_def) |
458 |
478 |
459 lemma ex2_lemma [simp]: |
479 lemma ex2_lemma [simp]: |
465 by (simp add: rec_all1_def) |
485 by (simp add: rec_all1_def) |
466 |
486 |
467 lemma all2_lemma [simp]: |
487 lemma all2_lemma [simp]: |
468 "rec_eval (rec_all2 f) [x, y1, y2] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)" |
488 "rec_eval (rec_all2 f) [x, y1, y2] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)" |
469 by (simp add: rec_all2_def) |
489 by (simp add: rec_all2_def) |
|
490 |
|
491 lemma all3_lemma [simp]: |
|
492 "rec_eval (rec_all3 f) [x, y1, y2, y3] = (if (\<forall>z \<le> x. 0 < rec_eval f [z, y1, y2, y3]) then 1 else 0)" |
|
493 by (simp add: rec_all3_def) |
|
494 |
|
495 lemma all1_less_lemma [simp]: |
|
496 "rec_eval (rec_all1_less f) [x, y] = (if (\<forall>z < x. 0 < rec_eval f [z, y]) then 1 else 0)" |
|
497 apply(auto simp add: Let_def rec_all1_less_def) |
|
498 apply (metis nat_less_le)+ |
|
499 done |
|
500 |
|
501 lemma all2_less_lemma [simp]: |
|
502 "rec_eval (rec_all2_less f) [x, y1, y2] = (if (\<forall>z < x. 0 < rec_eval f [z, y1, y2]) then 1 else 0)" |
|
503 apply(auto simp add: Let_def rec_all2_less_def) |
|
504 apply(metis nat_less_le)+ |
|
505 done |
470 |
506 |
471 |
507 |
472 lemma dvd_alt_def: |
508 lemma dvd_alt_def: |
473 fixes x y k:: nat |
509 fixes x y k:: nat |
474 shows "(x dvd y) = (\<exists> k \<le> y. y = x * k)" |
510 shows "(x dvd y) = (\<exists> k \<le> y. y = x * k)" |