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.9  proof (cases w, cases z, simp add: le add int_of_nat_def)
    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.54 -  by (simp add: int_def add)
    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.58 -  by (simp add: zadd_int zadd_assoc [symmetric])
    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.73 -by (simp add: le add int_def linorder_not_le [symmetric]) 
    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.109 -by (simp add: One_int_def [folded int_def] zadd_int)
   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.155 -by (simp add: order_less_le)
   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.163 -by (simp add: minus_le_iff)
   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.179 -by (simp add: linorder_not_less)
   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.187 -proof (cases w, cases z, simp add: le add int_def)
   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.204 -by (simp add: abs_if)
   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.208 -by (simp add: neg_def)
   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)