773 |
773 |
774 instance .. |
774 instance .. |
775 |
775 |
776 end |
776 end |
777 |
777 |
|
778 |
|
779 subsection \<open>More lemmas\<close> |
|
780 |
|
781 lemma twice_conv_BIT: "2 * x = x BIT False" |
|
782 by (rule bin_rl_eqI) (simp_all, simp_all add: bin_rest_def bin_last_def) |
|
783 |
|
784 lemma not_int_cmp_0 [simp]: |
|
785 fixes i :: int shows |
|
786 "0 < NOT i \<longleftrightarrow> i < -1" |
|
787 "0 \<le> NOT i \<longleftrightarrow> i < 0" |
|
788 "NOT i < 0 \<longleftrightarrow> i \<ge> 0" |
|
789 "NOT i \<le> 0 \<longleftrightarrow> i \<ge> -1" |
|
790 by(simp_all add: int_not_def) arith+ |
|
791 |
|
792 lemma bbw_ao_dist2: "(x :: int) AND (y OR z) = x AND y OR x AND z" |
|
793 by(metis int_and_comm bbw_ao_dist) |
|
794 |
|
795 lemmas int_and_ac = bbw_lcs(1) int_and_comm int_and_assoc |
|
796 |
|
797 lemma int_nand_same [simp]: fixes x :: int shows "x AND NOT x = 0" |
|
798 by(induct x y\<equiv>"NOT x" rule: bitAND_int.induct)(subst bitAND_int.simps, clarsimp) |
|
799 |
|
800 lemma int_nand_same_middle: fixes x :: int shows "x AND y AND NOT x = 0" |
|
801 by (metis bbw_lcs(1) int_and_0 int_nand_same) |
|
802 |
|
803 lemma and_xor_dist: fixes x :: int shows |
|
804 "x AND (y XOR z) = (x AND y) XOR (x AND z)" |
|
805 by(simp add: int_xor_def bbw_ao_dist2 bbw_ao_dist bbw_not_dist int_and_ac int_nand_same_middle) |
|
806 |
|
807 lemma BIT_lt0 [simp]: "x BIT b < 0 \<longleftrightarrow> x < 0" |
|
808 by(cases b)(auto simp add: Bit_def) |
|
809 |
|
810 lemma BIT_ge0 [simp]: "x BIT b \<ge> 0 \<longleftrightarrow> x \<ge> 0" |
|
811 by(cases b)(auto simp add: Bit_def) |
|
812 |
|
813 lemma [simp]: |
|
814 shows bin_rest_lt0: "bin_rest i < 0 \<longleftrightarrow> i < 0" |
|
815 and bin_rest_ge_0: "bin_rest i \<ge> 0 \<longleftrightarrow> i \<ge> 0" |
|
816 by(auto simp add: bin_rest_def) |
|
817 |
|
818 lemma bin_rest_gt_0 [simp]: "bin_rest x > 0 \<longleftrightarrow> x > 1" |
|
819 by(simp add: bin_rest_def add1_zle_eq pos_imp_zdiv_pos_iff) (metis add1_zle_eq one_add_one) |
|
820 |
|
821 lemma int_and_lt0 [simp]: fixes x y :: int shows |
|
822 "x AND y < 0 \<longleftrightarrow> x < 0 \<and> y < 0" |
|
823 by(induct x y rule: bitAND_int.induct)(subst bitAND_int.simps, simp) |
|
824 |
|
825 lemma int_and_ge0 [simp]: fixes x y :: int shows |
|
826 "x AND y \<ge> 0 \<longleftrightarrow> x \<ge> 0 \<or> y \<ge> 0" |
|
827 by (metis int_and_lt0 linorder_not_less) |
|
828 |
|
829 lemma int_and_1: fixes x :: int shows "x AND 1 = x mod 2" |
|
830 by(subst bitAND_int.simps)(simp add: Bit_def bin_last_def zmod_minus1) |
|
831 |
|
832 lemma int_1_and: fixes x :: int shows "1 AND x = x mod 2" |
|
833 by(subst int_and_comm)(simp add: int_and_1) |
|
834 |
|
835 lemma int_or_lt0 [simp]: fixes x y :: int shows |
|
836 "x OR y < 0 \<longleftrightarrow> x < 0 \<or> y < 0" |
|
837 by(simp add: int_or_def) |
|
838 |
|
839 lemma int_xor_lt0 [simp]: fixes x y :: int shows |
|
840 "x XOR y < 0 \<longleftrightarrow> ((x < 0) \<noteq> (y < 0))" |
|
841 by(auto simp add: int_xor_def) |
|
842 |
|
843 lemma int_xor_ge0 [simp]: fixes x y :: int shows |
|
844 "x XOR y \<ge> 0 \<longleftrightarrow> ((x \<ge> 0) \<longleftrightarrow> (y \<ge> 0))" |
|
845 by (metis int_xor_lt0 linorder_not_le) |
|
846 |
|
847 lemma bin_last_conv_AND: |
|
848 "bin_last i \<longleftrightarrow> i AND 1 \<noteq> 0" |
|
849 proof - |
|
850 obtain x b where "i = x BIT b" by(cases i rule: bin_exhaust) |
|
851 hence "i AND 1 = 0 BIT b" |
|
852 by(simp add: BIT_special_simps(2)[symmetric] del: BIT_special_simps(2)) |
|
853 thus ?thesis using \<open>i = x BIT b\<close> by(cases b) simp_all |
|
854 qed |
|
855 |
|
856 lemma bitval_bin_last: |
|
857 "of_bool (bin_last i) = i AND 1" |
|
858 proof - |
|
859 obtain x b where "i = x BIT b" by(cases i rule: bin_exhaust) |
|
860 hence "i AND 1 = 0 BIT b" |
|
861 by(simp add: BIT_special_simps(2)[symmetric] del: BIT_special_simps(2)) |
|
862 thus ?thesis by(cases b)(simp_all add: bin_last_conv_AND) |
|
863 qed |
|
864 |
|
865 lemma bl_to_bin_BIT: |
|
866 "bl_to_bin bs BIT b = bl_to_bin (bs @ [b])" |
|
867 by(simp add: bl_to_bin_append) |
|
868 |
|
869 lemma bin_last_bl_to_bin: "bin_last (bl_to_bin bs) \<longleftrightarrow> bs \<noteq> [] \<and> last bs" |
|
870 by(cases "bs = []")(auto simp add: bl_to_bin_def last_bin_last'[where w=0]) |
|
871 |
|
872 lemma bin_rest_bl_to_bin: "bin_rest (bl_to_bin bs) = bl_to_bin (butlast bs)" |
|
873 by(cases "bs = []")(simp_all add: bl_to_bin_def butlast_rest_bl2bin_aux) |
|
874 |
|
875 lemma bin_nth_numeral_unfold: |
|
876 "bin_nth (numeral (num.Bit0 x)) n \<longleftrightarrow> n > 0 \<and> bin_nth (numeral x) (n - 1)" |
|
877 "bin_nth (numeral (num.Bit1 x)) n \<longleftrightarrow> (n > 0 \<longrightarrow> bin_nth (numeral x) (n - 1))" |
|
878 by(case_tac [!] n) simp_all |
|
879 |
|
880 lemma bin_sign_and: |
|
881 "bin_sign (i AND j) = - (bin_sign i * bin_sign j)" |
|
882 by(simp add: bin_sign_def) |
|
883 |
|
884 lemma minus_BIT_0: fixes x y :: int shows "x BIT b - y BIT False = (x - y) BIT b" |
|
885 by(simp add: Bit_def) |
|
886 |
|
887 lemma int_not_neg_numeral: "NOT (- numeral n) = (Num.sub n num.One :: int)" |
|
888 by(simp add: int_not_def) |
|
889 |
|
890 lemma sub_inc_One: "Num.sub (Num.inc n) num.One = numeral n" |
|
891 by (metis add_diff_cancel diff_minus_eq_add diff_numeral_special(2) diff_numeral_special(6)) |
|
892 |
|
893 lemma inc_BitM: "Num.inc (Num.BitM n) = num.Bit0 n" |
|
894 by(simp add: BitM_plus_one[symmetric] add_One) |
|
895 |
|
896 lemma int_neg_numeral_pOne_conv_not: "- numeral (n + num.One) = (NOT (numeral n) :: int)" |
|
897 by(simp add: int_not_def) |
|
898 |
|
899 lemma int_lsb_BIT [simp]: fixes x :: int shows |
|
900 "lsb (x BIT b) \<longleftrightarrow> b" |
|
901 by(simp add: lsb_int_def) |
|
902 |
|
903 lemma bin_last_conv_lsb: "bin_last = lsb" |
|
904 by(clarsimp simp add: lsb_int_def fun_eq_iff) |
|
905 |
|
906 lemma int_lsb_numeral [simp]: |
|
907 "lsb (0 :: int) = False" |
|
908 "lsb (1 :: int) = True" |
|
909 "lsb (Numeral1 :: int) = True" |
|
910 "lsb (- 1 :: int) = True" |
|
911 "lsb (- Numeral1 :: int) = True" |
|
912 "lsb (numeral (num.Bit0 w) :: int) = False" |
|
913 "lsb (numeral (num.Bit1 w) :: int) = True" |
|
914 "lsb (- numeral (num.Bit0 w) :: int) = False" |
|
915 "lsb (- numeral (num.Bit1 w) :: int) = True" |
|
916 by(simp_all add: lsb_int_def) |
|
917 |
|
918 lemma int_set_bit_0 [simp]: fixes x :: int shows |
|
919 "set_bit x 0 b = bin_rest x BIT b" |
|
920 by(auto simp add: set_bit_int_def intro: bin_rl_eqI) |
|
921 |
|
922 lemma int_set_bit_Suc: fixes x :: int shows |
|
923 "set_bit x (Suc n) b = set_bit (bin_rest x) n b BIT bin_last x" |
|
924 by(auto simp add: set_bit_int_def twice_conv_BIT intro: bin_rl_eqI) |
|
925 |
|
926 lemma bin_last_set_bit: |
|
927 "bin_last (set_bit x n b) = (if n > 0 then bin_last x else b)" |
|
928 by(cases n)(simp_all add: int_set_bit_Suc) |
|
929 |
|
930 lemma bin_rest_set_bit: |
|
931 "bin_rest (set_bit x n b) = (if n > 0 then set_bit (bin_rest x) (n - 1) b else bin_rest x)" |
|
932 by(cases n)(simp_all add: int_set_bit_Suc) |
|
933 |
|
934 lemma int_set_bit_numeral: fixes x :: int shows |
|
935 "set_bit x (numeral w) b = set_bit (bin_rest x) (pred_numeral w) b BIT bin_last x" |
|
936 by(simp add: set_bit_int_def) |
|
937 |
|
938 lemmas int_set_bit_numerals [simp] = |
|
939 int_set_bit_numeral[where x="numeral w'"] |
|
940 int_set_bit_numeral[where x="- numeral w'"] |
|
941 int_set_bit_numeral[where x="Numeral1"] |
|
942 int_set_bit_numeral[where x="1"] |
|
943 int_set_bit_numeral[where x="0"] |
|
944 int_set_bit_Suc[where x="numeral w'"] |
|
945 int_set_bit_Suc[where x="- numeral w'"] |
|
946 int_set_bit_Suc[where x="Numeral1"] |
|
947 int_set_bit_Suc[where x="1"] |
|
948 int_set_bit_Suc[where x="0"] |
|
949 for w' |
|
950 |
|
951 lemma int_shiftl_BIT: fixes x :: int |
|
952 shows int_shiftl0 [simp]: "x << 0 = x" |
|
953 and int_shiftl_Suc [simp]: "x << Suc n = (x << n) BIT False" |
|
954 by(auto simp add: shiftl_int_def Bit_def) |
|
955 |
|
956 lemma int_0_shiftl [simp]: "0 << n = (0 :: int)" |
|
957 by(induct n) simp_all |
|
958 |
|
959 lemma bin_last_shiftl: "bin_last (x << n) \<longleftrightarrow> n = 0 \<and> bin_last x" |
|
960 by(cases n)(simp_all) |
|
961 |
|
962 lemma bin_rest_shiftl: "bin_rest (x << n) = (if n > 0 then x << (n - 1) else bin_rest x)" |
|
963 by(cases n)(simp_all) |
|
964 |
|
965 lemma bin_nth_shiftl [simp]: "bin_nth (x << n) m \<longleftrightarrow> n \<le> m \<and> bin_nth x (m - n)" |
|
966 proof(induct n arbitrary: x m) |
|
967 case (Suc n) |
|
968 thus ?case by(cases m) simp_all |
|
969 qed simp |
|
970 |
|
971 lemma int_shiftr_BIT [simp]: fixes x :: int |
|
972 shows int_shiftr0: "x >> 0 = x" |
|
973 and int_shiftr_Suc: "x BIT b >> Suc n = x >> n" |
|
974 proof - |
|
975 show "x >> 0 = x" by (simp add: shiftr_int_def) |
|
976 show "x BIT b >> Suc n = x >> n" by (cases b) |
|
977 (simp_all add: shiftr_int_def Bit_def add.commute pos_zdiv_mult_2) |
|
978 qed |
|
979 |
|
980 lemma bin_last_shiftr: "bin_last (x >> n) \<longleftrightarrow> x !! n" |
|
981 proof(induct n arbitrary: x) |
|
982 case 0 thus ?case by simp |
|
983 next |
|
984 case (Suc n) |
|
985 thus ?case by(cases x rule: bin_exhaust) simp |
|
986 qed |
|
987 |
|
988 lemma bin_rest_shiftr [simp]: "bin_rest (x >> n) = x >> Suc n" |
|
989 proof(induct n arbitrary: x) |
|
990 case 0 |
|
991 thus ?case by(cases x rule: bin_exhaust) auto |
|
992 next |
|
993 case (Suc n) |
|
994 thus ?case by(cases x rule: bin_exhaust) auto |
|
995 qed |
|
996 |
|
997 lemma bin_nth_shiftr [simp]: "bin_nth (x >> n) m = bin_nth x (n + m)" |
|
998 proof(induct n arbitrary: x m) |
|
999 case (Suc n) |
|
1000 thus ?case by(cases x rule: bin_exhaust) simp_all |
|
1001 qed simp |
|
1002 |
|
1003 lemma bin_nth_conv_AND: |
|
1004 fixes x :: int shows |
|
1005 "bin_nth x n \<longleftrightarrow> x AND (1 << n) \<noteq> 0" |
|
1006 proof(induct n arbitrary: x) |
|
1007 case 0 |
|
1008 thus ?case by(simp add: int_and_1 bin_last_def) |
|
1009 next |
|
1010 case (Suc n) |
|
1011 thus ?case by(cases x rule: bin_exhaust)(simp_all add: bin_nth_ops Bit_eq_0_iff) |
|
1012 qed |
|
1013 |
|
1014 lemma int_shiftl_numeral [simp]: |
|
1015 "(numeral w :: int) << numeral w' = numeral (num.Bit0 w) << pred_numeral w'" |
|
1016 "(- numeral w :: int) << numeral w' = - numeral (num.Bit0 w) << pred_numeral w'" |
|
1017 by(simp_all add: numeral_eq_Suc Bit_def shiftl_int_def) |
|
1018 (metis add_One mult_inc semiring_norm(11) semiring_norm(13) semiring_norm(2) semiring_norm(6) semiring_norm(87))+ |
|
1019 |
|
1020 lemma int_shiftl_One_numeral [simp]: "(1 :: int) << numeral w = 2 << pred_numeral w" |
|
1021 by(metis int_shiftl_numeral numeral_One) |
|
1022 |
|
1023 lemma shiftl_ge_0 [simp]: fixes i :: int shows "i << n \<ge> 0 \<longleftrightarrow> i \<ge> 0" |
|
1024 by(induct n) simp_all |
|
1025 |
|
1026 lemma shiftl_lt_0 [simp]: fixes i :: int shows "i << n < 0 \<longleftrightarrow> i < 0" |
|
1027 by (metis not_le shiftl_ge_0) |
|
1028 |
|
1029 lemma int_shiftl_test_bit: "(n << i :: int) !! m \<longleftrightarrow> m \<ge> i \<and> n !! (m - i)" |
|
1030 proof(induction i) |
|
1031 case (Suc n) |
|
1032 thus ?case by(cases m) simp_all |
|
1033 qed simp |
|
1034 |
|
1035 lemma int_0shiftr [simp]: "(0 :: int) >> x = 0" |
|
1036 by(simp add: shiftr_int_def) |
|
1037 |
|
1038 lemma int_minus1_shiftr [simp]: "(-1 :: int) >> x = -1" |
|
1039 by(simp add: shiftr_int_def div_eq_minus1) |
|
1040 |
|
1041 lemma int_shiftr_ge_0 [simp]: fixes i :: int shows "i >> n \<ge> 0 \<longleftrightarrow> i \<ge> 0" |
|
1042 proof(induct n arbitrary: i) |
|
1043 case (Suc n) |
|
1044 thus ?case by(cases i rule: bin_exhaust) simp_all |
|
1045 qed simp |
|
1046 |
|
1047 lemma int_shiftr_lt_0 [simp]: fixes i :: int shows "i >> n < 0 \<longleftrightarrow> i < 0" |
|
1048 by (metis int_shiftr_ge_0 not_less) |
|
1049 |
|
1050 lemma uminus_Bit_eq: |
|
1051 "- k BIT b = (- k - of_bool b) BIT b" |
|
1052 by (cases b) (simp_all add: Bit_def) |
|
1053 |
|
1054 lemma int_shiftr_numeral [simp]: |
|
1055 "(1 :: int) >> numeral w' = 0" |
|
1056 "(numeral num.One :: int) >> numeral w' = 0" |
|
1057 "(numeral (num.Bit0 w) :: int) >> numeral w' = numeral w >> pred_numeral w'" |
|
1058 "(numeral (num.Bit1 w) :: int) >> numeral w' = numeral w >> pred_numeral w'" |
|
1059 "(- numeral (num.Bit0 w) :: int) >> numeral w' = - numeral w >> pred_numeral w'" |
|
1060 "(- numeral (num.Bit1 w) :: int) >> numeral w' = - numeral (Num.inc w) >> pred_numeral w'" |
|
1061 by (simp_all only: numeral_One expand_BIT numeral_eq_Suc int_shiftr_Suc BIT_special_simps(2)[symmetric] int_0shiftr add_One uminus_Bit_eq) |
|
1062 (simp_all add: add_One) |
|
1063 |
|
1064 lemma int_shiftr_numeral_Suc0 [simp]: |
|
1065 "(1 :: int) >> Suc 0 = 0" |
|
1066 "(numeral num.One :: int) >> Suc 0 = 0" |
|
1067 "(numeral (num.Bit0 w) :: int) >> Suc 0 = numeral w" |
|
1068 "(numeral (num.Bit1 w) :: int) >> Suc 0 = numeral w" |
|
1069 "(- numeral (num.Bit0 w) :: int) >> Suc 0 = - numeral w" |
|
1070 "(- numeral (num.Bit1 w) :: int) >> Suc 0 = - numeral (Num.inc w)" |
|
1071 by(simp_all only: One_nat_def[symmetric] numeral_One[symmetric] int_shiftr_numeral pred_numeral_simps int_shiftr0) |
|
1072 |
|
1073 lemma bin_nth_minus_p2: |
|
1074 assumes sign: "bin_sign x = 0" |
|
1075 and y: "y = 1 << n" |
|
1076 and m: "m < n" |
|
1077 and x: "x < y" |
|
1078 shows "bin_nth (x - y) m = bin_nth x m" |
|
1079 using sign m x unfolding y |
|
1080 proof(induction m arbitrary: x y n) |
|
1081 case 0 |
|
1082 thus ?case |
|
1083 by(simp add: bin_last_def shiftl_int_def) (metis (hide_lams, no_types) mod_diff_right_eq mod_self neq0_conv numeral_One power_eq_0_iff power_mod diff_zero zero_neq_numeral) |
|
1084 next |
|
1085 case (Suc m) |
|
1086 from \<open>Suc m < n\<close> obtain n' where [simp]: "n = Suc n'" by(cases n) auto |
|
1087 obtain x' b where [simp]: "x = x' BIT b" by(cases x rule: bin_exhaust) |
|
1088 from \<open>bin_sign x = 0\<close> have "bin_sign x' = 0" by simp |
|
1089 moreover from \<open>x < 1 << n\<close> have "x' < 1 << n'" |
|
1090 by(cases b)(simp_all add: Bit_def shiftl_int_def) |
|
1091 moreover have "(2 * x' + of_bool b - 2 * 2 ^ n') div 2 = x' + (- (2 ^ n') + of_bool b div 2)" |
|
1092 by(simp only: add_diff_eq[symmetric] add.commute div_mult_self2[OF zero_neq_numeral[symmetric]]) |
|
1093 ultimately show ?case using Suc.IH[of x' n'] Suc.prems |
|
1094 by(cases b)(simp_all add: Bit_def bin_rest_def shiftl_int_def) |
|
1095 qed |
|
1096 |
|
1097 lemma bin_clr_conv_NAND: |
|
1098 "bin_sc n False i = i AND NOT (1 << n)" |
|
1099 by(induct n arbitrary: i)(auto intro: bin_rl_eqI) |
|
1100 |
|
1101 lemma bin_set_conv_OR: |
|
1102 "bin_sc n True i = i OR (1 << n)" |
|
1103 by(induct n arbitrary: i)(auto intro: bin_rl_eqI) |
|
1104 |
|
1105 lemma int_set_bits_K_True [simp]: "(BITS _. True) = (-1 :: int)" |
|
1106 by(auto simp add: set_bits_int_def bin_last_bl_to_bin) |
|
1107 |
|
1108 lemma int_set_bits_K_False [simp]: "(BITS _. False) = (0 :: int)" |
|
1109 by(auto simp add: set_bits_int_def) |
|
1110 |
|
1111 lemma msb_conv_bin_sign: "msb x \<longleftrightarrow> bin_sign x = -1" |
|
1112 by(simp add: bin_sign_def not_le msb_int_def) |
|
1113 |
|
1114 lemma msb_BIT [simp]: "msb (x BIT b) = msb x" |
|
1115 by(simp add: msb_int_def) |
|
1116 |
|
1117 lemma msb_bin_rest [simp]: "msb (bin_rest x) = msb x" |
|
1118 by(simp add: msb_int_def) |
|
1119 |
|
1120 lemma int_msb_and [simp]: "msb ((x :: int) AND y) \<longleftrightarrow> msb x \<and> msb y" |
|
1121 by(simp add: msb_int_def) |
|
1122 |
|
1123 lemma int_msb_or [simp]: "msb ((x :: int) OR y) \<longleftrightarrow> msb x \<or> msb y" |
|
1124 by(simp add: msb_int_def) |
|
1125 |
|
1126 lemma int_msb_xor [simp]: "msb ((x :: int) XOR y) \<longleftrightarrow> msb x \<noteq> msb y" |
|
1127 by(simp add: msb_int_def) |
|
1128 |
|
1129 lemma int_msb_not [simp]: "msb (NOT (x :: int)) \<longleftrightarrow> \<not> msb x" |
|
1130 by(simp add: msb_int_def not_less) |
|
1131 |
|
1132 lemma msb_shiftl [simp]: "msb ((x :: int) << n) \<longleftrightarrow> msb x" |
|
1133 by(simp add: msb_int_def) |
|
1134 |
|
1135 lemma msb_shiftr [simp]: "msb ((x :: int) >> r) \<longleftrightarrow> msb x" |
|
1136 by(simp add: msb_int_def) |
|
1137 |
|
1138 lemma msb_bin_sc [simp]: "msb (bin_sc n b x) \<longleftrightarrow> msb x" |
|
1139 by(simp add: msb_conv_bin_sign) |
|
1140 |
|
1141 lemma msb_set_bit [simp]: "msb (set_bit (x :: int) n b) \<longleftrightarrow> msb x" |
|
1142 by(simp add: msb_conv_bin_sign set_bit_int_def) |
|
1143 |
|
1144 lemma msb_0 [simp]: "msb (0 :: int) = False" |
|
1145 by(simp add: msb_int_def) |
|
1146 |
|
1147 lemma msb_1 [simp]: "msb (1 :: int) = False" |
|
1148 by(simp add: msb_int_def) |
|
1149 |
|
1150 lemma msb_numeral [simp]: |
|
1151 "msb (numeral n :: int) = False" |
|
1152 "msb (- numeral n :: int) = True" |
|
1153 by(simp_all add: msb_int_def) |
|
1154 |
778 end |
1155 end |