426 |
440 |
427 lemma prime_lemma [simp]: |
441 lemma prime_lemma [simp]: |
428 "rec_eval rec_prime [x] = (if prime x then 1 else 0)" |
442 "rec_eval rec_prime [x] = (if prime x then 1 else 0)" |
429 by (simp add: rec_prime_def Let_def prime_alt_def) |
443 by (simp add: rec_prime_def Let_def prime_alt_def) |
430 |
444 |
|
445 definition |
|
446 "rec_minr2 f = rec_sigma2 (rec_accum2 (CN rec_not [f]))" |
|
447 |
|
448 fun Minr2 :: "(nat list \<Rightarrow> bool) \<Rightarrow> nat list \<Rightarrow> nat" |
|
449 where "Minr2 R (x # ys) = Min ({z | z. z \<le> x \<and> R (z # ys)} \<union> {Suc x})" |
|
450 |
|
451 lemma minr_lemma [simp]: |
|
452 shows "rec_eval (rec_minr2 f) [x, y1, y2] = Minr2 (\<lambda>xs. (0 < rec_eval f xs)) [x, y1, y2]" |
|
453 apply(simp only: rec_minr2_def) |
|
454 apply(simp) |
|
455 apply(rule sym) |
|
456 apply(rule Min_eqI) |
|
457 apply(auto)[1] |
|
458 apply(simp) |
|
459 apply(erule disjE) |
|
460 apply(simp) |
|
461 apply(rule setsum_one_le) |
|
462 apply(auto)[1] |
|
463 apply(rule setprod_one_le) |
|
464 apply(auto)[1] |
|
465 apply(subst setsum_cut_off_le) |
|
466 apply(auto)[2] |
|
467 apply(rule setsum_one_less) |
|
468 apply(auto)[1] |
|
469 apply(rule setprod_one_le) |
|
470 apply(auto)[1] |
|
471 apply(simp) |
|
472 thm setsum_eq_one_le |
|
473 apply(subgoal_tac "(\<forall>z\<le>x. (\<Prod>z\<le>z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)) \<or> |
|
474 (\<not> (\<forall>z\<le>x. (\<Prod>z\<le>z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)))") |
|
475 prefer 2 |
|
476 apply(auto)[1] |
|
477 apply(erule disjE) |
|
478 apply(rule disjI1) |
|
479 apply(rule setsum_eq_one_le) |
|
480 apply(simp) |
|
481 apply(rule disjI2) |
|
482 apply(simp) |
|
483 apply(clarify) |
|
484 apply(subgoal_tac "\<exists>l. l = (LEAST z. 0 < rec_eval f [z, y1, y2])") |
|
485 defer |
|
486 apply metis |
|
487 apply(erule exE) |
|
488 apply(subgoal_tac "l \<le> x") |
|
489 defer |
|
490 apply (metis not_leE not_less_Least order_trans) |
|
491 apply(subst setsum_least_eq) |
|
492 apply(rotate_tac 4) |
|
493 apply(assumption) |
|
494 apply(auto)[1] |
|
495 apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])") |
|
496 prefer 2 |
|
497 apply(auto)[1] |
|
498 apply(rotate_tac 5) |
|
499 apply(drule not_less_Least) |
|
500 apply(auto)[1] |
|
501 apply(auto) |
|
502 apply(rule_tac x="(LEAST z. 0 < rec_eval f [z, y1, y2])" in exI) |
|
503 apply(simp) |
|
504 apply (metis LeastI_ex) |
|
505 apply(subst setsum_least_eq) |
|
506 apply(rotate_tac 3) |
|
507 apply(assumption) |
|
508 apply(simp) |
|
509 apply(auto)[1] |
|
510 apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])") |
|
511 prefer 2 |
|
512 apply(auto)[1] |
|
513 apply (metis neq0_conv not_less_Least) |
|
514 apply(auto)[1] |
|
515 apply (metis (mono_tags) LeastI_ex) |
|
516 by (metis LeastI_ex) |
|
517 |
|
518 definition quo :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
|
519 where |
|
520 "quo x y = (if y = 0 then 0 else x div y)" |
|
521 |
|
522 |
|
523 definition |
|
524 "rec_quo = CN rec_mult [CN rec_sign [id 2 1], |
|
525 CN (rec_minr2 (CN rec_less [id 3 1, CN rec_mult [CN s [id 3 0], id 3 2]])) |
|
526 [id 2 0, id 2 0, id 2 1]]" |
|
527 |
|
528 lemma div_lemma [simp]: |
|
529 "rec_eval rec_quo [x, y] = quo x y" |
|
530 apply(simp add: rec_quo_def quo_def) |
|
531 apply(rule impI) |
|
532 apply(rule Min_eqI) |
|
533 apply(auto)[1] |
|
534 apply(simp) |
|
535 apply(erule disjE) |
|
536 apply(simp) |
|
537 apply(auto)[1] |
|
538 apply (metis div_le_dividend le_SucI) |
|
539 defer |
|
540 apply(simp) |
|
541 apply(auto)[1] |
|
542 apply (metis mult_Suc_right nat_mult_commute split_div_lemma) |
|
543 apply(auto)[1] |
|
544 |
|
545 apply (smt div_le_dividend fst_divmod_nat) |
|
546 apply(simp add: quo_def) |
|
547 apply(auto)[1] |
|
548 |
|
549 apply(auto) |
431 |
550 |
432 fun Minr :: "(nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
551 fun Minr :: "(nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
433 where "Minr R x y = (let setx = {z | z. z \<le> x \<and> R [z, y]} in |
552 where "Minr R x y = (let setx = {z | z. z \<le> x \<and> R [z, y]} in |
434 if (setx = {}) then (Suc x) else (Min setx))" |
553 if (setx = {}) then (Suc x) else (Min setx))" |
435 |
554 |
436 definition |
555 definition |
437 "rec_minr f = rec_sigma (rec_accum (CN rec_not [f]))" |
556 "rec_minr f = rec_sigma1 (rec_accum1 (CN rec_not [f]))" |
438 |
557 |
439 lemma minr_lemma [simp]: |
558 lemma minr_lemma [simp]: |
440 shows "rec_eval (rec_minr f) [x, y] = Minr (\<lambda>xs. (0 < rec_eval f xs)) x y" |
559 shows "rec_eval (rec_minr f) [x, y] = Minr (\<lambda>xs. (0 < rec_eval f xs)) x y" |
441 apply(simp only: rec_minr_def) |
560 apply(simp only: rec_minr_def) |
442 apply(simp only: sigma_lemma) |
561 apply(simp only: sigma1_lemma) |
443 apply(simp only: accum_lemma) |
562 apply(simp only: accum1_lemma) |
444 apply(subst rec_eval.simps) |
563 apply(subst rec_eval.simps) |
445 apply(simp only: map.simps nth) |
564 apply(simp only: map.simps nth) |
446 apply(simp only: Minr.simps Let_def) |
565 apply(simp only: Minr.simps Let_def) |
447 apply(auto simp del: not_lemma) |
566 apply(auto simp del: not_lemma) |
448 apply(simp) |
567 apply(simp) |
493 apply(drule not_less_Least) |
612 apply(drule not_less_Least) |
494 apply(auto)[1] |
613 apply(auto)[1] |
495 apply(auto) |
614 apply(auto) |
496 by (metis (mono_tags) LeastI_ex) |
615 by (metis (mono_tags) LeastI_ex) |
497 |
616 |
498 (* |
617 |
499 lemma prime_alt_iff: |
618 fun Minr2 :: "(nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
500 fixes x::nat |
619 where "Minr2 R x y = (let setx = {z | z. z \<le> x \<and> R [z, y]} in |
501 shows "prime x \<longleftrightarrow> 1 < x \<and> (\<forall>u < x. \<forall>v < x. x \<noteq> u * v)" |
620 Min (setx \<union> {Suc x}))" |
502 unfolding prime_nat_simp dvd_def |
621 |
|
622 lemma Minr2_Minr: |
|
623 "Minr2 R x y = Minr R x y" |
503 apply(auto) |
624 apply(auto) |
504 by (smt n_less_m_mult_n nat_mult_commute) |
625 apply (metis (lifting, no_types) Min_singleton empty_Collect_eq) |
505 |
626 apply(rule min_absorb2) |
506 lemma prime_alt2_iff: |
627 apply(subst Min_le_iff) |
507 fixes x::nat |
628 apply(auto) |
508 shows "prime x \<longleftrightarrow> 1 < x \<and> (\<forall>u \<le> x - 1. \<forall>v \<le> x - 1. x \<noteq> u * v)" |
|
509 unfolding prime_alt_iff |
|
510 sorry |
|
511 *) |
|
512 |
|
513 definition |
|
514 "rec_prime = CN rec_conj |
|
515 [CN rec_less [constn 1, id 1 0], |
|
516 CN (rec_all (CN (rec_all2 (CN rec_noteq [id 3 2, CN rec_mult [id 3 1, id 3 0]])) |
|
517 [CN rec_pred [id 2 1], id 2 0, id 2 1])) |
|
518 [CN rec_pred [id 1 0], id 1 0]]" |
|
519 |
|
520 lemma prime_lemma [simp]: |
|
521 "rec_eval rec_prime [x] = (if prime x then 1 else 0)" |
|
522 apply(rule trans) |
|
523 apply(simp add: rec_prime_def) |
|
524 apply(simp only: prime_nat_def dvd_def) |
|
525 apply(auto) |
|
526 apply(drule_tac x="m" in spec) |
|
527 apply(auto) |
|
528 apply(case_tac m) |
|
529 apply(auto) |
|
530 apply(case_tac nat) |
|
531 apply(auto) |
|
532 apply(case_tac k) |
|
533 apply(auto) |
|
534 apply(case_tac nat) |
|
535 apply(auto) |
|
536 done |
629 done |
537 |
630 |
538 lemma if_zero [simp]: |
|
539 "(0::nat) < (if P then 1 else 0) = P" |
|
540 by (simp) |
|
541 |
|
542 lemma if_cong: |
|
543 "P = Q \<Longrightarrow> (if P then 1 else (0::nat)) = (if Q then 1 else 0)" |
|
544 by simp |
|
545 |
|
546 |
|
547 |
|
548 |
|
549 end |
631 end |