1.1 --- a/src/HOL/Integ/Int.thy Thu Feb 05 10:45:28 2004 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,409 +0,0 @@
1.4 -(* Title: Integ/Int.thy
1.5 - ID: $Id$
1.6 - Author: Lawrence C Paulson, Cambridge University Computer Laboratory
1.7 - Copyright 1998 University of Cambridge
1.8 -*)
1.9 -
1.10 -header {*Type "int" is an Ordered Ring and Other Lemmas*}
1.11 -
1.12 -theory Int = IntDef:
1.13 -
1.14 -constdefs
1.15 - nat :: "int => nat"
1.16 - "nat(Z) == if neg Z then 0 else (THE m. Z = int m)"
1.17 -
1.18 -defs (overloaded)
1.19 - zabs_def: "abs(i::int) == if i < 0 then -i else i"
1.20 -
1.21 -
1.22 -lemma int_0 [simp]: "int 0 = (0::int)"
1.23 -by (simp add: Zero_int_def)
1.24 -
1.25 -lemma int_1 [simp]: "int 1 = 1"
1.26 -by (simp add: One_int_def)
1.27 -
1.28 -lemma int_Suc0_eq_1: "int (Suc 0) = 1"
1.29 -by (simp add: One_int_def One_nat_def)
1.30 -
1.31 -lemma neg_eq_less_0: "neg x = (x < 0)"
1.32 -by (unfold zdiff_def zless_def, auto)
1.33 -
1.34 -lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"
1.35 -apply (unfold zle_def)
1.36 -apply (simp add: neg_eq_less_0)
1.37 -done
1.38 -
1.39 -subsection{*To simplify inequalities when Numeral1 can get simplified to 1*}
1.40 -
1.41 -lemma not_neg_0: "~ neg 0"
1.42 -by (simp add: One_int_def neg_eq_less_0)
1.43 -
1.44 -lemma not_neg_1: "~ neg 1"
1.45 -by (simp add: One_int_def neg_eq_less_0)
1.46 -
1.47 -lemma iszero_0: "iszero 0"
1.48 -by (simp add: iszero_def)
1.49 -
1.50 -lemma not_iszero_1: "~ iszero 1"
1.51 -by (simp only: Zero_int_def One_int_def One_nat_def iszero_def int_int_eq)
1.52 -
1.53 -
1.54 -subsection{*nat: magnitide of an integer, as a natural number*}
1.55 -
1.56 -lemma nat_int [simp]: "nat(int n) = n"
1.57 -by (unfold nat_def, auto)
1.58 -
1.59 -lemma nat_zero [simp]: "nat 0 = 0"
1.60 -apply (unfold Zero_int_def)
1.61 -apply (rule nat_int)
1.62 -done
1.63 -
1.64 -lemma neg_nat: "neg z ==> nat z = 0"
1.65 -by (unfold nat_def, auto)
1.66 -
1.67 -lemma not_neg_nat: "~ neg z ==> int (nat z) = z"
1.68 -apply (drule not_neg_eq_ge_0 [THEN iffD1])
1.69 -apply (drule zle_imp_zless_or_eq)
1.70 -apply (auto simp add: zless_iff_Suc_zadd)
1.71 -done
1.72 -
1.73 -lemma nat_0_le [simp]: "0 \<le> z ==> int (nat z) = z"
1.74 -by (simp add: neg_eq_less_0 zle_def not_neg_nat)
1.75 -
1.76 -lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0"
1.77 -by (auto simp add: order_le_less neg_eq_less_0 zle_def neg_nat)
1.78 -
1.79 -text{*An alternative condition is @{term "0 \<le> w"} *}
1.80 -lemma nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)"
1.81 -apply (subst zless_int [symmetric])
1.82 -apply (simp (no_asm_simp) add: not_neg_nat not_neg_eq_ge_0 order_le_less)
1.83 -apply (case_tac "neg w")
1.84 - apply (simp add: neg_eq_less_0 neg_nat)
1.85 - apply (blast intro: order_less_trans)
1.86 -apply (simp add: not_neg_nat)
1.87 -done
1.88 -
1.89 -lemma zless_nat_conj: "(nat w < nat z) = (0 < z & w < z)"
1.90 -apply (case_tac "0 < z")
1.91 -apply (auto simp add: nat_mono_iff linorder_not_less)
1.92 -done
1.93 -
1.94 -subsection{*Monotonicity results*}
1.95 -
1.96 -text{*Most are available in theory @{text Ring_and_Field}, but they are
1.97 - not yet available: we must prove @{text zadd_zless_mono} before we
1.98 - can prove that the integers are a ring.*}
1.99 -
1.100 -lemma zadd_right_cancel_zless [simp]: "(v+z < w+z) = (v < (w::int))"
1.101 -by (simp add: zless_def zdiff_def zadd_ac)
1.102 -
1.103 -lemma zadd_left_cancel_zless [simp]: "(z+v < z+w) = (v < (w::int))"
1.104 -by (simp add: zless_def zdiff_def zadd_ac)
1.105 -
1.106 -lemma zadd_right_cancel_zle [simp] : "(v+z \<le> w+z) = (v \<le> (w::int))"
1.107 -by (simp add: linorder_not_less [symmetric])
1.108 -
1.109 -lemma zadd_left_cancel_zle [simp] : "(z+v \<le> z+w) = (v \<le> (w::int))"
1.110 -by (simp add: linorder_not_less [symmetric])
1.111 -
1.112 -(*"v\<le>w ==> v+z \<le> w+z"*)
1.113 -lemmas zadd_zless_mono1 = zadd_right_cancel_zless [THEN iffD2, standard]
1.114 -
1.115 -(*"v\<le>w ==> z+v \<le> z+w"*)
1.116 -lemmas zadd_zless_mono2 = zadd_left_cancel_zless [THEN iffD2, standard]
1.117 -
1.118 -(*"v\<le>w ==> v+z \<le> w+z"*)
1.119 -lemmas zadd_zle_mono1 = zadd_right_cancel_zle [THEN iffD2, standard]
1.120 -
1.121 -(*"v\<le>w ==> z+v \<le> z+w"*)
1.122 -lemmas zadd_zle_mono2 = zadd_left_cancel_zle [THEN iffD2, standard]
1.123 -
1.124 -lemma zadd_zle_mono: "[| w'\<le>w; z'\<le>z |] ==> w' + z' \<le> w + (z::int)"
1.125 -by (erule zadd_zle_mono1 [THEN zle_trans], simp)
1.126 -
1.127 -lemma zadd_zless_mono: "[| w'<w; z'\<le>z |] ==> w' + z' < w + (z::int)"
1.128 -by (erule zadd_zless_mono1 [THEN order_less_le_trans], simp)
1.129 -
1.130 -
1.131 -subsection{*Strict Monotonicity of Multiplication*}
1.132 -
1.133 -text{*strict, in 1st argument; proof is by induction on k>0*}
1.134 -lemma zmult_zless_mono2_lemma: "i<j ==> 0<k --> int k * i < int k * j"
1.135 -apply (induct_tac "k", simp)
1.136 -apply (simp add: int_Suc)
1.137 -apply (case_tac "n=0")
1.138 -apply (simp_all add: zadd_zmult_distrib int_Suc0_eq_1 order_le_less)
1.139 -apply (simp_all add: zadd_zless_mono int_Suc0_eq_1 order_le_less)
1.140 -done
1.141 -
1.142 -lemma zmult_zless_mono2: "[| i<j; (0::int) < k |] ==> k*i < k*j"
1.143 -apply (rule_tac t = k in not_neg_nat [THEN subst])
1.144 -apply (erule_tac [2] zmult_zless_mono2_lemma [THEN mp])
1.145 -apply (simp add: not_neg_eq_ge_0 order_le_less)
1.146 -apply (frule conjI [THEN zless_nat_conj [THEN iffD2]], auto)
1.147 -done
1.148 -
1.149 -
1.150 -text{*The Integers Form an Ordered Ring*}
1.151 -instance int :: ordered_ring
1.152 -proof
1.153 - fix i j k :: int
1.154 - show "0 < (1::int)" by (rule int_0_less_1)
1.155 - show "i \<le> j ==> k + i \<le> k + j" by simp
1.156 - show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: zmult_zless_mono2)
1.157 - show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
1.158 -qed
1.159 -
1.160 -
1.161 -subsection{*Comparison laws*}
1.162 -
1.163 -text{*Legacy bindings: all are in theory @{text Ring_and_Field}.*}
1.164 -
1.165 -lemma zminus_zless_zminus: "(- x < - y) = (y < (x::int))"
1.166 - by (rule Ring_and_Field.neg_less_iff_less)
1.167 -
1.168 -lemma zminus_zle_zminus: "(- x \<le> - y) = (y \<le> (x::int))"
1.169 - by (rule Ring_and_Field.neg_le_iff_le)
1.170 -
1.171 -
1.172 -text{*The next several equations can make the simplifier loop!*}
1.173 -
1.174 -lemma zless_zminus: "(x < - y) = (y < - (x::int))"
1.175 - by (rule Ring_and_Field.less_minus_iff)
1.176 -
1.177 -lemma zminus_zless: "(- x < y) = (- y < (x::int))"
1.178 - by (rule Ring_and_Field.minus_less_iff)
1.179 -
1.180 -lemma zle_zminus: "(x \<le> - y) = (y \<le> - (x::int))"
1.181 - by (rule Ring_and_Field.le_minus_iff)
1.182 -
1.183 -lemma zminus_zle: "(- x \<le> y) = (- y \<le> (x::int))"
1.184 - by (rule Ring_and_Field.minus_le_iff)
1.185 -
1.186 -lemma equation_zminus: "(x = - y) = (y = - (x::int))"
1.187 - by (rule Ring_and_Field.equation_minus_iff)
1.188 -
1.189 -lemma zminus_equation: "(- x = y) = (- (y::int) = x)"
1.190 - by (rule Ring_and_Field.minus_equation_iff)
1.191 -
1.192 -
1.193 -subsection{*Lemmas about the Function @{term int} and Orderings*}
1.194 -
1.195 -lemma negative_zless_0: "- (int (Suc n)) < 0"
1.196 -by (simp add: zless_def)
1.197 -
1.198 -lemma negative_zless [iff]: "- (int (Suc n)) < int m"
1.199 -by (rule negative_zless_0 [THEN order_less_le_trans], simp)
1.200 -
1.201 -lemma negative_zle_0: "- int n \<le> 0"
1.202 -by (simp add: zminus_zle)
1.203 -
1.204 -lemma negative_zle [iff]: "- int n \<le> int m"
1.205 -by (simp add: zless_def zle_def zdiff_def zadd_int)
1.206 -
1.207 -lemma not_zle_0_negative [simp]: "~(0 \<le> - (int (Suc n)))"
1.208 -by (subst zle_zminus, simp)
1.209 -
1.210 -lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)"
1.211 -apply safe
1.212 -apply (drule_tac [2] zle_zminus [THEN iffD1])
1.213 -apply (auto dest: zle_trans [OF _ negative_zle_0])
1.214 -done
1.215 -
1.216 -lemma not_int_zless_negative [simp]: "~(int n < - int m)"
1.217 -by (simp add: zle_def [symmetric])
1.218 -
1.219 -lemma negative_eq_positive [simp]: "(- int n = int m) = (n = 0 & m = 0)"
1.220 -apply (rule iffI)
1.221 -apply (rule int_zle_neg [THEN iffD1])
1.222 -apply (drule sym)
1.223 -apply (simp_all (no_asm_simp))
1.224 -done
1.225 -
1.226 -lemma zle_iff_zadd: "(w \<le> z) = (\<exists>n. z = w + int n)"
1.227 -by (force intro: exI [of _ "0::nat"]
1.228 - intro!: not_sym [THEN not0_implies_Suc]
1.229 - simp add: zless_iff_Suc_zadd int_le_less)
1.230 -
1.231 -lemma abs_int_eq [simp]: "abs (int m) = int m"
1.232 -by (simp add: zabs_def)
1.233 -
1.234 -text{*This version is proved for all ordered rings, not just integers!
1.235 - It is proved here because attribute @{text arith_split} is not available
1.236 - in theory @{text Ring_and_Field}.
1.237 - But is it really better than just rewriting with @{text abs_if}?*}
1.238 -lemma abs_split [arith_split]:
1.239 - "P(abs(a::'a::ordered_ring)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
1.240 -by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
1.241 -
1.242 -
1.243 -subsection{*Misc Results*}
1.244 -
1.245 -lemma nat_zminus_int [simp]: "nat(- (int n)) = 0"
1.246 -apply (unfold nat_def)
1.247 -apply (auto simp add: neg_eq_less_0 zero_reorient zminus_zless)
1.248 -done
1.249 -
1.250 -lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)"
1.251 -apply (case_tac "neg z")
1.252 -apply (erule_tac [2] not_neg_nat [THEN subst])
1.253 -apply (auto simp add: neg_nat)
1.254 -apply (auto dest: order_less_trans simp add: neg_eq_less_0)
1.255 -done
1.256 -
1.257 -lemma zless_eq_neg: "(w<z) = neg(w-z)"
1.258 -by (simp add: zless_def)
1.259 -
1.260 -lemma eq_eq_iszero: "(w=z) = iszero(w-z)"
1.261 -by (simp add: iszero_def diff_eq_eq)
1.262 -
1.263 -lemma zle_eq_not_neg: "(w\<le>z) = (~ neg(z-w))"
1.264 -by (simp add: zle_def zless_def)
1.265 -
1.266 -
1.267 -subsection{*Monotonicity of Multiplication*}
1.268 -
1.269 -lemma zmult_zle_mono1: "[| i \<le> j; (0::int) \<le> k |] ==> i*k \<le> j*k"
1.270 - by (rule Ring_and_Field.mult_right_mono)
1.271 -
1.272 -lemma zmult_zle_mono1_neg: "[| i \<le> j; k \<le> (0::int) |] ==> j*k \<le> i*k"
1.273 - by (rule Ring_and_Field.mult_right_mono_neg)
1.274 -
1.275 -lemma zmult_zle_mono2: "[| i \<le> j; (0::int) \<le> k |] ==> k*i \<le> k*j"
1.276 - by (rule Ring_and_Field.mult_left_mono)
1.277 -
1.278 -lemma zmult_zle_mono2_neg: "[| i \<le> j; k \<le> (0::int) |] ==> k*j \<le> k*i"
1.279 - by (rule Ring_and_Field.mult_left_mono_neg)
1.280 -
1.281 -(* \<le> monotonicity, BOTH arguments*)
1.282 -lemma zmult_zle_mono:
1.283 - "[| i \<le> j; k \<le> l; (0::int) \<le> j; (0::int) \<le> k |] ==> i*k \<le> j*l"
1.284 - by (rule Ring_and_Field.mult_mono)
1.285 -
1.286 -lemma zmult_zless_mono1: "[| i<j; (0::int) < k |] ==> i*k < j*k"
1.287 - by (rule Ring_and_Field.mult_strict_right_mono)
1.288 -
1.289 -lemma zmult_zless_mono1_neg: "[| i<j; k < (0::int) |] ==> j*k < i*k"
1.290 - by (rule Ring_and_Field.mult_strict_right_mono_neg)
1.291 -
1.292 -lemma zmult_zless_mono2_neg: "[| i<j; k < (0::int) |] ==> k*j < k*i"
1.293 - by (rule Ring_and_Field.mult_strict_left_mono_neg)
1.294 -
1.295 -lemma zmult_eq_0_iff [iff]: "(m*n = (0::int)) = (m = 0 | n = 0)"
1.296 - by simp
1.297 -
1.298 -lemma zmult_zless_cancel2: "(m*k < n*k) = (((0::int) < k & m<n) | (k<0 & n<m))"
1.299 - by (rule Ring_and_Field.mult_less_cancel_right)
1.300 -
1.301 -lemma zmult_zless_cancel1:
1.302 - "(k*m < k*n) = (((0::int) < k & m<n) | (k < 0 & n<m))"
1.303 - by (rule Ring_and_Field.mult_less_cancel_left)
1.304 -
1.305 -lemma zmult_zle_cancel2:
1.306 - "(m*k \<le> n*k) = (((0::int) < k --> m\<le>n) & (k < 0 --> n\<le>m))"
1.307 - by (rule Ring_and_Field.mult_le_cancel_right)
1.308 -
1.309 -lemma zmult_zle_cancel1:
1.310 - "(k*m \<le> k*n) = (((0::int) < k --> m\<le>n) & (k < 0 --> n\<le>m))"
1.311 - by (rule Ring_and_Field.mult_le_cancel_left)
1.312 -
1.313 -lemma zmult_cancel2: "(m*k = n*k) = (k = (0::int) | m=n)"
1.314 - by (rule Ring_and_Field.mult_cancel_right)
1.315 -
1.316 -lemma zmult_cancel1 [simp]: "(k*m = k*n) = (k = (0::int) | m=n)"
1.317 - by (rule Ring_and_Field.mult_cancel_left)
1.318 -
1.319 -
1.320 -text{*A case theorem distinguishing non-negative and negative int*}
1.321 -
1.322 -lemma negD: "neg x ==> \<exists>n. x = - (int (Suc n))"
1.323 -by (auto simp add: neg_eq_less_0 zless_iff_Suc_zadd
1.324 - diff_eq_eq [symmetric] zdiff_def)
1.325 -
1.326 -lemma int_cases [cases type: int, case_names nonneg neg]:
1.327 - "[|!! n. z = int n ==> P; !! n. z = - (int (Suc n)) ==> P |] ==> P"
1.328 -apply (case_tac "neg z")
1.329 -apply (fast dest!: negD)
1.330 -apply (drule not_neg_nat [symmetric], auto)
1.331 -done
1.332 -
1.333 -lemma int_induct [induct type: int, case_names nonneg neg]:
1.334 - "[|!! n. P (int n); !!n. P (- (int (Suc n))) |] ==> P z"
1.335 - by (cases z) auto
1.336 -
1.337 -
1.338 -(*Legacy ML bindings, but no longer the structure Int.*)
1.339 -ML
1.340 -{*
1.341 -val zabs_def = thm "zabs_def"
1.342 -val nat_def = thm "nat_def"
1.343 -
1.344 -val int_0 = thm "int_0";
1.345 -val int_1 = thm "int_1";
1.346 -val int_Suc0_eq_1 = thm "int_Suc0_eq_1";
1.347 -val neg_eq_less_0 = thm "neg_eq_less_0";
1.348 -val not_neg_eq_ge_0 = thm "not_neg_eq_ge_0";
1.349 -val not_neg_0 = thm "not_neg_0";
1.350 -val not_neg_1 = thm "not_neg_1";
1.351 -val iszero_0 = thm "iszero_0";
1.352 -val not_iszero_1 = thm "not_iszero_1";
1.353 -val int_0_less_1 = thm "int_0_less_1";
1.354 -val int_0_neq_1 = thm "int_0_neq_1";
1.355 -val zless_eq_neg = thm "zless_eq_neg";
1.356 -val eq_eq_iszero = thm "eq_eq_iszero";
1.357 -val zle_eq_not_neg = thm "zle_eq_not_neg";
1.358 -val zadd_right_cancel_zless = thm "zadd_right_cancel_zless";
1.359 -val zadd_left_cancel_zless = thm "zadd_left_cancel_zless";
1.360 -val zadd_right_cancel_zle = thm "zadd_right_cancel_zle";
1.361 -val zadd_left_cancel_zle = thm "zadd_left_cancel_zle";
1.362 -val zadd_zless_mono1 = thm "zadd_zless_mono1";
1.363 -val zadd_zless_mono2 = thm "zadd_zless_mono2";
1.364 -val zadd_zle_mono1 = thm "zadd_zle_mono1";
1.365 -val zadd_zle_mono2 = thm "zadd_zle_mono2";
1.366 -val zadd_zle_mono = thm "zadd_zle_mono";
1.367 -val zadd_zless_mono = thm "zadd_zless_mono";
1.368 -val zminus_zless_zminus = thm "zminus_zless_zminus";
1.369 -val zminus_zle_zminus = thm "zminus_zle_zminus";
1.370 -val zless_zminus = thm "zless_zminus";
1.371 -val zminus_zless = thm "zminus_zless";
1.372 -val zle_zminus = thm "zle_zminus";
1.373 -val zminus_zle = thm "zminus_zle";
1.374 -val equation_zminus = thm "equation_zminus";
1.375 -val zminus_equation = thm "zminus_equation";
1.376 -val negative_zless = thm "negative_zless";
1.377 -val negative_zle = thm "negative_zle";
1.378 -val not_zle_0_negative = thm "not_zle_0_negative";
1.379 -val not_int_zless_negative = thm "not_int_zless_negative";
1.380 -val negative_eq_positive = thm "negative_eq_positive";
1.381 -val zle_iff_zadd = thm "zle_iff_zadd";
1.382 -val abs_int_eq = thm "abs_int_eq";
1.383 -val abs_split = thm"abs_split";
1.384 -val nat_int = thm "nat_int";
1.385 -val nat_zminus_int = thm "nat_zminus_int";
1.386 -val nat_zero = thm "nat_zero";
1.387 -val not_neg_nat = thm "not_neg_nat";
1.388 -val neg_nat = thm "neg_nat";
1.389 -val zless_nat_eq_int_zless = thm "zless_nat_eq_int_zless";
1.390 -val nat_0_le = thm "nat_0_le";
1.391 -val nat_le_0 = thm "nat_le_0";
1.392 -val zless_nat_conj = thm "zless_nat_conj";
1.393 -val int_cases = thm "int_cases";
1.394 -val zmult_zle_mono1 = thm "zmult_zle_mono1";
1.395 -val zmult_zle_mono1_neg = thm "zmult_zle_mono1_neg";
1.396 -val zmult_zle_mono2 = thm "zmult_zle_mono2";
1.397 -val zmult_zle_mono2_neg = thm "zmult_zle_mono2_neg";
1.398 -val zmult_zle_mono = thm "zmult_zle_mono";
1.399 -val zmult_zless_mono2 = thm "zmult_zless_mono2";
1.400 -val zmult_zless_mono1 = thm "zmult_zless_mono1";
1.401 -val zmult_zless_mono1_neg = thm "zmult_zless_mono1_neg";
1.402 -val zmult_zless_mono2_neg = thm "zmult_zless_mono2_neg";
1.403 -val zmult_eq_0_iff = thm "zmult_eq_0_iff";
1.404 -val zmult_zless_cancel2 = thm "zmult_zless_cancel2";
1.405 -val zmult_zless_cancel1 = thm "zmult_zless_cancel1";
1.406 -val zmult_zle_cancel2 = thm "zmult_zle_cancel2";
1.407 -val zmult_zle_cancel1 = thm "zmult_zle_cancel1";
1.408 -val zmult_cancel2 = thm "zmult_cancel2";
1.409 -val zmult_cancel1 = thm "zmult_cancel1";
1.410 -*}
1.411 -
1.412 -end