src/HOL/Int.thy
changeset 66816 212a3334e7da
parent 66035 de6cd60b1226
child 66836 4eb431c3f974
     1.1 --- a/src/HOL/Int.thy	Sun Oct 08 22:28:22 2017 +0200
     1.2 +++ b/src/HOL/Int.thy	Sun Oct 08 22:28:22 2017 +0200
     1.3 @@ -255,6 +255,10 @@
     1.4  lemma of_int_power [simp]: "of_int (z ^ n) = of_int z ^ n"
     1.5    by (induct n) simp_all
     1.6  
     1.7 +lemma of_int_of_bool [simp]:
     1.8 +  "of_int (of_bool P) = of_bool P"
     1.9 +  by auto
    1.10 +
    1.11  end
    1.12  
    1.13  context ring_char_0
    1.14 @@ -548,6 +552,10 @@
    1.15  lemma diff_nat_numeral [simp]: "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
    1.16    by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
    1.17  
    1.18 +lemma nat_of_bool [simp]:
    1.19 +  "nat (of_bool P) = of_bool P"
    1.20 +  by auto
    1.21 +
    1.22  
    1.23  text \<open>For termination proofs:\<close>
    1.24  lemma measure_function_int[measure_function]: "is_measure (nat \<circ> abs)" ..
    1.25 @@ -668,6 +676,31 @@
    1.26    \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close>
    1.27    by (fact Let_neg_numeral) \<comment> \<open>FIXME drop\<close>
    1.28  
    1.29 +lemma sgn_mult_dvd_iff [simp]:
    1.30 +  "sgn r * l dvd k \<longleftrightarrow> l dvd k \<and> (r = 0 \<longrightarrow> k = 0)" for k l r :: int
    1.31 +  by (cases r rule: int_cases3) auto
    1.32 +
    1.33 +lemma mult_sgn_dvd_iff [simp]:
    1.34 +  "l * sgn r dvd k \<longleftrightarrow> l dvd k \<and> (r = 0 \<longrightarrow> k = 0)" for k l r :: int
    1.35 +  using sgn_mult_dvd_iff [of r l k] by (simp add: ac_simps)
    1.36 +
    1.37 +lemma dvd_sgn_mult_iff [simp]:
    1.38 +  "l dvd sgn r * k \<longleftrightarrow> l dvd k \<or> r = 0" for k l r :: int
    1.39 +  by (cases r rule: int_cases3) simp_all
    1.40 +
    1.41 +lemma dvd_mult_sgn_iff [simp]:
    1.42 +  "l dvd k * sgn r \<longleftrightarrow> l dvd k \<or> r = 0" for k l r :: int
    1.43 +  using dvd_sgn_mult_iff [of l r k] by (simp add: ac_simps)
    1.44 +
    1.45 +lemma int_sgnE:
    1.46 +  fixes k :: int
    1.47 +  obtains n and l where "k = sgn l * int n"
    1.48 +proof -
    1.49 +  have "k = sgn k * int (nat \<bar>k\<bar>)"
    1.50 +    by (simp add: sgn_mult_abs)
    1.51 +  then show ?thesis ..
    1.52 +qed
    1.53 +
    1.54  text \<open>Unfold \<open>min\<close> and \<open>max\<close> on numerals.\<close>
    1.55  
    1.56  lemmas max_number_of [simp] =
    1.57 @@ -1629,19 +1662,10 @@
    1.58    shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
    1.59      (is "?lhs \<longleftrightarrow> ?rhs")
    1.60  proof -
    1.61 -  from assms obtain k where "d = a * k" by (rule dvdE)
    1.62 -  show ?thesis
    1.63 -  proof
    1.64 -    assume ?lhs
    1.65 -    then obtain l where "x + t = a * l" by (rule dvdE)
    1.66 -    then have "x = a * l - t" by simp
    1.67 -    with \<open>d = a * k\<close> show ?rhs by simp
    1.68 -  next
    1.69 -    assume ?rhs
    1.70 -    then obtain l where "x + c * d + t = a * l" by (rule dvdE)
    1.71 -    then have "x = a * l - c * d - t" by simp
    1.72 -    with \<open>d = a * k\<close> show ?lhs by simp
    1.73 -  qed
    1.74 +  from assms have "a dvd (x + t) \<longleftrightarrow> a dvd ((x + t) + c * d)"
    1.75 +    by (simp add: dvd_add_left_iff)
    1.76 +  then show ?thesis
    1.77 +    by (simp add: ac_simps)
    1.78  qed
    1.79  
    1.80