src/HOL/Divides.thy
changeset 55440 721b4561007a
parent 55414 eab03e9cee8a
parent 55439 db691cc79289
child 57492 74bf65a1910a
equal deleted inserted replaced
55428:0ab52bf7b5e6 55440:721b4561007a
  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)"