author paulson Thu, 16 Jun 2005 19:51:04 +0200 changeset 16413 47ffc49c7d7b parent 16412 50eab0183aea child 16414 cad2cf55c851
a few new integer lemmas
 src/HOL/Integ/IntArith.thy file | annotate | diff | comparison | revisions src/HOL/Integ/IntDef.thy file | annotate | diff | comparison | revisions src/HOL/Integ/IntDiv.thy file | annotate | diff | comparison | revisions src/HOL/Integ/NatBin.thy file | annotate | diff | comparison | revisions src/HOL/Integ/Parity.thy file | annotate | diff | comparison | revisions
```--- 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])
+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)
done
```
```--- 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 @@
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)"

+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)

-
"[| (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)```
```--- 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 (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 @@
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_all
+done
+
ML
{*
val quorem_def = thm "quorem_def";```
```--- 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 @@
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}*}
```
```--- 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 @@

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)"