src/HOL/Int.thy
 author huffman Sun Mar 25 20:15:39 2012 +0200 (2012-03-25) changeset 47108 2a1953f0d20d parent 46756 faf62905cd53 child 47192 0c0501cb6da6 permissions -rw-r--r--
merged fork with new numeral representation (see NEWS)
 wenzelm@41959 ` 1` ```(* Title: HOL/Int.thy ``` haftmann@25919 ` 2` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` wenzelm@41959 ` 3` ``` Author: Tobias Nipkow, Florian Haftmann, TU Muenchen ``` haftmann@25919 ` 4` ```*) ``` haftmann@25919 ` 5` haftmann@25919 ` 6` ```header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} ``` haftmann@25919 ` 7` haftmann@25919 ` 8` ```theory Int ``` huffman@47108 ` 9` ```imports Equiv_Relations Wellfounded ``` haftmann@25919 ` 10` ```uses ``` haftmann@25919 ` 11` ``` ("Tools/numeral.ML") ``` haftmann@31068 ` 12` ``` ("Tools/int_arith.ML") ``` haftmann@25919 ` 13` ```begin ``` haftmann@25919 ` 14` haftmann@25919 ` 15` ```subsection {* The equivalence relation underlying the integers *} ``` haftmann@25919 ` 16` haftmann@28661 ` 17` ```definition intrel :: "((nat \ nat) \ (nat \ nat)) set" where ``` haftmann@37767 ` 18` ``` "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }" ``` haftmann@25919 ` 19` wenzelm@45694 ` 20` ```definition "Integ = UNIV//intrel" ``` wenzelm@45694 ` 21` wenzelm@45694 ` 22` ```typedef (open) int = Integ ``` wenzelm@45694 ` 23` ``` morphisms Rep_Integ Abs_Integ ``` wenzelm@45694 ` 24` ``` unfolding Integ_def by (auto simp add: quotient_def) ``` haftmann@25919 ` 25` haftmann@25919 ` 26` ```instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}" ``` haftmann@25919 ` 27` ```begin ``` haftmann@25919 ` 28` haftmann@25919 ` 29` ```definition ``` haftmann@37767 ` 30` ``` Zero_int_def: "0 = Abs_Integ (intrel `` {(0, 0)})" ``` haftmann@25919 ` 31` haftmann@25919 ` 32` ```definition ``` haftmann@37767 ` 33` ``` One_int_def: "1 = Abs_Integ (intrel `` {(1, 0)})" ``` haftmann@25919 ` 34` haftmann@25919 ` 35` ```definition ``` haftmann@37767 ` 36` ``` add_int_def: "z + w = Abs_Integ ``` haftmann@25919 ` 37` ``` (\(x, y) \ Rep_Integ z. \(u, v) \ Rep_Integ w. ``` haftmann@25919 ` 38` ``` intrel `` {(x + u, y + v)})" ``` haftmann@25919 ` 39` haftmann@25919 ` 40` ```definition ``` haftmann@37767 ` 41` ``` minus_int_def: ``` haftmann@25919 ` 42` ``` "- z = Abs_Integ (\(x, y) \ Rep_Integ z. intrel `` {(y, x)})" ``` haftmann@25919 ` 43` haftmann@25919 ` 44` ```definition ``` haftmann@37767 ` 45` ``` diff_int_def: "z - w = z + (-w \ int)" ``` haftmann@25919 ` 46` haftmann@25919 ` 47` ```definition ``` haftmann@37767 ` 48` ``` mult_int_def: "z * w = Abs_Integ ``` haftmann@25919 ` 49` ``` (\(x, y) \ Rep_Integ z. \(u,v ) \ Rep_Integ w. ``` haftmann@25919 ` 50` ``` intrel `` {(x*u + y*v, x*v + y*u)})" ``` haftmann@25919 ` 51` haftmann@25919 ` 52` ```definition ``` haftmann@37767 ` 53` ``` le_int_def: ``` haftmann@25919 ` 54` ``` "z \ w \ (\x y u v. x+v \ u+y \ (x, y) \ Rep_Integ z \ (u, v) \ Rep_Integ w)" ``` haftmann@25919 ` 55` haftmann@25919 ` 56` ```definition ``` haftmann@37767 ` 57` ``` less_int_def: "(z\int) < w \ z \ w \ z \ w" ``` haftmann@25919 ` 58` haftmann@25919 ` 59` ```definition ``` haftmann@25919 ` 60` ``` zabs_def: "\i\int\ = (if i < 0 then - i else i)" ``` haftmann@25919 ` 61` haftmann@25919 ` 62` ```definition ``` haftmann@25919 ` 63` ``` zsgn_def: "sgn (i\int) = (if i=0 then 0 else if 0 intrel) = (x+v = u+y)" ``` haftmann@25919 ` 73` ```by (simp add: intrel_def) ``` haftmann@25919 ` 74` haftmann@25919 ` 75` ```lemma equiv_intrel: "equiv UNIV intrel" ``` nipkow@30198 ` 76` ```by (simp add: intrel_def equiv_def refl_on_def sym_def trans_def) ``` haftmann@25919 ` 77` haftmann@25919 ` 78` ```text{*Reduces equality of equivalence classes to the @{term intrel} relation: ``` haftmann@25919 ` 79` ``` @{term "(intrel `` {x} = intrel `` {y}) = ((x,y) \ intrel)"} *} ``` haftmann@25919 ` 80` ```lemmas equiv_intrel_iff [simp] = eq_equiv_class_iff [OF equiv_intrel UNIV_I UNIV_I] ``` haftmann@25919 ` 81` haftmann@25919 ` 82` ```text{*All equivalence classes belong to set of representatives*} ``` haftmann@25919 ` 83` ```lemma [simp]: "intrel``{(x,y)} \ Integ" ``` haftmann@25919 ` 84` ```by (auto simp add: Integ_def intrel_def quotient_def) ``` haftmann@25919 ` 85` haftmann@25919 ` 86` ```text{*Reduces equality on abstractions to equality on representatives: ``` haftmann@25919 ` 87` ``` @{prop "\x \ Integ; y \ Integ\ \ (Abs_Integ x = Abs_Integ y) = (x=y)"} *} ``` blanchet@35828 ` 88` ```declare Abs_Integ_inject [simp,no_atp] Abs_Integ_inverse [simp,no_atp] ``` haftmann@25919 ` 89` haftmann@25919 ` 90` ```text{*Case analysis on the representation of an integer as an equivalence ``` haftmann@25919 ` 91` ``` class of pairs of naturals.*} ``` haftmann@25919 ` 92` ```lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]: ``` haftmann@25919 ` 93` ``` "(!!x y. z = Abs_Integ(intrel``{(x,y)}) ==> P) ==> P" ``` haftmann@25919 ` 94` ```apply (rule Abs_Integ_cases [of z]) ``` haftmann@25919 ` 95` ```apply (auto simp add: Integ_def quotient_def) ``` haftmann@25919 ` 96` ```done ``` haftmann@25919 ` 97` haftmann@25919 ` 98` haftmann@25919 ` 99` ```subsection {* Arithmetic Operations *} ``` haftmann@25919 ` 100` haftmann@25919 ` 101` ```lemma minus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})" ``` haftmann@25919 ` 102` ```proof - ``` haftmann@25919 ` 103` ``` have "(\(x,y). intrel``{(y,x)}) respects intrel" ``` haftmann@40819 ` 104` ``` by (auto simp add: congruent_def) ``` haftmann@25919 ` 105` ``` thus ?thesis ``` haftmann@25919 ` 106` ``` by (simp add: minus_int_def UN_equiv_class [OF equiv_intrel]) ``` haftmann@25919 ` 107` ```qed ``` haftmann@25919 ` 108` haftmann@25919 ` 109` ```lemma add: ``` haftmann@25919 ` 110` ``` "Abs_Integ (intrel``{(x,y)}) + Abs_Integ (intrel``{(u,v)}) = ``` haftmann@25919 ` 111` ``` Abs_Integ (intrel``{(x+u, y+v)})" ``` haftmann@25919 ` 112` ```proof - ``` haftmann@25919 ` 113` ``` have "(\z w. (\(x,y). (\(u,v). intrel `` {(x+u, y+v)}) w) z) ``` haftmann@25919 ` 114` ``` respects2 intrel" ``` haftmann@40819 ` 115` ``` by (auto simp add: congruent2_def) ``` haftmann@25919 ` 116` ``` thus ?thesis ``` haftmann@25919 ` 117` ``` by (simp add: add_int_def UN_UN_split_split_eq ``` haftmann@25919 ` 118` ``` UN_equiv_class2 [OF equiv_intrel equiv_intrel]) ``` haftmann@25919 ` 119` ```qed ``` haftmann@25919 ` 120` haftmann@25919 ` 121` ```text{*Congruence property for multiplication*} ``` haftmann@25919 ` 122` ```lemma mult_congruent2: ``` haftmann@25919 ` 123` ``` "(%p1 p2. (%(x,y). (%(u,v). intrel``{(x*u + y*v, x*v + y*u)}) p2) p1) ``` haftmann@25919 ` 124` ``` respects2 intrel" ``` haftmann@25919 ` 125` ```apply (rule equiv_intrel [THEN congruent2_commuteI]) ``` haftmann@25919 ` 126` ``` apply (force simp add: mult_ac, clarify) ``` haftmann@25919 ` 127` ```apply (simp add: congruent_def mult_ac) ``` haftmann@25919 ` 128` ```apply (rename_tac u v w x y z) ``` haftmann@25919 ` 129` ```apply (subgoal_tac "u*y + x*y = w*y + v*y & u*z + x*z = w*z + v*z") ``` haftmann@25919 ` 130` ```apply (simp add: mult_ac) ``` haftmann@25919 ` 131` ```apply (simp add: add_mult_distrib [symmetric]) ``` haftmann@25919 ` 132` ```done ``` haftmann@25919 ` 133` haftmann@25919 ` 134` ```lemma mult: ``` haftmann@25919 ` 135` ``` "Abs_Integ((intrel``{(x,y)})) * Abs_Integ((intrel``{(u,v)})) = ``` haftmann@25919 ` 136` ``` Abs_Integ(intrel `` {(x*u + y*v, x*v + y*u)})" ``` haftmann@25919 ` 137` ```by (simp add: mult_int_def UN_UN_split_split_eq mult_congruent2 ``` haftmann@25919 ` 138` ``` UN_equiv_class2 [OF equiv_intrel equiv_intrel]) ``` haftmann@25919 ` 139` haftmann@25919 ` 140` ```text{*The integers form a @{text comm_ring_1}*} ``` haftmann@25919 ` 141` ```instance int :: comm_ring_1 ``` haftmann@25919 ` 142` ```proof ``` haftmann@25919 ` 143` ``` fix i j k :: int ``` haftmann@25919 ` 144` ``` show "(i + j) + k = i + (j + k)" ``` haftmann@25919 ` 145` ``` by (cases i, cases j, cases k) (simp add: add add_assoc) ``` haftmann@25919 ` 146` ``` show "i + j = j + i" ``` haftmann@25919 ` 147` ``` by (cases i, cases j) (simp add: add_ac add) ``` haftmann@25919 ` 148` ``` show "0 + i = i" ``` haftmann@25919 ` 149` ``` by (cases i) (simp add: Zero_int_def add) ``` haftmann@25919 ` 150` ``` show "- i + i = 0" ``` haftmann@25919 ` 151` ``` by (cases i) (simp add: Zero_int_def minus add) ``` haftmann@25919 ` 152` ``` show "i - j = i + - j" ``` haftmann@25919 ` 153` ``` by (simp add: diff_int_def) ``` haftmann@25919 ` 154` ``` show "(i * j) * k = i * (j * k)" ``` nipkow@29667 ` 155` ``` by (cases i, cases j, cases k) (simp add: mult algebra_simps) ``` haftmann@25919 ` 156` ``` show "i * j = j * i" ``` nipkow@29667 ` 157` ``` by (cases i, cases j) (simp add: mult algebra_simps) ``` haftmann@25919 ` 158` ``` show "1 * i = i" ``` haftmann@25919 ` 159` ``` by (cases i) (simp add: One_int_def mult) ``` haftmann@25919 ` 160` ``` show "(i + j) * k = i * k + j * k" ``` nipkow@29667 ` 161` ``` by (cases i, cases j, cases k) (simp add: add mult algebra_simps) ``` haftmann@25919 ` 162` ``` show "0 \ (1::int)" ``` haftmann@25919 ` 163` ``` by (simp add: Zero_int_def One_int_def) ``` haftmann@25919 ` 164` ```qed ``` haftmann@25919 ` 165` huffman@44709 ` 166` ```abbreviation int :: "nat \ int" where ``` huffman@44709 ` 167` ``` "int \ of_nat" ``` huffman@44709 ` 168` huffman@44709 ` 169` ```lemma int_def: "int m = Abs_Integ (intrel `` {(m, 0)})" ``` wenzelm@42676 ` 170` ```by (induct m) (simp_all add: Zero_int_def One_int_def add) ``` haftmann@25919 ` 171` haftmann@25919 ` 172` haftmann@25919 ` 173` ```subsection {* The @{text "\"} Ordering *} ``` haftmann@25919 ` 174` haftmann@25919 ` 175` ```lemma le: ``` haftmann@25919 ` 176` ``` "(Abs_Integ(intrel``{(x,y)}) \ Abs_Integ(intrel``{(u,v)})) = (x+v \ u+y)" ``` haftmann@25919 ` 177` ```by (force simp add: le_int_def) ``` haftmann@25919 ` 178` haftmann@25919 ` 179` ```lemma less: ``` haftmann@25919 ` 180` ``` "(Abs_Integ(intrel``{(x,y)}) < Abs_Integ(intrel``{(u,v)})) = (x+v < u+y)" ``` haftmann@25919 ` 181` ```by (simp add: less_int_def le order_less_le) ``` haftmann@25919 ` 182` haftmann@25919 ` 183` ```instance int :: linorder ``` haftmann@25919 ` 184` ```proof ``` haftmann@25919 ` 185` ``` fix i j k :: int ``` haftmann@27682 ` 186` ``` show antisym: "i \ j \ j \ i \ i = j" ``` haftmann@27682 ` 187` ``` by (cases i, cases j) (simp add: le) ``` haftmann@27682 ` 188` ``` show "(i < j) = (i \ j \ \ j \ i)" ``` haftmann@27682 ` 189` ``` by (auto simp add: less_int_def dest: antisym) ``` haftmann@25919 ` 190` ``` show "i \ i" ``` haftmann@25919 ` 191` ``` by (cases i) (simp add: le) ``` haftmann@25919 ` 192` ``` show "i \ j \ j \ k \ i \ k" ``` haftmann@25919 ` 193` ``` by (cases i, cases j, cases k) (simp add: le) ``` haftmann@25919 ` 194` ``` show "i \ j \ j \ i" ``` haftmann@25919 ` 195` ``` by (cases i, cases j) (simp add: le linorder_linear) ``` haftmann@25919 ` 196` ```qed ``` haftmann@25919 ` 197` haftmann@25919 ` 198` ```instantiation int :: distrib_lattice ``` haftmann@25919 ` 199` ```begin ``` haftmann@25919 ` 200` haftmann@25919 ` 201` ```definition ``` haftmann@25919 ` 202` ``` "(inf \ int \ int \ int) = min" ``` haftmann@25919 ` 203` haftmann@25919 ` 204` ```definition ``` haftmann@25919 ` 205` ``` "(sup \ int \ int \ int) = max" ``` haftmann@25919 ` 206` haftmann@25919 ` 207` ```instance ``` haftmann@25919 ` 208` ``` by intro_classes ``` haftmann@25919 ` 209` ``` (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1) ``` haftmann@25919 ` 210` haftmann@25919 ` 211` ```end ``` haftmann@25919 ` 212` haftmann@35028 ` 213` ```instance int :: ordered_cancel_ab_semigroup_add ``` haftmann@25919 ` 214` ```proof ``` haftmann@25919 ` 215` ``` fix i j k :: int ``` haftmann@25919 ` 216` ``` show "i \ j \ k + i \ k + j" ``` haftmann@25919 ` 217` ``` by (cases i, cases j, cases k) (simp add: le add) ``` haftmann@25919 ` 218` ```qed ``` haftmann@25919 ` 219` haftmann@25961 ` 220` haftmann@25919 ` 221` ```text{*Strict Monotonicity of Multiplication*} ``` haftmann@25919 ` 222` haftmann@25919 ` 223` ```text{*strict, in 1st argument; proof is by induction on k>0*} ``` haftmann@25919 ` 224` ```lemma zmult_zless_mono2_lemma: ``` huffman@44709 ` 225` ``` "(i::int) 0 int k * i < int k * j" ``` wenzelm@42676 ` 226` ```apply (induct k) ``` wenzelm@42676 ` 227` ```apply simp ``` haftmann@25919 ` 228` ```apply (simp add: left_distrib) ``` haftmann@25919 ` 229` ```apply (case_tac "k=0") ``` haftmann@25919 ` 230` ```apply (simp_all add: add_strict_mono) ``` haftmann@25919 ` 231` ```done ``` haftmann@25919 ` 232` huffman@44709 ` 233` ```lemma zero_le_imp_eq_int: "(0::int) \ k ==> \n. k = int n" ``` haftmann@25919 ` 234` ```apply (cases k) ``` haftmann@25919 ` 235` ```apply (auto simp add: le add int_def Zero_int_def) ``` haftmann@25919 ` 236` ```apply (rule_tac x="x-y" in exI, simp) ``` haftmann@25919 ` 237` ```done ``` haftmann@25919 ` 238` huffman@44709 ` 239` ```lemma zero_less_imp_eq_int: "(0::int) < k ==> \n>0. k = int n" ``` haftmann@25919 ` 240` ```apply (cases k) ``` haftmann@25919 ` 241` ```apply (simp add: less int_def Zero_int_def) ``` haftmann@25919 ` 242` ```apply (rule_tac x="x-y" in exI, simp) ``` haftmann@25919 ` 243` ```done ``` haftmann@25919 ` 244` haftmann@25919 ` 245` ```lemma zmult_zless_mono2: "[| i k*i < k*j" ``` haftmann@25919 ` 246` ```apply (drule zero_less_imp_eq_int) ``` haftmann@25919 ` 247` ```apply (auto simp add: zmult_zless_mono2_lemma) ``` haftmann@25919 ` 248` ```done ``` haftmann@25919 ` 249` haftmann@25919 ` 250` ```text{*The integers form an ordered integral domain*} ``` haftmann@35028 ` 251` ```instance int :: linordered_idom ``` haftmann@25919 ` 252` ```proof ``` haftmann@25919 ` 253` ``` fix i j k :: int ``` haftmann@25919 ` 254` ``` show "i < j \ 0 < k \ k * i < k * j" ``` haftmann@25919 ` 255` ``` by (rule zmult_zless_mono2) ``` haftmann@25919 ` 256` ``` show "\i\ = (if i < 0 then -i else i)" ``` haftmann@25919 ` 257` ``` by (simp only: zabs_def) ``` haftmann@25919 ` 258` ``` show "sgn (i\int) = (if i=0 then 0 else if 0 w + (1\int) \ z" ``` haftmann@25919 ` 263` ```apply (cases w, cases z) ``` haftmann@25919 ` 264` ```apply (simp add: less le add One_int_def) ``` haftmann@25919 ` 265` ```done ``` haftmann@25919 ` 266` haftmann@25919 ` 267` ```lemma zless_iff_Suc_zadd: ``` huffman@44709 ` 268` ``` "(w \ int) < z \ (\n. z = w + int (Suc n))" ``` haftmann@25919 ` 269` ```apply (cases z, cases w) ``` haftmann@25919 ` 270` ```apply (auto simp add: less add int_def) ``` haftmann@25919 ` 271` ```apply (rename_tac a b c d) ``` haftmann@25919 ` 272` ```apply (rule_tac x="a+d - Suc(c+b)" in exI) ``` haftmann@25919 ` 273` ```apply arith ``` haftmann@25919 ` 274` ```done ``` haftmann@25919 ` 275` haftmann@25919 ` 276` ```lemmas int_distrib = ``` wenzelm@45607 ` 277` ``` left_distrib [of z1 z2 w] ``` wenzelm@45607 ` 278` ``` right_distrib [of w z1 z2] ``` wenzelm@45607 ` 279` ``` left_diff_distrib [of z1 z2 w] ``` wenzelm@45607 ` 280` ``` right_diff_distrib [of w z1 z2] ``` wenzelm@45607 ` 281` ``` for z1 z2 w :: int ``` haftmann@25919 ` 282` haftmann@25919 ` 283` haftmann@25919 ` 284` ```subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*} ``` haftmann@25919 ` 285` haftmann@25919 ` 286` ```context ring_1 ``` haftmann@25919 ` 287` ```begin ``` haftmann@25919 ` 288` haftmann@31015 ` 289` ```definition of_int :: "int \ 'a" where ``` haftmann@39910 ` 290` ``` "of_int z = the_elem (\(i, j) \ Rep_Integ z. { of_nat i - of_nat j })" ``` haftmann@25919 ` 291` haftmann@25919 ` 292` ```lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j" ``` haftmann@25919 ` 293` ```proof - ``` haftmann@25919 ` 294` ``` have "(\(i,j). { of_nat i - (of_nat j :: 'a) }) respects intrel" ``` haftmann@40819 ` 295` ``` by (auto simp add: congruent_def) (simp add: algebra_simps of_nat_add [symmetric] ``` haftmann@25919 ` 296` ``` del: of_nat_add) ``` haftmann@25919 ` 297` ``` thus ?thesis ``` haftmann@25919 ` 298` ``` by (simp add: of_int_def UN_equiv_class [OF equiv_intrel]) ``` haftmann@25919 ` 299` ```qed ``` haftmann@25919 ` 300` haftmann@25919 ` 301` ```lemma of_int_0 [simp]: "of_int 0 = 0" ``` nipkow@29667 ` 302` ```by (simp add: of_int Zero_int_def) ``` haftmann@25919 ` 303` haftmann@25919 ` 304` ```lemma of_int_1 [simp]: "of_int 1 = 1" ``` nipkow@29667 ` 305` ```by (simp add: of_int One_int_def) ``` haftmann@25919 ` 306` haftmann@25919 ` 307` ```lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z" ``` wenzelm@42676 ` 308` ```by (cases w, cases z) (simp add: algebra_simps of_int add) ``` haftmann@25919 ` 309` haftmann@25919 ` 310` ```lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)" ``` wenzelm@42676 ` 311` ```by (cases z) (simp add: algebra_simps of_int minus) ``` haftmann@25919 ` 312` haftmann@25919 ` 313` ```lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z" ``` haftmann@35050 ` 314` ```by (simp add: diff_minus Groups.diff_minus) ``` haftmann@25919 ` 315` haftmann@25919 ` 316` ```lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z" ``` haftmann@25919 ` 317` ```apply (cases w, cases z) ``` nipkow@29667 ` 318` ```apply (simp add: algebra_simps of_int mult of_nat_mult) ``` haftmann@25919 ` 319` ```done ``` haftmann@25919 ` 320` haftmann@25919 ` 321` ```text{*Collapse nested embeddings*} ``` huffman@44709 ` 322` ```lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n" ``` nipkow@29667 ` 323` ```by (induct n) auto ``` haftmann@25919 ` 324` huffman@47108 ` 325` ```lemma of_int_numeral [simp, code_post]: "of_int (numeral k) = numeral k" ``` huffman@47108 ` 326` ``` by (simp add: of_nat_numeral [symmetric] of_int_of_nat_eq [symmetric]) ``` huffman@47108 ` 327` huffman@47108 ` 328` ```lemma of_int_neg_numeral [simp, code_post]: "of_int (neg_numeral k) = neg_numeral k" ``` huffman@47108 ` 329` ``` unfolding neg_numeral_def neg_numeral_class.neg_numeral_def ``` huffman@47108 ` 330` ``` by (simp only: of_int_minus of_int_numeral) ``` huffman@47108 ` 331` haftmann@31015 ` 332` ```lemma of_int_power: ``` haftmann@31015 ` 333` ``` "of_int (z ^ n) = of_int z ^ n" ``` haftmann@31015 ` 334` ``` by (induct n) simp_all ``` haftmann@31015 ` 335` haftmann@25919 ` 336` ```end ``` haftmann@25919 ` 337` huffman@47108 ` 338` ```context ring_char_0 ``` haftmann@25919 ` 339` ```begin ``` haftmann@25919 ` 340` haftmann@25919 ` 341` ```lemma of_int_eq_iff [simp]: ``` haftmann@25919 ` 342` ``` "of_int w = of_int z \ w = z" ``` wenzelm@42676 ` 343` ```apply (cases w, cases z) ``` wenzelm@42676 ` 344` ```apply (simp add: of_int) ``` haftmann@25919 ` 345` ```apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq) ``` haftmann@25919 ` 346` ```apply (simp only: of_nat_add [symmetric] of_nat_eq_iff) ``` haftmann@25919 ` 347` ```done ``` haftmann@25919 ` 348` haftmann@25919 ` 349` ```text{*Special cases where either operand is zero*} ``` haftmann@36424 ` 350` ```lemma of_int_eq_0_iff [simp]: ``` haftmann@36424 ` 351` ``` "of_int z = 0 \ z = 0" ``` haftmann@36424 ` 352` ``` using of_int_eq_iff [of z 0] by simp ``` haftmann@36424 ` 353` haftmann@36424 ` 354` ```lemma of_int_0_eq_iff [simp]: ``` haftmann@36424 ` 355` ``` "0 = of_int z \ z = 0" ``` haftmann@36424 ` 356` ``` using of_int_eq_iff [of 0 z] by simp ``` haftmann@25919 ` 357` haftmann@25919 ` 358` ```end ``` haftmann@25919 ` 359` haftmann@36424 ` 360` ```context linordered_idom ``` haftmann@36424 ` 361` ```begin ``` haftmann@36424 ` 362` haftmann@35028 ` 363` ```text{*Every @{text linordered_idom} has characteristic zero.*} ``` haftmann@36424 ` 364` ```subclass ring_char_0 .. ``` haftmann@36424 ` 365` haftmann@36424 ` 366` ```lemma of_int_le_iff [simp]: ``` haftmann@36424 ` 367` ``` "of_int w \ of_int z \ w \ z" ``` wenzelm@42676 ` 368` ``` by (cases w, cases z) ``` wenzelm@42676 ` 369` ``` (simp add: of_int le minus algebra_simps of_nat_add [symmetric] del: of_nat_add) ``` haftmann@36424 ` 370` haftmann@36424 ` 371` ```lemma of_int_less_iff [simp]: ``` haftmann@36424 ` 372` ``` "of_int w < of_int z \ w < z" ``` haftmann@36424 ` 373` ``` by (simp add: less_le order_less_le) ``` haftmann@36424 ` 374` haftmann@36424 ` 375` ```lemma of_int_0_le_iff [simp]: ``` haftmann@36424 ` 376` ``` "0 \ of_int z \ 0 \ z" ``` haftmann@36424 ` 377` ``` using of_int_le_iff [of 0 z] by simp ``` haftmann@36424 ` 378` haftmann@36424 ` 379` ```lemma of_int_le_0_iff [simp]: ``` haftmann@36424 ` 380` ``` "of_int z \ 0 \ z \ 0" ``` haftmann@36424 ` 381` ``` using of_int_le_iff [of z 0] by simp ``` haftmann@36424 ` 382` haftmann@36424 ` 383` ```lemma of_int_0_less_iff [simp]: ``` haftmann@36424 ` 384` ``` "0 < of_int z \ 0 < z" ``` haftmann@36424 ` 385` ``` using of_int_less_iff [of 0 z] by simp ``` haftmann@36424 ` 386` haftmann@36424 ` 387` ```lemma of_int_less_0_iff [simp]: ``` haftmann@36424 ` 388` ``` "of_int z < 0 \ z < 0" ``` haftmann@36424 ` 389` ``` using of_int_less_iff [of z 0] by simp ``` haftmann@36424 ` 390` haftmann@36424 ` 391` ```end ``` haftmann@25919 ` 392` haftmann@25919 ` 393` ```lemma of_int_eq_id [simp]: "of_int = id" ``` haftmann@25919 ` 394` ```proof ``` haftmann@25919 ` 395` ``` fix z show "of_int z = id z" ``` haftmann@25919 ` 396` ``` by (cases z) (simp add: of_int add minus int_def diff_minus) ``` haftmann@25919 ` 397` ```qed ``` haftmann@25919 ` 398` haftmann@25919 ` 399` haftmann@25919 ` 400` ```subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *} ``` haftmann@25919 ` 401` haftmann@37767 ` 402` ```definition nat :: "int \ nat" where ``` haftmann@39910 ` 403` ``` "nat z = the_elem (\(x, y) \ Rep_Integ z. {x-y})" ``` haftmann@25919 ` 404` haftmann@25919 ` 405` ```lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y" ``` haftmann@25919 ` 406` ```proof - ``` haftmann@25919 ` 407` ``` have "(\(x,y). {x-y}) respects intrel" ``` haftmann@40819 ` 408` ``` by (auto simp add: congruent_def) ``` haftmann@25919 ` 409` ``` thus ?thesis ``` haftmann@25919 ` 410` ``` by (simp add: nat_def UN_equiv_class [OF equiv_intrel]) ``` haftmann@25919 ` 411` ```qed ``` haftmann@25919 ` 412` huffman@44709 ` 413` ```lemma nat_int [simp]: "nat (int n) = n" ``` haftmann@25919 ` 414` ```by (simp add: nat int_def) ``` haftmann@25919 ` 415` huffman@44709 ` 416` ```lemma int_nat_eq [simp]: "int (nat z) = (if 0 \ z then z else 0)" ``` wenzelm@42676 ` 417` ```by (cases z) (simp add: nat le int_def Zero_int_def) ``` haftmann@25919 ` 418` huffman@44709 ` 419` ```corollary nat_0_le: "0 \ z ==> int (nat z) = z" ``` haftmann@25919 ` 420` ```by simp ``` haftmann@25919 ` 421` haftmann@25919 ` 422` ```lemma nat_le_0 [simp]: "z \ 0 ==> nat z = 0" ``` wenzelm@42676 ` 423` ```by (cases z) (simp add: nat le Zero_int_def) ``` haftmann@25919 ` 424` haftmann@25919 ` 425` ```lemma nat_le_eq_zle: "0 < w | 0 \ z ==> (nat w \ nat z) = (w\z)" ``` haftmann@25919 ` 426` ```apply (cases w, cases z) ``` haftmann@25919 ` 427` ```apply (simp add: nat le linorder_not_le [symmetric] Zero_int_def, arith) ``` haftmann@25919 ` 428` ```done ``` haftmann@25919 ` 429` haftmann@25919 ` 430` ```text{*An alternative condition is @{term "0 \ w"} *} ``` haftmann@25919 ` 431` ```corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)" ``` haftmann@25919 ` 432` ```by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) ``` haftmann@25919 ` 433` haftmann@25919 ` 434` ```corollary nat_less_eq_zless: "0 \ w ==> (nat w < nat z) = (w z" and "\m. z = int m \ P" ``` haftmann@25919 ` 445` ``` shows P ``` haftmann@25919 ` 446` ``` using assms by (blast dest: nat_0_le sym) ``` haftmann@25919 ` 447` huffman@44709 ` 448` ```lemma nat_eq_iff: "(nat w = m) = (if 0 \ w then w = int m else m=0)" ``` wenzelm@42676 ` 449` ```by (cases w) (simp add: nat le int_def Zero_int_def, arith) ``` haftmann@25919 ` 450` huffman@44709 ` 451` ```corollary nat_eq_iff2: "(m = nat w) = (if 0 \ w then w = int m else m=0)" ``` haftmann@25919 ` 452` ```by (simp only: eq_commute [of m] nat_eq_iff) ``` haftmann@25919 ` 453` haftmann@25919 ` 454` ```lemma nat_less_iff: "0 \ w ==> (nat w < m) = (w < of_nat m)" ``` haftmann@25919 ` 455` ```apply (cases w) ``` nipkow@29700 ` 456` ```apply (simp add: nat le int_def Zero_int_def linorder_not_le[symmetric], arith) ``` haftmann@25919 ` 457` ```done ``` haftmann@25919 ` 458` huffman@44709 ` 459` ```lemma nat_le_iff: "nat x \ n \ x \ int n" ``` huffman@44707 ` 460` ``` by (cases x, simp add: nat le int_def le_diff_conv) ``` huffman@44707 ` 461` huffman@44707 ` 462` ```lemma nat_mono: "x \ y \ nat x \ nat y" ``` huffman@44707 ` 463` ``` by (cases x, cases y, simp add: nat le) ``` huffman@44707 ` 464` nipkow@29700 ` 465` ```lemma nat_0_iff[simp]: "nat(i::int) = 0 \ i\0" ``` nipkow@29700 ` 466` ```by(simp add: nat_eq_iff) arith ``` nipkow@29700 ` 467` haftmann@25919 ` 468` ```lemma int_eq_iff: "(of_nat m = z) = (m = nat z & 0 \ z)" ``` haftmann@25919 ` 469` ```by (auto simp add: nat_eq_iff2) ``` haftmann@25919 ` 470` haftmann@25919 ` 471` ```lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)" ``` haftmann@25919 ` 472` ```by (insert zless_nat_conj [of 0], auto) ``` haftmann@25919 ` 473` haftmann@25919 ` 474` ```lemma nat_add_distrib: ``` haftmann@25919 ` 475` ``` "[| (0::int) \ z; 0 \ z' |] ==> nat (z+z') = nat z + nat z'" ``` wenzelm@42676 ` 476` ```by (cases z, cases z') (simp add: nat add le Zero_int_def) ``` haftmann@25919 ` 477` haftmann@25919 ` 478` ```lemma nat_diff_distrib: ``` haftmann@25919 ` 479` ``` "[| (0::int) \ z'; z' \ z |] ==> nat (z-z') = nat z - nat z'" ``` wenzelm@42676 ` 480` ```by (cases z, cases z') ``` wenzelm@42676 ` 481` ``` (simp add: nat add minus diff_minus le Zero_int_def) ``` haftmann@25919 ` 482` huffman@44709 ` 483` ```lemma nat_zminus_int [simp]: "nat (- int n) = 0" ``` haftmann@25919 ` 484` ```by (simp add: int_def minus nat Zero_int_def) ``` haftmann@25919 ` 485` huffman@44709 ` 486` ```lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)" ``` wenzelm@42676 ` 487` ```by (cases z) (simp add: nat less int_def, arith) ``` haftmann@25919 ` 488` haftmann@25919 ` 489` ```context ring_1 ``` haftmann@25919 ` 490` ```begin ``` haftmann@25919 ` 491` haftmann@25919 ` 492` ```lemma of_nat_nat: "0 \ z \ of_nat (nat z) = of_int z" ``` haftmann@25919 ` 493` ``` by (cases z rule: eq_Abs_Integ) ``` haftmann@25919 ` 494` ``` (simp add: nat le of_int Zero_int_def of_nat_diff) ``` haftmann@25919 ` 495` haftmann@25919 ` 496` ```end ``` haftmann@25919 ` 497` krauss@29779 ` 498` ```text {* For termination proofs: *} ``` krauss@29779 ` 499` ```lemma measure_function_int[measure_function]: "is_measure (nat o abs)" .. ``` krauss@29779 ` 500` haftmann@25919 ` 501` haftmann@25919 ` 502` ```subsection{*Lemmas about the Function @{term of_nat} and Orderings*} ``` haftmann@25919 ` 503` huffman@44709 ` 504` ```lemma negative_zless_0: "- (int (Suc n)) < (0 \ int)" ``` haftmann@25919 ` 505` ```by (simp add: order_less_le del: of_nat_Suc) ``` haftmann@25919 ` 506` huffman@44709 ` 507` ```lemma negative_zless [iff]: "- (int (Suc n)) < int m" ``` haftmann@25919 ` 508` ```by (rule negative_zless_0 [THEN order_less_le_trans], simp) ``` haftmann@25919 ` 509` huffman@44709 ` 510` ```lemma negative_zle_0: "- int n \ 0" ``` haftmann@25919 ` 511` ```by (simp add: minus_le_iff) ``` haftmann@25919 ` 512` huffman@44709 ` 513` ```lemma negative_zle [iff]: "- int n \ int m" ``` haftmann@25919 ` 514` ```by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff]) ``` haftmann@25919 ` 515` huffman@44709 ` 516` ```lemma not_zle_0_negative [simp]: "~ (0 \ - (int (Suc n)))" ``` haftmann@25919 ` 517` ```by (subst le_minus_iff, simp del: of_nat_Suc) ``` haftmann@25919 ` 518` huffman@44709 ` 519` ```lemma int_zle_neg: "(int n \ - int m) = (n = 0 & m = 0)" ``` haftmann@25919 ` 520` ```by (simp add: int_def le minus Zero_int_def) ``` haftmann@25919 ` 521` huffman@44709 ` 522` ```lemma not_int_zless_negative [simp]: "~ (int n < - int m)" ``` haftmann@25919 ` 523` ```by (simp add: linorder_not_less) ``` haftmann@25919 ` 524` huffman@44709 ` 525` ```lemma negative_eq_positive [simp]: "(- int n = of_nat m) = (n = 0 & m = 0)" ``` haftmann@25919 ` 526` ```by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg) ``` haftmann@25919 ` 527` huffman@44709 ` 528` ```lemma zle_iff_zadd: "w \ z \ (\n. z = w + int n)" ``` haftmann@25919 ` 529` ```proof - ``` haftmann@25919 ` 530` ``` have "(w \ z) = (0 \ z - w)" ``` haftmann@25919 ` 531` ``` by (simp only: le_diff_eq add_0_left) ``` haftmann@25919 ` 532` ``` also have "\ = (\n. z - w = of_nat n)" ``` haftmann@25919 ` 533` ``` by (auto elim: zero_le_imp_eq_int) ``` haftmann@25919 ` 534` ``` also have "\ = (\n. z = w + of_nat n)" ``` nipkow@29667 ` 535` ``` by (simp only: algebra_simps) ``` haftmann@25919 ` 536` ``` finally show ?thesis . ``` haftmann@25919 ` 537` ```qed ``` haftmann@25919 ` 538` huffman@44709 ` 539` ```lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z" ``` haftmann@25919 ` 540` ```by simp ``` haftmann@25919 ` 541` huffman@44709 ` 542` ```lemma int_Suc0_eq_1: "int (Suc 0) = 1" ``` haftmann@25919 ` 543` ```by simp ``` haftmann@25919 ` 544` haftmann@25919 ` 545` ```text{*This version is proved for all ordered rings, not just integers! ``` haftmann@25919 ` 546` ``` It is proved here because attribute @{text arith_split} is not available ``` haftmann@35050 ` 547` ``` in theory @{text Rings}. ``` haftmann@25919 ` 548` ``` But is it really better than just rewriting with @{text abs_if}?*} ``` blanchet@35828 ` 549` ```lemma abs_split [arith_split,no_atp]: ``` haftmann@35028 ` 550` ``` "P(abs(a::'a::linordered_idom)) = ((0 \ a --> P a) & (a < 0 --> P(-a)))" ``` haftmann@25919 ` 551` ```by (force dest: order_less_le_trans simp add: abs_if linorder_not_less) ``` haftmann@25919 ` 552` huffman@44709 ` 553` ```lemma negD: "x < 0 \ \n. x = - (int (Suc n))" ``` haftmann@25919 ` 554` ```apply (cases x) ``` haftmann@25919 ` 555` ```apply (auto simp add: le minus Zero_int_def int_def order_less_le) ``` haftmann@25919 ` 556` ```apply (rule_tac x="y - Suc x" in exI, arith) ``` haftmann@25919 ` 557` ```done ``` haftmann@25919 ` 558` haftmann@25919 ` 559` haftmann@25919 ` 560` ```subsection {* Cases and induction *} ``` haftmann@25919 ` 561` haftmann@25919 ` 562` ```text{*Now we replace the case analysis rule by a more conventional one: ``` haftmann@25919 ` 563` ```whether an integer is negative or not.*} ``` haftmann@25919 ` 564` wenzelm@42676 ` 565` ```theorem int_cases [case_names nonneg neg, cases type: int]: ``` huffman@44709 ` 566` ``` "[|!! n. z = int n ==> P; !! n. z = - (int (Suc n)) ==> P |] ==> P" ``` wenzelm@42676 ` 567` ```apply (cases "z < 0") ``` wenzelm@42676 ` 568` ```apply (blast dest!: negD) ``` haftmann@25919 ` 569` ```apply (simp add: linorder_not_less del: of_nat_Suc) ``` haftmann@25919 ` 570` ```apply auto ``` haftmann@25919 ` 571` ```apply (blast dest: nat_0_le [THEN sym]) ``` haftmann@25919 ` 572` ```done ``` haftmann@25919 ` 573` wenzelm@42676 ` 574` ```theorem int_of_nat_induct [case_names nonneg neg, induct type: int]: ``` huffman@44709 ` 575` ``` "[|!! n. P (int n); !!n. P (- (int (Suc n))) |] ==> P z" ``` wenzelm@42676 ` 576` ``` by (cases z) auto ``` haftmann@25919 ` 577` haftmann@25919 ` 578` ```text{*Contributed by Brian Huffman*} ``` haftmann@25919 ` 579` ```theorem int_diff_cases: ``` huffman@44709 ` 580` ``` obtains (diff) m n where "z = int m - int n" ``` haftmann@25919 ` 581` ```apply (cases z rule: eq_Abs_Integ) ``` haftmann@25919 ` 582` ```apply (rule_tac m=x and n=y in diff) ``` haftmann@37887 ` 583` ```apply (simp add: int_def minus add diff_minus) ``` haftmann@25919 ` 584` ```done ``` haftmann@25919 ` 585` huffman@47108 ` 586` ```lemma Let_numeral [simp]: "Let (numeral v) f = f (numeral v)" ``` huffman@47108 ` 587` ``` -- {* Unfold all @{text let}s involving constants *} ``` huffman@47108 ` 588` ``` unfolding Let_def .. ``` haftmann@37767 ` 589` huffman@47108 ` 590` ```lemma Let_neg_numeral [simp]: "Let (neg_numeral v) f = f (neg_numeral v)" ``` haftmann@25919 ` 591` ``` -- {* Unfold all @{text let}s involving constants *} ``` haftmann@25919 ` 592` ``` unfolding Let_def .. ``` haftmann@25919 ` 593` huffman@47108 ` 594` ```text {* Unfold @{text min} and @{text max} on numerals. *} ``` huffman@28958 ` 595` huffman@47108 ` 596` ```lemmas max_number_of [simp] = ``` huffman@47108 ` 597` ``` max_def [of "numeral u" "numeral v"] ``` huffman@47108 ` 598` ``` max_def [of "numeral u" "neg_numeral v"] ``` huffman@47108 ` 599` ``` max_def [of "neg_numeral u" "numeral v"] ``` huffman@47108 ` 600` ``` max_def [of "neg_numeral u" "neg_numeral v"] for u v ``` huffman@28958 ` 601` huffman@47108 ` 602` ```lemmas min_number_of [simp] = ``` huffman@47108 ` 603` ``` min_def [of "numeral u" "numeral v"] ``` huffman@47108 ` 604` ``` min_def [of "numeral u" "neg_numeral v"] ``` huffman@47108 ` 605` ``` min_def [of "neg_numeral u" "numeral v"] ``` huffman@47108 ` 606` ``` min_def [of "neg_numeral u" "neg_numeral v"] for u v ``` huffman@26075 ` 607` haftmann@25919 ` 608` huffman@28958 ` 609` ```subsubsection {* Binary comparisons *} ``` huffman@28958 ` 610` huffman@28958 ` 611` ```text {* Preliminaries *} ``` huffman@28958 ` 612` huffman@28958 ` 613` ```lemma even_less_0_iff: ``` haftmann@35028 ` 614` ``` "a + a < 0 \ a < (0::'a::linordered_idom)" ``` huffman@28958 ` 615` ```proof - ``` huffman@47108 ` 616` ``` have "a + a < 0 \ (1+1)*a < 0" by (simp add: left_distrib del: one_add_one) ``` huffman@28958 ` 617` ``` also have "(1+1)*a < 0 \ a < 0" ``` huffman@28958 ` 618` ``` by (simp add: mult_less_0_iff zero_less_two ``` huffman@28958 ` 619` ``` order_less_not_sym [OF zero_less_two]) ``` huffman@28958 ` 620` ``` finally show ?thesis . ``` huffman@28958 ` 621` ```qed ``` huffman@28958 ` 622` huffman@28958 ` 623` ```lemma le_imp_0_less: ``` huffman@28958 ` 624` ``` assumes le: "0 \ z" ``` huffman@28958 ` 625` ``` shows "(0::int) < 1 + z" ``` huffman@28958 ` 626` ```proof - ``` huffman@28958 ` 627` ``` have "0 \ z" by fact ``` huffman@47108 ` 628` ``` also have "... < z + 1" by (rule less_add_one) ``` huffman@28958 ` 629` ``` also have "... = 1 + z" by (simp add: add_ac) ``` huffman@28958 ` 630` ``` finally show "0 < 1 + z" . ``` huffman@28958 ` 631` ```qed ``` huffman@28958 ` 632` huffman@28958 ` 633` ```lemma odd_less_0_iff: ``` huffman@28958 ` 634` ``` "(1 + z + z < 0) = (z < (0::int))" ``` wenzelm@42676 ` 635` ```proof (cases z) ``` huffman@28958 ` 636` ``` case (nonneg n) ``` huffman@28958 ` 637` ``` thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing ``` huffman@28958 ` 638` ``` le_imp_0_less [THEN order_less_imp_le]) ``` huffman@28958 ` 639` ```next ``` huffman@28958 ` 640` ``` case (neg n) ``` huffman@30079 ` 641` ``` thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1 ``` huffman@30079 ` 642` ``` add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric]) ``` huffman@28958 ` 643` ```qed ``` huffman@28958 ` 644` huffman@28958 ` 645` ```subsubsection {* Comparisons, for Ordered Rings *} ``` haftmann@25919 ` 646` haftmann@25919 ` 647` ```lemmas double_eq_0_iff = double_zero ``` haftmann@25919 ` 648` haftmann@25919 ` 649` ```lemma odd_nonzero: ``` haftmann@33296 ` 650` ``` "1 + z + z \ (0::int)" ``` wenzelm@42676 ` 651` ```proof (cases z) ``` haftmann@25919 ` 652` ``` case (nonneg n) ``` haftmann@25919 ` 653` ``` have le: "0 \ z+z" by (simp add: nonneg add_increasing) ``` haftmann@25919 ` 654` ``` thus ?thesis using le_imp_0_less [OF le] ``` haftmann@25919 ` 655` ``` by (auto simp add: add_assoc) ``` haftmann@25919 ` 656` ```next ``` haftmann@25919 ` 657` ``` case (neg n) ``` haftmann@25919 ` 658` ``` show ?thesis ``` haftmann@25919 ` 659` ``` proof ``` haftmann@25919 ` 660` ``` assume eq: "1 + z + z = 0" ``` huffman@44709 ` 661` ``` have "(0::int) < 1 + (int n + int n)" ``` haftmann@25919 ` 662` ``` by (simp add: le_imp_0_less add_increasing) ``` haftmann@25919 ` 663` ``` also have "... = - (1 + z + z)" ``` haftmann@25919 ` 664` ``` by (simp add: neg add_assoc [symmetric]) ``` haftmann@25919 ` 665` ``` also have "... = 0" by (simp add: eq) ``` haftmann@25919 ` 666` ``` finally have "0<0" .. ``` haftmann@25919 ` 667` ``` thus False by blast ``` haftmann@25919 ` 668` ``` qed ``` haftmann@25919 ` 669` ```qed ``` haftmann@25919 ` 670` haftmann@30652 ` 671` haftmann@25919 ` 672` ```subsection {* The Set of Integers *} ``` haftmann@25919 ` 673` haftmann@25919 ` 674` ```context ring_1 ``` haftmann@25919 ` 675` ```begin ``` haftmann@25919 ` 676` haftmann@30652 ` 677` ```definition Ints :: "'a set" where ``` haftmann@37767 ` 678` ``` "Ints = range of_int" ``` haftmann@25919 ` 679` haftmann@25919 ` 680` ```notation (xsymbols) ``` haftmann@25919 ` 681` ``` Ints ("\") ``` haftmann@25919 ` 682` huffman@35634 ` 683` ```lemma Ints_of_int [simp]: "of_int z \ \" ``` huffman@35634 ` 684` ``` by (simp add: Ints_def) ``` huffman@35634 ` 685` huffman@35634 ` 686` ```lemma Ints_of_nat [simp]: "of_nat n \ \" ``` huffman@45533 ` 687` ``` using Ints_of_int [of "of_nat n"] by simp ``` huffman@35634 ` 688` haftmann@25919 ` 689` ```lemma Ints_0 [simp]: "0 \ \" ``` huffman@45533 ` 690` ``` using Ints_of_int [of "0"] by simp ``` haftmann@25919 ` 691` haftmann@25919 ` 692` ```lemma Ints_1 [simp]: "1 \ \" ``` huffman@45533 ` 693` ``` using Ints_of_int [of "1"] by simp ``` haftmann@25919 ` 694` haftmann@25919 ` 695` ```lemma Ints_add [simp]: "a \ \ \ b \ \ \ a + b \ \" ``` haftmann@25919 ` 696` ```apply (auto simp add: Ints_def) ``` haftmann@25919 ` 697` ```apply (rule range_eqI) ``` haftmann@25919 ` 698` ```apply (rule of_int_add [symmetric]) ``` haftmann@25919 ` 699` ```done ``` haftmann@25919 ` 700` haftmann@25919 ` 701` ```lemma Ints_minus [simp]: "a \ \ \ -a \ \" ``` haftmann@25919 ` 702` ```apply (auto simp add: Ints_def) ``` haftmann@25919 ` 703` ```apply (rule range_eqI) ``` haftmann@25919 ` 704` ```apply (rule of_int_minus [symmetric]) ``` haftmann@25919 ` 705` ```done ``` haftmann@25919 ` 706` huffman@35634 ` 707` ```lemma Ints_diff [simp]: "a \ \ \ b \ \ \ a - b \ \" ``` huffman@35634 ` 708` ```apply (auto simp add: Ints_def) ``` huffman@35634 ` 709` ```apply (rule range_eqI) ``` huffman@35634 ` 710` ```apply (rule of_int_diff [symmetric]) ``` huffman@35634 ` 711` ```done ``` huffman@35634 ` 712` haftmann@25919 ` 713` ```lemma Ints_mult [simp]: "a \ \ \ b \ \ \ a * b \ \" ``` haftmann@25919 ` 714` ```apply (auto simp add: Ints_def) ``` haftmann@25919 ` 715` ```apply (rule range_eqI) ``` haftmann@25919 ` 716` ```apply (rule of_int_mult [symmetric]) ``` haftmann@25919 ` 717` ```done ``` haftmann@25919 ` 718` huffman@35634 ` 719` ```lemma Ints_power [simp]: "a \ \ \ a ^ n \ \" ``` huffman@35634 ` 720` ```by (induct n) simp_all ``` huffman@35634 ` 721` haftmann@25919 ` 722` ```lemma Ints_cases [cases set: Ints]: ``` haftmann@25919 ` 723` ``` assumes "q \ \" ``` haftmann@25919 ` 724` ``` obtains (of_int) z where "q = of_int z" ``` haftmann@25919 ` 725` ``` unfolding Ints_def ``` haftmann@25919 ` 726` ```proof - ``` haftmann@25919 ` 727` ``` from `q \ \` have "q \ range of_int" unfolding Ints_def . ``` haftmann@25919 ` 728` ``` then obtain z where "q = of_int z" .. ``` haftmann@25919 ` 729` ``` then show thesis .. ``` haftmann@25919 ` 730` ```qed ``` haftmann@25919 ` 731` haftmann@25919 ` 732` ```lemma Ints_induct [case_names of_int, induct set: Ints]: ``` haftmann@25919 ` 733` ``` "q \ \ \ (\z. P (of_int z)) \ P q" ``` haftmann@25919 ` 734` ``` by (rule Ints_cases) auto ``` haftmann@25919 ` 735` haftmann@25919 ` 736` ```end ``` haftmann@25919 ` 737` haftmann@25919 ` 738` ```text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *} ``` haftmann@25919 ` 739` haftmann@25919 ` 740` ```lemma Ints_double_eq_0_iff: ``` haftmann@25919 ` 741` ``` assumes in_Ints: "a \ Ints" ``` haftmann@25919 ` 742` ``` shows "(a + a = 0) = (a = (0::'a::ring_char_0))" ``` haftmann@25919 ` 743` ```proof - ``` haftmann@25919 ` 744` ``` from in_Ints have "a \ range of_int" unfolding Ints_def [symmetric] . ``` haftmann@25919 ` 745` ``` then obtain z where a: "a = of_int z" .. ``` haftmann@25919 ` 746` ``` show ?thesis ``` haftmann@25919 ` 747` ``` proof ``` haftmann@25919 ` 748` ``` assume "a = 0" ``` haftmann@25919 ` 749` ``` thus "a + a = 0" by simp ``` haftmann@25919 ` 750` ``` next ``` haftmann@25919 ` 751` ``` assume eq: "a + a = 0" ``` haftmann@25919 ` 752` ``` hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a) ``` haftmann@25919 ` 753` ``` hence "z + z = 0" by (simp only: of_int_eq_iff) ``` haftmann@25919 ` 754` ``` hence "z = 0" by (simp only: double_eq_0_iff) ``` haftmann@25919 ` 755` ``` thus "a = 0" by (simp add: a) ``` haftmann@25919 ` 756` ``` qed ``` haftmann@25919 ` 757` ```qed ``` haftmann@25919 ` 758` haftmann@25919 ` 759` ```lemma Ints_odd_nonzero: ``` haftmann@25919 ` 760` ``` assumes in_Ints: "a \ Ints" ``` haftmann@25919 ` 761` ``` shows "1 + a + a \ (0::'a::ring_char_0)" ``` haftmann@25919 ` 762` ```proof - ``` haftmann@25919 ` 763` ``` from in_Ints have "a \ range of_int" unfolding Ints_def [symmetric] . ``` haftmann@25919 ` 764` ``` then obtain z where a: "a = of_int z" .. ``` haftmann@25919 ` 765` ``` show ?thesis ``` haftmann@25919 ` 766` ``` proof ``` haftmann@25919 ` 767` ``` assume eq: "1 + a + a = 0" ``` haftmann@25919 ` 768` ``` hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a) ``` haftmann@25919 ` 769` ``` hence "1 + z + z = 0" by (simp only: of_int_eq_iff) ``` haftmann@25919 ` 770` ``` with odd_nonzero show False by blast ``` haftmann@25919 ` 771` ``` qed ``` haftmann@25919 ` 772` ```qed ``` haftmann@25919 ` 773` huffman@47108 ` 774` ```lemma Nats_numeral [simp]: "numeral w \ Nats" ``` huffman@47108 ` 775` ``` using of_nat_in_Nats [of "numeral w"] by simp ``` huffman@35634 ` 776` haftmann@25919 ` 777` ```lemma Ints_odd_less_0: ``` haftmann@25919 ` 778` ``` assumes in_Ints: "a \ Ints" ``` haftmann@35028 ` 779` ``` shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))" ``` haftmann@25919 ` 780` ```proof - ``` haftmann@25919 ` 781` ``` from in_Ints have "a \ range of_int" unfolding Ints_def [symmetric] . ``` haftmann@25919 ` 782` ``` then obtain z where a: "a = of_int z" .. ``` haftmann@25919 ` 783` ``` hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))" ``` haftmann@25919 ` 784` ``` by (simp add: a) ``` huffman@45532 ` 785` ``` also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0_iff) ``` haftmann@25919 ` 786` ``` also have "... = (a < 0)" by (simp add: a) ``` haftmann@25919 ` 787` ``` finally show ?thesis . ``` haftmann@25919 ` 788` ```qed ``` haftmann@25919 ` 789` haftmann@25919 ` 790` haftmann@25919 ` 791` ```subsection {* @{term setsum} and @{term setprod} *} ``` haftmann@25919 ` 792` haftmann@25919 ` 793` ```lemma of_nat_setsum: "of_nat (setsum f A) = (\x\A. of_nat(f x))" ``` haftmann@25919 ` 794` ``` apply (cases "finite A") ``` haftmann@25919 ` 795` ``` apply (erule finite_induct, auto) ``` haftmann@25919 ` 796` ``` done ``` haftmann@25919 ` 797` haftmann@25919 ` 798` ```lemma of_int_setsum: "of_int (setsum f A) = (\x\A. of_int(f x))" ``` haftmann@25919 ` 799` ``` apply (cases "finite A") ``` haftmann@25919 ` 800` ``` apply (erule finite_induct, auto) ``` haftmann@25919 ` 801` ``` done ``` haftmann@25919 ` 802` haftmann@25919 ` 803` ```lemma of_nat_setprod: "of_nat (setprod f A) = (\x\A. of_nat(f x))" ``` haftmann@25919 ` 804` ``` apply (cases "finite A") ``` haftmann@25919 ` 805` ``` apply (erule finite_induct, auto simp add: of_nat_mult) ``` haftmann@25919 ` 806` ``` done ``` haftmann@25919 ` 807` haftmann@25919 ` 808` ```lemma of_int_setprod: "of_int (setprod f A) = (\x\A. of_int(f x))" ``` haftmann@25919 ` 809` ``` apply (cases "finite A") ``` haftmann@25919 ` 810` ``` apply (erule finite_induct, auto) ``` haftmann@25919 ` 811` ``` done ``` haftmann@25919 ` 812` haftmann@25919 ` 813` ```lemmas int_setsum = of_nat_setsum [where 'a=int] ``` haftmann@25919 ` 814` ```lemmas int_setprod = of_nat_setprod [where 'a=int] ``` haftmann@25919 ` 815` haftmann@25919 ` 816` haftmann@25919 ` 817` ```text {* Legacy theorems *} ``` haftmann@25919 ` 818` haftmann@25919 ` 819` ```lemmas zle_int = of_nat_le_iff [where 'a=int] ``` haftmann@25919 ` 820` ```lemmas int_int_eq = of_nat_eq_iff [where 'a=int] ``` huffman@47108 ` 821` ```lemmas numeral_1_eq_1 = numeral_One ``` haftmann@25919 ` 822` huffman@30802 ` 823` ```subsection {* Setting up simplification procedures *} ``` huffman@30802 ` 824` huffman@30802 ` 825` ```lemmas int_arith_rules = ``` huffman@47108 ` 826` ``` neg_le_iff_le numeral_One ``` huffman@30802 ` 827` ``` minus_zero diff_minus left_minus right_minus ``` huffman@45219 ` 828` ``` mult_zero_left mult_zero_right mult_1_left mult_1_right ``` huffman@30802 ` 829` ``` mult_minus_left mult_minus_right ``` huffman@30802 ` 830` ``` minus_add_distrib minus_minus mult_assoc ``` huffman@30802 ` 831` ``` of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult ``` huffman@30802 ` 832` ``` of_int_0 of_int_1 of_int_add of_int_mult ``` huffman@30802 ` 833` huffman@47108 ` 834` ```use "Tools/numeral.ML" ``` haftmann@28952 ` 835` ```use "Tools/int_arith.ML" ``` haftmann@30496 ` 836` ```declaration {* K Int_Arith.setup *} ``` haftmann@25919 ` 837` huffman@47108 ` 838` ```simproc_setup fast_arith ("(m::'a::linordered_idom) < n" | ``` huffman@47108 ` 839` ``` "(m::'a::linordered_idom) <= n" | ``` huffman@47108 ` 840` ``` "(m::'a::linordered_idom) = n") = ``` wenzelm@43595 ` 841` ``` {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *} ``` wenzelm@43595 ` 842` huffman@31024 ` 843` ```setup {* ``` wenzelm@33523 ` 844` ``` Reorient_Proc.add ``` huffman@47108 ` 845` ``` (fn Const (@{const_name numeral}, _) \$ _ => true ``` huffman@47108 ` 846` ``` | Const (@{const_name neg_numeral}, _) \$ _ => true ``` huffman@47108 ` 847` ``` | _ => false) ``` huffman@31024 ` 848` ```*} ``` huffman@31024 ` 849` huffman@47108 ` 850` ```simproc_setup reorient_numeral ``` huffman@47108 ` 851` ``` ("numeral w = x" | "neg_numeral w = y") = Reorient_Proc.proc ``` huffman@31024 ` 852` haftmann@25919 ` 853` haftmann@25919 ` 854` ```subsection{*Lemmas About Small Numerals*} ``` haftmann@25919 ` 855` haftmann@25919 ` 856` ```lemma abs_power_minus_one [simp]: ``` huffman@47108 ` 857` ``` "abs(-1 ^ n) = (1::'a::linordered_idom)" ``` haftmann@25919 ` 858` ```by (simp add: power_abs) ``` haftmann@25919 ` 859` haftmann@25919 ` 860` ```text{*Lemmas for specialist use, NOT as default simprules*} ``` huffman@43531 ` 861` ```(* TODO: see if semiring duplication can be removed without breaking proofs *) ``` huffman@47108 ` 862` ```lemma mult_2: "2 * z = (z+z::'a::semiring_1)" ``` huffman@47108 ` 863` ```unfolding one_add_one [symmetric] left_distrib by simp ``` huffman@43531 ` 864` huffman@47108 ` 865` ```lemma mult_2_right: "z * 2 = (z+z::'a::semiring_1)" ``` huffman@47108 ` 866` ```unfolding one_add_one [symmetric] right_distrib by simp ``` haftmann@25919 ` 867` haftmann@25919 ` 868` haftmann@25919 ` 869` ```subsection{*More Inequality Reasoning*} ``` haftmann@25919 ` 870` haftmann@25919 ` 871` ```lemma zless_add1_eq: "(w < z + (1::int)) = (w z) = (w z - (1::int)) = (wz)" ``` haftmann@25919 ` 881` ```by arith ``` haftmann@25919 ` 882` haftmann@25919 ` 883` ```lemma int_one_le_iff_zero_less: "((1::int) \ z) = (0 < z)" ``` haftmann@25919 ` 884` ```by arith ``` haftmann@25919 ` 885` haftmann@25919 ` 886` huffman@28958 ` 887` ```subsection{*The functions @{term nat} and @{term int}*} ``` haftmann@25919 ` 888` haftmann@25919 ` 889` ```text{*Simplify the terms @{term "int 0"}, @{term "int(Suc 0)"} and ``` haftmann@25919 ` 890` ``` @{term "w + - z"}*} ``` haftmann@25919 ` 891` ```declare Zero_int_def [symmetric, simp] ``` haftmann@25919 ` 892` ```declare One_int_def [symmetric, simp] ``` haftmann@25919 ` 893` haftmann@25919 ` 894` ```lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp] ``` haftmann@25919 ` 895` huffman@44695 ` 896` ```lemma nat_0 [simp]: "nat 0 = 0" ``` haftmann@25919 ` 897` ```by (simp add: nat_eq_iff) ``` haftmann@25919 ` 898` haftmann@25919 ` 899` ```lemma nat_1: "nat 1 = Suc 0" ``` haftmann@25919 ` 900` ```by (subst nat_eq_iff, simp) ``` haftmann@25919 ` 901` haftmann@25919 ` 902` ```lemma nat_2: "nat 2 = Suc (Suc 0)" ``` haftmann@25919 ` 903` ```by (subst nat_eq_iff, simp) ``` haftmann@25919 ` 904` haftmann@25919 ` 905` ```lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)" ``` haftmann@25919 ` 906` ```apply (insert zless_nat_conj [of 1 z]) ``` haftmann@25919 ` 907` ```apply (auto simp add: nat_1) ``` haftmann@25919 ` 908` ```done ``` haftmann@25919 ` 909` haftmann@25919 ` 910` ```text{*This simplifies expressions of the form @{term "int n = z"} where ``` haftmann@25919 ` 911` ``` z is an integer literal.*} ``` huffman@47108 ` 912` ```lemmas int_eq_iff_numeral [simp] = int_eq_iff [of _ "numeral v"] for v ``` haftmann@25919 ` 913` haftmann@25919 ` 914` ```lemma split_nat [arith_split]: ``` huffman@44709 ` 915` ``` "P(nat(i::int)) = ((\n. i = int n \ P n) & (i < 0 \ P 0))" ``` haftmann@25919 ` 916` ``` (is "?P = (?L & ?R)") ``` haftmann@25919 ` 917` ```proof (cases "i < 0") ``` haftmann@25919 ` 918` ``` case True thus ?thesis by auto ``` haftmann@25919 ` 919` ```next ``` haftmann@25919 ` 920` ``` case False ``` haftmann@25919 ` 921` ``` have "?P = ?L" ``` haftmann@25919 ` 922` ``` proof ``` haftmann@25919 ` 923` ``` assume ?P thus ?L using False by clarsimp ``` haftmann@25919 ` 924` ``` next ``` haftmann@25919 ` 925` ``` assume ?L thus ?P using False by simp ``` haftmann@25919 ` 926` ``` qed ``` haftmann@25919 ` 927` ``` with False show ?thesis by simp ``` haftmann@25919 ` 928` ```qed ``` haftmann@25919 ` 929` haftmann@25919 ` 930` ```context ring_1 ``` haftmann@25919 ` 931` ```begin ``` haftmann@25919 ` 932` blanchet@33056 ` 933` ```lemma of_int_of_nat [nitpick_simp]: ``` haftmann@25919 ` 934` ``` "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))" ``` haftmann@25919 ` 935` ```proof (cases "k < 0") ``` haftmann@25919 ` 936` ``` case True then have "0 \ - k" by simp ``` haftmann@25919 ` 937` ``` then have "of_nat (nat (- k)) = of_int (- k)" by (rule of_nat_nat) ``` haftmann@25919 ` 938` ``` with True show ?thesis by simp ``` haftmann@25919 ` 939` ```next ``` haftmann@25919 ` 940` ``` case False then show ?thesis by (simp add: not_less of_nat_nat) ``` haftmann@25919 ` 941` ```qed ``` haftmann@25919 ` 942` haftmann@25919 ` 943` ```end ``` haftmann@25919 ` 944` haftmann@25919 ` 945` ```lemma nat_mult_distrib: ``` haftmann@25919 ` 946` ``` fixes z z' :: int ``` haftmann@25919 ` 947` ``` assumes "0 \ z" ``` haftmann@25919 ` 948` ``` shows "nat (z * z') = nat z * nat z'" ``` haftmann@25919 ` 949` ```proof (cases "0 \ z'") ``` haftmann@25919 ` 950` ``` case False with assms have "z * z' \ 0" ``` haftmann@25919 ` 951` ``` by (simp add: not_le mult_le_0_iff) ``` haftmann@25919 ` 952` ``` then have "nat (z * z') = 0" by simp ``` haftmann@25919 ` 953` ``` moreover from False have "nat z' = 0" by simp ``` haftmann@25919 ` 954` ``` ultimately show ?thesis by simp ``` haftmann@25919 ` 955` ```next ``` haftmann@25919 ` 956` ``` case True with assms have ge_0: "z * z' \ 0" by (simp add: zero_le_mult_iff) ``` haftmann@25919 ` 957` ``` show ?thesis ``` haftmann@25919 ` 958` ``` by (rule injD [of "of_nat :: nat \ int", OF inj_of_nat]) ``` haftmann@25919 ` 959` ``` (simp only: of_nat_mult of_nat_nat [OF True] ``` haftmann@25919 ` 960` ``` of_nat_nat [OF assms] of_nat_nat [OF ge_0], simp) ``` haftmann@25919 ` 961` ```qed ``` haftmann@25919 ` 962` haftmann@25919 ` 963` ```lemma nat_mult_distrib_neg: "z \ (0::int) ==> nat(z*z') = nat(-z) * nat(-z')" ``` haftmann@25919 ` 964` ```apply (rule trans) ``` haftmann@25919 ` 965` ```apply (rule_tac [2] nat_mult_distrib, auto) ``` haftmann@25919 ` 966` ```done ``` haftmann@25919 ` 967` haftmann@25919 ` 968` ```lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)" ``` haftmann@25919 ` 969` ```apply (cases "z=0 | w=0") ``` haftmann@25919 ` 970` ```apply (auto simp add: abs_if nat_mult_distrib [symmetric] ``` haftmann@25919 ` 971` ``` nat_mult_distrib_neg [symmetric] mult_less_0_iff) ``` haftmann@25919 ` 972` ```done ``` haftmann@25919 ` 973` haftmann@25919 ` 974` haftmann@25919 ` 975` ```subsection "Induction principles for int" ``` haftmann@25919 ` 976` haftmann@25919 ` 977` ```text{*Well-founded segments of the integers*} ``` haftmann@25919 ` 978` haftmann@25919 ` 979` ```definition ``` haftmann@25919 ` 980` ``` int_ge_less_than :: "int => (int * int) set" ``` haftmann@25919 ` 981` ```where ``` haftmann@25919 ` 982` ``` "int_ge_less_than d = {(z',z). d \ z' & z' < z}" ``` haftmann@25919 ` 983` haftmann@25919 ` 984` ```theorem wf_int_ge_less_than: "wf (int_ge_less_than d)" ``` haftmann@25919 ` 985` ```proof - ``` haftmann@25919 ` 986` ``` have "int_ge_less_than d \ measure (%z. nat (z-d))" ``` haftmann@25919 ` 987` ``` by (auto simp add: int_ge_less_than_def) ``` haftmann@25919 ` 988` ``` thus ?thesis ``` haftmann@25919 ` 989` ``` by (rule wf_subset [OF wf_measure]) ``` haftmann@25919 ` 990` ```qed ``` haftmann@25919 ` 991` haftmann@25919 ` 992` ```text{*This variant looks odd, but is typical of the relations suggested ``` haftmann@25919 ` 993` ```by RankFinder.*} ``` haftmann@25919 ` 994` haftmann@25919 ` 995` ```definition ``` haftmann@25919 ` 996` ``` int_ge_less_than2 :: "int => (int * int) set" ``` haftmann@25919 ` 997` ```where ``` haftmann@25919 ` 998` ``` "int_ge_less_than2 d = {(z',z). d \ z & z' < z}" ``` haftmann@25919 ` 999` haftmann@25919 ` 1000` ```theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)" ``` haftmann@25919 ` 1001` ```proof - ``` haftmann@25919 ` 1002` ``` have "int_ge_less_than2 d \ measure (%z. nat (1+z-d))" ``` haftmann@25919 ` 1003` ``` by (auto simp add: int_ge_less_than2_def) ``` haftmann@25919 ` 1004` ``` thus ?thesis ``` haftmann@25919 ` 1005` ``` by (rule wf_subset [OF wf_measure]) ``` haftmann@25919 ` 1006` ```qed ``` haftmann@25919 ` 1007` haftmann@25919 ` 1008` ```(* `set:int': dummy construction *) ``` haftmann@25919 ` 1009` ```theorem int_ge_induct [case_names base step, induct set: int]: ``` haftmann@25919 ` 1010` ``` fixes i :: int ``` haftmann@25919 ` 1011` ``` assumes ge: "k \ i" and ``` haftmann@25919 ` 1012` ``` base: "P k" and ``` haftmann@25919 ` 1013` ``` step: "\i. k \ i \ P i \ P (i + 1)" ``` haftmann@25919 ` 1014` ``` shows "P i" ``` haftmann@25919 ` 1015` ```proof - ``` wenzelm@42676 ` 1016` ``` { fix n ``` wenzelm@42676 ` 1017` ``` have "\i::int. n = nat (i - k) \ k \ i \ P i" ``` haftmann@25919 ` 1018` ``` proof (induct n) ``` haftmann@25919 ` 1019` ``` case 0 ``` haftmann@25919 ` 1020` ``` hence "i = k" by arith ``` haftmann@25919 ` 1021` ``` thus "P i" using base by simp ``` haftmann@25919 ` 1022` ``` next ``` haftmann@25919 ` 1023` ``` case (Suc n) ``` haftmann@25919 ` 1024` ``` then have "n = nat((i - 1) - k)" by arith ``` haftmann@25919 ` 1025` ``` moreover ``` haftmann@25919 ` 1026` ``` have ki1: "k \ i - 1" using Suc.prems by arith ``` haftmann@25919 ` 1027` ``` ultimately ``` wenzelm@42676 ` 1028` ``` have "P (i - 1)" by (rule Suc.hyps) ``` wenzelm@42676 ` 1029` ``` from step [OF ki1 this] show ?case by simp ``` haftmann@25919 ` 1030` ``` qed ``` haftmann@25919 ` 1031` ``` } ``` haftmann@25919 ` 1032` ``` with ge show ?thesis by fast ``` haftmann@25919 ` 1033` ```qed ``` haftmann@25919 ` 1034` haftmann@25928 ` 1035` ```(* `set:int': dummy construction *) ``` haftmann@25928 ` 1036` ```theorem int_gr_induct [case_names base step, induct set: int]: ``` haftmann@25919 ` 1037` ``` assumes gr: "k < (i::int)" and ``` haftmann@25919 ` 1038` ``` base: "P(k+1)" and ``` haftmann@25919 ` 1039` ``` step: "\i. \k < i; P i\ \ P(i+1)" ``` haftmann@25919 ` 1040` ``` shows "P i" ``` haftmann@25919 ` 1041` ```apply(rule int_ge_induct[of "k + 1"]) ``` haftmann@25919 ` 1042` ``` using gr apply arith ``` haftmann@25919 ` 1043` ``` apply(rule base) ``` haftmann@25919 ` 1044` ```apply (rule step, simp+) ``` haftmann@25919 ` 1045` ```done ``` haftmann@25919 ` 1046` wenzelm@42676 ` 1047` ```theorem int_le_induct [consumes 1, case_names base step]: ``` haftmann@25919 ` 1048` ``` assumes le: "i \ (k::int)" and ``` haftmann@25919 ` 1049` ``` base: "P(k)" and ``` haftmann@25919 ` 1050` ``` step: "\i. \i \ k; P i\ \ P(i - 1)" ``` haftmann@25919 ` 1051` ``` shows "P i" ``` haftmann@25919 ` 1052` ```proof - ``` wenzelm@42676 ` 1053` ``` { fix n ``` wenzelm@42676 ` 1054` ``` have "\i::int. n = nat(k-i) \ i \ k \ P i" ``` haftmann@25919 ` 1055` ``` proof (induct n) ``` haftmann@25919 ` 1056` ``` case 0 ``` haftmann@25919 ` 1057` ``` hence "i = k" by arith ``` haftmann@25919 ` 1058` ``` thus "P i" using base by simp ``` haftmann@25919 ` 1059` ``` next ``` haftmann@25919 ` 1060` ``` case (Suc n) ``` wenzelm@42676 ` 1061` ``` hence "n = nat (k - (i + 1))" by arith ``` haftmann@25919 ` 1062` ``` moreover ``` haftmann@25919 ` 1063` ``` have ki1: "i + 1 \ k" using Suc.prems by arith ``` haftmann@25919 ` 1064` ``` ultimately ``` wenzelm@42676 ` 1065` ``` have "P (i + 1)" by(rule Suc.hyps) ``` haftmann@25919 ` 1066` ``` from step[OF ki1 this] show ?case by simp ``` haftmann@25919 ` 1067` ``` qed ``` haftmann@25919 ` 1068` ``` } ``` haftmann@25919 ` 1069` ``` with le show ?thesis by fast ``` haftmann@25919 ` 1070` ```qed ``` haftmann@25919 ` 1071` wenzelm@42676 ` 1072` ```theorem int_less_induct [consumes 1, case_names base step]: ``` haftmann@25919 ` 1073` ``` assumes less: "(i::int) < k" and ``` haftmann@25919 ` 1074` ``` base: "P(k - 1)" and ``` haftmann@25919 ` 1075` ``` step: "\i. \i < k; P i\ \ P(i - 1)" ``` haftmann@25919 ` 1076` ``` shows "P i" ``` haftmann@25919 ` 1077` ```apply(rule int_le_induct[of _ "k - 1"]) ``` haftmann@25919 ` 1078` ``` using less apply arith ``` haftmann@25919 ` 1079` ``` apply(rule base) ``` haftmann@25919 ` 1080` ```apply (rule step, simp+) ``` haftmann@25919 ` 1081` ```done ``` haftmann@25919 ` 1082` haftmann@36811 ` 1083` ```theorem int_induct [case_names base step1 step2]: ``` haftmann@36801 ` 1084` ``` fixes k :: int ``` haftmann@36801 ` 1085` ``` assumes base: "P k" ``` haftmann@36801 ` 1086` ``` and step1: "\i. k \ i \ P i \ P (i + 1)" ``` haftmann@36801 ` 1087` ``` and step2: "\i. k \ i \ P i \ P (i - 1)" ``` haftmann@36801 ` 1088` ``` shows "P i" ``` haftmann@36801 ` 1089` ```proof - ``` haftmann@36801 ` 1090` ``` have "i \ k \ i \ k" by arith ``` wenzelm@42676 ` 1091` ``` then show ?thesis ``` wenzelm@42676 ` 1092` ``` proof ``` wenzelm@42676 ` 1093` ``` assume "i \ k" ``` wenzelm@42676 ` 1094` ``` then show ?thesis using base ``` haftmann@36801 ` 1095` ``` by (rule int_ge_induct) (fact step1) ``` haftmann@36801 ` 1096` ``` next ``` wenzelm@42676 ` 1097` ``` assume "i \ k" ``` wenzelm@42676 ` 1098` ``` then show ?thesis using base ``` haftmann@36801 ` 1099` ``` by (rule int_le_induct) (fact step2) ``` haftmann@36801 ` 1100` ``` qed ``` haftmann@36801 ` 1101` ```qed ``` haftmann@36801 ` 1102` haftmann@25919 ` 1103` ```subsection{*Intermediate value theorems*} ``` haftmann@25919 ` 1104` haftmann@25919 ` 1105` ```lemma int_val_lemma: ``` haftmann@25919 ` 1106` ``` "(\i 1) --> ``` haftmann@25919 ` 1107` ``` f 0 \ k --> k \ f n --> (\i \ n. f i = (k::int))" ``` huffman@30079 ` 1108` ```unfolding One_nat_def ``` wenzelm@42676 ` 1109` ```apply (induct n) ``` wenzelm@42676 ` 1110` ```apply simp ``` haftmann@25919 ` 1111` ```apply (intro strip) ``` haftmann@25919 ` 1112` ```apply (erule impE, simp) ``` haftmann@25919 ` 1113` ```apply (erule_tac x = n in allE, simp) ``` huffman@30079 ` 1114` ```apply (case_tac "k = f (Suc n)") ``` haftmann@27106 ` 1115` ```apply force ``` haftmann@25919 ` 1116` ```apply (erule impE) ``` haftmann@25919 ` 1117` ``` apply (simp add: abs_if split add: split_if_asm) ``` haftmann@25919 ` 1118` ```apply (blast intro: le_SucI) ``` haftmann@25919 ` 1119` ```done ``` haftmann@25919 ` 1120` haftmann@25919 ` 1121` ```lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)] ``` haftmann@25919 ` 1122` haftmann@25919 ` 1123` ```lemma nat_intermed_int_val: ``` haftmann@25919 ` 1124` ``` "[| \i. m \ i & i < n --> abs(f(i + 1::nat) - f i) \ 1; m < n; ``` haftmann@25919 ` 1125` ``` f m \ k; k \ f n |] ==> ? i. m \ i & i \ n & f i = (k::int)" ``` haftmann@25919 ` 1126` ```apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k ``` haftmann@25919 ` 1127` ``` in int_val_lemma) ``` huffman@30079 ` 1128` ```unfolding One_nat_def ``` haftmann@25919 ` 1129` ```apply simp ``` haftmann@25919 ` 1130` ```apply (erule exE) ``` haftmann@25919 ` 1131` ```apply (rule_tac x = "i+m" in exI, arith) ``` haftmann@25919 ` 1132` ```done ``` haftmann@25919 ` 1133` haftmann@25919 ` 1134` haftmann@25919 ` 1135` ```subsection{*Products and 1, by T. M. Rasmussen*} ``` haftmann@25919 ` 1136` haftmann@25919 ` 1137` ```lemma zabs_less_one_iff [simp]: "(\z\ < 1) = (z = (0::int))" ``` haftmann@25919 ` 1138` ```by arith ``` haftmann@25919 ` 1139` paulson@34055 ` 1140` ```lemma abs_zmult_eq_1: ``` paulson@34055 ` 1141` ``` assumes mn: "\m * n\ = 1" ``` paulson@34055 ` 1142` ``` shows "\m\ = (1::int)" ``` paulson@34055 ` 1143` ```proof - ``` paulson@34055 ` 1144` ``` have 0: "m \ 0 & n \ 0" using mn ``` paulson@34055 ` 1145` ``` by auto ``` paulson@34055 ` 1146` ``` have "~ (2 \ \m\)" ``` paulson@34055 ` 1147` ``` proof ``` paulson@34055 ` 1148` ``` assume "2 \ \m\" ``` paulson@34055 ` 1149` ``` hence "2*\n\ \ \m\*\n\" ``` paulson@34055 ` 1150` ``` by (simp add: mult_mono 0) ``` paulson@34055 ` 1151` ``` also have "... = \m*n\" ``` paulson@34055 ` 1152` ``` by (simp add: abs_mult) ``` paulson@34055 ` 1153` ``` also have "... = 1" ``` paulson@34055 ` 1154` ``` by (simp add: mn) ``` paulson@34055 ` 1155` ``` finally have "2*\n\ \ 1" . ``` paulson@34055 ` 1156` ``` thus "False" using 0 ``` huffman@47108 ` 1157` ``` by arith ``` paulson@34055 ` 1158` ``` qed ``` paulson@34055 ` 1159` ``` thus ?thesis using 0 ``` paulson@34055 ` 1160` ``` by auto ``` paulson@34055 ` 1161` ```qed ``` haftmann@25919 ` 1162` huffman@47108 ` 1163` ```ML_val {* @{const_name neg_numeral} *} ``` huffman@47108 ` 1164` haftmann@25919 ` 1165` ```lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1" ``` haftmann@25919 ` 1166` ```by (insert abs_zmult_eq_1 [of m n], arith) ``` haftmann@25919 ` 1167` boehmes@35815 ` 1168` ```lemma pos_zmult_eq_1_iff: ``` boehmes@35815 ` 1169` ``` assumes "0 < (m::int)" shows "(m * n = 1) = (m = 1 & n = 1)" ``` boehmes@35815 ` 1170` ```proof - ``` boehmes@35815 ` 1171` ``` from assms have "m * n = 1 ==> m = 1" by (auto dest: pos_zmult_eq_1_iff_lemma) ``` boehmes@35815 ` 1172` ``` thus ?thesis by (auto dest: pos_zmult_eq_1_iff_lemma) ``` boehmes@35815 ` 1173` ```qed ``` haftmann@25919 ` 1174` haftmann@25919 ` 1175` ```lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))" ``` haftmann@25919 ` 1176` ```apply (rule iffI) ``` haftmann@25919 ` 1177` ``` apply (frule pos_zmult_eq_1_iff_lemma) ``` haftmann@25919 ` 1178` ``` apply (simp add: mult_commute [of m]) ``` haftmann@25919 ` 1179` ``` apply (frule pos_zmult_eq_1_iff_lemma, auto) ``` haftmann@25919 ` 1180` ```done ``` haftmann@25919 ` 1181` haftmann@33296 ` 1182` ```lemma infinite_UNIV_int: "\ finite (UNIV::int set)" ``` haftmann@25919 ` 1183` ```proof ``` haftmann@33296 ` 1184` ``` assume "finite (UNIV::int set)" ``` haftmann@33296 ` 1185` ``` moreover have "inj (\i\int. 2 * i)" ``` haftmann@33296 ` 1186` ``` by (rule injI) simp ``` haftmann@33296 ` 1187` ``` ultimately have "surj (\i\int. 2 * i)" ``` haftmann@33296 ` 1188` ``` by (rule finite_UNIV_inj_surj) ``` haftmann@33296 ` 1189` ``` then obtain i :: int where "1 = 2 * i" by (rule surjE) ``` haftmann@33296 ` 1190` ``` then show False by (simp add: pos_zmult_eq_1_iff) ``` haftmann@25919 ` 1191` ```qed ``` haftmann@25919 ` 1192` haftmann@25919 ` 1193` haftmann@30652 ` 1194` ```subsection {* Further theorems on numerals *} ``` haftmann@30652 ` 1195` haftmann@30652 ` 1196` ```subsubsection{*Special Simplification for Constants*} ``` haftmann@30652 ` 1197` haftmann@30652 ` 1198` ```text{*These distributive laws move literals inside sums and differences.*} ``` haftmann@30652 ` 1199` huffman@47108 ` 1200` ```lemmas left_distrib_numeral [simp] = left_distrib [of _ _ "numeral v"] for v ``` huffman@47108 ` 1201` ```lemmas right_distrib_numeral [simp] = right_distrib [of "numeral v"] for v ``` huffman@47108 ` 1202` ```lemmas left_diff_distrib_numeral [simp] = left_diff_distrib [of _ _ "numeral v"] for v ``` huffman@47108 ` 1203` ```lemmas right_diff_distrib_numeral [simp] = right_diff_distrib [of "numeral v"] for v ``` haftmann@30652 ` 1204` haftmann@30652 ` 1205` ```text{*These are actually for fields, like real: but where else to put them?*} ``` haftmann@30652 ` 1206` huffman@47108 ` 1207` ```lemmas zero_less_divide_iff_numeral [simp, no_atp] = zero_less_divide_iff [of "numeral w"] for w ``` huffman@47108 ` 1208` ```lemmas divide_less_0_iff_numeral [simp, no_atp] = divide_less_0_iff [of "numeral w"] for w ``` huffman@47108 ` 1209` ```lemmas zero_le_divide_iff_numeral [simp, no_atp] = zero_le_divide_iff [of "numeral w"] for w ``` huffman@47108 ` 1210` ```lemmas divide_le_0_iff_numeral [simp, no_atp] = divide_le_0_iff [of "numeral w"] for w ``` haftmann@30652 ` 1211` haftmann@30652 ` 1212` haftmann@30652 ` 1213` ```text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}. It looks ``` haftmann@30652 ` 1214` ``` strange, but then other simprocs simplify the quotient.*} ``` haftmann@30652 ` 1215` huffman@47108 ` 1216` ```lemmas inverse_eq_divide_numeral [simp] = ``` huffman@47108 ` 1217` ``` inverse_eq_divide [of "numeral w"] for w ``` huffman@47108 ` 1218` huffman@47108 ` 1219` ```lemmas inverse_eq_divide_neg_numeral [simp] = ``` huffman@47108 ` 1220` ``` inverse_eq_divide [of "neg_numeral w"] for w ``` haftmann@30652 ` 1221` haftmann@30652 ` 1222` ```text {*These laws simplify inequalities, moving unary minus from a term ``` haftmann@30652 ` 1223` ```into the literal.*} ``` haftmann@30652 ` 1224` huffman@47108 ` 1225` ```lemmas le_minus_iff_numeral [simp, no_atp] = ``` huffman@47108 ` 1226` ``` le_minus_iff [of "numeral v"] ``` huffman@47108 ` 1227` ``` le_minus_iff [of "neg_numeral v"] for v ``` huffman@47108 ` 1228` huffman@47108 ` 1229` ```lemmas equation_minus_iff_numeral [simp, no_atp] = ``` huffman@47108 ` 1230` ``` equation_minus_iff [of "numeral v"] ``` huffman@47108 ` 1231` ``` equation_minus_iff [of "neg_numeral v"] for v ``` huffman@47108 ` 1232` huffman@47108 ` 1233` ```lemmas minus_less_iff_numeral [simp, no_atp] = ``` huffman@47108 ` 1234` ``` minus_less_iff [of _ "numeral v"] ``` huffman@47108 ` 1235` ``` minus_less_iff [of _ "neg_numeral v"] for v ``` huffman@47108 ` 1236` huffman@47108 ` 1237` ```lemmas minus_le_iff_numeral [simp, no_atp] = ``` huffman@47108 ` 1238` ``` minus_le_iff [of _ "numeral v"] ``` huffman@47108 ` 1239` ``` minus_le_iff [of _ "neg_numeral v"] for v ``` huffman@47108 ` 1240` huffman@47108 ` 1241` ```lemmas minus_equation_iff_numeral [simp, no_atp] = ``` huffman@47108 ` 1242` ``` minus_equation_iff [of _ "numeral v"] ``` huffman@47108 ` 1243` ``` minus_equation_iff [of _ "neg_numeral v"] for v ``` haftmann@30652 ` 1244` haftmann@30652 ` 1245` ```text{*To Simplify Inequalities Where One Side is the Constant 1*} ``` haftmann@30652 ` 1246` blanchet@35828 ` 1247` ```lemma less_minus_iff_1 [simp,no_atp]: ``` huffman@47108 ` 1248` ``` fixes b::"'b::linordered_idom" ``` haftmann@30652 ` 1249` ``` shows "(1 < - b) = (b < -1)" ``` haftmann@30652 ` 1250` ```by auto ``` haftmann@30652 ` 1251` blanchet@35828 ` 1252` ```lemma le_minus_iff_1 [simp,no_atp]: ``` huffman@47108 ` 1253` ``` fixes b::"'b::linordered_idom" ``` haftmann@30652 ` 1254` ``` shows "(1 \ - b) = (b \ -1)" ``` haftmann@30652 ` 1255` ```by auto ``` haftmann@30652 ` 1256` blanchet@35828 ` 1257` ```lemma equation_minus_iff_1 [simp,no_atp]: ``` huffman@47108 ` 1258` ``` fixes b::"'b::ring_1" ``` haftmann@30652 ` 1259` ``` shows "(1 = - b) = (b = -1)" ``` haftmann@30652 ` 1260` ```by (subst equation_minus_iff, auto) ``` haftmann@30652 ` 1261` blanchet@35828 ` 1262` ```lemma minus_less_iff_1 [simp,no_atp]: ``` huffman@47108 ` 1263` ``` fixes a::"'b::linordered_idom" ``` haftmann@30652 ` 1264` ``` shows "(- a < 1) = (-1 < a)" ``` haftmann@30652 ` 1265` ```by auto ``` haftmann@30652 ` 1266` blanchet@35828 ` 1267` ```lemma minus_le_iff_1 [simp,no_atp]: ``` huffman@47108 ` 1268` ``` fixes a::"'b::linordered_idom" ``` haftmann@30652 ` 1269` ``` shows "(- a \ 1) = (-1 \ a)" ``` haftmann@30652 ` 1270` ```by auto ``` haftmann@30652 ` 1271` blanchet@35828 ` 1272` ```lemma minus_equation_iff_1 [simp,no_atp]: ``` huffman@47108 ` 1273` ``` fixes a::"'b::ring_1" ``` haftmann@30652 ` 1274` ``` shows "(- a = 1) = (a = -1)" ``` haftmann@30652 ` 1275` ```by (subst minus_equation_iff, auto) ``` haftmann@30652 ` 1276` haftmann@30652 ` 1277` haftmann@30652 ` 1278` ```text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\"}) *} ``` haftmann@30652 ` 1279` huffman@47108 ` 1280` ```lemmas mult_less_cancel_left_numeral [simp, no_atp] = mult_less_cancel_left [of "numeral v"] for v ``` huffman@47108 ` 1281` ```lemmas mult_less_cancel_right_numeral [simp, no_atp] = mult_less_cancel_right [of _ "numeral v"] for v ``` huffman@47108 ` 1282` ```lemmas mult_le_cancel_left_numeral [simp, no_atp] = mult_le_cancel_left [of "numeral v"] for v ``` huffman@47108 ` 1283` ```lemmas mult_le_cancel_right_numeral [simp, no_atp] = mult_le_cancel_right [of _ "numeral v"] for v ``` haftmann@30652 ` 1284` haftmann@30652 ` 1285` haftmann@30652 ` 1286` ```text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\"} and @{text "="}) *} ``` haftmann@30652 ` 1287` huffman@47108 ` 1288` ```lemmas le_divide_eq_numeral1 [simp] = ``` huffman@47108 ` 1289` ``` pos_le_divide_eq [of "numeral w", OF zero_less_numeral] ``` huffman@47108 ` 1290` ``` neg_le_divide_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w ``` huffman@47108 ` 1291` huffman@47108 ` 1292` ```lemmas divide_le_eq_numeral1 [simp] = ``` huffman@47108 ` 1293` ``` pos_divide_le_eq [of "numeral w", OF zero_less_numeral] ``` huffman@47108 ` 1294` ``` neg_divide_le_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w ``` huffman@47108 ` 1295` huffman@47108 ` 1296` ```lemmas less_divide_eq_numeral1 [simp] = ``` huffman@47108 ` 1297` ``` pos_less_divide_eq [of "numeral w", OF zero_less_numeral] ``` huffman@47108 ` 1298` ``` neg_less_divide_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w ``` haftmann@30652 ` 1299` huffman@47108 ` 1300` ```lemmas divide_less_eq_numeral1 [simp] = ``` huffman@47108 ` 1301` ``` pos_divide_less_eq [of "numeral w", OF zero_less_numeral] ``` huffman@47108 ` 1302` ``` neg_divide_less_eq [of "neg_numeral w", OF neg_numeral_less_zero] for w ``` huffman@47108 ` 1303` huffman@47108 ` 1304` ```lemmas eq_divide_eq_numeral1 [simp] = ``` huffman@47108 ` 1305` ``` eq_divide_eq [of _ _ "numeral w"] ``` huffman@47108 ` 1306` ``` eq_divide_eq [of _ _ "neg_numeral w"] for w ``` huffman@47108 ` 1307` huffman@47108 ` 1308` ```lemmas divide_eq_eq_numeral1 [simp] = ``` huffman@47108 ` 1309` ``` divide_eq_eq [of _ "numeral w"] ``` huffman@47108 ` 1310` ``` divide_eq_eq [of _ "neg_numeral w"] for w ``` haftmann@30652 ` 1311` haftmann@30652 ` 1312` ```subsubsection{*Optional Simplification Rules Involving Constants*} ``` haftmann@30652 ` 1313` haftmann@30652 ` 1314` ```text{*Simplify quotients that are compared with a literal constant.*} ``` haftmann@30652 ` 1315` huffman@47108 ` 1316` ```lemmas le_divide_eq_numeral = ``` huffman@47108 ` 1317` ``` le_divide_eq [of "numeral w"] ``` huffman@47108 ` 1318` ``` le_divide_eq [of "neg_numeral w"] for w ``` huffman@47108 ` 1319` huffman@47108 ` 1320` ```lemmas divide_le_eq_numeral = ``` huffman@47108 ` 1321` ``` divide_le_eq [of _ _ "numeral w"] ``` huffman@47108 ` 1322` ``` divide_le_eq [of _ _ "neg_numeral w"] for w ``` huffman@47108 ` 1323` huffman@47108 ` 1324` ```lemmas less_divide_eq_numeral = ``` huffman@47108 ` 1325` ``` less_divide_eq [of "numeral w"] ``` huffman@47108 ` 1326` ``` less_divide_eq [of "neg_numeral w"] for w ``` huffman@47108 ` 1327` huffman@47108 ` 1328` ```lemmas divide_less_eq_numeral = ``` huffman@47108 ` 1329` ``` divide_less_eq [of _ _ "numeral w"] ``` huffman@47108 ` 1330` ``` divide_less_eq [of _ _ "neg_numeral w"] for w ``` huffman@47108 ` 1331` huffman@47108 ` 1332` ```lemmas eq_divide_eq_numeral = ``` huffman@47108 ` 1333` ``` eq_divide_eq [of "numeral w"] ``` huffman@47108 ` 1334` ``` eq_divide_eq [of "neg_numeral w"] for w ``` huffman@47108 ` 1335` huffman@47108 ` 1336` ```lemmas divide_eq_eq_numeral = ``` huffman@47108 ` 1337` ``` divide_eq_eq [of _ _ "numeral w"] ``` huffman@47108 ` 1338` ``` divide_eq_eq [of _ _ "neg_numeral w"] for w ``` haftmann@30652 ` 1339` haftmann@30652 ` 1340` haftmann@30652 ` 1341` ```text{*Not good as automatic simprules because they cause case splits.*} ``` haftmann@30652 ` 1342` ```lemmas divide_const_simps = ``` huffman@47108 ` 1343` ``` le_divide_eq_numeral divide_le_eq_numeral less_divide_eq_numeral ``` huffman@47108 ` 1344` ``` divide_less_eq_numeral eq_divide_eq_numeral divide_eq_eq_numeral ``` haftmann@30652 ` 1345` ``` le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1 ``` haftmann@30652 ` 1346` haftmann@30652 ` 1347` ```text{*Division By @{text "-1"}*} ``` haftmann@30652 ` 1348` huffman@47108 ` 1349` ```lemma divide_minus1 [simp]: "(x::'a::field) / -1 = - x" ``` huffman@47108 ` 1350` ``` unfolding minus_one [symmetric] ``` huffman@47108 ` 1351` ``` unfolding nonzero_minus_divide_right [OF one_neq_zero, symmetric] ``` huffman@47108 ` 1352` ``` by simp ``` haftmann@30652 ` 1353` huffman@47108 ` 1354` ```lemma minus1_divide [simp]: "-1 / (x::'a::field) = - (1 / x)" ``` huffman@47108 ` 1355` ``` unfolding minus_one [symmetric] by (rule divide_minus_left) ``` haftmann@30652 ` 1356` haftmann@30652 ` 1357` ```lemma half_gt_zero_iff: ``` huffman@47108 ` 1358` ``` "(0 < r/2) = (0 < (r::'a::linordered_field_inverse_zero))" ``` haftmann@30652 ` 1359` ```by auto ``` haftmann@30652 ` 1360` wenzelm@45607 ` 1361` ```lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2] ``` haftmann@30652 ` 1362` huffman@47108 ` 1363` ```lemma divide_Numeral1: "(x::'a::field) / Numeral1 = x" ``` haftmann@36719 ` 1364` ``` by simp ``` haftmann@36719 ` 1365` haftmann@30652 ` 1366` haftmann@33320 ` 1367` ```subsection {* The divides relation *} ``` haftmann@33320 ` 1368` nipkow@33657 ` 1369` ```lemma zdvd_antisym_nonneg: ``` nipkow@33657 ` 1370` ``` "0 <= m ==> 0 <= n ==> m dvd n ==> n dvd m ==> m = (n::int)" ``` haftmann@33320 ` 1371` ``` apply (simp add: dvd_def, auto) ``` nipkow@33657 ` 1372` ``` apply (auto simp add: mult_assoc zero_le_mult_iff zmult_eq_1_iff) ``` haftmann@33320 ` 1373` ``` done ``` haftmann@33320 ` 1374` nipkow@33657 ` 1375` ```lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a" ``` haftmann@33320 ` 1376` ``` shows "\a\ = \b\" ``` nipkow@33657 ` 1377` ```proof cases ``` nipkow@33657 ` 1378` ``` assume "a = 0" with assms show ?thesis by simp ``` nipkow@33657 ` 1379` ```next ``` nipkow@33657 ` 1380` ``` assume "a \ 0" ``` haftmann@33320 ` 1381` ``` from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast ``` haftmann@33320 ` 1382` ``` from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast ``` haftmann@33320 ` 1383` ``` from k k' have "a = a*k*k'" by simp ``` haftmann@33320 ` 1384` ``` with mult_cancel_left1[where c="a" and b="k*k'"] ``` haftmann@33320 ` 1385` ``` have kk':"k*k' = 1" using `a\0` by (simp add: mult_assoc) ``` haftmann@33320 ` 1386` ``` hence "k = 1 \ k' = 1 \ k = -1 \ k' = -1" by (simp add: zmult_eq_1_iff) ``` haftmann@33320 ` 1387` ``` thus ?thesis using k k' by auto ``` haftmann@33320 ` 1388` ```qed ``` haftmann@33320 ` 1389` haftmann@33320 ` 1390` ```lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)" ``` haftmann@33320 ` 1391` ``` apply (subgoal_tac "m = n + (m - n)") ``` haftmann@33320 ` 1392` ``` apply (erule ssubst) ``` haftmann@33320 ` 1393` ``` apply (blast intro: dvd_add, simp) ``` haftmann@33320 ` 1394` ``` done ``` haftmann@33320 ` 1395` haftmann@33320 ` 1396` ```lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))" ``` haftmann@33320 ` 1397` ```apply (rule iffI) ``` haftmann@33320 ` 1398` ``` apply (erule_tac [2] dvd_add) ``` haftmann@33320 ` 1399` ``` apply (subgoal_tac "n = (n + k * m) - k * m") ``` haftmann@33320 ` 1400` ``` apply (erule ssubst) ``` haftmann@33320 ` 1401` ``` apply (erule dvd_diff) ``` haftmann@33320 ` 1402` ``` apply(simp_all) ``` haftmann@33320 ` 1403` ```done ``` haftmann@33320 ` 1404` haftmann@33320 ` 1405` ```lemma dvd_imp_le_int: ``` haftmann@33320 ` 1406` ``` fixes d i :: int ``` haftmann@33320 ` 1407` ``` assumes "i \ 0" and "d dvd i" ``` haftmann@33320 ` 1408` ``` shows "\d\ \ \i\" ``` haftmann@33320 ` 1409` ```proof - ``` haftmann@33320 ` 1410` ``` from `d dvd i` obtain k where "i = d * k" .. ``` haftmann@33320 ` 1411` ``` with `i \ 0` have "k \ 0" by auto ``` haftmann@33320 ` 1412` ``` then have "1 \ \k\" and "0 \ \d\" by auto ``` haftmann@33320 ` 1413` ``` then have "\d\ * 1 \ \d\ * \k\" by (rule mult_left_mono) ``` haftmann@33320 ` 1414` ``` with `i = d * k` show ?thesis by (simp add: abs_mult) ``` haftmann@33320 ` 1415` ```qed ``` haftmann@33320 ` 1416` haftmann@33320 ` 1417` ```lemma zdvd_not_zless: ``` haftmann@33320 ` 1418` ``` fixes m n :: int ``` haftmann@33320 ` 1419` ``` assumes "0 < m" and "m < n" ``` haftmann@33320 ` 1420` ``` shows "\ n dvd m" ``` haftmann@33320 ` 1421` ```proof ``` haftmann@33320 ` 1422` ``` from assms have "0 < n" by auto ``` haftmann@33320 ` 1423` ``` assume "n dvd m" then obtain k where k: "m = n * k" .. ``` haftmann@33320 ` 1424` ``` with `0 < m` have "0 < n * k" by auto ``` haftmann@33320 ` 1425` ``` with `0 < n` have "0 < k" by (simp add: zero_less_mult_iff) ``` haftmann@33320 ` 1426` ``` with k `0 < n` `m < n` have "n * k < n * 1" by simp ``` haftmann@33320 ` 1427` ``` with `0 < n` `0 < k` show False unfolding mult_less_cancel_left by auto ``` haftmann@33320 ` 1428` ```qed ``` haftmann@33320 ` 1429` haftmann@33320 ` 1430` ```lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \ (0::int)" ``` haftmann@33320 ` 1431` ``` shows "m dvd n" ``` haftmann@33320 ` 1432` ```proof- ``` haftmann@33320 ` 1433` ``` from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast ``` haftmann@33320 ` 1434` ``` {assume "n \ m*h" hence "k* n \ k* (m*h)" using kz by simp ``` haftmann@33320 ` 1435` ``` with h have False by (simp add: mult_assoc)} ``` haftmann@33320 ` 1436` ``` hence "n = m * h" by blast ``` haftmann@33320 ` 1437` ``` thus ?thesis by simp ``` haftmann@33320 ` 1438` ```qed ``` haftmann@33320 ` 1439` haftmann@33320 ` 1440` ```theorem zdvd_int: "(x dvd y) = (int x dvd int y)" ``` haftmann@33320 ` 1441` ```proof - ``` haftmann@33320 ` 1442` ``` have "\k. int y = int x * k \ x dvd y" ``` haftmann@33320 ` 1443` ``` proof - ``` haftmann@33320 ` 1444` ``` fix k ``` haftmann@33320 ` 1445` ``` assume A: "int y = int x * k" ``` wenzelm@42676 ` 1446` ``` then show "x dvd y" ``` wenzelm@42676 ` 1447` ``` proof (cases k) ``` wenzelm@42676 ` 1448` ``` case (nonneg n) ``` wenzelm@42676 ` 1449` ``` with A have "y = x * n" by (simp add: of_nat_mult [symmetric]) ``` haftmann@33320 ` 1450` ``` then show ?thesis .. ``` haftmann@33320 ` 1451` ``` next ``` wenzelm@42676 ` 1452` ``` case (neg n) ``` wenzelm@42676 ` 1453` ``` with A have "int y = int x * (- int (Suc n))" by simp ``` haftmann@33320 ` 1454` ``` also have "\ = - (int x * int (Suc n))" by (simp only: mult_minus_right) ``` haftmann@33320 ` 1455` ``` also have "\ = - int (x * Suc n)" by (simp only: of_nat_mult [symmetric]) ``` haftmann@33320 ` 1456` ``` finally have "- int (x * Suc n) = int y" .. ``` haftmann@33320 ` 1457` ``` then show ?thesis by (simp only: negative_eq_positive) auto ``` haftmann@33320 ` 1458` ``` qed ``` haftmann@33320 ` 1459` ``` qed ``` haftmann@33320 ` 1460` ``` then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left of_nat_mult) ``` haftmann@33320 ` 1461` ```qed ``` haftmann@33320 ` 1462` wenzelm@42676 ` 1463` ```lemma zdvd1_eq[simp]: "(x::int) dvd 1 = (\x\ = 1)" ``` haftmann@33320 ` 1464` ```proof ``` haftmann@33320 ` 1465` ``` assume d: "x dvd 1" hence "int (nat \x\) dvd int (nat 1)" by simp ``` haftmann@33320 ` 1466` ``` hence "nat \x\ dvd 1" by (simp add: zdvd_int) ``` haftmann@33320 ` 1467` ``` hence "nat \x\ = 1" by simp ``` wenzelm@42676 ` 1468` ``` thus "\x\ = 1" by (cases "x < 0") auto ``` haftmann@33320 ` 1469` ```next ``` haftmann@33320 ` 1470` ``` assume "\x\=1" ``` haftmann@33320 ` 1471` ``` then have "x = 1 \ x = -1" by auto ``` haftmann@33320 ` 1472` ``` then show "x dvd 1" by (auto intro: dvdI) ``` haftmann@33320 ` 1473` ```qed ``` haftmann@33320 ` 1474` haftmann@33320 ` 1475` ```lemma zdvd_mult_cancel1: ``` haftmann@33320 ` 1476` ``` assumes mp:"m \(0::int)" shows "(m * n dvd m) = (\n\ = 1)" ``` haftmann@33320 ` 1477` ```proof ``` haftmann@33320 ` 1478` ``` assume n1: "\n\ = 1" thus "m * n dvd m" ``` wenzelm@42676 ` 1479` ``` by (cases "n >0") (auto simp add: minus_equation_iff) ``` haftmann@33320 ` 1480` ```next ``` haftmann@33320 ` 1481` ``` assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp ``` haftmann@33320 ` 1482` ``` from zdvd_mult_cancel[OF H2 mp] show "\n\ = 1" by (simp only: zdvd1_eq) ``` haftmann@33320 ` 1483` ```qed ``` haftmann@33320 ` 1484` haftmann@33320 ` 1485` ```lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))" ``` haftmann@33320 ` 1486` ``` unfolding zdvd_int by (cases "z \ 0") simp_all ``` haftmann@33320 ` 1487` haftmann@33320 ` 1488` ```lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)" ``` haftmann@33320 ` 1489` ``` unfolding zdvd_int by (cases "z \ 0") simp_all ``` haftmann@33320 ` 1490` haftmann@33320 ` 1491` ```lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \ z then (z dvd int m) else m = 0)" ``` haftmann@33320 ` 1492` ``` by (auto simp add: dvd_int_iff) ``` haftmann@33320 ` 1493` haftmann@33341 ` 1494` ```lemma eq_nat_nat_iff: ``` haftmann@33341 ` 1495` ``` "0 \ z \ 0 \ z' \ nat z = nat z' \ z = z'" ``` haftmann@33341 ` 1496` ``` by (auto elim!: nonneg_eq_int) ``` haftmann@33341 ` 1497` haftmann@33341 ` 1498` ```lemma nat_power_eq: ``` haftmann@33341 ` 1499` ``` "0 \ z \ nat (z ^ n) = nat z ^ n" ``` haftmann@33341 ` 1500` ``` by (induct n) (simp_all add: nat_mult_distrib) ``` haftmann@33341 ` 1501` haftmann@33320 ` 1502` ```lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \ (n::int)" ``` wenzelm@42676 ` 1503` ``` apply (cases n) ``` haftmann@33320 ` 1504` ``` apply (auto simp add: dvd_int_iff) ``` wenzelm@42676 ` 1505` ``` apply (cases z) ``` haftmann@33320 ` 1506` ``` apply (auto simp add: dvd_imp_le) ``` haftmann@33320 ` 1507` ``` done ``` haftmann@33320 ` 1508` haftmann@36749 ` 1509` ```lemma zdvd_period: ``` haftmann@36749 ` 1510` ``` fixes a d :: int ``` haftmann@36749 ` 1511` ``` assumes "a dvd d" ``` haftmann@36749 ` 1512` ``` shows "a dvd (x + t) \ a dvd ((x + c * d) + t)" ``` haftmann@36749 ` 1513` ```proof - ``` haftmann@36749 ` 1514` ``` from assms obtain k where "d = a * k" by (rule dvdE) ``` wenzelm@42676 ` 1515` ``` show ?thesis ``` wenzelm@42676 ` 1516` ``` proof ``` haftmann@36749 ` 1517` ``` assume "a dvd (x + t)" ``` haftmann@36749 ` 1518` ``` then obtain l where "x + t = a * l" by (rule dvdE) ``` haftmann@36749 ` 1519` ``` then have "x = a * l - t" by simp ``` haftmann@36749 ` 1520` ``` with `d = a * k` show "a dvd x + c * d + t" by simp ``` haftmann@36749 ` 1521` ``` next ``` haftmann@36749 ` 1522` ``` assume "a dvd x + c * d + t" ``` haftmann@36749 ` 1523` ``` then obtain l where "x + c * d + t = a * l" by (rule dvdE) ``` haftmann@36749 ` 1524` ``` then have "x = a * l - c * d - t" by simp ``` haftmann@36749 ` 1525` ``` with `d = a * k` show "a dvd (x + t)" by simp ``` haftmann@36749 ` 1526` ``` qed ``` haftmann@36749 ` 1527` ```qed ``` haftmann@36749 ` 1528` haftmann@33320 ` 1529` bulwahn@46756 ` 1530` ```subsection {* Finiteness of intervals *} ``` bulwahn@46756 ` 1531` bulwahn@46756 ` 1532` ```lemma finite_interval_int1 [iff]: "finite {i :: int. a <= i & i <= b}" ``` bulwahn@46756 ` 1533` ```proof (cases "a <= b") ``` bulwahn@46756 ` 1534` ``` case True ``` bulwahn@46756 ` 1535` ``` from this show ?thesis ``` bulwahn@46756 ` 1536` ``` proof (induct b rule: int_ge_induct) ``` bulwahn@46756 ` 1537` ``` case base ``` bulwahn@46756 ` 1538` ``` have "{i. a <= i & i <= a} = {a}" by auto ``` bulwahn@46756 ` 1539` ``` from this show ?case by simp ``` bulwahn@46756 ` 1540` ``` next ``` bulwahn@46756 ` 1541` ``` case (step b) ``` bulwahn@46756 ` 1542` ``` from this have "{i. a <= i & i <= b + 1} = {i. a <= i & i <= b} \ {b + 1}" by auto ``` bulwahn@46756 ` 1543` ``` from this step show ?case by simp ``` bulwahn@46756 ` 1544` ``` qed ``` bulwahn@46756 ` 1545` ```next ``` bulwahn@46756 ` 1546` ``` case False from this show ?thesis ``` bulwahn@46756 ` 1547` ``` by (metis (lifting, no_types) Collect_empty_eq finite.emptyI order_trans) ``` bulwahn@46756 ` 1548` ```qed ``` bulwahn@46756 ` 1549` bulwahn@46756 ` 1550` ```lemma finite_interval_int2 [iff]: "finite {i :: int. a <= i & i < b}" ``` bulwahn@46756 ` 1551` ```by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto ``` bulwahn@46756 ` 1552` bulwahn@46756 ` 1553` ```lemma finite_interval_int3 [iff]: "finite {i :: int. a < i & i <= b}" ``` bulwahn@46756 ` 1554` ```by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto ``` bulwahn@46756 ` 1555` bulwahn@46756 ` 1556` ```lemma finite_interval_int4 [iff]: "finite {i :: int. a < i & i < b}" ``` bulwahn@46756 ` 1557` ```by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto ``` bulwahn@46756 ` 1558` bulwahn@46756 ` 1559` haftmann@25919 ` 1560` ```subsection {* Configuration of the code generator *} ``` haftmann@25919 ` 1561` huffman@47108 ` 1562` ```text {* Constructors *} ``` huffman@47108 ` 1563` huffman@47108 ` 1564` ```definition Pos :: "num \ int" where ``` huffman@47108 ` 1565` ``` [simp, code_abbrev]: "Pos = numeral" ``` huffman@47108 ` 1566` huffman@47108 ` 1567` ```definition Neg :: "num \ int" where ``` huffman@47108 ` 1568` ``` [simp, code_abbrev]: "Neg = neg_numeral" ``` huffman@47108 ` 1569` huffman@47108 ` 1570` ```code_datatype "0::int" Pos Neg ``` huffman@47108 ` 1571` huffman@47108 ` 1572` huffman@47108 ` 1573` ```text {* Auxiliary operations *} ``` huffman@47108 ` 1574` huffman@47108 ` 1575` ```definition dup :: "int \ int" where ``` huffman@47108 ` 1576` ``` [simp]: "dup k = k + k" ``` haftmann@26507 ` 1577` huffman@47108 ` 1578` ```lemma dup_code [code]: ``` huffman@47108 ` 1579` ``` "dup 0 = 0" ``` huffman@47108 ` 1580` ``` "dup (Pos n) = Pos (Num.Bit0 n)" ``` huffman@47108 ` 1581` ``` "dup (Neg n) = Neg (Num.Bit0 n)" ``` huffman@47108 ` 1582` ``` unfolding Pos_def Neg_def neg_numeral_def ``` huffman@47108 ` 1583` ``` by (simp_all add: numeral_Bit0) ``` huffman@47108 ` 1584` huffman@47108 ` 1585` ```definition sub :: "num \ num \ int" where ``` huffman@47108 ` 1586` ``` [simp]: "sub m n = numeral m - numeral n" ``` haftmann@26507 ` 1587` huffman@47108 ` 1588` ```lemma sub_code [code]: ``` huffman@47108 ` 1589` ``` "sub Num.One Num.One = 0" ``` huffman@47108 ` 1590` ``` "sub (Num.Bit0 m) Num.One = Pos (Num.BitM m)" ``` huffman@47108 ` 1591` ``` "sub (Num.Bit1 m) Num.One = Pos (Num.Bit0 m)" ``` huffman@47108 ` 1592` ``` "sub Num.One (Num.Bit0 n) = Neg (Num.BitM n)" ``` huffman@47108 ` 1593` ``` "sub Num.One (Num.Bit1 n) = Neg (Num.Bit0 n)" ``` huffman@47108 ` 1594` ``` "sub (Num.Bit0 m) (Num.Bit0 n) = dup (sub m n)" ``` huffman@47108 ` 1595` ``` "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)" ``` huffman@47108 ` 1596` ``` "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1" ``` huffman@47108 ` 1597` ``` "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1" ``` huffman@47108 ` 1598` ``` unfolding sub_def dup_def numeral.simps Pos_def Neg_def ``` huffman@47108 ` 1599` ``` neg_numeral_def numeral_BitM ``` huffman@47108 ` 1600` ``` by (simp_all only: algebra_simps) ``` haftmann@26507 ` 1601` huffman@47108 ` 1602` huffman@47108 ` 1603` ```text {* Implementations *} ``` huffman@47108 ` 1604` huffman@47108 ` 1605` ```lemma one_int_code [code, code_unfold]: ``` huffman@47108 ` 1606` ``` "1 = Pos Num.One" ``` huffman@47108 ` 1607` ``` by simp ``` huffman@47108 ` 1608` huffman@47108 ` 1609` ```lemma plus_int_code [code]: ``` huffman@47108 ` 1610` ``` "k + 0 = (k::int)" ``` huffman@47108 ` 1611` ``` "0 + l = (l::int)" ``` huffman@47108 ` 1612` ``` "Pos m + Pos n = Pos (m + n)" ``` huffman@47108 ` 1613` ``` "Pos m + Neg n = sub m n" ``` huffman@47108 ` 1614` ``` "Neg m + Pos n = sub n m" ``` huffman@47108 ` 1615` ``` "Neg m + Neg n = Neg (m + n)" ``` huffman@47108 ` 1616` ``` by simp_all ``` haftmann@26507 ` 1617` huffman@47108 ` 1618` ```lemma uminus_int_code [code]: ``` huffman@47108 ` 1619` ``` "uminus 0 = (0::int)" ``` huffman@47108 ` 1620` ``` "uminus (Pos m) = Neg m" ``` huffman@47108 ` 1621` ``` "uminus (Neg m) = Pos m" ``` huffman@47108 ` 1622` ``` by simp_all ``` huffman@47108 ` 1623` huffman@47108 ` 1624` ```lemma minus_int_code [code]: ``` huffman@47108 ` 1625` ``` "k - 0 = (k::int)" ``` huffman@47108 ` 1626` ``` "0 - l = uminus (l::int)" ``` huffman@47108 ` 1627` ``` "Pos m - Pos n = sub m n" ``` huffman@47108 ` 1628` ``` "Pos m - Neg n = Pos (m + n)" ``` huffman@47108 ` 1629` ``` "Neg m - Pos n = Neg (m + n)" ``` huffman@47108 ` 1630` ``` "Neg m - Neg n = sub n m" ``` huffman@47108 ` 1631` ``` by simp_all ``` huffman@47108 ` 1632` huffman@47108 ` 1633` ```lemma times_int_code [code]: ``` huffman@47108 ` 1634` ``` "k * 0 = (0::int)" ``` huffman@47108 ` 1635` ``` "0 * l = (0::int)" ``` huffman@47108 ` 1636` ``` "Pos m * Pos n = Pos (m * n)" ``` huffman@47108 ` 1637` ``` "Pos m * Neg n = Neg (m * n)" ``` huffman@47108 ` 1638` ``` "Neg m * Pos n = Neg (m * n)" ``` huffman@47108 ` 1639` ``` "Neg m * Neg n = Pos (m * n)" ``` huffman@47108 ` 1640` ``` by simp_all ``` haftmann@26507 ` 1641` haftmann@38857 ` 1642` ```instantiation int :: equal ``` haftmann@26507 ` 1643` ```begin ``` haftmann@26507 ` 1644` haftmann@37767 ` 1645` ```definition ``` huffman@47108 ` 1646` ``` "HOL.equal k l \ k = (l::int)" ``` haftmann@38857 ` 1647` huffman@47108 ` 1648` ```instance by default (rule equal_int_def) ``` haftmann@26507 ` 1649` haftmann@26507 ` 1650` ```end ``` haftmann@26507 ` 1651` huffman@47108 ` 1652` ```lemma equal_int_code [code]: ``` huffman@47108 ` 1653` ``` "HOL.equal 0 (0::int) \ True" ``` huffman@47108 ` 1654` ``` "HOL.equal 0 (Pos l) \ False" ``` huffman@47108 ` 1655` ``` "HOL.equal 0 (Neg l) \ False" ``` huffman@47108 ` 1656` ``` "HOL.equal (Pos k) 0 \ False" ``` huffman@47108 ` 1657` ``` "HOL.equal (Pos k) (Pos l) \ HOL.equal k l" ``` huffman@47108 ` 1658` ``` "HOL.equal (Pos k) (Neg l) \ False" ``` huffman@47108 ` 1659` ``` "HOL.equal (Neg k) 0 \ False" ``` huffman@47108 ` 1660` ``` "HOL.equal (Neg k) (Pos l) \ False" ``` huffman@47108 ` 1661` ``` "HOL.equal (Neg k) (Neg l) \ HOL.equal k l" ``` huffman@47108 ` 1662` ``` by (auto simp add: equal) ``` haftmann@26507 ` 1663` huffman@47108 ` 1664` ```lemma equal_int_refl [code nbe]: ``` haftmann@38857 ` 1665` ``` "HOL.equal (k::int) k \ True" ``` huffman@47108 ` 1666` ``` by (fact equal_refl) ``` haftmann@26507 ` 1667` haftmann@28562 ` 1668` ```lemma less_eq_int_code [code]: ``` huffman@47108 ` 1669` ``` "0 \ (0::int) \ True" ``` huffman@47108 ` 1670` ``` "0 \ Pos l \ True" ``` huffman@47108 ` 1671` ``` "0 \ Neg l \ False" ``` huffman@47108 ` 1672` ``` "Pos k \ 0 \ False" ``` huffman@47108 ` 1673` ``` "Pos k \ Pos l \ k \ l" ``` huffman@47108 ` 1674` ``` "Pos k \ Neg l \ False" ``` huffman@47108 ` 1675` ``` "Neg k \ 0 \ True" ``` huffman@47108 ` 1676` ``` "Neg k \ Pos l \ True" ``` huffman@47108 ` 1677` ``` "Neg k \ Neg l \ l \ k" ``` huffman@28958 ` 1678` ``` by simp_all ``` haftmann@26507 ` 1679` haftmann@28562 ` 1680` ```lemma less_int_code [code]: ``` huffman@47108 ` 1681` ``` "0 < (0::int) \ False" ``` huffman@47108 ` 1682` ``` "0 < Pos l \ True" ``` huffman@47108 ` 1683` ``` "0 < Neg l \ False" ``` huffman@47108 ` 1684` ``` "Pos k < 0 \ False" ``` huffman@47108 ` 1685` ``` "Pos k < Pos l \ k < l" ``` huffman@47108 ` 1686` ``` "Pos k < Neg l \ False" ``` huffman@47108 ` 1687` ``` "Neg k < 0 \ True" ``` huffman@47108 ` 1688` ``` "Neg k < Pos l \ True" ``` huffman@47108 ` 1689` ``` "Neg k < Neg l \ l < k" ``` huffman@28958 ` 1690` ``` by simp_all ``` haftmann@25919 ` 1691` huffman@47108 ` 1692` ```lemma nat_numeral [simp, code_abbrev]: ``` huffman@47108 ` 1693` ``` "nat (numeral k) = numeral k" ``` huffman@47108 ` 1694` ``` by (simp add: nat_eq_iff) ``` haftmann@25919 ` 1695` huffman@47108 ` 1696` ```lemma nat_code [code]: ``` huffman@47108 ` 1697` ``` "nat (Int.Neg k) = 0" ``` huffman@47108 ` 1698` ``` "nat 0 = 0" ``` huffman@47108 ` 1699` ``` "nat (Int.Pos k) = nat_of_num k" ``` huffman@47108 ` 1700` ``` by (simp_all add: nat_of_num_numeral nat_numeral) ``` haftmann@25928 ` 1701` huffman@47108 ` 1702` ```lemma (in ring_1) of_int_code [code]: ``` huffman@47108 ` 1703` ``` "of_int (Int.Neg k) = neg_numeral k" ``` huffman@47108 ` 1704` ``` "of_int 0 = 0" ``` huffman@47108 ` 1705` ``` "of_int (Int.Pos k) = numeral k" ``` huffman@47108 ` 1706` ``` by simp_all ``` haftmann@25919 ` 1707` huffman@47108 ` 1708` huffman@47108 ` 1709` ```text {* Serializer setup *} ``` haftmann@25919 ` 1710` haftmann@25919 ` 1711` ```code_modulename SML ``` haftmann@33364 ` 1712` ``` Int Arith ``` haftmann@25919 ` 1713` haftmann@25919 ` 1714` ```code_modulename OCaml ``` haftmann@33364 ` 1715` ``` Int Arith ``` haftmann@25919 ` 1716` haftmann@25919 ` 1717` ```code_modulename Haskell ``` haftmann@33364 ` 1718` ``` Int Arith ``` haftmann@25919 ` 1719` haftmann@25919 ` 1720` ```quickcheck_params [default_type = int] ``` haftmann@25919 ` 1721` huffman@47108 ` 1722` ```hide_const (open) Pos Neg sub dup ``` haftmann@25919 ` 1723` haftmann@25919 ` 1724` haftmann@25919 ` 1725` ```subsection {* Legacy theorems *} ``` haftmann@25919 ` 1726` haftmann@25919 ` 1727` ```lemmas inj_int = inj_of_nat [where 'a=int] ``` haftmann@25919 ` 1728` ```lemmas zadd_int = of_nat_add [where 'a=int, symmetric] ``` haftmann@25919 ` 1729` ```lemmas int_mult = of_nat_mult [where 'a=int] ``` haftmann@25919 ` 1730` ```lemmas zmult_int = of_nat_mult [where 'a=int, symmetric] ``` wenzelm@45607 ` 1731` ```lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="n"] for n ``` haftmann@25919 ` 1732` ```lemmas zless_int = of_nat_less_iff [where 'a=int] ``` wenzelm@45607 ` 1733` ```lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="k"] for k ``` haftmann@25919 ` 1734` ```lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int] ``` haftmann@25919 ` 1735` ```lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int] ``` wenzelm@45607 ` 1736` ```lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="n"] for n ``` haftmann@25919 ` 1737` ```lemmas int_0 = of_nat_0 [where 'a=int] ``` haftmann@25919 ` 1738` ```lemmas int_1 = of_nat_1 [where 'a=int] ``` haftmann@25919 ` 1739` ```lemmas int_Suc = of_nat_Suc [where 'a=int] ``` wenzelm@45607 ` 1740` ```lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m"] for m ``` haftmann@25919 ` 1741` ```lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int] ``` haftmann@25919 ` 1742` ```lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric] ``` haftmann@30960 ` 1743` haftmann@31015 ` 1744` ```lemma zpower_zpower: ``` haftmann@31015 ` 1745` ``` "(x ^ y) ^ z = (x ^ (y * z)::int)" ``` haftmann@31015 ` 1746` ``` by (rule power_mult [symmetric]) ``` haftmann@31015 ` 1747` haftmann@31015 ` 1748` ```lemma int_power: ``` haftmann@31015 ` 1749` ``` "int (m ^ n) = int m ^ n" ``` haftmann@31015 ` 1750` ``` by (rule of_nat_power) ``` haftmann@31015 ` 1751` haftmann@31015 ` 1752` ```lemmas zpower_int = int_power [symmetric] ``` haftmann@31015 ` 1753` haftmann@25919 ` 1754` ```end ``` huffman@47108 ` 1755`