src/HOL/IntDef.thy
 changeset 23308 95a01ddfb024 parent 23307 2fe3345035c7 child 23365 f31794033ae1
```     1.1 --- a/src/HOL/IntDef.thy	Mon Jun 11 05:20:05 2007 +0200
1.2 +++ b/src/HOL/IntDef.thy	Mon Jun 11 06:14:32 2007 +0200
1.3 @@ -447,7 +447,7 @@
1.4    "(- int_of_nat n = int_of_nat m) = (n = 0 & m = 0)"
1.5  by (force simp add: order_eq_iff [of "- int_of_nat n"] int_zle_neg')
1.6
1.7 -lemma zle_iff_zadd: "(w \<le> z) = (\<exists>n. z = w + int_of_nat n)"
1.8 +lemma zle_iff_zadd': "(w \<le> z) = (\<exists>n. z = w + int_of_nat n)"
1.10    fix a b c d
1.11    assume "w = Abs_Integ (intrel `` {(a,b)})" "z = Abs_Integ (intrel `` {(c,d)})"
1.12 @@ -779,14 +779,14 @@
1.13  apply (rule_tac x="y - Suc x" in exI, arith)
1.14  done
1.15
1.16 -theorem int_cases' [case_names nonneg neg]:
1.17 +theorem int_cases' [cases type: int, 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  apply (blast dest: nat_0_le' [THEN sym])
1.22  done
1.23
1.24 -theorem int_induct':
1.25 +theorem int_induct' [induct type: int, case_names nonneg neg]:
1.26       "[|!! n. P (int_of_nat n);  !!n. P (- (int_of_nat (Suc n))) |] ==> P z"
1.27    by (cases z rule: int_cases') auto
1.28
1.29 @@ -799,7 +799,7 @@
1.30  done
1.31
1.32  lemma of_nat_nat: "0 \<le> z ==> of_nat (nat z) = of_int z"
1.33 -by (cases z, simp add: nat le of_int Zero_int_def)
1.34 +by (cases z rule: eq_Abs_Integ, simp add: nat le of_int Zero_int_def)
1.35
1.36  lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq]
1.37
1.38 @@ -811,147 +811,129 @@
1.39  where
1.40    [code func del]: "int m = Abs_Integ (intrel `` {(m, 0)})"
1.41
1.42 +text{*Agreement with the specific embedding for the integers*}
1.43 +lemma int_eq_of_nat: "int = (of_nat :: nat => int)"
1.44 +by (simp add: expand_fun_eq int_of_nat_def int_def)
1.45 +
1.46  lemma inj_int: "inj int"
1.47  by (simp add: inj_on_def int_def)
1.48
1.49  lemma int_int_eq [iff]: "(int m = int n) = (m = n)"
1.50 -by (fast elim!: inj_int [THEN injD])
1.51 +unfolding int_eq_of_nat by (rule of_nat_eq_iff)
1.52
1.53  lemma zadd_int: "(int m) + (int n) = int (m + n)"
1.55 +unfolding int_eq_of_nat by (rule of_nat_add [symmetric])
1.56
1.57  lemma zadd_int_left: "(int m) + (int n + z) = int (m + n) + z"
1.59 +unfolding int_eq_of_nat by simp
1.60
1.61  lemma int_mult: "int (m * n) = (int m) * (int n)"
1.62 -by (simp add: int_def mult)
1.63 +unfolding int_eq_of_nat by (rule of_nat_mult)
1.64
1.65  text{*Compatibility binding*}
1.66  lemmas zmult_int = int_mult [symmetric]
1.67
1.68  lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)"
1.69 -by (simp add: Zero_int_def [folded int_def])
1.70 +unfolding int_eq_of_nat by (rule of_nat_eq_0_iff)
1.71
1.72  lemma zless_int [simp]: "(int m < int n) = (m<n)"
1.74 +unfolding int_eq_of_nat by (rule of_nat_less_iff)
1.75
1.76  lemma int_less_0_conv [simp]: "~ (int k < 0)"
1.77 -by (simp add: Zero_int_def [folded int_def])
1.78 +unfolding int_eq_of_nat by (rule of_nat_less_0_iff)
1.79
1.80  lemma zero_less_int_conv [simp]: "(0 < int n) = (0 < n)"
1.81 -by (simp add: Zero_int_def [folded int_def])
1.82 +unfolding int_eq_of_nat by (rule of_nat_0_less_iff)
1.83
1.84  lemma zle_int [simp]: "(int m \<le> int n) = (m\<le>n)"
1.85 -by (simp add: linorder_not_less [symmetric])
1.86 +unfolding int_eq_of_nat by (rule of_nat_le_iff)
1.87
1.88  lemma zero_zle_int [simp]: "(0 \<le> int n)"
1.89 -by (simp add: Zero_int_def [folded int_def])
1.90 +unfolding int_eq_of_nat by (rule of_nat_0_le_iff)
1.91
1.92  lemma int_le_0_conv [simp]: "(int n \<le> 0) = (n = 0)"
1.93 -by (simp add: Zero_int_def [folded int_def])
1.94 +unfolding int_eq_of_nat by (rule of_nat_le_0_iff)
1.95
1.96  lemma int_0 [simp]: "int 0 = (0::int)"
1.97 -by (simp add: Zero_int_def [folded int_def])
1.98 +unfolding int_eq_of_nat by (rule of_nat_0)
1.99
1.100  lemma int_1 [simp]: "int 1 = 1"
1.101 -by (simp add: One_int_def [folded int_def])
1.102 +unfolding int_eq_of_nat by (rule of_nat_1)
1.103
1.104  lemma int_Suc0_eq_1: "int (Suc 0) = 1"
1.105 -by (simp add: One_int_def [folded int_def])
1.106 +unfolding int_eq_of_nat by simp
1.107
1.108  lemma int_Suc: "int (Suc m) = 1 + (int m)"
1.110 +unfolding int_eq_of_nat by simp
1.111
1.112  lemma nat_int [simp]: "nat(int n) = n"
1.113 -by (simp add: nat int_def)
1.114 +unfolding int_eq_of_nat by (rule nat_int_of_nat)
1.115
1.116  lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
1.117 -by (cases z, simp add: nat le int_def Zero_int_def)
1.118 +unfolding int_eq_of_nat by (rule int_of_nat_nat_eq)
1.119
1.120  corollary nat_0_le: "0 \<le> z ==> int (nat z) = z"
1.121 -by simp
1.122 +unfolding int_eq_of_nat by (rule nat_0_le')
1.123
1.124  lemma nonneg_eq_int: "[| 0 \<le> z;  !!m. z = int m ==> P |] ==> P"
1.125 -by (blast dest: nat_0_le sym)
1.126 +unfolding int_eq_of_nat by (blast elim: nonneg_eq_int_of_nat)
1.127
1.128  lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"
1.129 -by (cases w, simp add: nat le int_def Zero_int_def, arith)
1.130 +unfolding int_eq_of_nat by (rule nat_eq_iff')
1.131
1.132  corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"
1.133 -by (simp only: eq_commute [of m] nat_eq_iff)
1.134 +unfolding int_eq_of_nat by (rule nat_eq_iff2')
1.135
1.136  lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < int m)"
1.137 -apply (cases w)
1.138 -apply (simp add: nat le int_def Zero_int_def linorder_not_le [symmetric], arith)
1.139 -done
1.140 +unfolding int_eq_of_nat by (rule nat_less_iff')
1.141
1.142  lemma int_eq_iff: "(int m = z) = (m = nat z & 0 \<le> z)"
1.143 -by (auto simp add: nat_eq_iff2)
1.144 +unfolding int_eq_of_nat by (rule int_of_nat_eq_iff)
1.145
1.146  lemma nat_zminus_int [simp]: "nat (- (int n)) = 0"
1.147 -by (simp add: int_def minus nat Zero_int_def)
1.148 +unfolding int_eq_of_nat by (rule nat_zminus_int_of_nat)
1.149
1.150  lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
1.151 -by (cases z, simp add: nat le int_def  linorder_not_le [symmetric], arith)
1.152 +unfolding int_eq_of_nat by (rule zless_nat_eq_int_zless')
1.153
1.154  lemma negative_zless_0: "- (int (Suc n)) < 0"
1.156 +unfolding int_eq_of_nat by (rule negative_zless_0')
1.157
1.158  lemma negative_zless [iff]: "- (int (Suc n)) < int m"
1.159 -by (rule negative_zless_0 [THEN order_less_le_trans], simp)
1.160 +unfolding int_eq_of_nat by (rule negative_zless')
1.161
1.162  lemma negative_zle_0: "- int n \<le> 0"
1.164 +unfolding int_eq_of_nat by (rule negative_zle_0')
1.165
1.166  lemma negative_zle [iff]: "- int n \<le> int m"
1.167 -by (rule order_trans [OF negative_zle_0 zero_zle_int])
1.168 +unfolding int_eq_of_nat by (rule negative_zle')
1.169
1.170  lemma not_zle_0_negative [simp]: "~ (0 \<le> - (int (Suc n)))"
1.171 -by (subst le_minus_iff, simp)
1.172 +unfolding int_eq_of_nat by (rule not_zle_0_negative')
1.173
1.174  lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
1.175 -by (simp add: int_def le minus Zero_int_def)
1.176 +unfolding int_eq_of_nat by (rule int_zle_neg')
1.177
1.178  lemma not_int_zless_negative [simp]: "~ (int n < - int m)"
1.180 +unfolding int_eq_of_nat by (rule not_int_zless_negative')
1.181
1.182  lemma negative_eq_positive [simp]: "(- int n = int m) = (n = 0 & m = 0)"
1.183 -by (force simp add: order_eq_iff [of "- int n"] int_zle_neg)
1.184 +unfolding int_eq_of_nat by (rule negative_eq_positive')
1.185
1.186  lemma zle_iff_zadd: "(w \<le> z) = (\<exists>n. z = w + int n)"
1.188 -  fix a b c d
1.189 -  assume "w = Abs_Integ (intrel `` {(a,b)})" "z = Abs_Integ (intrel `` {(c,d)})"
1.190 -  show "(a+d \<le> c+b) = (\<exists>n. c+b = a+n+d)"
1.191 -  proof
1.192 -    assume "a + d \<le> c + b"
1.193 -    thus "\<exists>n. c + b = a + n + d"
1.194 -      by (auto intro!: exI [where x="c+b - (a+d)"])
1.195 -  next
1.196 -    assume "\<exists>n. c + b = a + n + d"
1.197 -    then obtain n where "c + b = a + n + d" ..
1.198 -    thus "a + d \<le> c + b" by arith
1.199 -  qed
1.200 -qed
1.201 +unfolding int_eq_of_nat by (rule zle_iff_zadd')
1.202
1.203  lemma abs_int_eq [simp]: "abs (int m) = int m"
1.205 +unfolding int_eq_of_nat by (rule abs_of_nat)
1.206
1.207  lemma not_neg_int [simp]: "~ neg(int n)"
1.209 +unfolding int_eq_of_nat by (rule not_neg_int_of_nat)
1.210
1.211  lemma neg_zminus_int [simp]: "neg(- (int (Suc n)))"
1.212 -by (simp add: neg_def neg_less_0_iff_less)
1.213 +unfolding int_eq_of_nat by (rule neg_zminus_int_of_nat)
1.214
1.215  lemma not_neg_nat: "~ neg z ==> int (nat z) = z"
1.216 -by (simp add: linorder_not_less neg_def)
1.217 -
1.218 -text{*Agreement with the specific embedding for the integers*}
1.219 -lemma int_eq_of_nat: "int = (of_nat :: nat => int)"
1.220 -proof
1.221 -  fix n
1.222 -  show "int n = of_nat n"  by (induct n, simp_all add: int_Suc add_ac)
1.223 -qed
1.224 +unfolding int_eq_of_nat by (rule not_neg_nat')
1.225
1.226  lemma of_int_int_eq [simp]: "of_int (int n) = of_nat n"
1.227  unfolding int_eq_of_nat by (rule of_int_of_nat_eq)
```