src/HOL/Divides.thy
changeset 64238 b60a9752b6d0
parent 64164 38c407446400
child 64240 eabf80376aab
equal deleted inserted replaced
64237:c1b5165b73db 64238:b60a9752b6d0
  2217   assumes "0 \<le> b"
  2217   assumes "0 \<le> b"
  2218   assumes "divmod_int_rel a b (q, r)"
  2218   assumes "divmod_int_rel a b (q, r)"
  2219   shows "divmod_int_rel (1 + 2*a) (2*b) (q, 1 + 2*r)"
  2219   shows "divmod_int_rel (1 + 2*a) (2*b) (q, 1 + 2*r)"
  2220   using assms unfolding divmod_int_rel_def by auto
  2220   using assms unfolding divmod_int_rel_def by auto
  2221 
  2221 
  2222 declaration \<open>K (Lin_Arith.add_simps @{thms uminus_numeral_One})\<close>
       
  2223 
       
  2224 lemma neg_divmod_int_rel_mult_2:
  2222 lemma neg_divmod_int_rel_mult_2:
  2225   assumes "b \<le> 0"
  2223   assumes "b \<le> 0"
  2226   assumes "divmod_int_rel (a + 1) b (q, r)"
  2224   assumes "divmod_int_rel (a + 1) b (q, r)"
  2227   shows "divmod_int_rel (1 + 2*a) (2*b) (q, 2*r - 1)"
  2225   shows "divmod_int_rel (1 + 2*a) (2*b) (q, 2*r - 1)"
  2228   using assms unfolding divmod_int_rel_def by auto
  2226   using assms unfolding divmod_int_rel_def by auto