# HG changeset patch
# User paulson
# Date 1118944264 -7200
# Node ID 47ffc49c7d7b62634caaec665246b6cca5a9245e
# Parent  50eab0183aea7151dbb9c6a17b8c90b73e24c759
a few new integer lemmas

diff -r 50eab0183aea -r 47ffc49c7d7b src/HOL/Integ/IntArith.thy
--- a/src/HOL/Integ/IntArith.thy	Thu Jun 16 18:25:54 2005 +0200
+++ b/src/HOL/Integ/IntArith.thy	Thu Jun 16 19:51:04 2005 +0200
@@ -13,6 +13,7 @@
 text{*Duplicate: can't understand why it's necessary*}
 declare numeral_0_eq_0 [simp]
 
+
 subsection{*Instantiating Binary Arithmetic for the Integers*}
 
 instance
@@ -174,6 +175,11 @@
 lemma nat_2: "nat 2 = Suc (Suc 0)"
 by (subst nat_eq_iff, simp)
 
+lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
+apply (insert zless_nat_conj [of 1 z])
+apply (auto simp add: nat_1)
+done
+
 text{*This simplifies expressions of the form @{term "int n = z"} where
       z is an integer literal.*}
 declare int_eq_iff [of _ "number_of v", standard, simp]
@@ -202,7 +208,7 @@
 lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'"
 apply (case_tac "0 \<le> z'")
 apply (rule inj_int [THEN injD])
-apply (simp add: zmult_int [symmetric] zero_le_mult_iff)
+apply (simp add: int_mult zero_le_mult_iff)
 apply (simp add: mult_le_0_iff)
 done
 
diff -r 50eab0183aea -r 47ffc49c7d7b src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Thu Jun 16 18:25:54 2005 +0200
+++ b/src/HOL/Integ/IntDef.thy	Thu Jun 16 19:51:04 2005 +0200
@@ -217,9 +217,12 @@
   zadd_zmult_distrib zadd_zmult_distrib2
   zdiff_zmult_distrib zdiff_zmult_distrib2
 
-lemma zmult_int: "(int m) * (int n) = int (m * n)"
+lemma int_mult: "int (m * n) = (int m) * (int n)"
 by (simp add: int_def mult)
 
+text{*Compatibility binding*}
+lemmas zmult_int = int_mult [symmetric]
+
 lemma zmult_1: "(1::int) * z = z"
 by (cases z, simp add: One_int_def int_def mult)
 
@@ -442,7 +445,6 @@
 lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
 by (insert zless_nat_conj [of 0], auto)
 
-
 lemma nat_add_distrib:
      "[| (0::int) \<le> z;  0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
 by (cases z, cases z', simp add: nat add le int_def Zero_int_def)
diff -r 50eab0183aea -r 47ffc49c7d7b src/HOL/Integ/IntDiv.thy
--- a/src/HOL/Integ/IntDiv.thy	Thu Jun 16 18:25:54 2005 +0200
+++ b/src/HOL/Integ/IntDiv.thy	Thu Jun 16 19:51:04 2005 +0200
@@ -582,7 +582,6 @@
 apply (erule subst, simp_all)
 done
 
-
 subsection{*More Algebraic Laws for div and mod*}
 
 text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *}
@@ -1112,11 +1111,11 @@
   apply (auto simp add: dvd_def nat_abs_mult_distrib)
   apply (auto simp add: nat_eq_iff abs_if split add: split_if_asm)
    apply (rule_tac x = "-(int k)" in exI)
-  apply (auto simp add: zmult_int [symmetric])
+  apply (auto simp add: int_mult)
   done
 
 lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
-  apply (auto simp add: dvd_def abs_if zmult_int [symmetric])
+  apply (auto simp add: dvd_def abs_if int_mult)
     apply (rule_tac [3] x = "nat k" in exI)
     apply (rule_tac [2] x = "-(int k)" in exI)
     apply (rule_tac x = "nat (-k)" in exI)
@@ -1127,7 +1126,7 @@
   done
 
 lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
-  apply (auto simp add: dvd_def zmult_int [symmetric])
+  apply (auto simp add: dvd_def int_mult)
   apply (rule_tac x = "nat k" in exI)
   apply (cut_tac k = m in int_less_0_conv)
   apply (auto simp add: zero_le_mult_iff mult_less_0_iff
@@ -1195,8 +1194,11 @@
 apply (auto simp add: zero_le_mult_iff)
 done
 
-theorem zpower_int: "(int m)^n = int (m^n)"
-  by (induct n) (simp_all add: zmult_int)
+lemma int_power: "int (m^n) = (int m) ^ n"
+  by (induct n, simp_all add: int_mult)
+
+text{*Compatibility binding*}
+lemmas zpower_int = int_power [symmetric]
 
 lemma zdiv_int: "int (a div b) = (int a) div (int b)"
 apply (subst split_div, auto)
@@ -1208,10 +1210,20 @@
 lemma zmod_int: "int (a mod b) = (int a) mod (int b)"
 apply (subst split_mod, auto)
 apply (subst split_zmod, auto)
-apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia in IntDiv.unique_remainder)
+apply (rule_tac a="int (b * i) + int j" and b="int b" and q="int i" and q'=ia 
+       in unique_remainder)
 apply (auto simp add: IntDiv.quorem_def int_eq_of_nat)
 done
 
+text{*Suggested by Matthias Daum*}
+lemma int_power_div_base:
+     "\<lbrakk>0 < m; 0 < k\<rbrakk> \<Longrightarrow> k ^ m div k = (k::int) ^ (m - Suc 0)"
+apply (subgoal_tac "k ^ m = k ^ ((m - 1) + 1)")
+ apply (erule ssubst)
+ apply (simp only: power_add)
+ apply simp_all
+done
+
 ML
 {*
 val quorem_def = thm "quorem_def";
diff -r 50eab0183aea -r 47ffc49c7d7b src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Thu Jun 16 18:25:54 2005 +0200
+++ b/src/HOL/Integ/NatBin.thy	Thu Jun 16 19:51:04 2005 +0200
@@ -76,6 +76,13 @@
 apply (simp add: nat_less_iff [symmetric] quorem_def nat_numeral_0_eq_0 zadd_int zmult_int)
 done
 
+text{*Suggested by Matthias Daum*}
+lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
+apply (subgoal_tac "nat x div nat k < nat x") 
+ apply (simp add: nat_div_distrib [symmetric])
+apply (rule Divides.div_less_dividend, simp_all) 
+done
+
 
 subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
 
diff -r 50eab0183aea -r 47ffc49c7d7b src/HOL/Integ/Parity.thy
--- a/src/HOL/Integ/Parity.thy	Thu Jun 16 18:25:54 2005 +0200
+++ b/src/HOL/Integ/Parity.thy	Thu Jun 16 19:51:04 2005 +0200
@@ -28,13 +28,6 @@
   even_nat_def: "even (x::nat) == even (int x)"
 
 
-subsection {* Casting a nat power to an integer *}
-
-lemma zpow_int: "int (x^y) = (int x)^y"
-  apply (induct y)
-  apply (simp, simp add: zmult_int [THEN sym])
-  done
-
 subsection {* Even and odd are mutually exclusive *}
 
 lemma int_pos_lt_two_imp_zero_or_one: 
@@ -143,7 +136,7 @@
   by (simp add: even_nat_def)
 
 lemma even_nat_product: "even((x::nat) * y) = (even x | even y)"
-  by (simp add: even_nat_def zmult_int [THEN sym])
+  by (simp add: even_nat_def int_mult)
 
 lemma even_nat_sum: "even ((x::nat) + y) = 
     ((even x & even y) | (odd x & odd y))"
@@ -163,7 +156,7 @@
 lemmas even_nat_suc = even_nat_Suc
 
 lemma even_nat_power: "even ((x::nat)^y) = (even x & 0 < y)"
-  by (simp add: even_nat_def zpow_int)
+  by (simp add: even_nat_def int_power)
 
 lemma even_nat_zero: "even (0::nat)"
   by (simp add: even_nat_def)