src/HOL/Int.thy
changeset 60868 dd18c33c001e
parent 60758 d8d85a8172b5
child 61070 b72a990adfe2
     1.1 --- a/src/HOL/Int.thy	Thu Aug 06 23:56:48 2015 +0200
     1.2 +++ b/src/HOL/Int.thy	Sat Aug 08 10:51:33 2015 +0200
     1.3 @@ -515,6 +515,25 @@
     1.4  apply (blast dest: nat_0_le [THEN sym])
     1.5  done
     1.6  
     1.7 +lemma int_cases3 [case_names zero pos neg]:
     1.8 +  fixes k :: int
     1.9 +  assumes "k = 0 \<Longrightarrow> P" and "\<And>n. k = int n \<Longrightarrow> n > 0 \<Longrightarrow> P"
    1.10 +    and "\<And>n. k = - int n \<Longrightarrow> n > 0 \<Longrightarrow> P" 
    1.11 +  shows "P"
    1.12 +proof (cases k "0::int" rule: linorder_cases)
    1.13 +  case equal with assms(1) show P by simp
    1.14 +next
    1.15 +  case greater
    1.16 +  then have "nat k > 0" by simp
    1.17 +  moreover from this have "k = int (nat k)" by auto
    1.18 +  ultimately show P using assms(2) by blast
    1.19 +next
    1.20 +  case less
    1.21 +  then have "nat (- k) > 0" by simp
    1.22 +  moreover from this have "k = - int (nat (- k))" by auto
    1.23 +  ultimately show P using assms(3) by blast
    1.24 +qed
    1.25 +
    1.26  theorem int_of_nat_induct [case_names nonneg neg, induct type: int]:
    1.27       "[|!! n. P (int n);  !!n. P (- (int (Suc n))) |] ==> P z"
    1.28    by (cases z) auto