625 |
625 |
626 lemma log_exp [simp]: |
626 lemma log_exp [simp]: |
627 "log (2 ^ n) = n" |
627 "log (2 ^ n) = n" |
628 by (induct n) simp_all |
628 by (induct n) simp_all |
629 |
629 |
630 fun divby2 :: "nat \<Rightarrow> nat" where |
630 fun oddfactor :: "nat \<Rightarrow> nat" where |
631 [simp del]: "divby2 n = (if n = 0 then 0 |
631 [simp del]: "oddfactor n = (if n = 0 then 0 else if even n then oddfactor (n div 2) else n)" |
632 else if even n then divby2 (n div 2) else n)" |
632 |
633 |
633 lemma oddfactor[simp]: |
634 lemma divby2[simp]: |
634 "oddfactor 0 = 0" |
635 "divby2 0 = 0" |
635 "odd n \<Longrightarrow> oddfactor n = n" |
636 "odd n \<Longrightarrow> divby2 n = n" |
636 "even n \<Longrightarrow> oddfactor n = oddfactor (n div 2)" |
637 "even n \<Longrightarrow> divby2 n = divby2 (n div 2)" |
637 apply(simp_all add: oddfactor.simps) |
638 apply(simp_all add: divby2.simps) |
638 done |
639 done |
639 |
640 |
640 lemma oddfactor_odd: |
641 lemma divby2_odd: |
641 "oddfactor n = 0 \<or> odd (oddfactor n)" |
642 "divby2 n = 0 \<or> odd (divby2 n)" |
|
643 apply(induct n rule: nat_less_induct) |
642 apply(induct n rule: nat_less_induct) |
644 apply(case_tac "n = 0") |
643 apply(case_tac "n = 0") |
645 apply(simp) |
644 apply(simp) |
646 apply(case_tac "odd n") |
645 apply(case_tac "odd n") |
647 apply(auto) |
646 apply(auto) |
648 done |
647 done |
649 |
648 |
650 lemma bigger: "divby2 (Suc n) > 0" |
649 lemma bigger: "oddfactor (Suc n) > 0" |
651 apply(induct n rule: nat_less_induct) |
650 apply(induct n rule: nat_less_induct) |
652 apply(case_tac "n = 0") |
651 apply(case_tac "n = 0") |
653 apply(simp) |
652 apply(simp) |
654 apply(case_tac "odd n") |
653 apply(case_tac "odd n") |
655 apply(auto) |
654 apply(auto) |
660 |
659 |
661 fun pencode :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
660 fun pencode :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
662 "pencode m n = (2 ^ m) * ((2 * n) + 1) - 1" |
661 "pencode m n = (2 ^ m) * ((2 * n) + 1) - 1" |
663 |
662 |
664 fun pdecode2 :: "nat \<Rightarrow> nat" where |
663 fun pdecode2 :: "nat \<Rightarrow> nat" where |
665 "pdecode2 z = (divby2 (Suc z) - 1) div 2" |
664 "pdecode2 z = (oddfactor (Suc z) - 1) div 2" |
666 |
665 |
667 fun pdecode1 :: "nat \<Rightarrow> nat" where |
666 fun pdecode1 :: "nat \<Rightarrow> nat" where |
668 "pdecode1 z = log ((Suc z) div (divby2 (Suc z)))" |
667 "pdecode1 z = log ((Suc z) div (oddfactor (Suc z)))" |
669 |
668 |
670 lemma k: |
669 lemma k: |
671 "odd n \<Longrightarrow> divby2 (2 ^ m * n) = n" |
670 "odd n \<Longrightarrow> oddfactor (2 ^ m * n) = n" |
672 apply(induct m) |
671 apply(induct m) |
673 apply(simp_all) |
672 apply(simp_all) |
674 done |
673 done |
675 |
674 |
676 lemma ww: "\<exists>k. n = 2 ^ k * divby2 n" |
675 lemma ww: "\<exists>k. n = 2 ^ k * oddfactor n" |
677 apply(induct n rule: nat_less_induct) |
676 apply(induct n rule: nat_less_induct) |
678 apply(case_tac "n=0") |
677 apply(case_tac "n=0") |
679 apply(simp) |
678 apply(simp) |
680 apply(case_tac "odd n") |
679 apply(case_tac "odd n") |
681 apply(simp) |
680 apply(simp) |
705 by (induct n) (simp_all) |
704 by (induct n) (simp_all) |
706 |
705 |
707 lemma test: "x = y \<Longrightarrow> 2 * x = 2 * y" |
706 lemma test: "x = y \<Longrightarrow> 2 * x = 2 * y" |
708 by simp |
707 by simp |
709 |
708 |
710 lemma m: "0 < n ==> 2 ^ log (n div (divby2 n)) = n div (divby2 n)" |
709 lemma m: "0 < n ==> 2 ^ log (n div (oddfactor n)) = n div (oddfactor n)" |
711 apply(induct n rule: nat_less_induct) |
710 apply(induct n rule: nat_less_induct) |
712 apply(case_tac "n=0") |
711 apply(case_tac "n=0") |
713 apply(simp) |
712 apply(simp) |
714 apply(case_tac "odd n") |
713 apply(case_tac "odd n") |
715 apply(simp) |
714 apply(simp) |
716 apply(drule_tac x="n div 2" in spec) |
715 apply(drule_tac x="n div 2" in spec) |
717 apply(drule mp) |
716 apply(drule mp) |
718 apply(auto)[1] |
717 apply(auto)[1] |
719 apply(drule mp) |
718 apply(drule mp) |
720 apply (metis One_nat_def Suc_lessI div_2_gt_zero odd_1_nat) |
719 apply (metis One_nat_def Suc_lessI div_2_gt_zero odd_1_nat) |
721 apply(subst (asm) divby2(3)[symmetric]) |
720 apply(subst (asm) oddfactor(3)[symmetric]) |
722 apply(simp) |
721 apply(simp) |
723 apply(subst (asm) divby2(3)[symmetric]) |
722 apply(subst (asm) oddfactor(3)[symmetric]) |
724 apply(simp) |
723 apply(simp) |
725 apply(subgoal_tac "n div 2 div divby2 n = n div (divby2 n) div 2") |
724 apply(subgoal_tac "n div 2 div oddfactor n = n div (oddfactor n) div 2") |
726 prefer 2 |
725 prefer 2 |
727 apply (metis div_mult2_eq nat_mult_commute) |
726 apply (metis div_mult2_eq nat_mult_commute) |
728 apply(simp only: log_half) |
727 apply(simp only: log_half) |
729 apply(case_tac "n div divby2 n = 0") |
728 apply(case_tac "n div oddfactor n = 0") |
730 apply(simp) |
729 apply(simp) |
731 apply(simp del: divby2) |
730 apply(simp del: oddfactor) |
732 apply(drule test) |
731 apply(drule test) |
733 apply(subst (asm) power.simps(2)[symmetric]) |
732 apply(subst (asm) power.simps(2)[symmetric]) |
734 apply(subgoal_tac "Suc (log (n div divby2 n) - 1) = log (n div divby2 n)") |
733 apply(subgoal_tac "Suc (log (n div oddfactor n) - 1) = log (n div oddfactor n)") |
735 prefer 2 |
734 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)) |
735 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:) |
736 apply(simp only:) |
738 apply(subst dvd_mult_div_cancel) |
737 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) |
738 apply (smt Suc_1 div_by_0 div_mult_self2_is_id oddfactor_odd dvd_power even_Suc even_numeral_nat even_product_nat nat_even_iff_2_dvd power_0 ww) |
740 apply(simp (no_asm)) |
739 apply(simp (no_asm)) |
741 done |
740 done |
742 |
741 |
743 lemma m1: "n div divby2 n * divby2 n = n" |
742 lemma m1: "n div oddfactor n * oddfactor n = n" |
744 apply(induct n rule: nat_less_induct) |
743 apply(induct n rule: nat_less_induct) |
745 apply(case_tac "n=0") |
744 apply(case_tac "n=0") |
746 apply(simp) |
745 apply(simp) |
747 apply(case_tac "odd n") |
746 apply(case_tac "odd n") |
748 apply(simp) |
747 apply(simp) |
749 apply(simp) |
748 apply(simp) |
750 apply(drule_tac x="n div 2" in spec) |
749 apply(drule_tac x="n div 2" in spec) |
751 apply(drule mp) |
750 apply(drule mp) |
752 apply(auto)[1] |
751 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) |
752 by (metis add_eq_if diff_add_inverse oddfactor(3) mod_eq_0_iff mult_div_cancel nat_mult_commute ww) |
754 |
753 |
755 |
754 |
756 lemma m2: "0 < n ==> 2 ^ log (n div (divby2 n)) * (divby2 n) = n" |
755 lemma m2: "0 < n ==> 2 ^ log (n div (oddfactor n)) * (oddfactor n) = n" |
757 apply(subst m) |
756 apply(subst m) |
758 apply(simp) |
757 apply(simp) |
759 apply(subst m1) |
758 apply(subst m1) |
760 apply(simp) |
759 apply(simp) |
761 done |
760 done |
767 apply(auto) |
766 apply(auto) |
768 done |
767 done |
769 |
768 |
770 lemma y2: |
769 lemma y2: |
771 "pdecode1 (pencode m n) = m" |
770 "pdecode1 (pencode m n) = m" |
|
771 using [[simp_trace]] |
772 apply(simp) |
772 apply(simp) |
773 apply(subst k) |
773 apply(subst k) |
774 apply(auto)[1] |
774 apply(auto)[1] |
|
775 using [[simp_trace_depth_limit=10]] |
775 apply(simp) |
776 apply(simp) |
776 done |
777 done |
777 |
778 |
778 lemma yy: |
779 lemma yy: |
779 "pencode (pdecode1 m) (pdecode2 m) = m" |
780 "pencode (pdecode1 m) (pdecode2 m) = m" |
780 apply(induct m rule: nat_less_induct) |
781 apply(induct m rule: nat_less_induct) |
781 apply(simp (no_asm)) |
782 apply(simp (no_asm)) |
782 apply(case_tac "n = 0") |
783 apply(case_tac "n = 0") |
783 apply(simp) |
784 apply(simp) |
784 apply(subst dvd_mult_div_cancel) |
785 apply(subst dvd_mult_div_cancel) |
785 using divby2_odd |
786 using oddfactor_odd |
786 apply - |
787 apply - |
787 apply(drule_tac x="Suc n" in meta_spec) |
788 apply(drule_tac x="Suc n" in meta_spec) |
788 apply(erule disjE) |
789 apply(erule disjE) |
789 apply(auto)[1] |
790 apply(auto)[1] |
790 apply (metis even_num_iff nat_even_iff_2_dvd odd_pos) |
791 apply (metis even_num_iff nat_even_iff_2_dvd odd_pos) |