585 by (induct x) (simp_all add: rec_max2_def) |
585 by (induct x) (simp_all add: rec_max2_def) |
586 |
586 |
587 section {* Encodings using Cantor's pairing function *} |
587 section {* Encodings using Cantor's pairing function *} |
588 |
588 |
589 text {* |
589 text {* |
590 We first have to prove that we can extract the maximal |
590 We use Cantor's pairing function from Nat_Bijection. |
591 triangle number using @{term prod_decode}. |
591 However, we need to prove that the formulation of the |
|
592 decoding function there is recursive. For this we first |
|
593 prove that we can extract the maximal triangle number |
|
594 using @{term prod_decode}. |
592 *} |
595 *} |
593 |
596 |
594 abbreviation Max_triangle_aux where |
597 abbreviation Max_triangle_aux where |
595 "Max_triangle_aux k z \<equiv> fst (prod_decode_aux k z) + snd (prod_decode_aux k z)" |
598 "Max_triangle_aux k z \<equiv> fst (prod_decode_aux k z) + snd (prod_decode_aux k z)" |
596 |
599 |
597 abbreviation Max_triangle where |
600 abbreviation Max_triangle where |
598 "Max_triangle z \<equiv> Max_triangle_aux 0 z" |
601 "Max_triangle z \<equiv> Max_triangle_aux 0 z" |
599 |
602 |
|
603 abbreviation |
|
604 "pdec1 z \<equiv> fst (prod_decode z)" |
|
605 |
|
606 abbreviation |
|
607 "pdec2 z \<equiv> snd (prod_decode z)" |
|
608 |
|
609 abbreviation |
|
610 "penc m n \<equiv> prod_encode (m, n)" |
|
611 |
600 lemma fst_prod_decode: |
612 lemma fst_prod_decode: |
601 "fst (prod_decode z) = z - triangle (Max_triangle z)" |
613 "pdec1 z = z - triangle (Max_triangle z)" |
602 apply(subst (3) prod_decode_inverse[symmetric]) |
614 by (subst (3) prod_decode_inverse[symmetric]) |
603 apply(simp add: prod_encode_def) |
615 (simp add: prod_encode_def prod_decode_def split: prod.split) |
604 apply(case_tac "prod_decode z") |
|
605 apply(simp add: prod_decode_def) |
|
606 done |
|
607 |
616 |
608 lemma snd_prod_decode: |
617 lemma snd_prod_decode: |
609 "snd (prod_decode z) = Max_triangle z - fst (prod_decode z)" |
618 "pdec2 z = Max_triangle z - pdec1 z" |
610 by (simp only: prod_decode_def) |
619 by (simp only: prod_decode_def) |
611 |
620 |
612 lemma le_triangle: |
621 lemma le_triangle: |
613 "m \<le> triangle (n + m)" |
622 "m \<le> triangle (n + m)" |
614 by (induct_tac m) (simp_all) |
623 by (induct_tac m) (simp_all) |
615 |
624 |
616 lemma k_aux: |
625 lemma Max_triangle_triangle_le: |
|
626 "triangle (Max_triangle z) \<le> z" |
|
627 by (subst (9) prod_decode_inverse[symmetric]) |
|
628 (simp add: prod_decode_def prod_encode_def split: prod.split) |
|
629 |
|
630 lemma Max_triangle_le: |
617 "Max_triangle z \<le> z" |
631 "Max_triangle z \<le> z" |
618 apply(subst (8) prod_decode_inverse[symmetric]) |
632 proof - |
619 apply(case_tac "prod_decode z") |
633 have "Max_triangle z \<le> triangle (Max_triangle z)" |
620 apply(simp add: prod_decode_def prod_encode_def le_triangle) |
634 using le_triangle[of _ 0, simplified] by simp |
621 done |
635 also have "... \<le> z" by (rule Max_triangle_triangle_le) |
622 |
636 finally show "Max_triangle z \<le> z" . |
623 lemma t_aux: |
637 qed |
624 "triangle (Max_triangle z) \<le> z" |
|
625 apply(subst (9) prod_decode_inverse[symmetric]) |
|
626 apply(case_tac "prod_decode z") |
|
627 apply(simp add: prod_decode_def prod_encode_def) |
|
628 done |
|
629 |
638 |
630 lemma w_aux: |
639 lemma w_aux: |
631 "Max_triangle (triangle k + m) = Max_triangle_aux k m" |
640 "Max_triangle (triangle k + m) = Max_triangle_aux k m" |
632 by (simp add: prod_decode_def[symmetric] prod_decode_triangle_add) |
641 by (simp add: prod_decode_def[symmetric] prod_decode_triangle_add) |
633 |
642 |
684 |
693 |
685 definition |
694 definition |
686 "rec_pdec2 = CN rec_minus [CN rec_max_triangle [Id 1 0], CN rec_pdec1 [Id 1 0]]" |
695 "rec_pdec2 = CN rec_minus [CN rec_max_triangle [Id 1 0], CN rec_pdec1 [Id 1 0]]" |
687 |
696 |
688 lemma pdec1_lemma [simp]: |
697 lemma pdec1_lemma [simp]: |
689 "rec_eval rec_pdec1 [z] = fst (prod_decode z)" |
698 "rec_eval rec_pdec1 [z] = pdec1 z" |
690 by (simp add: rec_pdec1_def fst_prod_decode) |
699 by (simp add: rec_pdec1_def fst_prod_decode) |
691 |
700 |
692 lemma pdec2_lemma [simp]: |
701 lemma pdec2_lemma [simp]: |
693 "rec_eval rec_pdec2 [z] = snd (prod_decode z)" |
702 "rec_eval rec_pdec2 [z] = pdec2 z" |
694 by (simp add: rec_pdec2_def snd_prod_decode) |
703 by (simp add: rec_pdec2_def snd_prod_decode) |
695 |
704 |
696 lemma penc_lemma [simp]: |
705 lemma penc_lemma [simp]: |
697 "rec_eval rec_penc [m, n] = prod_encode (m, n)" |
706 "rec_eval rec_penc [m, n] = penc m n" |
698 by (simp add: rec_penc_def prod_encode_def) |
707 by (simp add: rec_penc_def prod_encode_def) |
699 |
708 |
700 |
709 fun |
|
710 lenc :: "nat list \<Rightarrow> nat" |
|
711 where |
|
712 "lenc [] = 0" |
|
713 | "lenc (x # xs) = penc (Suc x) (lenc xs)" |
|
714 |
|
715 fun |
|
716 ldec :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
|
717 where |
|
718 "ldec z 0 = (pdec1 z) - 1" |
|
719 | "ldec z (Suc n) = ldec (pdec2 z) n" |
|
720 |
|
721 lemma pdec_zero_simps [simp]: |
|
722 "pdec1 0 = 0" |
|
723 "pdec2 0 = 0" |
|
724 by (simp_all add: prod_decode_def prod_decode_aux.simps) |
|
725 |
|
726 lemma w: |
|
727 "ldec 0 n = 0" |
|
728 by (induct n) (simp_all add: prod_decode_def prod_decode_aux.simps) |
|
729 |
|
730 lemma list_encode_inverse: |
|
731 "ldec (lenc xs) n = (if n < length xs then xs ! n else 0)" |
|
732 apply(induct xs arbitrary: n rule: lenc.induct) |
|
733 apply(simp_all add: w) |
|
734 apply(case_tac n) |
|
735 apply(simp_all) |
|
736 done |
|
737 |
|
738 fun within :: "nat \<Rightarrow> nat \<Rightarrow> bool" where |
|
739 "within z 0 = (0 < z)" |
|
740 | "within z (Suc n) = within (pdec2 z) n" |
|
741 |
701 |
742 |
702 section {* Discrete Logarithms *} |
743 section {* Discrete Logarithms *} |
703 |
744 |
704 definition |
745 definition |
705 "rec_lg = |
746 "rec_lg = |