src/HOL/Int.thy
changeset 59613 7103019278f0
parent 59582 0fbed69ff081
child 59667 651ea265d568
     1.1 --- a/src/HOL/Int.thy	Thu Mar 05 11:11:42 2015 +0100
     1.2 +++ b/src/HOL/Int.thy	Thu Mar 05 17:30:29 2015 +0000
     1.3 @@ -498,8 +498,16 @@
     1.4  text{*Now we replace the case analysis rule by a more conventional one:
     1.5  whether an integer is negative or not.*}
     1.6  
     1.7 +text{*This version is symmetric in the two subgoals.*}
     1.8 +theorem int_cases2 [case_names nonneg nonpos, cases type: int]:
     1.9 +  "\<lbrakk>!! n. z = int n \<Longrightarrow> P;  !! n. z = - (int n) \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    1.10 +apply (cases "z < 0")
    1.11 +apply (auto simp add: linorder_not_less dest!: negD nat_0_le [THEN sym])
    1.12 +done
    1.13 +
    1.14 +text{*This is the default, with a negative case.*}
    1.15  theorem int_cases [case_names nonneg neg, cases type: int]:
    1.16 -  "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
    1.17 +  "[|!! n. z = int n ==> P;  !! n. z = - (int (Suc n)) ==> P |] ==> P"
    1.18  apply (cases "z < 0")
    1.19  apply (blast dest!: negD)
    1.20  apply (simp add: linorder_not_less del: of_nat_Suc)