complete set of cases rules for integers known to be (non-)positive/negative;
authorhaftmann
Fri Dec 30 18:02:27 2016 +0100 (2016-12-30)
changeset 6471453bab28983f1
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
     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.65    by transfer (clarsimp simp add: le_imp_diff_is_add)
    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>