src/HOL/IntDef.thy
changeset 23299 292b1cbd05dc
parent 23282 dfc459989d24
child 23303 6091e530ff77
     1.1 --- a/src/HOL/IntDef.thy	Sat Jun 09 00:28:47 2007 +0200
     1.2 +++ b/src/HOL/IntDef.thy	Sat Jun 09 02:38:51 2007 +0200
     1.3 @@ -28,10 +28,10 @@
     1.4    [code func del]: "int m = Abs_Integ (intrel `` {(m, 0)})"
     1.5  
     1.6  instance int :: zero
     1.7 -  Zero_int_def: "0 \<equiv> int 0" ..
     1.8 +  Zero_int_def: "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})" ..
     1.9  
    1.10  instance int :: one
    1.11 -  One_int_def: "1 \<equiv> int 1" ..
    1.12 +  One_int_def: "1 \<equiv> Abs_Integ (intrel `` {(1, 0)})" ..
    1.13  
    1.14  instance int :: plus
    1.15    add_int_def: "z + w \<equiv> Abs_Integ
    1.16 @@ -88,15 +88,6 @@
    1.17  done
    1.18  
    1.19  
    1.20 -subsubsection{*@{term int}: Embedding the Naturals into the Integers*}
    1.21 -
    1.22 -lemma inj_int: "inj int"
    1.23 -by (simp add: inj_on_def int_def)
    1.24 -
    1.25 -lemma int_int_eq [iff]: "(int m = int n) = (m = n)"
    1.26 -by (fast elim!: inj_int [THEN injD])
    1.27 -
    1.28 -
    1.29  subsubsection{*Integer Unary Negation*}
    1.30  
    1.31  lemma minus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})"
    1.32 @@ -111,7 +102,7 @@
    1.33    by (cases z) (simp add: minus)
    1.34  
    1.35  lemma zminus_0: "- 0 = (0::int)"
    1.36 -  by (simp add: int_def Zero_int_def minus)
    1.37 +  by (simp add: Zero_int_def minus)
    1.38  
    1.39  
    1.40  subsection{*Integer Addition*}
    1.41 @@ -148,15 +139,9 @@
    1.42  
    1.43  lemmas zmult_ac = OrderedGroup.mult_ac
    1.44  
    1.45 -lemma zadd_int: "(int m) + (int n) = int (m + n)"
    1.46 -  by (simp add: int_def add)
    1.47 -
    1.48 -lemma zadd_int_left: "(int m) + (int n + z) = int (m + n) + z"
    1.49 -  by (simp add: zadd_int zadd_assoc [symmetric])
    1.50 -
    1.51  (*also for the instance declaration int :: comm_monoid_add*)
    1.52  lemma zadd_0: "(0::int) + z = z"
    1.53 -apply (simp add: Zero_int_def int_def)
    1.54 +apply (simp add: Zero_int_def)
    1.55  apply (cases z, simp add: add)
    1.56  done
    1.57  
    1.58 @@ -164,7 +149,7 @@
    1.59  by (rule trans [OF zadd_commute zadd_0])
    1.60  
    1.61  lemma zadd_zminus_inverse2: "(- z) + z = (0::int)"
    1.62 -by (cases z, simp add: int_def Zero_int_def minus add)
    1.63 +by (cases z, simp add: Zero_int_def minus add)
    1.64  
    1.65  
    1.66  subsection{*Integer Multiplication*}
    1.67 @@ -214,14 +199,9 @@
    1.68    zadd_zmult_distrib zadd_zmult_distrib2
    1.69    zdiff_zmult_distrib zdiff_zmult_distrib2
    1.70  
    1.71 -lemma int_mult: "int (m * n) = (int m) * (int n)"
    1.72 -by (simp add: int_def mult)
    1.73 -
    1.74 -text{*Compatibility binding*}
    1.75 -lemmas zmult_int = int_mult [symmetric]
    1.76  
    1.77  lemma zmult_1: "(1::int) * z = z"
    1.78 -by (cases z, simp add: One_int_def int_def mult)
    1.79 +by (cases z, simp add: One_int_def mult)
    1.80  
    1.81  lemma zmult_1_right: "z * (1::int) = z"
    1.82  by (rule trans [OF zmult_commute zmult_1])
    1.83 @@ -240,8 +220,7 @@
    1.84    show "i * j = j * i" by (rule zmult_commute)
    1.85    show "1 * i = i" by (rule zmult_1) 
    1.86    show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
    1.87 -  show "0 \<noteq> (1::int)"
    1.88 -    by (simp only: Zero_int_def One_int_def One_nat_def int_int_eq)
    1.89 +  show "0 \<noteq> (1::int)" by (simp add: Zero_int_def One_int_def)
    1.90  qed
    1.91  
    1.92  
    1.93 @@ -251,6 +230,10 @@
    1.94    "(Abs_Integ(intrel``{(x,y)}) \<le> Abs_Integ(intrel``{(u,v)})) = (x+v \<le> u+y)"
    1.95  by (force simp add: le_int_def)
    1.96  
    1.97 +lemma less:
    1.98 +  "(Abs_Integ(intrel``{(x,y)}) < Abs_Integ(intrel``{(u,v)})) = (x+v < u+y)"
    1.99 +by (simp add: less_int_def le order_less_le)
   1.100 +
   1.101  lemma zle_refl: "w \<le> (w::int)"
   1.102  by (cases w, simp add: le)
   1.103  
   1.104 @@ -274,81 +257,60 @@
   1.105  lemmas zless_linear = linorder_less_linear [where 'a = int]
   1.106  
   1.107  
   1.108 -lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)"
   1.109 -by (simp add: Zero_int_def)
   1.110 -
   1.111 -lemma zless_int [simp]: "(int m < int n) = (m<n)"
   1.112 -by (simp add: le add int_def linorder_not_le [symmetric]) 
   1.113 -
   1.114 -lemma int_less_0_conv [simp]: "~ (int k < 0)"
   1.115 -by (simp add: Zero_int_def)
   1.116 -
   1.117 -lemma zero_less_int_conv [simp]: "(0 < int n) = (0 < n)"
   1.118 -by (simp add: Zero_int_def)
   1.119 -
   1.120  lemma int_0_less_1: "0 < (1::int)"
   1.121 -by (simp only: Zero_int_def One_int_def One_nat_def zless_int)
   1.122 +by (simp add: Zero_int_def One_int_def less)
   1.123  
   1.124  lemma int_0_neq_1 [simp]: "0 \<noteq> (1::int)"
   1.125 -by (simp only: Zero_int_def One_int_def One_nat_def int_int_eq)
   1.126 -
   1.127 -lemma zle_int [simp]: "(int m \<le> int n) = (m\<le>n)"
   1.128 -by (simp add: linorder_not_less [symmetric])
   1.129 -
   1.130 -lemma zero_zle_int [simp]: "(0 \<le> int n)"
   1.131 -by (simp add: Zero_int_def)
   1.132 -
   1.133 -lemma int_le_0_conv [simp]: "(int n \<le> 0) = (n = 0)"
   1.134 -by (simp add: Zero_int_def)
   1.135 -
   1.136 -lemma int_0 [simp]: "int 0 = (0::int)"
   1.137 -by (simp add: Zero_int_def)
   1.138 -
   1.139 -lemma int_1 [simp]: "int 1 = 1"
   1.140 -by (simp add: One_int_def)
   1.141 -
   1.142 -lemma int_Suc0_eq_1: "int (Suc 0) = 1"
   1.143 -by (simp add: One_int_def One_nat_def)
   1.144 -
   1.145 -lemma int_Suc: "int (Suc m) = 1 + (int m)"
   1.146 -by (simp add: One_int_def zadd_int)
   1.147 +by (rule int_0_less_1 [THEN less_imp_neq])
   1.148  
   1.149  
   1.150  subsection{*Monotonicity results*}
   1.151  
   1.152 +instance int :: pordered_cancel_ab_semigroup_add
   1.153 +proof
   1.154 +  fix a b c :: int
   1.155 +  show "a \<le> b \<Longrightarrow> c + a \<le> c + b"
   1.156 +    by (cases a, cases b, cases c, simp add: le add)
   1.157 +qed
   1.158 +
   1.159  lemma zadd_left_mono: "i \<le> j ==> k + i \<le> k + (j::int)"
   1.160 -by (cases i, cases j, cases k, simp add: le add)
   1.161 +by (rule add_left_mono)
   1.162  
   1.163  lemma zadd_strict_right_mono: "i < j ==> i + k < j + (k::int)"
   1.164 -apply (cases i, cases j, cases k)
   1.165 -apply (simp add: linorder_not_le [where 'a = int, symmetric]
   1.166 -                 linorder_not_le [where 'a = nat]  le add)
   1.167 -done
   1.168 +by (rule add_strict_right_mono)
   1.169  
   1.170  lemma zadd_zless_mono: "[| w'<w; z'\<le>z |] ==> w' + z' < w + (z::int)"
   1.171 -by (rule order_less_le_trans [OF zadd_strict_right_mono zadd_left_mono])
   1.172 +by (rule add_less_le_mono)
   1.173  
   1.174  
   1.175  subsection{*Strict Monotonicity of Multiplication*}
   1.176  
   1.177  text{*strict, in 1st argument; proof is by induction on k>0*}
   1.178  lemma zmult_zless_mono2_lemma:
   1.179 -     "i<j ==> 0<k ==> int k * i < int k * j"
   1.180 +     "(i::int)<j ==> 0<k ==> of_nat k * i < of_nat k * j"
   1.181  apply (induct "k", simp)
   1.182 -apply (simp add: int_Suc)
   1.183 +apply (simp add: left_distrib)
   1.184  apply (case_tac "k=0")
   1.185 -apply (simp_all add: zadd_zmult_distrib int_Suc0_eq_1 order_le_less)
   1.186 -apply (simp add: zadd_zless_mono int_Suc0_eq_1 order_le_less)
   1.187 +apply (simp_all add: add_strict_mono)
   1.188  done
   1.189  
   1.190 -lemma zero_le_imp_eq_int: "0 \<le> k ==> \<exists>n. k = int n"
   1.191 +lemma int_of_nat_def: "of_nat m = Abs_Integ (intrel `` {(m, 0)})"
   1.192 +by (induct m, simp_all add: Zero_int_def One_int_def add)
   1.193 +
   1.194 +lemma zero_le_imp_eq_int: "(0::int) \<le> k ==> \<exists>n. k = of_nat n"
   1.195  apply (cases k)
   1.196 -apply (auto simp add: le add int_def Zero_int_def)
   1.197 +apply (auto simp add: le add int_of_nat_def Zero_int_def)
   1.198 +apply (rule_tac x="x-y" in exI, simp)
   1.199 +done
   1.200 +
   1.201 +lemma zero_less_imp_eq_int: "(0::int) < k ==> \<exists>n>0. k = of_nat n"
   1.202 +apply (cases k)
   1.203 +apply (simp add: less int_of_nat_def Zero_int_def)
   1.204  apply (rule_tac x="x-y" in exI, simp)
   1.205  done
   1.206  
   1.207  lemma zmult_zless_mono2: "[| i<j;  (0::int) < k |] ==> k*i < k*j"
   1.208 -apply (frule order_less_imp_le [THEN zero_le_imp_eq_int])
   1.209 +apply (drule zero_less_imp_eq_int)
   1.210  apply (auto simp add: zmult_zless_mono2_lemma)
   1.211  done
   1.212  
   1.213 @@ -361,21 +323,75 @@
   1.214    by intro_classes
   1.215      (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
   1.216  
   1.217 -text{*The integers form an ordered @{text comm_ring_1}*}
   1.218 +text{*The integers form an ordered integral domain*}
   1.219  instance int :: ordered_idom
   1.220  proof
   1.221    fix i j k :: int
   1.222 -  show "i \<le> j ==> k + i \<le> k + j" by (rule zadd_left_mono)
   1.223    show "i < j ==> 0 < k ==> k * i < k * j" by (rule zmult_zless_mono2)
   1.224    show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
   1.225  qed
   1.226  
   1.227  lemma zless_imp_add1_zle: "w<z ==> w + (1::int) \<le> z"
   1.228  apply (cases w, cases z) 
   1.229 -apply (simp add: linorder_not_le [symmetric] le int_def add One_int_def)
   1.230 +apply (simp add: less le add One_int_def)
   1.231  done
   1.232  
   1.233 -subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*}
   1.234 +
   1.235 +subsection{*@{term int}: Embedding the Naturals into the Integers*}
   1.236 +
   1.237 +lemma inj_int: "inj int"
   1.238 +by (simp add: inj_on_def int_def)
   1.239 +
   1.240 +lemma int_int_eq [iff]: "(int m = int n) = (m = n)"
   1.241 +by (fast elim!: inj_int [THEN injD])
   1.242 +
   1.243 +lemma zadd_int: "(int m) + (int n) = int (m + n)"
   1.244 +  by (simp add: int_def add)
   1.245 +
   1.246 +lemma zadd_int_left: "(int m) + (int n + z) = int (m + n) + z"
   1.247 +  by (simp add: zadd_int zadd_assoc [symmetric])
   1.248 +
   1.249 +lemma int_mult: "int (m * n) = (int m) * (int n)"
   1.250 +by (simp add: int_def mult)
   1.251 +
   1.252 +text{*Compatibility binding*}
   1.253 +lemmas zmult_int = int_mult [symmetric]
   1.254 +
   1.255 +lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)"
   1.256 +by (simp add: Zero_int_def [folded int_def])
   1.257 +
   1.258 +lemma zless_int [simp]: "(int m < int n) = (m<n)"
   1.259 +by (simp add: le add int_def linorder_not_le [symmetric]) 
   1.260 +
   1.261 +lemma int_less_0_conv [simp]: "~ (int k < 0)"
   1.262 +by (simp add: Zero_int_def [folded int_def])
   1.263 +
   1.264 +lemma zero_less_int_conv [simp]: "(0 < int n) = (0 < n)"
   1.265 +by (simp add: Zero_int_def [folded int_def])
   1.266 +
   1.267 +lemma zle_int [simp]: "(int m \<le> int n) = (m\<le>n)"
   1.268 +by (simp add: linorder_not_less [symmetric])
   1.269 +
   1.270 +lemma zero_zle_int [simp]: "(0 \<le> int n)"
   1.271 +by (simp add: Zero_int_def [folded int_def])
   1.272 +
   1.273 +lemma int_le_0_conv [simp]: "(int n \<le> 0) = (n = 0)"
   1.274 +by (simp add: Zero_int_def [folded int_def])
   1.275 +
   1.276 +lemma int_0 [simp]: "int 0 = (0::int)"
   1.277 +by (simp add: Zero_int_def [folded int_def])
   1.278 +
   1.279 +lemma int_1 [simp]: "int 1 = 1"
   1.280 +by (simp add: One_int_def [folded int_def])
   1.281 +
   1.282 +lemma int_Suc0_eq_1: "int (Suc 0) = 1"
   1.283 +by (simp add: One_int_def [folded int_def])
   1.284 +
   1.285 +lemma int_Suc: "int (Suc m) = 1 + (int m)"
   1.286 +by (simp add: One_int_def [folded int_def] zadd_int)
   1.287 +
   1.288 +
   1.289 +subsection{*Magnitude of an Integer, as a Natural Number: @{term nat}*}
   1.290  
   1.291  definition
   1.292    nat :: "int \<Rightarrow> nat"
   1.293 @@ -394,7 +410,7 @@
   1.294  by (simp add: nat int_def) 
   1.295  
   1.296  lemma nat_zero [simp]: "nat 0 = 0"
   1.297 -by (simp only: Zero_int_def nat_int)
   1.298 +by (simp only: Zero_int_def [folded int_def] nat_int)
   1.299  
   1.300  lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
   1.301  by (cases z, simp add: nat le int_def Zero_int_def)
   1.302 @@ -688,7 +704,7 @@
   1.303  lemma of_int_eq_id [simp]: "of_int = (id :: int => int)"
   1.304  proof
   1.305    fix z
   1.306 -  show "of_int z = id z"  
   1.307 +  show "of_int z = id z"
   1.308      by (cases z)
   1.309        (simp add: of_int add minus int_eq_of_nat [symmetric] int_def diff_minus)
   1.310  qed