src/HOL/IntDef.thy
 author huffman Mon Jun 11 06:14:32 2007 +0200 (2007-06-11) changeset 23308 95a01ddfb024 parent 23307 2fe3345035c7 child 23365 f31794033ae1 permissions -rw-r--r--
simplify int proofs
 wenzelm@23164 ` 1` ```(* Title: IntDef.thy ``` wenzelm@23164 ` 2` ``` ID: \$Id\$ ``` wenzelm@23164 ` 3` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` wenzelm@23164 ` 4` ``` Copyright 1996 University of Cambridge ``` wenzelm@23164 ` 5` wenzelm@23164 ` 6` ```*) ``` wenzelm@23164 ` 7` wenzelm@23164 ` 8` ```header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*} ``` wenzelm@23164 ` 9` wenzelm@23164 ` 10` ```theory IntDef ``` wenzelm@23164 ` 11` ```imports Equiv_Relations Nat ``` wenzelm@23164 ` 12` ```begin ``` wenzelm@23164 ` 13` wenzelm@23164 ` 14` ```text {* the equivalence relation underlying the integers *} ``` wenzelm@23164 ` 15` wenzelm@23164 ` 16` ```definition ``` wenzelm@23164 ` 17` ``` intrel :: "((nat \ nat) \ (nat \ nat)) set" ``` wenzelm@23164 ` 18` ```where ``` wenzelm@23164 ` 19` ``` "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }" ``` wenzelm@23164 ` 20` wenzelm@23164 ` 21` ```typedef (Integ) ``` wenzelm@23164 ` 22` ``` int = "UNIV//intrel" ``` wenzelm@23164 ` 23` ``` by (auto simp add: quotient_def) ``` wenzelm@23164 ` 24` wenzelm@23164 ` 25` ```instance int :: zero ``` huffman@23299 ` 26` ``` Zero_int_def: "0 \ Abs_Integ (intrel `` {(0, 0)})" .. ``` wenzelm@23164 ` 27` wenzelm@23164 ` 28` ```instance int :: one ``` huffman@23299 ` 29` ``` One_int_def: "1 \ Abs_Integ (intrel `` {(1, 0)})" .. ``` wenzelm@23164 ` 30` wenzelm@23164 ` 31` ```instance int :: plus ``` wenzelm@23164 ` 32` ``` add_int_def: "z + w \ Abs_Integ ``` wenzelm@23164 ` 33` ``` (\(x, y) \ Rep_Integ z. \(u, v) \ Rep_Integ w. ``` wenzelm@23164 ` 34` ``` intrel `` {(x + u, y + v)})" .. ``` wenzelm@23164 ` 35` wenzelm@23164 ` 36` ```instance int :: minus ``` wenzelm@23164 ` 37` ``` minus_int_def: ``` wenzelm@23164 ` 38` ``` "- z \ Abs_Integ (\(x, y) \ Rep_Integ z. intrel `` {(y, x)})" ``` wenzelm@23164 ` 39` ``` diff_int_def: "z - w \ z + (-w)" .. ``` wenzelm@23164 ` 40` wenzelm@23164 ` 41` ```instance int :: times ``` wenzelm@23164 ` 42` ``` mult_int_def: "z * w \ Abs_Integ ``` wenzelm@23164 ` 43` ``` (\(x, y) \ Rep_Integ z. \(u,v ) \ Rep_Integ w. ``` wenzelm@23164 ` 44` ``` intrel `` {(x*u + y*v, x*v + y*u)})" .. ``` wenzelm@23164 ` 45` wenzelm@23164 ` 46` ```instance int :: ord ``` wenzelm@23164 ` 47` ``` le_int_def: ``` wenzelm@23164 ` 48` ``` "z \ w \ \x y u v. x+v \ u+y \ (x, y) \ Rep_Integ z \ (u, v) \ Rep_Integ w" ``` wenzelm@23164 ` 49` ``` less_int_def: "z < w \ z \ w \ z \ w" .. ``` wenzelm@23164 ` 50` wenzelm@23164 ` 51` ```lemmas [code func del] = Zero_int_def One_int_def add_int_def ``` wenzelm@23164 ` 52` ``` minus_int_def mult_int_def le_int_def less_int_def ``` wenzelm@23164 ` 53` wenzelm@23164 ` 54` wenzelm@23164 ` 55` ```subsection{*Construction of the Integers*} ``` wenzelm@23164 ` 56` wenzelm@23164 ` 57` ```subsubsection{*Preliminary Lemmas about the Equivalence Relation*} ``` wenzelm@23164 ` 58` wenzelm@23164 ` 59` ```lemma intrel_iff [simp]: "(((x,y),(u,v)) \ intrel) = (x+v = u+y)" ``` wenzelm@23164 ` 60` ```by (simp add: intrel_def) ``` wenzelm@23164 ` 61` wenzelm@23164 ` 62` ```lemma equiv_intrel: "equiv UNIV intrel" ``` wenzelm@23164 ` 63` ```by (simp add: intrel_def equiv_def refl_def sym_def trans_def) ``` wenzelm@23164 ` 64` wenzelm@23164 ` 65` ```text{*Reduces equality of equivalence classes to the @{term intrel} relation: ``` wenzelm@23164 ` 66` ``` @{term "(intrel `` {x} = intrel `` {y}) = ((x,y) \ intrel)"} *} ``` wenzelm@23164 ` 67` ```lemmas equiv_intrel_iff [simp] = eq_equiv_class_iff [OF equiv_intrel UNIV_I UNIV_I] ``` wenzelm@23164 ` 68` wenzelm@23164 ` 69` ```text{*All equivalence classes belong to set of representatives*} ``` wenzelm@23164 ` 70` ```lemma [simp]: "intrel``{(x,y)} \ Integ" ``` wenzelm@23164 ` 71` ```by (auto simp add: Integ_def intrel_def quotient_def) ``` wenzelm@23164 ` 72` wenzelm@23164 ` 73` ```text{*Reduces equality on abstractions to equality on representatives: ``` wenzelm@23164 ` 74` ``` @{prop "\x \ Integ; y \ Integ\ \ (Abs_Integ x = Abs_Integ y) = (x=y)"} *} ``` wenzelm@23164 ` 75` ```declare Abs_Integ_inject [simp] Abs_Integ_inverse [simp] ``` wenzelm@23164 ` 76` wenzelm@23164 ` 77` ```text{*Case analysis on the representation of an integer as an equivalence ``` wenzelm@23164 ` 78` ``` class of pairs of naturals.*} ``` wenzelm@23164 ` 79` ```lemma eq_Abs_Integ [case_names Abs_Integ, cases type: int]: ``` wenzelm@23164 ` 80` ``` "(!!x y. z = Abs_Integ(intrel``{(x,y)}) ==> P) ==> P" ``` wenzelm@23164 ` 81` ```apply (rule Abs_Integ_cases [of z]) ``` wenzelm@23164 ` 82` ```apply (auto simp add: Integ_def quotient_def) ``` wenzelm@23164 ` 83` ```done ``` wenzelm@23164 ` 84` wenzelm@23164 ` 85` wenzelm@23164 ` 86` ```subsubsection{*Integer Unary Negation*} ``` wenzelm@23164 ` 87` wenzelm@23164 ` 88` ```lemma minus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})" ``` wenzelm@23164 ` 89` ```proof - ``` wenzelm@23164 ` 90` ``` have "(\(x,y). intrel``{(y,x)}) respects intrel" ``` wenzelm@23164 ` 91` ``` by (simp add: congruent_def) ``` wenzelm@23164 ` 92` ``` thus ?thesis ``` wenzelm@23164 ` 93` ``` by (simp add: minus_int_def UN_equiv_class [OF equiv_intrel]) ``` wenzelm@23164 ` 94` ```qed ``` wenzelm@23164 ` 95` wenzelm@23164 ` 96` ```lemma zminus_zminus: "- (- z) = (z::int)" ``` wenzelm@23164 ` 97` ``` by (cases z) (simp add: minus) ``` wenzelm@23164 ` 98` wenzelm@23164 ` 99` ```lemma zminus_0: "- 0 = (0::int)" ``` huffman@23299 ` 100` ``` by (simp add: Zero_int_def minus) ``` wenzelm@23164 ` 101` wenzelm@23164 ` 102` wenzelm@23164 ` 103` ```subsection{*Integer Addition*} ``` wenzelm@23164 ` 104` wenzelm@23164 ` 105` ```lemma add: ``` wenzelm@23164 ` 106` ``` "Abs_Integ (intrel``{(x,y)}) + Abs_Integ (intrel``{(u,v)}) = ``` wenzelm@23164 ` 107` ``` Abs_Integ (intrel``{(x+u, y+v)})" ``` wenzelm@23164 ` 108` ```proof - ``` wenzelm@23164 ` 109` ``` have "(\z w. (\(x,y). (\(u,v). intrel `` {(x+u, y+v)}) w) z) ``` wenzelm@23164 ` 110` ``` respects2 intrel" ``` wenzelm@23164 ` 111` ``` by (simp add: congruent2_def) ``` wenzelm@23164 ` 112` ``` thus ?thesis ``` wenzelm@23164 ` 113` ``` by (simp add: add_int_def UN_UN_split_split_eq ``` wenzelm@23164 ` 114` ``` UN_equiv_class2 [OF equiv_intrel equiv_intrel]) ``` wenzelm@23164 ` 115` ```qed ``` wenzelm@23164 ` 116` wenzelm@23164 ` 117` ```lemma zminus_zadd_distrib: "- (z + w) = (- z) + (- w::int)" ``` wenzelm@23164 ` 118` ``` by (cases z, cases w) (simp add: minus add) ``` wenzelm@23164 ` 119` wenzelm@23164 ` 120` ```lemma zadd_commute: "(z::int) + w = w + z" ``` wenzelm@23164 ` 121` ``` by (cases z, cases w) (simp add: add_ac add) ``` wenzelm@23164 ` 122` wenzelm@23164 ` 123` ```lemma zadd_assoc: "((z1::int) + z2) + z3 = z1 + (z2 + z3)" ``` wenzelm@23164 ` 124` ``` by (cases z1, cases z2, cases z3) (simp add: add add_assoc) ``` wenzelm@23164 ` 125` wenzelm@23164 ` 126` ```(*For AC rewriting*) ``` wenzelm@23164 ` 127` ```lemma zadd_left_commute: "x + (y + z) = y + ((x + z) ::int)" ``` wenzelm@23164 ` 128` ``` apply (rule mk_left_commute [of "op +"]) ``` wenzelm@23164 ` 129` ``` apply (rule zadd_assoc) ``` wenzelm@23164 ` 130` ``` apply (rule zadd_commute) ``` wenzelm@23164 ` 131` ``` done ``` wenzelm@23164 ` 132` wenzelm@23164 ` 133` ```lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute ``` wenzelm@23164 ` 134` wenzelm@23164 ` 135` ```lemmas zmult_ac = OrderedGroup.mult_ac ``` wenzelm@23164 ` 136` wenzelm@23164 ` 137` ```(*also for the instance declaration int :: comm_monoid_add*) ``` wenzelm@23164 ` 138` ```lemma zadd_0: "(0::int) + z = z" ``` huffman@23299 ` 139` ```apply (simp add: Zero_int_def) ``` wenzelm@23164 ` 140` ```apply (cases z, simp add: add) ``` wenzelm@23164 ` 141` ```done ``` wenzelm@23164 ` 142` wenzelm@23164 ` 143` ```lemma zadd_0_right: "z + (0::int) = z" ``` wenzelm@23164 ` 144` ```by (rule trans [OF zadd_commute zadd_0]) ``` wenzelm@23164 ` 145` wenzelm@23164 ` 146` ```lemma zadd_zminus_inverse2: "(- z) + z = (0::int)" ``` huffman@23299 ` 147` ```by (cases z, simp add: Zero_int_def minus add) ``` wenzelm@23164 ` 148` wenzelm@23164 ` 149` wenzelm@23164 ` 150` ```subsection{*Integer Multiplication*} ``` wenzelm@23164 ` 151` wenzelm@23164 ` 152` ```text{*Congruence property for multiplication*} ``` wenzelm@23164 ` 153` ```lemma mult_congruent2: ``` wenzelm@23164 ` 154` ``` "(%p1 p2. (%(x,y). (%(u,v). intrel``{(x*u + y*v, x*v + y*u)}) p2) p1) ``` wenzelm@23164 ` 155` ``` respects2 intrel" ``` wenzelm@23164 ` 156` ```apply (rule equiv_intrel [THEN congruent2_commuteI]) ``` wenzelm@23164 ` 157` ``` apply (force simp add: mult_ac, clarify) ``` wenzelm@23164 ` 158` ```apply (simp add: congruent_def mult_ac) ``` wenzelm@23164 ` 159` ```apply (rename_tac u v w x y z) ``` wenzelm@23164 ` 160` ```apply (subgoal_tac "u*y + x*y = w*y + v*y & u*z + x*z = w*z + v*z") ``` wenzelm@23164 ` 161` ```apply (simp add: mult_ac) ``` wenzelm@23164 ` 162` ```apply (simp add: add_mult_distrib [symmetric]) ``` wenzelm@23164 ` 163` ```done ``` wenzelm@23164 ` 164` wenzelm@23164 ` 165` wenzelm@23164 ` 166` ```lemma mult: ``` wenzelm@23164 ` 167` ``` "Abs_Integ((intrel``{(x,y)})) * Abs_Integ((intrel``{(u,v)})) = ``` wenzelm@23164 ` 168` ``` Abs_Integ(intrel `` {(x*u + y*v, x*v + y*u)})" ``` wenzelm@23164 ` 169` ```by (simp add: mult_int_def UN_UN_split_split_eq mult_congruent2 ``` wenzelm@23164 ` 170` ``` UN_equiv_class2 [OF equiv_intrel equiv_intrel]) ``` wenzelm@23164 ` 171` wenzelm@23164 ` 172` ```lemma zmult_zminus: "(- z) * w = - (z * (w::int))" ``` wenzelm@23164 ` 173` ```by (cases z, cases w, simp add: minus mult add_ac) ``` wenzelm@23164 ` 174` wenzelm@23164 ` 175` ```lemma zmult_commute: "(z::int) * w = w * z" ``` wenzelm@23164 ` 176` ```by (cases z, cases w, simp add: mult add_ac mult_ac) ``` wenzelm@23164 ` 177` wenzelm@23164 ` 178` ```lemma zmult_assoc: "((z1::int) * z2) * z3 = z1 * (z2 * z3)" ``` wenzelm@23164 ` 179` ```by (cases z1, cases z2, cases z3, simp add: mult add_mult_distrib2 mult_ac) ``` wenzelm@23164 ` 180` wenzelm@23164 ` 181` ```lemma zadd_zmult_distrib: "((z1::int) + z2) * w = (z1 * w) + (z2 * w)" ``` wenzelm@23164 ` 182` ```by (cases z1, cases z2, cases w, simp add: add mult add_mult_distrib2 mult_ac) ``` wenzelm@23164 ` 183` wenzelm@23164 ` 184` ```lemma zadd_zmult_distrib2: "(w::int) * (z1 + z2) = (w * z1) + (w * z2)" ``` wenzelm@23164 ` 185` ```by (simp add: zmult_commute [of w] zadd_zmult_distrib) ``` wenzelm@23164 ` 186` wenzelm@23164 ` 187` ```lemma zdiff_zmult_distrib: "((z1::int) - z2) * w = (z1 * w) - (z2 * w)" ``` wenzelm@23164 ` 188` ```by (simp add: diff_int_def zadd_zmult_distrib zmult_zminus) ``` wenzelm@23164 ` 189` wenzelm@23164 ` 190` ```lemma zdiff_zmult_distrib2: "(w::int) * (z1 - z2) = (w * z1) - (w * z2)" ``` wenzelm@23164 ` 191` ```by (simp add: zmult_commute [of w] zdiff_zmult_distrib) ``` wenzelm@23164 ` 192` wenzelm@23164 ` 193` ```lemmas int_distrib = ``` wenzelm@23164 ` 194` ``` zadd_zmult_distrib zadd_zmult_distrib2 ``` wenzelm@23164 ` 195` ``` zdiff_zmult_distrib zdiff_zmult_distrib2 ``` wenzelm@23164 ` 196` wenzelm@23164 ` 197` wenzelm@23164 ` 198` ```lemma zmult_1: "(1::int) * z = z" ``` huffman@23299 ` 199` ```by (cases z, simp add: One_int_def mult) ``` wenzelm@23164 ` 200` wenzelm@23164 ` 201` ```lemma zmult_1_right: "z * (1::int) = z" ``` wenzelm@23164 ` 202` ```by (rule trans [OF zmult_commute zmult_1]) ``` wenzelm@23164 ` 203` wenzelm@23164 ` 204` wenzelm@23164 ` 205` ```text{*The integers form a @{text comm_ring_1}*} ``` wenzelm@23164 ` 206` ```instance int :: comm_ring_1 ``` wenzelm@23164 ` 207` ```proof ``` wenzelm@23164 ` 208` ``` fix i j k :: int ``` wenzelm@23164 ` 209` ``` show "(i + j) + k = i + (j + k)" by (simp add: zadd_assoc) ``` wenzelm@23164 ` 210` ``` show "i + j = j + i" by (simp add: zadd_commute) ``` wenzelm@23164 ` 211` ``` show "0 + i = i" by (rule zadd_0) ``` wenzelm@23164 ` 212` ``` show "- i + i = 0" by (rule zadd_zminus_inverse2) ``` wenzelm@23164 ` 213` ``` show "i - j = i + (-j)" by (simp add: diff_int_def) ``` wenzelm@23164 ` 214` ``` show "(i * j) * k = i * (j * k)" by (rule zmult_assoc) ``` wenzelm@23164 ` 215` ``` show "i * j = j * i" by (rule zmult_commute) ``` wenzelm@23164 ` 216` ``` show "1 * i = i" by (rule zmult_1) ``` wenzelm@23164 ` 217` ``` show "(i + j) * k = i * k + j * k" by (simp add: int_distrib) ``` huffman@23299 ` 218` ``` show "0 \ (1::int)" by (simp add: Zero_int_def One_int_def) ``` wenzelm@23164 ` 219` ```qed ``` wenzelm@23164 ` 220` huffman@23303 ` 221` ```abbreviation ``` huffman@23303 ` 222` ``` int_of_nat :: "nat \ int" ``` huffman@23303 ` 223` ```where ``` huffman@23303 ` 224` ``` "int_of_nat \ of_nat" ``` huffman@23303 ` 225` wenzelm@23164 ` 226` wenzelm@23164 ` 227` ```subsection{*The @{text "\"} Ordering*} ``` wenzelm@23164 ` 228` wenzelm@23164 ` 229` ```lemma le: ``` wenzelm@23164 ` 230` ``` "(Abs_Integ(intrel``{(x,y)}) \ Abs_Integ(intrel``{(u,v)})) = (x+v \ u+y)" ``` wenzelm@23164 ` 231` ```by (force simp add: le_int_def) ``` wenzelm@23164 ` 232` huffman@23299 ` 233` ```lemma less: ``` huffman@23299 ` 234` ``` "(Abs_Integ(intrel``{(x,y)}) < Abs_Integ(intrel``{(u,v)})) = (x+v < u+y)" ``` huffman@23299 ` 235` ```by (simp add: less_int_def le order_less_le) ``` huffman@23299 ` 236` wenzelm@23164 ` 237` ```lemma zle_refl: "w \ (w::int)" ``` wenzelm@23164 ` 238` ```by (cases w, simp add: le) ``` wenzelm@23164 ` 239` wenzelm@23164 ` 240` ```lemma zle_trans: "[| i \ j; j \ k |] ==> i \ (k::int)" ``` wenzelm@23164 ` 241` ```by (cases i, cases j, cases k, simp add: le) ``` wenzelm@23164 ` 242` wenzelm@23164 ` 243` ```lemma zle_anti_sym: "[| z \ w; w \ z |] ==> z = (w::int)" ``` wenzelm@23164 ` 244` ```by (cases w, cases z, simp add: le) ``` wenzelm@23164 ` 245` wenzelm@23164 ` 246` ```instance int :: order ``` wenzelm@23164 ` 247` ``` by intro_classes ``` wenzelm@23164 ` 248` ``` (assumption | ``` wenzelm@23164 ` 249` ``` rule zle_refl zle_trans zle_anti_sym less_int_def [THEN meta_eq_to_obj_eq])+ ``` wenzelm@23164 ` 250` wenzelm@23164 ` 251` ```lemma zle_linear: "(z::int) \ w \ w \ z" ``` wenzelm@23164 ` 252` ```by (cases z, cases w) (simp add: le linorder_linear) ``` wenzelm@23164 ` 253` wenzelm@23164 ` 254` ```instance int :: linorder ``` wenzelm@23164 ` 255` ``` by intro_classes (rule zle_linear) ``` wenzelm@23164 ` 256` wenzelm@23164 ` 257` ```lemmas zless_linear = linorder_less_linear [where 'a = int] ``` wenzelm@23164 ` 258` wenzelm@23164 ` 259` wenzelm@23164 ` 260` ```lemma int_0_less_1: "0 < (1::int)" ``` huffman@23299 ` 261` ```by (simp add: Zero_int_def One_int_def less) ``` wenzelm@23164 ` 262` wenzelm@23164 ` 263` ```lemma int_0_neq_1 [simp]: "0 \ (1::int)" ``` huffman@23299 ` 264` ```by (rule int_0_less_1 [THEN less_imp_neq]) ``` wenzelm@23164 ` 265` wenzelm@23164 ` 266` wenzelm@23164 ` 267` ```subsection{*Monotonicity results*} ``` wenzelm@23164 ` 268` huffman@23299 ` 269` ```instance int :: pordered_cancel_ab_semigroup_add ``` huffman@23299 ` 270` ```proof ``` huffman@23299 ` 271` ``` fix a b c :: int ``` huffman@23299 ` 272` ``` show "a \ b \ c + a \ c + b" ``` huffman@23299 ` 273` ``` by (cases a, cases b, cases c, simp add: le add) ``` huffman@23299 ` 274` ```qed ``` huffman@23299 ` 275` wenzelm@23164 ` 276` ```lemma zadd_left_mono: "i \ j ==> k + i \ k + (j::int)" ``` huffman@23299 ` 277` ```by (rule add_left_mono) ``` wenzelm@23164 ` 278` wenzelm@23164 ` 279` ```lemma zadd_strict_right_mono: "i < j ==> i + k < j + (k::int)" ``` huffman@23299 ` 280` ```by (rule add_strict_right_mono) ``` wenzelm@23164 ` 281` wenzelm@23164 ` 282` ```lemma zadd_zless_mono: "[| w'z |] ==> w' + z' < w + (z::int)" ``` huffman@23299 ` 283` ```by (rule add_less_le_mono) ``` wenzelm@23164 ` 284` wenzelm@23164 ` 285` wenzelm@23164 ` 286` ```subsection{*Strict Monotonicity of Multiplication*} ``` wenzelm@23164 ` 287` wenzelm@23164 ` 288` ```text{*strict, in 1st argument; proof is by induction on k>0*} ``` wenzelm@23164 ` 289` ```lemma zmult_zless_mono2_lemma: ``` huffman@23299 ` 290` ``` "(i::int) 0 of_nat k * i < of_nat k * j" ``` wenzelm@23164 ` 291` ```apply (induct "k", simp) ``` huffman@23299 ` 292` ```apply (simp add: left_distrib) ``` wenzelm@23164 ` 293` ```apply (case_tac "k=0") ``` huffman@23299 ` 294` ```apply (simp_all add: add_strict_mono) ``` wenzelm@23164 ` 295` ```done ``` wenzelm@23164 ` 296` huffman@23299 ` 297` ```lemma int_of_nat_def: "of_nat m = Abs_Integ (intrel `` {(m, 0)})" ``` huffman@23299 ` 298` ```by (induct m, simp_all add: Zero_int_def One_int_def add) ``` huffman@23299 ` 299` huffman@23299 ` 300` ```lemma zero_le_imp_eq_int: "(0::int) \ k ==> \n. k = of_nat n" ``` wenzelm@23164 ` 301` ```apply (cases k) ``` huffman@23299 ` 302` ```apply (auto simp add: le add int_of_nat_def Zero_int_def) ``` huffman@23299 ` 303` ```apply (rule_tac x="x-y" in exI, simp) ``` huffman@23299 ` 304` ```done ``` huffman@23299 ` 305` huffman@23299 ` 306` ```lemma zero_less_imp_eq_int: "(0::int) < k ==> \n>0. k = of_nat n" ``` huffman@23299 ` 307` ```apply (cases k) ``` huffman@23299 ` 308` ```apply (simp add: less int_of_nat_def Zero_int_def) ``` wenzelm@23164 ` 309` ```apply (rule_tac x="x-y" in exI, simp) ``` wenzelm@23164 ` 310` ```done ``` wenzelm@23164 ` 311` wenzelm@23164 ` 312` ```lemma zmult_zless_mono2: "[| i k*i < k*j" ``` huffman@23299 ` 313` ```apply (drule zero_less_imp_eq_int) ``` wenzelm@23164 ` 314` ```apply (auto simp add: zmult_zless_mono2_lemma) ``` wenzelm@23164 ` 315` ```done ``` wenzelm@23164 ` 316` wenzelm@23164 ` 317` ```instance int :: minus ``` wenzelm@23164 ` 318` ``` zabs_def: "\i\int\ \ if i < 0 then - i else i" .. ``` wenzelm@23164 ` 319` wenzelm@23164 ` 320` ```instance int :: distrib_lattice ``` wenzelm@23164 ` 321` ``` "inf \ min" ``` wenzelm@23164 ` 322` ``` "sup \ max" ``` wenzelm@23164 ` 323` ``` by intro_classes ``` wenzelm@23164 ` 324` ``` (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1) ``` wenzelm@23164 ` 325` huffman@23299 ` 326` ```text{*The integers form an ordered integral domain*} ``` wenzelm@23164 ` 327` ```instance int :: ordered_idom ``` wenzelm@23164 ` 328` ```proof ``` wenzelm@23164 ` 329` ``` fix i j k :: int ``` wenzelm@23164 ` 330` ``` show "i < j ==> 0 < k ==> k * i < k * j" by (rule zmult_zless_mono2) ``` wenzelm@23164 ` 331` ``` show "\i\ = (if i < 0 then -i else i)" by (simp only: zabs_def) ``` wenzelm@23164 ` 332` ```qed ``` wenzelm@23164 ` 333` wenzelm@23164 ` 334` ```lemma zless_imp_add1_zle: "w w + (1::int) \ z" ``` wenzelm@23164 ` 335` ```apply (cases w, cases z) ``` huffman@23299 ` 336` ```apply (simp add: less le add One_int_def) ``` wenzelm@23164 ` 337` ```done ``` wenzelm@23164 ` 338` huffman@23299 ` 339` huffman@23299 ` 340` ```subsection{*Magnitude of an Integer, as a Natural Number: @{term nat}*} ``` wenzelm@23164 ` 341` wenzelm@23164 ` 342` ```definition ``` wenzelm@23164 ` 343` ``` nat :: "int \ nat" ``` wenzelm@23164 ` 344` ```where ``` wenzelm@23164 ` 345` ``` [code func del]: "nat z = contents (\(x, y) \ Rep_Integ z. {x-y})" ``` wenzelm@23164 ` 346` wenzelm@23164 ` 347` ```lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y" ``` wenzelm@23164 ` 348` ```proof - ``` wenzelm@23164 ` 349` ``` have "(\(x,y). {x-y}) respects intrel" ``` wenzelm@23164 ` 350` ``` by (simp add: congruent_def) arith ``` wenzelm@23164 ` 351` ``` thus ?thesis ``` wenzelm@23164 ` 352` ``` by (simp add: nat_def UN_equiv_class [OF equiv_intrel]) ``` wenzelm@23164 ` 353` ```qed ``` wenzelm@23164 ` 354` huffman@23303 ` 355` ```lemma nat_int_of_nat [simp]: "nat (int_of_nat n) = n" ``` huffman@23303 ` 356` ```by (simp add: nat int_of_nat_def) ``` wenzelm@23164 ` 357` wenzelm@23164 ` 358` ```lemma nat_zero [simp]: "nat 0 = 0" ``` huffman@23303 ` 359` ```by (simp add: Zero_int_def nat) ``` wenzelm@23164 ` 360` huffman@23303 ` 361` ```lemma int_of_nat_nat_eq [simp]: "int_of_nat (nat z) = (if 0 \ z then z else 0)" ``` huffman@23303 ` 362` ```by (cases z, simp add: nat le int_of_nat_def Zero_int_def) ``` wenzelm@23164 ` 363` huffman@23303 ` 364` ```corollary nat_0_le': "0 \ z ==> int_of_nat (nat z) = z" ``` wenzelm@23164 ` 365` ```by simp ``` wenzelm@23164 ` 366` wenzelm@23164 ` 367` ```lemma nat_le_0 [simp]: "z \ 0 ==> nat z = 0" ``` huffman@23303 ` 368` ```by (cases z, simp add: nat le Zero_int_def) ``` wenzelm@23164 ` 369` wenzelm@23164 ` 370` ```lemma nat_le_eq_zle: "0 < w | 0 \ z ==> (nat w \ nat z) = (w\z)" ``` wenzelm@23164 ` 371` ```apply (cases w, cases z) ``` huffman@23303 ` 372` ```apply (simp add: nat le linorder_not_le [symmetric] Zero_int_def, arith) ``` wenzelm@23164 ` 373` ```done ``` wenzelm@23164 ` 374` wenzelm@23164 ` 375` ```text{*An alternative condition is @{term "0 \ w"} *} ``` wenzelm@23164 ` 376` ```corollary nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)" ``` wenzelm@23164 ` 377` ```by (simp add: nat_le_eq_zle linorder_not_le [symmetric]) ``` wenzelm@23164 ` 378` wenzelm@23164 ` 379` ```corollary nat_less_eq_zless: "0 \ w ==> (nat w < nat z) = (w z; !!m. z = int_of_nat m ==> P |] ==> P" ``` huffman@23303 ` 388` ```by (blast dest: nat_0_le' sym) ``` wenzelm@23164 ` 389` huffman@23303 ` 390` ```lemma nat_eq_iff': "(nat w = m) = (if 0 \ w then w = int_of_nat m else m=0)" ``` huffman@23303 ` 391` ```by (cases w, simp add: nat le int_of_nat_def Zero_int_def, arith) ``` wenzelm@23164 ` 392` huffman@23303 ` 393` ```corollary nat_eq_iff2': "(m = nat w) = (if 0 \ w then w = int_of_nat m else m=0)" ``` huffman@23303 ` 394` ```by (simp only: eq_commute [of m] nat_eq_iff') ``` wenzelm@23164 ` 395` huffman@23303 ` 396` ```lemma nat_less_iff': "0 \ w ==> (nat w < m) = (w < int_of_nat m)" ``` wenzelm@23164 ` 397` ```apply (cases w) ``` huffman@23303 ` 398` ```apply (simp add: nat le int_of_nat_def Zero_int_def linorder_not_le [symmetric], arith) ``` wenzelm@23164 ` 399` ```done ``` wenzelm@23164 ` 400` huffman@23303 ` 401` ```lemma int_of_nat_eq_iff: "(int_of_nat m = z) = (m = nat z & 0 \ z)" ``` huffman@23303 ` 402` ```by (auto simp add: nat_eq_iff2') ``` wenzelm@23164 ` 403` wenzelm@23164 ` 404` ```lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)" ``` wenzelm@23164 ` 405` ```by (insert zless_nat_conj [of 0], auto) ``` wenzelm@23164 ` 406` wenzelm@23164 ` 407` ```lemma nat_add_distrib: ``` wenzelm@23164 ` 408` ``` "[| (0::int) \ z; 0 \ z' |] ==> nat (z+z') = nat z + nat z'" ``` huffman@23303 ` 409` ```by (cases z, cases z', simp add: nat add le Zero_int_def) ``` wenzelm@23164 ` 410` wenzelm@23164 ` 411` ```lemma nat_diff_distrib: ``` wenzelm@23164 ` 412` ``` "[| (0::int) \ z'; z' \ z |] ==> nat (z-z') = nat z - nat z'" ``` wenzelm@23164 ` 413` ```by (cases z, cases z', ``` huffman@23303 ` 414` ``` simp add: nat add minus diff_minus le Zero_int_def) ``` wenzelm@23164 ` 415` huffman@23303 ` 416` ```lemma nat_zminus_int_of_nat [simp]: "nat (- (int_of_nat n)) = 0" ``` huffman@23303 ` 417` ```by (simp add: int_of_nat_def minus nat Zero_int_def) ``` wenzelm@23164 ` 418` huffman@23307 ` 419` ```lemma zless_nat_eq_int_zless': "(m < nat z) = (int_of_nat m < z)" ``` huffman@23303 ` 420` ```by (cases z, simp add: nat less int_of_nat_def, arith) ``` wenzelm@23164 ` 421` wenzelm@23164 ` 422` wenzelm@23164 ` 423` ```subsection{*Lemmas about the Function @{term int} and Orderings*} ``` wenzelm@23164 ` 424` huffman@23303 ` 425` ```lemma negative_zless_0': "- (int_of_nat (Suc n)) < 0" ``` huffman@23303 ` 426` ```by (simp add: order_less_le del: of_nat_Suc) ``` wenzelm@23164 ` 427` huffman@23303 ` 428` ```lemma negative_zless' [iff]: "- (int_of_nat (Suc n)) < int_of_nat m" ``` huffman@23303 ` 429` ```by (rule negative_zless_0' [THEN order_less_le_trans], simp) ``` wenzelm@23164 ` 430` huffman@23303 ` 431` ```lemma negative_zle_0': "- int_of_nat n \ 0" ``` wenzelm@23164 ` 432` ```by (simp add: minus_le_iff) ``` wenzelm@23164 ` 433` huffman@23303 ` 434` ```lemma negative_zle' [iff]: "- int_of_nat n \ int_of_nat m" ``` huffman@23303 ` 435` ```by (rule order_trans [OF negative_zle_0' of_nat_0_le_iff]) ``` wenzelm@23164 ` 436` huffman@23303 ` 437` ```lemma not_zle_0_negative' [simp]: "~ (0 \ - (int_of_nat (Suc n)))" ``` huffman@23303 ` 438` ```by (subst le_minus_iff, simp del: of_nat_Suc) ``` wenzelm@23164 ` 439` huffman@23303 ` 440` ```lemma int_zle_neg': "(int_of_nat n \ - int_of_nat m) = (n = 0 & m = 0)" ``` huffman@23303 ` 441` ```by (simp add: int_of_nat_def le minus Zero_int_def) ``` wenzelm@23164 ` 442` huffman@23303 ` 443` ```lemma not_int_zless_negative' [simp]: "~ (int_of_nat n < - int_of_nat m)" ``` wenzelm@23164 ` 444` ```by (simp add: linorder_not_less) ``` wenzelm@23164 ` 445` huffman@23303 ` 446` ```lemma negative_eq_positive' [simp]: ``` huffman@23303 ` 447` ``` "(- int_of_nat n = int_of_nat m) = (n = 0 & m = 0)" ``` huffman@23303 ` 448` ```by (force simp add: order_eq_iff [of "- int_of_nat n"] int_zle_neg') ``` wenzelm@23164 ` 449` huffman@23308 ` 450` ```lemma zle_iff_zadd': "(w \ z) = (\n. z = w + int_of_nat n)" ``` huffman@23303 ` 451` ```proof (cases w, cases z, simp add: le add int_of_nat_def) ``` wenzelm@23164 ` 452` ``` fix a b c d ``` wenzelm@23164 ` 453` ``` assume "w = Abs_Integ (intrel `` {(a,b)})" "z = Abs_Integ (intrel `` {(c,d)})" ``` wenzelm@23164 ` 454` ``` show "(a+d \ c+b) = (\n. c+b = a+n+d)" ``` wenzelm@23164 ` 455` ``` proof ``` wenzelm@23164 ` 456` ``` assume "a + d \ c + b" ``` wenzelm@23164 ` 457` ``` thus "\n. c + b = a + n + d" ``` wenzelm@23164 ` 458` ``` by (auto intro!: exI [where x="c+b - (a+d)"]) ``` wenzelm@23164 ` 459` ``` next ``` wenzelm@23164 ` 460` ``` assume "\n. c + b = a + n + d" ``` wenzelm@23164 ` 461` ``` then obtain n where "c + b = a + n + d" .. ``` wenzelm@23164 ` 462` ``` thus "a + d \ c + b" by arith ``` wenzelm@23164 ` 463` ``` qed ``` wenzelm@23164 ` 464` ```qed ``` wenzelm@23164 ` 465` huffman@23303 ` 466` ```lemma abs_of_nat [simp]: "\of_nat n::'a::ordered_idom\ = of_nat n" ``` huffman@23303 ` 467` ```by (rule of_nat_0_le_iff [THEN abs_of_nonneg]) (* belongs in Nat.thy *) ``` wenzelm@23164 ` 468` wenzelm@23164 ` 469` ```text{*This version is proved for all ordered rings, not just integers! ``` wenzelm@23164 ` 470` ``` It is proved here because attribute @{text arith_split} is not available ``` wenzelm@23164 ` 471` ``` in theory @{text Ring_and_Field}. ``` wenzelm@23164 ` 472` ``` But is it really better than just rewriting with @{text abs_if}?*} ``` wenzelm@23164 ` 473` ```lemma abs_split [arith_split]: ``` wenzelm@23164 ` 474` ``` "P(abs(a::'a::ordered_idom)) = ((0 \ a --> P a) & (a < 0 --> P(-a)))" ``` wenzelm@23164 ` 475` ```by (force dest: order_less_le_trans simp add: abs_if linorder_not_less) ``` wenzelm@23164 ` 476` wenzelm@23164 ` 477` wenzelm@23164 ` 478` ```subsection {* Constants @{term neg} and @{term iszero} *} ``` wenzelm@23164 ` 479` wenzelm@23164 ` 480` ```definition ``` wenzelm@23164 ` 481` ``` neg :: "'a\ordered_idom \ bool" ``` wenzelm@23164 ` 482` ```where ``` wenzelm@23164 ` 483` ``` [code inline]: "neg Z \ Z < 0" ``` wenzelm@23164 ` 484` wenzelm@23164 ` 485` ```definition (*for simplifying equalities*) ``` huffman@23276 ` 486` ``` iszero :: "'a\semiring_1 \ bool" ``` wenzelm@23164 ` 487` ```where ``` wenzelm@23164 ` 488` ``` "iszero z \ z = 0" ``` wenzelm@23164 ` 489` huffman@23303 ` 490` ```lemma not_neg_int_of_nat [simp]: "~ neg (int_of_nat n)" ``` wenzelm@23164 ` 491` ```by (simp add: neg_def) ``` wenzelm@23164 ` 492` huffman@23303 ` 493` ```lemma neg_zminus_int_of_nat [simp]: "neg (- (int_of_nat (Suc n)))" ``` huffman@23303 ` 494` ```by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc) ``` wenzelm@23164 ` 495` wenzelm@23164 ` 496` ```lemmas neg_eq_less_0 = neg_def ``` wenzelm@23164 ` 497` wenzelm@23164 ` 498` ```lemma not_neg_eq_ge_0: "(~neg x) = (0 \ x)" ``` wenzelm@23164 ` 499` ```by (simp add: neg_def linorder_not_less) ``` wenzelm@23164 ` 500` wenzelm@23164 ` 501` wenzelm@23164 ` 502` ```subsection{*To simplify inequalities when Numeral1 can get simplified to 1*} ``` wenzelm@23164 ` 503` wenzelm@23164 ` 504` ```lemma not_neg_0: "~ neg 0" ``` wenzelm@23164 ` 505` ```by (simp add: One_int_def neg_def) ``` wenzelm@23164 ` 506` wenzelm@23164 ` 507` ```lemma not_neg_1: "~ neg 1" ``` wenzelm@23164 ` 508` ```by (simp add: neg_def linorder_not_less zero_le_one) ``` wenzelm@23164 ` 509` wenzelm@23164 ` 510` ```lemma iszero_0: "iszero 0" ``` wenzelm@23164 ` 511` ```by (simp add: iszero_def) ``` wenzelm@23164 ` 512` wenzelm@23164 ` 513` ```lemma not_iszero_1: "~ iszero 1" ``` wenzelm@23164 ` 514` ```by (simp add: iszero_def eq_commute) ``` wenzelm@23164 ` 515` wenzelm@23164 ` 516` ```lemma neg_nat: "neg z ==> nat z = 0" ``` wenzelm@23164 ` 517` ```by (simp add: neg_def order_less_imp_le) ``` wenzelm@23164 ` 518` huffman@23303 ` 519` ```lemma not_neg_nat': "~ neg z ==> int_of_nat (nat z) = z" ``` wenzelm@23164 ` 520` ```by (simp add: linorder_not_less neg_def) ``` wenzelm@23164 ` 521` wenzelm@23164 ` 522` wenzelm@23164 ` 523` ```subsection{*The Set of Natural Numbers*} ``` wenzelm@23164 ` 524` wenzelm@23164 ` 525` ```constdefs ``` huffman@23276 ` 526` ``` Nats :: "'a::semiring_1 set" ``` wenzelm@23164 ` 527` ``` "Nats == range of_nat" ``` wenzelm@23164 ` 528` wenzelm@23164 ` 529` ```notation (xsymbols) ``` wenzelm@23164 ` 530` ``` Nats ("\") ``` wenzelm@23164 ` 531` wenzelm@23164 ` 532` ```lemma of_nat_in_Nats [simp]: "of_nat n \ Nats" ``` wenzelm@23164 ` 533` ```by (simp add: Nats_def) ``` wenzelm@23164 ` 534` wenzelm@23164 ` 535` ```lemma Nats_0 [simp]: "0 \ Nats" ``` wenzelm@23164 ` 536` ```apply (simp add: Nats_def) ``` wenzelm@23164 ` 537` ```apply (rule range_eqI) ``` wenzelm@23164 ` 538` ```apply (rule of_nat_0 [symmetric]) ``` wenzelm@23164 ` 539` ```done ``` wenzelm@23164 ` 540` wenzelm@23164 ` 541` ```lemma Nats_1 [simp]: "1 \ Nats" ``` wenzelm@23164 ` 542` ```apply (simp add: Nats_def) ``` wenzelm@23164 ` 543` ```apply (rule range_eqI) ``` wenzelm@23164 ` 544` ```apply (rule of_nat_1 [symmetric]) ``` wenzelm@23164 ` 545` ```done ``` wenzelm@23164 ` 546` wenzelm@23164 ` 547` ```lemma Nats_add [simp]: "[|a \ Nats; b \ Nats|] ==> a+b \ Nats" ``` wenzelm@23164 ` 548` ```apply (auto simp add: Nats_def) ``` wenzelm@23164 ` 549` ```apply (rule range_eqI) ``` wenzelm@23164 ` 550` ```apply (rule of_nat_add [symmetric]) ``` wenzelm@23164 ` 551` ```done ``` wenzelm@23164 ` 552` wenzelm@23164 ` 553` ```lemma Nats_mult [simp]: "[|a \ Nats; b \ Nats|] ==> a*b \ Nats" ``` wenzelm@23164 ` 554` ```apply (auto simp add: Nats_def) ``` wenzelm@23164 ` 555` ```apply (rule range_eqI) ``` wenzelm@23164 ` 556` ```apply (rule of_nat_mult [symmetric]) ``` wenzelm@23164 ` 557` ```done ``` wenzelm@23164 ` 558` wenzelm@23164 ` 559` ```lemma of_nat_eq_id [simp]: "of_nat = (id :: nat => nat)" ``` wenzelm@23164 ` 560` ```proof ``` wenzelm@23164 ` 561` ``` fix n ``` wenzelm@23164 ` 562` ``` show "of_nat n = id n" by (induct n, simp_all) ``` huffman@23303 ` 563` ```qed (* belongs in Nat.thy *) ``` wenzelm@23164 ` 564` wenzelm@23164 ` 565` wenzelm@23164 ` 566` ```subsection{*Embedding of the Integers into any @{text ring_1}: ``` wenzelm@23164 ` 567` ```@{term of_int}*} ``` wenzelm@23164 ` 568` wenzelm@23164 ` 569` ```constdefs ``` wenzelm@23164 ` 570` ``` of_int :: "int => 'a::ring_1" ``` wenzelm@23164 ` 571` ``` "of_int z == contents (\(i,j) \ Rep_Integ z. { of_nat i - of_nat j })" ``` wenzelm@23164 ` 572` wenzelm@23164 ` 573` wenzelm@23164 ` 574` ```lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j" ``` wenzelm@23164 ` 575` ```proof - ``` wenzelm@23164 ` 576` ``` have "(\(i,j). { of_nat i - (of_nat j :: 'a) }) respects intrel" ``` wenzelm@23164 ` 577` ``` by (simp add: congruent_def compare_rls of_nat_add [symmetric] ``` wenzelm@23164 ` 578` ``` del: of_nat_add) ``` wenzelm@23164 ` 579` ``` thus ?thesis ``` wenzelm@23164 ` 580` ``` by (simp add: of_int_def UN_equiv_class [OF equiv_intrel]) ``` wenzelm@23164 ` 581` ```qed ``` wenzelm@23164 ` 582` wenzelm@23164 ` 583` ```lemma of_int_0 [simp]: "of_int 0 = 0" ``` huffman@23303 ` 584` ```by (simp add: of_int Zero_int_def) ``` wenzelm@23164 ` 585` wenzelm@23164 ` 586` ```lemma of_int_1 [simp]: "of_int 1 = 1" ``` huffman@23303 ` 587` ```by (simp add: of_int One_int_def) ``` wenzelm@23164 ` 588` wenzelm@23164 ` 589` ```lemma of_int_add [simp]: "of_int (w+z) = of_int w + of_int z" ``` wenzelm@23164 ` 590` ```by (cases w, cases z, simp add: compare_rls of_int add) ``` wenzelm@23164 ` 591` wenzelm@23164 ` 592` ```lemma of_int_minus [simp]: "of_int (-z) = - (of_int z)" ``` wenzelm@23164 ` 593` ```by (cases z, simp add: compare_rls of_int minus) ``` wenzelm@23164 ` 594` wenzelm@23164 ` 595` ```lemma of_int_diff [simp]: "of_int (w-z) = of_int w - of_int z" ``` wenzelm@23164 ` 596` ```by (simp add: diff_minus) ``` wenzelm@23164 ` 597` wenzelm@23164 ` 598` ```lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z" ``` wenzelm@23164 ` 599` ```apply (cases w, cases z) ``` wenzelm@23164 ` 600` ```apply (simp add: compare_rls of_int left_diff_distrib right_diff_distrib ``` wenzelm@23164 ` 601` ``` mult add_ac) ``` wenzelm@23164 ` 602` ```done ``` wenzelm@23164 ` 603` wenzelm@23164 ` 604` ```lemma of_int_le_iff [simp]: ``` wenzelm@23164 ` 605` ``` "(of_int w \ (of_int z::'a::ordered_idom)) = (w \ z)" ``` wenzelm@23164 ` 606` ```apply (cases w) ``` wenzelm@23164 ` 607` ```apply (cases z) ``` wenzelm@23164 ` 608` ```apply (simp add: compare_rls of_int le diff_int_def add minus ``` wenzelm@23164 ` 609` ``` of_nat_add [symmetric] del: of_nat_add) ``` wenzelm@23164 ` 610` ```done ``` wenzelm@23164 ` 611` wenzelm@23164 ` 612` ```text{*Special cases where either operand is zero*} ``` wenzelm@23164 ` 613` ```lemmas of_int_0_le_iff [simp] = of_int_le_iff [of 0, simplified] ``` wenzelm@23164 ` 614` ```lemmas of_int_le_0_iff [simp] = of_int_le_iff [of _ 0, simplified] ``` wenzelm@23164 ` 615` wenzelm@23164 ` 616` wenzelm@23164 ` 617` ```lemma of_int_less_iff [simp]: ``` wenzelm@23164 ` 618` ``` "(of_int w < (of_int z::'a::ordered_idom)) = (w < z)" ``` wenzelm@23164 ` 619` ```by (simp add: linorder_not_le [symmetric]) ``` wenzelm@23164 ` 620` wenzelm@23164 ` 621` ```text{*Special cases where either operand is zero*} ``` wenzelm@23164 ` 622` ```lemmas of_int_0_less_iff [simp] = of_int_less_iff [of 0, simplified] ``` wenzelm@23164 ` 623` ```lemmas of_int_less_0_iff [simp] = of_int_less_iff [of _ 0, simplified] ``` wenzelm@23164 ` 624` wenzelm@23164 ` 625` ```text{*Class for unital rings with characteristic zero. ``` wenzelm@23164 ` 626` ``` Includes non-ordered rings like the complex numbers.*} ``` huffman@23282 ` 627` ```axclass ring_char_0 < ring_1, semiring_char_0 ``` wenzelm@23164 ` 628` wenzelm@23164 ` 629` ```lemma of_int_eq_iff [simp]: ``` wenzelm@23164 ` 630` ``` "(of_int w = (of_int z::'a::ring_char_0)) = (w = z)" ``` huffman@23282 ` 631` ```apply (cases w, cases z, simp add: of_int) ``` huffman@23282 ` 632` ```apply (simp only: diff_eq_eq diff_add_eq eq_diff_eq) ``` huffman@23282 ` 633` ```apply (simp only: of_nat_add [symmetric] of_nat_eq_iff) ``` huffman@23282 ` 634` ```done ``` wenzelm@23164 ` 635` wenzelm@23164 ` 636` ```text{*Every @{text ordered_idom} has characteristic zero.*} ``` huffman@23282 ` 637` ```instance ordered_idom < ring_char_0 .. ``` wenzelm@23164 ` 638` wenzelm@23164 ` 639` ```text{*Special cases where either operand is zero*} ``` wenzelm@23164 ` 640` ```lemmas of_int_0_eq_iff [simp] = of_int_eq_iff [of 0, simplified] ``` wenzelm@23164 ` 641` ```lemmas of_int_eq_0_iff [simp] = of_int_eq_iff [of _ 0, simplified] ``` wenzelm@23164 ` 642` wenzelm@23164 ` 643` ```lemma of_int_eq_id [simp]: "of_int = (id :: int => int)" ``` wenzelm@23164 ` 644` ```proof ``` wenzelm@23164 ` 645` ``` fix z ``` huffman@23299 ` 646` ``` show "of_int z = id z" ``` wenzelm@23164 ` 647` ``` by (cases z) ``` huffman@23303 ` 648` ``` (simp add: of_int add minus int_of_nat_def diff_minus) ``` wenzelm@23164 ` 649` ```qed ``` wenzelm@23164 ` 650` wenzelm@23164 ` 651` wenzelm@23164 ` 652` ```subsection{*The Set of Integers*} ``` wenzelm@23164 ` 653` wenzelm@23164 ` 654` ```constdefs ``` wenzelm@23164 ` 655` ``` Ints :: "'a::ring_1 set" ``` wenzelm@23164 ` 656` ``` "Ints == range of_int" ``` wenzelm@23164 ` 657` wenzelm@23164 ` 658` ```notation (xsymbols) ``` wenzelm@23164 ` 659` ``` Ints ("\") ``` wenzelm@23164 ` 660` wenzelm@23164 ` 661` ```lemma Ints_0 [simp]: "0 \ Ints" ``` wenzelm@23164 ` 662` ```apply (simp add: Ints_def) ``` wenzelm@23164 ` 663` ```apply (rule range_eqI) ``` wenzelm@23164 ` 664` ```apply (rule of_int_0 [symmetric]) ``` wenzelm@23164 ` 665` ```done ``` wenzelm@23164 ` 666` wenzelm@23164 ` 667` ```lemma Ints_1 [simp]: "1 \ Ints" ``` wenzelm@23164 ` 668` ```apply (simp add: Ints_def) ``` wenzelm@23164 ` 669` ```apply (rule range_eqI) ``` wenzelm@23164 ` 670` ```apply (rule of_int_1 [symmetric]) ``` wenzelm@23164 ` 671` ```done ``` wenzelm@23164 ` 672` wenzelm@23164 ` 673` ```lemma Ints_add [simp]: "[|a \ Ints; b \ Ints|] ==> a+b \ Ints" ``` wenzelm@23164 ` 674` ```apply (auto simp add: Ints_def) ``` wenzelm@23164 ` 675` ```apply (rule range_eqI) ``` wenzelm@23164 ` 676` ```apply (rule of_int_add [symmetric]) ``` wenzelm@23164 ` 677` ```done ``` wenzelm@23164 ` 678` wenzelm@23164 ` 679` ```lemma Ints_minus [simp]: "a \ Ints ==> -a \ Ints" ``` wenzelm@23164 ` 680` ```apply (auto simp add: Ints_def) ``` wenzelm@23164 ` 681` ```apply (rule range_eqI) ``` wenzelm@23164 ` 682` ```apply (rule of_int_minus [symmetric]) ``` wenzelm@23164 ` 683` ```done ``` wenzelm@23164 ` 684` wenzelm@23164 ` 685` ```lemma Ints_diff [simp]: "[|a \ Ints; b \ Ints|] ==> a-b \ Ints" ``` wenzelm@23164 ` 686` ```apply (auto simp add: Ints_def) ``` wenzelm@23164 ` 687` ```apply (rule range_eqI) ``` wenzelm@23164 ` 688` ```apply (rule of_int_diff [symmetric]) ``` wenzelm@23164 ` 689` ```done ``` wenzelm@23164 ` 690` wenzelm@23164 ` 691` ```lemma Ints_mult [simp]: "[|a \ Ints; b \ Ints|] ==> a*b \ Ints" ``` wenzelm@23164 ` 692` ```apply (auto simp add: Ints_def) ``` wenzelm@23164 ` 693` ```apply (rule range_eqI) ``` wenzelm@23164 ` 694` ```apply (rule of_int_mult [symmetric]) ``` wenzelm@23164 ` 695` ```done ``` wenzelm@23164 ` 696` wenzelm@23164 ` 697` ```text{*Collapse nested embeddings*} ``` wenzelm@23164 ` 698` ```lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n" ``` wenzelm@23164 ` 699` ```by (induct n, auto) ``` wenzelm@23164 ` 700` wenzelm@23164 ` 701` ```lemma Ints_cases [cases set: Ints]: ``` wenzelm@23164 ` 702` ``` assumes "q \ \" ``` wenzelm@23164 ` 703` ``` obtains (of_int) z where "q = of_int z" ``` wenzelm@23164 ` 704` ``` unfolding Ints_def ``` wenzelm@23164 ` 705` ```proof - ``` wenzelm@23164 ` 706` ``` from `q \ \` have "q \ range of_int" unfolding Ints_def . ``` wenzelm@23164 ` 707` ``` then obtain z where "q = of_int z" .. ``` wenzelm@23164 ` 708` ``` then show thesis .. ``` wenzelm@23164 ` 709` ```qed ``` wenzelm@23164 ` 710` wenzelm@23164 ` 711` ```lemma Ints_induct [case_names of_int, induct set: Ints]: ``` wenzelm@23164 ` 712` ``` "q \ \ ==> (!!z. P (of_int z)) ==> P q" ``` wenzelm@23164 ` 713` ``` by (rule Ints_cases) auto ``` wenzelm@23164 ` 714` wenzelm@23164 ` 715` wenzelm@23164 ` 716` ```(* int (Suc n) = 1 + int n *) ``` wenzelm@23164 ` 717` wenzelm@23164 ` 718` wenzelm@23164 ` 719` wenzelm@23164 ` 720` ```subsection{*More Properties of @{term setsum} and @{term setprod}*} ``` wenzelm@23164 ` 721` wenzelm@23164 ` 722` ```text{*By Jeremy Avigad*} ``` wenzelm@23164 ` 723` wenzelm@23164 ` 724` wenzelm@23164 ` 725` ```lemma of_nat_setsum: "of_nat (setsum f A) = (\x\A. of_nat(f x))" ``` wenzelm@23164 ` 726` ``` apply (cases "finite A") ``` wenzelm@23164 ` 727` ``` apply (erule finite_induct, auto) ``` wenzelm@23164 ` 728` ``` done ``` wenzelm@23164 ` 729` wenzelm@23164 ` 730` ```lemma of_int_setsum: "of_int (setsum f A) = (\x\A. of_int(f x))" ``` wenzelm@23164 ` 731` ``` apply (cases "finite A") ``` wenzelm@23164 ` 732` ``` apply (erule finite_induct, auto) ``` wenzelm@23164 ` 733` ``` done ``` wenzelm@23164 ` 734` wenzelm@23164 ` 735` ```lemma of_nat_setprod: "of_nat (setprod f A) = (\x\A. of_nat(f x))" ``` wenzelm@23164 ` 736` ``` apply (cases "finite A") ``` wenzelm@23164 ` 737` ``` apply (erule finite_induct, auto) ``` wenzelm@23164 ` 738` ``` done ``` wenzelm@23164 ` 739` wenzelm@23164 ` 740` ```lemma of_int_setprod: "of_int (setprod f A) = (\x\A. of_int(f x))" ``` wenzelm@23164 ` 741` ``` apply (cases "finite A") ``` wenzelm@23164 ` 742` ``` apply (erule finite_induct, auto) ``` wenzelm@23164 ` 743` ``` done ``` wenzelm@23164 ` 744` wenzelm@23164 ` 745` ```lemma setprod_nonzero_nat: ``` wenzelm@23164 ` 746` ``` "finite A ==> (\x \ A. f x \ (0::nat)) ==> setprod f A \ 0" ``` wenzelm@23164 ` 747` ``` by (rule setprod_nonzero, auto) ``` wenzelm@23164 ` 748` wenzelm@23164 ` 749` ```lemma setprod_zero_eq_nat: ``` wenzelm@23164 ` 750` ``` "finite A ==> (setprod f A = (0::nat)) = (\x \ A. f x = 0)" ``` wenzelm@23164 ` 751` ``` by (rule setprod_zero_eq, auto) ``` wenzelm@23164 ` 752` wenzelm@23164 ` 753` ```lemma setprod_nonzero_int: ``` wenzelm@23164 ` 754` ``` "finite A ==> (\x \ A. f x \ (0::int)) ==> setprod f A \ 0" ``` wenzelm@23164 ` 755` ``` by (rule setprod_nonzero, auto) ``` wenzelm@23164 ` 756` wenzelm@23164 ` 757` ```lemma setprod_zero_eq_int: ``` wenzelm@23164 ` 758` ``` "finite A ==> (setprod f A = (0::int)) = (\x \ A. f x = 0)" ``` wenzelm@23164 ` 759` ``` by (rule setprod_zero_eq, auto) ``` wenzelm@23164 ` 760` wenzelm@23164 ` 761` wenzelm@23164 ` 762` ```subsection {* Further properties *} ``` wenzelm@23164 ` 763` wenzelm@23164 ` 764` ```text{*Now we replace the case analysis rule by a more conventional one: ``` wenzelm@23164 ` 765` ```whether an integer is negative or not.*} ``` wenzelm@23164 ` 766` huffman@23303 ` 767` ```lemma zless_iff_Suc_zadd': ``` huffman@23303 ` 768` ``` "(w < z) = (\n. z = w + int_of_nat (Suc n))" ``` huffman@23303 ` 769` ```apply (cases z, cases w) ``` huffman@23303 ` 770` ```apply (auto simp add: le add int_of_nat_def linorder_not_le [symmetric]) ``` huffman@23303 ` 771` ```apply (rename_tac a b c d) ``` huffman@23303 ` 772` ```apply (rule_tac x="a+d - Suc(c+b)" in exI) ``` huffman@23303 ` 773` ```apply arith ``` huffman@23303 ` 774` ```done ``` huffman@23303 ` 775` huffman@23303 ` 776` ```lemma negD': "x<0 ==> \n. x = - (int_of_nat (Suc n))" ``` huffman@23303 ` 777` ```apply (cases x) ``` huffman@23303 ` 778` ```apply (auto simp add: le minus Zero_int_def int_of_nat_def order_less_le) ``` huffman@23303 ` 779` ```apply (rule_tac x="y - Suc x" in exI, arith) ``` huffman@23303 ` 780` ```done ``` huffman@23303 ` 781` huffman@23308 ` 782` ```theorem int_cases' [cases type: int, case_names nonneg neg]: ``` huffman@23303 ` 783` ``` "[|!! n. z = int_of_nat n ==> P; !! n. z = - (int_of_nat (Suc n)) ==> P |] ==> P" ``` huffman@23303 ` 784` ```apply (cases "z < 0", blast dest!: negD') ``` huffman@23303 ` 785` ```apply (simp add: linorder_not_less del: of_nat_Suc) ``` huffman@23303 ` 786` ```apply (blast dest: nat_0_le' [THEN sym]) ``` huffman@23303 ` 787` ```done ``` huffman@23303 ` 788` huffman@23308 ` 789` ```theorem int_induct' [induct type: int, case_names nonneg neg]: ``` huffman@23303 ` 790` ``` "[|!! n. P (int_of_nat n); !!n. P (- (int_of_nat (Suc n))) |] ==> P z" ``` huffman@23303 ` 791` ``` by (cases z rule: int_cases') auto ``` huffman@23303 ` 792` huffman@23303 ` 793` ```text{*Contributed by Brian Huffman*} ``` huffman@23303 ` 794` ```theorem int_diff_cases' [case_names diff]: ``` huffman@23303 ` 795` ```assumes prem: "!!m n. z = int_of_nat m - int_of_nat n ==> P" shows "P" ``` huffman@23303 ` 796` ```apply (cases z rule: eq_Abs_Integ) ``` huffman@23303 ` 797` ```apply (rule_tac m=x and n=y in prem) ``` huffman@23303 ` 798` ```apply (simp add: int_of_nat_def diff_def minus add) ``` huffman@23303 ` 799` ```done ``` huffman@23303 ` 800` huffman@23303 ` 801` ```lemma of_nat_nat: "0 \ z ==> of_nat (nat z) = of_int z" ``` huffman@23308 ` 802` ```by (cases z rule: eq_Abs_Integ, simp add: nat le of_int Zero_int_def) ``` huffman@23303 ` 803` huffman@23303 ` 804` ```lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq] ``` huffman@23303 ` 805` huffman@23303 ` 806` huffman@23303 ` 807` ```subsection{*@{term int}: Embedding the Naturals into the Integers*} ``` huffman@23303 ` 808` huffman@23303 ` 809` ```definition ``` huffman@23303 ` 810` ``` int :: "nat \ int" ``` huffman@23303 ` 811` ```where ``` huffman@23303 ` 812` ``` [code func del]: "int m = Abs_Integ (intrel `` {(m, 0)})" ``` huffman@23303 ` 813` huffman@23308 ` 814` ```text{*Agreement with the specific embedding for the integers*} ``` huffman@23308 ` 815` ```lemma int_eq_of_nat: "int = (of_nat :: nat => int)" ``` huffman@23308 ` 816` ```by (simp add: expand_fun_eq int_of_nat_def int_def) ``` huffman@23308 ` 817` huffman@23303 ` 818` ```lemma inj_int: "inj int" ``` huffman@23303 ` 819` ```by (simp add: inj_on_def int_def) ``` huffman@23303 ` 820` huffman@23303 ` 821` ```lemma int_int_eq [iff]: "(int m = int n) = (m = n)" ``` huffman@23308 ` 822` ```unfolding int_eq_of_nat by (rule of_nat_eq_iff) ``` huffman@23303 ` 823` huffman@23303 ` 824` ```lemma zadd_int: "(int m) + (int n) = int (m + n)" ``` huffman@23308 ` 825` ```unfolding int_eq_of_nat by (rule of_nat_add [symmetric]) ``` huffman@23303 ` 826` huffman@23303 ` 827` ```lemma zadd_int_left: "(int m) + (int n + z) = int (m + n) + z" ``` huffman@23308 ` 828` ```unfolding int_eq_of_nat by simp ``` huffman@23303 ` 829` huffman@23303 ` 830` ```lemma int_mult: "int (m * n) = (int m) * (int n)" ``` huffman@23308 ` 831` ```unfolding int_eq_of_nat by (rule of_nat_mult) ``` huffman@23303 ` 832` huffman@23303 ` 833` ```text{*Compatibility binding*} ``` huffman@23303 ` 834` ```lemmas zmult_int = int_mult [symmetric] ``` huffman@23303 ` 835` huffman@23303 ` 836` ```lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)" ``` huffman@23308 ` 837` ```unfolding int_eq_of_nat by (rule of_nat_eq_0_iff) ``` huffman@23303 ` 838` huffman@23303 ` 839` ```lemma zless_int [simp]: "(int m < int n) = (m int n) = (m\n)" ``` huffman@23308 ` 849` ```unfolding int_eq_of_nat by (rule of_nat_le_iff) ``` huffman@23303 ` 850` huffman@23303 ` 851` ```lemma zero_zle_int [simp]: "(0 \ int n)" ``` huffman@23308 ` 852` ```unfolding int_eq_of_nat by (rule of_nat_0_le_iff) ``` huffman@23303 ` 853` huffman@23303 ` 854` ```lemma int_le_0_conv [simp]: "(int n \ 0) = (n = 0)" ``` huffman@23308 ` 855` ```unfolding int_eq_of_nat by (rule of_nat_le_0_iff) ``` huffman@23303 ` 856` huffman@23303 ` 857` ```lemma int_0 [simp]: "int 0 = (0::int)" ``` huffman@23308 ` 858` ```unfolding int_eq_of_nat by (rule of_nat_0) ``` huffman@23303 ` 859` huffman@23303 ` 860` ```lemma int_1 [simp]: "int 1 = 1" ``` huffman@23308 ` 861` ```unfolding int_eq_of_nat by (rule of_nat_1) ``` huffman@23303 ` 862` huffman@23303 ` 863` ```lemma int_Suc0_eq_1: "int (Suc 0) = 1" ``` huffman@23308 ` 864` ```unfolding int_eq_of_nat by simp ``` huffman@23303 ` 865` huffman@23303 ` 866` ```lemma int_Suc: "int (Suc m) = 1 + (int m)" ``` huffman@23308 ` 867` ```unfolding int_eq_of_nat by simp ``` huffman@23303 ` 868` huffman@23303 ` 869` ```lemma nat_int [simp]: "nat(int n) = n" ``` huffman@23308 ` 870` ```unfolding int_eq_of_nat by (rule nat_int_of_nat) ``` huffman@23303 ` 871` huffman@23303 ` 872` ```lemma int_nat_eq [simp]: "int (nat z) = (if 0 \ z then z else 0)" ``` huffman@23308 ` 873` ```unfolding int_eq_of_nat by (rule int_of_nat_nat_eq) ``` huffman@23303 ` 874` huffman@23303 ` 875` ```corollary nat_0_le: "0 \ z ==> int (nat z) = z" ``` huffman@23308 ` 876` ```unfolding int_eq_of_nat by (rule nat_0_le') ``` huffman@23303 ` 877` huffman@23303 ` 878` ```lemma nonneg_eq_int: "[| 0 \ z; !!m. z = int m ==> P |] ==> P" ``` huffman@23308 ` 879` ```unfolding int_eq_of_nat by (blast elim: nonneg_eq_int_of_nat) ``` huffman@23303 ` 880` huffman@23303 ` 881` ```lemma nat_eq_iff: "(nat w = m) = (if 0 \ w then w = int m else m=0)" ``` huffman@23308 ` 882` ```unfolding int_eq_of_nat by (rule nat_eq_iff') ``` huffman@23303 ` 883` huffman@23303 ` 884` ```corollary nat_eq_iff2: "(m = nat w) = (if 0 \ w then w = int m else m=0)" ``` huffman@23308 ` 885` ```unfolding int_eq_of_nat by (rule nat_eq_iff2') ``` huffman@23303 ` 886` huffman@23303 ` 887` ```lemma nat_less_iff: "0 \ w ==> (nat w < m) = (w < int m)" ``` huffman@23308 ` 888` ```unfolding int_eq_of_nat by (rule nat_less_iff') ``` huffman@23303 ` 889` huffman@23303 ` 890` ```lemma int_eq_iff: "(int m = z) = (m = nat z & 0 \ z)" ``` huffman@23308 ` 891` ```unfolding int_eq_of_nat by (rule int_of_nat_eq_iff) ``` huffman@23303 ` 892` huffman@23303 ` 893` ```lemma nat_zminus_int [simp]: "nat (- (int n)) = 0" ``` huffman@23308 ` 894` ```unfolding int_eq_of_nat by (rule nat_zminus_int_of_nat) ``` huffman@23303 ` 895` huffman@23303 ` 896` ```lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)" ``` huffman@23308 ` 897` ```unfolding int_eq_of_nat by (rule zless_nat_eq_int_zless') ``` huffman@23303 ` 898` huffman@23303 ` 899` ```lemma negative_zless_0: "- (int (Suc n)) < 0" ``` huffman@23308 ` 900` ```unfolding int_eq_of_nat by (rule negative_zless_0') ``` huffman@23303 ` 901` huffman@23303 ` 902` ```lemma negative_zless [iff]: "- (int (Suc n)) < int m" ``` huffman@23308 ` 903` ```unfolding int_eq_of_nat by (rule negative_zless') ``` huffman@23303 ` 904` huffman@23303 ` 905` ```lemma negative_zle_0: "- int n \ 0" ``` huffman@23308 ` 906` ```unfolding int_eq_of_nat by (rule negative_zle_0') ``` huffman@23303 ` 907` huffman@23303 ` 908` ```lemma negative_zle [iff]: "- int n \ int m" ``` huffman@23308 ` 909` ```unfolding int_eq_of_nat by (rule negative_zle') ``` huffman@23303 ` 910` huffman@23303 ` 911` ```lemma not_zle_0_negative [simp]: "~ (0 \ - (int (Suc n)))" ``` huffman@23308 ` 912` ```unfolding int_eq_of_nat by (rule not_zle_0_negative') ``` huffman@23303 ` 913` huffman@23303 ` 914` ```lemma int_zle_neg: "(int n \ - int m) = (n = 0 & m = 0)" ``` huffman@23308 ` 915` ```unfolding int_eq_of_nat by (rule int_zle_neg') ``` huffman@23303 ` 916` huffman@23303 ` 917` ```lemma not_int_zless_negative [simp]: "~ (int n < - int m)" ``` huffman@23308 ` 918` ```unfolding int_eq_of_nat by (rule not_int_zless_negative') ``` huffman@23303 ` 919` huffman@23303 ` 920` ```lemma negative_eq_positive [simp]: "(- int n = int m) = (n = 0 & m = 0)" ``` huffman@23308 ` 921` ```unfolding int_eq_of_nat by (rule negative_eq_positive') ``` huffman@23303 ` 922` huffman@23303 ` 923` ```lemma zle_iff_zadd: "(w \ z) = (\n. z = w + int n)" ``` huffman@23308 ` 924` ```unfolding int_eq_of_nat by (rule zle_iff_zadd') ``` huffman@23303 ` 925` huffman@23303 ` 926` ```lemma abs_int_eq [simp]: "abs (int m) = int m" ``` huffman@23308 ` 927` ```unfolding int_eq_of_nat by (rule abs_of_nat) ``` huffman@23303 ` 928` huffman@23303 ` 929` ```lemma not_neg_int [simp]: "~ neg(int n)" ``` huffman@23308 ` 930` ```unfolding int_eq_of_nat by (rule not_neg_int_of_nat) ``` huffman@23303 ` 931` huffman@23303 ` 932` ```lemma neg_zminus_int [simp]: "neg(- (int (Suc n)))" ``` huffman@23308 ` 933` ```unfolding int_eq_of_nat by (rule neg_zminus_int_of_nat) ``` huffman@23303 ` 934` huffman@23303 ` 935` ```lemma not_neg_nat: "~ neg z ==> int (nat z) = z" ``` huffman@23308 ` 936` ```unfolding int_eq_of_nat by (rule not_neg_nat') ``` huffman@23303 ` 937` huffman@23303 ` 938` ```lemma of_int_int_eq [simp]: "of_int (int n) = of_nat n" ``` huffman@23307 ` 939` ```unfolding int_eq_of_nat by (rule of_int_of_nat_eq) ``` huffman@23303 ` 940` huffman@23303 ` 941` ```lemma int_setsum: "int (setsum f A) = (\x\A. int(f x))" ``` huffman@23307 ` 942` ```unfolding int_eq_of_nat by (rule of_nat_setsum) ``` huffman@23303 ` 943` huffman@23303 ` 944` ```lemma int_setprod: "int (setprod f A) = (\x\A. int(f x))" ``` huffman@23307 ` 945` ```unfolding int_eq_of_nat by (rule of_nat_setprod) ``` huffman@23303 ` 946` huffman@23303 ` 947` ```text{*Now we replace the case analysis rule by a more conventional one: ``` huffman@23303 ` 948` ```whether an integer is negative or not.*} ``` huffman@23303 ` 949` wenzelm@23164 ` 950` ```lemma zless_iff_Suc_zadd: ``` wenzelm@23164 ` 951` ``` "(w < z) = (\n. z = w + int(Suc n))" ``` huffman@23307 ` 952` ```unfolding int_eq_of_nat by (rule zless_iff_Suc_zadd') ``` wenzelm@23164 ` 953` wenzelm@23164 ` 954` ```lemma negD: "x<0 ==> \n. x = - (int (Suc n))" ``` huffman@23307 ` 955` ```unfolding int_eq_of_nat by (rule negD') ``` wenzelm@23164 ` 956` wenzelm@23164 ` 957` ```theorem int_cases [cases type: int, case_names nonneg neg]: ``` wenzelm@23164 ` 958` ``` "[|!! n. z = int n ==> P; !! n. z = - (int (Suc n)) ==> P |] ==> P" ``` huffman@23307 ` 959` ```unfolding int_eq_of_nat ``` huffman@23307 ` 960` ```apply (cases "z < 0", blast dest!: negD') ``` wenzelm@23164 ` 961` ```apply (simp add: linorder_not_less) ``` huffman@23307 ` 962` ```apply (blast dest: nat_0_le' [THEN sym]) ``` wenzelm@23164 ` 963` ```done ``` wenzelm@23164 ` 964` wenzelm@23164 ` 965` ```theorem int_induct [induct type: int, case_names nonneg neg]: ``` wenzelm@23164 ` 966` ``` "[|!! n. P (int n); !!n. P (- (int (Suc n))) |] ==> P z" ``` wenzelm@23164 ` 967` ``` by (cases z) auto ``` wenzelm@23164 ` 968` wenzelm@23164 ` 969` ```text{*Contributed by Brian Huffman*} ``` wenzelm@23164 ` 970` ```theorem int_diff_cases [case_names diff]: ``` wenzelm@23164 ` 971` ```assumes prem: "!!m n. z = int m - int n ==> P" shows "P" ``` wenzelm@23164 ` 972` ``` apply (rule_tac z=z in int_cases) ``` wenzelm@23164 ` 973` ``` apply (rule_tac m=n and n=0 in prem, simp) ``` wenzelm@23164 ` 974` ``` apply (rule_tac m=0 and n="Suc n" in prem, simp) ``` wenzelm@23164 ` 975` ```done ``` wenzelm@23164 ` 976` wenzelm@23164 ` 977` ```lemmas zless_le = less_int_def [THEN meta_eq_to_obj_eq] ``` wenzelm@23164 ` 978` wenzelm@23164 ` 979` ```lemmas [simp] = int_Suc ``` wenzelm@23164 ` 980` wenzelm@23164 ` 981` wenzelm@23164 ` 982` ```subsection {* Legacy ML bindings *} ``` wenzelm@23164 ` 983` wenzelm@23164 ` 984` ```ML {* ``` wenzelm@23164 ` 985` ```val of_nat_0 = @{thm of_nat_0}; ``` wenzelm@23164 ` 986` ```val of_nat_1 = @{thm of_nat_1}; ``` wenzelm@23164 ` 987` ```val of_nat_Suc = @{thm of_nat_Suc}; ``` wenzelm@23164 ` 988` ```val of_nat_add = @{thm of_nat_add}; ``` wenzelm@23164 ` 989` ```val of_nat_mult = @{thm of_nat_mult}; ``` wenzelm@23164 ` 990` ```val of_int_0 = @{thm of_int_0}; ``` wenzelm@23164 ` 991` ```val of_int_1 = @{thm of_int_1}; ``` wenzelm@23164 ` 992` ```val of_int_add = @{thm of_int_add}; ``` wenzelm@23164 ` 993` ```val of_int_mult = @{thm of_int_mult}; ``` wenzelm@23164 ` 994` ```val int_eq_of_nat = @{thm int_eq_of_nat}; ``` wenzelm@23164 ` 995` ```val zle_int = @{thm zle_int}; ``` wenzelm@23164 ` 996` ```val int_int_eq = @{thm int_int_eq}; ``` wenzelm@23164 ` 997` ```val diff_int_def = @{thm diff_int_def}; ``` wenzelm@23164 ` 998` ```val zadd_ac = @{thms zadd_ac}; ``` wenzelm@23164 ` 999` ```val zless_int = @{thm zless_int}; ``` wenzelm@23164 ` 1000` ```val zadd_int = @{thm zadd_int}; ``` wenzelm@23164 ` 1001` ```val zmult_int = @{thm zmult_int}; ``` wenzelm@23164 ` 1002` ```val nat_0_le = @{thm nat_0_le}; ``` wenzelm@23164 ` 1003` ```val int_0 = @{thm int_0}; ``` wenzelm@23164 ` 1004` ```val int_1 = @{thm int_1}; ``` wenzelm@23164 ` 1005` ```val abs_split = @{thm abs_split}; ``` wenzelm@23164 ` 1006` ```*} ``` wenzelm@23164 ` 1007` wenzelm@23164 ` 1008` ```end ```