complete set of cases rules for integers known to be (non-)positive/negative;
legacy theorem branding

--- a/src/HOL/Int.thy	Fri Dec 30 18:02:27 2016 +0100
+++ b/src/HOL/Int.thy	Fri Dec 30 18:02:27 2016 +0100
@@ -433,11 +433,57 @@
 lemma zless_nat_conj [simp]: "nat w < nat z \<longleftrightarrow> 0 < z \<and> w < z"
   by transfer (clarsimp, arith)
 
-lemma nonneg_eq_int:
-  fixes z :: int
-  assumes "0 \<le> z" and "\<And>m. z = int m \<Longrightarrow> P"
-  shows P
-  using assms by (blast dest: nat_0_le sym)
+lemma nonneg_int_cases:
+  assumes "0 \<le> k"
+  obtains n where "k = int n"
+proof -
+  from assms have "k = int (nat k)"
+    by simp
+  then show thesis
+    by (rule that)
+qed
+
+lemma pos_int_cases:
+  assumes "0 < k"
+  obtains n where "k = int n" and "n > 0"
+proof -
+  from assms have "0 \<le> k"
+    by simp
+  then obtain n where "k = int n"
+    by (rule nonneg_int_cases)
+  moreover have "n > 0"
+    using \<open>k = int n\<close> assms by simp
+  ultimately show thesis
+    by (rule that)
+qed
+
+lemma nonpos_int_cases:
+  assumes "k \<le> 0"
+  obtains n where "k = - int n"
+proof -
+  from assms have "- k \<ge> 0"
+    by simp
+  then obtain n where "- k = int n"
+    by (rule nonneg_int_cases)
+  then have "k = - int n"
+    by simp
+  then show thesis
+    by (rule that)
+qed
+
+lemma neg_int_cases:
+  assumes "k < 0"
+  obtains n where "k = - int n" and "n > 0"
+proof -
+  from assms have "- k > 0"
+    by simp
+  then obtain n where "- k = int n" and "- k > 0"
+    by (blast elim: pos_int_cases)
+  then have "k = - int n" and "n > 0"
+    by simp_all
+  then show thesis
+    by (rule that)
+qed
 
 lemma nat_eq_iff: "nat w = m \<longleftrightarrow> (if 0 \<le> w then w = int m else m = 0)"
   by transfer (clarsimp simp add: le_imp_diff_is_add)
@@ -615,11 +661,6 @@
   "(\<And>n. P (int n)) \<Longrightarrow> (\<And>n. P (- (int (Suc n)))) \<Longrightarrow> P z"
   by (cases z) auto
 
-lemma nonneg_int_cases:
-  assumes "0 \<le> k"
-  obtains n where "k = int n"
-  using assms by (rule nonneg_eq_int)
-
 lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
   \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close>
   by (fact Let_numeral) \<comment> \<open>FIXME drop\<close>
@@ -880,14 +921,14 @@
 lemma of_int_prod [simp]: "of_int (prod f A) = (\<Prod>x\<in>A. of_int(f x))"
   by (induct A rule: infinite_finite_induct) auto
 
-lemmas int_sum = of_nat_sum [where 'a=int]
-lemmas int_prod = of_nat_prod [where 'a=int]
-
 
 text \<open>Legacy theorems\<close>
 
+lemmas int_sum = of_nat_sum [where 'a=int]
+lemmas int_prod = of_nat_prod [where 'a=int]
 lemmas zle_int = of_nat_le_iff [where 'a=int]
 lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
+lemmas nonneg_eq_int = nonneg_int_cases
 
 
 subsection \<open>Setting up simplification procedures\<close>