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.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.40      "(w < z) = (\<exists>n. z = w + int(Suc n))"
1.41 -apply (cases z, cases w)
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')