src/HOL/Integ/IntArith.thy
 author paulson Thu Dec 04 10:29:17 2003 +0100 (2003-12-04) changeset 14272 5efbb548107d parent 14271 8ed6989228bb child 14295 7f115e5c5de4 permissions -rw-r--r--
Tidying of the integer development; towards removing the
abel_cancel simproc
 paulson@14259 ` 1` ```(* Title: HOL/Integ/IntArith.thy ``` paulson@14259 ` 2` ``` ID: \$Id\$ ``` paulson@14259 ` 3` ``` Authors: Larry Paulson and Tobias Nipkow ``` paulson@14259 ` 4` ```*) ``` wenzelm@12023 ` 5` wenzelm@12023 ` 6` ```header {* Integer arithmetic *} ``` wenzelm@12023 ` 7` wenzelm@9436 ` 8` ```theory IntArith = Bin ``` paulson@14259 ` 9` ```files ("int_arith1.ML"): ``` wenzelm@9436 ` 10` paulson@14272 ` 11` ```subsection{*Inequality Reasoning for the Arithmetic Simproc*} ``` paulson@14272 ` 12` paulson@14272 ` 13` ```lemma zless_imp_add1_zle: "w w + (1::int) \ z" ``` paulson@14272 ` 14` ``` proof (auto simp add: zle_def zless_iff_Suc_zadd) ``` paulson@14272 ` 15` ``` fix m n ``` paulson@14272 ` 16` ``` assume "w + 1 = w + (1 + int m) + (1 + int n)" ``` paulson@14272 ` 17` ``` hence "(w + 1) + (1 + int (m + n)) = (w + 1) + 0" ``` paulson@14272 ` 18` ``` by (simp add: add_ac zadd_int [symmetric]) ``` paulson@14272 ` 19` ``` hence "int (Suc(m+n)) = 0" ``` paulson@14272 ` 20` ``` by (simp only: Ring_and_Field.add_left_cancel int_Suc) ``` paulson@14272 ` 21` ``` thus False by (simp only: int_eq_0_conv) ``` paulson@14272 ` 22` ``` qed ``` paulson@14272 ` 23` wenzelm@12023 ` 24` ```use "int_arith1.ML" ``` wenzelm@12023 ` 25` ```setup int_arith_setup ``` paulson@14259 ` 26` paulson@14272 ` 27` ```subsection{*More inequality reasoning*} ``` paulson@14272 ` 28` paulson@14272 ` 29` ```lemma zless_add1_eq: "(w < z + (1::int)) = (w z) = (w z - (1::int)) = (w<(z::int))" ``` paulson@14272 ` 36` ```by arith ``` paulson@14272 ` 37` paulson@14272 ` 38` ```lemma zle_add1_eq_le [simp]: "(w < z + 1) = (w\(z::int))" ``` paulson@14259 ` 39` ```by arith ``` paulson@14259 ` 40` paulson@14259 ` 41` ```lemma zadd_left_cancel0 [simp]: "(z = z + w) = (w = (0::int))" ``` paulson@14259 ` 42` ```by arith ``` paulson@14259 ` 43` paulson@14259 ` 44` ```subsection{*Results about @{term nat}*} ``` paulson@14259 ` 45` paulson@14272 ` 46` ```lemma nonneg_eq_int: "[| 0 \ z; !!m. z = int m ==> P |] ==> P" ``` paulson@14259 ` 47` ```by (blast dest: nat_0_le sym) ``` paulson@14259 ` 48` paulson@14272 ` 49` ```lemma nat_eq_iff: "(nat w = m) = (if 0 \ w then w = int m else m=0)" ``` paulson@14259 ` 50` ```by auto ``` paulson@14259 ` 51` paulson@14272 ` 52` ```lemma nat_eq_iff2: "(m = nat w) = (if 0 \ w then w = int m else m=0)" ``` paulson@14259 ` 53` ```by auto ``` paulson@14259 ` 54` paulson@14272 ` 55` ```lemma nat_less_iff: "0 \ w ==> (nat w < m) = (w < int m)" ``` paulson@14259 ` 56` ```apply (rule iffI) ``` paulson@14259 ` 57` ```apply (erule nat_0_le [THEN subst]) ``` paulson@14259 ` 58` ```apply (simp_all del: zless_int add: zless_int [symmetric]) ``` paulson@14259 ` 59` ```done ``` paulson@14259 ` 60` paulson@14272 ` 61` ```lemma int_eq_iff: "(int m = z) = (m = nat z & 0 \ z)" ``` paulson@14259 ` 62` ```by (auto simp add: nat_eq_iff2) ``` paulson@14259 ` 63` paulson@14259 ` 64` paulson@14259 ` 65` ```(*Users don't want to see (int 0), int(Suc 0) or w + - z*) ``` paulson@14259 ` 66` ```declare Zero_int_def [symmetric, simp] ``` paulson@14259 ` 67` ```declare One_int_def [symmetric, simp] ``` paulson@14259 ` 68` paulson@14259 ` 69` ```text{*cooper.ML refers to this theorem*} ``` paulson@14259 ` 70` ```lemmas zdiff_def_symmetric = zdiff_def [symmetric, simp] ``` paulson@14259 ` 71` paulson@14259 ` 72` ```lemma nat_0: "nat 0 = 0" ``` paulson@14259 ` 73` ```by (simp add: nat_eq_iff) ``` paulson@14259 ` 74` paulson@14259 ` 75` ```lemma nat_1: "nat 1 = Suc 0" ``` paulson@14259 ` 76` ```by (subst nat_eq_iff, simp) ``` paulson@14259 ` 77` paulson@14259 ` 78` ```lemma nat_2: "nat 2 = Suc (Suc 0)" ``` paulson@14259 ` 79` ```by (subst nat_eq_iff, simp) ``` paulson@14259 ` 80` paulson@14272 ` 81` ```lemma nat_less_eq_zless: "0 \ w ==> (nat w < nat z) = (w z ==> (nat w \ nat z) = (w\z)" ``` paulson@14259 ` 88` ```by (auto simp add: linorder_not_less [symmetric] zless_nat_conj) ``` paulson@14259 ` 89` paulson@14259 ` 90` ```subsection{*@{term abs}: Absolute Value, as an Integer*} ``` paulson@14259 ` 91` paulson@14259 ` 92` ```(* Simpler: use zabs_def as rewrite rule ``` paulson@14259 ` 93` ``` but arith_tac is not parameterized by such simp rules ``` paulson@14259 ` 94` ```*) ``` paulson@14259 ` 95` paulson@14272 ` 96` ```lemma zabs_split: "P(abs(i::int)) = ((0 \ i --> P i) & (i < 0 --> P(-i)))" ``` paulson@14259 ` 97` ```by (simp add: zabs_def) ``` paulson@14259 ` 98` paulson@14272 ` 99` ```lemma zero_le_zabs [iff]: "0 \ abs (z::int)" ``` paulson@14259 ` 100` ```by (simp add: zabs_def) ``` paulson@14259 ` 101` paulson@14259 ` 102` paulson@14259 ` 103` ```text{*This simplifies expressions of the form @{term "int n = z"} where ``` paulson@14259 ` 104` ``` z is an integer literal.*} ``` paulson@14259 ` 105` ```declare int_eq_iff [of _ "number_of v", standard, simp] ``` paulson@13837 ` 106` wenzelm@12023 ` 107` ```declare zabs_split [arith_split] ``` wenzelm@12023 ` 108` paulson@13837 ` 109` ```lemma zabs_eq_iff: ``` paulson@14272 ` 110` ``` "(abs (z::int) = w) = (z = w \ 0 \ z \ z = -w \ z < 0)" ``` paulson@13837 ` 111` ``` by (auto simp add: zabs_def) ``` paulson@13837 ` 112` paulson@13849 ` 113` ```lemma int_nat_eq [simp]: "int (nat z) = (if 0 \ z then z else 0)" ``` paulson@13849 ` 114` ``` by simp ``` paulson@13849 ` 115` nipkow@13575 ` 116` ```lemma split_nat[arith_split]: ``` paulson@14259 ` 117` ``` "P(nat(i::int)) = ((\n. i = int n \ P n) & (i < 0 \ P 0))" ``` nipkow@13575 ` 118` ``` (is "?P = (?L & ?R)") ``` nipkow@13575 ` 119` ```proof (cases "i < 0") ``` nipkow@13575 ` 120` ``` case True thus ?thesis by simp ``` nipkow@13575 ` 121` ```next ``` nipkow@13575 ` 122` ``` case False ``` nipkow@13575 ` 123` ``` have "?P = ?L" ``` nipkow@13575 ` 124` ``` proof ``` nipkow@13575 ` 125` ``` assume ?P thus ?L using False by clarsimp ``` nipkow@13575 ` 126` ``` next ``` nipkow@13575 ` 127` ``` assume ?L thus ?P using False by simp ``` nipkow@13575 ` 128` ``` qed ``` nipkow@13575 ` 129` ``` with False show ?thesis by simp ``` nipkow@13575 ` 130` ```qed ``` nipkow@13575 ` 131` nipkow@13685 ` 132` ```subsubsection "Induction principles for int" ``` nipkow@13685 ` 133` nipkow@13685 ` 134` ``` (* `set:int': dummy construction *) ``` nipkow@13685 ` 135` ```theorem int_ge_induct[case_names base step,induct set:int]: ``` nipkow@13685 ` 136` ``` assumes ge: "k \ (i::int)" and ``` nipkow@13685 ` 137` ``` base: "P(k)" and ``` nipkow@13685 ` 138` ``` step: "\i. \k \ i; P i\ \ P(i+1)" ``` nipkow@13685 ` 139` ``` shows "P i" ``` nipkow@13685 ` 140` ```proof - ``` paulson@14272 ` 141` ``` { fix n have "\i::int. n = nat(i-k) \ k \ i \ P i" ``` nipkow@13685 ` 142` ``` proof (induct n) ``` nipkow@13685 ` 143` ``` case 0 ``` nipkow@13685 ` 144` ``` hence "i = k" by arith ``` nipkow@13685 ` 145` ``` thus "P i" using base by simp ``` nipkow@13685 ` 146` ``` next ``` nipkow@13685 ` 147` ``` case (Suc n) ``` nipkow@13685 ` 148` ``` hence "n = nat((i - 1) - k)" by arith ``` nipkow@13685 ` 149` ``` moreover ``` nipkow@13685 ` 150` ``` have ki1: "k \ i - 1" using Suc.prems by arith ``` nipkow@13685 ` 151` ``` ultimately ``` nipkow@13685 ` 152` ``` have "P(i - 1)" by(rule Suc.hyps) ``` nipkow@13685 ` 153` ``` from step[OF ki1 this] show ?case by simp ``` nipkow@13685 ` 154` ``` qed ``` nipkow@13685 ` 155` ``` } ``` nipkow@13685 ` 156` ``` from this ge show ?thesis by fast ``` nipkow@13685 ` 157` ```qed ``` nipkow@13685 ` 158` nipkow@13685 ` 159` ``` (* `set:int': dummy construction *) ``` nipkow@13685 ` 160` ```theorem int_gr_induct[case_names base step,induct set:int]: ``` nipkow@13685 ` 161` ``` assumes gr: "k < (i::int)" and ``` nipkow@13685 ` 162` ``` base: "P(k+1)" and ``` nipkow@13685 ` 163` ``` step: "\i. \k < i; P i\ \ P(i+1)" ``` nipkow@13685 ` 164` ``` shows "P i" ``` nipkow@13685 ` 165` ```apply(rule int_ge_induct[of "k + 1"]) ``` nipkow@13685 ` 166` ``` using gr apply arith ``` nipkow@13685 ` 167` ``` apply(rule base) ``` paulson@14259 ` 168` ```apply (rule step, simp+) ``` nipkow@13685 ` 169` ```done ``` nipkow@13685 ` 170` nipkow@13685 ` 171` ```theorem int_le_induct[consumes 1,case_names base step]: ``` nipkow@13685 ` 172` ``` assumes le: "i \ (k::int)" and ``` nipkow@13685 ` 173` ``` base: "P(k)" and ``` nipkow@13685 ` 174` ``` step: "\i. \i \ k; P i\ \ P(i - 1)" ``` nipkow@13685 ` 175` ``` shows "P i" ``` nipkow@13685 ` 176` ```proof - ``` paulson@14272 ` 177` ``` { fix n have "\i::int. n = nat(k-i) \ i \ k \ P i" ``` nipkow@13685 ` 178` ``` proof (induct n) ``` nipkow@13685 ` 179` ``` case 0 ``` nipkow@13685 ` 180` ``` hence "i = k" by arith ``` nipkow@13685 ` 181` ``` thus "P i" using base by simp ``` nipkow@13685 ` 182` ``` next ``` nipkow@13685 ` 183` ``` case (Suc n) ``` nipkow@13685 ` 184` ``` hence "n = nat(k - (i+1))" by arith ``` nipkow@13685 ` 185` ``` moreover ``` nipkow@13685 ` 186` ``` have ki1: "i + 1 \ k" using Suc.prems by arith ``` nipkow@13685 ` 187` ``` ultimately ``` nipkow@13685 ` 188` ``` have "P(i+1)" by(rule Suc.hyps) ``` nipkow@13685 ` 189` ``` from step[OF ki1 this] show ?case by simp ``` nipkow@13685 ` 190` ``` qed ``` nipkow@13685 ` 191` ``` } ``` nipkow@13685 ` 192` ``` from this le show ?thesis by fast ``` nipkow@13685 ` 193` ```qed ``` nipkow@13685 ` 194` nipkow@13685 ` 195` ```theorem int_less_induct[consumes 1,case_names base step]: ``` nipkow@13685 ` 196` ``` assumes less: "(i::int) < k" and ``` nipkow@13685 ` 197` ``` base: "P(k - 1)" and ``` nipkow@13685 ` 198` ``` step: "\i. \i < k; P i\ \ P(i - 1)" ``` nipkow@13685 ` 199` ``` shows "P i" ``` nipkow@13685 ` 200` ```apply(rule int_le_induct[of _ "k - 1"]) ``` nipkow@13685 ` 201` ``` using less apply arith ``` nipkow@13685 ` 202` ``` apply(rule base) ``` paulson@14259 ` 203` ```apply (rule step, simp+) ``` paulson@14259 ` 204` ```done ``` paulson@14259 ` 205` paulson@14259 ` 206` ```subsection{*Simple Equations*} ``` paulson@14259 ` 207` paulson@14259 ` 208` ```lemma int_diff_minus_eq [simp]: "x - - y = x + (y::int)" ``` paulson@14259 ` 209` ```by simp ``` paulson@14259 ` 210` paulson@14259 ` 211` ```lemma abs_abs [simp]: "abs(abs(x::int)) = abs(x)" ``` paulson@14259 ` 212` ```by arith ``` paulson@14259 ` 213` paulson@14259 ` 214` ```lemma abs_minus [simp]: "abs(-(x::int)) = abs(x)" ``` paulson@14259 ` 215` ```by arith ``` paulson@14259 ` 216` paulson@14272 ` 217` ```lemma triangle_ineq: "abs(x+y) \ abs(x) + abs(y::int)" ``` paulson@14259 ` 218` ```by arith ``` paulson@14259 ` 219` paulson@14259 ` 220` paulson@14259 ` 221` ```subsection{*Intermediate value theorems*} ``` paulson@14259 ` 222` paulson@14259 ` 223` ```lemma int_val_lemma: ``` paulson@14259 ` 224` ``` "(\i 1) --> ``` paulson@14259 ` 225` ``` f 0 \ k --> k \ f n --> (\i \ n. f i = (k::int))" ``` paulson@14271 ` 226` ```apply (induct_tac "n", simp) ``` paulson@14259 ` 227` ```apply (intro strip) ``` paulson@14259 ` 228` ```apply (erule impE, simp) ``` paulson@14259 ` 229` ```apply (erule_tac x = n in allE, simp) ``` paulson@14259 ` 230` ```apply (case_tac "k = f (n+1) ") ``` paulson@14259 ` 231` ``` apply force ``` paulson@14259 ` 232` ```apply (erule impE) ``` paulson@14259 ` 233` ``` apply (simp add: zabs_def split add: split_if_asm) ``` paulson@14259 ` 234` ```apply (blast intro: le_SucI) ``` paulson@14259 ` 235` ```done ``` paulson@14259 ` 236` paulson@14259 ` 237` ```lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)] ``` paulson@14259 ` 238` paulson@14259 ` 239` ```lemma nat_intermed_int_val: ``` paulson@14259 ` 240` ``` "[| \i. m \ i & i < n --> abs(f(i + 1::nat) - f i) \ 1; m < n; ``` paulson@14259 ` 241` ``` f m \ k; k \ f n |] ==> ? i. m \ i & i \ n & f i = (k::int)" ``` paulson@14259 ` 242` ```apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k ``` paulson@14259 ` 243` ``` in int_val_lemma) ``` paulson@14259 ` 244` ```apply simp ``` paulson@14259 ` 245` ```apply (erule impE) ``` paulson@14259 ` 246` ``` apply (intro strip) ``` paulson@14259 ` 247` ``` apply (erule_tac x = "i+m" in allE, arith) ``` paulson@14259 ` 248` ```apply (erule exE) ``` paulson@14259 ` 249` ```apply (rule_tac x = "i+m" in exI, arith) ``` paulson@14259 ` 250` ```done ``` paulson@14259 ` 251` paulson@14259 ` 252` paulson@14259 ` 253` ```subsection{*Some convenient biconditionals for products of signs*} ``` paulson@14259 ` 254` paulson@14259 ` 255` ```lemma zmult_pos: "[| (0::int) < i; 0 < j |] ==> 0 < i*j" ``` paulson@14266 ` 256` ``` by (rule Ring_and_Field.mult_pos) ``` paulson@14259 ` 257` paulson@14259 ` 258` ```lemma zmult_neg: "[| i < (0::int); j < 0 |] ==> 0 < i*j" ``` paulson@14266 ` 259` ``` by (rule Ring_and_Field.mult_neg) ``` paulson@14259 ` 260` paulson@14259 ` 261` ```lemma zmult_pos_neg: "[| (0::int) < i; j < 0 |] ==> i*j < 0" ``` paulson@14266 ` 262` ``` by (rule Ring_and_Field.mult_pos_neg) ``` paulson@14259 ` 263` paulson@14259 ` 264` ```lemma int_0_less_mult_iff: "((0::int) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)" ``` paulson@14266 ` 265` ``` by (rule Ring_and_Field.zero_less_mult_iff) ``` paulson@14259 ` 266` paulson@14259 ` 267` ```lemma int_0_le_mult_iff: "((0::int) \ x*y) = (0 \ x & 0 \ y | x \ 0 & y \ 0)" ``` paulson@14266 ` 268` ``` by (rule Ring_and_Field.zero_le_mult_iff) ``` paulson@14259 ` 269` paulson@14259 ` 270` ```lemma zmult_less_0_iff: "(x*y < (0::int)) = (0 < x & y < 0 | x < 0 & 0 < y)" ``` paulson@14266 ` 271` ``` by (rule Ring_and_Field.mult_less_0_iff) ``` paulson@14259 ` 272` paulson@14259 ` 273` ```lemma zmult_le_0_iff: "(x*y \ (0::int)) = (0 \ x & y \ 0 | x \ 0 & 0 \ y)" ``` paulson@14266 ` 274` ``` by (rule Ring_and_Field.mult_le_0_iff) ``` paulson@14259 ` 275` paulson@14259 ` 276` ```lemma abs_eq_0 [iff]: "(abs x = 0) = (x = (0::int))" ``` paulson@14266 ` 277` ``` by (rule Ring_and_Field.abs_eq_0) ``` paulson@14259 ` 278` paulson@14259 ` 279` ```lemma zero_less_abs_iff [iff]: "(0 < abs x) = (x ~= (0::int))" ``` paulson@14266 ` 280` ``` by (rule Ring_and_Field.zero_less_abs_iff) ``` paulson@14259 ` 281` paulson@14259 ` 282` ```lemma square_nonzero [simp]: "0 \ x * (x::int)" ``` paulson@14266 ` 283` ``` by (rule Ring_and_Field.zero_le_square) ``` paulson@14259 ` 284` paulson@14259 ` 285` paulson@14259 ` 286` ```subsection{*Products and 1, by T. M. Rasmussen*} ``` paulson@14259 ` 287` paulson@14259 ` 288` ```lemma zmult_eq_self_iff: "(m = m*(n::int)) = (n = 1 | m = 0)" ``` paulson@14259 ` 289` ```apply auto ``` paulson@14259 ` 290` ```apply (subgoal_tac "m*1 = m*n") ``` paulson@14259 ` 291` ```apply (drule zmult_cancel1 [THEN iffD1], auto) ``` nipkow@13685 ` 292` ```done ``` nipkow@13685 ` 293` paulson@14259 ` 294` ```lemma zless_1_zmult: "[| 1 < m; 1 < n |] ==> 1 < m*(n::int)" ``` paulson@14259 ` 295` ```apply (rule_tac y = "1*n" in order_less_trans) ``` paulson@14259 ` 296` ```apply (rule_tac [2] zmult_zless_mono1) ``` paulson@14259 ` 297` ```apply (simp_all (no_asm_simp)) ``` paulson@14259 ` 298` ```done ``` paulson@14259 ` 299` paulson@14259 ` 300` ```lemma pos_zmult_eq_1_iff: "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)" ``` paulson@14259 ` 301` ```apply auto ``` paulson@14259 ` 302` ```apply (case_tac "m=1") ``` paulson@14259 ` 303` ```apply (case_tac [2] "n=1") ``` paulson@14259 ` 304` ```apply (case_tac [4] "m=1") ``` paulson@14259 ` 305` ```apply (case_tac [5] "n=1", auto) ``` paulson@14259 ` 306` ```apply (tactic"distinct_subgoals_tac") ``` paulson@14259 ` 307` ```apply (subgoal_tac "1 m ==> int m - int n = int (m-n)" ``` paulson@14271 ` 328` ```by (induct m n rule: diff_induct, simp_all) ``` paulson@14271 ` 329` paulson@14259 ` 330` ```lemma nat_add_distrib: ``` paulson@14259 ` 331` ``` "[| (0::int) \ z; 0 \ z' |] ==> nat (z+z') = nat z + nat z'" ``` paulson@14259 ` 332` ```apply (rule inj_int [THEN injD]) ``` paulson@14271 ` 333` ```apply (simp add: zadd_int [symmetric]) ``` paulson@14259 ` 334` ```done ``` paulson@14259 ` 335` paulson@14259 ` 336` ```lemma nat_diff_distrib: ``` paulson@14259 ` 337` ``` "[| (0::int) \ z'; z' \ z |] ==> nat (z-z') = nat z - nat z'" ``` paulson@14259 ` 338` ```apply (rule inj_int [THEN injD]) ``` paulson@14271 ` 339` ```apply (simp add: zdiff_int [symmetric] nat_le_eq_zle) ``` paulson@14259 ` 340` ```done ``` paulson@14259 ` 341` paulson@14259 ` 342` ```lemma nat_mult_distrib: "(0::int) \ z ==> nat (z*z') = nat z * nat z'" ``` paulson@14259 ` 343` ```apply (case_tac "0 \ z'") ``` paulson@14259 ` 344` ```apply (rule inj_int [THEN injD]) ``` paulson@14271 ` 345` ```apply (simp add: zmult_int [symmetric] int_0_le_mult_iff) ``` paulson@14259 ` 346` ```apply (simp add: zmult_le_0_iff) ``` paulson@14259 ` 347` ```done ``` paulson@14259 ` 348` paulson@14259 ` 349` ```lemma nat_mult_distrib_neg: "z \ (0::int) ==> nat(z*z') = nat(-z) * nat(-z')" ``` paulson@14259 ` 350` ```apply (rule trans) ``` paulson@14259 ` 351` ```apply (rule_tac [2] nat_mult_distrib, auto) ``` paulson@14259 ` 352` ```done ``` paulson@14259 ` 353` paulson@14259 ` 354` ```lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)" ``` paulson@14259 ` 355` ```apply (case_tac "z=0 | w=0") ``` paulson@14259 ` 356` ```apply (auto simp add: zabs_def nat_mult_distrib [symmetric] ``` paulson@14259 ` 357` ``` nat_mult_distrib_neg [symmetric] zmult_less_0_iff) ``` paulson@14259 ` 358` ```done ``` paulson@14259 ` 359` paulson@14259 ` 360` ```ML ``` paulson@14259 ` 361` ```{* ``` paulson@14259 ` 362` ```val zle_diff1_eq = thm "zle_diff1_eq"; ``` paulson@14259 ` 363` ```val zle_add1_eq_le = thm "zle_add1_eq_le"; ``` paulson@14259 ` 364` ```val nonneg_eq_int = thm "nonneg_eq_int"; ``` paulson@14259 ` 365` ```val nat_eq_iff = thm "nat_eq_iff"; ``` paulson@14259 ` 366` ```val nat_eq_iff2 = thm "nat_eq_iff2"; ``` paulson@14259 ` 367` ```val nat_less_iff = thm "nat_less_iff"; ``` paulson@14259 ` 368` ```val int_eq_iff = thm "int_eq_iff"; ``` paulson@14259 ` 369` ```val nat_0 = thm "nat_0"; ``` paulson@14259 ` 370` ```val nat_1 = thm "nat_1"; ``` paulson@14259 ` 371` ```val nat_2 = thm "nat_2"; ``` paulson@14259 ` 372` ```val nat_less_eq_zless = thm "nat_less_eq_zless"; ``` paulson@14259 ` 373` ```val nat_le_eq_zle = thm "nat_le_eq_zle"; ``` paulson@14259 ` 374` ```val zabs_split = thm "zabs_split"; ``` paulson@14259 ` 375` ```val zero_le_zabs = thm "zero_le_zabs"; ``` paulson@14259 ` 376` paulson@14259 ` 377` ```val int_diff_minus_eq = thm "int_diff_minus_eq"; ``` paulson@14259 ` 378` ```val abs_abs = thm "abs_abs"; ``` paulson@14259 ` 379` ```val abs_minus = thm "abs_minus"; ``` paulson@14259 ` 380` ```val triangle_ineq = thm "triangle_ineq"; ``` paulson@14259 ` 381` ```val nat_intermed_int_val = thm "nat_intermed_int_val"; ``` paulson@14259 ` 382` ```val zmult_pos = thm "zmult_pos"; ``` paulson@14259 ` 383` ```val zmult_neg = thm "zmult_neg"; ``` paulson@14259 ` 384` ```val zmult_pos_neg = thm "zmult_pos_neg"; ``` paulson@14259 ` 385` ```val int_0_less_mult_iff = thm "int_0_less_mult_iff"; ``` paulson@14259 ` 386` ```val int_0_le_mult_iff = thm "int_0_le_mult_iff"; ``` paulson@14259 ` 387` ```val zmult_less_0_iff = thm "zmult_less_0_iff"; ``` paulson@14259 ` 388` ```val zmult_le_0_iff = thm "zmult_le_0_iff"; ``` paulson@14259 ` 389` ```val abs_mult = thm "abs_mult"; ``` paulson@14259 ` 390` ```val abs_eq_0 = thm "abs_eq_0"; ``` paulson@14259 ` 391` ```val zero_less_abs_iff = thm "zero_less_abs_iff"; ``` paulson@14259 ` 392` ```val square_nonzero = thm "square_nonzero"; ``` paulson@14259 ` 393` ```val zmult_eq_self_iff = thm "zmult_eq_self_iff"; ``` paulson@14259 ` 394` ```val zless_1_zmult = thm "zless_1_zmult"; ``` paulson@14259 ` 395` ```val pos_zmult_eq_1_iff = thm "pos_zmult_eq_1_iff"; ``` paulson@14259 ` 396` ```val zmult_eq_1_iff = thm "zmult_eq_1_iff"; ``` paulson@14259 ` 397` ```val nat_add_distrib = thm "nat_add_distrib"; ``` paulson@14259 ` 398` ```val nat_diff_distrib = thm "nat_diff_distrib"; ``` paulson@14259 ` 399` ```val nat_mult_distrib = thm "nat_mult_distrib"; ``` paulson@14259 ` 400` ```val nat_mult_distrib_neg = thm "nat_mult_distrib_neg"; ``` paulson@14259 ` 401` ```val nat_abs_mult_distrib = thm "nat_abs_mult_distrib"; ``` paulson@14259 ` 402` ```*} ``` paulson@14259 ` 403` wenzelm@7707 ` 404` ```end ```