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