removed constant int :: nat => int;
int is now an abbreviation for of_nat :: nat => int
--- a/src/HOL/IntArith.thy Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/IntArith.thy Wed Jun 13 03:31:11 2007 +0200
@@ -196,25 +196,6 @@
z is an integer literal.*}
lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v", standard]
-lemmas int_of_nat_eq_iff_number_of [simp] =
- int_of_nat_eq_iff [of _ "number_of v", standard]
-
-lemma split_nat':
- "P(nat(i::int)) = ((\<forall>n. i = int_of_nat n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
- (is "?P = (?L & ?R)")
-proof (cases "i < 0")
- case True thus ?thesis by simp
-next
- case False
- have "?P = ?L"
- proof
- assume ?P thus ?L using False by clarsimp
- next
- assume ?L thus ?P using False by simp
- qed
- with False show ?thesis by simp
-qed
-
lemma split_nat [arith_split]:
"P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
(is "?P = (?L & ?R)")
@@ -232,10 +213,6 @@
qed
-(*Analogous to zadd_int*)
-lemma zdiff_int: "n \<le> m ==> int m - int n = int (m-n)"
-by (induct m n rule: diff_induct, simp_all)
-
lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'"
apply (cases "0 \<le> z'")
apply (rule inj_int [THEN injD])
--- a/src/HOL/IntDef.thy Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/IntDef.thy Wed Jun 13 03:31:11 2007 +0200
@@ -219,9 +219,12 @@
qed
abbreviation
- int_of_nat :: "nat \<Rightarrow> int"
+ int :: "nat \<Rightarrow> int"
where
- "int_of_nat \<equiv> of_nat"
+ "int \<equiv> of_nat"
+
+lemma int_def: "int m = Abs_Integ (intrel `` {(m, 0)})"
+by (induct m, simp_all add: Zero_int_def One_int_def add)
subsection{*The @{text "\<le>"} Ordering*}
@@ -294,18 +297,15 @@
apply (simp_all add: add_strict_mono)
done
-lemma int_of_nat_def: "of_nat m = Abs_Integ (intrel `` {(m, 0)})"
-by (induct m, simp_all add: Zero_int_def One_int_def add)
-
lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = of_nat n"
apply (cases k)
-apply (auto simp add: le add int_of_nat_def Zero_int_def)
+apply (auto simp add: le add int_def Zero_int_def)
apply (rule_tac x="x-y" in exI, simp)
done
lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = of_nat n"
apply (cases k)
-apply (simp add: less int_of_nat_def Zero_int_def)
+apply (simp add: less int_def Zero_int_def)
apply (rule_tac x="x-y" in exI, simp)
done
@@ -352,16 +352,16 @@
by (simp add: nat_def UN_equiv_class [OF equiv_intrel])
qed
-lemma nat_int_of_nat [simp]: "nat (int_of_nat n) = n"
-by (simp add: nat int_of_nat_def)
+lemma nat_int [simp]: "nat (int n) = n"
+by (simp add: nat int_def)
lemma nat_zero [simp]: "nat 0 = 0"
by (simp add: Zero_int_def nat)
-lemma int_of_nat_nat_eq [simp]: "int_of_nat (nat z) = (if 0 \<le> z then z else 0)"
-by (cases z, simp add: nat le int_of_nat_def Zero_int_def)
+lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
+by (cases z, simp add: nat le int_def Zero_int_def)
-corollary nat_0_le': "0 \<le> z ==> int_of_nat (nat z) = z"
+corollary nat_0_le: "0 \<le> z ==> int (nat z) = z"
by simp
lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
@@ -379,27 +379,27 @@
corollary nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
by (simp add: nat_le_eq_zle linorder_not_le [symmetric])
-lemma zless_nat_conj: "(nat w < nat z) = (0 < z & w < z)"
+lemma zless_nat_conj [simp]: "(nat w < nat z) = (0 < z & w < z)"
apply (cases w, cases z)
apply (simp add: nat le Zero_int_def linorder_not_le [symmetric], arith)
done
-lemma nonneg_eq_int_of_nat: "[| 0 \<le> z; !!m. z = int_of_nat m ==> P |] ==> P"
-by (blast dest: nat_0_le' sym)
+lemma nonneg_eq_int: "[| 0 \<le> z; !!m. z = int m ==> P |] ==> P"
+by (blast dest: nat_0_le sym)
-lemma nat_eq_iff': "(nat w = m) = (if 0 \<le> w then w = int_of_nat m else m=0)"
-by (cases w, simp add: nat le int_of_nat_def Zero_int_def, arith)
+lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"
+by (cases w, simp add: nat le int_def Zero_int_def, arith)
-corollary nat_eq_iff2': "(m = nat w) = (if 0 \<le> w then w = int_of_nat m else m=0)"
-by (simp only: eq_commute [of m] nat_eq_iff')
+corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"
+by (simp only: eq_commute [of m] nat_eq_iff)
-lemma nat_less_iff': "0 \<le> w ==> (nat w < m) = (w < int_of_nat m)"
+lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < int m)"
apply (cases w)
-apply (simp add: nat le int_of_nat_def Zero_int_def linorder_not_le [symmetric], arith)
+apply (simp add: nat le int_def Zero_int_def linorder_not_le [symmetric], arith)
done
-lemma int_of_nat_eq_iff: "(int_of_nat m = z) = (m = nat z & 0 \<le> z)"
-by (auto simp add: nat_eq_iff2')
+lemma int_eq_iff: "(int m = z) = (m = nat z & 0 \<le> z)"
+by (auto simp add: nat_eq_iff2)
lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
by (insert zless_nat_conj [of 0], auto)
@@ -413,42 +413,41 @@
by (cases z, cases z',
simp add: nat add minus diff_minus le Zero_int_def)
-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 nat_zminus_int [simp]: "nat (- (int n)) = 0"
+by (simp add: int_def minus nat Zero_int_def)
-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)
+lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
+by (cases z, simp add: nat less int_def, arith)
subsection{*Lemmas about the Function @{term int} and Orderings*}
-lemma negative_zless_0': "- (int_of_nat (Suc n)) < 0"
+lemma negative_zless_0: "- (int (Suc n)) < 0"
by (simp add: order_less_le del: of_nat_Suc)
-lemma negative_zless' [iff]: "- (int_of_nat (Suc n)) < int_of_nat m"
-by (rule negative_zless_0' [THEN order_less_le_trans], simp)
+lemma negative_zless [iff]: "- (int (Suc n)) < int m"
+by (rule negative_zless_0 [THEN order_less_le_trans], simp)
-lemma negative_zle_0': "- int_of_nat n \<le> 0"
+lemma negative_zle_0: "- int n \<le> 0"
by (simp add: minus_le_iff)
-lemma negative_zle' [iff]: "- int_of_nat n \<le> int_of_nat m"
-by (rule order_trans [OF negative_zle_0' of_nat_0_le_iff])
+lemma negative_zle [iff]: "- int n \<le> int m"
+by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff])
-lemma not_zle_0_negative' [simp]: "~ (0 \<le> - (int_of_nat (Suc n)))"
+lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))"
by (subst le_minus_iff, simp del: of_nat_Suc)
-lemma int_zle_neg': "(int_of_nat n \<le> - int_of_nat m) = (n = 0 & m = 0)"
-by (simp add: int_of_nat_def le minus Zero_int_def)
+lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
+by (simp add: int_def le minus Zero_int_def)
-lemma not_int_zless_negative' [simp]: "~ (int_of_nat n < - int_of_nat m)"
+lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
by (simp add: linorder_not_less)
-lemma negative_eq_positive' [simp]:
- "(- int_of_nat n = int_of_nat m) = (n = 0 & m = 0)"
-by (force simp add: order_eq_iff [of "- int_of_nat n"] int_zle_neg')
+lemma negative_eq_positive [simp]: "(- int n = int m) = (n = 0 & m = 0)"
+by (force simp add: order_eq_iff [of "- int n"] int_zle_neg)
-lemma zle_iff_zadd': "(w \<le> z) = (\<exists>n. z = w + int_of_nat n)"
-proof (cases w, cases z, simp add: le add int_of_nat_def)
+lemma zle_iff_zadd: "(w \<le> z) = (\<exists>n. z = w + int n)"
+proof (cases w, cases z, simp add: le add int_def)
fix a b c d
assume "w = Abs_Integ (intrel `` {(a,b)})" "z = Abs_Integ (intrel `` {(c,d)})"
show "(a+d \<le> c+b) = (\<exists>n. c+b = a+n+d)"
@@ -487,10 +486,10 @@
where
"iszero z \<longleftrightarrow> z = 0"
-lemma not_neg_int_of_nat [simp]: "~ neg (int_of_nat n)"
+lemma not_neg_int [simp]: "~ neg (int n)"
by (simp add: neg_def)
-lemma neg_zminus_int_of_nat [simp]: "neg (- (int_of_nat (Suc n)))"
+lemma neg_zminus_int [simp]: "neg (- (int (Suc n)))"
by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc)
lemmas neg_eq_less_0 = neg_def
@@ -516,7 +515,7 @@
lemma neg_nat: "neg z ==> nat z = 0"
by (simp add: neg_def order_less_imp_le)
-lemma not_neg_nat': "~ neg z ==> int_of_nat (nat z) = z"
+lemma not_neg_nat: "~ neg z ==> int (nat z) = z"
by (simp add: linorder_not_less neg_def)
@@ -645,7 +644,7 @@
fix z
show "of_int z = id z"
by (cases z)
- (simp add: of_int add minus int_of_nat_def diff_minus)
+ (simp add: of_int add minus int_def diff_minus)
qed
@@ -764,245 +763,80 @@
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_of_nat (Suc n))"
+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_of_nat_def linorder_not_le [symmetric])
+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
-lemma negD': "x<0 ==> \<exists>n. x = - (int_of_nat (Suc n))"
+lemma negD: "x<0 ==> \<exists>n. x = - (int (Suc n))"
apply (cases x)
-apply (auto simp add: le minus Zero_int_def int_of_nat_def order_less_le)
+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
-theorem int_cases' [cases type: int, 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')
+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)
apply (simp add: linorder_not_less del: of_nat_Suc)
-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]:
- "[|!! n. P (int_of_nat n); !!n. P (- (int_of_nat (Suc n))) |] ==> P z"
- by (cases z rule: int_cases') auto
+theorem int_induct'[induct type: int, case_names nonneg neg]:
+ "[|!! n. P (int n); !!n. P (- (int (Suc n))) |] ==> P z"
+ by (cases z rule: int_cases) auto
text{*Contributed by Brian Huffman*}
-theorem int_diff_cases' [case_names diff]:
-assumes prem: "!!m n. z = int_of_nat m - int_of_nat n ==> P" shows "P"
+theorem int_diff_cases [case_names diff]:
+assumes prem: "!!m n. z = int m - int n ==> P" shows "P"
apply (cases z rule: eq_Abs_Integ)
apply (rule_tac m=x and n=y in prem)
-apply (simp add: int_of_nat_def diff_def minus add)
+apply (simp add: int_def diff_def minus add)
done
lemma of_nat_nat: "0 \<le> z ==> of_nat (nat z) = of_int z"
by (cases z rule: eq_Abs_Integ, simp add: nat le of_int Zero_int_def)
-lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq]
-
-subsection{*@{term int}: Embedding the Naturals into the Integers*}
-
-definition
- int :: "nat \<Rightarrow> int"
-where
- [code func del]: "int m = Abs_Integ (intrel `` {(m, 0)})"
-
-text{*Agreement with the specific embedding for the integers*}
-lemma int_eq_of_nat: "int = (of_nat :: nat => int)"
-by (simp add: expand_fun_eq int_of_nat_def int_def)
-
-lemma inj_int: "inj int"
-by (simp add: inj_on_def int_def)
-
-lemma int_int_eq [iff]: "(int m = int n) = (m = n)"
-unfolding int_eq_of_nat by (rule of_nat_eq_iff)
-
-lemma zadd_int: "(int m) + (int n) = int (m + n)"
-unfolding int_eq_of_nat by (rule of_nat_add [symmetric])
+subsection {* Legacy theorems *}
lemma zadd_int_left: "(int m) + (int n + z) = int (m + n) + z"
-unfolding int_eq_of_nat by simp
-
-lemma int_mult: "int (m * n) = (int m) * (int n)"
-unfolding int_eq_of_nat by (rule of_nat_mult)
-
-text{*Compatibility binding*}
-lemmas zmult_int = int_mult [symmetric]
-
-lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)"
-unfolding int_eq_of_nat by (rule of_nat_eq_0_iff)
-
-lemma zless_int [simp]: "(int m < int n) = (m<n)"
-unfolding int_eq_of_nat by (rule of_nat_less_iff)
-
-lemma int_less_0_conv [simp]: "~ (int k < 0)"
-unfolding int_eq_of_nat by (rule of_nat_less_0_iff)
-
-lemma zero_less_int_conv [simp]: "(0 < int n) = (0 < n)"
-unfolding int_eq_of_nat by (rule of_nat_0_less_iff)
-
-lemma zle_int [simp]: "(int m \<le> int n) = (m\<le>n)"
-unfolding int_eq_of_nat by (rule of_nat_le_iff)
-
-lemma zero_zle_int [simp]: "(0 \<le> int n)"
-unfolding int_eq_of_nat by (rule of_nat_0_le_iff)
-
-lemma int_le_0_conv [simp]: "(int n \<le> 0) = (n = 0)"
-unfolding int_eq_of_nat by (rule of_nat_le_0_iff)
-
-lemma int_0 [simp]: "int 0 = (0::int)"
-unfolding int_eq_of_nat by (rule of_nat_0)
-
-lemma int_1 [simp]: "int 1 = 1"
-unfolding int_eq_of_nat by (rule of_nat_1)
-
-lemma int_Suc0_eq_1: "int (Suc 0) = 1"
-unfolding int_eq_of_nat by simp
+by simp
lemma int_Suc: "int (Suc m) = 1 + (int m)"
-unfolding int_eq_of_nat by simp
-
-lemma nat_int [simp]: "nat(int n) = n"
-unfolding int_eq_of_nat by (rule nat_int_of_nat)
-
-lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
-unfolding int_eq_of_nat by (rule int_of_nat_nat_eq)
-
-corollary nat_0_le: "0 \<le> z ==> int (nat z) = z"
-unfolding int_eq_of_nat by (rule nat_0_le')
-
-lemma nonneg_eq_int: "[| 0 \<le> z; !!m. z = int m ==> P |] ==> P"
-unfolding int_eq_of_nat by (blast elim: nonneg_eq_int_of_nat)
-
-lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"
-unfolding int_eq_of_nat by (rule nat_eq_iff')
-
-corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"
-unfolding int_eq_of_nat by (rule nat_eq_iff2')
-
-lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < int m)"
-unfolding int_eq_of_nat by (rule nat_less_iff')
-
-lemma int_eq_iff: "(int m = z) = (m = nat z & 0 \<le> z)"
-unfolding int_eq_of_nat by (rule int_of_nat_eq_iff)
-
-lemma nat_zminus_int [simp]: "nat (- (int n)) = 0"
-unfolding int_eq_of_nat by (rule nat_zminus_int_of_nat)
-
-lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
-unfolding int_eq_of_nat by (rule zless_nat_eq_int_zless')
+by simp
-lemma negative_zless_0: "- (int (Suc n)) < 0"
-unfolding int_eq_of_nat by (rule negative_zless_0')
-
-lemma negative_zless [iff]: "- (int (Suc n)) < int m"
-unfolding int_eq_of_nat by (rule negative_zless')
-
-lemma negative_zle_0: "- int n \<le> 0"
-unfolding int_eq_of_nat by (rule negative_zle_0')
-
-lemma negative_zle [iff]: "- int n \<le> int m"
-unfolding int_eq_of_nat by (rule negative_zle')
-
-lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))"
-unfolding int_eq_of_nat by (rule not_zle_0_negative')
-
-lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
-unfolding int_eq_of_nat by (rule int_zle_neg')
-
-lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
-unfolding int_eq_of_nat by (rule not_int_zless_negative')
-
-lemma negative_eq_positive [simp]: "(- int n = int m) = (n = 0 & m = 0)"
-unfolding int_eq_of_nat by (rule negative_eq_positive')
-
-lemma zle_iff_zadd: "(w \<le> z) = (\<exists>n. z = w + int n)"
-unfolding int_eq_of_nat by (rule zle_iff_zadd')
-
-lemma abs_int_eq [simp]: "abs (int m) = int m"
-unfolding int_eq_of_nat by (rule abs_of_nat)
-
-lemma not_neg_int [simp]: "~ neg(int n)"
-unfolding int_eq_of_nat by (rule not_neg_int_of_nat)
-
-lemma neg_zminus_int [simp]: "neg(- (int (Suc n)))"
-unfolding int_eq_of_nat by (rule neg_zminus_int_of_nat)
+lemma int_Suc0_eq_1: "int (Suc 0) = 1"
+by simp
-lemma not_neg_nat: "~ neg z ==> int (nat z) = z"
-unfolding int_eq_of_nat by (rule not_neg_nat')
-
-lemma of_int_int_eq [simp]: "of_int (int n) = of_nat n"
-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))"
-unfolding int_eq_of_nat by (rule of_nat_setsum)
-
-lemma int_setprod: "int (setprod f A) = (\<Prod>x\<in>A. int(f x))"
-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))"
-unfolding int_eq_of_nat by (rule zless_iff_Suc_zadd')
-
-lemma negD: "x<0 ==> \<exists>n. x = - (int (Suc n))"
-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"
-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])
-done
-
-theorem int_induct [induct type: int, case_names nonneg neg]:
- "[|!! n. P (int n); !!n. P (- (int (Suc n))) |] ==> P z"
- by (cases z) auto
+lemmas inj_int = inj_of_nat [where 'a=int]
+lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
+lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
+lemmas int_mult = of_nat_mult [where 'a=int]
+lemmas zmult_int = of_nat_mult [where 'a=int, symmetric]
+lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int]
+lemmas zless_int = of_nat_less_iff [where 'a=int]
+lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int]
+lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
+lemmas zle_int = of_nat_le_iff [where 'a=int]
+lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
+lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int]
+lemmas int_0 = of_nat_0 [where ?'a_1.0=int]
+lemmas int_1 = of_nat_1 [where 'a=int]
+lemmas abs_int_eq = abs_of_nat [where 'a=int]
+lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
+lemmas int_setsum = of_nat_setsum [where 'a=int]
+lemmas int_setprod = of_nat_setprod [where 'a=int]
+lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
+lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq]
+lemmas int_eq_of_nat = TrueI
-text{*Contributed by Brian Huffman*}
-theorem int_diff_cases [case_names diff]:
-assumes prem: "!!m n. z = int m - int n ==> P" shows "P"
- apply (rule_tac z=z in int_cases)
- apply (rule_tac m=n and n=0 in prem, simp)
- apply (rule_tac m=0 and n="Suc n" in prem, simp)
-done
-
-lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq]
-
-lemmas [simp] = int_Suc
-
-
-subsection {* Legacy ML bindings *}
-
-ML {*
-val of_nat_0 = @{thm of_nat_0};
-val of_nat_1 = @{thm of_nat_1};
-val of_nat_Suc = @{thm of_nat_Suc};
-val of_nat_add = @{thm of_nat_add};
-val of_nat_mult = @{thm of_nat_mult};
-val of_int_0 = @{thm of_int_0};
-val of_int_1 = @{thm of_int_1};
-val of_int_add = @{thm of_int_add};
-val of_int_mult = @{thm of_int_mult};
-val int_eq_of_nat = @{thm int_eq_of_nat};
-val zle_int = @{thm zle_int};
-val int_int_eq = @{thm int_int_eq};
-val diff_int_def = @{thm diff_int_def};
-val zadd_ac = @{thms zadd_ac};
-val zless_int = @{thm zless_int};
-val zadd_int = @{thm zadd_int};
-val zmult_int = @{thm zmult_int};
-val nat_0_le = @{thm nat_0_le};
-val int_0 = @{thm int_0};
-val int_1 = @{thm int_1};
-val abs_split = @{thm abs_split};
-*}
+abbreviation
+ int_of_nat :: "nat \<Rightarrow> int"
+where
+ "int_of_nat \<equiv> of_nat"
end
--- a/src/HOL/IntDiv.thy Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/IntDiv.thy Wed Jun 13 03:31:11 2007 +0200
@@ -11,8 +11,6 @@
imports IntArith Divides FunDef
begin
-declare zless_nat_conj [simp]
-
constdefs
quorem :: "(int*int) * (int*int) => bool"
--{*definition of quotient and remainder*}
@@ -266,7 +264,7 @@
val trans = trans;
val prove_eq_sums =
let
- val simps = diff_int_def :: Int_Numeral_Simprocs.add_0s @ zadd_ac
+ val simps = @{thm diff_int_def} :: Int_Numeral_Simprocs.add_0s @ @{thms zadd_ac}
in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end;
end)
@@ -1238,9 +1236,9 @@
apply simp
done
-theorem zdvd_int_of_nat: "(x dvd y) = (int_of_nat x dvd int_of_nat y)"
+theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
unfolding dvd_def
- apply (rule_tac s="\<exists>k. int_of_nat y = int_of_nat x * int_of_nat k" in trans)
+ apply (rule_tac s="\<exists>k. int y = int x * int k" in trans)
apply (simp only: of_nat_mult [symmetric] of_nat_eq_iff)
apply (simp add: ex_nat cong add: conj_cong)
apply (rule iffI)
@@ -1257,9 +1255,6 @@
apply (simp add: mult_ac)
done
-theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
- unfolding int_eq_of_nat by (rule zdvd_int_of_nat)
-
lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \<bar>x\<bar> = 1)"
proof
assume d: "x dvd 1" hence "int (nat \<bar>x\<bar>) dvd int (nat 1)" by (simp add: zdvd_abs1)
@@ -1280,40 +1275,31 @@
from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
qed
-lemma int_of_nat_dvd_iff: "(int_of_nat m dvd z) = (m dvd nat (abs z))"
+lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
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_of_nat k)" in exI)
+ apply (auto simp add: nat_eq_iff abs_if split add: split_if_asm)
+ apply (rule_tac x = "-(int k)" in exI)
apply auto
done
-lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
- unfolding int_eq_of_nat by (rule int_of_nat_dvd_iff)
-
-lemma dvd_int_of_nat_iff: "(z dvd int_of_nat m) = (nat (abs z) dvd m)"
+lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
apply (auto simp add: dvd_def abs_if)
apply (rule_tac [3] x = "nat k" in exI)
- apply (rule_tac [2] x = "-(int_of_nat k)" in exI)
+ apply (rule_tac [2] x = "-(int k)" in exI)
apply (rule_tac x = "nat (-k)" in exI)
- apply (cut_tac [3] m = m and 'a=int in of_nat_less_0_iff)
- apply (cut_tac m = m and 'a=int in of_nat_less_0_iff)
+ apply (cut_tac [3] m = m in int_less_0_conv)
+ apply (cut_tac m = m in int_less_0_conv)
apply (auto simp add: zero_le_mult_iff mult_less_0_iff
- nat_mult_distrib [symmetric] nat_eq_iff2')
- done
-
-lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
- unfolding int_eq_of_nat by (rule dvd_int_of_nat_iff)
-
-lemma nat_dvd_iff': "(nat z dvd m) = (if 0 \<le> z then (z dvd int_of_nat m) else m = 0)"
- apply (auto simp add: dvd_def)
- apply (rule_tac x = "nat k" in exI)
- apply (cut_tac m = m and 'a=int in of_nat_less_0_iff)
- apply (auto simp add: zero_le_mult_iff mult_less_0_iff
- nat_mult_distrib [symmetric] nat_eq_iff2')
+ nat_mult_distrib [symmetric] nat_eq_iff2)
done
lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)"
- unfolding int_eq_of_nat by (rule nat_dvd_iff')
+ apply (auto simp add: dvd_def)
+ apply (rule_tac x = "nat k" in exI)
+ apply (cut_tac m = m in int_less_0_conv)
+ apply (auto simp add: zero_le_mult_iff mult_less_0_iff
+ nat_mult_distrib [symmetric] nat_eq_iff2)
+ done
lemma zminus_dvd_iff [iff]: "(-z dvd w) = (z dvd (w::int))"
apply (auto simp add: dvd_def)
@@ -1327,9 +1313,9 @@
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_of_nat_iff)
- apply (rule_tac z=z in int_cases')
+ 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)
done
@@ -1377,33 +1363,25 @@
done
lemma int_power: "int (m^n) = (int m) ^ n"
- by (induct n, simp_all add: int_mult)
+ by (rule of_nat_power)
text{*Compatibility binding*}
lemmas zpower_int = int_power [symmetric]
-lemma int_of_nat_div:
- "int_of_nat (a div b) = (int_of_nat a) div (int_of_nat b)"
+lemma zdiv_int: "int (a div b) = (int a) div (int b)"
apply (subst split_div, auto)
apply (subst split_zdiv, auto)
-apply (rule_tac a="int_of_nat (b * i) + int_of_nat j" and b="int_of_nat b" and r="int_of_nat j" and r'=ja in IntDiv.unique_quotient)
-apply (auto simp add: IntDiv.quorem_def)
-done
-
-lemma zdiv_int: "int (a div b) = (int a) div (int b)"
- unfolding int_eq_of_nat by (rule int_of_nat_div)
-
-lemma int_of_nat_mod:
- "int_of_nat (a mod b) = (int_of_nat a) mod (int_of_nat b)"
-apply (subst split_mod, auto)
-apply (subst split_zmod, auto)
-apply (rule_tac a="int_of_nat (b * i) + int_of_nat j" and b="int_of_nat b" and q="int_of_nat i" and q'=ia
- in unique_remainder)
+apply (rule_tac a="int (b * i) + int j" and b="int b" and r="int j" and r'=ja in IntDiv.unique_quotient)
apply (auto simp add: IntDiv.quorem_def)
done
lemma zmod_int: "int (a mod b) = (int a) mod (int b)"
- unfolding int_eq_of_nat by (rule int_of_nat_mod)
+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 unique_remainder)
+apply (auto simp add: IntDiv.quorem_def)
+done
text{*Suggested by Matthias Daum*}
lemma int_power_div_base:
--- a/src/HOL/Library/EfficientNat.thy Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/Library/EfficientNat.thy Wed Jun 13 03:31:11 2007 +0200
@@ -31,6 +31,19 @@
nat_of_int :: "int \<Rightarrow> nat" where
"k \<ge> 0 \<Longrightarrow> nat_of_int k = nat k"
+definition
+ int' :: "nat \<Rightarrow> int" where
+ "int' n = of_nat n"
+
+lemma int'_Suc [simp]: "int' (Suc n) = 1 + int' n"
+unfolding int'_def by simp
+
+lemma int'_add: "int' (m + n) = int' m + int' n"
+unfolding int'_def by (rule of_nat_add)
+
+lemma int'_mult: "int' (m * n) = int' m * int' n"
+unfolding int'_def by (rule of_nat_mult)
+
lemma nat_of_int_of_number_of:
fixes k
assumes "k \<ge> 0"
@@ -44,8 +57,11 @@
using prems unfolding Pls_def by simp
lemma nat_of_int_int:
- "nat_of_int (int n) = n"
- using zero_zle_int nat_of_int_def by simp
+ "nat_of_int (int' n) = n"
+ using nat_of_int_def int'_def by simp
+
+lemma eq_nat_of_int: "int' n = x \<Longrightarrow> n = nat_of_int x"
+by (erule subst, simp only: nat_of_int_int)
text {*
Case analysis on natural numbers is rephrased using a conditional
@@ -66,10 +82,10 @@
qed
lemma [code inline]:
- "nat_case = (\<lambda>f g n. if n = 0 then f else g (nat_of_int (int n - 1)))"
+ "nat_case = (\<lambda>f g n. if n = 0 then f else g (nat_of_int (int' n - 1)))"
proof (rule ext)+
fix f g n
- show "nat_case f g n = (if n = 0 then f else g (nat_of_int (int n - 1)))"
+ show "nat_case f g n = (if n = 0 then f else g (nat_of_int (int' n - 1)))"
by (cases n) (simp_all add: nat_of_int_int)
qed
@@ -82,43 +98,33 @@
by (simp add: nat_of_int_def)
lemma [code func, code inline]: "1 = nat_of_int 1"
by (simp add: nat_of_int_def)
-lemma [code func]: "Suc n = nat_of_int (int n + 1)"
- by (simp add: nat_of_int_def)
-lemma [code]: "m + n = nat (int m + int n)"
- by arith
-lemma [code func, code inline]: "m + n = nat_of_int (int m + int n)"
- by (simp add: nat_of_int_def)
-lemma [code, code inline]: "m - n = nat (int m - int n)"
- by arith
-lemma [code]: "m * n = nat (int m * int n)"
- unfolding zmult_int by simp
-lemma [code func, code inline]: "m * n = nat_of_int (int m * int n)"
-proof -
- have "int (m * n) = int m * int n"
- by (induct m) (simp_all add: zadd_zmult_distrib)
- then have "m * n = nat (int m * int n)" by auto
- also have "\<dots> = nat_of_int (int m * int n)"
- proof -
- have "int m \<ge> 0" and "int n \<ge> 0" by auto
- have "int m * int n \<ge> 0" by (rule split_mult_pos_le) auto
- with nat_of_int_def show ?thesis by auto
- qed
- finally show ?thesis .
-qed
-lemma [code]: "m div n = nat (int m div int n)"
- unfolding zdiv_int [symmetric] by simp
+lemma [code func]: "Suc n = nat_of_int (int' n + 1)"
+ by (simp add: eq_nat_of_int)
+lemma [code]: "m + n = nat (int' m + int' n)"
+ by (simp add: int'_def nat_eq_iff2)
+lemma [code func, code inline]: "m + n = nat_of_int (int' m + int' n)"
+ by (simp add: eq_nat_of_int int'_add)
+lemma [code, code inline]: "m - n = nat (int' m - int' n)"
+ by (simp add: int'_def nat_eq_iff2)
+lemma [code]: "m * n = nat (int' m * int' n)"
+ unfolding int'_def
+ by (simp add: of_nat_mult [symmetric] del: of_nat_mult)
+lemma [code func, code inline]: "m * n = nat_of_int (int' m * int' n)"
+ by (simp add: eq_nat_of_int int'_mult)
+lemma [code]: "m div n = nat (int' m div int' n)"
+ unfolding int'_def zdiv_int [symmetric] by simp
lemma [code func]: "m div n = fst (Divides.divmod m n)"
unfolding divmod_def by simp
-lemma [code]: "m mod n = nat (int m mod int n)"
- unfolding zmod_int [symmetric] by simp
+lemma [code]: "m mod n = nat (int' m mod int' n)"
+ unfolding int'_def zmod_int [symmetric] by simp
lemma [code func]: "m mod n = snd (Divides.divmod m n)"
unfolding divmod_def by simp
-lemma [code, code inline]: "(m < n) \<longleftrightarrow> (int m < int n)"
- by simp
-lemma [code func, code inline]: "(m \<le> n) \<longleftrightarrow> (int m \<le> int n)"
- by simp
-lemma [code func, code inline]: "m = n \<longleftrightarrow> int m = int n"
- by simp
+lemma [code, code inline]: "(m < n) \<longleftrightarrow> (int' m < int' n)"
+ unfolding int'_def by simp
+lemma [code func, code inline]: "(m \<le> n) \<longleftrightarrow> (int' m \<le> int' n)"
+ unfolding int'_def by simp
+lemma [code func, code inline]: "m = n \<longleftrightarrow> int' m = int' n"
+ unfolding int'_def by simp
lemma [code func]: "nat k = (if k < 0 then 0 else nat_of_int k)"
proof (cases "k < 0")
case True then show ?thesis by simp
@@ -126,26 +132,27 @@
case False then show ?thesis by (simp add: nat_of_int_def)
qed
lemma [code func]:
- "int_aux i n = (if int n = 0 then i else int_aux (i + 1) (nat_of_int (int n - 1)))"
+ "int_aux i n = (if int' n = 0 then i else int_aux (i + 1) (nat_of_int (int' n - 1)))"
proof -
- have "0 < n \<Longrightarrow> int n = 1 + int (nat_of_int (int n - 1))"
+ have "0 < n \<Longrightarrow> int' n = 1 + int' (nat_of_int (int' n - 1))"
proof -
assume prem: "n > 0"
- then have "int n - 1 \<ge> 0" by auto
- then have "nat_of_int (int n - 1) = nat (int n - 1)" by (simp add: nat_of_int_def)
- with prem show "int n = 1 + int (nat_of_int (int n - 1))" by simp
+ then have "int' n - 1 \<ge> 0" unfolding int'_def by auto
+ then have "nat_of_int (int' n - 1) = nat (int' n - 1)" by (simp add: nat_of_int_def)
+ with prem show "int' n = 1 + int' (nat_of_int (int' n - 1))" unfolding int'_def by simp
qed
- then show ?thesis unfolding int_aux_def by simp
+ then show ?thesis unfolding int_aux_def int'_def by simp
qed
lemma div_nat_code [code func]:
- "m div k = nat_of_int (fst (divAlg (int m, int k)))"
- unfolding div_def [symmetric] zdiv_int [symmetric] nat_of_int_int ..
+ "m div k = nat_of_int (fst (divAlg (int' m, int' k)))"
+ unfolding div_def [symmetric] int'_def zdiv_int [symmetric]
+ unfolding int'_def [symmetric] nat_of_int_int ..
lemma mod_nat_code [code func]:
- "m mod k = nat_of_int (snd (divAlg (int m, int k)))"
- unfolding mod_def [symmetric] zmod_int [symmetric] nat_of_int_int ..
-
+ "m mod k = nat_of_int (snd (divAlg (int' m, int' k)))"
+ unfolding mod_def [symmetric] int'_def zmod_int [symmetric]
+ unfolding int'_def [symmetric] nat_of_int_int ..
subsection {* Code generator setup for basic functions *}
@@ -185,13 +192,13 @@
*}
consts_code
- int ("(_)")
+ int' ("(_)")
nat ("\<module>nat")
attach {*
fun nat i = if i < 0 then 0 else i;
*}
-code_const int
+code_const int'
(SML "_")
(OCaml "_")
(Haskell "_")
@@ -392,6 +399,6 @@
Nat Integer
EfficientNat Integer
-hide const nat_of_int
+hide const nat_of_int int'
end
--- a/src/HOL/Library/GCD.thy Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/Library/GCD.thy Wed Jun 13 03:31:11 2007 +0200
@@ -265,7 +265,7 @@
from relprime_dvd_mult [OF g th] obtain h' where h': "nat \<bar>k\<bar> = nat \<bar>i\<bar> * h'"
unfolding dvd_def by blast
from h' have "int (nat \<bar>k\<bar>) = int (nat \<bar>i\<bar> * h')" by simp
- then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by (simp add: int_mult)
+ then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by simp
then show ?thesis
apply (subst zdvd_abs1 [symmetric])
apply (subst zdvd_abs2 [symmetric])
--- a/src/HOL/Library/Word.thy Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/Library/Word.thy Wed Jun 13 03:31:11 2007 +0200
@@ -989,12 +989,12 @@
next
fix xs
assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs"
- show "bv_to_int (norm_signed (\<one>#xs)) = -1 - int (bv_to_nat (bv_not xs))"
+ show "bv_to_int (norm_signed (\<one>#xs)) = - int (bv_to_nat (bv_not xs)) + -1"
proof (rule bit_list_cases [of xs],simp_all)
fix ys
assume [simp]: "xs = \<one>#ys"
from ind
- show "bv_to_int (norm_signed (\<one>#ys)) = -1 - int (bv_to_nat (bv_not ys))"
+ show "bv_to_int (norm_signed (\<one>#ys)) = - int (bv_to_nat (bv_not ys)) + -1"
by simp
qed
qed
@@ -1007,11 +1007,11 @@
by (simp add: int_nat_two_exp)
next
fix bs
- have "-1 - int (bv_to_nat (bv_not bs)) \<le> 0"
+ have "- int (bv_to_nat (bv_not bs)) + -1 \<le> 0"
by simp
also have "... < 2 ^ length bs"
by (induct bs,simp_all)
- finally show "-1 - int (bv_to_nat (bv_not bs)) < 2 ^ length bs"
+ finally show "- int (bv_to_nat (bv_not bs)) + -1 < 2 ^ length bs"
.
qed
@@ -1027,7 +1027,7 @@
next
fix bs
from bv_to_nat_upper_range [of "bv_not bs"]
- show "- (2 ^ length bs) \<le> -1 - int (bv_to_nat (bv_not bs))"
+ show "- (2 ^ length bs) \<le> - int (bv_to_nat (bv_not bs)) + -1"
by (simp add: int_nat_two_exp)
qed
--- a/src/HOL/NatBin.thy Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/NatBin.thy Wed Jun 13 03:31:11 2007 +0200
@@ -58,14 +58,14 @@
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_of_nat)
+apply (auto elim!: nonneg_eq_int)
apply (rename_tac m m')
-apply (subgoal_tac "0 <= int_of_nat m div int_of_nat m'")
+apply (subgoal_tac "0 <= int m div int m'")
prefer 2 apply (simp add: nat_numeral_0_eq_0 pos_imp_zdiv_nonneg_iff)
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)
+apply (rule_tac r = "int (m mod m') " in quorem_div)
prefer 2 apply force
-apply (simp add: nat_less_iff' [symmetric] quorem_def nat_numeral_0_eq_0
+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
@@ -74,14 +74,14 @@
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_of_nat)
+apply (auto elim!: nonneg_eq_int)
apply (rename_tac m 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 of_nat_eq_iff [where 'a=int, THEN iffD1], simp)
-apply (rule_tac q = "int_of_nat (m div m') " in quorem_mod)
+apply (subgoal_tac "0 <= int m mod int m'")
+ prefer 2 apply (simp add: nat_less_iff nat_numeral_0_eq_0 pos_mod_sign)
+apply (rule int_int_eq [THEN iffD1], simp)
+apply (rule_tac q = "int (m div m') " in quorem_mod)
prefer 2 apply force
-apply (simp add: nat_less_iff' [symmetric] quorem_def nat_numeral_0_eq_0
+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
@@ -97,14 +97,7 @@
(*"neg" is used in rewrite rules for binary comparisons*)
lemma int_nat_number_of [simp]:
- "int (number_of v :: nat) =
- (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)
-
-lemma int_of_nat_number_of [simp]:
- "int_of_nat (number_of v) =
+ "int (number_of v) =
(if neg (number_of v :: int) then 0
else (number_of v :: int))"
by (simp del: nat_number_of
@@ -520,9 +513,6 @@
by (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
-(* Push int(.) inwards: *)
-declare zadd_int [symmetric, simp]
-
lemma lemma1: "(m+m = n+n) = (m = (n::int))"
by auto
--- a/src/HOL/NumberTheory/Fib.thy Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/NumberTheory/Fib.thy Wed Jun 13 03:31:11 2007 +0200
@@ -85,7 +85,7 @@
(if n mod 2 = 0 then fib (Suc n) * fib (Suc n) - 1
else fib (Suc n) * fib (Suc n) + 1)"
apply (rule int_int_eq [THEN iffD1])
- apply (simp add: fib_Cassini_int)
+ apply (simp add: fib_Cassini_int del: of_nat_mult)
apply (subst zdiff_int [symmetric])
apply (insert fib_Suc_gr_0 [of n], simp_all)
done
--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Wed Jun 13 03:31:11 2007 +0200
@@ -281,7 +281,7 @@
lemma S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))"
using P_set_card Q_set_card P_set_finite Q_set_finite
- by (auto simp add: S_def zmult_int setsum_constant)
+ by (auto simp add: S_def setsum_constant)
lemma S1_Int_S2_prop: "S1 \<inter> S2 = {}"
by (auto simp add: S1_def S2_def)
--- a/src/HOL/Numeral.thy Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/Numeral.thy Wed Jun 13 03:31:11 2007 +0200
@@ -457,7 +457,7 @@
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])
@@ -593,7 +593,7 @@
"int_aux i (Suc n) = int_aux (i + 1) n" -- {* tail recursive *}
by (simp add: int_aux_def)+
-lemma [code]:
+lemma [code unfold]:
"int n = int_aux 0 n"
by (simp add: int_aux_def)
--- a/src/HOL/Presburger.thy Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/Presburger.thy Wed Jun 13 03:31:11 2007 +0200
@@ -383,29 +383,14 @@
by (simp split add: split_nat)
lemma ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
- by (auto split add: split_nat)
-(rule_tac x = "nat x" in exI,erule_tac x = "nat x" in allE, simp)
+ apply (auto split add: split_nat)
+ apply (rule_tac x="int x" in exI, simp)
+ apply (rule_tac x = "nat x" in exI,erule_tac x = "nat x" in allE, simp)
+ done
lemma zdiff_int_split: "P (int (x - y)) =
((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
- by (case_tac "y \<le> x",simp_all add: zdiff_int)
-
-lemma zdvd_int: "(x dvd y) = (int x dvd int y)"
- apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
- nat_0_le cong add: conj_cong)
- apply (rule iffI)
- apply iprover
- apply (erule exE)
- apply (case_tac "x=0")
- apply (rule_tac x=0 in exI)
- apply simp
- apply (case_tac "0 \<le> k")
- apply iprover
- apply (simp add: linorder_not_le)
- apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
- apply assumption
- apply (simp add: mult_ac)
- done
+ by (case_tac "y \<le> x", simp_all)
lemma number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)" by simp
lemma number_of2: "(0::int) <= Numeral0" by simp
@@ -670,4 +655,4 @@
less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1
less_number_of
-end
\ No newline at end of file
+end
--- a/src/HOL/Real/Float.thy Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/Real/Float.thy Wed Jun 13 03:31:11 2007 +0200
@@ -35,7 +35,8 @@
apply (auto, induct_tac n)
apply (simp_all add: pow2_def)
apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if])
- by (auto simp add: h)
+ apply (auto simp add: h)
+ by (simp add: add_commute)
show ?thesis
proof (induct a)
case (1 n)
@@ -45,7 +46,7 @@
show ?case
apply (auto)
apply (subst pow2_neg[of "- int n"])
- apply (subst pow2_neg[of "-1 - int n"])
+ apply (subst pow2_neg[of "- int n + -1"])
apply (auto simp add: g pos)
done
qed
--- a/src/HOL/Real/Rational.thy Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/Real/Rational.thy Wed Jun 13 03:31:11 2007 +0200
@@ -565,7 +565,7 @@
by (induct n) (simp_all add: of_rat_add)
lemma of_rat_of_int_eq [simp]: "of_rat (of_int z) = of_int z"
-by (cases z rule: int_diff_cases', simp add: of_rat_diff)
+by (cases z rule: int_diff_cases, simp add: of_rat_diff)
lemma of_rat_number_of_eq [simp]:
"of_rat (number_of w) = (number_of w :: 'a::{number_ring,field_char_0})"
--- a/src/HOL/arith_data.ML Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/arith_data.ML Wed Jun 13 03:31:11 2007 +0200
@@ -601,7 +601,7 @@
val terms2 = map (subst_term [(split_term, zero_nat)]) rev_terms
val t1' = incr_boundvars 1 t1
val t1_eq_int_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
- (Const ("IntDef.int", HOLogic.natT --> HOLogic.intT) $ n)
+ (Const ("Nat.of_nat", HOLogic.natT --> HOLogic.intT) $ n)
val t1_lt_zero = Const (@{const_name Orderings.less},
HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
--- a/src/HOL/int_arith1.ML Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/int_arith1.ML Wed Jun 13 03:31:11 2007 +0200
@@ -573,10 +573,11 @@
@{thm mult_zero_left}, @{thm mult_zero_right}, @{thm mult_num1}, @{thm mult_1_right},
@{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym,
@{thm minus_add_distrib}, @{thm minus_minus}, @{thm mult_assoc},
- of_nat_0, of_nat_1, of_nat_Suc, of_nat_add, of_nat_mult,
- of_int_0, of_int_1, of_int_add, of_int_mult, int_eq_of_nat]
+ @{thm of_nat_0}, @{thm of_nat_1}, @{thm of_nat_Suc}, @{thm of_nat_add},
+ @{thm of_nat_mult}, @{thm of_int_0}, @{thm of_int_1}, @{thm of_int_add},
+ @{thm of_int_mult}]
-val nat_inj_thms = [zle_int RS iffD2, int_int_eq RS iffD2]
+val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
val Int_Numeral_Base_Simprocs = assoc_fold_simproc
:: Int_Numeral_Simprocs.combine_numerals
@@ -595,7 +596,6 @@
addsimprocs Int_Numeral_Base_Simprocs
addcongs [if_weak_cong]}) #>
arith_inj_const ("Nat.of_nat", HOLogic.natT --> HOLogic.intT) #>
- arith_inj_const ("IntDef.int", HOLogic.natT --> HOLogic.intT) #>
arith_discrete "IntDef.int"
end;