src/HOL/Divides.thy
changeset 55172 92735f0d5302
parent 55085 0e8e4dc55866
child 55414 eab03e9cee8a
child 55439 db691cc79289
equal deleted inserted replaced
55171:dc7a6f6be01b 55172:92735f0d5302
  1961 
  1961 
  1962 lemmas negDivAlg_eqn_numeral [simp] =
  1962 lemmas negDivAlg_eqn_numeral [simp] =
  1963     negDivAlg_eqn [of "numeral v" "- numeral w", OF zero_less_numeral] for v w
  1963     negDivAlg_eqn [of "numeral v" "- numeral w", OF zero_less_numeral] for v w
  1964 
  1964 
  1965 
  1965 
  1966 text{*Special-case simplification *}
  1966 text {* Special-case simplification: @{text "\<plusminus>1 div z"} and @{text "\<plusminus>1 mod z"} *}
  1967 
  1967 
  1968 (** The last remaining special cases for constant arithmetic:
  1968 lemma [simp]:
  1969     1 div z and 1 mod z **)
  1969   shows div_one_bit0: "1 div numeral (Num.Bit0 v) = (0 :: int)"
  1970 
  1970     and mod_one_bit0: "1 mod numeral (Num.Bit0 v) = (1 :: int)"
  1971 lemmas div_pos_pos_1_numeral [simp] =
  1971 	  and div_one_bit1: "1 div numeral (Num.Bit1 v) = (0 :: int)"
  1972   div_pos_pos [OF zero_less_one, of "numeral w", OF zero_le_numeral] for w
  1972 	  and mod_one_bit1: "1 mod numeral (Num.Bit1 v) = (1 :: int)"
  1973 
  1973 	  and div_one_neg_numeral: "1 div - numeral v = (- 1 :: int)"
  1974 lemmas div_pos_neg_1_numeral [simp] =
  1974 	  and mod_one_neg_numeral: "1 mod - numeral v = (1 :: int) - numeral v"
  1975   div_pos_neg [OF zero_less_one, of "- numeral w",
  1975   by (simp_all del: arith_special
  1976   OF neg_numeral_less_zero] for w
  1976     add: div_pos_pos mod_pos_pos div_pos_neg mod_pos_neg posDivAlg_eqn)
  1977 
  1977 	
  1978 lemmas mod_pos_pos_1_numeral [simp] =
  1978 lemma [simp]:
  1979   mod_pos_pos [OF zero_less_one, of "numeral w", OF zero_le_numeral] for w
  1979   shows div_neg_one_numeral: "- 1 div numeral v = (- 1 :: int)"
  1980 
  1980     and mod_neg_one_numeral: "- 1 mod numeral v = numeral v - (1 :: int)"
  1981 lemmas mod_pos_neg_1_numeral [simp] =
  1981     and div_neg_one_neg_bit0: "- 1 div - numeral (Num.Bit0 v) = (0 :: int)"
  1982   mod_pos_neg [OF zero_less_one, of "- numeral w",
  1982     and mod_neg_one_neb_bit0: "- 1 mod - numeral (Num.Bit0 v) = (- 1 :: int)"
  1983   OF neg_numeral_less_zero] for w
  1983     and div_neg_one_neg_bit1: "- 1 div - numeral (Num.Bit1 v) = (0 :: int)"
  1984 
  1984     and mod_neg_one_neb_bit1: "- 1 mod - numeral (Num.Bit1 v) = (- 1 :: int)"
  1985 lemmas posDivAlg_eqn_1_numeral [simp] =
  1985   by (simp_all add: div_eq_minus1 zmod_minus1)
  1986     posDivAlg_eqn [of concl: 1 "numeral w", OF zero_less_numeral] for w
       
  1987 
       
  1988 lemmas negDivAlg_eqn_1_numeral [simp] =
       
  1989     negDivAlg_eqn [of concl: 1 "numeral w", OF zero_less_numeral] for w
       
  1990 
  1986 
  1991 
  1987 
  1992 subsubsection {* Monotonicity in the First Argument (Dividend) *}
  1988 subsubsection {* Monotonicity in the First Argument (Dividend) *}
  1993 
  1989 
  1994 lemma zdiv_mono1: "[| a \<le> a';  0 < (b::int) |] ==> a div b \<le> a' div b"
  1990 lemma zdiv_mono1: "[| a \<le> a';  0 < (b::int) |] ==> a div b \<le> a' div b"