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