a few new integer lemmas
authorpaulson
Thu Jun 16 19:51:04 2005 +0200 (2005-06-16)
changeset 1641347ffc49c7d7b
parent 16412 50eab0183aea
child 16414 cad2cf55c851
a few new integer lemmas
src/HOL/Integ/IntArith.thy
src/HOL/Integ/IntDef.thy
src/HOL/Integ/IntDiv.thy
src/HOL/Integ/NatBin.thy
src/HOL/Integ/Parity.thy
     1.1 --- a/src/HOL/Integ/IntArith.thy	Thu Jun 16 18:25:54 2005 +0200
     1.2 +++ b/src/HOL/Integ/IntArith.thy	Thu Jun 16 19:51:04 2005 +0200
     1.3 @@ -13,6 +13,7 @@
     1.4  text{*Duplicate: can't understand why it's necessary*}
     1.5  declare numeral_0_eq_0 [simp]
     1.6  
     1.7 +
     1.8  subsection{*Instantiating Binary Arithmetic for the Integers*}
     1.9  
    1.10  instance
    1.11 @@ -174,6 +175,11 @@
    1.12  lemma nat_2: "nat 2 = Suc (Suc 0)"
    1.13  by (subst nat_eq_iff, simp)
    1.14  
    1.15 +lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
    1.16 +apply (insert zless_nat_conj [of 1 z])
    1.17 +apply (auto simp add: nat_1)
    1.18 +done
    1.19 +
    1.20  text{*This simplifies expressions of the form @{term "int n = z"} where
    1.21        z is an integer literal.*}
    1.22  declare int_eq_iff [of _ "number_of v", standard, simp]
    1.23 @@ -202,7 +208,7 @@
    1.24  lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'"
    1.25  apply (case_tac "0 \<le> z'")
    1.26  apply (rule inj_int [THEN injD])
    1.27 -apply (simp add: zmult_int [symmetric] zero_le_mult_iff)
    1.28 +apply (simp add: int_mult zero_le_mult_iff)
    1.29  apply (simp add: mult_le_0_iff)
    1.30  done
    1.31  
     2.1 --- a/src/HOL/Integ/IntDef.thy	Thu Jun 16 18:25:54 2005 +0200
     2.2 +++ b/src/HOL/Integ/IntDef.thy	Thu Jun 16 19:51:04 2005 +0200
     2.3 @@ -217,9 +217,12 @@
     2.4    zadd_zmult_distrib zadd_zmult_distrib2
     2.5    zdiff_zmult_distrib zdiff_zmult_distrib2
     2.6  
     2.7 -lemma zmult_int: "(int m) * (int n) = int (m * n)"
     2.8 +lemma int_mult: "int (m * n) = (int m) * (int n)"
     2.9  by (simp add: int_def mult)
    2.10  
    2.11 +text{*Compatibility binding*}
    2.12 +lemmas zmult_int = int_mult [symmetric]
    2.13 +
    2.14  lemma zmult_1: "(1::int) * z = z"
    2.15  by (cases z, simp add: One_int_def int_def mult)
    2.16  
    2.17 @@ -442,7 +445,6 @@
    2.18  lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
    2.19  by (insert zless_nat_conj [of 0], auto)
    2.20  
    2.21 -
    2.22  lemma nat_add_distrib:
    2.23       "[| (0::int) \<le> z;  0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
    2.24  by (cases z, cases z', simp add: nat add le int_def Zero_int_def)
     3.1 --- a/src/HOL/Integ/IntDiv.thy	Thu Jun 16 18:25:54 2005 +0200
     3.2 +++ b/src/HOL/Integ/IntDiv.thy	Thu Jun 16 19:51:04 2005 +0200
     3.3 @@ -582,7 +582,6 @@
     3.4  apply (erule subst, simp_all)
     3.5  done
     3.6  
     3.7 -
     3.8  subsection{*More Algebraic Laws for div and mod*}
     3.9  
    3.10  text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *}
    3.11 @@ -1112,11 +1111,11 @@
    3.12    apply (auto simp add: dvd_def nat_abs_mult_distrib)
    3.13    apply (auto simp add: nat_eq_iff abs_if split add: split_if_asm)
    3.14     apply (rule_tac x = "-(int k)" in exI)
    3.15 -  apply (auto simp add: zmult_int [symmetric])
    3.16 +  apply (auto simp add: int_mult)
    3.17    done
    3.18  
    3.19  lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
    3.20 -  apply (auto simp add: dvd_def abs_if zmult_int [symmetric])
    3.21 +  apply (auto simp add: dvd_def abs_if int_mult)
    3.22      apply (rule_tac [3] x = "nat k" in exI)
    3.23      apply (rule_tac [2] x = "-(int k)" in exI)
    3.24      apply (rule_tac x = "nat (-k)" in exI)
    3.25 @@ -1127,7 +1126,7 @@
    3.26    done
    3.27  
    3.28  lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
    3.29 -  apply (auto simp add: dvd_def zmult_int [symmetric])
    3.30 +  apply (auto simp add: dvd_def int_mult)
    3.31    apply (rule_tac x = "nat k" in exI)
    3.32    apply (cut_tac k = m in int_less_0_conv)
    3.33    apply (auto simp add: zero_le_mult_iff mult_less_0_iff
    3.34 @@ -1195,8 +1194,11 @@
    3.35  apply (auto simp add: zero_le_mult_iff)
    3.36  done
    3.37  
    3.38 -theorem zpower_int: "(int m)^n = int (m^n)"
    3.39 -  by (induct n) (simp_all add: zmult_int)
    3.40 +lemma int_power: "int (m^n) = (int m) ^ n"
    3.41 +  by (induct n, simp_all add: int_mult)
    3.42 +
    3.43 +text{*Compatibility binding*}
    3.44 +lemmas zpower_int = int_power [symmetric]
    3.45  
    3.46  lemma zdiv_int: "int (a div b) = (int a) div (int b)"
    3.47  apply (subst split_div, auto)
    3.48 @@ -1208,10 +1210,20 @@
    3.49  lemma zmod_int: "int (a mod b) = (int a) mod (int b)"
    3.50  apply (subst split_mod, auto)
    3.51  apply (subst split_zmod, auto)
    3.52 -apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia in IntDiv.unique_remainder)
    3.53 +apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia 
    3.54 +       in unique_remainder)
    3.55  apply (auto simp add: IntDiv.quorem_def int_eq_of_nat)
    3.56  done
    3.57  
    3.58 +text{*Suggested by Matthias Daum*}
    3.59 +lemma int_power_div_base:
    3.60 +     "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"
    3.61 +apply (subgoal_tac "k ^ m = k ^ ((m - 1) + 1)")
    3.62 + apply (erule ssubst)
    3.63 + apply (simp only: power_add)
    3.64 + apply simp_all
    3.65 +done
    3.66 +
    3.67  ML
    3.68  {*
    3.69  val quorem_def = thm "quorem_def";
     4.1 --- a/src/HOL/Integ/NatBin.thy	Thu Jun 16 18:25:54 2005 +0200
     4.2 +++ b/src/HOL/Integ/NatBin.thy	Thu Jun 16 19:51:04 2005 +0200
     4.3 @@ -76,6 +76,13 @@
     4.4  apply (simp add: nat_less_iff [symmetric] quorem_def nat_numeral_0_eq_0 zadd_int zmult_int)
     4.5  done
     4.6  
     4.7 +text{*Suggested by Matthias Daum*}
     4.8 +lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
     4.9 +apply (subgoal_tac "nat x div nat k < nat x") 
    4.10 + apply (simp add: nat_div_distrib [symmetric])
    4.11 +apply (rule Divides.div_less_dividend, simp_all) 
    4.12 +done
    4.13 +
    4.14  
    4.15  subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
    4.16  
     5.1 --- a/src/HOL/Integ/Parity.thy	Thu Jun 16 18:25:54 2005 +0200
     5.2 +++ b/src/HOL/Integ/Parity.thy	Thu Jun 16 19:51:04 2005 +0200
     5.3 @@ -28,13 +28,6 @@
     5.4    even_nat_def: "even (x::nat) == even (int x)"
     5.5  
     5.6  
     5.7 -subsection {* Casting a nat power to an integer *}
     5.8 -
     5.9 -lemma zpow_int: "int (x^y) = (int x)^y"
    5.10 -  apply (induct y)
    5.11 -  apply (simp, simp add: zmult_int [THEN sym])
    5.12 -  done
    5.13 -
    5.14  subsection {* Even and odd are mutually exclusive *}
    5.15  
    5.16  lemma int_pos_lt_two_imp_zero_or_one: 
    5.17 @@ -143,7 +136,7 @@
    5.18    by (simp add: even_nat_def)
    5.19  
    5.20  lemma even_nat_product: "even((x::nat) * y) = (even x | even y)"
    5.21 -  by (simp add: even_nat_def zmult_int [THEN sym])
    5.22 +  by (simp add: even_nat_def int_mult)
    5.23  
    5.24  lemma even_nat_sum: "even ((x::nat) + y) = 
    5.25      ((even x & even y) | (odd x & odd y))"
    5.26 @@ -163,7 +156,7 @@
    5.27  lemmas even_nat_suc = even_nat_Suc
    5.28  
    5.29  lemma even_nat_power: "even ((x::nat)^y) = (even x & 0 < y)"
    5.30 -  by (simp add: even_nat_def zpow_int)
    5.31 +  by (simp add: even_nat_def int_power)
    5.32  
    5.33  lemma even_nat_zero: "even (0::nat)"
    5.34    by (simp add: even_nat_def)