535 |
538 |
536 lemma prime_lemma [simp]: |
539 lemma prime_lemma [simp]: |
537 "rec_eval rec_prime [x] = (if prime x then 1 else 0)" |
540 "rec_eval rec_prime [x] = (if prime x then 1 else 0)" |
538 by (auto simp add: rec_prime_def Let_def prime_alt_def) |
541 by (auto simp add: rec_prime_def Let_def prime_alt_def) |
539 |
542 |
540 section {* Bounded Min and Maximisation *} |
543 section {* Bounded Maximisation *} |
541 |
544 |
542 fun BMax_rec where |
545 fun BMax_rec where |
543 "BMax_rec R 0 = 0" |
546 "BMax_rec R 0 = 0" |
544 | "BMax_rec R (Suc n) = (if R (Suc n) then (Suc n) else BMax_rec R n)" |
547 | "BMax_rec R (Suc n) = (if R (Suc n) then (Suc n) else BMax_rec R n)" |
545 |
548 |
546 definition BMax_set :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat" |
549 definition BMax_set :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat" |
547 where "BMax_set R x = Max ({z | z. z \<le> x \<and> R z} \<union> {0})" |
550 where "BMax_set R x = Max ({z. z \<le> x \<and> R z} \<union> {0})" |
548 |
551 |
549 definition (in ord) |
552 definition (in ord) |
550 Great :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "GREAT " 10) where |
553 Great :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "GREAT " 10) where |
551 "Great P = (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> y \<le> x))" |
554 "Great P = (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> y \<le> x))" |
552 |
555 |
553 lemma Great_equality: |
556 lemma Great_equality: |
554 fixes x::nat |
557 fixes x::nat |
555 assumes "P x" "\<And>y. P y \<Longrightarrow> y \<le> x" |
558 assumes "P x" "\<And>y. P y \<Longrightarrow> y \<le> x" |
556 shows "Great P = x" |
559 shows "Great P = x" |
557 unfolding Great_def |
560 unfolding Great_def |
558 using assms |
561 using assms by(rule_tac the_equality) (auto intro: le_antisym) |
559 by(rule_tac the_equality) (auto intro: le_antisym) |
|
560 |
562 |
561 lemma BMax_rec_eq1: |
563 lemma BMax_rec_eq1: |
562 "BMax_rec R x = (GREAT z. (R z \<and> z \<le> x) \<or> z = 0)" |
564 "BMax_rec R x = (GREAT z. (R z \<and> z \<le> x) \<or> z = 0)" |
563 apply(induct x) |
565 apply(induct x) |
564 apply(auto intro: Great_equality Great_equality[symmetric]) |
566 apply(auto intro: Great_equality Great_equality[symmetric]) |
565 apply(simp add: le_Suc_eq) |
567 apply(simp add: le_Suc_eq) |
566 by metis |
568 by metis |
567 |
569 |
568 lemma BMax_rec_eq2: |
570 lemma BMax_rec_eq2: |
569 "BMax_rec R x = Max ({z | z. z \<le> x \<and> R z} \<union> {0})" |
571 "BMax_rec R x = Max ({z. z \<le> x \<and> R z} \<union> {0})" |
570 apply(induct x) |
572 apply(induct x) |
571 apply(auto intro: Max_eqI Max_eqI[symmetric]) |
573 apply(auto intro: Max_eqI Max_eqI[symmetric]) |
572 apply(simp add: le_Suc_eq) |
574 apply(simp add: le_Suc_eq) |
573 by metis |
575 by metis |
574 |
576 |
575 definition |
577 definition |
576 "rec_max1 f = PR (constn 0) |
578 "rec_max1 f = PR (constn 0) (CN rec_ifz [CN f [CN S [Id 3 0], Id 3 2], CN S [Id 4 0], Id 4 1])" |
577 (CN rec_ifz [CN f [CN S [Id 3 0], Id 3 2], CN S [Id 4 0], Id 4 1])" |
|
578 |
579 |
579 lemma max1_lemma [simp]: |
580 lemma max1_lemma [simp]: |
580 "rec_eval (rec_max1 f) [x, y] = BMax_rec (\<lambda>u. rec_eval f [u, y] = 0) x" |
581 "rec_eval (rec_max1 f) [x, y] = BMax_rec (\<lambda>u. rec_eval f [u, y] = 0) x" |
581 by (induct x) (simp_all add: rec_max1_def) |
582 by (induct x) (simp_all add: rec_max1_def) |
582 |
583 |
583 definition |
584 definition |
584 "rec_max2 f = PR (constn 0) |
585 "rec_max2 f = PR (constn 0) (CN rec_ifz [CN f [CN S [Id 4 0], Id 4 2, Id 4 3], CN S [Id 4 0], Id 4 1])" |
585 (CN rec_ifz [CN f [CN S [Id 4 0], Id 4 2, Id 4 3], CN S [Id 4 0], Id 4 1])" |
|
586 |
586 |
587 lemma max2_lemma [simp]: |
587 lemma max2_lemma [simp]: |
588 "rec_eval (rec_max2 f) [x, y1, y2] = BMax_rec (\<lambda>u. rec_eval f [u, y1, y2] = 0) x" |
588 "rec_eval (rec_max2 f) [x, y1, y2] = BMax_rec (\<lambda>u. rec_eval f [u, y1, y2] = 0) x" |
589 by (induct x) (simp_all add: rec_max2_def) |
589 by (induct x) (simp_all add: rec_max2_def) |
590 |
590 |
|
591 section {* Encodings *} |
|
592 |
|
593 fun log :: "nat \<Rightarrow> nat" where |
|
594 [simp del]: "log n = (if n < 2 then 0 else Suc (log (n div 2)))" |
|
595 |
|
596 lemma log_zero [simp]: |
|
597 "log 0 = 0" |
|
598 by (simp add: log.simps) |
|
599 |
|
600 lemma log_one [simp]: |
|
601 "log 1 = 0" |
|
602 by (simp add: log.simps) |
|
603 |
|
604 lemma log_suc [simp]: |
|
605 "log (Suc 0) = 0" |
|
606 by (simp add: log.simps) |
|
607 |
|
608 lemma log_rec: |
|
609 "n \<ge> 2 \<Longrightarrow> log n = Suc (log (n div 2))" |
|
610 by (simp add: log.simps) |
|
611 |
|
612 lemma log_twice [simp]: |
|
613 "n \<noteq> 0 \<Longrightarrow> log (2 * n) = Suc (log n)" |
|
614 by (simp add: log_rec) |
|
615 |
|
616 lemma log_half [simp]: |
|
617 "log (n div 2) = log n - 1" |
|
618 proof (cases "n < 2") |
|
619 case True |
|
620 then have "n = 0 \<or> n = 1" by arith |
|
621 then show ?thesis by (auto simp del: One_nat_def) |
|
622 next |
|
623 case False then show ?thesis by (simp add: log_rec) |
|
624 qed |
|
625 |
|
626 lemma log_exp [simp]: |
|
627 "log (2 ^ n) = n" |
|
628 by (induct n) simp_all |
|
629 |
|
630 fun divby2 :: "nat \<Rightarrow> nat" where |
|
631 [simp del]: "divby2 n = (if n = 0 then 0 |
|
632 else if even n then divby2 (n div 2) else n)" |
|
633 |
|
634 lemma divby2[simp]: |
|
635 "divby2 0 = 0" |
|
636 "odd n \<Longrightarrow> divby2 n = n" |
|
637 "even n \<Longrightarrow> divby2 n = divby2 (n div 2)" |
|
638 apply(simp_all add: divby2.simps) |
|
639 done |
|
640 |
|
641 lemma divby2_odd: |
|
642 "divby2 n = 0 \<or> odd (divby2 n)" |
|
643 apply(induct n rule: nat_less_induct) |
|
644 apply(case_tac "n = 0") |
|
645 apply(simp) |
|
646 apply(case_tac "odd n") |
|
647 apply(auto) |
|
648 done |
|
649 |
|
650 lemma bigger: "divby2 (Suc n) > 0" |
|
651 apply(induct n rule: nat_less_induct) |
|
652 apply(case_tac "n = 0") |
|
653 apply(simp) |
|
654 apply(case_tac "odd n") |
|
655 apply(auto) |
|
656 apply(drule_tac x="n div 2" in spec) |
|
657 apply(drule mp) |
|
658 apply(auto) |
|
659 by (smt numeral_2_eq_2 odd_nat_plus_one_div_two) |
|
660 |
|
661 fun pencode :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
|
662 "pencode m n = (2 ^ m) * ((2 * n) + 1) - 1" |
|
663 |
|
664 fun pdecode2 :: "nat \<Rightarrow> nat" where |
|
665 "pdecode2 z = (divby2 (Suc z) - 1) div 2" |
|
666 |
|
667 fun pdecode1 :: "nat \<Rightarrow> nat" where |
|
668 "pdecode1 z = log ((Suc z) div (divby2 (Suc z)))" |
|
669 |
|
670 lemma k: |
|
671 "odd n \<Longrightarrow> divby2 (2 ^ m * n) = n" |
|
672 apply(induct m) |
|
673 apply(simp_all) |
|
674 done |
|
675 |
|
676 lemma ww: "\<exists>k. n = 2 ^ k * divby2 n" |
|
677 apply(induct n rule: nat_less_induct) |
|
678 apply(case_tac "n=0") |
|
679 apply(simp) |
|
680 apply(case_tac "odd n") |
|
681 apply(simp) |
|
682 apply(rule_tac x="0" in exI) |
|
683 apply(simp) |
|
684 apply(simp) |
|
685 apply(drule_tac x="n div 2" in spec) |
|
686 apply(erule impE) |
|
687 apply(simp) |
|
688 apply(erule exE) |
|
689 apply(rule_tac x="Suc k" in exI) |
|
690 apply(simp) |
|
691 by (metis div_mult_self2_is_id even_mult_two_ex nat_mult_assoc nat_mult_commute zero_neq_numeral) |
|
692 |
|
693 |
|
694 |
|
695 lemma t: |
|
696 "(Suc (Suc m)) div 2 = Suc (m div 2)" |
|
697 by (induct m) (auto) |
|
698 |
|
699 lemma u: |
|
700 "((Suc (Suc m)) mod 2 = 0) <-> m mod 2 = 0" |
|
701 by (auto) |
|
702 |
|
703 lemma u2: |
|
704 "0 < n ==> 2 * 2 ^ (n - 1) = (2::nat) ^ (n::nat)" |
|
705 by (induct n) (simp_all) |
|
706 |
|
707 lemma test: "x = y \<Longrightarrow> 2 * x = 2 * y" |
|
708 by simp |
|
709 |
|
710 lemma m: "0 < n ==> 2 ^ log (n div (divby2 n)) = n div (divby2 n)" |
|
711 apply(induct n rule: nat_less_induct) |
|
712 apply(case_tac "n=0") |
|
713 apply(simp) |
|
714 apply(case_tac "odd n") |
|
715 apply(simp) |
|
716 apply(drule_tac x="n div 2" in spec) |
|
717 apply(drule mp) |
|
718 apply(auto)[1] |
|
719 apply(drule mp) |
|
720 apply (metis One_nat_def Suc_lessI div_2_gt_zero odd_1_nat) |
|
721 apply(subst (asm) divby2(3)[symmetric]) |
|
722 apply(simp) |
|
723 apply(subst (asm) divby2(3)[symmetric]) |
|
724 apply(simp) |
|
725 apply(subgoal_tac "n div 2 div divby2 n = n div (divby2 n) div 2") |
|
726 prefer 2 |
|
727 apply (metis div_mult2_eq nat_mult_commute) |
|
728 apply(simp only: log_half) |
|
729 apply(case_tac "n div divby2 n = 0") |
|
730 apply(simp) |
|
731 apply(simp del: divby2) |
|
732 apply(drule test) |
|
733 apply(subst (asm) power.simps(2)[symmetric]) |
|
734 apply(subgoal_tac "Suc (log (n div divby2 n) - 1) = log (n div divby2 n)") |
|
735 prefer 2 |
|
736 apply (smt Recs.log.simps Suc_1 div_less div_mult_self1_is_id log_half log_zero numeral_1_eq_Suc_0 numeral_One odd_1_nat odd_nat_plus_one_div_two one_less_numeral_iff power_one_right semiring_norm(76)) |
|
737 apply(simp only:) |
|
738 apply(subst dvd_mult_div_cancel) |
|
739 apply (smt Suc_1 div_by_0 div_mult_self2_is_id divby2_odd dvd_power even_Suc even_numeral_nat even_product_nat nat_even_iff_2_dvd power_0 ww) |
|
740 apply(simp (no_asm)) |
|
741 done |
|
742 |
|
743 lemma m1: "n div divby2 n * divby2 n = n" |
|
744 apply(induct n rule: nat_less_induct) |
|
745 apply(case_tac "n=0") |
|
746 apply(simp) |
|
747 apply(case_tac "odd n") |
|
748 apply(simp) |
|
749 apply(simp) |
|
750 apply(drule_tac x="n div 2" in spec) |
|
751 apply(drule mp) |
|
752 apply(auto)[1] |
|
753 by (metis add_eq_if diff_add_inverse divby2(3) mod_eq_0_iff mult_div_cancel nat_mult_commute ww) |
|
754 |
|
755 |
|
756 lemma m2: "0 < n ==> 2 ^ log (n div (divby2 n)) * (divby2 n) = n" |
|
757 apply(subst m) |
|
758 apply(simp) |
|
759 apply(subst m1) |
|
760 apply(simp) |
|
761 done |
|
762 |
|
763 lemma y1: |
|
764 "pdecode2 (pencode m n) = n" |
|
765 apply(simp) |
|
766 apply(subst k) |
|
767 apply(auto) |
|
768 done |
|
769 |
|
770 lemma y2: |
|
771 "pdecode1 (pencode m n) = m" |
|
772 apply(simp) |
|
773 apply(subst k) |
|
774 apply(auto)[1] |
|
775 apply(simp) |
|
776 done |
|
777 |
|
778 lemma yy: |
|
779 "pencode (pdecode1 m) (pdecode2 m) = m" |
|
780 apply(induct m rule: nat_less_induct) |
|
781 apply(simp (no_asm)) |
|
782 apply(case_tac "n = 0") |
|
783 apply(simp) |
|
784 apply(subst dvd_mult_div_cancel) |
|
785 using divby2_odd |
|
786 apply - |
|
787 apply(drule_tac x="Suc n" in meta_spec) |
|
788 apply(erule disjE) |
|
789 apply(auto)[1] |
|
790 apply (metis even_num_iff nat_even_iff_2_dvd odd_pos) |
|
791 using bigger |
|
792 apply - |
|
793 apply(rotate_tac 3) |
|
794 apply(drule_tac x="n" in meta_spec) |
|
795 apply(simp del: pencode.simps pdecode2.simps pdecode1.simps) |
|
796 apply(subst m2) |
|
797 apply(simp) |
|
798 apply(simp) |
|
799 done |
|
800 |
|
801 fun penc where |
|
802 "penc (m, n) = pencode m n" |
|
803 |
|
804 fun pdec where |
|
805 "pdec m = (pdecode1 m, pdecode2 m)" |
|
806 |
|
807 lemma q1: "penc (pdec m) = m" |
|
808 apply(simp only: penc.simps pdec.simps) |
|
809 apply(rule yy) |
|
810 done |
|
811 |
|
812 lemma q2: "pdec (penc m) = m" |
|
813 apply(simp only: penc.simps pdec.simps) |
|
814 apply(case_tac m) |
|
815 apply(simp only: penc.simps pdec.simps) |
|
816 apply(subst y1) |
|
817 apply(subst y2) |
|
818 apply(simp) |
|
819 done |
|
820 |
|
821 lemma inj_penc: "inj_on penc A" |
|
822 apply(rule inj_on_inverseI) |
|
823 apply(rule q2) |
|
824 done |
|
825 |
|
826 lemma inj_pdec: "inj_on pdec A" |
|
827 apply(rule inj_on_inverseI) |
|
828 apply(rule q1) |
|
829 done |
|
830 |
|
831 lemma surj_penc: "surj penc" |
|
832 apply(rule surjI) |
|
833 apply(rule q1) |
|
834 done |
|
835 |
|
836 lemma surj_pdec: "surj pdec" |
|
837 apply(rule surjI) |
|
838 apply(rule q2) |
|
839 done |
|
840 |
|
841 lemma |
|
842 "bij pdec" |
|
843 by(simp add: bij_def surj_pdec inj_pdec) |
|
844 |
|
845 lemma |
|
846 "bij penc" |
|
847 by(simp add: bij_def surj_penc inj_penc) |
|
848 |
|
849 lemma "a \<le> penc (a, 0)" |
|
850 apply(induct a) |
|
851 apply(simp) |
|
852 apply(simp) |
|
853 by (smt nat_one_le_power) |
|
854 |
|
855 lemma "penc(a, 0) \<le> penc (a, b)" |
|
856 apply(simp) |
|
857 by (metis diff_le_mono le_add1 mult_2_right mult_le_mono1 nat_add_commute nat_mult_1 nat_mult_commute) |
|
858 |
|
859 lemma "b \<le> penc (a, b)" |
|
860 apply(simp) |
|
861 proof - |
|
862 have f1: "(1\<Colon>nat) + 1 = 2" |
|
863 by (metis mult_2 nat_mult_1_right) |
|
864 have f2: "\<And>x\<^isub>1 x\<^isub>2. (x\<^isub>1\<Colon>nat) \<le> x\<^isub>1 * x\<^isub>2 \<or> \<not> 1 \<le> x\<^isub>2" |
|
865 by (metis mult_le_mono2 nat_mult_1_right) |
|
866 have "1 + (b + b) \<le> 1 + b \<longrightarrow> b \<le> (1 + (b + b)) * (1 + 1) ^ a - 1" |
|
867 by (metis le_add1 le_trans nat_add_left_cancel_le) |
|
868 hence "(1 + (b + b)) * (1 + 1) ^ a \<le> 1 + b \<longrightarrow> b \<le> (1 + (b + b)) * (1 + 1) ^ a - 1" |
|
869 using f2 by (metis le_add1 le_trans one_le_power) |
|
870 hence "b \<le> 2 ^ a * (b + b + 1) - 1" |
|
871 using f1 by (metis le_diff_conv nat_add_commute nat_le_linear nat_mult_commute) |
|
872 thus "b \<le> 2 ^ a * (2 * b + 1) - 1" |
|
873 by (metis mult_2) |
|
874 qed |
591 |
875 |
592 section {* Discrete Logarithms *} |
876 section {* Discrete Logarithms *} |
593 |
877 |
594 definition |
878 definition |
595 "rec_lg = |
879 "rec_lg = |