author haftmann Fri, 30 Dec 2016 18:02:27 +0100 changeset 64714 53bab28983f1 parent 64713 9638c07283bc child 64715 33d5fa0ce6e5
complete set of cases rules for integers known to be (non-)positive/negative; legacy theorem branding
 src/HOL/Int.thy file | annotate | diff | comparison | revisions
```--- 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)"
@@ -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>```