src/ZF/Int_ZF.thy
 author paulson Tue Mar 06 16:06:52 2012 +0000 (2012-03-06) changeset 46821 ff6b0c1087f2 parent 46820 c656222c4dc1 child 46841 49b91b716cbe permissions -rw-r--r--
Using mathematical notation for <-> and cardinal arithmetic
 wenzelm@41777 ` 1` ```(* Title: ZF/Int_ZF.thy ``` krauss@26056 ` 2` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` krauss@26056 ` 3` ``` Copyright 1993 University of Cambridge ``` krauss@26056 ` 4` ```*) ``` krauss@26056 ` 5` krauss@26056 ` 6` ```header{*The Integers as Equivalence Classes Over Pairs of Natural Numbers*} ``` krauss@26056 ` 7` krauss@26056 ` 8` ```theory Int_ZF imports EquivClass ArithSimp begin ``` krauss@26056 ` 9` krauss@26056 ` 10` ```definition ``` krauss@26056 ` 11` ``` intrel :: i where ``` paulson@46820 ` 12` ``` "intrel == {p \ (nat*nat)*(nat*nat). ``` krauss@26056 ` 13` ``` \x1 y1 x2 y2. p=<,> & x1#+y2 = x2#+y1}" ``` krauss@26056 ` 14` krauss@26056 ` 15` ```definition ``` krauss@26056 ` 16` ``` int :: i where ``` krauss@26056 ` 17` ``` "int == (nat*nat)//intrel" ``` krauss@26056 ` 18` krauss@26056 ` 19` ```definition ``` krauss@26056 ` 20` ``` int_of :: "i=>i" --{*coercion from nat to int*} ("\$# _" [80] 80) where ``` krauss@26056 ` 21` ``` "\$# m == intrel `` {}" ``` krauss@26056 ` 22` krauss@26056 ` 23` ```definition ``` krauss@26056 ` 24` ``` intify :: "i=>i" --{*coercion from ANYTHING to int*} where ``` paulson@46820 ` 25` ``` "intify(m) == if m \ int then m else \$#0" ``` krauss@26056 ` 26` krauss@26056 ` 27` ```definition ``` krauss@26056 ` 28` ``` raw_zminus :: "i=>i" where ``` krauss@26056 ` 29` ``` "raw_zminus(z) == \\z. intrel``{}" ``` krauss@26056 ` 30` krauss@26056 ` 31` ```definition ``` krauss@26056 ` 32` ``` zminus :: "i=>i" ("\$- _" [80] 80) where ``` krauss@26056 ` 33` ``` "\$- z == raw_zminus (intify(z))" ``` krauss@26056 ` 34` krauss@26056 ` 35` ```definition ``` krauss@26056 ` 36` ``` znegative :: "i=>o" where ``` krauss@26056 ` 37` ``` "znegative(z) == \x y. xnat & \z" ``` krauss@26056 ` 38` krauss@26056 ` 39` ```definition ``` krauss@26056 ` 40` ``` iszero :: "i=>o" where ``` krauss@26056 ` 41` ``` "iszero(z) == z = \$# 0" ``` krauss@26056 ` 42` ``` ``` krauss@26056 ` 43` ```definition ``` krauss@26056 ` 44` ``` raw_nat_of :: "i=>i" where ``` krauss@26056 ` 45` ``` "raw_nat_of(z) == natify (\\z. x#-y)" ``` krauss@26056 ` 46` krauss@26056 ` 47` ```definition ``` krauss@26056 ` 48` ``` nat_of :: "i=>i" where ``` krauss@26056 ` 49` ``` "nat_of(z) == raw_nat_of (intify(z))" ``` krauss@26056 ` 50` krauss@26056 ` 51` ```definition ``` krauss@26056 ` 52` ``` zmagnitude :: "i=>i" where ``` krauss@26056 ` 53` ``` --{*could be replaced by an absolute value function from int to int?*} ``` krauss@26056 ` 54` ``` "zmagnitude(z) == ``` krauss@26056 ` 55` ``` THE m. m\nat & ((~ znegative(z) & z = \$# m) | ``` wenzelm@32960 ` 56` ``` (znegative(z) & \$- z = \$# m))" ``` krauss@26056 ` 57` krauss@26056 ` 58` ```definition ``` krauss@26056 ` 59` ``` raw_zmult :: "[i,i]=>i" where ``` krauss@26056 ` 60` ``` (*Cannot use UN here or in zadd because of the form of congruent2. ``` krauss@26056 ` 61` ``` Perhaps a "curried" or even polymorphic congruent predicate would be ``` krauss@26056 ` 62` ``` better.*) ``` krauss@26056 ` 63` ``` "raw_zmult(z1,z2) == ``` krauss@26056 ` 64` ``` \p1\z1. \p2\z2. split(%x1 y1. split(%x2 y2. ``` krauss@26056 ` 65` ``` intrel``{}, p2), p1)" ``` krauss@26056 ` 66` krauss@26056 ` 67` ```definition ``` krauss@26056 ` 68` ``` zmult :: "[i,i]=>i" (infixl "\$*" 70) where ``` krauss@26056 ` 69` ``` "z1 \$* z2 == raw_zmult (intify(z1),intify(z2))" ``` krauss@26056 ` 70` krauss@26056 ` 71` ```definition ``` krauss@26056 ` 72` ``` raw_zadd :: "[i,i]=>i" where ``` krauss@26056 ` 73` ``` "raw_zadd (z1, z2) == ``` krauss@26056 ` 74` ``` \z1\z1. \z2\z2. let =z1; =z2 ``` krauss@26056 ` 75` ``` in intrel``{}" ``` krauss@26056 ` 76` krauss@26056 ` 77` ```definition ``` krauss@26056 ` 78` ``` zadd :: "[i,i]=>i" (infixl "\$+" 65) where ``` krauss@26056 ` 79` ``` "z1 \$+ z2 == raw_zadd (intify(z1),intify(z2))" ``` krauss@26056 ` 80` krauss@26056 ` 81` ```definition ``` krauss@26056 ` 82` ``` zdiff :: "[i,i]=>i" (infixl "\$-" 65) where ``` krauss@26056 ` 83` ``` "z1 \$- z2 == z1 \$+ zminus(z2)" ``` krauss@26056 ` 84` krauss@26056 ` 85` ```definition ``` krauss@26056 ` 86` ``` zless :: "[i,i]=>o" (infixl "\$<" 50) where ``` krauss@26056 ` 87` ``` "z1 \$< z2 == znegative(z1 \$- z2)" ``` krauss@26056 ` 88` ``` ``` krauss@26056 ` 89` ```definition ``` krauss@26056 ` 90` ``` zle :: "[i,i]=>o" (infixl "\$<=" 50) where ``` krauss@26056 ` 91` ``` "z1 \$<= z2 == z1 \$< z2 | intify(z1)=intify(z2)" ``` krauss@26056 ` 92` ``` ``` krauss@26056 ` 93` krauss@26056 ` 94` ```notation (xsymbols) ``` krauss@26056 ` 95` ``` zmult (infixl "\$\" 70) and ``` krauss@26056 ` 96` ``` zle (infixl "\$\" 50) --{*less than or equals*} ``` krauss@26056 ` 97` krauss@26056 ` 98` ```notation (HTML output) ``` krauss@26056 ` 99` ``` zmult (infixl "\$\" 70) and ``` krauss@26056 ` 100` ``` zle (infixl "\$\" 50) ``` krauss@26056 ` 101` krauss@26056 ` 102` krauss@26056 ` 103` ```declare quotientE [elim!] ``` krauss@26056 ` 104` krauss@26056 ` 105` ```subsection{*Proving that @{term intrel} is an equivalence relation*} ``` krauss@26056 ` 106` krauss@26056 ` 107` ```(** Natural deduction for intrel **) ``` krauss@26056 ` 108` krauss@26056 ` 109` ```lemma intrel_iff [simp]: ``` paulson@46821 ` 110` ``` "<,>: intrel \ ``` krauss@26056 ` 111` ``` x1\nat & y1\nat & x2\nat & y2\nat & x1#+y2 = x2#+y1" ``` krauss@26056 ` 112` ```by (simp add: intrel_def) ``` krauss@26056 ` 113` krauss@26056 ` 114` ```lemma intrelI [intro!]: ``` krauss@26056 ` 115` ``` "[| x1#+y2 = x2#+y1; x1\nat; y1\nat; x2\nat; y2\nat |] ``` krauss@26056 ` 116` ``` ==> <,>: intrel" ``` krauss@26056 ` 117` ```by (simp add: intrel_def) ``` krauss@26056 ` 118` krauss@26056 ` 119` ```lemma intrelE [elim!]: ``` krauss@26056 ` 120` ``` "[| p: intrel; ``` krauss@26056 ` 121` ``` !!x1 y1 x2 y2. [| p = <,>; x1#+y2 = x2#+y1; ``` krauss@26056 ` 122` ``` x1\nat; y1\nat; x2\nat; y2\nat |] ==> Q |] ``` krauss@26056 ` 123` ``` ==> Q" ``` krauss@26056 ` 124` ```by (simp add: intrel_def, blast) ``` krauss@26056 ` 125` krauss@26056 ` 126` ```lemma int_trans_lemma: ``` krauss@26056 ` 127` ``` "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2 |] ==> x1 #+ y3 = x3 #+ y1" ``` krauss@26056 ` 128` ```apply (rule sym) ``` krauss@26056 ` 129` ```apply (erule add_left_cancel)+ ``` krauss@26056 ` 130` ```apply (simp_all (no_asm_simp)) ``` krauss@26056 ` 131` ```done ``` krauss@26056 ` 132` krauss@26056 ` 133` ```lemma equiv_intrel: "equiv(nat*nat, intrel)" ``` krauss@26056 ` 134` ```apply (simp add: equiv_def refl_def sym_def trans_def) ``` krauss@26056 ` 135` ```apply (fast elim!: sym int_trans_lemma) ``` krauss@26056 ` 136` ```done ``` krauss@26056 ` 137` paulson@46820 ` 138` ```lemma image_intrel_int: "[| m\nat; n\nat |] ==> intrel `` {} \ int" ``` krauss@26056 ` 139` ```by (simp add: int_def) ``` krauss@26056 ` 140` krauss@26056 ` 141` ```declare equiv_intrel [THEN eq_equiv_class_iff, simp] ``` krauss@26056 ` 142` ```declare conj_cong [cong] ``` krauss@26056 ` 143` krauss@26056 ` 144` ```lemmas eq_intrelD = eq_equiv_class [OF _ equiv_intrel] ``` krauss@26056 ` 145` krauss@26056 ` 146` ```(** int_of: the injection from nat to int **) ``` krauss@26056 ` 147` paulson@46820 ` 148` ```lemma int_of_type [simp,TC]: "\$#m \ int" ``` krauss@26056 ` 149` ```by (simp add: int_def quotient_def int_of_def, auto) ``` krauss@26056 ` 150` paulson@46821 ` 151` ```lemma int_of_eq [iff]: "(\$# m = \$# n) \ natify(m)=natify(n)" ``` krauss@26056 ` 152` ```by (simp add: int_of_def) ``` krauss@26056 ` 153` krauss@26056 ` 154` ```lemma int_of_inject: "[| \$#m = \$#n; m\nat; n\nat |] ==> m=n" ``` krauss@26056 ` 155` ```by (drule int_of_eq [THEN iffD1], auto) ``` krauss@26056 ` 156` krauss@26056 ` 157` krauss@26056 ` 158` ```(** intify: coercion from anything to int **) ``` krauss@26056 ` 159` paulson@46820 ` 160` ```lemma intify_in_int [iff,TC]: "intify(x) \ int" ``` krauss@26056 ` 161` ```by (simp add: intify_def) ``` krauss@26056 ` 162` paulson@46820 ` 163` ```lemma intify_ident [simp]: "n \ int ==> intify(n) = n" ``` krauss@26056 ` 164` ```by (simp add: intify_def) ``` krauss@26056 ` 165` krauss@26056 ` 166` krauss@26056 ` 167` ```subsection{*Collapsing rules: to remove @{term intify} ``` krauss@26056 ` 168` ``` from arithmetic expressions*} ``` krauss@26056 ` 169` krauss@26056 ` 170` ```lemma intify_idem [simp]: "intify(intify(x)) = intify(x)" ``` krauss@26056 ` 171` ```by simp ``` krauss@26056 ` 172` krauss@26056 ` 173` ```lemma int_of_natify [simp]: "\$# (natify(m)) = \$# m" ``` krauss@26056 ` 174` ```by (simp add: int_of_def) ``` krauss@26056 ` 175` krauss@26056 ` 176` ```lemma zminus_intify [simp]: "\$- (intify(m)) = \$- m" ``` krauss@26056 ` 177` ```by (simp add: zminus_def) ``` krauss@26056 ` 178` krauss@26056 ` 179` ```(** Addition **) ``` krauss@26056 ` 180` krauss@26056 ` 181` ```lemma zadd_intify1 [simp]: "intify(x) \$+ y = x \$+ y" ``` krauss@26056 ` 182` ```by (simp add: zadd_def) ``` krauss@26056 ` 183` krauss@26056 ` 184` ```lemma zadd_intify2 [simp]: "x \$+ intify(y) = x \$+ y" ``` krauss@26056 ` 185` ```by (simp add: zadd_def) ``` krauss@26056 ` 186` krauss@26056 ` 187` ```(** Subtraction **) ``` krauss@26056 ` 188` krauss@26056 ` 189` ```lemma zdiff_intify1 [simp]:"intify(x) \$- y = x \$- y" ``` krauss@26056 ` 190` ```by (simp add: zdiff_def) ``` krauss@26056 ` 191` krauss@26056 ` 192` ```lemma zdiff_intify2 [simp]:"x \$- intify(y) = x \$- y" ``` krauss@26056 ` 193` ```by (simp add: zdiff_def) ``` krauss@26056 ` 194` krauss@26056 ` 195` ```(** Multiplication **) ``` krauss@26056 ` 196` krauss@26056 ` 197` ```lemma zmult_intify1 [simp]:"intify(x) \$* y = x \$* y" ``` krauss@26056 ` 198` ```by (simp add: zmult_def) ``` krauss@26056 ` 199` krauss@26056 ` 200` ```lemma zmult_intify2 [simp]:"x \$* intify(y) = x \$* y" ``` krauss@26056 ` 201` ```by (simp add: zmult_def) ``` krauss@26056 ` 202` krauss@26056 ` 203` ```(** Orderings **) ``` krauss@26056 ` 204` paulson@46821 ` 205` ```lemma zless_intify1 [simp]:"intify(x) \$< y \ x \$< y" ``` krauss@26056 ` 206` ```by (simp add: zless_def) ``` krauss@26056 ` 207` paulson@46821 ` 208` ```lemma zless_intify2 [simp]:"x \$< intify(y) \ x \$< y" ``` krauss@26056 ` 209` ```by (simp add: zless_def) ``` krauss@26056 ` 210` paulson@46821 ` 211` ```lemma zle_intify1 [simp]:"intify(x) \$<= y \ x \$<= y" ``` krauss@26056 ` 212` ```by (simp add: zle_def) ``` krauss@26056 ` 213` paulson@46821 ` 214` ```lemma zle_intify2 [simp]:"x \$<= intify(y) \ x \$<= y" ``` krauss@26056 ` 215` ```by (simp add: zle_def) ``` krauss@26056 ` 216` krauss@26056 ` 217` krauss@26056 ` 218` ```subsection{*@{term zminus}: unary negation on @{term int}*} ``` krauss@26056 ` 219` krauss@26056 ` 220` ```lemma zminus_congruent: "(%. intrel``{}) respects intrel" ``` krauss@26056 ` 221` ```by (auto simp add: congruent_def add_ac) ``` krauss@26056 ` 222` paulson@46820 ` 223` ```lemma raw_zminus_type: "z \ int ==> raw_zminus(z) \ int" ``` krauss@26056 ` 224` ```apply (simp add: int_def raw_zminus_def) ``` krauss@26056 ` 225` ```apply (typecheck add: UN_equiv_class_type [OF equiv_intrel zminus_congruent]) ``` krauss@26056 ` 226` ```done ``` krauss@26056 ` 227` paulson@46820 ` 228` ```lemma zminus_type [TC,iff]: "\$-z \ int" ``` krauss@26056 ` 229` ```by (simp add: zminus_def raw_zminus_type) ``` krauss@26056 ` 230` krauss@26056 ` 231` ```lemma raw_zminus_inject: ``` krauss@26056 ` 232` ``` "[| raw_zminus(z) = raw_zminus(w); z: int; w: int |] ==> z=w" ``` krauss@26056 ` 233` ```apply (simp add: int_def raw_zminus_def) ``` krauss@26056 ` 234` ```apply (erule UN_equiv_class_inject [OF equiv_intrel zminus_congruent], safe) ``` krauss@26056 ` 235` ```apply (auto dest: eq_intrelD simp add: add_ac) ``` krauss@26056 ` 236` ```done ``` krauss@26056 ` 237` krauss@26056 ` 238` ```lemma zminus_inject_intify [dest!]: "\$-z = \$-w ==> intify(z) = intify(w)" ``` krauss@26056 ` 239` ```apply (simp add: zminus_def) ``` krauss@26056 ` 240` ```apply (blast dest!: raw_zminus_inject) ``` krauss@26056 ` 241` ```done ``` krauss@26056 ` 242` krauss@26056 ` 243` ```lemma zminus_inject: "[| \$-z = \$-w; z: int; w: int |] ==> z=w" ``` krauss@26056 ` 244` ```by auto ``` krauss@26056 ` 245` krauss@26056 ` 246` ```lemma raw_zminus: ``` krauss@26056 ` 247` ``` "[| x\nat; y\nat |] ==> raw_zminus(intrel``{}) = intrel `` {}" ``` krauss@26056 ` 248` ```apply (simp add: raw_zminus_def UN_equiv_class [OF equiv_intrel zminus_congruent]) ``` krauss@26056 ` 249` ```done ``` krauss@26056 ` 250` krauss@26056 ` 251` ```lemma zminus: ``` krauss@26056 ` 252` ``` "[| x\nat; y\nat |] ``` krauss@26056 ` 253` ``` ==> \$- (intrel``{}) = intrel `` {}" ``` krauss@26056 ` 254` ```by (simp add: zminus_def raw_zminus image_intrel_int) ``` krauss@26056 ` 255` paulson@46820 ` 256` ```lemma raw_zminus_zminus: "z \ int ==> raw_zminus (raw_zminus(z)) = z" ``` krauss@26056 ` 257` ```by (auto simp add: int_def raw_zminus) ``` krauss@26056 ` 258` krauss@26056 ` 259` ```lemma zminus_zminus_intify [simp]: "\$- (\$- z) = intify(z)" ``` krauss@26056 ` 260` ```by (simp add: zminus_def raw_zminus_type raw_zminus_zminus) ``` krauss@26056 ` 261` krauss@26056 ` 262` ```lemma zminus_int0 [simp]: "\$- (\$#0) = \$#0" ``` krauss@26056 ` 263` ```by (simp add: int_of_def zminus) ``` krauss@26056 ` 264` paulson@46820 ` 265` ```lemma zminus_zminus: "z \ int ==> \$- (\$- z) = z" ``` krauss@26056 ` 266` ```by simp ``` krauss@26056 ` 267` krauss@26056 ` 268` krauss@26056 ` 269` ```subsection{*@{term znegative}: the test for negative integers*} ``` krauss@26056 ` 270` paulson@46821 ` 271` ```lemma znegative: "[| x\nat; y\nat |] ==> znegative(intrel``{}) \ x natify(n)=0" ``` krauss@26056 ` 286` ```by (simp add: znegative int_of_def zminus Ord_0_lt_iff [THEN iff_sym]) ``` krauss@26056 ` 287` krauss@26056 ` 288` krauss@26056 ` 289` ```subsection{*@{term nat_of}: Coercion of an Integer to a Natural Number*} ``` krauss@26056 ` 290` krauss@26056 ` 291` ```lemma nat_of_intify [simp]: "nat_of(intify(z)) = nat_of(z)" ``` krauss@26056 ` 292` ```by (simp add: nat_of_def) ``` krauss@26056 ` 293` krauss@26056 ` 294` ```lemma nat_of_congruent: "(\x. (\\x,y\. x #- y)(x)) respects intrel" ``` krauss@26056 ` 295` ```by (auto simp add: congruent_def split add: nat_diff_split) ``` krauss@26056 ` 296` krauss@26056 ` 297` ```lemma raw_nat_of: ``` krauss@26056 ` 298` ``` "[| x\nat; y\nat |] ==> raw_nat_of(intrel``{}) = x#-y" ``` krauss@26056 ` 299` ```by (simp add: raw_nat_of_def UN_equiv_class [OF equiv_intrel nat_of_congruent]) ``` krauss@26056 ` 300` krauss@26056 ` 301` ```lemma raw_nat_of_int_of: "raw_nat_of(\$# n) = natify(n)" ``` krauss@26056 ` 302` ```by (simp add: int_of_def raw_nat_of) ``` krauss@26056 ` 303` krauss@26056 ` 304` ```lemma nat_of_int_of [simp]: "nat_of(\$# n) = natify(n)" ``` krauss@26056 ` 305` ```by (simp add: raw_nat_of_int_of nat_of_def) ``` krauss@26056 ` 306` krauss@26056 ` 307` ```lemma raw_nat_of_type: "raw_nat_of(z) \ nat" ``` krauss@26056 ` 308` ```by (simp add: raw_nat_of_def) ``` krauss@26056 ` 309` krauss@26056 ` 310` ```lemma nat_of_type [iff,TC]: "nat_of(z) \ nat" ``` krauss@26056 ` 311` ```by (simp add: nat_of_def raw_nat_of_type) ``` krauss@26056 ` 312` krauss@26056 ` 313` ```subsection{*zmagnitude: magnitide of an integer, as a natural number*} ``` krauss@26056 ` 314` krauss@26056 ` 315` ```lemma zmagnitude_int_of [simp]: "zmagnitude(\$# n) = natify(n)" ``` krauss@26056 ` 316` ```by (auto simp add: zmagnitude_def int_of_eq) ``` krauss@26056 ` 317` krauss@26056 ` 318` ```lemma natify_int_of_eq: "natify(x)=n ==> \$#x = \$# n" ``` krauss@26056 ` 319` ```apply (drule sym) ``` krauss@26056 ` 320` ```apply (simp (no_asm_simp) add: int_of_eq) ``` krauss@26056 ` 321` ```done ``` krauss@26056 ` 322` krauss@26056 ` 323` ```lemma zmagnitude_zminus_int_of [simp]: "zmagnitude(\$- \$# n) = natify(n)" ``` krauss@26056 ` 324` ```apply (simp add: zmagnitude_def) ``` krauss@26056 ` 325` ```apply (rule the_equality) ``` krauss@26056 ` 326` ```apply (auto dest!: not_znegative_imp_zero natify_int_of_eq ``` krauss@26056 ` 327` ``` iff del: int_of_eq, auto) ``` krauss@26056 ` 328` ```done ``` krauss@26056 ` 329` krauss@26056 ` 330` ```lemma zmagnitude_type [iff,TC]: "zmagnitude(z)\nat" ``` krauss@26056 ` 331` ```apply (simp add: zmagnitude_def) ``` krauss@26056 ` 332` ```apply (rule theI2, auto) ``` krauss@26056 ` 333` ```done ``` krauss@26056 ` 334` krauss@26056 ` 335` ```lemma not_zneg_int_of: ``` krauss@26056 ` 336` ``` "[| z: int; ~ znegative(z) |] ==> \n\nat. z = \$# n" ``` krauss@26056 ` 337` ```apply (auto simp add: int_def znegative int_of_def not_lt_iff_le) ``` krauss@26056 ` 338` ```apply (rename_tac x y) ``` krauss@26056 ` 339` ```apply (rule_tac x="x#-y" in bexI) ``` krauss@26056 ` 340` ```apply (auto simp add: add_diff_inverse2) ``` krauss@26056 ` 341` ```done ``` krauss@26056 ` 342` krauss@26056 ` 343` ```lemma not_zneg_mag [simp]: ``` krauss@26056 ` 344` ``` "[| z: int; ~ znegative(z) |] ==> \$# (zmagnitude(z)) = z" ``` krauss@26056 ` 345` ```by (drule not_zneg_int_of, auto) ``` krauss@26056 ` 346` krauss@26056 ` 347` ```lemma zneg_int_of: ``` krauss@26056 ` 348` ``` "[| znegative(z); z: int |] ==> \n\nat. z = \$- (\$# succ(n))" ``` krauss@26056 ` 349` ```by (auto simp add: int_def znegative zminus int_of_def dest!: less_imp_succ_add) ``` krauss@26056 ` 350` krauss@26056 ` 351` ```lemma zneg_mag [simp]: ``` krauss@26056 ` 352` ``` "[| znegative(z); z: int |] ==> \$# (zmagnitude(z)) = \$- z" ``` krauss@26056 ` 353` ```by (drule zneg_int_of, auto) ``` krauss@26056 ` 354` paulson@46820 ` 355` ```lemma int_cases: "z \ int ==> \n\nat. z = \$# n | z = \$- (\$# succ(n))" ``` krauss@26056 ` 356` ```apply (case_tac "znegative (z) ") ``` krauss@26056 ` 357` ```prefer 2 apply (blast dest: not_zneg_mag sym) ``` krauss@26056 ` 358` ```apply (blast dest: zneg_int_of) ``` krauss@26056 ` 359` ```done ``` krauss@26056 ` 360` krauss@26056 ` 361` ```lemma not_zneg_raw_nat_of: ``` krauss@26056 ` 362` ``` "[| ~ znegative(z); z: int |] ==> \$# (raw_nat_of(z)) = z" ``` krauss@26056 ` 363` ```apply (drule not_zneg_int_of) ``` krauss@26056 ` 364` ```apply (auto simp add: raw_nat_of_type raw_nat_of_int_of) ``` krauss@26056 ` 365` ```done ``` krauss@26056 ` 366` krauss@26056 ` 367` ```lemma not_zneg_nat_of_intify: ``` krauss@26056 ` 368` ``` "~ znegative(intify(z)) ==> \$# (nat_of(z)) = intify(z)" ``` krauss@26056 ` 369` ```by (simp (no_asm_simp) add: nat_of_def not_zneg_raw_nat_of) ``` krauss@26056 ` 370` krauss@26056 ` 371` ```lemma not_zneg_nat_of: "[| ~ znegative(z); z: int |] ==> \$# (nat_of(z)) = z" ``` krauss@26056 ` 372` ```apply (simp (no_asm_simp) add: not_zneg_nat_of_intify) ``` krauss@26056 ` 373` ```done ``` krauss@26056 ` 374` krauss@26056 ` 375` ```lemma zneg_nat_of [simp]: "znegative(intify(z)) ==> nat_of(z) = 0" ``` krauss@26056 ` 376` ```apply (subgoal_tac "intify(z) \ int") ``` krauss@26056 ` 377` ```apply (simp add: int_def) ``` krauss@26056 ` 378` ```apply (auto simp add: znegative nat_of_def raw_nat_of ``` krauss@26056 ` 379` ``` split add: nat_diff_split) ``` krauss@26056 ` 380` ```done ``` krauss@26056 ` 381` krauss@26056 ` 382` krauss@26056 ` 383` ```subsection{*@{term zadd}: addition on int*} ``` krauss@26056 ` 384` krauss@26056 ` 385` ```text{*Congruence Property for Addition*} ``` krauss@26056 ` 386` ```lemma zadd_congruent2: ``` krauss@26056 ` 387` ``` "(%z1 z2. let =z1; =z2 ``` krauss@26056 ` 388` ``` in intrel``{}) ``` krauss@26056 ` 389` ``` respects2 intrel" ``` krauss@26056 ` 390` ```apply (simp add: congruent2_def) ``` krauss@26056 ` 391` ```(*Proof via congruent2_commuteI seems longer*) ``` krauss@26056 ` 392` ```apply safe ``` krauss@26056 ` 393` ```apply (simp (no_asm_simp) add: add_assoc Let_def) ``` krauss@26056 ` 394` ```(*The rest should be trivial, but rearranging terms is hard ``` krauss@26056 ` 395` ``` add_ac does not help rewriting with the assumptions.*) ``` krauss@26056 ` 396` ```apply (rule_tac m1 = x1a in add_left_commute [THEN ssubst]) ``` krauss@26056 ` 397` ```apply (rule_tac m1 = x2a in add_left_commute [THEN ssubst]) ``` krauss@26056 ` 398` ```apply (simp (no_asm_simp) add: add_assoc [symmetric]) ``` krauss@26056 ` 399` ```done ``` krauss@26056 ` 400` paulson@46820 ` 401` ```lemma raw_zadd_type: "[| z: int; w: int |] ==> raw_zadd(z,w) \ int" ``` krauss@26056 ` 402` ```apply (simp add: int_def raw_zadd_def) ``` krauss@26056 ` 403` ```apply (rule UN_equiv_class_type2 [OF equiv_intrel zadd_congruent2], assumption+) ``` krauss@26056 ` 404` ```apply (simp add: Let_def) ``` krauss@26056 ` 405` ```done ``` krauss@26056 ` 406` paulson@46820 ` 407` ```lemma zadd_type [iff,TC]: "z \$+ w \ int" ``` krauss@26056 ` 408` ```by (simp add: zadd_def raw_zadd_type) ``` krauss@26056 ` 409` krauss@26056 ` 410` ```lemma raw_zadd: ``` krauss@26056 ` 411` ``` "[| x1\nat; y1\nat; x2\nat; y2\nat |] ``` krauss@26056 ` 412` ``` ==> raw_zadd (intrel``{}, intrel``{}) = ``` krauss@26056 ` 413` ``` intrel `` {}" ``` krauss@26056 ` 414` ```apply (simp add: raw_zadd_def ``` krauss@26056 ` 415` ``` UN_equiv_class2 [OF equiv_intrel equiv_intrel zadd_congruent2]) ``` krauss@26056 ` 416` ```apply (simp add: Let_def) ``` krauss@26056 ` 417` ```done ``` krauss@26056 ` 418` krauss@26056 ` 419` ```lemma zadd: ``` krauss@26056 ` 420` ``` "[| x1\nat; y1\nat; x2\nat; y2\nat |] ``` krauss@26056 ` 421` ``` ==> (intrel``{}) \$+ (intrel``{}) = ``` krauss@26056 ` 422` ``` intrel `` {}" ``` krauss@26056 ` 423` ```by (simp add: zadd_def raw_zadd image_intrel_int) ``` krauss@26056 ` 424` paulson@46820 ` 425` ```lemma raw_zadd_int0: "z \ int ==> raw_zadd (\$#0,z) = z" ``` krauss@26056 ` 426` ```by (auto simp add: int_def int_of_def raw_zadd) ``` krauss@26056 ` 427` krauss@26056 ` 428` ```lemma zadd_int0_intify [simp]: "\$#0 \$+ z = intify(z)" ``` krauss@26056 ` 429` ```by (simp add: zadd_def raw_zadd_int0) ``` krauss@26056 ` 430` krauss@26056 ` 431` ```lemma zadd_int0: "z: int ==> \$#0 \$+ z = z" ``` krauss@26056 ` 432` ```by simp ``` krauss@26056 ` 433` krauss@26056 ` 434` ```lemma raw_zminus_zadd_distrib: ``` krauss@26056 ` 435` ``` "[| z: int; w: int |] ==> \$- raw_zadd(z,w) = raw_zadd(\$- z, \$- w)" ``` krauss@26056 ` 436` ```by (auto simp add: zminus raw_zadd int_def) ``` krauss@26056 ` 437` krauss@26056 ` 438` ```lemma zminus_zadd_distrib [simp]: "\$- (z \$+ w) = \$- z \$+ \$- w" ``` krauss@26056 ` 439` ```by (simp add: zadd_def raw_zminus_zadd_distrib) ``` krauss@26056 ` 440` krauss@26056 ` 441` ```lemma raw_zadd_commute: ``` krauss@26056 ` 442` ``` "[| z: int; w: int |] ==> raw_zadd(z,w) = raw_zadd(w,z)" ``` krauss@26056 ` 443` ```by (auto simp add: raw_zadd add_ac int_def) ``` krauss@26056 ` 444` krauss@26056 ` 445` ```lemma zadd_commute: "z \$+ w = w \$+ z" ``` krauss@26056 ` 446` ```by (simp add: zadd_def raw_zadd_commute) ``` krauss@26056 ` 447` krauss@26056 ` 448` ```lemma raw_zadd_assoc: ``` krauss@26056 ` 449` ``` "[| z1: int; z2: int; z3: int |] ``` krauss@26056 ` 450` ``` ==> raw_zadd (raw_zadd(z1,z2),z3) = raw_zadd(z1,raw_zadd(z2,z3))" ``` krauss@26056 ` 451` ```by (auto simp add: int_def raw_zadd add_assoc) ``` krauss@26056 ` 452` krauss@26056 ` 453` ```lemma zadd_assoc: "(z1 \$+ z2) \$+ z3 = z1 \$+ (z2 \$+ z3)" ``` krauss@26056 ` 454` ```by (simp add: zadd_def raw_zadd_type raw_zadd_assoc) ``` krauss@26056 ` 455` krauss@26056 ` 456` ```(*For AC rewriting*) ``` krauss@26056 ` 457` ```lemma zadd_left_commute: "z1\$+(z2\$+z3) = z2\$+(z1\$+z3)" ``` krauss@26056 ` 458` ```apply (simp add: zadd_assoc [symmetric]) ``` krauss@26056 ` 459` ```apply (simp add: zadd_commute) ``` krauss@26056 ` 460` ```done ``` krauss@26056 ` 461` krauss@26056 ` 462` ```(*Integer addition is an AC operator*) ``` krauss@26056 ` 463` ```lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute ``` krauss@26056 ` 464` krauss@26056 ` 465` ```lemma int_of_add: "\$# (m #+ n) = (\$#m) \$+ (\$#n)" ``` krauss@26056 ` 466` ```by (simp add: int_of_def zadd) ``` krauss@26056 ` 467` krauss@26056 ` 468` ```lemma int_succ_int_1: "\$# succ(m) = \$# 1 \$+ (\$# m)" ``` krauss@26056 ` 469` ```by (simp add: int_of_add [symmetric] natify_succ) ``` krauss@26056 ` 470` krauss@26056 ` 471` ```lemma int_of_diff: ``` paulson@46820 ` 472` ``` "[| m\nat; n \ m |] ==> \$# (m #- n) = (\$#m) \$- (\$#n)" ``` krauss@26056 ` 473` ```apply (simp add: int_of_def zdiff_def) ``` krauss@26056 ` 474` ```apply (frule lt_nat_in_nat) ``` krauss@26056 ` 475` ```apply (simp_all add: zadd zminus add_diff_inverse2) ``` krauss@26056 ` 476` ```done ``` krauss@26056 ` 477` paulson@46820 ` 478` ```lemma raw_zadd_zminus_inverse: "z \ int ==> raw_zadd (z, \$- z) = \$#0" ``` krauss@26056 ` 479` ```by (auto simp add: int_def int_of_def zminus raw_zadd add_commute) ``` krauss@26056 ` 480` krauss@26056 ` 481` ```lemma zadd_zminus_inverse [simp]: "z \$+ (\$- z) = \$#0" ``` krauss@26056 ` 482` ```apply (simp add: zadd_def) ``` krauss@26056 ` 483` ```apply (subst zminus_intify [symmetric]) ``` krauss@26056 ` 484` ```apply (rule intify_in_int [THEN raw_zadd_zminus_inverse]) ``` krauss@26056 ` 485` ```done ``` krauss@26056 ` 486` krauss@26056 ` 487` ```lemma zadd_zminus_inverse2 [simp]: "(\$- z) \$+ z = \$#0" ``` krauss@26056 ` 488` ```by (simp add: zadd_commute zadd_zminus_inverse) ``` krauss@26056 ` 489` krauss@26056 ` 490` ```lemma zadd_int0_right_intify [simp]: "z \$+ \$#0 = intify(z)" ``` krauss@26056 ` 491` ```by (rule trans [OF zadd_commute zadd_int0_intify]) ``` krauss@26056 ` 492` krauss@26056 ` 493` ```lemma zadd_int0_right: "z:int ==> z \$+ \$#0 = z" ``` krauss@26056 ` 494` ```by simp ``` krauss@26056 ` 495` krauss@26056 ` 496` krauss@26056 ` 497` ```subsection{*@{term zmult}: Integer Multiplication*} ``` krauss@26056 ` 498` krauss@26056 ` 499` ```text{*Congruence property for multiplication*} ``` krauss@26056 ` 500` ```lemma zmult_congruent2: ``` krauss@26056 ` 501` ``` "(%p1 p2. split(%x1 y1. split(%x2 y2. ``` krauss@26056 ` 502` ``` intrel``{}, p2), p1)) ``` krauss@26056 ` 503` ``` respects2 intrel" ``` krauss@26056 ` 504` ```apply (rule equiv_intrel [THEN congruent2_commuteI], auto) ``` krauss@26056 ` 505` ```(*Proof that zmult is congruent in one argument*) ``` krauss@26056 ` 506` ```apply (rename_tac x y) ``` krauss@26056 ` 507` ```apply (frule_tac t = "%u. x#*u" in sym [THEN subst_context]) ``` krauss@26056 ` 508` ```apply (drule_tac t = "%u. y#*u" in subst_context) ``` krauss@26056 ` 509` ```apply (erule add_left_cancel)+ ``` krauss@26056 ` 510` ```apply (simp_all add: add_mult_distrib_left) ``` krauss@26056 ` 511` ```done ``` krauss@26056 ` 512` krauss@26056 ` 513` paulson@46820 ` 514` ```lemma raw_zmult_type: "[| z: int; w: int |] ==> raw_zmult(z,w) \ int" ``` krauss@26056 ` 515` ```apply (simp add: int_def raw_zmult_def) ``` krauss@26056 ` 516` ```apply (rule UN_equiv_class_type2 [OF equiv_intrel zmult_congruent2], assumption+) ``` krauss@26056 ` 517` ```apply (simp add: Let_def) ``` krauss@26056 ` 518` ```done ``` krauss@26056 ` 519` paulson@46820 ` 520` ```lemma zmult_type [iff,TC]: "z \$* w \ int" ``` krauss@26056 ` 521` ```by (simp add: zmult_def raw_zmult_type) ``` krauss@26056 ` 522` krauss@26056 ` 523` ```lemma raw_zmult: ``` krauss@26056 ` 524` ``` "[| x1\nat; y1\nat; x2\nat; y2\nat |] ``` krauss@26056 ` 525` ``` ==> raw_zmult(intrel``{}, intrel``{}) = ``` krauss@26056 ` 526` ``` intrel `` {}" ``` krauss@26056 ` 527` ```by (simp add: raw_zmult_def ``` krauss@26056 ` 528` ``` UN_equiv_class2 [OF equiv_intrel equiv_intrel zmult_congruent2]) ``` krauss@26056 ` 529` krauss@26056 ` 530` ```lemma zmult: ``` krauss@26056 ` 531` ``` "[| x1\nat; y1\nat; x2\nat; y2\nat |] ``` krauss@26056 ` 532` ``` ==> (intrel``{}) \$* (intrel``{}) = ``` krauss@26056 ` 533` ``` intrel `` {}" ``` krauss@26056 ` 534` ```by (simp add: zmult_def raw_zmult image_intrel_int) ``` krauss@26056 ` 535` paulson@46820 ` 536` ```lemma raw_zmult_int0: "z \ int ==> raw_zmult (\$#0,z) = \$#0" ``` krauss@26056 ` 537` ```by (auto simp add: int_def int_of_def raw_zmult) ``` krauss@26056 ` 538` krauss@26056 ` 539` ```lemma zmult_int0 [simp]: "\$#0 \$* z = \$#0" ``` krauss@26056 ` 540` ```by (simp add: zmult_def raw_zmult_int0) ``` krauss@26056 ` 541` paulson@46820 ` 542` ```lemma raw_zmult_int1: "z \ int ==> raw_zmult (\$#1,z) = z" ``` krauss@26056 ` 543` ```by (auto simp add: int_def int_of_def raw_zmult) ``` krauss@26056 ` 544` krauss@26056 ` 545` ```lemma zmult_int1_intify [simp]: "\$#1 \$* z = intify(z)" ``` krauss@26056 ` 546` ```by (simp add: zmult_def raw_zmult_int1) ``` krauss@26056 ` 547` paulson@46820 ` 548` ```lemma zmult_int1: "z \ int ==> \$#1 \$* z = z" ``` krauss@26056 ` 549` ```by simp ``` krauss@26056 ` 550` krauss@26056 ` 551` ```lemma raw_zmult_commute: ``` krauss@26056 ` 552` ``` "[| z: int; w: int |] ==> raw_zmult(z,w) = raw_zmult(w,z)" ``` krauss@26056 ` 553` ```by (auto simp add: int_def raw_zmult add_ac mult_ac) ``` krauss@26056 ` 554` krauss@26056 ` 555` ```lemma zmult_commute: "z \$* w = w \$* z" ``` krauss@26056 ` 556` ```by (simp add: zmult_def raw_zmult_commute) ``` krauss@26056 ` 557` krauss@26056 ` 558` ```lemma raw_zmult_zminus: ``` krauss@26056 ` 559` ``` "[| z: int; w: int |] ==> raw_zmult(\$- z, w) = \$- raw_zmult(z, w)" ``` krauss@26056 ` 560` ```by (auto simp add: int_def zminus raw_zmult add_ac) ``` krauss@26056 ` 561` krauss@26056 ` 562` ```lemma zmult_zminus [simp]: "(\$- z) \$* w = \$- (z \$* w)" ``` krauss@26056 ` 563` ```apply (simp add: zmult_def raw_zmult_zminus) ``` krauss@26056 ` 564` ```apply (subst zminus_intify [symmetric], rule raw_zmult_zminus, auto) ``` krauss@26056 ` 565` ```done ``` krauss@26056 ` 566` krauss@26056 ` 567` ```lemma zmult_zminus_right [simp]: "w \$* (\$- z) = \$- (w \$* z)" ``` krauss@26056 ` 568` ```by (simp add: zmult_commute [of w]) ``` krauss@26056 ` 569` krauss@26056 ` 570` ```lemma raw_zmult_assoc: ``` krauss@26056 ` 571` ``` "[| z1: int; z2: int; z3: int |] ``` krauss@26056 ` 572` ``` ==> raw_zmult (raw_zmult(z1,z2),z3) = raw_zmult(z1,raw_zmult(z2,z3))" ``` krauss@26056 ` 573` ```by (auto simp add: int_def raw_zmult add_mult_distrib_left add_ac mult_ac) ``` krauss@26056 ` 574` krauss@26056 ` 575` ```lemma zmult_assoc: "(z1 \$* z2) \$* z3 = z1 \$* (z2 \$* z3)" ``` krauss@26056 ` 576` ```by (simp add: zmult_def raw_zmult_type raw_zmult_assoc) ``` krauss@26056 ` 577` krauss@26056 ` 578` ```(*For AC rewriting*) ``` krauss@26056 ` 579` ```lemma zmult_left_commute: "z1\$*(z2\$*z3) = z2\$*(z1\$*z3)" ``` krauss@26056 ` 580` ```apply (simp add: zmult_assoc [symmetric]) ``` krauss@26056 ` 581` ```apply (simp add: zmult_commute) ``` krauss@26056 ` 582` ```done ``` krauss@26056 ` 583` krauss@26056 ` 584` ```(*Integer multiplication is an AC operator*) ``` krauss@26056 ` 585` ```lemmas zmult_ac = zmult_assoc zmult_commute zmult_left_commute ``` krauss@26056 ` 586` krauss@26056 ` 587` ```lemma raw_zadd_zmult_distrib: ``` krauss@26056 ` 588` ``` "[| z1: int; z2: int; w: int |] ``` krauss@26056 ` 589` ``` ==> raw_zmult(raw_zadd(z1,z2), w) = ``` krauss@26056 ` 590` ``` raw_zadd (raw_zmult(z1,w), raw_zmult(z2,w))" ``` krauss@26056 ` 591` ```by (auto simp add: int_def raw_zadd raw_zmult add_mult_distrib_left add_ac mult_ac) ``` krauss@26056 ` 592` krauss@26056 ` 593` ```lemma zadd_zmult_distrib: "(z1 \$+ z2) \$* w = (z1 \$* w) \$+ (z2 \$* w)" ``` krauss@26056 ` 594` ```by (simp add: zmult_def zadd_def raw_zadd_type raw_zmult_type ``` krauss@26056 ` 595` ``` raw_zadd_zmult_distrib) ``` krauss@26056 ` 596` krauss@26056 ` 597` ```lemma zadd_zmult_distrib2: "w \$* (z1 \$+ z2) = (w \$* z1) \$+ (w \$* z2)" ``` krauss@26056 ` 598` ```by (simp add: zmult_commute [of w] zadd_zmult_distrib) ``` krauss@26056 ` 599` krauss@26056 ` 600` ```lemmas int_typechecks = ``` krauss@26056 ` 601` ``` int_of_type zminus_type zmagnitude_type zadd_type zmult_type ``` krauss@26056 ` 602` krauss@26056 ` 603` krauss@26056 ` 604` ```(*** Subtraction laws ***) ``` krauss@26056 ` 605` paulson@46820 ` 606` ```lemma zdiff_type [iff,TC]: "z \$- w \ int" ``` krauss@26056 ` 607` ```by (simp add: zdiff_def) ``` krauss@26056 ` 608` krauss@26056 ` 609` ```lemma zminus_zdiff_eq [simp]: "\$- (z \$- y) = y \$- z" ``` krauss@26056 ` 610` ```by (simp add: zdiff_def zadd_commute) ``` krauss@26056 ` 611` krauss@26056 ` 612` ```lemma zdiff_zmult_distrib: "(z1 \$- z2) \$* w = (z1 \$* w) \$- (z2 \$* w)" ``` krauss@26056 ` 613` ```apply (simp add: zdiff_def) ``` krauss@26056 ` 614` ```apply (subst zadd_zmult_distrib) ``` krauss@26056 ` 615` ```apply (simp add: zmult_zminus) ``` krauss@26056 ` 616` ```done ``` krauss@26056 ` 617` krauss@26056 ` 618` ```lemma zdiff_zmult_distrib2: "w \$* (z1 \$- z2) = (w \$* z1) \$- (w \$* z2)" ``` krauss@26056 ` 619` ```by (simp add: zmult_commute [of w] zdiff_zmult_distrib) ``` krauss@26056 ` 620` krauss@26056 ` 621` ```lemma zadd_zdiff_eq: "x \$+ (y \$- z) = (x \$+ y) \$- z" ``` krauss@26056 ` 622` ```by (simp add: zdiff_def zadd_ac) ``` krauss@26056 ` 623` krauss@26056 ` 624` ```lemma zdiff_zadd_eq: "(x \$- y) \$+ z = (x \$+ z) \$- y" ``` krauss@26056 ` 625` ```by (simp add: zdiff_def zadd_ac) ``` krauss@26056 ` 626` krauss@26056 ` 627` krauss@26056 ` 628` ```subsection{*The "Less Than" Relation*} ``` krauss@26056 ` 629` krauss@26056 ` 630` ```(*"Less than" is a linear ordering*) ``` krauss@26056 ` 631` ```lemma zless_linear_lemma: ``` krauss@26056 ` 632` ``` "[| z: int; w: int |] ==> z\$ (x \ y) \ (x \$< y | y \$< x)" ``` krauss@26056 ` 648` ```by (cut_tac z = x and w = y in zless_linear, auto) ``` krauss@26056 ` 649` paulson@46820 ` 650` ```lemma zless_imp_intify_neq: "w \$< z ==> intify(w) \ intify(z)" ``` krauss@26056 ` 651` ```apply auto ``` krauss@26056 ` 652` ```apply (subgoal_tac "~ (intify (w) \$< intify (z))") ``` krauss@26056 ` 653` ```apply (erule_tac [2] ssubst) ``` krauss@26056 ` 654` ```apply (simp (no_asm_use)) ``` krauss@26056 ` 655` ```apply auto ``` krauss@26056 ` 656` ```done ``` krauss@26056 ` 657` krauss@26056 ` 658` ```(*This lemma allows direct proofs of other <-properties*) ``` krauss@26056 ` 659` ```lemma zless_imp_succ_zadd_lemma: ``` krauss@26056 ` 660` ``` "[| w \$< z; w: int; z: int |] ==> (\n\nat. z = w \$+ \$#(succ(n)))" ``` krauss@26056 ` 661` ```apply (simp add: zless_def znegative_def zdiff_def int_def) ``` krauss@26056 ` 662` ```apply (auto dest!: less_imp_succ_add simp add: zadd zminus int_of_def) ``` krauss@26056 ` 663` ```apply (rule_tac x = k in bexI) ``` krauss@26056 ` 664` ```apply (erule add_left_cancel, auto) ``` krauss@26056 ` 665` ```done ``` krauss@26056 ` 666` krauss@26056 ` 667` ```lemma zless_imp_succ_zadd: ``` krauss@26056 ` 668` ``` "w \$< z ==> (\n\nat. w \$+ \$#(succ(n)) = intify(z))" ``` krauss@26056 ` 669` ```apply (subgoal_tac "intify (w) \$< intify (z) ") ``` krauss@26056 ` 670` ```apply (drule_tac w = "intify (w) " in zless_imp_succ_zadd_lemma) ``` krauss@26056 ` 671` ```apply auto ``` krauss@26056 ` 672` ```done ``` krauss@26056 ` 673` krauss@26056 ` 674` ```lemma zless_succ_zadd_lemma: ``` paulson@46820 ` 675` ``` "w \ int ==> w \$< w \$+ \$# succ(n)" ``` krauss@26056 ` 676` ```apply (simp add: zless_def znegative_def zdiff_def int_def) ``` krauss@26056 ` 677` ```apply (auto simp add: zadd zminus int_of_def image_iff) ``` krauss@26056 ` 678` ```apply (rule_tac x = 0 in exI, auto) ``` krauss@26056 ` 679` ```done ``` krauss@26056 ` 680` krauss@26056 ` 681` ```lemma zless_succ_zadd: "w \$< w \$+ \$# succ(n)" ``` krauss@26056 ` 682` ```by (cut_tac intify_in_int [THEN zless_succ_zadd_lemma], auto) ``` krauss@26056 ` 683` krauss@26056 ` 684` ```lemma zless_iff_succ_zadd: ``` paulson@46821 ` 685` ``` "w \$< z \ (\n\nat. w \$+ \$#(succ(n)) = intify(z))" ``` krauss@26056 ` 686` ```apply (rule iffI) ``` krauss@26056 ` 687` ```apply (erule zless_imp_succ_zadd, auto) ``` krauss@26056 ` 688` ```apply (rename_tac "n") ``` krauss@26056 ` 689` ```apply (cut_tac w = w and n = n in zless_succ_zadd, auto) ``` krauss@26056 ` 690` ```done ``` krauss@26056 ` 691` paulson@46821 ` 692` ```lemma zless_int_of [simp]: "[| m\nat; n\nat |] ==> (\$#m \$< \$#n) \ (m int; z: int |] ==> x \$< z" ``` krauss@26056 ` 699` ```apply (simp add: zless_def znegative_def zdiff_def int_def) ``` krauss@26056 ` 700` ```apply (auto simp add: zadd zminus image_iff) ``` krauss@26056 ` 701` ```apply (rename_tac x1 x2 y1 y2) ``` krauss@26056 ` 702` ```apply (rule_tac x = "x1#+x2" in exI) ``` krauss@26056 ` 703` ```apply (rule_tac x = "y1#+y2" in exI) ``` krauss@26056 ` 704` ```apply (auto simp add: add_lt_mono) ``` krauss@26056 ` 705` ```apply (rule sym) ``` krauss@26056 ` 706` ```apply (erule add_left_cancel)+ ``` krauss@26056 ` 707` ```apply auto ``` krauss@26056 ` 708` ```done ``` krauss@26056 ` 709` krauss@26056 ` 710` ```lemma zless_trans: "[| x \$< y; y \$< z |] ==> x \$< z" ``` krauss@26056 ` 711` ```apply (subgoal_tac "intify (x) \$< intify (z) ") ``` krauss@26056 ` 712` ```apply (rule_tac [2] y = "intify (y) " in zless_trans_lemma) ``` krauss@26056 ` 713` ```apply auto ``` krauss@26056 ` 714` ```done ``` krauss@26056 ` 715` krauss@26056 ` 716` ```lemma zless_not_sym: "z \$< w ==> ~ (w \$< z)" ``` krauss@26056 ` 717` ```by (blast dest: zless_trans) ``` krauss@26056 ` 718` krauss@26056 ` 719` ```(* [| z \$< w; ~ P ==> w \$< z |] ==> P *) ``` wenzelm@45602 ` 720` ```lemmas zless_asym = zless_not_sym [THEN swap] ``` krauss@26056 ` 721` krauss@26056 ` 722` ```lemma zless_imp_zle: "z \$< w ==> z \$<= w" ``` krauss@26056 ` 723` ```by (simp add: zle_def) ``` krauss@26056 ` 724` krauss@26056 ` 725` ```lemma zle_linear: "z \$<= w | w \$<= z" ``` krauss@26056 ` 726` ```apply (simp add: zle_def) ``` krauss@26056 ` 727` ```apply (cut_tac zless_linear, blast) ``` krauss@26056 ` 728` ```done ``` krauss@26056 ` 729` krauss@26056 ` 730` krauss@26056 ` 731` ```subsection{*Less Than or Equals*} ``` krauss@26056 ` 732` krauss@26056 ` 733` ```lemma zle_refl: "z \$<= z" ``` krauss@26056 ` 734` ```by (simp add: zle_def) ``` krauss@26056 ` 735` krauss@26056 ` 736` ```lemma zle_eq_refl: "x=y ==> x \$<= y" ``` krauss@26056 ` 737` ```by (simp add: zle_refl) ``` krauss@26056 ` 738` krauss@26056 ` 739` ```lemma zle_anti_sym_intify: "[| x \$<= y; y \$<= x |] ==> intify(x) = intify(y)" ``` krauss@26056 ` 740` ```apply (simp add: zle_def, auto) ``` krauss@26056 ` 741` ```apply (blast dest: zless_trans) ``` krauss@26056 ` 742` ```done ``` krauss@26056 ` 743` krauss@26056 ` 744` ```lemma zle_anti_sym: "[| x \$<= y; y \$<= x; x: int; y: int |] ==> x=y" ``` krauss@26056 ` 745` ```by (drule zle_anti_sym_intify, auto) ``` krauss@26056 ` 746` krauss@26056 ` 747` ```lemma zle_trans_lemma: ``` krauss@26056 ` 748` ``` "[| x: int; y: int; z: int; x \$<= y; y \$<= z |] ==> x \$<= z" ``` krauss@26056 ` 749` ```apply (simp add: zle_def, auto) ``` krauss@26056 ` 750` ```apply (blast intro: zless_trans) ``` krauss@26056 ` 751` ```done ``` krauss@26056 ` 752` krauss@26056 ` 753` ```lemma zle_trans: "[| x \$<= y; y \$<= z |] ==> x \$<= z" ``` krauss@26056 ` 754` ```apply (subgoal_tac "intify (x) \$<= intify (z) ") ``` krauss@26056 ` 755` ```apply (rule_tac [2] y = "intify (y) " in zle_trans_lemma) ``` krauss@26056 ` 756` ```apply auto ``` krauss@26056 ` 757` ```done ``` krauss@26056 ` 758` krauss@26056 ` 759` ```lemma zle_zless_trans: "[| i \$<= j; j \$< k |] ==> i \$< k" ``` krauss@26056 ` 760` ```apply (auto simp add: zle_def) ``` krauss@26056 ` 761` ```apply (blast intro: zless_trans) ``` krauss@26056 ` 762` ```apply (simp add: zless_def zdiff_def zadd_def) ``` krauss@26056 ` 763` ```done ``` krauss@26056 ` 764` krauss@26056 ` 765` ```lemma zless_zle_trans: "[| i \$< j; j \$<= k |] ==> i \$< k" ``` krauss@26056 ` 766` ```apply (auto simp add: zle_def) ``` krauss@26056 ` 767` ```apply (blast intro: zless_trans) ``` krauss@26056 ` 768` ```apply (simp add: zless_def zdiff_def zminus_def) ``` krauss@26056 ` 769` ```done ``` krauss@26056 ` 770` paulson@46821 ` 771` ```lemma not_zless_iff_zle: "~ (z \$< w) \ (w \$<= z)" ``` krauss@26056 ` 772` ```apply (cut_tac z = z and w = w in zless_linear) ``` krauss@26056 ` 773` ```apply (auto dest: zless_trans simp add: zle_def) ``` krauss@26056 ` 774` ```apply (auto dest!: zless_imp_intify_neq) ``` krauss@26056 ` 775` ```done ``` krauss@26056 ` 776` paulson@46821 ` 777` ```lemma not_zle_iff_zless: "~ (z \$<= w) \ (w \$< z)" ``` krauss@26056 ` 778` ```by (simp add: not_zless_iff_zle [THEN iff_sym]) ``` krauss@26056 ` 779` krauss@26056 ` 780` krauss@26056 ` 781` ```subsection{*More subtraction laws (for @{text zcompare_rls})*} ``` krauss@26056 ` 782` krauss@26056 ` 783` ```lemma zdiff_zdiff_eq: "(x \$- y) \$- z = x \$- (y \$+ z)" ``` krauss@26056 ` 784` ```by (simp add: zdiff_def zadd_ac) ``` krauss@26056 ` 785` krauss@26056 ` 786` ```lemma zdiff_zdiff_eq2: "x \$- (y \$- z) = (x \$+ z) \$- y" ``` krauss@26056 ` 787` ```by (simp add: zdiff_def zadd_ac) ``` krauss@26056 ` 788` paulson@46821 ` 789` ```lemma zdiff_zless_iff: "(x\$-y \$< z) \ (x \$< z \$+ y)" ``` krauss@26056 ` 790` ```by (simp add: zless_def zdiff_def zadd_ac) ``` krauss@26056 ` 791` paulson@46821 ` 792` ```lemma zless_zdiff_iff: "(x \$< z\$-y) \ (x \$+ y \$< z)" ``` krauss@26056 ` 793` ```by (simp add: zless_def zdiff_def zadd_ac) ``` krauss@26056 ` 794` paulson@46821 ` 795` ```lemma zdiff_eq_iff: "[| x: int; z: int |] ==> (x\$-y = z) \ (x = z \$+ y)" ``` krauss@26056 ` 796` ```by (auto simp add: zdiff_def zadd_assoc) ``` krauss@26056 ` 797` paulson@46821 ` 798` ```lemma eq_zdiff_iff: "[| x: int; z: int |] ==> (x = z\$-y) \ (x \$+ y = z)" ``` krauss@26056 ` 799` ```by (auto simp add: zdiff_def zadd_assoc) ``` krauss@26056 ` 800` krauss@26056 ` 801` ```lemma zdiff_zle_iff_lemma: ``` paulson@46821 ` 802` ``` "[| x: int; z: int |] ==> (x\$-y \$<= z) \ (x \$<= z \$+ y)" ``` krauss@26056 ` 803` ```by (auto simp add: zle_def zdiff_eq_iff zdiff_zless_iff) ``` krauss@26056 ` 804` paulson@46821 ` 805` ```lemma zdiff_zle_iff: "(x\$-y \$<= z) \ (x \$<= z \$+ y)" ``` krauss@26056 ` 806` ```by (cut_tac zdiff_zle_iff_lemma [OF intify_in_int intify_in_int], simp) ``` krauss@26056 ` 807` krauss@26056 ` 808` ```lemma zle_zdiff_iff_lemma: ``` paulson@46821 ` 809` ``` "[| x: int; z: int |] ==>(x \$<= z\$-y) \ (x \$+ y \$<= z)" ``` krauss@26056 ` 810` ```apply (auto simp add: zle_def zdiff_eq_iff zless_zdiff_iff) ``` krauss@26056 ` 811` ```apply (auto simp add: zdiff_def zadd_assoc) ``` krauss@26056 ` 812` ```done ``` krauss@26056 ` 813` paulson@46821 ` 814` ```lemma zle_zdiff_iff: "(x \$<= z\$-y) \ (x \$+ y \$<= z)" ``` krauss@26056 ` 815` ```by (cut_tac zle_zdiff_iff_lemma [ OF intify_in_int intify_in_int], simp) ``` krauss@26056 ` 816` krauss@26056 ` 817` ```text{*This list of rewrites simplifies (in)equalities by bringing subtractions ``` krauss@26056 ` 818` ``` to the top and then moving negative terms to the other side. ``` krauss@26056 ` 819` ``` Use with @{text zadd_ac}*} ``` krauss@26056 ` 820` ```lemmas zcompare_rls = ``` krauss@26056 ` 821` ``` zdiff_def [symmetric] ``` krauss@26056 ` 822` ``` zadd_zdiff_eq zdiff_zadd_eq zdiff_zdiff_eq zdiff_zdiff_eq2 ``` krauss@26056 ` 823` ``` zdiff_zless_iff zless_zdiff_iff zdiff_zle_iff zle_zdiff_iff ``` krauss@26056 ` 824` ``` zdiff_eq_iff eq_zdiff_iff ``` krauss@26056 ` 825` krauss@26056 ` 826` krauss@26056 ` 827` ```subsection{*Monotonicity and Cancellation Results for Instantiation ``` krauss@26056 ` 828` ``` of the CancelNumerals Simprocs*} ``` krauss@26056 ` 829` krauss@26056 ` 830` ```lemma zadd_left_cancel: ``` paulson@46821 ` 831` ``` "[| w: int; w': int |] ==> (z \$+ w' = z \$+ w) \ (w' = w)" ``` krauss@26056 ` 832` ```apply safe ``` krauss@26056 ` 833` ```apply (drule_tac t = "%x. x \$+ (\$-z) " in subst_context) ``` krauss@26056 ` 834` ```apply (simp add: zadd_ac) ``` krauss@26056 ` 835` ```done ``` krauss@26056 ` 836` krauss@26056 ` 837` ```lemma zadd_left_cancel_intify [simp]: ``` paulson@46821 ` 838` ``` "(z \$+ w' = z \$+ w) \ intify(w') = intify(w)" ``` krauss@26056 ` 839` ```apply (rule iff_trans) ``` krauss@26056 ` 840` ```apply (rule_tac [2] zadd_left_cancel, auto) ``` krauss@26056 ` 841` ```done ``` krauss@26056 ` 842` krauss@26056 ` 843` ```lemma zadd_right_cancel: ``` paulson@46821 ` 844` ``` "[| w: int; w': int |] ==> (w' \$+ z = w \$+ z) \ (w' = w)" ``` krauss@26056 ` 845` ```apply safe ``` krauss@26056 ` 846` ```apply (drule_tac t = "%x. x \$+ (\$-z) " in subst_context) ``` krauss@26056 ` 847` ```apply (simp add: zadd_ac) ``` krauss@26056 ` 848` ```done ``` krauss@26056 ` 849` krauss@26056 ` 850` ```lemma zadd_right_cancel_intify [simp]: ``` paulson@46821 ` 851` ``` "(w' \$+ z = w \$+ z) \ intify(w') = intify(w)" ``` krauss@26056 ` 852` ```apply (rule iff_trans) ``` krauss@26056 ` 853` ```apply (rule_tac [2] zadd_right_cancel, auto) ``` krauss@26056 ` 854` ```done ``` krauss@26056 ` 855` paulson@46821 ` 856` ```lemma zadd_right_cancel_zless [simp]: "(w' \$+ z \$< w \$+ z) \ (w' \$< w)" ``` krauss@26056 ` 857` ```by (simp add: zdiff_zless_iff [THEN iff_sym] zdiff_def zadd_assoc) ``` krauss@26056 ` 858` paulson@46821 ` 859` ```lemma zadd_left_cancel_zless [simp]: "(z \$+ w' \$< z \$+ w) \ (w' \$< w)" ``` krauss@26056 ` 860` ```by (simp add: zadd_commute [of z] zadd_right_cancel_zless) ``` krauss@26056 ` 861` paulson@46821 ` 862` ```lemma zadd_right_cancel_zle [simp]: "(w' \$+ z \$<= w \$+ z) \ w' \$<= w" ``` krauss@26056 ` 863` ```by (simp add: zle_def) ``` krauss@26056 ` 864` paulson@46821 ` 865` ```lemma zadd_left_cancel_zle [simp]: "(z \$+ w' \$<= z \$+ w) \ w' \$<= w" ``` krauss@26056 ` 866` ```by (simp add: zadd_commute [of z] zadd_right_cancel_zle) ``` krauss@26056 ` 867` krauss@26056 ` 868` krauss@26056 ` 869` ```(*"v \$<= w ==> v\$+z \$<= w\$+z"*) ``` wenzelm@45602 ` 870` ```lemmas zadd_zless_mono1 = zadd_right_cancel_zless [THEN iffD2] ``` krauss@26056 ` 871` krauss@26056 ` 872` ```(*"v \$<= w ==> z\$+v \$<= z\$+w"*) ``` wenzelm@45602 ` 873` ```lemmas zadd_zless_mono2 = zadd_left_cancel_zless [THEN iffD2] ``` krauss@26056 ` 874` krauss@26056 ` 875` ```(*"v \$<= w ==> v\$+z \$<= w\$+z"*) ``` wenzelm@45602 ` 876` ```lemmas zadd_zle_mono1 = zadd_right_cancel_zle [THEN iffD2] ``` krauss@26056 ` 877` krauss@26056 ` 878` ```(*"v \$<= w ==> z\$+v \$<= z\$+w"*) ``` wenzelm@45602 ` 879` ```lemmas zadd_zle_mono2 = zadd_left_cancel_zle [THEN iffD2] ``` krauss@26056 ` 880` krauss@26056 ` 881` ```lemma zadd_zle_mono: "[| w' \$<= w; z' \$<= z |] ==> w' \$+ z' \$<= w \$+ z" ``` krauss@26056 ` 882` ```by (erule zadd_zle_mono1 [THEN zle_trans], simp) ``` krauss@26056 ` 883` krauss@26056 ` 884` ```lemma zadd_zless_mono: "[| w' \$< w; z' \$<= z |] ==> w' \$+ z' \$< w \$+ z" ``` krauss@26056 ` 885` ```by (erule zadd_zless_mono1 [THEN zless_zle_trans], simp) ``` krauss@26056 ` 886` krauss@26056 ` 887` krauss@26056 ` 888` ```subsection{*Comparison laws*} ``` krauss@26056 ` 889` paulson@46821 ` 890` ```lemma zminus_zless_zminus [simp]: "(\$- x \$< \$- y) \ (y \$< x)" ``` krauss@26056 ` 891` ```by (simp add: zless_def zdiff_def zadd_ac) ``` krauss@26056 ` 892` paulson@46821 ` 893` ```lemma zminus_zle_zminus [simp]: "(\$- x \$<= \$- y) \ (y \$<= x)" ``` krauss@26056 ` 894` ```by (simp add: not_zless_iff_zle [THEN iff_sym]) ``` krauss@26056 ` 895` krauss@26056 ` 896` ```subsubsection{*More inequality lemmas*} ``` krauss@26056 ` 897` paulson@46821 ` 898` ```lemma equation_zminus: "[| x: int; y: int |] ==> (x = \$- y) \ (y = \$- x)" ``` krauss@26056 ` 899` ```by auto ``` krauss@26056 ` 900` paulson@46821 ` 901` ```lemma zminus_equation: "[| x: int; y: int |] ==> (\$- x = y) \ (\$- y = x)" ``` krauss@26056 ` 902` ```by auto ``` krauss@26056 ` 903` paulson@46821 ` 904` ```lemma equation_zminus_intify: "(intify(x) = \$- y) \ (intify(y) = \$- x)" ``` krauss@26056 ` 905` ```apply (cut_tac x = "intify (x) " and y = "intify (y) " in equation_zminus) ``` krauss@26056 ` 906` ```apply auto ``` krauss@26056 ` 907` ```done ``` krauss@26056 ` 908` paulson@46821 ` 909` ```lemma zminus_equation_intify: "(\$- x = intify(y)) \ (\$- y = intify(x))" ``` krauss@26056 ` 910` ```apply (cut_tac x = "intify (x) " and y = "intify (y) " in zminus_equation) ``` krauss@26056 ` 911` ```apply auto ``` krauss@26056 ` 912` ```done ``` krauss@26056 ` 913` krauss@26056 ` 914` krauss@26056 ` 915` ```subsubsection{*The next several equations are permutative: watch out!*} ``` krauss@26056 ` 916` paulson@46821 ` 917` ```lemma zless_zminus: "(x \$< \$- y) \ (y \$< \$- x)" ``` krauss@26056 ` 918` ```by (simp add: zless_def zdiff_def zadd_ac) ``` krauss@26056 ` 919` paulson@46821 ` 920` ```lemma zminus_zless: "(\$- x \$< y) \ (\$- y \$< x)" ``` krauss@26056 ` 921` ```by (simp add: zless_def zdiff_def zadd_ac) ``` krauss@26056 ` 922` paulson@46821 ` 923` ```lemma zle_zminus: "(x \$<= \$- y) \ (y \$<= \$- x)" ``` krauss@26056 ` 924` ```by (simp add: not_zless_iff_zle [THEN iff_sym] zminus_zless) ``` krauss@26056 ` 925` paulson@46821 ` 926` ```lemma zminus_zle: "(\$- x \$<= y) \ (\$- y \$<= x)" ``` krauss@26056 ` 927` ```by (simp add: not_zless_iff_zle [THEN iff_sym] zless_zminus) ``` krauss@26056 ` 928` krauss@26056 ` 929` ```end ```