src/HOL/Int.thy
 changeset 64714 53bab28983f1 parent 64272 f76b6dda2e56 child 64758 3b33d2fc5fc0
```     1.1 --- a/src/HOL/Int.thy	Fri Dec 30 18:02:27 2016 +0100
1.2 +++ b/src/HOL/Int.thy	Fri Dec 30 18:02:27 2016 +0100
1.3 @@ -433,11 +433,57 @@
1.4  lemma zless_nat_conj [simp]: "nat w < nat z \<longleftrightarrow> 0 < z \<and> w < z"
1.5    by transfer (clarsimp, arith)
1.6
1.7 -lemma nonneg_eq_int:
1.8 -  fixes z :: int
1.9 -  assumes "0 \<le> z" and "\<And>m. z = int m \<Longrightarrow> P"
1.10 -  shows P
1.11 -  using assms by (blast dest: nat_0_le sym)
1.12 +lemma nonneg_int_cases:
1.13 +  assumes "0 \<le> k"
1.14 +  obtains n where "k = int n"
1.15 +proof -
1.16 +  from assms have "k = int (nat k)"
1.17 +    by simp
1.18 +  then show thesis
1.19 +    by (rule that)
1.20 +qed
1.21 +
1.22 +lemma pos_int_cases:
1.23 +  assumes "0 < k"
1.24 +  obtains n where "k = int n" and "n > 0"
1.25 +proof -
1.26 +  from assms have "0 \<le> k"
1.27 +    by simp
1.28 +  then obtain n where "k = int n"
1.29 +    by (rule nonneg_int_cases)
1.30 +  moreover have "n > 0"
1.31 +    using \<open>k = int n\<close> assms by simp
1.32 +  ultimately show thesis
1.33 +    by (rule that)
1.34 +qed
1.35 +
1.36 +lemma nonpos_int_cases:
1.37 +  assumes "k \<le> 0"
1.38 +  obtains n where "k = - int n"
1.39 +proof -
1.40 +  from assms have "- k \<ge> 0"
1.41 +    by simp
1.42 +  then obtain n where "- k = int n"
1.43 +    by (rule nonneg_int_cases)
1.44 +  then have "k = - int n"
1.45 +    by simp
1.46 +  then show thesis
1.47 +    by (rule that)
1.48 +qed
1.49 +
1.50 +lemma neg_int_cases:
1.51 +  assumes "k < 0"
1.52 +  obtains n where "k = - int n" and "n > 0"
1.53 +proof -
1.54 +  from assms have "- k > 0"
1.55 +    by simp
1.56 +  then obtain n where "- k = int n" and "- k > 0"
1.57 +    by (blast elim: pos_int_cases)
1.58 +  then have "k = - int n" and "n > 0"
1.59 +    by simp_all
1.60 +  then show thesis
1.61 +    by (rule that)
1.62 +qed
1.63
1.64  lemma nat_eq_iff: "nat w = m \<longleftrightarrow> (if 0 \<le> w then w = int m else m = 0)"
1.66 @@ -615,11 +661,6 @@
1.67    "(\<And>n. P (int n)) \<Longrightarrow> (\<And>n. P (- (int (Suc n)))) \<Longrightarrow> P z"
1.68    by (cases z) auto
1.69
1.70 -lemma nonneg_int_cases:
1.71 -  assumes "0 \<le> k"
1.72 -  obtains n where "k = int n"
1.73 -  using assms by (rule nonneg_eq_int)
1.74 -
1.75  lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)"
1.76    \<comment> \<open>Unfold all \<open>let\<close>s involving constants\<close>
1.77    by (fact Let_numeral) \<comment> \<open>FIXME drop\<close>
1.78 @@ -880,14 +921,14 @@
1.79  lemma of_int_prod [simp]: "of_int (prod f A) = (\<Prod>x\<in>A. of_int(f x))"
1.80    by (induct A rule: infinite_finite_induct) auto
1.81
1.82 -lemmas int_sum = of_nat_sum [where 'a=int]
1.83 -lemmas int_prod = of_nat_prod [where 'a=int]
1.84 -
1.85
1.86  text \<open>Legacy theorems\<close>
1.87
1.88 +lemmas int_sum = of_nat_sum [where 'a=int]
1.89 +lemmas int_prod = of_nat_prod [where 'a=int]
1.90  lemmas zle_int = of_nat_le_iff [where 'a=int]
1.91  lemmas int_int_eq = of_nat_eq_iff [where 'a=int]
1.92 +lemmas nonneg_eq_int = nonneg_int_cases
1.93
1.94
1.95  subsection \<open>Setting up simplification procedures\<close>
```