593 |
582 |
594 lemma max2_lemma [simp]: |
583 lemma max2_lemma [simp]: |
595 "rec_eval (rec_max2 f) [x, y1, y2] = BMax_rec (\<lambda>u. rec_eval f [u, y1, y2] = 0) x" |
584 "rec_eval (rec_max2 f) [x, y1, y2] = BMax_rec (\<lambda>u. rec_eval f [u, y1, y2] = 0) x" |
596 by (induct x) (simp_all add: rec_max2_def) |
585 by (induct x) (simp_all add: rec_max2_def) |
597 |
586 |
598 section {* Encodings *} |
587 section {* Encodings using Cantor's pairing function *} |
599 |
588 |
600 fun prod_decode1 where |
589 text {* |
601 "prod_decode1 z = z - (triangle (BMax_rec (\<lambda>k. triangle k \<le> z) z))" |
590 We first have to prove that we can extract the maximal |
602 |
591 triangle number using @{term prod_decode}. |
603 fun prod_decode2 where |
592 *} |
604 "prod_decode2 z = BMax_rec (\<lambda>k. triangle k \<le> z) z - prod_decode1 z" |
593 |
605 |
594 abbreviation Max_triangle_aux where |
606 section {* Encodings *} |
595 "Max_triangle_aux k z \<equiv> fst (prod_decode_aux k z) + snd (prod_decode_aux k z)" |
607 |
596 |
608 lemma triangle_sum: |
597 abbreviation Max_triangle where |
609 "triangle k = (\<Sum>i \<le> k. i)" |
598 "Max_triangle z \<equiv> Max_triangle_aux 0 z" |
610 by (induct k) (simp_all) |
599 |
611 |
600 lemma fst_prod_decode: |
612 fun sqrt where |
601 "fst (prod_decode z) = z - triangle (Max_triangle z)" |
613 "sqrt z = BMax_rec (\<lambda>x. x * x \<le> z) z" |
602 apply(subst (3) prod_decode_inverse[symmetric]) |
614 |
603 apply(simp add: prod_encode_def) |
615 lemma sqrt_bounded_Max: |
604 apply(case_tac "prod_decode z") |
616 "Discrete.sqrt n = Max (Set.filter (\<lambda>m. m\<twosuperior> \<le> n) {0..n})" |
605 apply(simp add: prod_decode_def) |
617 proof - |
606 done |
618 from power2_nat_le_imp_le [of _ n] have "{m. m \<le> n \<and> m\<twosuperior> \<le> n} = {m. m\<twosuperior> \<le> n}" by auto |
607 |
619 then show ?thesis by (simp add: Discrete.sqrt_def Set.filter_def) |
608 lemma snd_prod_decode: |
620 qed |
609 "snd (prod_decode z) = Max_triangle z - fst (prod_decode z)" |
621 |
610 by (simp only: prod_decode_def) |
622 lemma sqrt: "Discrete.sqrt z = sqrt z" |
611 |
623 apply(simp add: BMax_rec_eq3 sqrt_bounded_Max Set.filter_def power2_eq_square) |
612 lemma le_triangle: |
624 apply(rule_tac f="Max" in arg_cong) |
613 "m \<le> triangle (n + m)" |
625 apply(auto) |
614 by (induct_tac m) (simp_all) |
626 done |
615 |
627 |
616 lemma k_aux: |
628 fun i where |
617 "Max_triangle z \<le> z" |
629 "i z = (Discrete.sqrt (1 + 8 * z) - 1) div 2" |
618 apply(subst (8) prod_decode_inverse[symmetric]) |
630 |
619 apply(case_tac "prod_decode z") |
631 lemma "map prod_decode [0,1,2,3,4,5,6,7,8,9,10,11,12] = |
620 apply(simp add: prod_decode_def prod_encode_def le_triangle) |
632 [(0, 0), (0, 1), (1, 0), (0, 2), (1, 1), (2, 0), (0, 3), |
621 done |
633 (1, 2), (2, 1), (3, 0), (0, 4), (1, 3), (2, 2)]" |
622 |
634 apply(simp add: prod_decode_def prod_decode_aux.simps) |
623 lemma t_aux: |
635 done |
624 "triangle (Max_triangle z) \<le> z" |
636 |
625 apply(subst (9) prod_decode_inverse[symmetric]) |
637 lemma "map triangle [0, 1, 2, 3, 4, 5, 6 ] = [0, 1, 3, 6, 10, 15, 21]" |
626 apply(case_tac "prod_decode z") |
638 by(simp add: numeral_eq_Suc One_nat_def) |
627 apply(simp add: prod_decode_def prod_encode_def) |
639 |
628 done |
640 lemma "map (\<lambda>z. (z - (i(z) * (1 + i(z))) div 2, (i(z) * (3 + i(z))) div 2 - z)) |
629 |
641 [0,1,2,3,4,5,6,7,8,9,10,11,12] = |
630 lemma w_aux: |
642 [(0, 0), (0, 1), (1, 0), (0, 2), (1, 1), (2, 0), (0, 3), |
631 "Max_triangle (triangle k + m) = Max_triangle_aux k m" |
643 (1, 2), (2, 1), (3, 0), (0, 4), (1, 3), (2, 2)]" |
632 by (simp add: prod_decode_def[symmetric] prod_decode_triangle_add) |
644 apply(simp add: sqrt) |
633 |
645 by eval |
634 lemma y_aux: "y \<le> Max_triangle_aux y k" |
646 |
|
647 fun prod_add where |
|
648 "prod_add (m, n) = m + n" |
|
649 |
|
650 fun |
|
651 Max_triangle :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
|
652 where |
|
653 "Max_triangle k m = |
|
654 (if m \<le> k then k else Max_triangle (Suc k) (m - Suc k))" |
|
655 |
|
656 declare Max_triangle.simps [simp del] |
|
657 |
|
658 lemma k: "Max_triangle k z \<le> k + z" |
|
659 apply(induct z arbitrary: k rule: nat_less_induct) |
|
660 apply(subst Max_triangle.simps) |
|
661 apply(simp del: Max_triangle.simps) |
|
662 apply(rule impI) |
|
663 apply(drule_tac x="n - Suc k" in spec) |
|
664 apply(drule mp) |
|
665 apply(auto)[1] |
|
666 apply(drule_tac x="Suc k" in spec) |
|
667 apply(simp) |
|
668 done |
|
669 |
|
670 lemma k_aux: "prod_add (prod_decode_aux k z) \<le> k + z" |
|
671 apply(induct z arbitrary: k rule: nat_less_induct) |
|
672 apply(subst prod_decode_aux.simps) |
|
673 apply(simp) |
|
674 apply(rule impI) |
|
675 apply(drule_tac x="n - Suc k" in spec) |
|
676 apply(drule mp) |
|
677 apply(auto)[1] |
|
678 apply(drule_tac x="Suc k" in spec) |
|
679 apply(simp) |
|
680 done |
|
681 |
|
682 lemma t: "triangle (Max_triangle k m) \<le> triangle k + m" |
|
683 apply (induct k m rule: Max_triangle.induct) |
|
684 apply (simp add: Max_triangle.simps) |
|
685 done |
|
686 |
|
687 lemma t_aux: |
|
688 "triangle (prod_add (prod_decode_aux k m)) \<le> triangle k + m" |
|
689 apply (induct k m rule: prod_decode_aux.induct) |
|
690 apply (simp add: prod_decode_aux.simps) |
|
691 done |
|
692 |
|
693 lemma w: "Max_triangle 0 (triangle y + m) = Max_triangle y m" |
|
694 apply(induct y arbitrary: m) |
|
695 apply(simp) |
|
696 apply(simp only: triangle_Suc add_assoc) |
|
697 apply(subst Max_triangle.simps) |
|
698 apply(simp) |
|
699 done |
|
700 |
|
701 lemma w_aux: "prod_add (prod_decode (triangle y + m)) = prod_add (prod_decode_aux y m)" |
|
702 apply(simp add: prod_decode_triangle_add) |
|
703 done |
|
704 |
|
705 lemma y: "y \<le> Max_triangle y k" |
|
706 apply(induct k arbitrary: y rule: nat_less_induct) |
635 apply(induct k arbitrary: y rule: nat_less_induct) |
707 apply(subst Max_triangle.simps) |
636 apply(subst (1 2) prod_decode_aux.simps) |
708 apply(simp del: Max_triangle.simps) |
|
709 apply(rule impI) |
|
710 apply(drule_tac x="n - Suc y" in spec) |
|
711 apply(drule mp) |
|
712 apply(auto)[1] |
|
713 apply(drule_tac x="Suc y" in spec) |
|
714 apply(erule Suc_leD) |
|
715 done |
|
716 |
|
717 lemma y_aux: "y \<le> prod_add (prod_decode_aux y k)" |
|
718 apply(induct k arbitrary: y rule: nat_less_induct) |
|
719 apply(subst prod_decode_aux.simps) |
|
720 apply(simp) |
637 apply(simp) |
721 apply(rule impI) |
638 apply(rule impI) |
722 apply(drule_tac x="n - Suc y" in spec) |
639 apply(drule_tac x="n - Suc y" in spec) |
723 apply(drule mp) |
640 apply(drule mp) |
724 apply(auto)[1] |
641 apply(auto)[1] |
725 apply(drule_tac x="Suc y" in spec) |
642 apply(drule_tac x="Suc y" in spec) |
726 apply(erule Suc_leD) |
643 apply(erule Suc_leD) |
727 done |
644 done |
728 |
645 |
729 lemma q3: "Max_triangle 0 z = (GREAT k. (triangle k \<le> z \<and> k \<le> z) \<or> k = 0)" |
646 lemma Max_triangle_greatest: |
730 apply(rule sym) |
647 "Max_triangle z = (GREATEST k. (triangle k \<le> z \<and> k \<le> z) \<or> k = 0)" |
731 apply(rule Great_equality) |
648 apply(rule Greatest_equality[symmetric]) |
732 apply(rule disjI1) |
649 apply(rule disjI1) |
733 apply(rule conjI) |
650 apply(rule conjI) |
734 apply(rule t[of 0, simplified]) |
651 apply(rule t_aux) |
735 apply(rule k[of 0, simplified]) |
652 apply(rule k_aux) |
736 apply(erule disjE) |
|
737 apply(erule conjE) |
|
738 apply(subst (asm) (1) le_iff_add) |
|
739 apply(erule exE) |
|
740 apply(clarify) |
|
741 apply(simp only: w) |
|
742 apply(rule y) |
|
743 apply(simp) |
|
744 done |
|
745 |
|
746 lemma q3_aux: "prod_add (prod_decode z) = (GREAT k. (triangle k \<le> z \<and> k \<le> z) \<or> k = 0)" |
|
747 apply(rule sym) |
|
748 apply(rule Great_equality) |
|
749 apply(rule disjI1) |
|
750 apply(rule conjI) |
|
751 apply(simp only: prod_decode_def) |
|
752 apply(rule t_aux[of 0, simplified]) |
|
753 apply(simp only: prod_decode_def) |
|
754 apply(rule k_aux[of 0, simplified]) |
|
755 apply(erule disjE) |
653 apply(erule disjE) |
756 apply(erule conjE) |
654 apply(erule conjE) |
757 apply(subst (asm) (1) le_iff_add) |
655 apply(subst (asm) (1) le_iff_add) |
758 apply(erule exE) |
656 apply(erule exE) |
759 apply(clarify) |
657 apply(clarify) |
760 apply(simp only: w_aux) |
658 apply(simp only: w_aux) |
761 apply(rule y_aux) |
659 apply(rule y_aux) |
762 apply(simp) |
660 apply(simp) |
763 done |
661 done |
764 |
662 |
765 |
663 definition |
766 definition |
664 "rec_triangle = CN rec_quo [CN rec_mult [Id 1 0, S], constn 2]" |
767 "rec_triangle = CN rec_quo [CN rec_mult [Id 1 0, CN S [Id 1 0]], constn 2]" |
|
768 |
665 |
769 lemma triangle_lemma [simp]: |
666 lemma triangle_lemma [simp]: |
770 "rec_eval rec_triangle [x] = triangle x" |
667 "rec_eval rec_triangle [x] = triangle x" |
771 by (simp add: rec_triangle_def triangle_def) |
668 by (simp add: rec_triangle_def triangle_def) |
772 |
669 |
773 definition |
670 definition |
774 "rec_max_triangle = |
671 "rec_max_triangle = |
775 (let cond = CN rec_not [CN rec_le [CN rec_triangle [Id 2 0], Id 2 1]] in |
672 (let cond = CN rec_not [CN rec_le [CN rec_triangle [Id 2 0], Id 2 1]] in |
776 CN (rec_max1 cond) [Id 1 0, Id 1 0])" |
673 CN (rec_max1 cond) [Id 1 0, Id 1 0])" |
777 |
674 |
778 lemma max_triangle_lemma_test: |
|
779 "rec_eval rec_max_triangle [x] = Max_triangle 0 x" |
|
780 apply(simp add: q3) |
|
781 apply(simp add: rec_max_triangle_def) |
|
782 apply(simp add: BMax_rec_eq1) |
|
783 done |
|
784 |
|
785 lemma max_triangle_lemma [simp]: |
675 lemma max_triangle_lemma [simp]: |
786 "rec_eval rec_max_triangle [x] = prod_add (prod_decode x)" |
676 "rec_eval rec_max_triangle [x] = Max_triangle x" |
787 apply(simp add: q3_aux) |
677 by (simp add: Max_triangle_greatest rec_max_triangle_def Let_def BMax_rec_eq1) |
788 apply(simp add: rec_max_triangle_def) |
|
789 apply(simp add: BMax_rec_eq1) |
|
790 done |
|
791 |
|
792 lemma ww: "fst (prod_decode_aux k z) + snd (prod_decode_aux k z) = Max_triangle k z" |
|
793 apply(induct z arbitrary: k rule: nat_less_induct) |
|
794 apply(subst Max_triangle.simps) |
|
795 apply(simp) |
|
796 apply(rule conjI) |
|
797 apply(simp add: prod_decode_aux.simps) |
|
798 apply(rule impI) |
|
799 apply(drule_tac x="n - Suc k" in spec) |
|
800 apply(drule mp) |
|
801 apply(auto)[1] |
|
802 apply(drule_tac x="Suc k" in spec) |
|
803 apply(subst prod_decode_aux.simps) |
|
804 apply(subst (2) prod_decode_aux.simps) |
|
805 apply(simp) |
|
806 done |
|
807 |
|
808 lemma ww0: |
|
809 "fst (prod_decode z) + snd (prod_decode z) = Max_triangle 0 z" |
|
810 by (simp only: prod_decode_def ww) |
|
811 |
|
812 lemma zz: "fst (prod_decode_aux k z) = (triangle k + z) - triangle (Max_triangle k z)" |
|
813 apply(induct z arbitrary: k rule: nat_less_induct) |
|
814 apply(subst Max_triangle.simps) |
|
815 apply(simp) |
|
816 apply(rule conjI) |
|
817 apply(rule impI) |
|
818 apply(subst prod_decode_aux.simps) |
|
819 apply(simp) |
|
820 apply(rule impI) |
|
821 apply(subst prod_decode_aux.simps) |
|
822 apply(simp) |
|
823 done |
|
824 |
|
825 lemma zz0: |
|
826 "fst (prod_decode z) = z - triangle (Max_triangle 0 z)" |
|
827 apply(simp add: prod_decode_def zz) |
|
828 done |
|
829 |
|
830 lemma yy0: |
|
831 "snd (prod_decode z) = Max_triangle 0 z - fst (prod_decode z)" |
|
832 apply(simp add: ww0[symmetric]) |
|
833 done |
|
834 |
|
835 lemma final: "prod_decode z = (let k = Max_triangle 0 z in |
|
836 let m = z - triangle k in (m, k - m))" |
|
837 apply(simp add: Let_def zz0[symmetric] yy0[symmetric]) |
|
838 done |
|
839 |
678 |
840 definition |
679 definition |
841 "rec_penc = CN rec_add [CN rec_triangle [CN rec_add [Id 2 0, Id 2 1]], Id 2 0]" |
680 "rec_penc = CN rec_add [CN rec_triangle [CN rec_add [Id 2 0, Id 2 1]], Id 2 0]" |
842 |
681 |
843 definition |
682 definition |
943 "rec_eval rec_pi [x] = Pi x" |
783 "rec_eval rec_pi [x] = Pi x" |
944 by (induct x) (simp_all add: rec_pi_def) |
784 by (induct x) (simp_all add: rec_pi_def) |
945 |
785 |
946 end |
786 end |
947 |
787 |
948 (* |
|
949 |
|
950 lemma rec_minr2_le_Suc: |
|
951 "rec_eval (rec_minr2 f) [x, y1, y2] \<le> Suc x" |
|
952 apply(simp add: rec_minr2_def) |
|
953 apply(auto intro!: setsum_one_le setprod_one_le) |
|
954 done |
|
955 |
|
956 lemma rec_minr2_eq_Suc: |
|
957 assumes "\<forall>z \<le> x. rec_eval f [z, y1, y2] = 0" |
|
958 shows "rec_eval (rec_minr2 f) [x, y1, y2] = Suc x" |
|
959 using assms by (simp add: rec_minr2_def) |
|
960 |
|
961 lemma rec_minr2_le: |
|
962 assumes h1: "y \<le> x" |
|
963 and h2: "0 < rec_eval f [y, y1, y2]" |
|
964 shows "rec_eval (rec_minr2 f) [x, y1, y2] \<le> y" |
|
965 apply(simp add: rec_minr2_def) |
|
966 apply(subst setsum_cut_off_le[OF h1]) |
|
967 using h2 apply(auto) |
|
968 apply(auto intro!: setsum_one_less setprod_one_le) |
|
969 done |
|
970 |
|
971 (* ??? *) |
|
972 lemma setsum_eq_one_le2: |
|
973 fixes n::nat |
|
974 assumes "\<forall>i \<le> n. f i \<le> 1" |
|
975 shows "((\<Sum>i \<le> n. f i) \<ge> Suc n) \<Longrightarrow> (\<forall>i \<le> n. f i = 1)" |
|
976 using assms |
|
977 apply(induct n) |
|
978 apply(simp add: One_nat_def) |
|
979 apply(simp) |
|
980 apply(auto simp add: One_nat_def) |
|
981 apply(drule_tac x="Suc n" in spec) |
|
982 apply(auto) |
|
983 by (metis le_Suc_eq) |
|
984 |
|
985 |
|
986 lemma rec_min2_not: |
|
987 assumes "rec_eval (rec_minr2 f) [x, y1, y2] = Suc x" |
|
988 shows "\<forall>z \<le> x. rec_eval f [z, y1, y2] = 0" |
|
989 using assms |
|
990 apply(simp add: rec_minr2_def) |
|
991 apply(subgoal_tac "\<forall>i \<le> x. (\<Prod>z\<le>i. if rec_eval f [z, y1, y2] = 0 then 1 else 0) = (1::nat)") |
|
992 apply(simp) |
|
993 apply (metis atMost_iff le_refl zero_neq_one) |
|
994 apply(rule setsum_eq_one_le2) |
|
995 apply(auto) |
|
996 apply(rule setprod_one_le) |
|
997 apply(auto) |
|
998 done |
|
999 |
|
1000 lemma disjCI2: |
|
1001 assumes "~P ==> Q" shows "P|Q" |
|
1002 apply (rule classical) |
|
1003 apply (iprover intro: assms disjI1 disjI2 notI elim: notE) |
|
1004 done |
|
1005 |
|
1006 lemma minr_lemma [simp]: |
|
1007 shows "rec_eval (rec_minr2 f) [x, y1, y2] = (LEAST z. (z \<le> x \<and> 0 < rec_eval f [z, y1, y2]) \<or> z = Suc x)" |
|
1008 apply(induct x) |
|
1009 apply(rule Least_equality[symmetric]) |
|
1010 apply(simp add: rec_minr2_def) |
|
1011 apply(erule disjE) |
|
1012 apply(rule rec_minr2_le) |
|
1013 apply(auto)[2] |
|
1014 apply(simp) |
|
1015 apply(rule rec_minr2_le_Suc) |
|
1016 apply(simp) |
|
1017 |
|
1018 apply(rule rec_minr2_le) |
|
1019 |
|
1020 |
|
1021 apply(rule rec_minr2_le_Suc) |
|
1022 apply(rule disjCI) |
|
1023 apply(simp add: rec_minr2_def) |
|
1024 |
|
1025 apply(ru le setsum_one_less) |
|
1026 apply(clarify) |
|
1027 apply(rule setprod_one_le) |
|
1028 apply(auto)[1] |
|
1029 apply(simp) |
|
1030 apply(rule setsum_one_le) |
|
1031 apply(clarify) |
|
1032 apply(rule setprod_one_le) |
|
1033 apply(auto)[1] |
|
1034 thm disj_CE |
|
1035 apply(auto) |
|
1036 |
|
1037 lemma minr_lemma: |
|
1038 shows "rec_eval (rec_minr2 f) [x, y1, y2] = Minr (\<lambda>x xs. (0 < rec_eval f (x #xs))) x [y1, y2]" |
|
1039 apply(simp only: Minr_def) |
|
1040 apply(rule sym) |
|
1041 apply(rule Min_eqI) |
|
1042 apply(auto)[1] |
|
1043 apply(simp) |
|
1044 apply(erule disjE) |
|
1045 apply(simp) |
|
1046 apply(rule rec_minr2_le_Suc) |
|
1047 apply(rule rec_minr2_le) |
|
1048 apply(auto)[2] |
|
1049 apply(simp) |
|
1050 apply(induct x) |
|
1051 apply(simp add: rec_minr2_def) |
|
1052 apply( |
|
1053 apply(rule disjCI) |
|
1054 apply(rule rec_minr2_eq_Suc) |
|
1055 apply(simp) |
|
1056 apply(auto) |
|
1057 |
|
1058 apply(rule setsum_one_le) |
|
1059 apply(auto)[1] |
|
1060 apply(rule setprod_one_le) |
|
1061 apply(auto)[1] |
|
1062 apply(subst setsum_cut_off_le) |
|
1063 apply(auto)[2] |
|
1064 apply(rule setsum_one_less) |
|
1065 apply(auto)[1] |
|
1066 apply(rule setprod_one_le) |
|
1067 apply(auto)[1] |
|
1068 apply(simp) |
|
1069 thm setsum_eq_one_le |
|
1070 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> |
|
1071 (\<not> (\<forall>z\<le>x. (\<Prod>z\<le>z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)))") |
|
1072 prefer 2 |
|
1073 apply(auto)[1] |
|
1074 apply(erule disjE) |
|
1075 apply(rule disjI1) |
|
1076 apply(rule setsum_eq_one_le) |
|
1077 apply(simp) |
|
1078 apply(rule disjI2) |
|
1079 apply(simp) |
|
1080 apply(clarify) |
|
1081 apply(subgoal_tac "\<exists>l. l = (LEAST z. 0 < rec_eval f [z, y1, y2])") |
|
1082 defer |
|
1083 apply metis |
|
1084 apply(erule exE) |
|
1085 apply(subgoal_tac "l \<le> x") |
|
1086 defer |
|
1087 apply (metis not_leE not_less_Least order_trans) |
|
1088 apply(subst setsum_least_eq) |
|
1089 apply(rotate_tac 4) |
|
1090 apply(assumption) |
|
1091 apply(auto)[1] |
|
1092 apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])") |
|
1093 prefer 2 |
|
1094 apply(auto)[1] |
|
1095 apply(rotate_tac 5) |
|
1096 apply(drule not_less_Least) |
|
1097 apply(auto)[1] |
|
1098 apply(auto) |
|
1099 apply(rule_tac x="(LEAST z. 0 < rec_eval f [z, y1, y2])" in exI) |
|
1100 apply(simp) |
|
1101 apply (metis LeastI_ex) |
|
1102 apply(subst setsum_least_eq) |
|
1103 apply(rotate_tac 3) |
|
1104 apply(assumption) |
|
1105 apply(simp) |
|
1106 apply(auto)[1] |
|
1107 apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])") |
|
1108 prefer 2 |
|
1109 apply(auto)[1] |
|
1110 apply (metis neq0_conv not_less_Least) |
|
1111 apply(auto)[1] |
|
1112 apply (metis (mono_tags) LeastI_ex) |
|
1113 by (metis LeastI_ex) |
|
1114 |
|
1115 lemma minr_lemma: |
|
1116 shows "rec_eval (rec_minr2 f) [x, y1, y2] = Minr (\<lambda>x xs. (0 < rec_eval f (x #xs))) x [y1, y2]" |
|
1117 apply(simp only: Minr_def rec_minr2_def) |
|
1118 apply(simp) |
|
1119 apply(rule sym) |
|
1120 apply(rule Min_eqI) |
|
1121 apply(auto)[1] |
|
1122 apply(simp) |
|
1123 apply(erule disjE) |
|
1124 apply(simp) |
|
1125 apply(rule setsum_one_le) |
|
1126 apply(auto)[1] |
|
1127 apply(rule setprod_one_le) |
|
1128 apply(auto)[1] |
|
1129 apply(subst setsum_cut_off_le) |
|
1130 apply(auto)[2] |
|
1131 apply(rule setsum_one_less) |
|
1132 apply(auto)[1] |
|
1133 apply(rule setprod_one_le) |
|
1134 apply(auto)[1] |
|
1135 apply(simp) |
|
1136 thm setsum_eq_one_le |
|
1137 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> |
|
1138 (\<not> (\<forall>z\<le>x. (\<Prod>z\<le>z. if rec_eval f [z, y1, y2] = (0::nat) then 1 else 0) > (0::nat)))") |
|
1139 prefer 2 |
|
1140 apply(auto)[1] |
|
1141 apply(erule disjE) |
|
1142 apply(rule disjI1) |
|
1143 apply(rule setsum_eq_one_le) |
|
1144 apply(simp) |
|
1145 apply(rule disjI2) |
|
1146 apply(simp) |
|
1147 apply(clarify) |
|
1148 apply(subgoal_tac "\<exists>l. l = (LEAST z. 0 < rec_eval f [z, y1, y2])") |
|
1149 defer |
|
1150 apply metis |
|
1151 apply(erule exE) |
|
1152 apply(subgoal_tac "l \<le> x") |
|
1153 defer |
|
1154 apply (metis not_leE not_less_Least order_trans) |
|
1155 apply(subst setsum_least_eq) |
|
1156 apply(rotate_tac 4) |
|
1157 apply(assumption) |
|
1158 apply(auto)[1] |
|
1159 apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])") |
|
1160 prefer 2 |
|
1161 apply(auto)[1] |
|
1162 apply(rotate_tac 5) |
|
1163 apply(drule not_less_Least) |
|
1164 apply(auto)[1] |
|
1165 apply(auto) |
|
1166 apply(rule_tac x="(LEAST z. 0 < rec_eval f [z, y1, y2])" in exI) |
|
1167 apply(simp) |
|
1168 apply (metis LeastI_ex) |
|
1169 apply(subst setsum_least_eq) |
|
1170 apply(rotate_tac 3) |
|
1171 apply(assumption) |
|
1172 apply(simp) |
|
1173 apply(auto)[1] |
|
1174 apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y1, y2])") |
|
1175 prefer 2 |
|
1176 apply(auto)[1] |
|
1177 apply (metis neq0_conv not_less_Least) |
|
1178 apply(auto)[1] |
|
1179 apply (metis (mono_tags) LeastI_ex) |
|
1180 by (metis LeastI_ex) |
|
1181 |
|
1182 lemma disjCI2: |
|
1183 assumes "~P ==> Q" shows "P|Q" |
|
1184 apply (rule classical) |
|
1185 apply (iprover intro: assms disjI1 disjI2 notI elim: notE) |
|
1186 done |
|
1187 |
|
1188 |
|
1189 lemma minr_lemma [simp]: |
|
1190 shows "rec_eval (rec_minr2 f) [x, y1, y2] = (LEAST z. (z \<le> x \<and> 0 < rec_eval f [z, y1, y2]) \<or> z = Suc x)" |
|
1191 (*apply(simp add: rec_minr2_def)*) |
|
1192 apply(rule Least_equality[symmetric]) |
|
1193 prefer 2 |
|
1194 apply(erule disjE) |
|
1195 apply(rule rec_minr2_le) |
|
1196 apply(auto)[2] |
|
1197 apply(clarify) |
|
1198 apply(rule rec_minr2_le_Suc) |
|
1199 apply(rule disjCI) |
|
1200 apply(simp add: rec_minr2_def) |
|
1201 |
|
1202 apply(ru le setsum_one_less) |
|
1203 apply(clarify) |
|
1204 apply(rule setprod_one_le) |
|
1205 apply(auto)[1] |
|
1206 apply(simp) |
|
1207 apply(rule setsum_one_le) |
|
1208 apply(clarify) |
|
1209 apply(rule setprod_one_le) |
|
1210 apply(auto)[1] |
|
1211 thm disj_CE |
|
1212 apply(auto) |
|
1213 apply(auto) |
|
1214 prefer 2 |
|
1215 apply(rule le_tran |
|
1216 |
|
1217 apply(rule le_trans) |
|
1218 apply(simp) |
|
1219 defer |
|
1220 apply(auto) |
|
1221 apply(subst setsum_cut_off_le) |
|
1222 |
|
1223 |
|
1224 lemma |
|
1225 "Minr R x ys = (LEAST z. (R z ys \<or> z = Suc x))" |
|
1226 apply(simp add: Minr_def) |
|
1227 apply(rule Min_eqI) |
|
1228 apply(auto)[1] |
|
1229 apply(simp) |
|
1230 apply(rule Least_le) |
|
1231 apply(auto)[1] |
|
1232 apply(rule LeastI2_wellorder) |
|
1233 apply(auto) |
|
1234 done |
|
1235 |
|
1236 definition (in ord) |
|
1237 Great :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "GREAT " 10) where |
|
1238 "Great P = (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> y \<le> x))" |
|
1239 |
|
1240 (* |
|
1241 lemma Great_equality: |
|
1242 assumes "P x" |
|
1243 and "\<And>y. P y \<Longrightarrow> y \<le> x" |
|
1244 shows "Great P = x" |
|
1245 unfolding Great_def |
|
1246 apply(rule the_equality) |
|
1247 apply(blast intro: assms) |
|
1248 *) |
|
1249 |
|
1250 |
|
1251 |
|
1252 lemma |
|
1253 "Maxr R x ys = (GREAT z. (R z ys \<or> z = 0))" |
|
1254 apply(simp add: Maxr_def) |
|
1255 apply(rule Max_eqI) |
|
1256 apply(auto)[1] |
|
1257 apply(simp) |
|
1258 thm Least_le Greatest_le |
|
1259 oops |
|
1260 |
|
1261 lemma |
|
1262 "Maxr R x ys = x - Minr (\<lambda>z. R (x - z)) x ys" |
|
1263 apply(simp add: Maxr_def Minr_def) |
|
1264 apply(rule Max_eqI) |
|
1265 apply(auto)[1] |
|
1266 apply(simp) |
|
1267 apply(erule disjE) |
|
1268 apply(simp) |
|
1269 apply(auto)[1] |
|
1270 defer |
|
1271 apply(simp) |
|
1272 apply(auto)[1] |
|
1273 thm Min_insert |
|
1274 defer |
|
1275 oops |
|
1276 |
|
1277 |
|
1278 |
|
1279 definition quo :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
|
1280 where |
|
1281 "quo x y = (if y = 0 then 0 else x div y)" |
|
1282 |
|
1283 |
|
1284 definition |
|
1285 "rec_quo = CN rec_mult [CN rec_sign [Id 2 1], |
|
1286 CN (rec_minr2 (CN rec_less [Id 3 1, CN rec_mult [CN S [Id 3 0], Id 3 2]])) |
|
1287 [Id 2 0, Id 2 0, Id 2 1]]" |
|
1288 |
|
1289 lemma div_lemma [simp]: |
|
1290 "rec_eval rec_quo [x, y] = quo x y" |
|
1291 apply(simp add: rec_quo_def quo_def) |
|
1292 apply(rule impI) |
|
1293 apply(rule Min_eqI) |
|
1294 apply(auto)[1] |
|
1295 apply(simp) |
|
1296 apply(erule disjE) |
|
1297 apply(simp) |
|
1298 apply(auto)[1] |
|
1299 apply (metis div_le_dividend le_SucI) |
|
1300 defer |
|
1301 apply(simp) |
|
1302 apply(auto)[1] |
|
1303 apply (metis mult_Suc_right nat_mult_commute split_div_lemma) |
|
1304 apply(auto)[1] |
|
1305 |
|
1306 apply (smt div_le_dividend fst_divmod_nat) |
|
1307 apply(simp add: quo_def) |
|
1308 apply(auto)[1] |
|
1309 |
|
1310 apply(auto) |
|
1311 |
|
1312 fun Minr :: "(nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
|
1313 where "Minr R x y = (let setx = {z | z. z \<le> x \<and> R [z, y]} in |
|
1314 if (setx = {}) then (Suc x) else (Min setx))" |
|
1315 |
|
1316 definition |
|
1317 "rec_minr f = rec_sigma1 (rec_accum1 (CN rec_not [f]))" |
|
1318 |
|
1319 lemma minr_lemma [simp]: |
|
1320 shows "rec_eval (rec_minr f) [x, y] = Minr (\<lambda>xs. (0 < rec_eval f xs)) x y" |
|
1321 apply(simp only: rec_minr_def) |
|
1322 apply(simp only: sigma1_lemma) |
|
1323 apply(simp only: accum1_lemma) |
|
1324 apply(subst rec_eval.simps) |
|
1325 apply(simp only: map.simps nth) |
|
1326 apply(simp only: Minr.simps Let_def) |
|
1327 apply(auto simp del: not_lemma) |
|
1328 apply(simp) |
|
1329 apply(simp only: not_lemma sign_lemma) |
|
1330 apply(rule sym) |
|
1331 apply(rule Min_eqI) |
|
1332 apply(auto)[1] |
|
1333 apply(simp) |
|
1334 apply(subst setsum_cut_off_le[where m="ya"]) |
|
1335 apply(simp) |
|
1336 apply(simp) |
|
1337 apply(metis Icc_subset_Ici_iff atLeast_def in_mono le_refl mem_Collect_eq) |
|
1338 apply(rule setsum_one_less) |
|
1339 apply(default) |
|
1340 apply(rule impI) |
|
1341 apply(rule setprod_one_le) |
|
1342 apply(auto split: if_splits)[1] |
|
1343 apply(simp) |
|
1344 apply(rule conjI) |
|
1345 apply(subst setsum_cut_off_le[where m="xa"]) |
|
1346 apply(simp) |
|
1347 apply(simp) |
|
1348 apply (metis Icc_subset_Ici_iff atLeast_def in_mono le_refl mem_Collect_eq) |
|
1349 apply(rule le_trans) |
|
1350 apply(rule setsum_one_less) |
|
1351 apply(default) |
|
1352 apply(rule impI) |
|
1353 apply(rule setprod_one_le) |
|
1354 apply(auto split: if_splits)[1] |
|
1355 apply(simp) |
|
1356 apply(subgoal_tac "\<exists>l. l = (LEAST z. 0 < rec_eval f [z, y])") |
|
1357 defer |
|
1358 apply metis |
|
1359 apply(erule exE) |
|
1360 apply(subgoal_tac "l \<le> x") |
|
1361 defer |
|
1362 apply (metis not_leE not_less_Least order_trans) |
|
1363 apply(subst setsum_least_eq) |
|
1364 apply(rotate_tac 3) |
|
1365 apply(assumption) |
|
1366 prefer 3 |
|
1367 apply (metis LeastI_ex) |
|
1368 apply(auto)[1] |
|
1369 apply(subgoal_tac "a < (LEAST z. 0 < rec_eval f [z, y])") |
|
1370 prefer 2 |
|
1371 apply(auto)[1] |
|
1372 apply(rotate_tac 5) |
|
1373 apply(drule not_less_Least) |
|
1374 apply(auto)[1] |
|
1375 apply(auto) |
|
1376 by (metis (mono_tags) LeastI_ex) |
|
1377 |
|
1378 |
|
1379 fun Minr2 :: "(nat list \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
|
1380 where "Minr2 R x y = (let setx = {z | z. z \<le> x \<and> R [z, y]} in |
|
1381 Min (setx \<union> {Suc x}))" |
|
1382 |
|
1383 lemma Minr2_Minr: |
|
1384 "Minr2 R x y = Minr R x y" |
|
1385 apply(auto) |
|
1386 apply (metis (lifting, no_types) Min_singleton empty_Collect_eq) |
|
1387 apply(rule min_absorb2) |
|
1388 apply(subst Min_le_iff) |
|
1389 apply(auto) |
|
1390 done |
|
1391 *) |
|