summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Int.thy

changeset 60868 | dd18c33c001e |

parent 60758 | d8d85a8172b5 |

child 61070 | b72a990adfe2 |

--- a/src/HOL/Int.thy Thu Aug 06 23:56:48 2015 +0200 +++ b/src/HOL/Int.thy Sat Aug 08 10:51:33 2015 +0200 @@ -515,6 +515,25 @@ apply (blast dest: nat_0_le [THEN sym]) done +lemma int_cases3 [case_names zero pos neg]: + fixes k :: int + assumes "k = 0 \<Longrightarrow> P" and "\<And>n. k = int n \<Longrightarrow> n > 0 \<Longrightarrow> P" + and "\<And>n. k = - int n \<Longrightarrow> n > 0 \<Longrightarrow> P" + shows "P" +proof (cases k "0::int" rule: linorder_cases) + case equal with assms(1) show P by simp +next + case greater + then have "nat k > 0" by simp + moreover from this have "k = int (nat k)" by auto + ultimately show P using assms(2) by blast +next + case less + then have "nat (- k) > 0" by simp + moreover from this have "k = - int (nat (- k))" by auto + ultimately show P using assms(3) by blast +qed + theorem int_of_nat_induct [case_names nonneg neg, induct type: int]: "[|!! n. P (int n); !!n. P (- (int (Suc n))) |] ==> P z" by (cases z) auto