more elementary rules about div / mod on int
authorhaftmann
Sat Dec 31 08:12:31 2016 +0100 (2016-12-31)
changeset 6471533d5fa0ce6e5
parent 64714 53bab28983f1
child 64716 473793d52d97
more elementary rules about div / mod on int
src/HOL/Divides.thy
src/HOL/Power.thy
     1.1 --- a/src/HOL/Divides.thy	Fri Dec 30 18:02:27 2016 +0100
     1.2 +++ b/src/HOL/Divides.thy	Sat Dec 31 08:12:31 2016 +0100
     1.3 @@ -1823,6 +1823,103 @@
     1.4    "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
     1.5    by auto
     1.6  
     1.7 +lemma zdiv_int:
     1.8 +  "int (a div b) = int a div int b"
     1.9 +  by (simp add: divide_int_def)
    1.10 +
    1.11 +lemma zmod_int:
    1.12 +  "int (a mod b) = int a mod int b"
    1.13 +  by (simp add: modulo_int_def int_dvd_iff)
    1.14 +
    1.15 +lemma div_abs_eq_div_nat:
    1.16 +  "\<bar>k\<bar> div \<bar>l\<bar> = int (nat \<bar>k\<bar> div nat \<bar>l\<bar>)"
    1.17 +  by (simp add: divide_int_def)
    1.18 +
    1.19 +lemma mod_abs_eq_div_nat:
    1.20 +  "\<bar>k\<bar> mod \<bar>l\<bar> = int (nat \<bar>k\<bar> mod nat \<bar>l\<bar>)"
    1.21 +  by (simp add: modulo_int_def dvd_int_unfold_dvd_nat)
    1.22 +
    1.23 +lemma div_sgn_abs_cancel:
    1.24 +  fixes k l v :: int
    1.25 +  assumes "v \<noteq> 0"
    1.26 +  shows "(sgn v * \<bar>k\<bar>) div (sgn v * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
    1.27 +proof -
    1.28 +  from assms have "sgn v = - 1 \<or> sgn v = 1"
    1.29 +    by (cases "v \<ge> 0") auto
    1.30 +  then show ?thesis
    1.31 +  using assms unfolding divide_int_def [of "sgn v * \<bar>k\<bar>" "sgn v * \<bar>l\<bar>"]
    1.32 +    by (auto simp add: not_less div_abs_eq_div_nat)
    1.33 +qed
    1.34 +
    1.35 +lemma div_eq_sgn_abs:
    1.36 +  fixes k l v :: int
    1.37 +  assumes "sgn k = sgn l"
    1.38 +  shows "k div l = \<bar>k\<bar> div \<bar>l\<bar>"
    1.39 +proof (cases "l = 0")
    1.40 +  case True
    1.41 +  then show ?thesis
    1.42 +    by simp
    1.43 +next
    1.44 +  case False
    1.45 +  with assms have "(sgn k * \<bar>k\<bar>) div (sgn l * \<bar>l\<bar>) = \<bar>k\<bar> div \<bar>l\<bar>"
    1.46 +    by (simp add: div_sgn_abs_cancel)
    1.47 +  then show ?thesis
    1.48 +    by (simp add: sgn_mult_abs)
    1.49 +qed
    1.50 +
    1.51 +lemma div_dvd_sgn_abs:
    1.52 +  fixes k l :: int
    1.53 +  assumes "l dvd k"
    1.54 +  shows "k div l = (sgn k * sgn l) * (\<bar>k\<bar> div \<bar>l\<bar>)"
    1.55 +proof (cases "k = 0")
    1.56 +  case True
    1.57 +  then show ?thesis
    1.58 +    by simp
    1.59 +next
    1.60 +  case False
    1.61 +  show ?thesis
    1.62 +  proof (cases "sgn l = sgn k")
    1.63 +    case True
    1.64 +    then show ?thesis
    1.65 +      by (simp add: div_eq_sgn_abs)
    1.66 +  next
    1.67 +    case False
    1.68 +    with \<open>k \<noteq> 0\<close> assms show ?thesis
    1.69 +      unfolding divide_int_def [of k l]
    1.70 +        by (auto simp add: zdiv_int)
    1.71 +  qed
    1.72 +qed
    1.73 +
    1.74 +lemma div_noneq_sgn_abs:
    1.75 +  fixes k l :: int
    1.76 +  assumes "l \<noteq> 0"
    1.77 +  assumes "sgn k \<noteq> sgn l"
    1.78 +  shows "k div l = - (\<bar>k\<bar> div \<bar>l\<bar>) - of_bool (\<not> l dvd k)"
    1.79 +  using assms
    1.80 +  by (simp only: divide_int_def [of k l], auto simp add: not_less zdiv_int)
    1.81 +  
    1.82 +lemma sgn_mod:
    1.83 +  fixes k l :: int
    1.84 +  assumes "l \<noteq> 0" "\<not> l dvd k"
    1.85 +  shows "sgn (k mod l) = sgn l"
    1.86 +proof -
    1.87 +  from \<open>\<not> l dvd k\<close>
    1.88 +  have "k mod l \<noteq> 0"
    1.89 +    by (simp add: dvd_eq_mod_eq_0)
    1.90 +  show ?thesis
    1.91 +    using \<open>l \<noteq> 0\<close> \<open>\<not> l dvd k\<close>
    1.92 +    unfolding modulo_int_def [of k l]
    1.93 +    by (auto simp add: sgn_1_pos sgn_1_neg mod_greater_zero_iff_not_dvd nat_dvd_iff not_less
    1.94 +      zless_nat_eq_int_zless [symmetric] elim: nonpos_int_cases)
    1.95 +qed
    1.96 +
    1.97 +lemma abs_mod_less:
    1.98 +  fixes k l :: int
    1.99 +  assumes "l \<noteq> 0"
   1.100 +  shows "\<bar>k mod l\<bar> < \<bar>l\<bar>"
   1.101 +  using assms unfolding modulo_int_def [of k l]
   1.102 +  by (auto simp add: not_less int_dvd_iff mod_greater_zero_iff_not_dvd elim: pos_int_cases neg_int_cases nonneg_int_cases nonpos_int_cases)
   1.103 +
   1.104  instance int :: ring_div
   1.105  proof
   1.106    fix k l s :: int
   1.107 @@ -1870,12 +1967,6 @@
   1.108  
   1.109  text\<open>Basic laws about division and remainder\<close>
   1.110  
   1.111 -lemma zdiv_int: "int (a div b) = int a div int b"
   1.112 -  by (simp add: divide_int_def)
   1.113 -
   1.114 -lemma zmod_int: "int (a mod b) = int a mod int b"
   1.115 -  by (simp add: modulo_int_def int_dvd_iff)
   1.116 -
   1.117  lemma pos_mod_conj: "(0::int) < b \<Longrightarrow> 0 \<le> a mod b \<and> a mod b < b"
   1.118    using eucl_rel_int [of a b]
   1.119    by (auto simp add: eucl_rel_int_iff prod_eq_iff)
     2.1 --- a/src/HOL/Power.thy	Fri Dec 30 18:02:27 2016 +0100
     2.2 +++ b/src/HOL/Power.thy	Sat Dec 31 08:12:31 2016 +0100
     2.3 @@ -582,10 +582,22 @@
     2.4  context linordered_idom
     2.5  begin
     2.6  
     2.7 -lemma power_abs: "\<bar>a ^ n\<bar> = \<bar>a\<bar> ^ n"
     2.8 -  by (induct n) (auto simp add: abs_mult)
     2.9 +lemma zero_le_power2 [simp]: "0 \<le> a\<^sup>2"
    2.10 +  by (simp add: power2_eq_square)
    2.11 +
    2.12 +lemma zero_less_power2 [simp]: "0 < a\<^sup>2 \<longleftrightarrow> a \<noteq> 0"
    2.13 +  by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
    2.14  
    2.15 -lemma abs_power_minus [simp]: "\<bar>(-a) ^ n\<bar> = \<bar>a ^ n\<bar>"
    2.16 +lemma power2_less_0 [simp]: "\<not> a\<^sup>2 < 0"
    2.17 +  by (force simp add: power2_eq_square mult_less_0_iff)
    2.18 +
    2.19 +lemma power_abs: "\<bar>a ^ n\<bar> = \<bar>a\<bar> ^ n" -- \<open>FIXME simp?\<close>
    2.20 +  by (induct n) (simp_all add: abs_mult)
    2.21 +
    2.22 +lemma power_sgn [simp]: "sgn (a ^ n) = sgn a ^ n"
    2.23 +  by (induct n) (simp_all add: sgn_mult)
    2.24 +    
    2.25 +lemma abs_power_minus [simp]: "\<bar>(- a) ^ n\<bar> = \<bar>a ^ n\<bar>"
    2.26    by (simp add: power_abs)
    2.27  
    2.28  lemma zero_less_power_abs_iff [simp]: "0 < \<bar>a\<bar> ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0"
    2.29 @@ -600,15 +612,6 @@
    2.30  lemma zero_le_power_abs [simp]: "0 \<le> \<bar>a\<bar> ^ n"
    2.31    by (rule zero_le_power [OF abs_ge_zero])
    2.32  
    2.33 -lemma zero_le_power2 [simp]: "0 \<le> a\<^sup>2"
    2.34 -  by (simp add: power2_eq_square)
    2.35 -
    2.36 -lemma zero_less_power2 [simp]: "0 < a\<^sup>2 \<longleftrightarrow> a \<noteq> 0"
    2.37 -  by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff)
    2.38 -
    2.39 -lemma power2_less_0 [simp]: "\<not> a\<^sup>2 < 0"
    2.40 -  by (force simp add: power2_eq_square mult_less_0_iff)
    2.41 -
    2.42  lemma power2_less_eq_zero_iff [simp]: "a\<^sup>2 \<le> 0 \<longleftrightarrow> a = 0"
    2.43    by (simp add: le_less)
    2.44  
    2.45 @@ -618,7 +621,7 @@
    2.46  lemma power2_abs [simp]: "\<bar>a\<bar>\<^sup>2 = a\<^sup>2"
    2.47    by (simp add: power2_eq_square)
    2.48  
    2.49 -lemma odd_power_less_zero: "a < 0 \<Longrightarrow> a ^ Suc (2*n) < 0"
    2.50 +lemma odd_power_less_zero: "a < 0 \<Longrightarrow> a ^ Suc (2 * n) < 0"
    2.51  proof (induct n)
    2.52    case 0
    2.53    then show ?case by simp
    2.54 @@ -630,11 +633,11 @@
    2.55      by (simp del: power_Suc add: Suc mult_less_0_iff mult_neg_neg)
    2.56  qed
    2.57  
    2.58 -lemma odd_0_le_power_imp_0_le: "0 \<le> a ^ Suc (2*n) \<Longrightarrow> 0 \<le> a"
    2.59 +lemma odd_0_le_power_imp_0_le: "0 \<le> a ^ Suc (2 * n) \<Longrightarrow> 0 \<le> a"
    2.60    using odd_power_less_zero [of a n]
    2.61    by (force simp add: linorder_not_less [symmetric])
    2.62  
    2.63 -lemma zero_le_even_power'[simp]: "0 \<le> a ^ (2*n)"
    2.64 +lemma zero_le_even_power'[simp]: "0 \<le> a ^ (2 * n)"
    2.65  proof (induct n)
    2.66    case 0
    2.67    show ?case by simp