--- a/src/HOL/IntDef.thy Mon Jun 11 02:25:55 2007 +0200
+++ b/src/HOL/IntDef.thy Mon Jun 11 05:20:05 2007 +0200
@@ -416,7 +416,7 @@
lemma nat_zminus_int_of_nat [simp]: "nat (- (int_of_nat n)) = 0"
by (simp add: int_of_nat_def minus nat Zero_int_def)
-lemma zless_nat_eq_int_zless: "(m < nat z) = (int_of_nat m < z)"
+lemma zless_nat_eq_int_zless': "(m < nat z) = (int_of_nat m < z)"
by (cases z, simp add: nat less int_of_nat_def, arith)
@@ -779,7 +779,7 @@
apply (rule_tac x="y - Suc x" in exI, arith)
done
-theorem int_cases':
+theorem int_cases' [case_names nonneg neg]:
"[|!! n. z = int_of_nat n ==> P; !! n. z = - (int_of_nat (Suc n)) ==> P |] ==> P"
apply (cases "z < 0", blast dest!: negD')
apply (simp add: linorder_not_less del: of_nat_Suc)
@@ -954,37 +954,30 @@
qed
lemma of_int_int_eq [simp]: "of_int (int n) = of_nat n"
-by (simp add: int_eq_of_nat)
+unfolding int_eq_of_nat by (rule of_int_of_nat_eq)
lemma int_setsum: "int (setsum f A) = (\<Sum>x\<in>A. int(f x))"
- by (simp add: int_eq_of_nat of_nat_setsum)
+unfolding int_eq_of_nat by (rule of_nat_setsum)
lemma int_setprod: "int (setprod f A) = (\<Prod>x\<in>A. int(f x))"
- by (simp add: int_eq_of_nat of_nat_setprod)
+unfolding int_eq_of_nat by (rule of_nat_setprod)
text{*Now we replace the case analysis rule by a more conventional one:
whether an integer is negative or not.*}
lemma zless_iff_Suc_zadd:
"(w < z) = (\<exists>n. z = w + int(Suc n))"
-apply (cases z, cases w)
-apply (auto simp add: le add int_def linorder_not_le [symmetric])
-apply (rename_tac a b c d)
-apply (rule_tac x="a+d - Suc(c+b)" in exI)
-apply arith
-done
+unfolding int_eq_of_nat by (rule zless_iff_Suc_zadd')
lemma negD: "x<0 ==> \<exists>n. x = - (int (Suc n))"
-apply (cases x)
-apply (auto simp add: le minus Zero_int_def int_def order_less_le)
-apply (rule_tac x="y - Suc x" in exI, arith)
-done
+unfolding int_eq_of_nat by (rule negD')
theorem int_cases [cases type: int, case_names nonneg neg]:
"[|!! n. z = int n ==> P; !! n. z = - (int (Suc n)) ==> P |] ==> P"
-apply (cases "z < 0", blast dest!: negD)
+unfolding int_eq_of_nat
+apply (cases "z < 0", blast dest!: negD')
apply (simp add: linorder_not_less)
-apply (blast dest: nat_0_le [THEN sym])
+apply (blast dest: nat_0_le' [THEN sym])
done
theorem int_induct [induct type: int, case_names nonneg neg]:
--- a/src/HOL/IntDiv.thy Mon Jun 11 02:25:55 2007 +0200
+++ b/src/HOL/IntDiv.thy Mon Jun 11 05:20:05 2007 +0200
@@ -1327,10 +1327,10 @@
done
lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
- apply (rule_tac z=n in int_cases)
- apply (auto simp add: dvd_int_iff)
- apply (rule_tac z=z in int_cases)
- apply (auto simp add: dvd_imp_le)
+ apply (rule_tac z=n in int_cases')
+ apply (auto simp add: dvd_int_of_nat_iff)
+ apply (rule_tac z=z in int_cases')
+ apply (auto simp add: dvd_imp_le)
done
--- a/src/HOL/NatBin.thy Mon Jun 11 02:25:55 2007 +0200
+++ b/src/HOL/NatBin.thy Mon Jun 11 05:20:05 2007 +0200
@@ -58,29 +58,32 @@
apply (case_tac "0 <= z'")
apply (auto simp add: div_nonneg_neg_le0 DIVISION_BY_ZERO_DIV)
apply (case_tac "z' = 0", simp add: DIVISION_BY_ZERO)
-apply (auto elim!: nonneg_eq_int)
+apply (auto elim!: nonneg_eq_int_of_nat)
apply (rename_tac m m')
-apply (subgoal_tac "0 <= int m div int m'")
+apply (subgoal_tac "0 <= int_of_nat m div int_of_nat m'")
prefer 2 apply (simp add: nat_numeral_0_eq_0 pos_imp_zdiv_nonneg_iff)
-apply (rule inj_int [THEN injD], simp)
-apply (rule_tac r = "int (m mod m') " in quorem_div)
+apply (rule of_nat_eq_iff [where 'a=int, THEN iffD1], simp)
+apply (rule_tac r = "int_of_nat (m mod m') " in quorem_div)
prefer 2 apply force
-apply (simp add: nat_less_iff [symmetric] quorem_def nat_numeral_0_eq_0 zadd_int
- zmult_int)
+apply (simp add: nat_less_iff' [symmetric] quorem_def nat_numeral_0_eq_0
+ of_nat_add [symmetric] of_nat_mult [symmetric]
+ del: of_nat_add of_nat_mult)
done
(*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*)
lemma nat_mod_distrib:
"[| (0::int) <= z; 0 <= z' |] ==> nat (z mod z') = nat z mod nat z'"
apply (case_tac "z' = 0", simp add: DIVISION_BY_ZERO)
-apply (auto elim!: nonneg_eq_int)
+apply (auto elim!: nonneg_eq_int_of_nat)
apply (rename_tac m m')
-apply (subgoal_tac "0 <= int m mod int m'")
+apply (subgoal_tac "0 <= int_of_nat m mod int_of_nat m'")
prefer 2 apply (simp add: nat_less_iff nat_numeral_0_eq_0 pos_mod_sign)
-apply (rule inj_int [THEN injD], simp)
-apply (rule_tac q = "int (m div m') " in quorem_mod)
+apply (rule of_nat_eq_iff [where 'a=int, THEN iffD1], simp)
+apply (rule_tac q = "int_of_nat (m div m') " in quorem_mod)
prefer 2 apply force
-apply (simp add: nat_less_iff [symmetric] quorem_def nat_numeral_0_eq_0 zadd_int zmult_int)
+apply (simp add: nat_less_iff' [symmetric] quorem_def nat_numeral_0_eq_0
+ of_nat_add [symmetric] of_nat_mult [symmetric]
+ del: of_nat_add of_nat_mult)
done
text{*Suggested by Matthias Daum*}
@@ -100,6 +103,13 @@
by (simp del: nat_number_of
add: neg_nat nat_number_of_def not_neg_nat add_assoc)
+lemma int_of_nat_number_of [simp]:
+ "int_of_nat (number_of v) =
+ (if neg (number_of v :: int) then 0
+ else (number_of v :: int))"
+by (simp del: nat_number_of
+ add: neg_nat nat_number_of_def not_neg_nat add_assoc)
+
subsubsection{*Successor *}
--- a/src/HOL/Numeral.thy Mon Jun 11 02:25:55 2007 +0200
+++ b/src/HOL/Numeral.thy Mon Jun 11 05:20:05 2007 +0200
@@ -457,14 +457,14 @@
lemma odd_less_0:
"(1 + z + z < 0) = (z < (0::int))";
-proof (cases z rule: int_cases)
+proof (cases z rule: int_cases')
case (nonneg n)
thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
le_imp_0_less [THEN order_less_imp_le])
next
case (neg n)
- thus ?thesis by (simp del: int_Suc
- add: int_Suc0_eq_1 [symmetric] zadd_int compare_rls)
+ thus ?thesis by (simp del: of_nat_Suc of_nat_add
+ add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric])
qed
text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}