src/HOL/Int.thy
changeset 61649 268d88ec9087
parent 61609 77b453bd616f
child 61694 6571c78c9667
     1.1 --- a/src/HOL/Int.thy	Thu Nov 12 11:22:26 2015 +0100
     1.2 +++ b/src/HOL/Int.thy	Fri Nov 13 12:27:13 2015 +0000
     1.3 @@ -319,25 +319,25 @@
     1.4  text \<open>Comparisons involving @{term of_int}.\<close>
     1.5  
     1.6  lemma of_int_eq_numeral_iff [iff]:
     1.7 -   "of_int z = (numeral n :: 'a::ring_char_0) 
     1.8 +   "of_int z = (numeral n :: 'a::ring_char_0)
     1.9     \<longleftrightarrow> z = numeral n"
    1.10    using of_int_eq_iff by fastforce
    1.11  
    1.12 -lemma of_int_le_numeral_iff [simp]:           
    1.13 -   "of_int z \<le> (numeral n :: 'a::linordered_idom) 
    1.14 +lemma of_int_le_numeral_iff [simp]:
    1.15 +   "of_int z \<le> (numeral n :: 'a::linordered_idom)
    1.16     \<longleftrightarrow> z \<le> numeral n"
    1.17    using of_int_le_iff [of z "numeral n"] by simp
    1.18  
    1.19 -lemma of_int_numeral_le_iff [simp]:  
    1.20 +lemma of_int_numeral_le_iff [simp]:
    1.21     "(numeral n :: 'a::linordered_idom) \<le> of_int z \<longleftrightarrow> numeral n \<le> z"
    1.22    using of_int_le_iff [of "numeral n"] by simp
    1.23  
    1.24 -lemma of_int_less_numeral_iff [simp]:           
    1.25 -   "of_int z < (numeral n :: 'a::linordered_idom) 
    1.26 +lemma of_int_less_numeral_iff [simp]:
    1.27 +   "of_int z < (numeral n :: 'a::linordered_idom)
    1.28     \<longleftrightarrow> z < numeral n"
    1.29    using of_int_less_iff [of z "numeral n"] by simp
    1.30  
    1.31 -lemma of_int_numeral_less_iff [simp]:           
    1.32 +lemma of_int_numeral_less_iff [simp]:
    1.33     "(numeral n :: 'a::linordered_idom) < of_int z \<longleftrightarrow> numeral n < z"
    1.34    using of_int_less_iff [of "numeral n" z] by simp
    1.35  
    1.36 @@ -815,22 +815,22 @@
    1.37  
    1.38  subsection \<open>@{term setsum} and @{term setprod}\<close>
    1.39  
    1.40 -lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
    1.41 +lemma of_nat_setsum [simp]: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
    1.42    apply (cases "finite A")
    1.43    apply (erule finite_induct, auto)
    1.44    done
    1.45  
    1.46 -lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
    1.47 +lemma of_int_setsum [simp]: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
    1.48    apply (cases "finite A")
    1.49    apply (erule finite_induct, auto)
    1.50    done
    1.51  
    1.52 -lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
    1.53 +lemma of_nat_setprod [simp]: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
    1.54    apply (cases "finite A")
    1.55    apply (erule finite_induct, auto simp add: of_nat_mult)
    1.56    done
    1.57  
    1.58 -lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
    1.59 +lemma of_int_setprod [simp]: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
    1.60    apply (cases "finite A")
    1.61    apply (erule finite_induct, auto)
    1.62    done
    1.63 @@ -1401,7 +1401,7 @@
    1.64      then show "x dvd y"
    1.65      proof (cases k)
    1.66        case (nonneg n)
    1.67 -      with A have "y = x * n" by (simp add: of_nat_mult [symmetric])
    1.68 +      with A have "y = x * n" by (simp del: of_nat_mult add: of_nat_mult [symmetric])
    1.69        then show ?thesis ..
    1.70      next
    1.71        case (neg n)
    1.72 @@ -1695,16 +1695,6 @@
    1.73  lemmas zpower_numeral_even = power_numeral_even [where 'a=int]
    1.74  lemmas zpower_numeral_odd = power_numeral_odd [where 'a=int]
    1.75  
    1.76 -lemma zpower_zpower:
    1.77 -  "(x ^ y) ^ z = (x ^ (y * z)::int)"
    1.78 -  by (rule power_mult [symmetric])
    1.79 -
    1.80 -lemma int_power:
    1.81 -  "int (m ^ n) = int m ^ n"
    1.82 -  by (fact of_nat_power)
    1.83 -
    1.84 -lemmas zpower_int = int_power [symmetric]
    1.85 -
    1.86  text \<open>De-register @{text "int"} as a quotient type:\<close>
    1.87  
    1.88  lifting_update int.lifting