src/HOL/Int.thy
 author wenzelm Mon Mar 22 20:58:52 2010 +0100 (2010-03-22) changeset 35898 c890a3835d15 parent 35829 c5f54c04a1aa child 36076 882403378a41 permissions -rw-r--r--
 haftmann@25919 ` 1` ```(* Title: Int.thy ``` haftmann@25919 ` 2` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` haftmann@25919 ` 3` ``` Tobias Nipkow, Florian Haftmann, TU Muenchen ``` haftmann@25919 ` 4` ``` Copyright 1994 University of Cambridge ``` haftmann@25919 ` 5` haftmann@25919 ` 6` ```*) ``` haftmann@25919 ` 7` haftmann@25919 ` 8` ```header {* The Integers as Equivalence Classes over Pairs of Natural Numbers *} ``` haftmann@25919 ` 9` haftmann@25919 ` 10` ```theory Int ``` krauss@26748 ` 11` ```imports Equiv_Relations Nat Wellfounded ``` haftmann@25919 ` 12` ```uses ``` haftmann@25919 ` 13` ``` ("Tools/numeral.ML") ``` haftmann@25919 ` 14` ``` ("Tools/numeral_syntax.ML") ``` haftmann@31068 ` 15` ``` ("Tools/int_arith.ML") ``` haftmann@25919 ` 16` ```begin ``` haftmann@25919 ` 17` haftmann@25919 ` 18` ```subsection {* The equivalence relation underlying the integers *} ``` haftmann@25919 ` 19` haftmann@28661 ` 20` ```definition intrel :: "((nat \ nat) \ (nat \ nat)) set" where ``` haftmann@28562 ` 21` ``` [code del]: "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }" ``` haftmann@25919 ` 22` haftmann@25919 ` 23` ```typedef (Integ) ``` haftmann@25919 ` 24` ``` int = "UNIV//intrel" ``` haftmann@25919 ` 25` ``` by (auto simp add: quotient_def) ``` haftmann@25919 ` 26` haftmann@25919 ` 27` ```instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}" ``` haftmann@25919 ` 28` ```begin ``` haftmann@25919 ` 29` haftmann@25919 ` 30` ```definition ``` haftmann@28562 ` 31` ``` Zero_int_def [code del]: "0 = Abs_Integ (intrel `` {(0, 0)})" ``` haftmann@25919 ` 32` haftmann@25919 ` 33` ```definition ``` haftmann@28562 ` 34` ``` One_int_def [code del]: "1 = Abs_Integ (intrel `` {(1, 0)})" ``` haftmann@25919 ` 35` haftmann@25919 ` 36` ```definition ``` haftmann@28562 ` 37` ``` add_int_def [code del]: "z + w = Abs_Integ ``` haftmann@25919 ` 38` ``` (\(x, y) \ Rep_Integ z. \(u, v) \ Rep_Integ w. ``` haftmann@25919 ` 39` ``` intrel `` {(x + u, y + v)})" ``` haftmann@25919 ` 40` haftmann@25919 ` 41` ```definition ``` haftmann@28562 ` 42` ``` minus_int_def [code del]: ``` haftmann@25919 ` 43` ``` "- z = Abs_Integ (\(x, y) \ Rep_Integ z. intrel `` {(y, x)})" ``` haftmann@25919 ` 44` haftmann@25919 ` 45` ```definition ``` haftmann@28562 ` 46` ``` diff_int_def [code del]: "z - w = z + (-w \ int)" ``` haftmann@25919 ` 47` haftmann@25919 ` 48` ```definition ``` haftmann@28562 ` 49` ``` mult_int_def [code del]: "z * w = Abs_Integ ``` haftmann@25919 ` 50` ``` (\(x, y) \ Rep_Integ z. \(u,v ) \ Rep_Integ w. ``` haftmann@25919 ` 51` ``` intrel `` {(x*u + y*v, x*v + y*u)})" ``` haftmann@25919 ` 52` haftmann@25919 ` 53` ```definition ``` haftmann@28562 ` 54` ``` le_int_def [code del]: ``` haftmann@25919 ` 55` ``` "z \ w \ (\x y u v. x+v \ u+y \ (x, y) \ Rep_Integ z \ (u, v) \ Rep_Integ w)" ``` haftmann@25919 ` 56` haftmann@25919 ` 57` ```definition ``` haftmann@28562 ` 58` ``` less_int_def [code del]: "(z\int) < w \ z \ w \ z \ w" ``` haftmann@25919 ` 59` haftmann@25919 ` 60` ```definition ``` haftmann@25919 ` 61` ``` zabs_def: "\i\int\ = (if i < 0 then - i else i)" ``` haftmann@25919 ` 62` haftmann@25919 ` 63` ```definition ``` haftmann@25919 ` 64` ``` zsgn_def: "sgn (i\int) = (if i=0 then 0 else if 0 intrel) = (x+v = u+y)" ``` haftmann@25919 ` 74` ```by (simp add: intrel_def) ``` haftmann@25919 ` 75` haftmann@25919 ` 76` ```lemma equiv_intrel: "equiv UNIV intrel" ``` nipkow@30198 ` 77` ```by (simp add: intrel_def equiv_def refl_on_def sym_def trans_def) ``` haftmann@25919 ` 78` haftmann@25919 ` 79` ```text{*Reduces equality of equivalence classes to the @{term intrel} relation: ``` haftmann@25919 ` 80` ``` @{term "(intrel `` {x} = intrel `` {y}) = ((x,y) \ intrel)"} *} ``` haftmann@25919 ` 81` ```lemmas equiv_intrel_iff [simp] = eq_equiv_class_iff [OF equiv_intrel UNIV_I UNIV_I] ``` haftmann@25919 ` 82` haftmann@25919 ` 83` ```text{*All equivalence classes belong to set of representatives*} ``` haftmann@25919 ` 84` ```lemma [simp]: "intrel``{(x,y)} \ Integ" ``` haftmann@25919 ` 85` ```by (auto simp add: Integ_def intrel_def quotient_def) ``` haftmann@25919 ` 86` haftmann@25919 ` 87` ```text{*Reduces equality on abstractions to equality on representatives: ``` haftmann@25919 ` 88` ``` @{prop "\x \ Integ; y \ Integ\ \ (Abs_Integ x = Abs_Integ y) = (x=y)"} *} ``` blanchet@35828 ` 89` ```declare Abs_Integ_inject [simp,no_atp] Abs_Integ_inverse [simp,no_atp] ``` haftmann@25919 ` 90` haftmann@25919 ` 91` ```text{*Case analysis on the representation of an integer as an equivalence ``` haftmann@25919 ` 92` ``` class of pairs of naturals.*} ``` haftmann@25919 ` 93` ```lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]: ``` haftmann@25919 ` 94` ``` "(!!x y. z = Abs_Integ(intrel``{(x,y)}) ==> P) ==> P" ``` haftmann@25919 ` 95` ```apply (rule Abs_Integ_cases [of z]) ``` haftmann@25919 ` 96` ```apply (auto simp add: Integ_def quotient_def) ``` haftmann@25919 ` 97` ```done ``` haftmann@25919 ` 98` haftmann@25919 ` 99` haftmann@25919 ` 100` ```subsection {* Arithmetic Operations *} ``` haftmann@25919 ` 101` haftmann@25919 ` 102` ```lemma minus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})" ``` haftmann@25919 ` 103` ```proof - ``` haftmann@25919 ` 104` ``` have "(\(x,y). intrel``{(y,x)}) respects intrel" ``` haftmann@25919 ` 105` ``` by (simp add: congruent_def) ``` haftmann@25919 ` 106` ``` thus ?thesis ``` haftmann@25919 ` 107` ``` by (simp add: minus_int_def UN_equiv_class [OF equiv_intrel]) ``` haftmann@25919 ` 108` ```qed ``` haftmann@25919 ` 109` haftmann@25919 ` 110` ```lemma add: ``` haftmann@25919 ` 111` ``` "Abs_Integ (intrel``{(x,y)}) + Abs_Integ (intrel``{(u,v)}) = ``` haftmann@25919 ` 112` ``` Abs_Integ (intrel``{(x+u, y+v)})" ``` haftmann@25919 ` 113` ```proof - ``` haftmann@25919 ` 114` ``` have "(\z w. (\(x,y). (\(u,v). intrel `` {(x+u, y+v)}) w) z) ``` haftmann@25919 ` 115` ``` respects2 intrel" ``` haftmann@25919 ` 116` ``` by (simp add: congruent2_def) ``` haftmann@25919 ` 117` ``` thus ?thesis ``` haftmann@25919 ` 118` ``` by (simp add: add_int_def UN_UN_split_split_eq ``` haftmann@25919 ` 119` ``` UN_equiv_class2 [OF equiv_intrel equiv_intrel]) ``` haftmann@25919 ` 120` ```qed ``` haftmann@25919 ` 121` haftmann@25919 ` 122` ```text{*Congruence property for multiplication*} ``` haftmann@25919 ` 123` ```lemma mult_congruent2: ``` haftmann@25919 ` 124` ``` "(%p1 p2. (%(x,y). (%(u,v). intrel``{(x*u + y*v, x*v + y*u)}) p2) p1) ``` haftmann@25919 ` 125` ``` respects2 intrel" ``` haftmann@25919 ` 126` ```apply (rule equiv_intrel [THEN congruent2_commuteI]) ``` haftmann@25919 ` 127` ``` apply (force simp add: mult_ac, clarify) ``` haftmann@25919 ` 128` ```apply (simp add: congruent_def mult_ac) ``` haftmann@25919 ` 129` ```apply (rename_tac u v w x y z) ``` haftmann@25919 ` 130` ```apply (subgoal_tac "u*y + x*y = w*y + v*y & u*z + x*z = w*z + v*z") ``` haftmann@25919 ` 131` ```apply (simp add: mult_ac) ``` haftmann@25919 ` 132` ```apply (simp add: add_mult_distrib [symmetric]) ``` haftmann@25919 ` 133` ```done ``` haftmann@25919 ` 134` haftmann@25919 ` 135` ```lemma mult: ``` haftmann@25919 ` 136` ``` "Abs_Integ((intrel``{(x,y)})) * Abs_Integ((intrel``{(u,v)})) = ``` haftmann@25919 ` 137` ``` Abs_Integ(intrel `` {(x*u + y*v, x*v + y*u)})" ``` haftmann@25919 ` 138` ```by (simp add: mult_int_def UN_UN_split_split_eq mult_congruent2 ``` haftmann@25919 ` 139` ``` UN_equiv_class2 [OF equiv_intrel equiv_intrel]) ``` haftmann@25919 ` 140` haftmann@25919 ` 141` ```text{*The integers form a @{text comm_ring_1}*} ``` haftmann@25919 ` 142` ```instance int :: comm_ring_1 ``` haftmann@25919 ` 143` ```proof ``` haftmann@25919 ` 144` ``` fix i j k :: int ``` haftmann@25919 ` 145` ``` show "(i + j) + k = i + (j + k)" ``` haftmann@25919 ` 146` ``` by (cases i, cases j, cases k) (simp add: add add_assoc) ``` haftmann@25919 ` 147` ``` show "i + j = j + i" ``` haftmann@25919 ` 148` ``` by (cases i, cases j) (simp add: add_ac add) ``` haftmann@25919 ` 149` ``` show "0 + i = i" ``` haftmann@25919 ` 150` ``` by (cases i) (simp add: Zero_int_def add) ``` haftmann@25919 ` 151` ``` show "- i + i = 0" ``` haftmann@25919 ` 152` ``` by (cases i) (simp add: Zero_int_def minus add) ``` haftmann@25919 ` 153` ``` show "i - j = i + - j" ``` haftmann@25919 ` 154` ``` by (simp add: diff_int_def) ``` haftmann@25919 ` 155` ``` show "(i * j) * k = i * (j * k)" ``` nipkow@29667 ` 156` ``` by (cases i, cases j, cases k) (simp add: mult algebra_simps) ``` haftmann@25919 ` 157` ``` show "i * j = j * i" ``` nipkow@29667 ` 158` ``` by (cases i, cases j) (simp add: mult algebra_simps) ``` haftmann@25919 ` 159` ``` show "1 * i = i" ``` haftmann@25919 ` 160` ``` by (cases i) (simp add: One_int_def mult) ``` haftmann@25919 ` 161` ``` show "(i + j) * k = i * k + j * k" ``` nipkow@29667 ` 162` ``` by (cases i, cases j, cases k) (simp add: add mult algebra_simps) ``` haftmann@25919 ` 163` ``` show "0 \ (1::int)" ``` haftmann@25919 ` 164` ``` by (simp add: Zero_int_def One_int_def) ``` haftmann@25919 ` 165` ```qed ``` haftmann@25919 ` 166` haftmann@25919 ` 167` ```lemma int_def: "of_nat m = Abs_Integ (intrel `` {(m, 0)})" ``` haftmann@25919 ` 168` ```by (induct m, simp_all add: Zero_int_def One_int_def add) ``` haftmann@25919 ` 169` haftmann@25919 ` 170` haftmann@25919 ` 171` ```subsection {* The @{text "\"} Ordering *} ``` haftmann@25919 ` 172` haftmann@25919 ` 173` ```lemma le: ``` haftmann@25919 ` 174` ``` "(Abs_Integ(intrel``{(x,y)}) \ Abs_Integ(intrel``{(u,v)})) = (x+v \ u+y)" ``` haftmann@25919 ` 175` ```by (force simp add: le_int_def) ``` haftmann@25919 ` 176` haftmann@25919 ` 177` ```lemma less: ``` haftmann@25919 ` 178` ``` "(Abs_Integ(intrel``{(x,y)}) < Abs_Integ(intrel``{(u,v)})) = (x+v < u+y)" ``` haftmann@25919 ` 179` ```by (simp add: less_int_def le order_less_le) ``` haftmann@25919 ` 180` haftmann@25919 ` 181` ```instance int :: linorder ``` haftmann@25919 ` 182` ```proof ``` haftmann@25919 ` 183` ``` fix i j k :: int ``` haftmann@27682 ` 184` ``` show antisym: "i \ j \ j \ i \ i = j" ``` haftmann@27682 ` 185` ``` by (cases i, cases j) (simp add: le) ``` haftmann@27682 ` 186` ``` show "(i < j) = (i \ j \ \ j \ i)" ``` haftmann@27682 ` 187` ``` by (auto simp add: less_int_def dest: antisym) ``` haftmann@25919 ` 188` ``` show "i \ i" ``` haftmann@25919 ` 189` ``` by (cases i) (simp add: le) ``` haftmann@25919 ` 190` ``` show "i \ j \ j \ k \ i \ k" ``` haftmann@25919 ` 191` ``` by (cases i, cases j, cases k) (simp add: le) ``` haftmann@25919 ` 192` ``` show "i \ j \ j \ i" ``` haftmann@25919 ` 193` ``` by (cases i, cases j) (simp add: le linorder_linear) ``` haftmann@25919 ` 194` ```qed ``` haftmann@25919 ` 195` haftmann@25919 ` 196` ```instantiation int :: distrib_lattice ``` haftmann@25919 ` 197` ```begin ``` haftmann@25919 ` 198` haftmann@25919 ` 199` ```definition ``` haftmann@25919 ` 200` ``` "(inf \ int \ int \ int) = min" ``` haftmann@25919 ` 201` haftmann@25919 ` 202` ```definition ``` haftmann@25919 ` 203` ``` "(sup \ int \ int \ int) = max" ``` haftmann@25919 ` 204` haftmann@25919 ` 205` ```instance ``` haftmann@25919 ` 206` ``` by intro_classes ``` haftmann@25919 ` 207` ``` (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1) ``` haftmann@25919 ` 208` haftmann@25919 ` 209` ```end ``` haftmann@25919 ` 210` haftmann@35028 ` 211` ```instance int :: ordered_cancel_ab_semigroup_add ``` haftmann@25919 ` 212` ```proof ``` haftmann@25919 ` 213` ``` fix i j k :: int ``` haftmann@25919 ` 214` ``` show "i \ j \ k + i \ k + j" ``` haftmann@25919 ` 215` ``` by (cases i, cases j, cases k) (simp add: le add) ``` haftmann@25919 ` 216` ```qed ``` haftmann@25919 ` 217` haftmann@25961 ` 218` haftmann@25919 ` 219` ```text{*Strict Monotonicity of Multiplication*} ``` haftmann@25919 ` 220` haftmann@25919 ` 221` ```text{*strict, in 1st argument; proof is by induction on k>0*} ``` haftmann@25919 ` 222` ```lemma zmult_zless_mono2_lemma: ``` haftmann@25919 ` 223` ``` "(i::int) 0 of_nat k * i < of_nat k * j" ``` haftmann@25919 ` 224` ```apply (induct "k", simp) ``` haftmann@25919 ` 225` ```apply (simp add: left_distrib) ``` haftmann@25919 ` 226` ```apply (case_tac "k=0") ``` haftmann@25919 ` 227` ```apply (simp_all add: add_strict_mono) ``` haftmann@25919 ` 228` ```done ``` haftmann@25919 ` 229` haftmann@25919 ` 230` ```lemma zero_le_imp_eq_int: "(0::int) \ k ==> \n. k = of_nat n" ``` haftmann@25919 ` 231` ```apply (cases k) ``` haftmann@25919 ` 232` ```apply (auto simp add: le add int_def Zero_int_def) ``` haftmann@25919 ` 233` ```apply (rule_tac x="x-y" in exI, simp) ``` haftmann@25919 ` 234` ```done ``` haftmann@25919 ` 235` haftmann@25919 ` 236` ```lemma zero_less_imp_eq_int: "(0::int) < k ==> \n>0. k = of_nat n" ``` haftmann@25919 ` 237` ```apply (cases k) ``` haftmann@25919 ` 238` ```apply (simp add: less int_def Zero_int_def) ``` haftmann@25919 ` 239` ```apply (rule_tac x="x-y" in exI, simp) ``` haftmann@25919 ` 240` ```done ``` haftmann@25919 ` 241` haftmann@25919 ` 242` ```lemma zmult_zless_mono2: "[| i k*i < k*j" ``` haftmann@25919 ` 243` ```apply (drule zero_less_imp_eq_int) ``` haftmann@25919 ` 244` ```apply (auto simp add: zmult_zless_mono2_lemma) ``` haftmann@25919 ` 245` ```done ``` haftmann@25919 ` 246` haftmann@25919 ` 247` ```text{*The integers form an ordered integral domain*} ``` haftmann@35028 ` 248` ```instance int :: linordered_idom ``` haftmann@25919 ` 249` ```proof ``` haftmann@25919 ` 250` ``` fix i j k :: int ``` haftmann@25919 ` 251` ``` show "i < j \ 0 < k \ k * i < k * j" ``` haftmann@25919 ` 252` ``` by (rule zmult_zless_mono2) ``` haftmann@25919 ` 253` ``` show "\i\ = (if i < 0 then -i else i)" ``` haftmann@25919 ` 254` ``` by (simp only: zabs_def) ``` haftmann@25919 ` 255` ``` show "sgn (i\int) = (if i=0 then 0 else if 0 w + (1\int) \ z" ``` haftmann@25919 ` 260` ```apply (cases w, cases z) ``` haftmann@25919 ` 261` ```apply (simp add: less le add One_int_def) ``` haftmann@25919 ` 262` ```done ``` haftmann@25919 ` 263` haftmann@25919 ` 264` ```lemma zless_iff_Suc_zadd: ``` haftmann@25919 ` 265` ``` "(w \ int) < z \ (\n. z = w + of_nat (Suc n))" ``` haftmann@25919 ` 266` ```apply (cases z, cases w) ``` haftmann@25919 ` 267` ```apply (auto simp add: less add int_def) ``` haftmann@25919 ` 268` ```apply (rename_tac a b c d) ``` haftmann@25919 ` 269` ```apply (rule_tac x="a+d - Suc(c+b)" in exI) ``` haftmann@25919 ` 270` ```apply arith ``` haftmann@25919 ` 271` ```done ``` haftmann@25919 ` 272` haftmann@25919 ` 273` ```lemmas int_distrib = ``` haftmann@25919 ` 274` ``` left_distrib [of "z1::int" "z2" "w", standard] ``` haftmann@25919 ` 275` ``` right_distrib [of "w::int" "z1" "z2", standard] ``` haftmann@25919 ` 276` ``` left_diff_distrib [of "z1::int" "z2" "w", standard] ``` haftmann@25919 ` 277` ``` right_diff_distrib [of "w::int" "z1" "z2", standard] ``` haftmann@25919 ` 278` haftmann@25919 ` 279` haftmann@25919 ` 280` ```subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*} ``` haftmann@25919 ` 281` haftmann@25919 ` 282` ```context ring_1 ``` haftmann@25919 ` 283` ```begin ``` haftmann@25919 ` 284` haftmann@31015 ` 285` ```definition of_int :: "int \ 'a" where ``` haftmann@28562 ` 286` ``` [code del]: "of_int z = contents (\(i, j) \ Rep_Integ z. { of_nat i - of_nat j })" ``` haftmann@25919 ` 287` haftmann@25919 ` 288` ```lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j" ``` haftmann@25919 ` 289` ```proof - ``` haftmann@25919 ` 290` ``` have "(\(i,j). { of_nat i - (of_nat j :: 'a) }) respects intrel" ``` nipkow@29667 ` 291` ``` by (simp add: congruent_def algebra_simps of_nat_add [symmetric] ``` haftmann@25919 ` 292` ``` del: of_nat_add) ``` haftmann@25919 ` 293` ``` thus ?thesis ``` haftmann@25919 ` 294` ``` by (simp add: of_int_def UN_equiv_class [OF equiv_intrel]) ``` haftmann@25919 ` 295` ```qed ``` haftmann@25919 ` 296` haftmann@25919 ` 297` ```lemma of_int_0 [simp]: "of_int 0 = 0" ``` nipkow@29667 ` 298` ```by (simp add: of_int Zero_int_def) ``` haftmann@25919 ` 299` haftmann@25919 ` 300` ```lemma of_int_1 [simp]: "of_int 1 = 1" ``` nipkow@29667 ` 301` ```by (simp add: of_int One_int_def) ``` haftmann@25919 ` 302` haftmann@25919 ` 303` ```lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z" ``` nipkow@29667 ` 304` ```by (cases w, cases z, simp add: algebra_simps of_int add) ``` haftmann@25919 ` 305` haftmann@25919 ` 306` ```lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)" ``` nipkow@29667 ` 307` ```by (cases z, simp add: algebra_simps of_int minus) ``` haftmann@25919 ` 308` haftmann@25919 ` 309` ```lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z" ``` haftmann@35050 ` 310` ```by (simp add: diff_minus Groups.diff_minus) ``` haftmann@25919 ` 311` haftmann@25919 ` 312` ```lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z" ``` haftmann@25919 ` 313` ```apply (cases w, cases z) ``` nipkow@29667 ` 314` ```apply (simp add: algebra_simps of_int mult of_nat_mult) ``` haftmann@25919 ` 315` ```done ``` haftmann@25919 ` 316` haftmann@25919 ` 317` ```text{*Collapse nested embeddings*} ``` haftmann@25919 ` 318` ```lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n" ``` nipkow@29667 ` 319` ```by (induct n) auto ``` haftmann@25919 ` 320` haftmann@31015 ` 321` ```lemma of_int_power: ``` haftmann@31015 ` 322` ``` "of_int (z ^ n) = of_int z ^ n" ``` haftmann@31015 ` 323` ``` by (induct n) simp_all ``` haftmann@31015 ` 324` haftmann@25919 ` 325` ```end ``` haftmann@25919 ` 326` haftmann@35028 ` 327` ```context linordered_idom ``` haftmann@25919 ` 328` ```begin ``` haftmann@25919 ` 329` haftmann@25919 ` 330` ```lemma of_int_le_iff [simp]: ``` haftmann@25919 ` 331` ``` "of_int w \ of_int z \ w \ z" ``` nipkow@29667 ` 332` ```by (cases w, cases z, simp add: of_int le minus algebra_simps of_nat_add [symmetric] del: of_nat_add) ``` haftmann@25919 ` 333` haftmann@25919 ` 334` ```text{*Special cases where either operand is zero*} ``` haftmann@25919 ` 335` ```lemmas of_int_0_le_iff [simp] = of_int_le_iff [of 0, simplified] ``` haftmann@25919 ` 336` ```lemmas of_int_le_0_iff [simp] = of_int_le_iff [of _ 0, simplified] ``` haftmann@25919 ` 337` haftmann@25919 ` 338` ```lemma of_int_less_iff [simp]: ``` haftmann@25919 ` 339` ``` "of_int w < of_int z \ w < z" ``` haftmann@25919 ` 340` ``` by (simp add: not_le [symmetric] linorder_not_le [symmetric]) ``` haftmann@25919 ` 341` haftmann@25919 ` 342` ```text{*Special cases where either operand is zero*} ``` haftmann@25919 ` 343` ```lemmas of_int_0_less_iff [simp] = of_int_less_iff [of 0, simplified] ``` haftmann@25919 ` 344` ```lemmas of_int_less_0_iff [simp] = of_int_less_iff [of _ 0, simplified] ``` haftmann@25919 ` 345` haftmann@25919 ` 346` ```end ``` haftmann@25919 ` 347` haftmann@25919 ` 348` ```text{*Class for unital rings with characteristic zero. ``` haftmann@25919 ` 349` ``` Includes non-ordered rings like the complex numbers.*} ``` haftmann@25919 ` 350` ```class ring_char_0 = ring_1 + semiring_char_0 ``` haftmann@25919 ` 351` ```begin ``` haftmann@25919 ` 352` haftmann@25919 ` 353` ```lemma of_int_eq_iff [simp]: ``` haftmann@25919 ` 354` ``` "of_int w = of_int z \ w = z" ``` haftmann@25919 ` 355` ```apply (cases w, cases z, simp add: of_int) ``` haftmann@25919 ` 356` ```apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq) ``` haftmann@25919 ` 357` ```apply (simp only: of_nat_add [symmetric] of_nat_eq_iff) ``` haftmann@25919 ` 358` ```done ``` haftmann@25919 ` 359` haftmann@25919 ` 360` ```text{*Special cases where either operand is zero*} ``` haftmann@25919 ` 361` ```lemmas of_int_0_eq_iff [simp] = of_int_eq_iff [of 0, simplified] ``` haftmann@25919 ` 362` ```lemmas of_int_eq_0_iff [simp] = of_int_eq_iff [of _ 0, simplified] ``` haftmann@25919 ` 363` haftmann@25919 ` 364` ```end ``` haftmann@25919 ` 365` haftmann@35028 ` 366` ```text{*Every @{text linordered_idom} has characteristic zero.*} ``` haftmann@35028 ` 367` ```subclass (in linordered_idom) ring_char_0 by intro_locales ``` haftmann@25919 ` 368` haftmann@25919 ` 369` ```lemma of_int_eq_id [simp]: "of_int = id" ``` haftmann@25919 ` 370` ```proof ``` haftmann@25919 ` 371` ``` fix z show "of_int z = id z" ``` haftmann@25919 ` 372` ``` by (cases z) (simp add: of_int add minus int_def diff_minus) ``` haftmann@25919 ` 373` ```qed ``` haftmann@25919 ` 374` haftmann@25919 ` 375` haftmann@25919 ` 376` ```subsection {* Magnitude of an Integer, as a Natural Number: @{text nat} *} ``` haftmann@25919 ` 377` haftmann@25919 ` 378` ```definition ``` haftmann@25919 ` 379` ``` nat :: "int \ nat" ``` haftmann@25919 ` 380` ```where ``` haftmann@28562 ` 381` ``` [code del]: "nat z = contents (\(x, y) \ Rep_Integ z. {x-y})" ``` haftmann@25919 ` 382` haftmann@25919 ` 383` ```lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y" ``` haftmann@25919 ` 384` ```proof - ``` haftmann@25919 ` 385` ``` have "(\(x,y). {x-y}) respects intrel" ``` haftmann@25919 ` 386` ``` by (simp add: congruent_def) arith ``` haftmann@25919 ` 387` ``` thus ?thesis ``` haftmann@25919 ` 388` ``` by (simp add: nat_def UN_equiv_class [OF equiv_intrel]) ``` haftmann@25919 ` 389` ```qed ``` haftmann@25919 ` 390` haftmann@25919 ` 391` ```lemma nat_int [simp]: "nat (of_nat n) = n" ``` haftmann@25919 ` 392` ```by (simp add: nat int_def) ``` haftmann@25919 ` 393` huffman@35216 ` 394` ```(* FIXME: duplicates nat_0 *) ``` haftmann@25919 ` 395` ```lemma nat_zero [simp]: "nat 0 = 0" ``` haftmann@25919 ` 396` ```by (simp add: Zero_int_def nat) ``` haftmann@25919 ` 397` haftmann@25919 ` 398` ```lemma int_nat_eq [simp]: "of_nat (nat z) = (if 0 \ z then z else 0)" ``` haftmann@25919 ` 399` ```by (cases z, simp add: nat le int_def Zero_int_def) ``` haftmann@25919 ` 400` haftmann@25919 ` 401` ```corollary nat_0_le: "0 \ z ==> of_nat (nat z) = z" ``` haftmann@25919 ` 402` ```by simp ``` haftmann@25919 ` 403` haftmann@25919 ` 404` ```lemma nat_le_0 [simp]: "z \ 0 ==> nat z = 0" ``` haftmann@25919 ` 405` ```by (cases z, simp add: nat le Zero_int_def) ``` haftmann@25919 ` 406` haftmann@25919 ` 407` ```lemma nat_le_eq_zle: "0 < w | 0 \ z ==> (nat w \ nat z) = (w\z)" ``` haftmann@25919 ` 408` ```apply (cases w, cases z) ``` haftmann@25919 ` 409` ```apply (simp add: nat le linorder_not_le [symmetric] Zero_int_def, arith) ``` haftmann@25919 ` 410` ```done ``` haftmann@25919 ` 411` haftmann@25919 ` 412` ```text{*An alternative condition is @{term "0 \ w"} *} ``` haftmann@25919 ` 413` ```corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)" ``` haftmann@25919 ` 414` ```by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) ``` haftmann@25919 ` 415` haftmann@25919 ` 416` ```corollary nat_less_eq_zless: "0 \ w ==> (nat w < nat z) = (w z" and "\m. z = of_nat m \ P" ``` haftmann@25919 ` 427` ``` shows P ``` haftmann@25919 ` 428` ``` using assms by (blast dest: nat_0_le sym) ``` haftmann@25919 ` 429` haftmann@25919 ` 430` ```lemma nat_eq_iff: "(nat w = m) = (if 0 \ w then w = of_nat m else m=0)" ``` haftmann@25919 ` 431` ```by (cases w, simp add: nat le int_def Zero_int_def, arith) ``` haftmann@25919 ` 432` haftmann@25919 ` 433` ```corollary nat_eq_iff2: "(m = nat w) = (if 0 \ w then w = of_nat m else m=0)" ``` haftmann@25919 ` 434` ```by (simp only: eq_commute [of m] nat_eq_iff) ``` haftmann@25919 ` 435` haftmann@25919 ` 436` ```lemma nat_less_iff: "0 \ w ==> (nat w < m) = (w < of_nat m)" ``` haftmann@25919 ` 437` ```apply (cases w) ``` nipkow@29700 ` 438` ```apply (simp add: nat le int_def Zero_int_def linorder_not_le[symmetric], arith) ``` haftmann@25919 ` 439` ```done ``` haftmann@25919 ` 440` nipkow@29700 ` 441` ```lemma nat_0_iff[simp]: "nat(i::int) = 0 \ i\0" ``` nipkow@29700 ` 442` ```by(simp add: nat_eq_iff) arith ``` nipkow@29700 ` 443` haftmann@25919 ` 444` ```lemma int_eq_iff: "(of_nat m = z) = (m = nat z & 0 \ z)" ``` haftmann@25919 ` 445` ```by (auto simp add: nat_eq_iff2) ``` haftmann@25919 ` 446` haftmann@25919 ` 447` ```lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)" ``` haftmann@25919 ` 448` ```by (insert zless_nat_conj [of 0], auto) ``` haftmann@25919 ` 449` haftmann@25919 ` 450` ```lemma nat_add_distrib: ``` haftmann@25919 ` 451` ``` "[| (0::int) \ z; 0 \ z' |] ==> nat (z+z') = nat z + nat z'" ``` haftmann@25919 ` 452` ```by (cases z, cases z', simp add: nat add le Zero_int_def) ``` haftmann@25919 ` 453` haftmann@25919 ` 454` ```lemma nat_diff_distrib: ``` haftmann@25919 ` 455` ``` "[| (0::int) \ z'; z' \ z |] ==> nat (z-z') = nat z - nat z'" ``` haftmann@25919 ` 456` ```by (cases z, cases z', ``` haftmann@25919 ` 457` ``` simp add: nat add minus diff_minus le Zero_int_def) ``` haftmann@25919 ` 458` haftmann@25919 ` 459` ```lemma nat_zminus_int [simp]: "nat (- (of_nat n)) = 0" ``` haftmann@25919 ` 460` ```by (simp add: int_def minus nat Zero_int_def) ``` haftmann@25919 ` 461` haftmann@25919 ` 462` ```lemma zless_nat_eq_int_zless: "(m < nat z) = (of_nat m < z)" ``` haftmann@25919 ` 463` ```by (cases z, simp add: nat less int_def, arith) ``` haftmann@25919 ` 464` haftmann@25919 ` 465` ```context ring_1 ``` haftmann@25919 ` 466` ```begin ``` haftmann@25919 ` 467` haftmann@25919 ` 468` ```lemma of_nat_nat: "0 \ z \ of_nat (nat z) = of_int z" ``` haftmann@25919 ` 469` ``` by (cases z rule: eq_Abs_Integ) ``` haftmann@25919 ` 470` ``` (simp add: nat le of_int Zero_int_def of_nat_diff) ``` haftmann@25919 ` 471` haftmann@25919 ` 472` ```end ``` haftmann@25919 ` 473` krauss@29779 ` 474` ```text {* For termination proofs: *} ``` krauss@29779 ` 475` ```lemma measure_function_int[measure_function]: "is_measure (nat o abs)" .. ``` krauss@29779 ` 476` haftmann@25919 ` 477` haftmann@25919 ` 478` ```subsection{*Lemmas about the Function @{term of_nat} and Orderings*} ``` haftmann@25919 ` 479` haftmann@25919 ` 480` ```lemma negative_zless_0: "- (of_nat (Suc n)) < (0 \ int)" ``` haftmann@25919 ` 481` ```by (simp add: order_less_le del: of_nat_Suc) ``` haftmann@25919 ` 482` haftmann@25919 ` 483` ```lemma negative_zless [iff]: "- (of_nat (Suc n)) < (of_nat m \ int)" ``` haftmann@25919 ` 484` ```by (rule negative_zless_0 [THEN order_less_le_trans], simp) ``` haftmann@25919 ` 485` haftmann@25919 ` 486` ```lemma negative_zle_0: "- of_nat n \ (0 \ int)" ``` haftmann@25919 ` 487` ```by (simp add: minus_le_iff) ``` haftmann@25919 ` 488` haftmann@25919 ` 489` ```lemma negative_zle [iff]: "- of_nat n \ (of_nat m \ int)" ``` haftmann@25919 ` 490` ```by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff]) ``` haftmann@25919 ` 491` haftmann@25919 ` 492` ```lemma not_zle_0_negative [simp]: "~ (0 \ - (of_nat (Suc n) \ int))" ``` haftmann@25919 ` 493` ```by (subst le_minus_iff, simp del: of_nat_Suc) ``` haftmann@25919 ` 494` haftmann@25919 ` 495` ```lemma int_zle_neg: "((of_nat n \ int) \ - of_nat m) = (n = 0 & m = 0)" ``` haftmann@25919 ` 496` ```by (simp add: int_def le minus Zero_int_def) ``` haftmann@25919 ` 497` haftmann@25919 ` 498` ```lemma not_int_zless_negative [simp]: "~ ((of_nat n \ int) < - of_nat m)" ``` haftmann@25919 ` 499` ```by (simp add: linorder_not_less) ``` haftmann@25919 ` 500` haftmann@25919 ` 501` ```lemma negative_eq_positive [simp]: "((- of_nat n \ int) = of_nat m) = (n = 0 & m = 0)" ``` haftmann@25919 ` 502` ```by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg) ``` haftmann@25919 ` 503` haftmann@25919 ` 504` ```lemma zle_iff_zadd: "(w\int) \ z \ (\n. z = w + of_nat n)" ``` haftmann@25919 ` 505` ```proof - ``` haftmann@25919 ` 506` ``` have "(w \ z) = (0 \ z - w)" ``` haftmann@25919 ` 507` ``` by (simp only: le_diff_eq add_0_left) ``` haftmann@25919 ` 508` ``` also have "\ = (\n. z - w = of_nat n)" ``` haftmann@25919 ` 509` ``` by (auto elim: zero_le_imp_eq_int) ``` haftmann@25919 ` 510` ``` also have "\ = (\n. z = w + of_nat n)" ``` nipkow@29667 ` 511` ``` by (simp only: algebra_simps) ``` haftmann@25919 ` 512` ``` finally show ?thesis . ``` haftmann@25919 ` 513` ```qed ``` haftmann@25919 ` 514` haftmann@25919 ` 515` ```lemma zadd_int_left: "of_nat m + (of_nat n + z) = of_nat (m + n) + (z\int)" ``` haftmann@25919 ` 516` ```by simp ``` haftmann@25919 ` 517` haftmann@25919 ` 518` ```lemma int_Suc0_eq_1: "of_nat (Suc 0) = (1\int)" ``` haftmann@25919 ` 519` ```by simp ``` haftmann@25919 ` 520` haftmann@25919 ` 521` ```text{*This version is proved for all ordered rings, not just integers! ``` haftmann@25919 ` 522` ``` It is proved here because attribute @{text arith_split} is not available ``` haftmann@35050 ` 523` ``` in theory @{text Rings}. ``` haftmann@25919 ` 524` ``` But is it really better than just rewriting with @{text abs_if}?*} ``` blanchet@35828 ` 525` ```lemma abs_split [arith_split,no_atp]: ``` haftmann@35028 ` 526` ``` "P(abs(a::'a::linordered_idom)) = ((0 \ a --> P a) & (a < 0 --> P(-a)))" ``` haftmann@25919 ` 527` ```by (force dest: order_less_le_trans simp add: abs_if linorder_not_less) ``` haftmann@25919 ` 528` haftmann@25919 ` 529` ```lemma negD: "(x \ int) < 0 \ \n. x = - (of_nat (Suc n))" ``` haftmann@25919 ` 530` ```apply (cases x) ``` haftmann@25919 ` 531` ```apply (auto simp add: le minus Zero_int_def int_def order_less_le) ``` haftmann@25919 ` 532` ```apply (rule_tac x="y - Suc x" in exI, arith) ``` haftmann@25919 ` 533` ```done ``` haftmann@25919 ` 534` haftmann@25919 ` 535` haftmann@25919 ` 536` ```subsection {* Cases and induction *} ``` haftmann@25919 ` 537` haftmann@25919 ` 538` ```text{*Now we replace the case analysis rule by a more conventional one: ``` haftmann@25919 ` 539` ```whether an integer is negative or not.*} ``` haftmann@25919 ` 540` haftmann@25919 ` 541` ```theorem int_cases [cases type: int, case_names nonneg neg]: ``` haftmann@25919 ` 542` ``` "[|!! n. (z \ int) = of_nat n ==> P; !! n. z = - (of_nat (Suc n)) ==> P |] ==> P" ``` haftmann@25919 ` 543` ```apply (cases "z < 0", blast dest!: negD) ``` haftmann@25919 ` 544` ```apply (simp add: linorder_not_less del: of_nat_Suc) ``` haftmann@25919 ` 545` ```apply auto ``` haftmann@25919 ` 546` ```apply (blast dest: nat_0_le [THEN sym]) ``` haftmann@25919 ` 547` ```done ``` haftmann@25919 ` 548` haftmann@25919 ` 549` ```theorem int_induct [induct type: int, case_names nonneg neg]: ``` haftmann@25919 ` 550` ``` "[|!! n. P (of_nat n \ int); !!n. P (- (of_nat (Suc n))) |] ==> P z" ``` haftmann@25919 ` 551` ``` by (cases z rule: int_cases) auto ``` haftmann@25919 ` 552` haftmann@25919 ` 553` ```text{*Contributed by Brian Huffman*} ``` haftmann@25919 ` 554` ```theorem int_diff_cases: ``` haftmann@25919 ` 555` ``` obtains (diff) m n where "(z\int) = of_nat m - of_nat n" ``` haftmann@25919 ` 556` ```apply (cases z rule: eq_Abs_Integ) ``` haftmann@25919 ` 557` ```apply (rule_tac m=x and n=y in diff) ``` haftmann@25919 ` 558` ```apply (simp add: int_def diff_def minus add) ``` haftmann@25919 ` 559` ```done ``` haftmann@25919 ` 560` haftmann@25919 ` 561` haftmann@25919 ` 562` ```subsection {* Binary representation *} ``` haftmann@25919 ` 563` haftmann@25919 ` 564` ```text {* ``` haftmann@25919 ` 565` ``` This formalization defines binary arithmetic in terms of the integers ``` haftmann@25919 ` 566` ``` rather than using a datatype. This avoids multiple representations (leading ``` haftmann@25919 ` 567` ``` zeroes, etc.) See @{text "ZF/Tools/twos-compl.ML"}, function @{text ``` haftmann@25919 ` 568` ``` int_of_binary}, for the numerical interpretation. ``` haftmann@25919 ` 569` haftmann@25919 ` 570` ``` The representation expects that @{text "(m mod 2)"} is 0 or 1, ``` haftmann@25919 ` 571` ``` even if m is negative; ``` haftmann@25919 ` 572` ``` For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus ``` haftmann@25919 ` 573` ``` @{text "-5 = (-3)*2 + 1"}. ``` haftmann@25919 ` 574` ``` ``` haftmann@25919 ` 575` ``` This two's complement binary representation derives from the paper ``` haftmann@25919 ` 576` ``` "An Efficient Representation of Arithmetic for Term Rewriting" by ``` haftmann@25919 ` 577` ``` Dave Cohen and Phil Watson, Rewriting Techniques and Applications, ``` haftmann@25919 ` 578` ``` Springer LNCS 488 (240-251), 1991. ``` haftmann@25919 ` 579` ```*} ``` haftmann@25919 ` 580` huffman@28958 ` 581` ```subsubsection {* The constructors @{term Bit0}, @{term Bit1}, @{term Pls} and @{term Min} *} ``` huffman@28958 ` 582` haftmann@25919 ` 583` ```definition ``` haftmann@25919 ` 584` ``` Pls :: int where ``` haftmann@28562 ` 585` ``` [code del]: "Pls = 0" ``` haftmann@25919 ` 586` haftmann@25919 ` 587` ```definition ``` haftmann@25919 ` 588` ``` Min :: int where ``` haftmann@28562 ` 589` ``` [code del]: "Min = - 1" ``` haftmann@25919 ` 590` haftmann@25919 ` 591` ```definition ``` huffman@26086 ` 592` ``` Bit0 :: "int \ int" where ``` haftmann@28562 ` 593` ``` [code del]: "Bit0 k = k + k" ``` huffman@26086 ` 594` huffman@26086 ` 595` ```definition ``` huffman@26086 ` 596` ``` Bit1 :: "int \ int" where ``` haftmann@28562 ` 597` ``` [code del]: "Bit1 k = 1 + k + k" ``` haftmann@25919 ` 598` haftmann@29608 ` 599` ```class number = -- {* for numeric types: nat, int, real, \dots *} ``` haftmann@25919 ` 600` ``` fixes number_of :: "int \ 'a" ``` haftmann@25919 ` 601` haftmann@25919 ` 602` ```use "Tools/numeral.ML" ``` haftmann@25919 ` 603` haftmann@25919 ` 604` ```syntax ``` haftmann@25919 ` 605` ``` "_Numeral" :: "num_const \ 'a" ("_") ``` haftmann@25919 ` 606` haftmann@25919 ` 607` ```use "Tools/numeral_syntax.ML" ``` wenzelm@35123 ` 608` ```setup Numeral_Syntax.setup ``` haftmann@25919 ` 609` haftmann@25919 ` 610` ```abbreviation ``` haftmann@25919 ` 611` ``` "Numeral0 \ number_of Pls" ``` haftmann@25919 ` 612` haftmann@25919 ` 613` ```abbreviation ``` huffman@26086 ` 614` ``` "Numeral1 \ number_of (Bit1 Pls)" ``` haftmann@25919 ` 615` haftmann@25919 ` 616` ```lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)" ``` haftmann@25919 ` 617` ``` -- {* Unfold all @{text let}s involving constants *} ``` haftmann@25919 ` 618` ``` unfolding Let_def .. ``` haftmann@25919 ` 619` haftmann@25919 ` 620` ```definition ``` haftmann@25919 ` 621` ``` succ :: "int \ int" where ``` haftmann@28562 ` 622` ``` [code del]: "succ k = k + 1" ``` haftmann@25919 ` 623` haftmann@25919 ` 624` ```definition ``` haftmann@25919 ` 625` ``` pred :: "int \ int" where ``` haftmann@28562 ` 626` ``` [code del]: "pred k = k - 1" ``` haftmann@25919 ` 627` haftmann@25919 ` 628` ```lemmas ``` haftmann@25919 ` 629` ``` max_number_of [simp] = max_def ``` huffman@35216 ` 630` ``` [of "number_of u" "number_of v", standard] ``` haftmann@25919 ` 631` ```and ``` haftmann@25919 ` 632` ``` min_number_of [simp] = min_def ``` huffman@35216 ` 633` ``` [of "number_of u" "number_of v", standard] ``` haftmann@25919 ` 634` ``` -- {* unfolding @{text minx} and @{text max} on numerals *} ``` haftmann@25919 ` 635` haftmann@25919 ` 636` ```lemmas numeral_simps = ``` huffman@26086 ` 637` ``` succ_def pred_def Pls_def Min_def Bit0_def Bit1_def ``` haftmann@25919 ` 638` haftmann@25919 ` 639` ```text {* Removal of leading zeroes *} ``` haftmann@25919 ` 640` haftmann@31998 ` 641` ```lemma Bit0_Pls [simp, code_post]: ``` huffman@26086 ` 642` ``` "Bit0 Pls = Pls" ``` haftmann@25919 ` 643` ``` unfolding numeral_simps by simp ``` haftmann@25919 ` 644` haftmann@31998 ` 645` ```lemma Bit1_Min [simp, code_post]: ``` huffman@26086 ` 646` ``` "Bit1 Min = Min" ``` haftmann@25919 ` 647` ``` unfolding numeral_simps by simp ``` haftmann@25919 ` 648` huffman@26075 ` 649` ```lemmas normalize_bin_simps = ``` huffman@26086 ` 650` ``` Bit0_Pls Bit1_Min ``` huffman@26075 ` 651` haftmann@25919 ` 652` huffman@28958 ` 653` ```subsubsection {* Successor and predecessor functions *} ``` huffman@28958 ` 654` huffman@28958 ` 655` ```text {* Successor *} ``` huffman@28958 ` 656` huffman@28958 ` 657` ```lemma succ_Pls: ``` huffman@26086 ` 658` ``` "succ Pls = Bit1 Pls" ``` haftmann@25919 ` 659` ``` unfolding numeral_simps by simp ``` haftmann@25919 ` 660` huffman@28958 ` 661` ```lemma succ_Min: ``` haftmann@25919 ` 662` ``` "succ Min = Pls" ``` haftmann@25919 ` 663` ``` unfolding numeral_simps by simp ``` haftmann@25919 ` 664` huffman@28958 ` 665` ```lemma succ_Bit0: ``` huffman@26086 ` 666` ``` "succ (Bit0 k) = Bit1 k" ``` haftmann@25919 ` 667` ``` unfolding numeral_simps by simp ``` haftmann@25919 ` 668` huffman@28958 ` 669` ```lemma succ_Bit1: ``` huffman@26086 ` 670` ``` "succ (Bit1 k) = Bit0 (succ k)" ``` haftmann@25919 ` 671` ``` unfolding numeral_simps by simp ``` haftmann@25919 ` 672` huffman@28958 ` 673` ```lemmas succ_bin_simps [simp] = ``` huffman@26086 ` 674` ``` succ_Pls succ_Min succ_Bit0 succ_Bit1 ``` huffman@26075 ` 675` huffman@28958 ` 676` ```text {* Predecessor *} ``` huffman@28958 ` 677` huffman@28958 ` 678` ```lemma pred_Pls: ``` haftmann@25919 ` 679` ``` "pred Pls = Min" ``` haftmann@25919 ` 680` ``` unfolding numeral_simps by simp ``` haftmann@25919 ` 681` huffman@28958 ` 682` ```lemma pred_Min: ``` huffman@26086 ` 683` ``` "pred Min = Bit0 Min" ``` haftmann@25919 ` 684` ``` unfolding numeral_simps by simp ``` haftmann@25919 ` 685` huffman@28958 ` 686` ```lemma pred_Bit0: ``` huffman@26086 ` 687` ``` "pred (Bit0 k) = Bit1 (pred k)" ``` haftmann@25919 ` 688` ``` unfolding numeral_simps by simp ``` haftmann@25919 ` 689` huffman@28958 ` 690` ```lemma pred_Bit1: ``` huffman@26086 ` 691` ``` "pred (Bit1 k) = Bit0 k" ``` huffman@26086 ` 692` ``` unfolding numeral_simps by simp ``` huffman@26086 ` 693` huffman@28958 ` 694` ```lemmas pred_bin_simps [simp] = ``` huffman@26086 ` 695` ``` pred_Pls pred_Min pred_Bit0 pred_Bit1 ``` huffman@26075 ` 696` huffman@28958 ` 697` huffman@28958 ` 698` ```subsubsection {* Binary arithmetic *} ``` huffman@28958 ` 699` huffman@28958 ` 700` ```text {* Addition *} ``` huffman@28958 ` 701` huffman@28958 ` 702` ```lemma add_Pls: ``` huffman@28958 ` 703` ``` "Pls + k = k" ``` huffman@28958 ` 704` ``` unfolding numeral_simps by simp ``` huffman@28958 ` 705` huffman@28958 ` 706` ```lemma add_Min: ``` huffman@28958 ` 707` ``` "Min + k = pred k" ``` huffman@28958 ` 708` ``` unfolding numeral_simps by simp ``` huffman@28958 ` 709` huffman@28958 ` 710` ```lemma add_Bit0_Bit0: ``` huffman@28958 ` 711` ``` "(Bit0 k) + (Bit0 l) = Bit0 (k + l)" ``` huffman@28958 ` 712` ``` unfolding numeral_simps by simp ``` huffman@28958 ` 713` huffman@28958 ` 714` ```lemma add_Bit0_Bit1: ``` huffman@28958 ` 715` ``` "(Bit0 k) + (Bit1 l) = Bit1 (k + l)" ``` huffman@28958 ` 716` ``` unfolding numeral_simps by simp ``` huffman@28958 ` 717` huffman@28958 ` 718` ```lemma add_Bit1_Bit0: ``` huffman@28958 ` 719` ``` "(Bit1 k) + (Bit0 l) = Bit1 (k + l)" ``` huffman@28958 ` 720` ``` unfolding numeral_simps by simp ``` huffman@28958 ` 721` huffman@28958 ` 722` ```lemma add_Bit1_Bit1: ``` huffman@28958 ` 723` ``` "(Bit1 k) + (Bit1 l) = Bit0 (k + succ l)" ``` huffman@28958 ` 724` ``` unfolding numeral_simps by simp ``` huffman@28958 ` 725` huffman@28958 ` 726` ```lemma add_Pls_right: ``` huffman@28958 ` 727` ``` "k + Pls = k" ``` huffman@28958 ` 728` ``` unfolding numeral_simps by simp ``` huffman@28958 ` 729` huffman@28958 ` 730` ```lemma add_Min_right: ``` huffman@28958 ` 731` ``` "k + Min = pred k" ``` huffman@28958 ` 732` ``` unfolding numeral_simps by simp ``` huffman@28958 ` 733` huffman@28958 ` 734` ```lemmas add_bin_simps [simp] = ``` huffman@28958 ` 735` ``` add_Pls add_Min add_Pls_right add_Min_right ``` huffman@28958 ` 736` ``` add_Bit0_Bit0 add_Bit0_Bit1 add_Bit1_Bit0 add_Bit1_Bit1 ``` huffman@28958 ` 737` huffman@28958 ` 738` ```text {* Negation *} ``` huffman@28958 ` 739` huffman@28958 ` 740` ```lemma minus_Pls: ``` haftmann@25919 ` 741` ``` "- Pls = Pls" ``` huffman@28958 ` 742` ``` unfolding numeral_simps by simp ``` huffman@28958 ` 743` huffman@28958 ` 744` ```lemma minus_Min: ``` huffman@26086 ` 745` ``` "- Min = Bit1 Pls" ``` huffman@28958 ` 746` ``` unfolding numeral_simps by simp ``` huffman@28958 ` 747` huffman@28958 ` 748` ```lemma minus_Bit0: ``` huffman@26086 ` 749` ``` "- (Bit0 k) = Bit0 (- k)" ``` huffman@28958 ` 750` ``` unfolding numeral_simps by simp ``` huffman@28958 ` 751` huffman@28958 ` 752` ```lemma minus_Bit1: ``` huffman@26086 ` 753` ``` "- (Bit1 k) = Bit1 (pred (- k))" ``` huffman@26086 ` 754` ``` unfolding numeral_simps by simp ``` haftmann@25919 ` 755` huffman@28958 ` 756` ```lemmas minus_bin_simps [simp] = ``` huffman@26086 ` 757` ``` minus_Pls minus_Min minus_Bit0 minus_Bit1 ``` huffman@26075 ` 758` huffman@28958 ` 759` ```text {* Subtraction *} ``` huffman@28958 ` 760` huffman@29046 ` 761` ```lemma diff_bin_simps [simp]: ``` huffman@29046 ` 762` ``` "k - Pls = k" ``` huffman@29046 ` 763` ``` "k - Min = succ k" ``` huffman@29046 ` 764` ``` "Pls - (Bit0 l) = Bit0 (Pls - l)" ``` huffman@29046 ` 765` ``` "Pls - (Bit1 l) = Bit1 (Min - l)" ``` huffman@29046 ` 766` ``` "Min - (Bit0 l) = Bit1 (Min - l)" ``` huffman@29046 ` 767` ``` "Min - (Bit1 l) = Bit0 (Min - l)" ``` huffman@28958 ` 768` ``` "(Bit0 k) - (Bit0 l) = Bit0 (k - l)" ``` huffman@28958 ` 769` ``` "(Bit0 k) - (Bit1 l) = Bit1 (pred k - l)" ``` huffman@28958 ` 770` ``` "(Bit1 k) - (Bit0 l) = Bit1 (k - l)" ``` huffman@28958 ` 771` ``` "(Bit1 k) - (Bit1 l) = Bit0 (k - l)" ``` huffman@29046 ` 772` ``` unfolding numeral_simps by simp_all ``` huffman@28958 ` 773` huffman@28958 ` 774` ```text {* Multiplication *} ``` huffman@28958 ` 775` huffman@28958 ` 776` ```lemma mult_Pls: ``` huffman@28958 ` 777` ``` "Pls * w = Pls" ``` huffman@26086 ` 778` ``` unfolding numeral_simps by simp ``` haftmann@25919 ` 779` huffman@28958 ` 780` ```lemma mult_Min: ``` haftmann@25919 ` 781` ``` "Min * k = - k" ``` haftmann@25919 ` 782` ``` unfolding numeral_simps by simp ``` haftmann@25919 ` 783` huffman@28958 ` 784` ```lemma mult_Bit0: ``` huffman@26086 ` 785` ``` "(Bit0 k) * l = Bit0 (k * l)" ``` huffman@26086 ` 786` ``` unfolding numeral_simps int_distrib by simp ``` haftmann@25919 ` 787` huffman@28958 ` 788` ```lemma mult_Bit1: ``` huffman@26086 ` 789` ``` "(Bit1 k) * l = (Bit0 (k * l)) + l" ``` huffman@28958 ` 790` ``` unfolding numeral_simps int_distrib by simp ``` huffman@28958 ` 791` huffman@28958 ` 792` ```lemmas mult_bin_simps [simp] = ``` huffman@26086 ` 793` ``` mult_Pls mult_Min mult_Bit0 mult_Bit1 ``` huffman@26075 ` 794` haftmann@25919 ` 795` huffman@28958 ` 796` ```subsubsection {* Binary comparisons *} ``` huffman@28958 ` 797` huffman@28958 ` 798` ```text {* Preliminaries *} ``` huffman@28958 ` 799` huffman@28958 ` 800` ```lemma even_less_0_iff: ``` haftmann@35028 ` 801` ``` "a + a < 0 \ a < (0::'a::linordered_idom)" ``` huffman@28958 ` 802` ```proof - ``` huffman@28958 ` 803` ``` have "a + a < 0 \ (1+1)*a < 0" by (simp add: left_distrib) ``` huffman@28958 ` 804` ``` also have "(1+1)*a < 0 \ a < 0" ``` huffman@28958 ` 805` ``` by (simp add: mult_less_0_iff zero_less_two ``` huffman@28958 ` 806` ``` order_less_not_sym [OF zero_less_two]) ``` huffman@28958 ` 807` ``` finally show ?thesis . ``` huffman@28958 ` 808` ```qed ``` huffman@28958 ` 809` huffman@28958 ` 810` ```lemma le_imp_0_less: ``` huffman@28958 ` 811` ``` assumes le: "0 \ z" ``` huffman@28958 ` 812` ``` shows "(0::int) < 1 + z" ``` huffman@28958 ` 813` ```proof - ``` huffman@28958 ` 814` ``` have "0 \ z" by fact ``` huffman@28958 ` 815` ``` also have "... < z + 1" by (rule less_add_one) ``` huffman@28958 ` 816` ``` also have "... = 1 + z" by (simp add: add_ac) ``` huffman@28958 ` 817` ``` finally show "0 < 1 + z" . ``` huffman@28958 ` 818` ```qed ``` huffman@28958 ` 819` huffman@28958 ` 820` ```lemma odd_less_0_iff: ``` huffman@28958 ` 821` ``` "(1 + z + z < 0) = (z < (0::int))" ``` huffman@28958 ` 822` ```proof (cases z rule: int_cases) ``` huffman@28958 ` 823` ``` case (nonneg n) ``` huffman@28958 ` 824` ``` thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing ``` huffman@28958 ` 825` ``` le_imp_0_less [THEN order_less_imp_le]) ``` huffman@28958 ` 826` ```next ``` huffman@28958 ` 827` ``` case (neg n) ``` huffman@30079 ` 828` ``` thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1 ``` huffman@30079 ` 829` ``` add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric]) ``` huffman@28958 ` 830` ```qed ``` huffman@28958 ` 831` huffman@28985 ` 832` ```lemma bin_less_0_simps: ``` huffman@28958 ` 833` ``` "Pls < 0 \ False" ``` huffman@28958 ` 834` ``` "Min < 0 \ True" ``` huffman@28958 ` 835` ``` "Bit0 w < 0 \ w < 0" ``` huffman@28958 ` 836` ``` "Bit1 w < 0 \ w < 0" ``` huffman@28958 ` 837` ``` unfolding numeral_simps ``` huffman@28958 ` 838` ``` by (simp_all add: even_less_0_iff odd_less_0_iff) ``` huffman@28958 ` 839` huffman@28958 ` 840` ```lemma less_bin_lemma: "k < l \ k - l < (0::int)" ``` huffman@28958 ` 841` ``` by simp ``` huffman@28958 ` 842` huffman@28958 ` 843` ```lemma le_iff_pred_less: "k \ l \ pred k < l" ``` huffman@28958 ` 844` ``` unfolding numeral_simps ``` huffman@28958 ` 845` ``` proof ``` huffman@28958 ` 846` ``` have "k - 1 < k" by simp ``` huffman@28958 ` 847` ``` also assume "k \ l" ``` huffman@28958 ` 848` ``` finally show "k - 1 < l" . ``` huffman@28958 ` 849` ``` next ``` huffman@28958 ` 850` ``` assume "k - 1 < l" ``` huffman@28958 ` 851` ``` hence "(k - 1) + 1 \ l" by (rule zless_imp_add1_zle) ``` huffman@28958 ` 852` ``` thus "k \ l" by simp ``` huffman@28958 ` 853` ``` qed ``` huffman@28958 ` 854` huffman@28958 ` 855` ```lemma succ_pred: "succ (pred x) = x" ``` huffman@28958 ` 856` ``` unfolding numeral_simps by simp ``` huffman@28958 ` 857` huffman@28958 ` 858` ```text {* Less-than *} ``` huffman@28958 ` 859` huffman@28958 ` 860` ```lemma less_bin_simps [simp]: ``` huffman@28958 ` 861` ``` "Pls < Pls \ False" ``` huffman@28958 ` 862` ``` "Pls < Min \ False" ``` huffman@28958 ` 863` ``` "Pls < Bit0 k \ Pls < k" ``` huffman@28958 ` 864` ``` "Pls < Bit1 k \ Pls \ k" ``` huffman@28958 ` 865` ``` "Min < Pls \ True" ``` huffman@28958 ` 866` ``` "Min < Min \ False" ``` huffman@28958 ` 867` ``` "Min < Bit0 k \ Min < k" ``` huffman@28958 ` 868` ``` "Min < Bit1 k \ Min < k" ``` huffman@28958 ` 869` ``` "Bit0 k < Pls \ k < Pls" ``` huffman@28958 ` 870` ``` "Bit0 k < Min \ k \ Min" ``` huffman@28958 ` 871` ``` "Bit1 k < Pls \ k < Pls" ``` huffman@28958 ` 872` ``` "Bit1 k < Min \ k < Min" ``` huffman@28958 ` 873` ``` "Bit0 k < Bit0 l \ k < l" ``` huffman@28958 ` 874` ``` "Bit0 k < Bit1 l \ k \ l" ``` huffman@28958 ` 875` ``` "Bit1 k < Bit0 l \ k < l" ``` huffman@28958 ` 876` ``` "Bit1 k < Bit1 l \ k < l" ``` huffman@28958 ` 877` ``` unfolding le_iff_pred_less ``` huffman@28958 ` 878` ``` less_bin_lemma [of Pls] ``` huffman@28958 ` 879` ``` less_bin_lemma [of Min] ``` huffman@28958 ` 880` ``` less_bin_lemma [of "k"] ``` huffman@28958 ` 881` ``` less_bin_lemma [of "Bit0 k"] ``` huffman@28958 ` 882` ``` less_bin_lemma [of "Bit1 k"] ``` huffman@28958 ` 883` ``` less_bin_lemma [of "pred Pls"] ``` huffman@28958 ` 884` ``` less_bin_lemma [of "pred k"] ``` huffman@28985 ` 885` ``` by (simp_all add: bin_less_0_simps succ_pred) ``` huffman@28958 ` 886` huffman@28958 ` 887` ```text {* Less-than-or-equal *} ``` huffman@28958 ` 888` huffman@28958 ` 889` ```lemma le_bin_simps [simp]: ``` huffman@28958 ` 890` ``` "Pls \ Pls \ True" ``` huffman@28958 ` 891` ``` "Pls \ Min \ False" ``` huffman@28958 ` 892` ``` "Pls \ Bit0 k \ Pls \ k" ``` huffman@28958 ` 893` ``` "Pls \ Bit1 k \ Pls \ k" ``` huffman@28958 ` 894` ``` "Min \ Pls \ True" ``` huffman@28958 ` 895` ``` "Min \ Min \ True" ``` huffman@28958 ` 896` ``` "Min \ Bit0 k \ Min < k" ``` huffman@28958 ` 897` ``` "Min \ Bit1 k \ Min \ k" ``` huffman@28958 ` 898` ``` "Bit0 k \ Pls \ k \ Pls" ``` huffman@28958 ` 899` ``` "Bit0 k \ Min \ k \ Min" ``` huffman@28958 ` 900` ``` "Bit1 k \ Pls \ k < Pls" ``` huffman@28958 ` 901` ``` "Bit1 k \ Min \ k \ Min" ``` huffman@28958 ` 902` ``` "Bit0 k \ Bit0 l \ k \ l" ``` huffman@28958 ` 903` ``` "Bit0 k \ Bit1 l \ k \ l" ``` huffman@28958 ` 904` ``` "Bit1 k \ Bit0 l \ k < l" ``` huffman@28958 ` 905` ``` "Bit1 k \ Bit1 l \ k \ l" ``` huffman@28958 ` 906` ``` unfolding not_less [symmetric] ``` huffman@28958 ` 907` ``` by (simp_all add: not_le) ``` huffman@28958 ` 908` huffman@28958 ` 909` ```text {* Equality *} ``` huffman@28958 ` 910` huffman@28958 ` 911` ```lemma eq_bin_simps [simp]: ``` huffman@28958 ` 912` ``` "Pls = Pls \ True" ``` huffman@28958 ` 913` ``` "Pls = Min \ False" ``` huffman@28958 ` 914` ``` "Pls = Bit0 l \ Pls = l" ``` huffman@28958 ` 915` ``` "Pls = Bit1 l \ False" ``` huffman@28958 ` 916` ``` "Min = Pls \ False" ``` huffman@28958 ` 917` ``` "Min = Min \ True" ``` huffman@28958 ` 918` ``` "Min = Bit0 l \ False" ``` huffman@28958 ` 919` ``` "Min = Bit1 l \ Min = l" ``` huffman@28958 ` 920` ``` "Bit0 k = Pls \ k = Pls" ``` huffman@28958 ` 921` ``` "Bit0 k = Min \ False" ``` huffman@28958 ` 922` ``` "Bit1 k = Pls \ False" ``` huffman@28958 ` 923` ``` "Bit1 k = Min \ k = Min" ``` huffman@28958 ` 924` ``` "Bit0 k = Bit0 l \ k = l" ``` huffman@28958 ` 925` ``` "Bit0 k = Bit1 l \ False" ``` huffman@28958 ` 926` ``` "Bit1 k = Bit0 l \ False" ``` huffman@28958 ` 927` ``` "Bit1 k = Bit1 l \ k = l" ``` huffman@28958 ` 928` ``` unfolding order_eq_iff [where 'a=int] ``` huffman@28958 ` 929` ``` by (simp_all add: not_less) ``` huffman@28958 ` 930` huffman@28958 ` 931` haftmann@25919 ` 932` ```subsection {* Converting Numerals to Rings: @{term number_of} *} ``` haftmann@25919 ` 933` haftmann@25919 ` 934` ```class number_ring = number + comm_ring_1 + ``` haftmann@25919 ` 935` ``` assumes number_of_eq: "number_of k = of_int k" ``` haftmann@25919 ` 936` haftmann@25919 ` 937` ```text {* self-embedding of the integers *} ``` haftmann@25919 ` 938` haftmann@25919 ` 939` ```instantiation int :: number_ring ``` haftmann@25919 ` 940` ```begin ``` haftmann@25919 ` 941` haftmann@28724 ` 942` ```definition int_number_of_def [code del]: ``` haftmann@28724 ` 943` ``` "number_of w = (of_int w \ int)" ``` haftmann@25919 ` 944` haftmann@28724 ` 945` ```instance proof ``` haftmann@28724 ` 946` ```qed (simp only: int_number_of_def) ``` haftmann@25919 ` 947` haftmann@25919 ` 948` ```end ``` haftmann@25919 ` 949` haftmann@25919 ` 950` ```lemma number_of_is_id: ``` haftmann@25919 ` 951` ``` "number_of (k::int) = k" ``` haftmann@25919 ` 952` ``` unfolding int_number_of_def by simp ``` haftmann@25919 ` 953` haftmann@25919 ` 954` ```lemma number_of_succ: ``` haftmann@25919 ` 955` ``` "number_of (succ k) = (1 + number_of k ::'a::number_ring)" ``` haftmann@25919 ` 956` ``` unfolding number_of_eq numeral_simps by simp ``` haftmann@25919 ` 957` haftmann@25919 ` 958` ```lemma number_of_pred: ``` haftmann@25919 ` 959` ``` "number_of (pred w) = (- 1 + number_of w ::'a::number_ring)" ``` haftmann@25919 ` 960` ``` unfolding number_of_eq numeral_simps by simp ``` haftmann@25919 ` 961` haftmann@25919 ` 962` ```lemma number_of_minus: ``` haftmann@25919 ` 963` ``` "number_of (uminus w) = (- (number_of w)::'a::number_ring)" ``` huffman@28958 ` 964` ``` unfolding number_of_eq by (rule of_int_minus) ``` haftmann@25919 ` 965` haftmann@25919 ` 966` ```lemma number_of_add: ``` haftmann@25919 ` 967` ``` "number_of (v + w) = (number_of v + number_of w::'a::number_ring)" ``` huffman@28958 ` 968` ``` unfolding number_of_eq by (rule of_int_add) ``` huffman@28958 ` 969` huffman@28958 ` 970` ```lemma number_of_diff: ``` huffman@28958 ` 971` ``` "number_of (v - w) = (number_of v - number_of w::'a::number_ring)" ``` huffman@28958 ` 972` ``` unfolding number_of_eq by (rule of_int_diff) ``` haftmann@25919 ` 973` haftmann@25919 ` 974` ```lemma number_of_mult: ``` haftmann@25919 ` 975` ``` "number_of (v * w) = (number_of v * number_of w::'a::number_ring)" ``` huffman@28958 ` 976` ``` unfolding number_of_eq by (rule of_int_mult) ``` haftmann@25919 ` 977` haftmann@25919 ` 978` ```text {* ``` haftmann@25919 ` 979` ``` The correctness of shifting. ``` haftmann@25919 ` 980` ``` But it doesn't seem to give a measurable speed-up. ``` haftmann@25919 ` 981` ```*} ``` haftmann@25919 ` 982` huffman@26086 ` 983` ```lemma double_number_of_Bit0: ``` huffman@26086 ` 984` ``` "(1 + 1) * number_of w = (number_of (Bit0 w) ::'a::number_ring)" ``` haftmann@25919 ` 985` ``` unfolding number_of_eq numeral_simps left_distrib by simp ``` haftmann@25919 ` 986` haftmann@25919 ` 987` ```text {* ``` haftmann@25919 ` 988` ``` Converting numerals 0 and 1 to their abstract versions. ``` haftmann@25919 ` 989` ```*} ``` haftmann@25919 ` 990` haftmann@32272 ` 991` ```lemma numeral_0_eq_0 [simp, code_post]: ``` haftmann@25919 ` 992` ``` "Numeral0 = (0::'a::number_ring)" ``` haftmann@25919 ` 993` ``` unfolding number_of_eq numeral_simps by simp ``` haftmann@25919 ` 994` haftmann@32272 ` 995` ```lemma numeral_1_eq_1 [simp, code_post]: ``` haftmann@25919 ` 996` ``` "Numeral1 = (1::'a::number_ring)" ``` haftmann@25919 ` 997` ``` unfolding number_of_eq numeral_simps by simp ``` haftmann@25919 ` 998` haftmann@25919 ` 999` ```text {* ``` haftmann@25919 ` 1000` ``` Special-case simplification for small constants. ``` haftmann@25919 ` 1001` ```*} ``` haftmann@25919 ` 1002` haftmann@25919 ` 1003` ```text{* ``` haftmann@25919 ` 1004` ``` Unary minus for the abstract constant 1. Cannot be inserted ``` haftmann@25919 ` 1005` ``` as a simprule until later: it is @{text number_of_Min} re-oriented! ``` haftmann@25919 ` 1006` ```*} ``` haftmann@25919 ` 1007` haftmann@25919 ` 1008` ```lemma numeral_m1_eq_minus_1: ``` haftmann@25919 ` 1009` ``` "(-1::'a::number_ring) = - 1" ``` haftmann@25919 ` 1010` ``` unfolding number_of_eq numeral_simps by simp ``` haftmann@25919 ` 1011` haftmann@25919 ` 1012` ```lemma mult_minus1 [simp]: ``` haftmann@25919 ` 1013` ``` "-1 * z = -(z::'a::number_ring)" ``` haftmann@25919 ` 1014` ``` unfolding number_of_eq numeral_simps by simp ``` haftmann@25919 ` 1015` haftmann@25919 ` 1016` ```lemma mult_minus1_right [simp]: ``` haftmann@25919 ` 1017` ``` "z * -1 = -(z::'a::number_ring)" ``` haftmann@25919 ` 1018` ``` unfolding number_of_eq numeral_simps by simp ``` haftmann@25919 ` 1019` haftmann@25919 ` 1020` ```(*Negation of a coefficient*) ``` haftmann@25919 ` 1021` ```lemma minus_number_of_mult [simp]: ``` haftmann@25919 ` 1022` ``` "- (number_of w) * z = number_of (uminus w) * (z::'a::number_ring)" ``` haftmann@25919 ` 1023` ``` unfolding number_of_eq by simp ``` haftmann@25919 ` 1024` haftmann@25919 ` 1025` ```text {* Subtraction *} ``` haftmann@25919 ` 1026` haftmann@25919 ` 1027` ```lemma diff_number_of_eq: ``` haftmann@25919 ` 1028` ``` "number_of v - number_of w = ``` haftmann@25919 ` 1029` ``` (number_of (v + uminus w)::'a::number_ring)" ``` haftmann@25919 ` 1030` ``` unfolding number_of_eq by simp ``` haftmann@25919 ` 1031` haftmann@25919 ` 1032` ```lemma number_of_Pls: ``` haftmann@25919 ` 1033` ``` "number_of Pls = (0::'a::number_ring)" ``` haftmann@25919 ` 1034` ``` unfolding number_of_eq numeral_simps by simp ``` haftmann@25919 ` 1035` haftmann@25919 ` 1036` ```lemma number_of_Min: ``` haftmann@25919 ` 1037` ``` "number_of Min = (- 1::'a::number_ring)" ``` haftmann@25919 ` 1038` ``` unfolding number_of_eq numeral_simps by simp ``` haftmann@25919 ` 1039` huffman@26086 ` 1040` ```lemma number_of_Bit0: ``` huffman@26086 ` 1041` ``` "number_of (Bit0 w) = (0::'a::number_ring) + (number_of w) + (number_of w)" ``` huffman@26086 ` 1042` ``` unfolding number_of_eq numeral_simps by simp ``` huffman@26086 ` 1043` huffman@26086 ` 1044` ```lemma number_of_Bit1: ``` huffman@26086 ` 1045` ``` "number_of (Bit1 w) = (1::'a::number_ring) + (number_of w) + (number_of w)" ``` huffman@26086 ` 1046` ``` unfolding number_of_eq numeral_simps by simp ``` haftmann@25919 ` 1047` haftmann@25919 ` 1048` huffman@28958 ` 1049` ```subsubsection {* Equality of Binary Numbers *} ``` haftmann@25919 ` 1050` haftmann@25919 ` 1051` ```text {* First version by Norbert Voelker *} ``` haftmann@25919 ` 1052` haftmann@25919 ` 1053` ```definition (*for simplifying equalities*) ``` haftmann@25919 ` 1054` ``` iszero :: "'a\semiring_1 \ bool" ``` haftmann@25919 ` 1055` ```where ``` haftmann@25919 ` 1056` ``` "iszero z \ z = 0" ``` haftmann@25919 ` 1057` haftmann@25919 ` 1058` ```lemma iszero_0: "iszero 0" ``` haftmann@25919 ` 1059` ```by (simp add: iszero_def) ``` haftmann@25919 ` 1060` haftmann@25919 ` 1061` ```lemma not_iszero_1: "~ iszero 1" ``` haftmann@25919 ` 1062` ```by (simp add: iszero_def eq_commute) ``` haftmann@25919 ` 1063` huffman@35216 ` 1064` ```lemma eq_number_of_eq [simp]: ``` haftmann@25919 ` 1065` ``` "((number_of x::'a::number_ring) = number_of y) = ``` haftmann@25919 ` 1066` ``` iszero (number_of (x + uminus y) :: 'a)" ``` nipkow@29667 ` 1067` ```unfolding iszero_def number_of_add number_of_minus ``` nipkow@29667 ` 1068` ```by (simp add: algebra_simps) ``` haftmann@25919 ` 1069` haftmann@25919 ` 1070` ```lemma iszero_number_of_Pls: ``` haftmann@25919 ` 1071` ``` "iszero ((number_of Pls)::'a::number_ring)" ``` nipkow@29667 ` 1072` ```unfolding iszero_def numeral_0_eq_0 .. ``` haftmann@25919 ` 1073` haftmann@25919 ` 1074` ```lemma nonzero_number_of_Min: ``` haftmann@25919 ` 1075` ``` "~ iszero ((number_of Min)::'a::number_ring)" ``` nipkow@29667 ` 1076` ```unfolding iszero_def numeral_m1_eq_minus_1 by simp ``` haftmann@25919 ` 1077` haftmann@25919 ` 1078` huffman@28958 ` 1079` ```subsubsection {* Comparisons, for Ordered Rings *} ``` haftmann@25919 ` 1080` haftmann@25919 ` 1081` ```lemmas double_eq_0_iff = double_zero ``` haftmann@25919 ` 1082` haftmann@25919 ` 1083` ```lemma odd_nonzero: ``` haftmann@33296 ` 1084` ``` "1 + z + z \ (0::int)" ``` haftmann@25919 ` 1085` ```proof (cases z rule: int_cases) ``` haftmann@25919 ` 1086` ``` case (nonneg n) ``` haftmann@25919 ` 1087` ``` have le: "0 \ z+z" by (simp add: nonneg add_increasing) ``` haftmann@25919 ` 1088` ``` thus ?thesis using le_imp_0_less [OF le] ``` haftmann@25919 ` 1089` ``` by (auto simp add: add_assoc) ``` haftmann@25919 ` 1090` ```next ``` haftmann@25919 ` 1091` ``` case (neg n) ``` haftmann@25919 ` 1092` ``` show ?thesis ``` haftmann@25919 ` 1093` ``` proof ``` haftmann@25919 ` 1094` ``` assume eq: "1 + z + z = 0" ``` haftmann@25919 ` 1095` ``` have "(0::int) < 1 + (of_nat n + of_nat n)" ``` haftmann@25919 ` 1096` ``` by (simp add: le_imp_0_less add_increasing) ``` haftmann@25919 ` 1097` ``` also have "... = - (1 + z + z)" ``` haftmann@25919 ` 1098` ``` by (simp add: neg add_assoc [symmetric]) ``` haftmann@25919 ` 1099` ``` also have "... = 0" by (simp add: eq) ``` haftmann@25919 ` 1100` ``` finally have "0<0" .. ``` haftmann@25919 ` 1101` ``` thus False by blast ``` haftmann@25919 ` 1102` ``` qed ``` haftmann@25919 ` 1103` ```qed ``` haftmann@25919 ` 1104` huffman@26086 ` 1105` ```lemma iszero_number_of_Bit0: ``` huffman@26086 ` 1106` ``` "iszero (number_of (Bit0 w)::'a) = ``` huffman@26086 ` 1107` ``` iszero (number_of w::'a::{ring_char_0,number_ring})" ``` haftmann@25919 ` 1108` ```proof - ``` haftmann@25919 ` 1109` ``` have "(of_int w + of_int w = (0::'a)) \ (w = 0)" ``` haftmann@25919 ` 1110` ``` proof - ``` haftmann@25919 ` 1111` ``` assume eq: "of_int w + of_int w = (0::'a)" ``` haftmann@25919 ` 1112` ``` then have "of_int (w + w) = (of_int 0 :: 'a)" by simp ``` haftmann@25919 ` 1113` ``` then have "w + w = 0" by (simp only: of_int_eq_iff) ``` haftmann@25919 ` 1114` ``` then show "w = 0" by (simp only: double_eq_0_iff) ``` haftmann@25919 ` 1115` ``` qed ``` huffman@26086 ` 1116` ``` thus ?thesis ``` huffman@26086 ` 1117` ``` by (auto simp add: iszero_def number_of_eq numeral_simps) ``` huffman@26086 ` 1118` ```qed ``` huffman@26086 ` 1119` huffman@26086 ` 1120` ```lemma iszero_number_of_Bit1: ``` huffman@26086 ` 1121` ``` "~ iszero (number_of (Bit1 w)::'a::{ring_char_0,number_ring})" ``` huffman@26086 ` 1122` ```proof - ``` huffman@26086 ` 1123` ``` have "1 + of_int w + of_int w \ (0::'a)" ``` haftmann@25919 ` 1124` ``` proof ``` haftmann@25919 ` 1125` ``` assume eq: "1 + of_int w + of_int w = (0::'a)" ``` haftmann@25919 ` 1126` ``` hence "of_int (1 + w + w) = (of_int 0 :: 'a)" by simp ``` haftmann@25919 ` 1127` ``` hence "1 + w + w = 0" by (simp only: of_int_eq_iff) ``` haftmann@25919 ` 1128` ``` with odd_nonzero show False by blast ``` haftmann@25919 ` 1129` ``` qed ``` huffman@26086 ` 1130` ``` thus ?thesis ``` huffman@26086 ` 1131` ``` by (auto simp add: iszero_def number_of_eq numeral_simps) ``` haftmann@25919 ` 1132` ```qed ``` haftmann@25919 ` 1133` huffman@35216 ` 1134` ```lemmas iszero_simps [simp] = ``` huffman@28985 ` 1135` ``` iszero_0 not_iszero_1 ``` huffman@28985 ` 1136` ``` iszero_number_of_Pls nonzero_number_of_Min ``` huffman@28985 ` 1137` ``` iszero_number_of_Bit0 iszero_number_of_Bit1 ``` huffman@28985 ` 1138` ```(* iszero_number_of_Pls would never normally be used ``` huffman@28985 ` 1139` ``` because its lhs simplifies to "iszero 0" *) ``` haftmann@25919 ` 1140` huffman@28958 ` 1141` ```subsubsection {* The Less-Than Relation *} ``` haftmann@25919 ` 1142` haftmann@25919 ` 1143` ```lemma double_less_0_iff: ``` haftmann@35028 ` 1144` ``` "(a + a < 0) = (a < (0::'a::linordered_idom))" ``` haftmann@25919 ` 1145` ```proof - ``` haftmann@25919 ` 1146` ``` have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib) ``` haftmann@25919 ` 1147` ``` also have "... = (a < 0)" ``` haftmann@25919 ` 1148` ``` by (simp add: mult_less_0_iff zero_less_two ``` haftmann@25919 ` 1149` ``` order_less_not_sym [OF zero_less_two]) ``` haftmann@25919 ` 1150` ``` finally show ?thesis . ``` haftmann@25919 ` 1151` ```qed ``` haftmann@25919 ` 1152` haftmann@25919 ` 1153` ```lemma odd_less_0: ``` haftmann@33296 ` 1154` ``` "(1 + z + z < 0) = (z < (0::int))" ``` haftmann@25919 ` 1155` ```proof (cases z rule: int_cases) ``` haftmann@25919 ` 1156` ``` case (nonneg n) ``` haftmann@25919 ` 1157` ``` thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing ``` haftmann@25919 ` 1158` ``` le_imp_0_less [THEN order_less_imp_le]) ``` haftmann@25919 ` 1159` ```next ``` haftmann@25919 ` 1160` ``` case (neg n) ``` huffman@30079 ` 1161` ``` thus ?thesis by (simp del: of_nat_Suc of_nat_add of_nat_1 ``` huffman@30079 ` 1162` ``` add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric]) ``` haftmann@25919 ` 1163` ```qed ``` haftmann@25919 ` 1164` haftmann@25919 ` 1165` ```text {* Less-Than or Equals *} ``` haftmann@25919 ` 1166` haftmann@25919 ` 1167` ```text {* Reduces @{term "a\b"} to @{term "~ (b x < y" ``` huffman@28962 ` 1212` ``` unfolding number_of_eq by (rule of_int_less_iff) ``` huffman@28962 ` 1213` huffman@28962 ` 1214` ```lemma le_number_of [simp]: ``` haftmann@35028 ` 1215` ``` "(number_of x::'a::{linordered_idom,number_ring}) \ number_of y \ x \ y" ``` huffman@28962 ` 1216` ``` unfolding number_of_eq by (rule of_int_le_iff) ``` huffman@28962 ` 1217` huffman@28967 ` 1218` ```lemma eq_number_of [simp]: ``` huffman@28967 ` 1219` ``` "(number_of x::'a::{ring_char_0,number_ring}) = number_of y \ x = y" ``` huffman@28967 ` 1220` ``` unfolding number_of_eq by (rule of_int_eq_iff) ``` huffman@28967 ` 1221` huffman@35216 ` 1222` ```lemmas rel_simps = ``` huffman@28962 ` 1223` ``` less_number_of less_bin_simps ``` huffman@28962 ` 1224` ``` le_number_of le_bin_simps ``` huffman@28988 ` 1225` ``` eq_number_of_eq eq_bin_simps ``` huffman@29039 ` 1226` ``` iszero_simps ``` haftmann@25919 ` 1227` haftmann@25919 ` 1228` huffman@28958 ` 1229` ```subsubsection {* Simplification of arithmetic when nested to the right. *} ``` haftmann@25919 ` 1230` haftmann@25919 ` 1231` ```lemma add_number_of_left [simp]: ``` haftmann@25919 ` 1232` ``` "number_of v + (number_of w + z) = ``` haftmann@25919 ` 1233` ``` (number_of(v + w) + z::'a::number_ring)" ``` haftmann@25919 ` 1234` ``` by (simp add: add_assoc [symmetric]) ``` haftmann@25919 ` 1235` haftmann@25919 ` 1236` ```lemma mult_number_of_left [simp]: ``` haftmann@25919 ` 1237` ``` "number_of v * (number_of w * z) = ``` haftmann@25919 ` 1238` ``` (number_of(v * w) * z::'a::number_ring)" ``` haftmann@25919 ` 1239` ``` by (simp add: mult_assoc [symmetric]) ``` haftmann@25919 ` 1240` haftmann@25919 ` 1241` ```lemma add_number_of_diff1: ``` haftmann@25919 ` 1242` ``` "number_of v + (number_of w - c) = ``` haftmann@25919 ` 1243` ``` number_of(v + w) - (c::'a::number_ring)" ``` huffman@35216 ` 1244` ``` by (simp add: diff_minus) ``` haftmann@25919 ` 1245` haftmann@25919 ` 1246` ```lemma add_number_of_diff2 [simp]: ``` haftmann@25919 ` 1247` ``` "number_of v + (c - number_of w) = ``` haftmann@25919 ` 1248` ``` number_of (v + uminus w) + (c::'a::number_ring)" ``` nipkow@29667 ` 1249` ```by (simp add: algebra_simps diff_number_of_eq [symmetric]) ``` haftmann@25919 ` 1250` haftmann@25919 ` 1251` haftmann@30652 ` 1252` haftmann@30652 ` 1253` haftmann@25919 ` 1254` ```subsection {* The Set of Integers *} ``` haftmann@25919 ` 1255` haftmann@25919 ` 1256` ```context ring_1 ``` haftmann@25919 ` 1257` ```begin ``` haftmann@25919 ` 1258` haftmann@30652 ` 1259` ```definition Ints :: "'a set" where ``` haftmann@28562 ` 1260` ``` [code del]: "Ints = range of_int" ``` haftmann@25919 ` 1261` haftmann@25919 ` 1262` ```notation (xsymbols) ``` haftmann@25919 ` 1263` ``` Ints ("\") ``` haftmann@25919 ` 1264` huffman@35634 ` 1265` ```lemma Ints_of_int [simp]: "of_int z \ \" ``` huffman@35634 ` 1266` ``` by (simp add: Ints_def) ``` huffman@35634 ` 1267` huffman@35634 ` 1268` ```lemma Ints_of_nat [simp]: "of_nat n \ \" ``` huffman@35634 ` 1269` ```apply (simp add: Ints_def) ``` huffman@35634 ` 1270` ```apply (rule range_eqI) ``` huffman@35634 ` 1271` ```apply (rule of_int_of_nat_eq [symmetric]) ``` huffman@35634 ` 1272` ```done ``` huffman@35634 ` 1273` haftmann@25919 ` 1274` ```lemma Ints_0 [simp]: "0 \ \" ``` haftmann@25919 ` 1275` ```apply (simp add: Ints_def) ``` haftmann@25919 ` 1276` ```apply (rule range_eqI) ``` haftmann@25919 ` 1277` ```apply (rule of_int_0 [symmetric]) ``` haftmann@25919 ` 1278` ```done ``` haftmann@25919 ` 1279` haftmann@25919 ` 1280` ```lemma Ints_1 [simp]: "1 \ \" ``` haftmann@25919 ` 1281` ```apply (simp add: Ints_def) ``` haftmann@25919 ` 1282` ```apply (rule range_eqI) ``` haftmann@25919 ` 1283` ```apply (rule of_int_1 [symmetric]) ``` haftmann@25919 ` 1284` ```done ``` haftmann@25919 ` 1285` haftmann@25919 ` 1286` ```lemma Ints_add [simp]: "a \ \ \ b \ \ \ a + b \ \" ``` haftmann@25919 ` 1287` ```apply (auto simp add: Ints_def) ``` haftmann@25919 ` 1288` ```apply (rule range_eqI) ``` haftmann@25919 ` 1289` ```apply (rule of_int_add [symmetric]) ``` haftmann@25919 ` 1290` ```done ``` haftmann@25919 ` 1291` haftmann@25919 ` 1292` ```lemma Ints_minus [simp]: "a \ \ \ -a \ \" ``` haftmann@25919 ` 1293` ```apply (auto simp add: Ints_def) ``` haftmann@25919 ` 1294` ```apply (rule range_eqI) ``` haftmann@25919 ` 1295` ```apply (rule of_int_minus [symmetric]) ``` haftmann@25919 ` 1296` ```done ``` haftmann@25919 ` 1297` huffman@35634 ` 1298` ```lemma Ints_diff [simp]: "a \ \ \ b \ \ \ a - b \ \" ``` huffman@35634 ` 1299` ```apply (auto simp add: Ints_def) ``` huffman@35634 ` 1300` ```apply (rule range_eqI) ``` huffman@35634 ` 1301` ```apply (rule of_int_diff [symmetric]) ``` huffman@35634 ` 1302` ```done ``` huffman@35634 ` 1303` haftmann@25919 ` 1304` ```lemma Ints_mult [simp]: "a \ \ \ b \ \ \ a * b \ \" ``` haftmann@25919 ` 1305` ```apply (auto simp add: Ints_def) ``` haftmann@25919 ` 1306` ```apply (rule range_eqI) ``` haftmann@25919 ` 1307` ```apply (rule of_int_mult [symmetric]) ``` haftmann@25919 ` 1308` ```done ``` haftmann@25919 ` 1309` huffman@35634 ` 1310` ```lemma Ints_power [simp]: "a \ \ \ a ^ n \ \" ``` huffman@35634 ` 1311` ```by (induct n) simp_all ``` huffman@35634 ` 1312` haftmann@25919 ` 1313` ```lemma Ints_cases [cases set: Ints]: ``` haftmann@25919 ` 1314` ``` assumes "q \ \" ``` haftmann@25919 ` 1315` ``` obtains (of_int) z where "q = of_int z" ``` haftmann@25919 ` 1316` ``` unfolding Ints_def ``` haftmann@25919 ` 1317` ```proof - ``` haftmann@25919 ` 1318` ``` from `q \ \` have "q \ range of_int" unfolding Ints_def . ``` haftmann@25919 ` 1319` ``` then obtain z where "q = of_int z" .. ``` haftmann@25919 ` 1320` ``` then show thesis .. ``` haftmann@25919 ` 1321` ```qed ``` haftmann@25919 ` 1322` haftmann@25919 ` 1323` ```lemma Ints_induct [case_names of_int, induct set: Ints]: ``` haftmann@25919 ` 1324` ``` "q \ \ \ (\z. P (of_int z)) \ P q" ``` haftmann@25919 ` 1325` ``` by (rule Ints_cases) auto ``` haftmann@25919 ` 1326` haftmann@25919 ` 1327` ```end ``` haftmann@25919 ` 1328` haftmann@25919 ` 1329` ```text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *} ``` haftmann@25919 ` 1330` haftmann@25919 ` 1331` ```lemma Ints_double_eq_0_iff: ``` haftmann@25919 ` 1332` ``` assumes in_Ints: "a \ Ints" ``` haftmann@25919 ` 1333` ``` shows "(a + a = 0) = (a = (0::'a::ring_char_0))" ``` haftmann@25919 ` 1334` ```proof - ``` haftmann@25919 ` 1335` ``` from in_Ints have "a \ range of_int" unfolding Ints_def [symmetric] . ``` haftmann@25919 ` 1336` ``` then obtain z where a: "a = of_int z" .. ``` haftmann@25919 ` 1337` ``` show ?thesis ``` haftmann@25919 ` 1338` ``` proof ``` haftmann@25919 ` 1339` ``` assume "a = 0" ``` haftmann@25919 ` 1340` ``` thus "a + a = 0" by simp ``` haftmann@25919 ` 1341` ``` next ``` haftmann@25919 ` 1342` ``` assume eq: "a + a = 0" ``` haftmann@25919 ` 1343` ``` hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a) ``` haftmann@25919 ` 1344` ``` hence "z + z = 0" by (simp only: of_int_eq_iff) ``` haftmann@25919 ` 1345` ``` hence "z = 0" by (simp only: double_eq_0_iff) ``` haftmann@25919 ` 1346` ``` thus "a = 0" by (simp add: a) ``` haftmann@25919 ` 1347` ``` qed ``` haftmann@25919 ` 1348` ```qed ``` haftmann@25919 ` 1349` haftmann@25919 ` 1350` ```lemma Ints_odd_nonzero: ``` haftmann@25919 ` 1351` ``` assumes in_Ints: "a \ Ints" ``` haftmann@25919 ` 1352` ``` shows "1 + a + a \ (0::'a::ring_char_0)" ``` haftmann@25919 ` 1353` ```proof - ``` haftmann@25919 ` 1354` ``` from in_Ints have "a \ range of_int" unfolding Ints_def [symmetric] . ``` haftmann@25919 ` 1355` ``` then obtain z where a: "a = of_int z" .. ``` haftmann@25919 ` 1356` ``` show ?thesis ``` haftmann@25919 ` 1357` ``` proof ``` haftmann@25919 ` 1358` ``` assume eq: "1 + a + a = 0" ``` haftmann@25919 ` 1359` ``` hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a) ``` haftmann@25919 ` 1360` ``` hence "1 + z + z = 0" by (simp only: of_int_eq_iff) ``` haftmann@25919 ` 1361` ``` with odd_nonzero show False by blast ``` haftmann@25919 ` 1362` ``` qed ``` haftmann@25919 ` 1363` ```qed ``` haftmann@25919 ` 1364` huffman@35634 ` 1365` ```lemma Ints_number_of [simp]: ``` haftmann@25919 ` 1366` ``` "(number_of w :: 'a::number_ring) \ Ints" ``` haftmann@25919 ` 1367` ``` unfolding number_of_eq Ints_def by simp ``` haftmann@25919 ` 1368` huffman@35634 ` 1369` ```lemma Nats_number_of [simp]: ``` huffman@35634 ` 1370` ``` "Int.Pls \ w \ (number_of w :: 'a::number_ring) \ Nats" ``` huffman@35634 ` 1371` ```unfolding Int.Pls_def number_of_eq ``` huffman@35634 ` 1372` ```by (simp only: of_nat_nat [symmetric] of_nat_in_Nats) ``` huffman@35634 ` 1373` haftmann@25919 ` 1374` ```lemma Ints_odd_less_0: ``` haftmann@25919 ` 1375` ``` assumes in_Ints: "a \ Ints" ``` haftmann@35028 ` 1376` ``` shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))" ``` haftmann@25919 ` 1377` ```proof - ``` haftmann@25919 ` 1378` ``` from in_Ints have "a \ range of_int" unfolding Ints_def [symmetric] . ``` haftmann@25919 ` 1379` ``` then obtain z where a: "a = of_int z" .. ``` haftmann@25919 ` 1380` ``` hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))" ``` haftmann@25919 ` 1381` ``` by (simp add: a) ``` haftmann@25919 ` 1382` ``` also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0) ``` haftmann@25919 ` 1383` ``` also have "... = (a < 0)" by (simp add: a) ``` haftmann@25919 ` 1384` ``` finally show ?thesis . ``` haftmann@25919 ` 1385` ```qed ``` haftmann@25919 ` 1386` haftmann@25919 ` 1387` haftmann@25919 ` 1388` ```subsection {* @{term setsum} and @{term setprod} *} ``` haftmann@25919 ` 1389` haftmann@25919 ` 1390` ```lemma of_nat_setsum: "of_nat (setsum f A) = (\x\A. of_nat(f x))" ``` haftmann@25919 ` 1391` ``` apply (cases "finite A") ``` haftmann@25919 ` 1392` ``` apply (erule finite_induct, auto) ``` haftmann@25919 ` 1393` ``` done ``` haftmann@25919 ` 1394` haftmann@25919 ` 1395` ```lemma of_int_setsum: "of_int (setsum f A) = (\x\A. of_int(f x))" ``` haftmann@25919 ` 1396` ``` apply (cases "finite A") ``` haftmann@25919 ` 1397` ``` apply (erule finite_induct, auto) ``` haftmann@25919 ` 1398` ``` done ``` haftmann@25919 ` 1399` haftmann@25919 ` 1400` ```lemma of_nat_setprod: "of_nat (setprod f A) = (\x\A. of_nat(f x))" ``` haftmann@25919 ` 1401` ``` apply (cases "finite A") ``` haftmann@25919 ` 1402` ``` apply (erule finite_induct, auto simp add: of_nat_mult) ``` haftmann@25919 ` 1403` ``` done ``` haftmann@25919 ` 1404` haftmann@25919 ` 1405` ```lemma of_int_setprod: "of_int (setprod f A) = (\x\A. of_int(f x))" ``` haftmann@25919 ` 1406` ``` apply (cases "finite A") ``` haftmann@25919 ` 1407` ``` apply (erule finite_induct, auto) ``` haftmann@25919 ` 1408` ``` done ``` haftmann@25919 ` 1409` haftmann@25919 ` 1410` ```lemmas int_setsum = of_nat_setsum [where 'a=int] ``` haftmann@25919 ` 1411` ```lemmas int_setprod = of_nat_setprod [where 'a=int] ``` haftmann@25919 ` 1412` haftmann@25919 ` 1413` haftmann@25919 ` 1414` ```subsection{*Inequality Reasoning for the Arithmetic Simproc*} ``` haftmann@25919 ` 1415` haftmann@25919 ` 1416` ```lemma add_numeral_0: "Numeral0 + a = (a::'a::number_ring)" ``` haftmann@25919 ` 1417` ```by simp ``` haftmann@25919 ` 1418` haftmann@25919 ` 1419` ```lemma add_numeral_0_right: "a + Numeral0 = (a::'a::number_ring)" ``` haftmann@25919 ` 1420` ```by simp ``` haftmann@25919 ` 1421` haftmann@25919 ` 1422` ```lemma mult_numeral_1: "Numeral1 * a = (a::'a::number_ring)" ``` haftmann@25919 ` 1423` ```by simp ``` haftmann@25919 ` 1424` haftmann@25919 ` 1425` ```lemma mult_numeral_1_right: "a * Numeral1 = (a::'a::number_ring)" ``` haftmann@25919 ` 1426` ```by simp ``` haftmann@25919 ` 1427` haftmann@25919 ` 1428` ```lemma divide_numeral_1: "a / Numeral1 = (a::'a::{number_ring,field})" ``` haftmann@25919 ` 1429` ```by simp ``` haftmann@25919 ` 1430` haftmann@25919 ` 1431` ```lemma inverse_numeral_1: ``` haftmann@25919 ` 1432` ``` "inverse Numeral1 = (Numeral1::'a::{number_ring,field})" ``` haftmann@25919 ` 1433` ```by simp ``` haftmann@25919 ` 1434` haftmann@25919 ` 1435` ```text{*Theorem lists for the cancellation simprocs. The use of binary numerals ``` haftmann@25919 ` 1436` ```for 0 and 1 reduces the number of special cases.*} ``` haftmann@25919 ` 1437` haftmann@25919 ` 1438` ```lemmas add_0s = add_numeral_0 add_numeral_0_right ``` haftmann@25919 ` 1439` ```lemmas mult_1s = mult_numeral_1 mult_numeral_1_right ``` haftmann@25919 ` 1440` ``` mult_minus1 mult_minus1_right ``` haftmann@25919 ` 1441` haftmann@25919 ` 1442` haftmann@25919 ` 1443` ```subsection{*Special Arithmetic Rules for Abstract 0 and 1*} ``` haftmann@25919 ` 1444` haftmann@25919 ` 1445` ```text{*Arithmetic computations are defined for binary literals, which leaves 0 ``` haftmann@25919 ` 1446` ```and 1 as special cases. Addition already has rules for 0, but not 1. ``` haftmann@25919 ` 1447` ```Multiplication and unary minus already have rules for both 0 and 1.*} ``` haftmann@25919 ` 1448` haftmann@25919 ` 1449` haftmann@25919 ` 1450` ```lemma binop_eq: "[|f x y = g x y; x = x'; y = y'|] ==> f x' y' = g x' y'" ``` haftmann@25919 ` 1451` ```by simp ``` haftmann@25919 ` 1452` haftmann@25919 ` 1453` haftmann@25919 ` 1454` ```lemmas add_number_of_eq = number_of_add [symmetric] ``` haftmann@25919 ` 1455` haftmann@25919 ` 1456` ```text{*Allow 1 on either or both sides*} ``` haftmann@25919 ` 1457` ```lemma one_add_one_is_two: "1 + 1 = (2::'a::number_ring)" ``` huffman@35216 ` 1458` ```by (simp del: numeral_1_eq_1 add: numeral_1_eq_1 [symmetric]) ``` haftmann@25919 ` 1459` haftmann@25919 ` 1460` ```lemmas add_special = ``` haftmann@25919 ` 1461` ``` one_add_one_is_two ``` haftmann@25919 ` 1462` ``` binop_eq [of "op +", OF add_number_of_eq numeral_1_eq_1 refl, standard] ``` haftmann@25919 ` 1463` ``` binop_eq [of "op +", OF add_number_of_eq refl numeral_1_eq_1, standard] ``` haftmann@25919 ` 1464` haftmann@25919 ` 1465` ```text{*Allow 1 on either or both sides (1-1 already simplifies to 0)*} ``` haftmann@25919 ` 1466` ```lemmas diff_special = ``` haftmann@25919 ` 1467` ``` binop_eq [of "op -", OF diff_number_of_eq numeral_1_eq_1 refl, standard] ``` haftmann@25919 ` 1468` ``` binop_eq [of "op -", OF diff_number_of_eq refl numeral_1_eq_1, standard] ``` haftmann@25919 ` 1469` haftmann@25919 ` 1470` ```text{*Allow 0 or 1 on either side with a binary numeral on the other*} ``` haftmann@25919 ` 1471` ```lemmas eq_special = ``` haftmann@25919 ` 1472` ``` binop_eq [of "op =", OF eq_number_of_eq numeral_0_eq_0 refl, standard] ``` haftmann@25919 ` 1473` ``` binop_eq [of "op =", OF eq_number_of_eq numeral_1_eq_1 refl, standard] ``` haftmann@25919 ` 1474` ``` binop_eq [of "op =", OF eq_number_of_eq refl numeral_0_eq_0, standard] ``` haftmann@25919 ` 1475` ``` binop_eq [of "op =", OF eq_number_of_eq refl numeral_1_eq_1, standard] ``` haftmann@25919 ` 1476` haftmann@25919 ` 1477` ```text{*Allow 0 or 1 on either side with a binary numeral on the other*} ``` haftmann@25919 ` 1478` ```lemmas less_special = ``` huffman@28984 ` 1479` ``` binop_eq [of "op <", OF less_number_of numeral_0_eq_0 refl, standard] ``` huffman@28984 ` 1480` ``` binop_eq [of "op <", OF less_number_of numeral_1_eq_1 refl, standard] ``` huffman@28984 ` 1481` ``` binop_eq [of "op <", OF less_number_of refl numeral_0_eq_0, standard] ``` huffman@28984 ` 1482` ``` binop_eq [of "op <", OF less_number_of refl numeral_1_eq_1, standard] ``` haftmann@25919 ` 1483` haftmann@25919 ` 1484` ```text{*Allow 0 or 1 on either side with a binary numeral on the other*} ``` haftmann@25919 ` 1485` ```lemmas le_special = ``` huffman@28984 ` 1486` ``` binop_eq [of "op \", OF le_number_of numeral_0_eq_0 refl, standard] ``` huffman@28984 ` 1487` ``` binop_eq [of "op \", OF le_number_of numeral_1_eq_1 refl, standard] ``` huffman@28984 ` 1488` ``` binop_eq [of "op \", OF le_number_of refl numeral_0_eq_0, standard] ``` huffman@28984 ` 1489` ``` binop_eq [of "op \", OF le_number_of refl numeral_1_eq_1, standard] ``` haftmann@25919 ` 1490` haftmann@25919 ` 1491` ```lemmas arith_special[simp] = ``` haftmann@25919 ` 1492` ``` add_special diff_special eq_special less_special le_special ``` haftmann@25919 ` 1493` haftmann@25919 ` 1494` haftmann@25919 ` 1495` ```text {* Legacy theorems *} ``` haftmann@25919 ` 1496` haftmann@25919 ` 1497` ```lemmas zle_int = of_nat_le_iff [where 'a=int] ``` haftmann@25919 ` 1498` ```lemmas int_int_eq = of_nat_eq_iff [where 'a=int] ``` haftmann@25919 ` 1499` huffman@30802 ` 1500` ```subsection {* Setting up simplification procedures *} ``` huffman@30802 ` 1501` huffman@30802 ` 1502` ```lemmas int_arith_rules = ``` huffman@30802 ` 1503` ``` neg_le_iff_le numeral_0_eq_0 numeral_1_eq_1 ``` huffman@30802 ` 1504` ``` minus_zero diff_minus left_minus right_minus ``` huffman@30802 ` 1505` ``` mult_zero_left mult_zero_right mult_Bit1 mult_1_right ``` huffman@30802 ` 1506` ``` mult_minus_left mult_minus_right ``` huffman@30802 ` 1507` ``` minus_add_distrib minus_minus mult_assoc ``` huffman@30802 ` 1508` ``` of_nat_0 of_nat_1 of_nat_Suc of_nat_add of_nat_mult ``` huffman@30802 ` 1509` ``` of_int_0 of_int_1 of_int_add of_int_mult ``` huffman@30802 ` 1510` haftmann@28952 ` 1511` ```use "Tools/int_arith.ML" ``` haftmann@31100 ` 1512` ```setup {* Int_Arith.global_setup *} ``` haftmann@30496 ` 1513` ```declaration {* K Int_Arith.setup *} ``` haftmann@25919 ` 1514` huffman@31024 ` 1515` ```setup {* ``` wenzelm@33523 ` 1516` ``` Reorient_Proc.add ``` haftmann@31065 ` 1517` ``` (fn Const (@{const_name number_of}, _) \$ _ => true | _ => false) ``` huffman@31024 ` 1518` ```*} ``` huffman@31024 ` 1519` wenzelm@33523 ` 1520` ```simproc_setup reorient_numeral ("number_of w = x") = Reorient_Proc.proc ``` huffman@31024 ` 1521` haftmann@25919 ` 1522` haftmann@25919 ` 1523` ```subsection{*Lemmas About Small Numerals*} ``` haftmann@25919 ` 1524` haftmann@25919 ` 1525` ```lemma of_int_m1 [simp]: "of_int -1 = (-1 :: 'a :: number_ring)" ``` haftmann@25919 ` 1526` ```proof - ``` haftmann@25919 ` 1527` ``` have "(of_int -1 :: 'a) = of_int (- 1)" by simp ``` haftmann@25919 ` 1528` ``` also have "... = - of_int 1" by (simp only: of_int_minus) ``` haftmann@25919 ` 1529` ``` also have "... = -1" by simp ``` haftmann@25919 ` 1530` ``` finally show ?thesis . ``` haftmann@25919 ` 1531` ```qed ``` haftmann@25919 ` 1532` haftmann@35028 ` 1533` ```lemma abs_minus_one [simp]: "abs (-1) = (1::'a::{linordered_idom,number_ring})" ``` haftmann@25919 ` 1534` ```by (simp add: abs_if) ``` haftmann@25919 ` 1535` haftmann@25919 ` 1536` ```lemma abs_power_minus_one [simp]: ``` haftmann@35028 ` 1537` ``` "abs(-1 ^ n) = (1::'a::{linordered_idom,number_ring})" ``` haftmann@25919 ` 1538` ```by (simp add: power_abs) ``` haftmann@25919 ` 1539` huffman@30000 ` 1540` ```lemma of_int_number_of_eq [simp]: ``` haftmann@25919 ` 1541` ``` "of_int (number_of v) = (number_of v :: 'a :: number_ring)" ``` haftmann@25919 ` 1542` ```by (simp add: number_of_eq) ``` haftmann@25919 ` 1543` haftmann@25919 ` 1544` ```text{*Lemmas for specialist use, NOT as default simprules*} ``` haftmann@25919 ` 1545` ```lemma mult_2: "2 * z = (z+z::'a::number_ring)" ``` haftmann@33296 ` 1546` ```unfolding one_add_one_is_two [symmetric] left_distrib by simp ``` haftmann@25919 ` 1547` haftmann@25919 ` 1548` ```lemma mult_2_right: "z * 2 = (z+z::'a::number_ring)" ``` haftmann@25919 ` 1549` ```by (subst mult_commute, rule mult_2) ``` haftmann@25919 ` 1550` haftmann@25919 ` 1551` haftmann@25919 ` 1552` ```subsection{*More Inequality Reasoning*} ``` haftmann@25919 ` 1553` haftmann@25919 ` 1554` ```lemma zless_add1_eq: "(w < z + (1::int)) = (w z) = (w z - (1::int)) = (wz)" ``` haftmann@25919 ` 1564` ```by arith ``` haftmann@25919 ` 1565` haftmann@25919 ` 1566` ```lemma int_one_le_iff_zero_less: "((1::int) \ z) = (0 < z)" ``` haftmann@25919 ` 1567` ```by arith ``` haftmann@25919 ` 1568` haftmann@25919 ` 1569` huffman@28958 ` 1570` ```subsection{*The functions @{term nat} and @{term int}*} ``` haftmann@25919 ` 1571` haftmann@25919 ` 1572` ```text{*Simplify the terms @{term "int 0"}, @{term "int(Suc 0)"} and ``` haftmann@25919 ` 1573` ``` @{term "w + - z"}*} ``` haftmann@25919 ` 1574` ```declare Zero_int_def [symmetric, simp] ``` haftmann@25919 ` 1575` ```declare One_int_def [symmetric, simp] ``` haftmann@25919 ` 1576` haftmann@25919 ` 1577` ```lemmas diff_int_def_symmetric = diff_int_def [symmetric, simp] ``` haftmann@25919 ` 1578` huffman@35216 ` 1579` ```(* FIXME: duplicates nat_zero *) ``` haftmann@25919 ` 1580` ```lemma nat_0: "nat 0 = 0" ``` haftmann@25919 ` 1581` ```by (simp add: nat_eq_iff) ``` haftmann@25919 ` 1582` haftmann@25919 ` 1583` ```lemma nat_1: "nat 1 = Suc 0" ``` haftmann@25919 ` 1584` ```by (subst nat_eq_iff, simp) ``` haftmann@25919 ` 1585` haftmann@25919 ` 1586` ```lemma nat_2: "nat 2 = Suc (Suc 0)" ``` haftmann@25919 ` 1587` ```by (subst nat_eq_iff, simp) ``` haftmann@25919 ` 1588` haftmann@25919 ` 1589` ```lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)" ``` haftmann@25919 ` 1590` ```apply (insert zless_nat_conj [of 1 z]) ``` haftmann@25919 ` 1591` ```apply (auto simp add: nat_1) ``` haftmann@25919 ` 1592` ```done ``` haftmann@25919 ` 1593` haftmann@25919 ` 1594` ```text{*This simplifies expressions of the form @{term "int n = z"} where ``` haftmann@25919 ` 1595` ``` z is an integer literal.*} ``` haftmann@25919 ` 1596` ```lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v", standard] ``` haftmann@25919 ` 1597` haftmann@25919 ` 1598` ```lemma split_nat [arith_split]: ``` haftmann@25919 ` 1599` ``` "P(nat(i::int)) = ((\n. i = of_nat n \ P n) & (i < 0 \ P 0))" ``` haftmann@25919 ` 1600` ``` (is "?P = (?L & ?R)") ``` haftmann@25919 ` 1601` ```proof (cases "i < 0") ``` haftmann@25919 ` 1602` ``` case True thus ?thesis by auto ``` haftmann@25919 ` 1603` ```next ``` haftmann@25919 ` 1604` ``` case False ``` haftmann@25919 ` 1605` ``` have "?P = ?L" ``` haftmann@25919 ` 1606` ``` proof ``` haftmann@25919 ` 1607` ``` assume ?P thus ?L using False by clarsimp ``` haftmann@25919 ` 1608` ``` next ``` haftmann@25919 ` 1609` ``` assume ?L thus ?P using False by simp ``` haftmann@25919 ` 1610` ``` qed ``` haftmann@25919 ` 1611` ``` with False show ?thesis by simp ``` haftmann@25919 ` 1612` ```qed ``` haftmann@25919 ` 1613` haftmann@25919 ` 1614` ```context ring_1 ``` haftmann@25919 ` 1615` ```begin ``` haftmann@25919 ` 1616` blanchet@33056 ` 1617` ```lemma of_int_of_nat [nitpick_simp]: ``` haftmann@25919 ` 1618` ``` "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))" ``` haftmann@25919 ` 1619` ```proof (cases "k < 0") ``` haftmann@25919 ` 1620` ``` case True then have "0 \ - k" by simp ``` haftmann@25919 ` 1621` ``` then have "of_nat (nat (- k)) = of_int (- k)" by (rule of_nat_nat) ``` haftmann@25919 ` 1622` ``` with True show ?thesis by simp ``` haftmann@25919 ` 1623` ```next ``` haftmann@25919 ` 1624` ``` case False then show ?thesis by (simp add: not_less of_nat_nat) ``` haftmann@25919 ` 1625` ```qed ``` haftmann@25919 ` 1626` haftmann@25919 ` 1627` ```end ``` haftmann@25919 ` 1628` haftmann@25919 ` 1629` ```lemma nat_mult_distrib: ``` haftmann@25919 ` 1630` ``` fixes z z' :: int ``` haftmann@25919 ` 1631` ``` assumes "0 \ z" ``` haftmann@25919 ` 1632` ``` shows "nat (z * z') = nat z * nat z'" ``` haftmann@25919 ` 1633` ```proof (cases "0 \ z'") ``` haftmann@25919 ` 1634` ``` case False with assms have "z * z' \ 0" ``` haftmann@25919 ` 1635` ``` by (simp add: not_le mult_le_0_iff) ``` haftmann@25919 ` 1636` ``` then have "nat (z * z') = 0" by simp ``` haftmann@25919 ` 1637` ``` moreover from False have "nat z' = 0" by simp ``` haftmann@25919 ` 1638` ``` ultimately show ?thesis by simp ``` haftmann@25919 ` 1639` ```next ``` haftmann@25919 ` 1640` ``` case True with assms have ge_0: "z * z' \ 0" by (simp add: zero_le_mult_iff) ``` haftmann@25919 ` 1641` ``` show ?thesis ``` haftmann@25919 ` 1642` ``` by (rule injD [of "of_nat :: nat \ int", OF inj_of_nat]) ``` haftmann@25919 ` 1643` ``` (simp only: of_nat_mult of_nat_nat [OF True] ``` haftmann@25919 ` 1644` ``` of_nat_nat [OF assms] of_nat_nat [OF ge_0], simp) ``` haftmann@25919 ` 1645` ```qed ``` haftmann@25919 ` 1646` haftmann@25919 ` 1647` ```lemma nat_mult_distrib_neg: "z \ (0::int) ==> nat(z*z') = nat(-z) * nat(-z')" ``` haftmann@25919 ` 1648` ```apply (rule trans) ``` haftmann@25919 ` 1649` ```apply (rule_tac [2] nat_mult_distrib, auto) ``` haftmann@25919 ` 1650` ```done ``` haftmann@25919 ` 1651` haftmann@25919 ` 1652` ```lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)" ``` haftmann@25919 ` 1653` ```apply (cases "z=0 | w=0") ``` haftmann@25919 ` 1654` ```apply (auto simp add: abs_if nat_mult_distrib [symmetric] ``` haftmann@25919 ` 1655` ``` nat_mult_distrib_neg [symmetric] mult_less_0_iff) ``` haftmann@25919 ` 1656` ```done ``` haftmann@25919 ` 1657` haftmann@25919 ` 1658` haftmann@25919 ` 1659` ```subsection "Induction principles for int" ``` haftmann@25919 ` 1660` haftmann@25919 ` 1661` ```text{*Well-founded segments of the integers*} ``` haftmann@25919 ` 1662` haftmann@25919 ` 1663` ```definition ``` haftmann@25919 ` 1664` ``` int_ge_less_than :: "int => (int * int) set" ``` haftmann@25919 ` 1665` ```where ``` haftmann@25919 ` 1666` ``` "int_ge_less_than d = {(z',z). d \ z' & z' < z}" ``` haftmann@25919 ` 1667` haftmann@25919 ` 1668` ```theorem wf_int_ge_less_than: "wf (int_ge_less_than d)" ``` haftmann@25919 ` 1669` ```proof - ``` haftmann@25919 ` 1670` ``` have "int_ge_less_than d \ measure (%z. nat (z-d))" ``` haftmann@25919 ` 1671` ``` by (auto simp add: int_ge_less_than_def) ``` haftmann@25919 ` 1672` ``` thus ?thesis ``` haftmann@25919 ` 1673` ``` by (rule wf_subset [OF wf_measure]) ``` haftmann@25919 ` 1674` ```qed ``` haftmann@25919 ` 1675` haftmann@25919 ` 1676` ```text{*This variant looks odd, but is typical of the relations suggested ``` haftmann@25919 ` 1677` ```by RankFinder.*} ``` haftmann@25919 ` 1678` haftmann@25919 ` 1679` ```definition ``` haftmann@25919 ` 1680` ``` int_ge_less_than2 :: "int => (int * int) set" ``` haftmann@25919 ` 1681` ```where ``` haftmann@25919 ` 1682` ``` "int_ge_less_than2 d = {(z',z). d \ z & z' < z}" ``` haftmann@25919 ` 1683` haftmann@25919 ` 1684` ```theorem wf_int_ge_less_than2: "wf (int_ge_less_than2 d)" ``` haftmann@25919 ` 1685` ```proof - ``` haftmann@25919 ` 1686` ``` have "int_ge_less_than2 d \ measure (%z. nat (1+z-d))" ``` haftmann@25919 ` 1687` ``` by (auto simp add: int_ge_less_than2_def) ``` haftmann@25919 ` 1688` ``` thus ?thesis ``` haftmann@25919 ` 1689` ``` by (rule wf_subset [OF wf_measure]) ``` haftmann@25919 ` 1690` ```qed ``` haftmann@25919 ` 1691` haftmann@25919 ` 1692` ```abbreviation ``` haftmann@25919 ` 1693` ``` int :: "nat \ int" ``` haftmann@25919 ` 1694` ```where ``` haftmann@25919 ` 1695` ``` "int \ of_nat" ``` haftmann@25919 ` 1696` haftmann@25919 ` 1697` ```(* `set:int': dummy construction *) ``` haftmann@25919 ` 1698` ```theorem int_ge_induct [case_names base step, induct set: int]: ``` haftmann@25919 ` 1699` ``` fixes i :: int ``` haftmann@25919 ` 1700` ``` assumes ge: "k \ i" and ``` haftmann@25919 ` 1701` ``` base: "P k" and ``` haftmann@25919 ` 1702` ``` step: "\i. k \ i \ P i \ P (i + 1)" ``` haftmann@25919 ` 1703` ``` shows "P i" ``` haftmann@25919 ` 1704` ```proof - ``` haftmann@25919 ` 1705` ``` { fix n have "\i::int. n = nat(i-k) \ k \ i \ P i" ``` haftmann@25919 ` 1706` ``` proof (induct n) ``` haftmann@25919 ` 1707` ``` case 0 ``` haftmann@25919 ` 1708` ``` hence "i = k" by arith ``` haftmann@25919 ` 1709` ``` thus "P i" using base by simp ``` haftmann@25919 ` 1710` ``` next ``` haftmann@25919 ` 1711` ``` case (Suc n) ``` haftmann@25919 ` 1712` ``` then have "n = nat((i - 1) - k)" by arith ``` haftmann@25919 ` 1713` ``` moreover ``` haftmann@25919 ` 1714` ``` have ki1: "k \ i - 1" using Suc.prems by arith ``` haftmann@25919 ` 1715` ``` ultimately ``` haftmann@25919 ` 1716` ``` have "P(i - 1)" by(rule Suc.hyps) ``` haftmann@25919 ` 1717` ``` from step[OF ki1 this] show ?case by simp ``` haftmann@25919 ` 1718` ``` qed ``` haftmann@25919 ` 1719` ``` } ``` haftmann@25919 ` 1720` ``` with ge show ?thesis by fast ``` haftmann@25919 ` 1721` ```qed ``` haftmann@25919 ` 1722` haftmann@25928 ` 1723` ```(* `set:int': dummy construction *) ``` haftmann@25928 ` 1724` ```theorem int_gr_induct [case_names base step, induct set: int]: ``` haftmann@25919 ` 1725` ``` assumes gr: "k < (i::int)" and ``` haftmann@25919 ` 1726` ``` base: "P(k+1)" and ``` haftmann@25919 ` 1727` ``` step: "\i. \k < i; P i\ \ P(i+1)" ``` haftmann@25919 ` 1728` ``` shows "P i" ``` haftmann@25919 ` 1729` ```apply(rule int_ge_induct[of "k + 1"]) ``` haftmann@25919 ` 1730` ``` using gr apply arith ``` haftmann@25919 ` 1731` ``` apply(rule base) ``` haftmann@25919 ` 1732` ```apply (rule step, simp+) ``` haftmann@25919 ` 1733` ```done ``` haftmann@25919 ` 1734` haftmann@25919 ` 1735` ```theorem int_le_induct[consumes 1,case_names base step]: ``` haftmann@25919 ` 1736` ``` assumes le: "i \ (k::int)" and ``` haftmann@25919 ` 1737` ``` base: "P(k)" and ``` haftmann@25919 ` 1738` ``` step: "\i. \i \ k; P i\ \ P(i - 1)" ``` haftmann@25919 ` 1739` ``` shows "P i" ``` haftmann@25919 ` 1740` ```proof - ``` haftmann@25919 ` 1741` ``` { fix n have "\i::int. n = nat(k-i) \ i \ k \ P i" ``` haftmann@25919 ` 1742` ``` proof (induct n) ``` haftmann@25919 ` 1743` ``` case 0 ``` haftmann@25919 ` 1744` ``` hence "i = k" by arith ``` haftmann@25919 ` 1745` ``` thus "P i" using base by simp ``` haftmann@25919 ` 1746` ``` next ``` haftmann@25919 ` 1747` ``` case (Suc n) ``` haftmann@25919 ` 1748` ``` hence "n = nat(k - (i+1))" by arith ``` haftmann@25919 ` 1749` ``` moreover ``` haftmann@25919 ` 1750` ``` have ki1: "i + 1 \ k" using Suc.prems by arith ``` haftmann@25919 ` 1751` ``` ultimately ``` haftmann@25919 ` 1752` ``` have "P(i+1)" by(rule Suc.hyps) ``` haftmann@25919 ` 1753` ``` from step[OF ki1 this] show ?case by simp ``` haftmann@25919 ` 1754` ``` qed ``` haftmann@25919 ` 1755` ``` } ``` haftmann@25919 ` 1756` ``` with le show ?thesis by fast ``` haftmann@25919 ` 1757` ```qed ``` haftmann@25919 ` 1758` haftmann@25919 ` 1759` ```theorem int_less_induct [consumes 1,case_names base step]: ``` haftmann@25919 ` 1760` ``` assumes less: "(i::int) < k" and ``` haftmann@25919 ` 1761` ``` base: "P(k - 1)" and ``` haftmann@25919 ` 1762` ``` step: "\i. \i < k; P i\ \ P(i - 1)" ``` haftmann@25919 ` 1763` ``` shows "P i" ``` haftmann@25919 ` 1764` ```apply(rule int_le_induct[of _ "k - 1"]) ``` haftmann@25919 ` 1765` ``` using less apply arith ``` haftmann@25919 ` 1766` ``` apply(rule base) ``` haftmann@25919 ` 1767` ```apply (rule step, simp+) ``` haftmann@25919 ` 1768` ```done ``` haftmann@25919 ` 1769` haftmann@25919 ` 1770` ```subsection{*Intermediate value theorems*} ``` haftmann@25919 ` 1771` haftmann@25919 ` 1772` ```lemma int_val_lemma: ``` haftmann@25919 ` 1773` ``` "(\i 1) --> ``` haftmann@25919 ` 1774` ``` f 0 \ k --> k \ f n --> (\i \ n. f i = (k::int))" ``` huffman@30079 ` 1775` ```unfolding One_nat_def ``` haftmann@27106 ` 1776` ```apply (induct n, simp) ``` haftmann@25919 ` 1777` ```apply (intro strip) ``` haftmann@25919 ` 1778` ```apply (erule impE, simp) ``` haftmann@25919 ` 1779` ```apply (erule_tac x = n in allE, simp) ``` huffman@30079 ` 1780` ```apply (case_tac "k = f (Suc n)") ``` haftmann@27106 ` 1781` ```apply force ``` haftmann@25919 ` 1782` ```apply (erule impE) ``` haftmann@25919 ` 1783` ``` apply (simp add: abs_if split add: split_if_asm) ``` haftmann@25919 ` 1784` ```apply (blast intro: le_SucI) ``` haftmann@25919 ` 1785` ```done ``` haftmann@25919 ` 1786` haftmann@25919 ` 1787` ```lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)] ``` haftmann@25919 ` 1788` haftmann@25919 ` 1789` ```lemma nat_intermed_int_val: ``` haftmann@25919 ` 1790` ``` "[| \i. m \ i & i < n --> abs(f(i + 1::nat) - f i) \ 1; m < n; ``` haftmann@25919 ` 1791` ``` f m \ k; k \ f n |] ==> ? i. m \ i & i \ n & f i = (k::int)" ``` haftmann@25919 ` 1792` ```apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k ``` haftmann@25919 ` 1793` ``` in int_val_lemma) ``` huffman@30079 ` 1794` ```unfolding One_nat_def ``` haftmann@25919 ` 1795` ```apply simp ``` haftmann@25919 ` 1796` ```apply (erule exE) ``` haftmann@25919 ` 1797` ```apply (rule_tac x = "i+m" in exI, arith) ``` haftmann@25919 ` 1798` ```done ``` haftmann@25919 ` 1799` haftmann@25919 ` 1800` haftmann@25919 ` 1801` ```subsection{*Products and 1, by T. M. Rasmussen*} ``` haftmann@25919 ` 1802` haftmann@25919 ` 1803` ```lemma zabs_less_one_iff [simp]: "(\z\ < 1) = (z = (0::int))" ``` haftmann@25919 ` 1804` ```by arith ``` haftmann@25919 ` 1805` paulson@34055 ` 1806` ```lemma abs_zmult_eq_1: ``` paulson@34055 ` 1807` ``` assumes mn: "\m * n\ = 1" ``` paulson@34055 ` 1808` ``` shows "\m\ = (1::int)" ``` paulson@34055 ` 1809` ```proof - ``` paulson@34055 ` 1810` ``` have 0: "m \ 0 & n \ 0" using mn ``` paulson@34055 ` 1811` ``` by auto ``` paulson@34055 ` 1812` ``` have "~ (2 \ \m\)" ``` paulson@34055 ` 1813` ``` proof ``` paulson@34055 ` 1814` ``` assume "2 \ \m\" ``` paulson@34055 ` 1815` ``` hence "2*\n\ \ \m\*\n\" ``` paulson@34055 ` 1816` ``` by (simp add: mult_mono 0) ``` paulson@34055 ` 1817` ``` also have "... = \m*n\" ``` paulson@34055 ` 1818` ``` by (simp add: abs_mult) ``` paulson@34055 ` 1819` ``` also have "... = 1" ``` paulson@34055 ` 1820` ``` by (simp add: mn) ``` paulson@34055 ` 1821` ``` finally have "2*\n\ \ 1" . ``` paulson@34055 ` 1822` ``` thus "False" using 0 ``` paulson@34055 ` 1823` ``` by auto ``` paulson@34055 ` 1824` ``` qed ``` paulson@34055 ` 1825` ``` thus ?thesis using 0 ``` paulson@34055 ` 1826` ``` by auto ``` paulson@34055 ` 1827` ```qed ``` haftmann@25919 ` 1828` haftmann@25919 ` 1829` ```lemma pos_zmult_eq_1_iff_lemma: "(m * n = 1) ==> m = (1::int) | m = -1" ``` haftmann@25919 ` 1830` ```by (insert abs_zmult_eq_1 [of m n], arith) ``` haftmann@25919 ` 1831` boehmes@35815 ` 1832` ```lemma pos_zmult_eq_1_iff: ``` boehmes@35815 ` 1833` ``` assumes "0 < (m::int)" shows "(m * n = 1) = (m = 1 & n = 1)" ``` boehmes@35815 ` 1834` ```proof - ``` boehmes@35815 ` 1835` ``` from assms have "m * n = 1 ==> m = 1" by (auto dest: pos_zmult_eq_1_iff_lemma) ``` boehmes@35815 ` 1836` ``` thus ?thesis by (auto dest: pos_zmult_eq_1_iff_lemma) ``` boehmes@35815 ` 1837` ```qed ``` haftmann@25919 ` 1838` haftmann@25919 ` 1839` ```lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))" ``` haftmann@25919 ` 1840` ```apply (rule iffI) ``` haftmann@25919 ` 1841` ``` apply (frule pos_zmult_eq_1_iff_lemma) ``` haftmann@25919 ` 1842` ``` apply (simp add: mult_commute [of m]) ``` haftmann@25919 ` 1843` ``` apply (frule pos_zmult_eq_1_iff_lemma, auto) ``` haftmann@25919 ` 1844` ```done ``` haftmann@25919 ` 1845` haftmann@33296 ` 1846` ```lemma infinite_UNIV_int: "\ finite (UNIV::int set)" ``` haftmann@25919 ` 1847` ```proof ``` haftmann@33296 ` 1848` ``` assume "finite (UNIV::int set)" ``` haftmann@33296 ` 1849` ``` moreover have "inj (\i\int. 2 * i)" ``` haftmann@33296 ` 1850` ``` by (rule injI) simp ``` haftmann@33296 ` 1851` ``` ultimately have "surj (\i\int. 2 * i)" ``` haftmann@33296 ` 1852` ``` by (rule finite_UNIV_inj_surj) ``` haftmann@33296 ` 1853` ``` then obtain i :: int where "1 = 2 * i" by (rule surjE) ``` haftmann@33296 ` 1854` ``` then show False by (simp add: pos_zmult_eq_1_iff) ``` haftmann@25919 ` 1855` ```qed ``` haftmann@25919 ` 1856` haftmann@25919 ` 1857` haftmann@30652 ` 1858` ```subsection {* Further theorems on numerals *} ``` haftmann@30652 ` 1859` haftmann@30652 ` 1860` ```subsubsection{*Special Simplification for Constants*} ``` haftmann@30652 ` 1861` haftmann@30652 ` 1862` ```text{*These distributive laws move literals inside sums and differences.*} ``` haftmann@30652 ` 1863` haftmann@30652 ` 1864` ```lemmas left_distrib_number_of [simp] = ``` haftmann@30652 ` 1865` ``` left_distrib [of _ _ "number_of v", standard] ``` haftmann@30652 ` 1866` haftmann@30652 ` 1867` ```lemmas right_distrib_number_of [simp] = ``` haftmann@30652 ` 1868` ``` right_distrib [of "number_of v", standard] ``` haftmann@30652 ` 1869` haftmann@30652 ` 1870` ```lemmas left_diff_distrib_number_of [simp] = ``` haftmann@30652 ` 1871` ``` left_diff_distrib [of _ _ "number_of v", standard] ``` haftmann@30652 ` 1872` haftmann@30652 ` 1873` ```lemmas right_diff_distrib_number_of [simp] = ``` haftmann@30652 ` 1874` ``` right_diff_distrib [of "number_of v", standard] ``` haftmann@30652 ` 1875` haftmann@30652 ` 1876` ```text{*These are actually for fields, like real: but where else to put them?*} ``` haftmann@30652 ` 1877` blanchet@35828 ` 1878` ```lemmas zero_less_divide_iff_number_of [simp, no_atp] = ``` haftmann@30652 ` 1879` ``` zero_less_divide_iff [of "number_of w", standard] ``` haftmann@30652 ` 1880` blanchet@35828 ` 1881` ```lemmas divide_less_0_iff_number_of [simp, no_atp] = ``` haftmann@30652 ` 1882` ``` divide_less_0_iff [of "number_of w", standard] ``` haftmann@30652 ` 1883` blanchet@35828 ` 1884` ```lemmas zero_le_divide_iff_number_of [simp, no_atp] = ``` haftmann@30652 ` 1885` ``` zero_le_divide_iff [of "number_of w", standard] ``` haftmann@30652 ` 1886` blanchet@35828 ` 1887` ```lemmas divide_le_0_iff_number_of [simp, no_atp] = ``` haftmann@30652 ` 1888` ``` divide_le_0_iff [of "number_of w", standard] ``` haftmann@30652 ` 1889` haftmann@30652 ` 1890` haftmann@30652 ` 1891` ```text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}. It looks ``` haftmann@30652 ` 1892` ``` strange, but then other simprocs simplify the quotient.*} ``` haftmann@30652 ` 1893` haftmann@30652 ` 1894` ```lemmas inverse_eq_divide_number_of [simp] = ``` haftmann@30652 ` 1895` ``` inverse_eq_divide [of "number_of w", standard] ``` haftmann@30652 ` 1896` haftmann@30652 ` 1897` ```text {*These laws simplify inequalities, moving unary minus from a term ``` haftmann@30652 ` 1898` ```into the literal.*} ``` haftmann@30652 ` 1899` blanchet@35828 ` 1900` ```lemmas less_minus_iff_number_of [simp, no_atp] = ``` haftmann@30652 ` 1901` ``` less_minus_iff [of "number_of v", standard] ``` haftmann@30652 ` 1902` blanchet@35828 ` 1903` ```lemmas le_minus_iff_number_of [simp, no_atp] = ``` haftmann@30652 ` 1904` ``` le_minus_iff [of "number_of v", standard] ``` haftmann@30652 ` 1905` blanchet@35828 ` 1906` ```lemmas equation_minus_iff_number_of [simp, no_atp] = ``` haftmann@30652 ` 1907` ``` equation_minus_iff [of "number_of v", standard] ``` haftmann@30652 ` 1908` blanchet@35828 ` 1909` ```lemmas minus_less_iff_number_of [simp, no_atp] = ``` haftmann@30652 ` 1910` ``` minus_less_iff [of _ "number_of v", standard] ``` haftmann@30652 ` 1911` blanchet@35828 ` 1912` ```lemmas minus_le_iff_number_of [simp, no_atp] = ``` haftmann@30652 ` 1913` ``` minus_le_iff [of _ "number_of v", standard] ``` haftmann@30652 ` 1914` blanchet@35828 ` 1915` ```lemmas minus_equation_iff_number_of [simp, no_atp] = ``` haftmann@30652 ` 1916` ``` minus_equation_iff [of _ "number_of v", standard] ``` haftmann@30652 ` 1917` haftmann@30652 ` 1918` haftmann@30652 ` 1919` ```text{*To Simplify Inequalities Where One Side is the Constant 1*} ``` haftmann@30652 ` 1920` blanchet@35828 ` 1921` ```lemma less_minus_iff_1 [simp,no_atp]: ``` haftmann@35028 ` 1922` ``` fixes b::"'b::{linordered_idom,number_ring}" ``` haftmann@30652 ` 1923` ``` shows "(1 < - b) = (b < -1)" ``` haftmann@30652 ` 1924` ```by auto ``` haftmann@30652 ` 1925` blanchet@35828 ` 1926` ```lemma le_minus_iff_1 [simp,no_atp]: ``` haftmann@35028 ` 1927` ``` fixes b::"'b::{linordered_idom,number_ring}" ``` haftmann@30652 ` 1928` ``` shows "(1 \ - b) = (b \ -1)" ``` haftmann@30652 ` 1929` ```by auto ``` haftmann@30652 ` 1930` blanchet@35828 ` 1931` ```lemma equation_minus_iff_1 [simp,no_atp]: ``` haftmann@30652 ` 1932` ``` fixes b::"'b::number_ring" ``` haftmann@30652 ` 1933` ``` shows "(1 = - b) = (b = -1)" ``` haftmann@30652 ` 1934` ```by (subst equation_minus_iff, auto) ``` haftmann@30652 ` 1935` blanchet@35828 ` 1936` ```lemma minus_less_iff_1 [simp,no_atp]: ``` haftmann@35028 ` 1937` ``` fixes a::"'b::{linordered_idom,number_ring}" ``` haftmann@30652 ` 1938` ``` shows "(- a < 1) = (-1 < a)" ``` haftmann@30652 ` 1939` ```by auto ``` haftmann@30652 ` 1940` blanchet@35828 ` 1941` ```lemma minus_le_iff_1 [simp,no_atp]: ``` haftmann@35028 ` 1942` ``` fixes a::"'b::{linordered_idom,number_ring}" ``` haftmann@30652 ` 1943` ``` shows "(- a \ 1) = (-1 \ a)" ``` haftmann@30652 ` 1944` ```by auto ``` haftmann@30652 ` 1945` blanchet@35828 ` 1946` ```lemma minus_equation_iff_1 [simp,no_atp]: ``` haftmann@30652 ` 1947` ``` fixes a::"'b::number_ring" ``` haftmann@30652 ` 1948` ``` shows "(- a = 1) = (a = -1)" ``` haftmann@30652 ` 1949` ```by (subst minus_equation_iff, auto) ``` haftmann@30652 ` 1950` haftmann@30652 ` 1951` haftmann@30652 ` 1952` ```text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\"}) *} ``` haftmann@30652 ` 1953` blanchet@35828 ` 1954` ```lemmas mult_less_cancel_left_number_of [simp, no_atp] = ``` haftmann@30652 ` 1955` ``` mult_less_cancel_left [of "number_of v", standard] ``` haftmann@30652 ` 1956` blanchet@35828 ` 1957` ```lemmas mult_less_cancel_right_number_of [simp, no_atp] = ``` haftmann@30652 ` 1958` ``` mult_less_cancel_right [of _ "number_of v", standard] ``` haftmann@30652 ` 1959` blanchet@35828 ` 1960` ```lemmas mult_le_cancel_left_number_of [simp, no_atp] = ``` haftmann@30652 ` 1961` ``` mult_le_cancel_left [of "number_of v", standard] ``` haftmann@30652 ` 1962` blanchet@35828 ` 1963` ```lemmas mult_le_cancel_right_number_of [simp, no_atp] = ``` haftmann@30652 ` 1964` ``` mult_le_cancel_right [of _ "number_of v", standard] ``` haftmann@30652 ` 1965` haftmann@30652 ` 1966` haftmann@30652 ` 1967` ```text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\"} and @{text "="}) *} ``` haftmann@30652 ` 1968` haftmann@30652 ` 1969` ```lemmas le_divide_eq_number_of1 [simp] = le_divide_eq [of _ _ "number_of w", standard] ``` haftmann@30652 ` 1970` ```lemmas divide_le_eq_number_of1 [simp] = divide_le_eq [of _ "number_of w", standard] ``` haftmann@30652 ` 1971` ```lemmas less_divide_eq_number_of1 [simp] = less_divide_eq [of _ _ "number_of w", standard] ``` haftmann@30652 ` 1972` ```lemmas divide_less_eq_number_of1 [simp] = divide_less_eq [of _ "number_of w", standard] ``` haftmann@30652 ` 1973` ```lemmas eq_divide_eq_number_of1 [simp] = eq_divide_eq [of _ _ "number_of w", standard] ``` haftmann@30652 ` 1974` ```lemmas divide_eq_eq_number_of1 [simp] = divide_eq_eq [of _ "number_of w", standard] ``` haftmann@30652 ` 1975` haftmann@30652 ` 1976` haftmann@30652 ` 1977` ```subsubsection{*Optional Simplification Rules Involving Constants*} ``` haftmann@30652 ` 1978` haftmann@30652 ` 1979` ```text{*Simplify quotients that are compared with a literal constant.*} ``` haftmann@30652 ` 1980` haftmann@30652 ` 1981` ```lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w", standard] ``` haftmann@30652 ` 1982` ```lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w", standard] ``` haftmann@30652 ` 1983` ```lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w", standard] ``` haftmann@30652 ` 1984` ```lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w", standard] ``` haftmann@30652 ` 1985` ```lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w", standard] ``` haftmann@30652 ` 1986` ```lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w", standard] ``` haftmann@30652 ` 1987` haftmann@30652 ` 1988` haftmann@30652 ` 1989` ```text{*Not good as automatic simprules because they cause case splits.*} ``` haftmann@30652 ` 1990` ```lemmas divide_const_simps = ``` haftmann@30652 ` 1991` ``` le_divide_eq_number_of divide_le_eq_number_of less_divide_eq_number_of ``` haftmann@30652 ` 1992` ``` divide_less_eq_number_of eq_divide_eq_number_of divide_eq_eq_number_of ``` haftmann@30652 ` 1993` ``` le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1 ``` haftmann@30652 ` 1994` haftmann@30652 ` 1995` ```text{*Division By @{text "-1"}*} ``` haftmann@30652 ` 1996` haftmann@30652 ` 1997` ```lemma divide_minus1 [simp]: ``` haftmann@30652 ` 1998` ``` "x/-1 = -(x::'a::{field,division_by_zero,number_ring})" ``` haftmann@30652 ` 1999` ```by simp ``` haftmann@30652 ` 2000` haftmann@30652 ` 2001` ```lemma minus1_divide [simp]: ``` haftmann@30652 ` 2002` ``` "-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)" ``` huffman@35216 ` 2003` ```by (simp add: divide_inverse) ``` haftmann@30652 ` 2004` haftmann@30652 ` 2005` ```lemma half_gt_zero_iff: ``` haftmann@35028 ` 2006` ``` "(0 < r/2) = (0 < (r::'a::{linordered_field,division_by_zero,number_ring}))" ``` haftmann@30652 ` 2007` ```by auto ``` haftmann@30652 ` 2008` haftmann@30652 ` 2009` ```lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2, standard] ``` haftmann@30652 ` 2010` haftmann@30652 ` 2011` haftmann@33320 ` 2012` ```subsection {* The divides relation *} ``` haftmann@33320 ` 2013` nipkow@33657 ` 2014` ```lemma zdvd_antisym_nonneg: ``` nipkow@33657 ` 2015` ``` "0 <= m ==> 0 <= n ==> m dvd n ==> n dvd m ==> m = (n::int)" ``` haftmann@33320 ` 2016` ``` apply (simp add: dvd_def, auto) ``` nipkow@33657 ` 2017` ``` apply (auto simp add: mult_assoc zero_le_mult_iff zmult_eq_1_iff) ``` haftmann@33320 ` 2018` ``` done ``` haftmann@33320 ` 2019` nipkow@33657 ` 2020` ```lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a" ``` haftmann@33320 ` 2021` ``` shows "\a\ = \b\" ``` nipkow@33657 ` 2022` ```proof cases ``` nipkow@33657 ` 2023` ``` assume "a = 0" with assms show ?thesis by simp ``` nipkow@33657 ` 2024` ```next ``` nipkow@33657 ` 2025` ``` assume "a \ 0" ``` haftmann@33320 ` 2026` ``` from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast ``` haftmann@33320 ` 2027` ``` from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast ``` haftmann@33320 ` 2028` ``` from k k' have "a = a*k*k'" by simp ``` haftmann@33320 ` 2029` ``` with mult_cancel_left1[where c="a" and b="k*k'"] ``` haftmann@33320 ` 2030` ``` have kk':"k*k' = 1" using `a\0` by (simp add: mult_assoc) ``` haftmann@33320 ` 2031` ``` hence "k = 1 \ k' = 1 \ k = -1 \ k' = -1" by (simp add: zmult_eq_1_iff) ``` haftmann@33320 ` 2032` ``` thus ?thesis using k k' by auto ``` haftmann@33320 ` 2033` ```qed ``` haftmann@33320 ` 2034` haftmann@33320 ` 2035` ```lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)" ``` haftmann@33320 ` 2036` ``` apply (subgoal_tac "m = n + (m - n)") ``` haftmann@33320 ` 2037` ``` apply (erule ssubst) ``` haftmann@33320 ` 2038` ``` apply (blast intro: dvd_add, simp) ``` haftmann@33320 ` 2039` ``` done ``` haftmann@33320 ` 2040` haftmann@33320 ` 2041` ```lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))" ``` haftmann@33320 ` 2042` ```apply (rule iffI) ``` haftmann@33320 ` 2043` ``` apply (erule_tac [2] dvd_add) ``` haftmann@33320 ` 2044` ``` apply (subgoal_tac "n = (n + k * m) - k * m") ``` haftmann@33320 ` 2045` ``` apply (erule ssubst) ``` haftmann@33320 ` 2046` ``` apply (erule dvd_diff) ``` haftmann@33320 ` 2047` ``` apply(simp_all) ``` haftmann@33320 ` 2048` ```done ``` haftmann@33320 ` 2049` haftmann@33320 ` 2050` ```lemma dvd_imp_le_int: ``` haftmann@33320 ` 2051` ``` fixes d i :: int ``` haftmann@33320 ` 2052` ``` assumes "i \ 0" and "d dvd i" ``` haftmann@33320 ` 2053` ``` shows "\d\ \ \i\" ``` haftmann@33320 ` 2054` ```proof - ``` haftmann@33320 ` 2055` ``` from `d dvd i` obtain k where "i = d * k" .. ``` haftmann@33320 ` 2056` ``` with `i \ 0` have "k \ 0" by auto ``` haftmann@33320 ` 2057` ``` then have "1 \ \k\" and "0 \ \d\" by auto ``` haftmann@33320 ` 2058` ``` then have "\d\ * 1 \ \d\ * \k\" by (rule mult_left_mono) ``` haftmann@33320 ` 2059` ``` with `i = d * k` show ?thesis by (simp add: abs_mult) ``` haftmann@33320 ` 2060` ```qed ``` haftmann@33320 ` 2061` haftmann@33320 ` 2062` ```lemma zdvd_not_zless: ``` haftmann@33320 ` 2063` ``` fixes m n :: int ``` haftmann@33320 ` 2064` ``` assumes "0 < m" and "m < n" ``` haftmann@33320 ` 2065` ``` shows "\ n dvd m" ``` haftmann@33320 ` 2066` ```proof ``` haftmann@33320 ` 2067` ``` from assms have "0 < n" by auto ``` haftmann@33320 ` 2068` ``` assume "n dvd m" then obtain k where k: "m = n * k" .. ``` haftmann@33320 ` 2069` ``` with `0 < m` have "0 < n * k" by auto ``` haftmann@33320 ` 2070` ``` with `0 < n` have "0 < k" by (simp add: zero_less_mult_iff) ``` haftmann@33320 ` 2071` ``` with k `0 < n` `m < n` have "n * k < n * 1" by simp ``` haftmann@33320 ` 2072` ``` with `0 < n` `0 < k` show False unfolding mult_less_cancel_left by auto ``` haftmann@33320 ` 2073` ```qed ``` haftmann@33320 ` 2074` haftmann@33320 ` 2075` ```lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \ (0::int)" ``` haftmann@33320 ` 2076` ``` shows "m dvd n" ``` haftmann@33320 ` 2077` ```proof- ``` haftmann@33320 ` 2078` ``` from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast ``` haftmann@33320 ` 2079` ``` {assume "n \ m*h" hence "k* n \ k* (m*h)" using kz by simp ``` haftmann@33320 ` 2080` ``` with h have False by (simp add: mult_assoc)} ``` haftmann@33320 ` 2081` ``` hence "n = m * h" by blast ``` haftmann@33320 ` 2082` ``` thus ?thesis by simp ``` haftmann@33320 ` 2083` ```qed ``` haftmann@33320 ` 2084` haftmann@33320 ` 2085` ```theorem zdvd_int: "(x dvd y) = (int x dvd int y)" ``` haftmann@33320 ` 2086` ```proof - ``` haftmann@33320 ` 2087` ``` have "\k. int y = int x * k \ x dvd y" ``` haftmann@33320 ` 2088` ``` proof - ``` haftmann@33320 ` 2089` ``` fix k ``` haftmann@33320 ` 2090` ``` assume A: "int y = int x * k" ``` haftmann@33320 ` 2091` ``` then show "x dvd y" proof (cases k) ``` haftmann@33320 ` 2092` ``` case (1 n) with A have "y = x * n" by (simp add: of_nat_mult [symmetric]) ``` haftmann@33320 ` 2093` ``` then show ?thesis .. ``` haftmann@33320 ` 2094` ``` next ``` haftmann@33320 ` 2095` ``` case (2 n) with A have "int y = int x * (- int (Suc n))" by simp ``` haftmann@33320 ` 2096` ``` also have "\ = - (int x * int (Suc n))" by (simp only: mult_minus_right) ``` haftmann@33320 ` 2097` ``` also have "\ = - int (x * Suc n)" by (simp only: of_nat_mult [symmetric]) ``` haftmann@33320 ` 2098` ``` finally have "- int (x * Suc n) = int y" .. ``` haftmann@33320 ` 2099` ``` then show ?thesis by (simp only: negative_eq_positive) auto ``` haftmann@33320 ` 2100` ``` qed ``` haftmann@33320 ` 2101` ``` qed ``` haftmann@33320 ` 2102` ``` then show ?thesis by (auto elim!: dvdE simp only: dvd_triv_left of_nat_mult) ``` haftmann@33320 ` 2103` ```qed ``` haftmann@33320 ` 2104` haftmann@33320 ` 2105` ```lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \x\ = 1)" ``` haftmann@33320 ` 2106` ```proof ``` haftmann@33320 ` 2107` ``` assume d: "x dvd 1" hence "int (nat \x\) dvd int (nat 1)" by simp ``` haftmann@33320 ` 2108` ``` hence "nat \x\ dvd 1" by (simp add: zdvd_int) ``` haftmann@33320 ` 2109` ``` hence "nat \x\ = 1" by simp ``` haftmann@33320 ` 2110` ``` thus "\x\ = 1" by (cases "x < 0", auto) ``` haftmann@33320 ` 2111` ```next ``` haftmann@33320 ` 2112` ``` assume "\x\=1" ``` haftmann@33320 ` 2113` ``` then have "x = 1 \ x = -1" by auto ``` haftmann@33320 ` 2114` ``` then show "x dvd 1" by (auto intro: dvdI) ``` haftmann@33320 ` 2115` ```qed ``` haftmann@33320 ` 2116` haftmann@33320 ` 2117` ```lemma zdvd_mult_cancel1: ``` haftmann@33320 ` 2118` ``` assumes mp:"m \(0::int)" shows "(m * n dvd m) = (\n\ = 1)" ``` haftmann@33320 ` 2119` ```proof ``` haftmann@33320 ` 2120` ``` assume n1: "\n\ = 1" thus "m * n dvd m" ``` huffman@35216 ` 2121` ``` by (cases "n >0", auto simp add: minus_equation_iff) ``` haftmann@33320 ` 2122` ```next ``` haftmann@33320 ` 2123` ``` assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp ``` haftmann@33320 ` 2124` ``` from zdvd_mult_cancel[OF H2 mp] show "\n\ = 1" by (simp only: zdvd1_eq) ``` haftmann@33320 ` 2125` ```qed ``` haftmann@33320 ` 2126` haftmann@33320 ` 2127` ```lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))" ``` haftmann@33320 ` 2128` ``` unfolding zdvd_int by (cases "z \ 0") simp_all ``` haftmann@33320 ` 2129` haftmann@33320 ` 2130` ```lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)" ``` haftmann@33320 ` 2131` ``` unfolding zdvd_int by (cases "z \ 0") simp_all ``` haftmann@33320 ` 2132` haftmann@33320 ` 2133` ```lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \ z then (z dvd int m) else m = 0)" ``` haftmann@33320 ` 2134` ``` by (auto simp add: dvd_int_iff) ``` haftmann@33320 ` 2135` haftmann@33341 ` 2136` ```lemma eq_nat_nat_iff: ``` haftmann@33341 ` 2137` ``` "0 \ z \ 0 \ z' \ nat z = nat z' \ z = z'" ``` haftmann@33341 ` 2138` ``` by (auto elim!: nonneg_eq_int) ``` haftmann@33341 ` 2139` haftmann@33341 ` 2140` ```lemma nat_power_eq: ``` haftmann@33341 ` 2141` ``` "0 \ z \ nat (z ^ n) = nat z ^ n" ``` haftmann@33341 ` 2142` ``` by (induct n) (simp_all add: nat_mult_distrib) ``` haftmann@33341 ` 2143` haftmann@33320 ` 2144` ```lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \ (n::int)" ``` haftmann@33320 ` 2145` ``` apply (rule_tac z=n in int_cases) ``` haftmann@33320 ` 2146` ``` apply (auto simp add: dvd_int_iff) ``` haftmann@33320 ` 2147` ``` apply (rule_tac z=z in int_cases) ``` haftmann@33320 ` 2148` ``` apply (auto simp add: dvd_imp_le) ``` haftmann@33320 ` 2149` ``` done ``` haftmann@33320 ` 2150` haftmann@33320 ` 2151` haftmann@25919 ` 2152` ```subsection {* Configuration of the code generator *} ``` haftmann@25919 ` 2153` haftmann@26507 ` 2154` ```code_datatype Pls Min Bit0 Bit1 "number_of \ int \ int" ``` haftmann@26507 ` 2155` haftmann@28562 ` 2156` ```lemmas pred_succ_numeral_code [code] = ``` haftmann@26507 ` 2157` ``` pred_bin_simps succ_bin_simps ``` haftmann@26507 ` 2158` haftmann@28562 ` 2159` ```lemmas plus_numeral_code [code] = ``` haftmann@26507 ` 2160` ``` add_bin_simps ``` haftmann@26507 ` 2161` ``` arith_extra_simps(1) [where 'a = int] ``` haftmann@26507 ` 2162` haftmann@28562 ` 2163` ```lemmas minus_numeral_code [code] = ``` haftmann@26507 ` 2164` ``` minus_bin_simps ``` haftmann@26507 ` 2165` ``` arith_extra_simps(2) [where 'a = int] ``` haftmann@26507 ` 2166` ``` arith_extra_simps(5) [where 'a = int] ``` haftmann@26507 ` 2167` haftmann@28562 ` 2168` ```lemmas times_numeral_code [code] = ``` haftmann@26507 ` 2169` ``` mult_bin_simps ``` haftmann@26507 ` 2170` ``` arith_extra_simps(4) [where 'a = int] ``` haftmann@26507 ` 2171` haftmann@26507 ` 2172` ```instantiation int :: eq ``` haftmann@26507 ` 2173` ```begin ``` haftmann@26507 ` 2174` haftmann@28562 ` 2175` ```definition [code del]: "eq_class.eq k l \ k - l = (0\int)" ``` haftmann@26507 ` 2176` haftmann@26507 ` 2177` ```instance by default (simp add: eq_int_def) ``` haftmann@26507 ` 2178` haftmann@26507 ` 2179` ```end ``` haftmann@26507 ` 2180` haftmann@28562 ` 2181` ```lemma eq_number_of_int_code [code]: ``` haftmann@26732 ` 2182` ``` "eq_class.eq (number_of k \ int) (number_of l) \ eq_class.eq k l" ``` haftmann@26507 ` 2183` ``` unfolding eq_int_def number_of_is_id .. ``` haftmann@26507 ` 2184` haftmann@28562 ` 2185` ```lemma eq_int_code [code]: ``` haftmann@26732 ` 2186` ``` "eq_class.eq Int.Pls Int.Pls \ True" ``` haftmann@26732 ` 2187` ``` "eq_class.eq Int.Pls Int.Min \ False" ``` haftmann@26732 ` 2188` ``` "eq_class.eq Int.Pls (Int.Bit0 k2) \ eq_class.eq Int.Pls k2" ``` haftmann@26732 ` 2189` ``` "eq_class.eq Int.Pls (Int.Bit1 k2) \ False" ``` haftmann@26732 ` 2190` ``` "eq_class.eq Int.Min Int.Pls \ False" ``` haftmann@26732 ` 2191` ``` "eq_class.eq Int.Min Int.Min \ True" ``` haftmann@26732 ` 2192` ``` "eq_class.eq Int.Min (Int.Bit0 k2) \ False" ``` haftmann@26732 ` 2193` ``` "eq_class.eq Int.Min (Int.Bit1 k2) \ eq_class.eq Int.Min k2" ``` huffman@28958 ` 2194` ``` "eq_class.eq (Int.Bit0 k1) Int.Pls \ eq_class.eq k1 Int.Pls" ``` haftmann@26732 ` 2195` ``` "eq_class.eq (Int.Bit1 k1) Int.Pls \ False" ``` haftmann@26732 ` 2196` ``` "eq_class.eq (Int.Bit0 k1) Int.Min \ False" ``` huffman@28958 ` 2197` ``` "eq_class.eq (Int.Bit1 k1) Int.Min \ eq_class.eq k1 Int.Min" ``` haftmann@26732 ` 2198` ``` "eq_class.eq (Int.Bit0 k1) (Int.Bit0 k2) \ eq_class.eq k1 k2" ``` haftmann@26732 ` 2199` ``` "eq_class.eq (Int.Bit0 k1) (Int.Bit1 k2) \ False" ``` haftmann@26732 ` 2200` ``` "eq_class.eq (Int.Bit1 k1) (Int.Bit0 k2) \ False" ``` haftmann@26732 ` 2201` ``` "eq_class.eq (Int.Bit1 k1) (Int.Bit1 k2) \ eq_class.eq k1 k2" ``` huffman@28958 ` 2202` ``` unfolding eq_equals by simp_all ``` haftmann@25919 ` 2203` haftmann@28351 ` 2204` ```lemma eq_int_refl [code nbe]: ``` haftmann@28351 ` 2205` ``` "eq_class.eq (k::int) k \ True" ``` haftmann@28351 ` 2206` ``` by (rule HOL.eq_refl) ``` haftmann@28351 ` 2207` haftmann@28562 ` 2208` ```lemma less_eq_number_of_int_code [code]: ``` haftmann@26507 ` 2209` ``` "(number_of k \ int) \ number_of l \ k \ l" ``` haftmann@26507 ` 2210` ``` unfolding number_of_is_id .. ``` haftmann@26507 ` 2211` haftmann@28562 ` 2212` ```lemma less_eq_int_code [code]: ``` haftmann@26507 ` 2213` ``` "Int.Pls \ Int.Pls \ True" ``` haftmann@26507 ` 2214` ``` "Int.Pls \ Int.Min \ False" ``` haftmann@26507 ` 2215` ``` "Int.Pls \ Int.Bit0 k \ Int.Pls \ k" ``` haftmann@26507 ` 2216` ``` "Int.Pls \ Int.Bit1 k \ Int.Pls \ k" ``` haftmann@26507 ` 2217` ``` "Int.Min \ Int.Pls \ True" ``` haftmann@26507 ` 2218` ``` "Int.Min \ Int.Min \ True" ``` haftmann@26507 ` 2219` ``` "Int.Min \ Int.Bit0 k \ Int.Min < k" ``` haftmann@26507 ` 2220` ``` "Int.Min \ Int.Bit1 k \ Int.Min \ k" ``` haftmann@26507 ` 2221` ``` "Int.Bit0 k \ Int.Pls \ k \ Int.Pls" ``` haftmann@26507 ` 2222` ``` "Int.Bit1 k \ Int.Pls \ k < Int.Pls" ``` haftmann@26507 ` 2223` ``` "Int.Bit0 k \ Int.Min \ k \ Int.Min" ``` haftmann@26507 ` 2224` ``` "Int.Bit1 k \ Int.Min \ k \ Int.Min" ``` haftmann@26507 ` 2225` ``` "Int.Bit0 k1 \ Int.Bit0 k2 \ k1 \ k2" ``` haftmann@26507 ` 2226` ``` "Int.Bit0 k1 \ Int.Bit1 k2 \ k1 \ k2" ``` haftmann@26507 ` 2227` ``` "Int.Bit1 k1 \ Int.Bit0 k2 \ k1 < k2" ``` haftmann@26507 ` 2228` ``` "Int.Bit1 k1 \ Int.Bit1 k2 \ k1 \ k2" ``` huffman@28958 ` 2229` ``` by simp_all ``` haftmann@26507 ` 2230` haftmann@28562 ` 2231` ```lemma less_number_of_int_code [code]: ``` haftmann@26507 ` 2232` ``` "(number_of k \ int) < number_of l \ k < l" ``` haftmann@26507 ` 2233` ``` unfolding number_of_is_id .. ``` haftmann@26507 ` 2234` haftmann@28562 ` 2235` ```lemma less_int_code [code]: ``` haftmann@26507 ` 2236` ``` "Int.Pls < Int.Pls \ False" ``` haftmann@26507 ` 2237` ``` "Int.Pls < Int.Min \ False" ``` haftmann@26507 ` 2238` ``` "Int.Pls < Int.Bit0 k \ Int.Pls < k" ``` haftmann@26507 ` 2239` ``` "Int.Pls < Int.Bit1 k \ Int.Pls \ k" ``` haftmann@26507 ` 2240` ``` "Int.Min < Int.Pls \ True" ``` haftmann@26507 ` 2241` ``` "Int.Min < Int.Min \ False" ``` haftmann@26507 ` 2242` ``` "Int.Min < Int.Bit0 k \ Int.Min < k" ``` haftmann@26507 ` 2243` ``` "Int.Min < Int.Bit1 k \ Int.Min < k" ``` haftmann@26507 ` 2244` ``` "Int.Bit0 k < Int.Pls \ k < Int.Pls" ``` haftmann@26507 ` 2245` ``` "Int.Bit1 k < Int.Pls \ k < Int.Pls" ``` haftmann@26507 ` 2246` ``` "Int.Bit0 k < Int.Min \ k \ Int.Min" ``` haftmann@26507 ` 2247` ``` "Int.Bit1 k < Int.Min \ k < Int.Min" ``` haftmann@26507 ` 2248` ``` "Int.Bit0 k1 < Int.Bit0 k2 \ k1 < k2" ``` haftmann@26507 ` 2249` ``` "Int.Bit0 k1 < Int.Bit1 k2 \ k1 \ k2" ``` haftmann@26507 ` 2250` ``` "Int.Bit1 k1 < Int.Bit0 k2 \ k1 < k2" ``` haftmann@26507 ` 2251` ``` "Int.Bit1 k1 < Int.Bit1 k2 \ k1 < k2" ``` huffman@28958 ` 2252` ``` by simp_all ``` haftmann@25919 ` 2253` haftmann@25919 ` 2254` ```definition ``` haftmann@25919 ` 2255` ``` nat_aux :: "int \ nat \ nat" where ``` haftmann@25919 ` 2256` ``` "nat_aux i n = nat i + n" ``` haftmann@25919 ` 2257` haftmann@25919 ` 2258` ```lemma [code]: ``` haftmann@25919 ` 2259` ``` "nat_aux i n = (if i \ 0 then n else nat_aux (i - 1) (Suc n))" -- {* tail recursive *} ``` haftmann@25919 ` 2260` ``` by (auto simp add: nat_aux_def nat_eq_iff linorder_not_le order_less_imp_le ``` haftmann@25919 ` 2261` ``` dest: zless_imp_add1_zle) ``` haftmann@25919 ` 2262` haftmann@25919 ` 2263` ```lemma [code]: "nat i = nat_aux i 0" ``` haftmann@25919 ` 2264` ``` by (simp add: nat_aux_def) ``` haftmann@25919 ` 2265` haftmann@28514 ` 2266` ```hide (open) const nat_aux ``` haftmann@25928 ` 2267` haftmann@32069 ` 2268` ```lemma zero_is_num_zero [code, code_unfold_post]: ``` haftmann@25919 ` 2269` ``` "(0\int) = Numeral0" ``` haftmann@25919 ` 2270` ``` by simp ``` haftmann@25919 ` 2271` haftmann@32069 ` 2272` ```lemma one_is_num_one [code, code_unfold_post]: ``` haftmann@25919 ` 2273` ``` "(1\int) = Numeral1" ``` haftmann@25961 ` 2274` ``` by simp ``` haftmann@25919 ` 2275` haftmann@25919 ` 2276` ```code_modulename SML ``` haftmann@33364 ` 2277` ``` Int Arith ``` haftmann@25919 ` 2278` haftmann@25919 ` 2279` ```code_modulename OCaml ``` haftmann@33364 ` 2280` ``` Int Arith ``` haftmann@25919 ` 2281` haftmann@25919 ` 2282` ```code_modulename Haskell ``` haftmann@33364 ` 2283` ``` Int Arith ``` haftmann@25919 ` 2284` haftmann@25919 ` 2285` ```types_code ``` haftmann@25919 ` 2286` ``` "int" ("int") ``` haftmann@25919 ` 2287` ```attach (term_of) {* ``` haftmann@25919 ` 2288` ```val term_of_int = HOLogic.mk_number HOLogic.intT; ``` haftmann@25919 ` 2289` ```*} ``` haftmann@25919 ` 2290` ```attach (test) {* ``` haftmann@25919 ` 2291` ```fun gen_int i = ``` haftmann@25919 ` 2292` ``` let val j = one_of [~1, 1] * random_range 0 i ``` haftmann@25919 ` 2293` ``` in (j, fn () => term_of_int j) end; ``` haftmann@25919 ` 2294` ```*} ``` haftmann@25919 ` 2295` haftmann@25919 ` 2296` ```setup {* ``` haftmann@25919 ` 2297` ```let ``` haftmann@25919 ` 2298` haftmann@25919 ` 2299` ```fun strip_number_of (@{term "Int.number_of :: int => int"} \$ t) = t ``` haftmann@25919 ` 2300` ``` | strip_number_of t = t; ``` haftmann@25919 ` 2301` haftmann@28537 ` 2302` ```fun numeral_codegen thy defs dep module b t gr = ``` haftmann@25919 ` 2303` ``` let val i = HOLogic.dest_numeral (strip_number_of t) ``` haftmann@25919 ` 2304` ``` in ``` haftmann@28537 ` 2305` ``` SOME (Codegen.str (string_of_int i), ``` haftmann@28537 ` 2306` ``` snd (Codegen.invoke_tycodegen thy defs dep module false HOLogic.intT gr)) ``` haftmann@25919 ` 2307` ``` end handle TERM _ => NONE; ``` haftmann@25919 ` 2308` haftmann@25919 ` 2309` ```in ``` haftmann@25919 ` 2310` haftmann@25919 ` 2311` ```Codegen.add_codegen "numeral_codegen" numeral_codegen ``` haftmann@25919 ` 2312` haftmann@25919 ` 2313` ```end ``` haftmann@25919 ` 2314` ```*} ``` haftmann@25919 ` 2315` haftmann@25919 ` 2316` ```consts_code ``` haftmann@25919 ` 2317` ``` "number_of :: int \ int" ("(_)") ``` haftmann@25919 ` 2318` ``` "0 :: int" ("0") ``` haftmann@25919 ` 2319` ``` "1 :: int" ("1") ``` haftmann@25919 ` 2320` ``` "uminus :: int => int" ("~") ``` haftmann@25919 ` 2321` ``` "op + :: int => int => int" ("(_ +/ _)") ``` haftmann@25919 ` 2322` ``` "op * :: int => int => int" ("(_ */ _)") ``` haftmann@25919 ` 2323` ``` "op \ :: int => int => bool" ("(_ <=/ _)") ``` haftmann@25919 ` 2324` ``` "op < :: int => int => bool" ("(_ (x \ (0::int) | n = 0)" ``` haftmann@30960 ` 2393` ``` by (rule zero_less_power_abs_iff) ``` haftmann@30960 ` 2394` haftmann@30960 ` 2395` ```lemma zero_le_zpower_abs: "(0::int) \ abs x ^ n" ``` haftmann@30960 ` 2396` ``` by (rule zero_le_power_abs) ``` haftmann@30960 ` 2397` haftmann@31015 ` 2398` ```lemma zpower_zpower: ``` haftmann@31015 ` 2399` ``` "(x ^ y) ^ z = (x ^ (y * z)::int)" ``` haftmann@31015 ` 2400` ``` by (rule power_mult [symmetric]) ``` haftmann@31015 ` 2401` haftmann@31015 ` 2402` ```lemma int_power: ``` haftmann@31015 ` 2403` ``` "int (m ^ n) = int m ^ n" ``` haftmann@31015 ` 2404` ``` by (rule of_nat_power) ``` haftmann@31015 ` 2405` haftmann@31015 ` 2406` ```lemmas zpower_int = int_power [symmetric] ``` haftmann@31015 ` 2407` haftmann@25919 ` 2408` ```end ```