1966 text {* Special-case simplification: @{text "\<plusminus>1 div z"} and @{text "\<plusminus>1 mod z"} *} |
1966 text {* Special-case simplification: @{text "\<plusminus>1 div z"} and @{text "\<plusminus>1 mod z"} *} |
1967 |
1967 |
1968 lemma [simp]: |
1968 lemma [simp]: |
1969 shows div_one_bit0: "1 div numeral (Num.Bit0 v) = (0 :: int)" |
1969 shows div_one_bit0: "1 div numeral (Num.Bit0 v) = (0 :: int)" |
1970 and mod_one_bit0: "1 mod numeral (Num.Bit0 v) = (1 :: int)" |
1970 and mod_one_bit0: "1 mod numeral (Num.Bit0 v) = (1 :: int)" |
1971 and div_one_bit1: "1 div numeral (Num.Bit1 v) = (0 :: int)" |
1971 and div_one_bit1: "1 div numeral (Num.Bit1 v) = (0 :: int)" |
1972 and mod_one_bit1: "1 mod numeral (Num.Bit1 v) = (1 :: int)" |
1972 and mod_one_bit1: "1 mod numeral (Num.Bit1 v) = (1 :: int)" |
1973 and div_one_neg_numeral: "1 div - numeral v = (- 1 :: int)" |
1973 and div_one_neg_numeral: "1 div - numeral v = (- 1 :: int)" |
1974 and mod_one_neg_numeral: "1 mod - numeral v = (1 :: int) - numeral v" |
1974 and mod_one_neg_numeral: "1 mod - numeral v = (1 :: int) - numeral v" |
1975 by (simp_all del: arith_special |
1975 by (simp_all del: arith_special |
1976 add: div_pos_pos mod_pos_pos div_pos_neg mod_pos_neg posDivAlg_eqn) |
1976 add: div_pos_pos mod_pos_pos div_pos_neg mod_pos_neg posDivAlg_eqn) |
1977 |
1977 |
1978 lemma [simp]: |
1978 lemma [simp]: |
1979 shows div_neg_one_numeral: "- 1 div numeral v = (- 1 :: int)" |
1979 shows div_neg_one_numeral: "- 1 div numeral v = (- 1 :: int)" |
1980 and mod_neg_one_numeral: "- 1 mod numeral v = numeral v - (1 :: int)" |
1980 and mod_neg_one_numeral: "- 1 mod numeral v = numeral v - (1 :: int)" |
1981 and div_neg_one_neg_bit0: "- 1 div - numeral (Num.Bit0 v) = (0 :: int)" |
1981 and div_neg_one_neg_bit0: "- 1 div - numeral (Num.Bit0 v) = (0 :: int)" |
1982 and mod_neg_one_neb_bit0: "- 1 mod - numeral (Num.Bit0 v) = (- 1 :: int)" |
1982 and mod_neg_one_neb_bit0: "- 1 mod - numeral (Num.Bit0 v) = (- 1 :: int)" |