equal
deleted
inserted
replaced
512 apply (blast dest!: negD) |
512 apply (blast dest!: negD) |
513 apply (simp add: linorder_not_less del: of_nat_Suc) |
513 apply (simp add: linorder_not_less del: of_nat_Suc) |
514 apply auto |
514 apply auto |
515 apply (blast dest: nat_0_le [THEN sym]) |
515 apply (blast dest: nat_0_le [THEN sym]) |
516 done |
516 done |
|
517 |
|
518 lemma int_cases3 [case_names zero pos neg]: |
|
519 fixes k :: int |
|
520 assumes "k = 0 \<Longrightarrow> P" and "\<And>n. k = int n \<Longrightarrow> n > 0 \<Longrightarrow> P" |
|
521 and "\<And>n. k = - int n \<Longrightarrow> n > 0 \<Longrightarrow> P" |
|
522 shows "P" |
|
523 proof (cases k "0::int" rule: linorder_cases) |
|
524 case equal with assms(1) show P by simp |
|
525 next |
|
526 case greater |
|
527 then have "nat k > 0" by simp |
|
528 moreover from this have "k = int (nat k)" by auto |
|
529 ultimately show P using assms(2) by blast |
|
530 next |
|
531 case less |
|
532 then have "nat (- k) > 0" by simp |
|
533 moreover from this have "k = - int (nat (- k))" by auto |
|
534 ultimately show P using assms(3) by blast |
|
535 qed |
517 |
536 |
518 theorem int_of_nat_induct [case_names nonneg neg, induct type: int]: |
537 theorem int_of_nat_induct [case_names nonneg neg, induct type: int]: |
519 "[|!! n. P (int n); !!n. P (- (int (Suc n))) |] ==> P z" |
538 "[|!! n. P (int n); !!n. P (- (int (Suc n))) |] ==> P z" |
520 by (cases z) auto |
539 by (cases z) auto |
521 |
540 |