--- a/src/HOL/Int.thy Thu Mar 29 14:47:31 2012 +0200
+++ b/src/HOL/Int.thy Fri Mar 30 08:10:28 2012 +0200
@@ -575,6 +575,10 @@
"[|!! n. P (int n); !!n. P (- (int (Suc n))) |] ==> P z"
by (cases z) auto
+lemma nonneg_int_cases:
+ assumes "0 \<le> k" obtains n where "k = int n"
+ using assms by (cases k, simp, simp del: of_nat_Suc)
+
text{*Contributed by Brian Huffman*}
theorem int_diff_cases:
obtains (diff) m n where "z = int m - int n"
@@ -888,7 +892,7 @@
lemma nat_0 [simp]: "nat 0 = 0"
by (simp add: nat_eq_iff)
-lemma nat_1: "nat 1 = Suc 0"
+lemma nat_1 [simp]: "nat 1 = Suc 0"
by (subst nat_eq_iff, simp)
lemma nat_2: "nat 2 = Suc (Suc 0)"
@@ -896,7 +900,7 @@
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)
+apply auto
done
text{*This simplifies expressions of the form @{term "int n = z"} where
@@ -963,6 +967,41 @@
nat_mult_distrib_neg [symmetric] mult_less_0_iff)
done
+lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
+apply (rule sym)
+apply (simp add: nat_eq_iff)
+done
+
+lemma diff_nat_eq_if:
+ "nat z - nat z' =
+ (if z' < 0 then nat z
+ else let d = z-z' in
+ if d < 0 then 0 else nat d)"
+by (simp add: Let_def nat_diff_distrib [symmetric])
+
+(* nat_diff_distrib has too-strong premises *)
+lemma nat_diff_distrib': "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x - y) = nat x - nat y"
+apply (rule int_int_eq [THEN iffD1], clarsimp)
+apply (subst of_nat_diff)
+apply (rule nat_mono, simp_all)
+done
+
+lemma nat_numeral [simp, code_abbrev]:
+ "nat (numeral k) = numeral k"
+ by (simp add: nat_eq_iff)
+
+lemma nat_neg_numeral [simp]:
+ "nat (neg_numeral k) = 0"
+ by simp
+
+lemma diff_nat_numeral [simp]:
+ "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
+ by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
+
+lemma nat_numeral_diff_1 [simp]:
+ "numeral v - (1::nat) = nat (numeral v - 1)"
+ using diff_nat_numeral [of v Num.One] by simp
+
subsection "Induction principles for int"
@@ -1681,10 +1720,6 @@
"Neg k < Neg l \<longleftrightarrow> l < k"
by simp_all
-lemma nat_numeral [simp, code_abbrev]:
- "nat (numeral k) = numeral k"
- by (simp add: nat_eq_iff)
-
lemma nat_code [code]:
"nat (Int.Neg k) = 0"
"nat 0 = 0"
@@ -1729,6 +1764,7 @@
lemmas int_0 = of_nat_0 [where 'a=int]
lemmas int_1 = of_nat_1 [where 'a=int]
lemmas int_Suc = of_nat_Suc [where 'a=int]
+lemmas int_numeral = of_nat_numeral [where 'a=int]
lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m"] for m
lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
@@ -1744,4 +1780,3 @@
lemmas zpower_int = int_power [symmetric]
end
-
--- a/src/HOL/Nat_Numeral.thy Thu Mar 29 14:47:31 2012 +0200
+++ b/src/HOL/Nat_Numeral.thy Fri Mar 30 08:10:28 2012 +0200
@@ -9,69 +9,8 @@
imports Int
begin
-subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*}
-
-declare nat_1 [simp]
-
-lemma nat_neg_numeral [simp]: "nat (neg_numeral w) = 0"
- by simp
-
-lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
- by simp
-
-
-subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
-
-lemma int_numeral: "int (numeral v) = numeral v"
- by (rule of_nat_numeral) (* already simp *)
-
-lemma nonneg_int_cases:
- fixes k :: int assumes "0 \<le> k" obtains n where "k = of_nat n"
- using assms by (cases k, simp, simp)
-
-subsubsection{*Successor *}
-
-lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
-apply (rule sym)
-apply (simp add: nat_eq_iff)
-done
-
-lemma Suc_nat_number_of_add:
- "Suc (numeral v + n) = numeral (v + Num.One) + n"
- by simp
-
-
-subsubsection{*Subtraction *}
-
-lemma diff_nat_eq_if:
- "nat z - nat z' =
- (if z' < 0 then nat z
- else let d = z-z' in
- if d < 0 then 0 else nat d)"
-by (simp add: Let_def nat_diff_distrib [symmetric])
-
-(* Int.nat_diff_distrib has too-strong premises *)
-lemma nat_diff_distrib': "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x - y) = nat x - nat y"
-apply (rule int_int_eq [THEN iffD1], clarsimp)
-apply (subst zdiff_int [symmetric])
-apply (rule nat_mono, simp_all)
-done
-
-lemma diff_nat_numeral [simp]:
- "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
- by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)
-
-lemma nat_numeral_diff_1 [simp]:
- "numeral v - (1::nat) = nat (numeral v - 1)"
- using diff_nat_numeral [of v Num.One] by simp
-
-
subsection{*Comparisons*}
-(*Maps #n to n for n = 1, 2*)
-lemmas numerals = numeral_1_eq_1 [where 'a=nat] numeral_2_eq_2
-
-
text{*Simprules for comparisons where common factors can be cancelled.*}
lemmas zero_compare_simps =
add_strict_increasing add_strict_increasing2 add_increasing
--- a/src/HOL/Num.thy Thu Mar 29 14:47:31 2012 +0200
+++ b/src/HOL/Num.thy Fri Mar 30 08:10:28 2012 +0200
@@ -876,6 +876,16 @@
lemma numeral_3_eq_3: "3 = Suc (Suc (Suc 0))"
by (simp add: nat_number(2-4))
+lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
+ by (simp only: numeral_One One_nat_def)
+
+lemma Suc_nat_number_of_add:
+ "Suc (numeral v + n) = numeral (v + Num.One) + n"
+ by simp
+
+(*Maps #n to n for n = 1, 2*)
+lemmas numerals = numeral_One [where 'a=nat] numeral_2_eq_2
+
subsection {* Numeral equations as default simplification rules *}
--- a/src/HOL/Tools/SMT/smt_normalize.ML Thu Mar 29 14:47:31 2012 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Fri Mar 30 08:10:28 2012 +0200
@@ -467,7 +467,7 @@
let
val eq = SMT_Utils.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
val ss = HOL_ss
- addsimps [@{thm Nat_Numeral.int_numeral}]
+ addsimps [@{thm Int.int_numeral}]
fun tac _ = Simplifier.simp_tac (Simplifier.context ctxt ss) 1
in Goal.norm_result (Goal.prove_internal [] eq tac) end