src/HOL/IntDef.thy
changeset 23307 2fe3345035c7
parent 23303 6091e530ff77
child 23308 95a01ddfb024
     1.1 --- a/src/HOL/IntDef.thy	Mon Jun 11 02:25:55 2007 +0200
     1.2 +++ b/src/HOL/IntDef.thy	Mon Jun 11 05:20:05 2007 +0200
     1.3 @@ -416,7 +416,7 @@
     1.4  lemma nat_zminus_int_of_nat [simp]: "nat (- (int_of_nat n)) = 0"
     1.5  by (simp add: int_of_nat_def minus nat Zero_int_def) 
     1.6  
     1.7 -lemma zless_nat_eq_int_zless: "(m < nat z) = (int_of_nat m < z)"
     1.8 +lemma zless_nat_eq_int_zless': "(m < nat z) = (int_of_nat m < z)"
     1.9  by (cases z, simp add: nat less int_of_nat_def, arith)
    1.10  
    1.11  
    1.12 @@ -779,7 +779,7 @@
    1.13  apply (rule_tac x="y - Suc x" in exI, arith)
    1.14  done
    1.15  
    1.16 -theorem int_cases':
    1.17 +theorem int_cases' [case_names nonneg neg]:
    1.18       "[|!! n. z = int_of_nat n ==> P;  !! n. z =  - (int_of_nat (Suc n)) ==> P |] ==> P"
    1.19  apply (cases "z < 0", blast dest!: negD')
    1.20  apply (simp add: linorder_not_less del: of_nat_Suc)
    1.21 @@ -954,37 +954,30 @@
    1.22  qed
    1.23  
    1.24  lemma of_int_int_eq [simp]: "of_int (int n) = of_nat n"
    1.25 -by (simp add: int_eq_of_nat)
    1.26 +unfolding int_eq_of_nat by (rule of_int_of_nat_eq)
    1.27  
    1.28  lemma int_setsum: "int (setsum f A) = (\<Sum>x\<in>A. int(f x))"
    1.29 -  by (simp add: int_eq_of_nat of_nat_setsum)
    1.30 +unfolding int_eq_of_nat by (rule of_nat_setsum)
    1.31  
    1.32  lemma int_setprod: "int (setprod f A) = (\<Prod>x\<in>A. int(f x))"
    1.33 -  by (simp add: int_eq_of_nat of_nat_setprod)
    1.34 +unfolding int_eq_of_nat by (rule of_nat_setprod)
    1.35  
    1.36  text{*Now we replace the case analysis rule by a more conventional one:
    1.37  whether an integer is negative or not.*}
    1.38  
    1.39  lemma zless_iff_Suc_zadd:
    1.40      "(w < z) = (\<exists>n. z = w + int(Suc n))"
    1.41 -apply (cases z, cases w)
    1.42 -apply (auto simp add: le add int_def linorder_not_le [symmetric]) 
    1.43 -apply (rename_tac a b c d) 
    1.44 -apply (rule_tac x="a+d - Suc(c+b)" in exI) 
    1.45 -apply arith
    1.46 -done
    1.47 +unfolding int_eq_of_nat by (rule zless_iff_Suc_zadd')
    1.48  
    1.49  lemma negD: "x<0 ==> \<exists>n. x = - (int (Suc n))"
    1.50 -apply (cases x)
    1.51 -apply (auto simp add: le minus Zero_int_def int_def order_less_le) 
    1.52 -apply (rule_tac x="y - Suc x" in exI, arith)
    1.53 -done
    1.54 +unfolding int_eq_of_nat by (rule negD')
    1.55  
    1.56  theorem int_cases [cases type: int, case_names nonneg neg]:
    1.57       "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
    1.58 -apply (cases "z < 0", blast dest!: negD)
    1.59 +unfolding int_eq_of_nat
    1.60 +apply (cases "z < 0", blast dest!: negD')
    1.61  apply (simp add: linorder_not_less)
    1.62 -apply (blast dest: nat_0_le [THEN sym])
    1.63 +apply (blast dest: nat_0_le' [THEN sym])
    1.64  done
    1.65  
    1.66  theorem int_induct [induct type: int, case_names nonneg neg]: