src/ZF/IntDiv_ZF.thy
 author wenzelm Sat Oct 17 14:43:18 2009 +0200 (2009-10-17) changeset 32960 69916a850301 parent 32149 ef59550a55d3 child 45602 2a858377c3d2 permissions -rw-r--r--
eliminated hard tabulators, guessing at each author's individual tab-width;
 wenzelm@32960 ` 1` ```(* Title: ZF/IntDiv_ZF.thy ``` krauss@26056 ` 2` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` krauss@26056 ` 3` ``` Copyright 1999 University of Cambridge ``` krauss@26056 ` 4` krauss@26056 ` 5` ```Here is the division algorithm in ML: ``` krauss@26056 ` 6` krauss@26056 ` 7` ``` fun posDivAlg (a,b) = ``` krauss@26056 ` 8` ``` if a0 then posDivAlg (a,b) ``` wenzelm@32960 ` 23` ``` else if a=0 then (0,0) ``` wenzelm@32960 ` 24` ``` else negateSnd (negDivAlg (~a,~b)) ``` wenzelm@32960 ` 25` ``` else ``` wenzelm@32960 ` 26` ``` if 0 o" where ``` krauss@26056 ` 36` ``` "quorem == % . ``` krauss@26056 ` 37` ``` a = b\$*q \$+ r & ``` krauss@26056 ` 38` ``` (#0\$ i" where ``` krauss@26056 ` 42` ``` "adjust(b) == %. if #0 \$<= r\$-b then <#2\$*q \$+ #1,r\$-b> ``` krauss@26056 ` 43` ``` else <#2\$*q,r>" ``` krauss@26056 ` 44` krauss@26056 ` 45` krauss@26056 ` 46` ```(** the division algorithm **) ``` krauss@26056 ` 47` krauss@26056 ` 48` ```definition ``` krauss@26056 ` 49` ``` posDivAlg :: "i => i" where ``` krauss@26056 ` 50` ```(*for the case a>=0, b>0*) ``` krauss@26056 ` 51` ```(*recdef posDivAlg "inv_image less_than (%(a,b). nat_of(a \$- b \$+ #1))"*) ``` krauss@26056 ` 52` ``` "posDivAlg(ab) == ``` krauss@26056 ` 53` ``` wfrec(measure(int*int, %. nat_of (a \$- b \$+ #1)), ``` wenzelm@32960 ` 54` ``` ab, ``` wenzelm@32960 ` 55` ``` % f. if (a\$ ``` krauss@26056 ` 56` ``` else adjust(b, f ` ))" ``` krauss@26056 ` 57` krauss@26056 ` 58` krauss@26056 ` 59` ```(*for the case a<0, b>0*) ``` krauss@26056 ` 60` ```definition ``` krauss@26056 ` 61` ``` negDivAlg :: "i => i" where ``` krauss@26056 ` 62` ```(*recdef negDivAlg "inv_image less_than (%(a,b). nat_of(- a \$- b))"*) ``` krauss@26056 ` 63` ``` "negDivAlg(ab) == ``` krauss@26056 ` 64` ``` wfrec(measure(int*int, %. nat_of (\$- a \$- b)), ``` wenzelm@32960 ` 65` ``` ab, ``` wenzelm@32960 ` 66` ``` % f. if (#0 \$<= a\$+b | b\$<=#0) then <#-1,a\$+b> ``` krauss@26056 ` 67` ``` else adjust(b, f ` ))" ``` krauss@26056 ` 68` krauss@26056 ` 69` ```(*for the general case b\0*) ``` krauss@26056 ` 70` krauss@26056 ` 71` ```definition ``` krauss@26056 ` 72` ``` negateSnd :: "i => i" where ``` krauss@26056 ` 73` ``` "negateSnd == %. " ``` krauss@26056 ` 74` krauss@26056 ` 75` ``` (*The full division algorithm considers all possible signs for a, b ``` krauss@26056 ` 76` ``` including the special case a=0, b<0, because negDivAlg requires a<0*) ``` krauss@26056 ` 77` ```definition ``` krauss@26056 ` 78` ``` divAlg :: "i => i" where ``` krauss@26056 ` 79` ``` "divAlg == ``` krauss@26056 ` 80` ``` %. if #0 \$<= a then ``` krauss@26056 ` 81` ``` if #0 \$<= b then posDivAlg () ``` krauss@26056 ` 82` ``` else if a=#0 then <#0,#0> ``` krauss@26056 ` 83` ``` else negateSnd (negDivAlg (<\$-a,\$-b>)) ``` krauss@26056 ` 84` ``` else ``` krauss@26056 ` 85` ``` if #0\$) ``` krauss@26056 ` 86` ``` else negateSnd (posDivAlg (<\$-a,\$-b>))" ``` krauss@26056 ` 87` krauss@26056 ` 88` ```definition ``` krauss@26056 ` 89` ``` zdiv :: "[i,i]=>i" (infixl "zdiv" 70) where ``` krauss@26056 ` 90` ``` "a zdiv b == fst (divAlg ())" ``` krauss@26056 ` 91` krauss@26056 ` 92` ```definition ``` krauss@26056 ` 93` ``` zmod :: "[i,i]=>i" (infixl "zmod" 70) where ``` krauss@26056 ` 94` ``` "a zmod b == snd (divAlg ())" ``` krauss@26056 ` 95` krauss@26056 ` 96` krauss@26056 ` 97` ```(** Some basic laws by Sidi Ehmety (need linear arithmetic!) **) ``` krauss@26056 ` 98` krauss@26056 ` 99` ```lemma zspos_add_zspos_imp_zspos: "[| #0 \$< x; #0 \$< y |] ==> #0 \$< x \$+ y" ``` krauss@26056 ` 100` ```apply (rule_tac y = "y" in zless_trans) ``` krauss@26056 ` 101` ```apply (rule_tac [2] zdiff_zless_iff [THEN iffD1]) ``` krauss@26056 ` 102` ```apply auto ``` krauss@26056 ` 103` ```done ``` krauss@26056 ` 104` krauss@26056 ` 105` ```lemma zpos_add_zpos_imp_zpos: "[| #0 \$<= x; #0 \$<= y |] ==> #0 \$<= x \$+ y" ``` krauss@26056 ` 106` ```apply (rule_tac y = "y" in zle_trans) ``` krauss@26056 ` 107` ```apply (rule_tac [2] zdiff_zle_iff [THEN iffD1]) ``` krauss@26056 ` 108` ```apply auto ``` krauss@26056 ` 109` ```done ``` krauss@26056 ` 110` krauss@26056 ` 111` ```lemma zneg_add_zneg_imp_zneg: "[| x \$< #0; y \$< #0 |] ==> x \$+ y \$< #0" ``` krauss@26056 ` 112` ```apply (rule_tac y = "y" in zless_trans) ``` krauss@26056 ` 113` ```apply (rule zless_zdiff_iff [THEN iffD1]) ``` krauss@26056 ` 114` ```apply auto ``` krauss@26056 ` 115` ```done ``` krauss@26056 ` 116` krauss@26056 ` 117` ```(* this theorem is used below *) ``` krauss@26056 ` 118` ```lemma zneg_or_0_add_zneg_or_0_imp_zneg_or_0: ``` krauss@26056 ` 119` ``` "[| x \$<= #0; y \$<= #0 |] ==> x \$+ y \$<= #0" ``` krauss@26056 ` 120` ```apply (rule_tac y = "y" in zle_trans) ``` krauss@26056 ` 121` ```apply (rule zle_zdiff_iff [THEN iffD1]) ``` krauss@26056 ` 122` ```apply auto ``` krauss@26056 ` 123` ```done ``` krauss@26056 ` 124` krauss@26056 ` 125` ```lemma zero_lt_zmagnitude: "[| #0 \$< k; k \ int |] ==> 0 < zmagnitude(k)" ``` krauss@26056 ` 126` ```apply (drule zero_zless_imp_znegative_zminus) ``` krauss@26056 ` 127` ```apply (drule_tac [2] zneg_int_of) ``` krauss@26056 ` 128` ```apply (auto simp add: zminus_equation [of k]) ``` krauss@26056 ` 129` ```apply (subgoal_tac "0 < zmagnitude (\$# succ (n))") ``` krauss@26056 ` 130` ``` apply simp ``` krauss@26056 ` 131` ```apply (simp only: zmagnitude_int_of) ``` krauss@26056 ` 132` ```apply simp ``` krauss@26056 ` 133` ```done ``` krauss@26056 ` 134` krauss@26056 ` 135` krauss@26056 ` 136` ```(*** Inequality lemmas involving \$#succ(m) ***) ``` krauss@26056 ` 137` krauss@26056 ` 138` ```lemma zless_add_succ_iff: ``` krauss@26056 ` 139` ``` "(w \$< z \$+ \$# succ(m)) <-> (w \$< z \$+ \$#m | intify(w) = z \$+ \$#m)" ``` krauss@26056 ` 140` ```apply (auto simp add: zless_iff_succ_zadd zadd_assoc int_of_add [symmetric]) ``` krauss@26056 ` 141` ```apply (rule_tac [3] x = "0" in bexI) ``` krauss@26056 ` 142` ```apply (cut_tac m = "m" in int_succ_int_1) ``` krauss@26056 ` 143` ```apply (cut_tac m = "n" in int_succ_int_1) ``` krauss@26056 ` 144` ```apply simp ``` krauss@26056 ` 145` ```apply (erule natE) ``` krauss@26056 ` 146` ```apply auto ``` krauss@26056 ` 147` ```apply (rule_tac x = "succ (n) " in bexI) ``` krauss@26056 ` 148` ```apply auto ``` krauss@26056 ` 149` ```done ``` krauss@26056 ` 150` krauss@26056 ` 151` ```lemma zadd_succ_lemma: ``` krauss@26056 ` 152` ``` "z \ int ==> (w \$+ \$# succ(m) \$<= z) <-> (w \$+ \$#m \$< z)" ``` krauss@26056 ` 153` ```apply (simp only: not_zless_iff_zle [THEN iff_sym] zless_add_succ_iff) ``` krauss@26056 ` 154` ```apply (auto intro: zle_anti_sym elim: zless_asym ``` krauss@26056 ` 155` ``` simp add: zless_imp_zle not_zless_iff_zle) ``` krauss@26056 ` 156` ```done ``` krauss@26056 ` 157` krauss@26056 ` 158` ```lemma zadd_succ_zle_iff: "(w \$+ \$# succ(m) \$<= z) <-> (w \$+ \$#m \$< z)" ``` krauss@26056 ` 159` ```apply (cut_tac z = "intify (z)" in zadd_succ_lemma) ``` krauss@26056 ` 160` ```apply auto ``` krauss@26056 ` 161` ```done ``` krauss@26056 ` 162` krauss@26056 ` 163` ```(** Inequality reasoning **) ``` krauss@26056 ` 164` krauss@26056 ` 165` ```lemma zless_add1_iff_zle: "(w \$< z \$+ #1) <-> (w\$<=z)" ``` krauss@26056 ` 166` ```apply (subgoal_tac "#1 = \$# 1") ``` krauss@26056 ` 167` ```apply (simp only: zless_add_succ_iff zle_def) ``` krauss@26056 ` 168` ```apply auto ``` krauss@26056 ` 169` ```done ``` krauss@26056 ` 170` krauss@26056 ` 171` ```lemma add1_zle_iff: "(w \$+ #1 \$<= z) <-> (w \$< z)" ``` krauss@26056 ` 172` ```apply (subgoal_tac "#1 = \$# 1") ``` krauss@26056 ` 173` ```apply (simp only: zadd_succ_zle_iff) ``` krauss@26056 ` 174` ```apply auto ``` krauss@26056 ` 175` ```done ``` krauss@26056 ` 176` krauss@26056 ` 177` ```lemma add1_left_zle_iff: "(#1 \$+ w \$<= z) <-> (w \$< z)" ``` krauss@26056 ` 178` ```apply (subst zadd_commute) ``` krauss@26056 ` 179` ```apply (rule add1_zle_iff) ``` krauss@26056 ` 180` ```done ``` krauss@26056 ` 181` krauss@26056 ` 182` krauss@26056 ` 183` ```(*** Monotonicity of Multiplication ***) ``` krauss@26056 ` 184` krauss@26056 ` 185` ```lemma zmult_mono_lemma: "k \ nat ==> i \$<= j ==> i \$* \$#k \$<= j \$* \$#k" ``` krauss@26056 ` 186` ```apply (induct_tac "k") ``` krauss@26056 ` 187` ``` prefer 2 apply (subst int_succ_int_1) ``` krauss@26056 ` 188` ```apply (simp_all (no_asm_simp) add: zadd_zmult_distrib2 zadd_zle_mono) ``` krauss@26056 ` 189` ```done ``` krauss@26056 ` 190` krauss@26056 ` 191` ```lemma zmult_zle_mono1: "[| i \$<= j; #0 \$<= k |] ==> i\$*k \$<= j\$*k" ``` krauss@26056 ` 192` ```apply (subgoal_tac "i \$* intify (k) \$<= j \$* intify (k) ") ``` krauss@26056 ` 193` ```apply (simp (no_asm_use)) ``` krauss@26056 ` 194` ```apply (rule_tac b = "intify (k)" in not_zneg_mag [THEN subst]) ``` krauss@26056 ` 195` ```apply (rule_tac [3] zmult_mono_lemma) ``` krauss@26056 ` 196` ```apply auto ``` krauss@26056 ` 197` ```apply (simp add: znegative_iff_zless_0 not_zless_iff_zle [THEN iff_sym]) ``` krauss@26056 ` 198` ```done ``` krauss@26056 ` 199` krauss@26056 ` 200` ```lemma zmult_zle_mono1_neg: "[| i \$<= j; k \$<= #0 |] ==> j\$*k \$<= i\$*k" ``` krauss@26056 ` 201` ```apply (rule zminus_zle_zminus [THEN iffD1]) ``` krauss@26056 ` 202` ```apply (simp del: zmult_zminus_right ``` krauss@26056 ` 203` ``` add: zmult_zminus_right [symmetric] zmult_zle_mono1 zle_zminus) ``` krauss@26056 ` 204` ```done ``` krauss@26056 ` 205` krauss@26056 ` 206` ```lemma zmult_zle_mono2: "[| i \$<= j; #0 \$<= k |] ==> k\$*i \$<= k\$*j" ``` krauss@26056 ` 207` ```apply (drule zmult_zle_mono1) ``` krauss@26056 ` 208` ```apply (simp_all add: zmult_commute) ``` krauss@26056 ` 209` ```done ``` krauss@26056 ` 210` krauss@26056 ` 211` ```lemma zmult_zle_mono2_neg: "[| i \$<= j; k \$<= #0 |] ==> k\$*j \$<= k\$*i" ``` krauss@26056 ` 212` ```apply (drule zmult_zle_mono1_neg) ``` krauss@26056 ` 213` ```apply (simp_all add: zmult_commute) ``` krauss@26056 ` 214` ```done ``` krauss@26056 ` 215` krauss@26056 ` 216` ```(* \$<= monotonicity, BOTH arguments*) ``` krauss@26056 ` 217` ```lemma zmult_zle_mono: ``` krauss@26056 ` 218` ``` "[| i \$<= j; k \$<= l; #0 \$<= j; #0 \$<= k |] ==> i\$*k \$<= j\$*l" ``` krauss@26056 ` 219` ```apply (erule zmult_zle_mono1 [THEN zle_trans]) ``` krauss@26056 ` 220` ```apply assumption ``` krauss@26056 ` 221` ```apply (erule zmult_zle_mono2) ``` krauss@26056 ` 222` ```apply assumption ``` krauss@26056 ` 223` ```done ``` krauss@26056 ` 224` krauss@26056 ` 225` krauss@26056 ` 226` ```(** strict, in 1st argument; proof is by induction on k>0 **) ``` krauss@26056 ` 227` krauss@26056 ` 228` ```lemma zmult_zless_mono2_lemma [rule_format]: ``` krauss@26056 ` 229` ``` "[| i\$ nat |] ==> 0 \$#k \$* i \$< \$#k \$* j" ``` krauss@26056 ` 230` ```apply (induct_tac "k") ``` krauss@26056 ` 231` ``` prefer 2 ``` krauss@26056 ` 232` ``` apply (subst int_succ_int_1) ``` krauss@26056 ` 233` ``` apply (erule natE) ``` krauss@26056 ` 234` ```apply (simp_all add: zadd_zmult_distrib zadd_zless_mono zle_def) ``` krauss@26056 ` 235` ```apply (frule nat_0_le) ``` krauss@26056 ` 236` ```apply (subgoal_tac "i \$+ (i \$+ \$# xa \$* i) \$< j \$+ (j \$+ \$# xa \$* j) ") ``` krauss@26056 ` 237` ```apply (simp (no_asm_use)) ``` krauss@26056 ` 238` ```apply (rule zadd_zless_mono) ``` krauss@26056 ` 239` ```apply (simp_all (no_asm_simp) add: zle_def) ``` krauss@26056 ` 240` ```done ``` krauss@26056 ` 241` krauss@26056 ` 242` ```lemma zmult_zless_mono2: "[| i\$ k\$*i \$< k\$*j" ``` krauss@26056 ` 243` ```apply (subgoal_tac "intify (k) \$* i \$< intify (k) \$* j") ``` krauss@26056 ` 244` ```apply (simp (no_asm_use)) ``` krauss@26056 ` 245` ```apply (rule_tac b = "intify (k)" in not_zneg_mag [THEN subst]) ``` krauss@26056 ` 246` ```apply (rule_tac [3] zmult_zless_mono2_lemma) ``` krauss@26056 ` 247` ```apply auto ``` krauss@26056 ` 248` ```apply (simp add: znegative_iff_zless_0) ``` krauss@26056 ` 249` ```apply (drule zless_trans, assumption) ``` krauss@26056 ` 250` ```apply (auto simp add: zero_lt_zmagnitude) ``` krauss@26056 ` 251` ```done ``` krauss@26056 ` 252` krauss@26056 ` 253` ```lemma zmult_zless_mono1: "[| i\$ i\$*k \$< j\$*k" ``` krauss@26056 ` 254` ```apply (drule zmult_zless_mono2) ``` krauss@26056 ` 255` ```apply (simp_all add: zmult_commute) ``` krauss@26056 ` 256` ```done ``` krauss@26056 ` 257` krauss@26056 ` 258` ```(* < monotonicity, BOTH arguments*) ``` krauss@26056 ` 259` ```lemma zmult_zless_mono: ``` krauss@26056 ` 260` ``` "[| i \$< j; k \$< l; #0 \$< j; #0 \$< k |] ==> i\$*k \$< j\$*l" ``` krauss@26056 ` 261` ```apply (erule zmult_zless_mono1 [THEN zless_trans]) ``` krauss@26056 ` 262` ```apply assumption ``` krauss@26056 ` 263` ```apply (erule zmult_zless_mono2) ``` krauss@26056 ` 264` ```apply assumption ``` krauss@26056 ` 265` ```done ``` krauss@26056 ` 266` krauss@26056 ` 267` ```lemma zmult_zless_mono1_neg: "[| i \$< j; k \$< #0 |] ==> j\$*k \$< i\$*k" ``` krauss@26056 ` 268` ```apply (rule zminus_zless_zminus [THEN iffD1]) ``` krauss@26056 ` 269` ```apply (simp del: zmult_zminus_right ``` krauss@26056 ` 270` ``` add: zmult_zminus_right [symmetric] zmult_zless_mono1 zless_zminus) ``` krauss@26056 ` 271` ```done ``` krauss@26056 ` 272` krauss@26056 ` 273` ```lemma zmult_zless_mono2_neg: "[| i \$< j; k \$< #0 |] ==> k\$*j \$< k\$*i" ``` krauss@26056 ` 274` ```apply (rule zminus_zless_zminus [THEN iffD1]) ``` krauss@26056 ` 275` ```apply (simp del: zmult_zminus ``` krauss@26056 ` 276` ``` add: zmult_zminus [symmetric] zmult_zless_mono2 zless_zminus) ``` krauss@26056 ` 277` ```done ``` krauss@26056 ` 278` krauss@26056 ` 279` krauss@26056 ` 280` ```(** Products of zeroes **) ``` krauss@26056 ` 281` krauss@26056 ` 282` ```lemma zmult_eq_lemma: ``` krauss@26056 ` 283` ``` "[| m \ int; n \ int |] ==> (m = #0 | n = #0) <-> (m\$*n = #0)" ``` krauss@26056 ` 284` ```apply (case_tac "m \$< #0") ``` krauss@26056 ` 285` ```apply (auto simp add: not_zless_iff_zle zle_def neq_iff_zless) ``` krauss@26056 ` 286` ```apply (force dest: zmult_zless_mono1_neg zmult_zless_mono1)+ ``` krauss@26056 ` 287` ```done ``` krauss@26056 ` 288` krauss@26056 ` 289` ```lemma zmult_eq_0_iff [iff]: "(m\$*n = #0) <-> (intify(m) = #0 | intify(n) = #0)" ``` krauss@26056 ` 290` ```apply (simp add: zmult_eq_lemma) ``` krauss@26056 ` 291` ```done ``` krauss@26056 ` 292` krauss@26056 ` 293` krauss@26056 ` 294` ```(** Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =, ``` krauss@26056 ` 295` ``` but not (yet?) for k*m < n*k. **) ``` krauss@26056 ` 296` krauss@26056 ` 297` ```lemma zmult_zless_lemma: ``` krauss@26056 ` 298` ``` "[| k \ int; m \ int; n \ int |] ``` krauss@26056 ` 299` ``` ==> (m\$*k \$< n\$*k) <-> ((#0 \$< k & m\$ ((#0 \$< k & m\$ ((#0 \$< k & m\$ ((#0 \$< k --> m\$<=n) & (k \$< #0 --> n\$<=m))" ``` krauss@26056 ` 322` ```by (auto simp add: not_zless_iff_zle [THEN iff_sym] zmult_zless_cancel2) ``` krauss@26056 ` 323` krauss@26056 ` 324` ```lemma zmult_zle_cancel1: ``` krauss@26056 ` 325` ``` "(k\$*m \$<= k\$*n) <-> ((#0 \$< k --> m\$<=n) & (k \$< #0 --> n\$<=m))" ``` krauss@26056 ` 326` ```by (auto simp add: not_zless_iff_zle [THEN iff_sym] zmult_zless_cancel1) ``` krauss@26056 ` 327` krauss@26056 ` 328` ```lemma int_eq_iff_zle: "[| m \ int; n \ int |] ==> m=n <-> (m \$<= n & n \$<= m)" ``` krauss@26056 ` 329` ```apply (blast intro: zle_refl zle_anti_sym) ``` krauss@26056 ` 330` ```done ``` krauss@26056 ` 331` krauss@26056 ` 332` ```lemma zmult_cancel2_lemma: ``` krauss@26056 ` 333` ``` "[| k \ int; m \ int; n \ int |] ==> (m\$*k = n\$*k) <-> (k=#0 | m=n)" ``` krauss@26056 ` 334` ```apply (simp add: int_eq_iff_zle [of "m\$*k"] int_eq_iff_zle [of m]) ``` krauss@26056 ` 335` ```apply (auto simp add: zmult_zle_cancel2 neq_iff_zless) ``` krauss@26056 ` 336` ```done ``` krauss@26056 ` 337` krauss@26056 ` 338` ```lemma zmult_cancel2 [simp]: ``` krauss@26056 ` 339` ``` "(m\$*k = n\$*k) <-> (intify(k) = #0 | intify(m) = intify(n))" ``` krauss@26056 ` 340` ```apply (rule iff_trans) ``` krauss@26056 ` 341` ```apply (rule_tac [2] zmult_cancel2_lemma) ``` krauss@26056 ` 342` ```apply auto ``` krauss@26056 ` 343` ```done ``` krauss@26056 ` 344` krauss@26056 ` 345` ```lemma zmult_cancel1 [simp]: ``` krauss@26056 ` 346` ``` "(k\$*m = k\$*n) <-> (intify(k) = #0 | intify(m) = intify(n))" ``` krauss@26056 ` 347` ```by (simp add: zmult_commute [of k] zmult_cancel2) ``` krauss@26056 ` 348` krauss@26056 ` 349` krauss@26056 ` 350` ```subsection{* Uniqueness and monotonicity of quotients and remainders *} ``` krauss@26056 ` 351` krauss@26056 ` 352` ```lemma unique_quotient_lemma: ``` krauss@26056 ` 353` ``` "[| b\$*q' \$+ r' \$<= b\$*q \$+ r; #0 \$<= r'; #0 \$< b; r \$< b |] ``` krauss@26056 ` 354` ``` ==> q' \$<= q" ``` krauss@26056 ` 355` ```apply (subgoal_tac "r' \$+ b \$* (q'\$-q) \$<= r") ``` krauss@26056 ` 356` ``` prefer 2 apply (simp add: zdiff_zmult_distrib2 zadd_ac zcompare_rls) ``` krauss@26056 ` 357` ```apply (subgoal_tac "#0 \$< b \$* (#1 \$+ q \$- q') ") ``` krauss@26056 ` 358` ``` prefer 2 ``` krauss@26056 ` 359` ``` apply (erule zle_zless_trans) ``` krauss@26056 ` 360` ``` apply (simp add: zdiff_zmult_distrib2 zadd_zmult_distrib2 zadd_ac zcompare_rls) ``` krauss@26056 ` 361` ``` apply (erule zle_zless_trans) ``` krauss@26056 ` 362` ``` apply (simp add: ); ``` krauss@26056 ` 363` ```apply (subgoal_tac "b \$* q' \$< b \$* (#1 \$+ q)") ``` krauss@26056 ` 364` ``` prefer 2 ``` krauss@26056 ` 365` ``` apply (simp add: zdiff_zmult_distrib2 zadd_zmult_distrib2 zadd_ac zcompare_rls) ``` krauss@26056 ` 366` ```apply (auto elim: zless_asym ``` krauss@26056 ` 367` ``` simp add: zmult_zless_cancel1 zless_add1_iff_zle zadd_ac zcompare_rls) ``` krauss@26056 ` 368` ```done ``` krauss@26056 ` 369` krauss@26056 ` 370` ```lemma unique_quotient_lemma_neg: ``` krauss@26056 ` 371` ``` "[| b\$*q' \$+ r' \$<= b\$*q \$+ r; r \$<= #0; b \$< #0; b \$< r' |] ``` krauss@26056 ` 372` ``` ==> q \$<= q'" ``` krauss@26056 ` 373` ```apply (rule_tac b = "\$-b" and r = "\$-r'" and r' = "\$-r" ``` krauss@26056 ` 374` ``` in unique_quotient_lemma) ``` krauss@26056 ` 375` ```apply (auto simp del: zminus_zadd_distrib ``` krauss@26056 ` 376` ``` simp add: zminus_zadd_distrib [symmetric] zle_zminus zless_zminus) ``` krauss@26056 ` 377` ```done ``` krauss@26056 ` 378` krauss@26056 ` 379` krauss@26056 ` 380` ```lemma unique_quotient: ``` krauss@26056 ` 381` ``` "[| quorem (, ); quorem (, ); b \ int; b ~= #0; ``` krauss@26056 ` 382` ``` q \ int; q' \ int |] ==> q = q'" ``` krauss@26056 ` 383` ```apply (simp add: split_ifs quorem_def neq_iff_zless) ``` krauss@26056 ` 384` ```apply safe ``` krauss@26056 ` 385` ```apply simp_all ``` krauss@26056 ` 386` ```apply (blast intro: zle_anti_sym ``` krauss@26056 ` 387` ``` dest: zle_eq_refl [THEN unique_quotient_lemma] ``` krauss@26056 ` 388` ``` zle_eq_refl [THEN unique_quotient_lemma_neg] sym)+ ``` krauss@26056 ` 389` ```done ``` krauss@26056 ` 390` krauss@26056 ` 391` ```lemma unique_remainder: ``` krauss@26056 ` 392` ``` "[| quorem (, ); quorem (, ); b \ int; b ~= #0; ``` krauss@26056 ` 393` ``` q \ int; q' \ int; ``` krauss@26056 ` 394` ``` r \ int; r' \ int |] ==> r = r'" ``` krauss@26056 ` 395` ```apply (subgoal_tac "q = q'") ``` krauss@26056 ` 396` ``` prefer 2 apply (blast intro: unique_quotient) ``` krauss@26056 ` 397` ```apply (simp add: quorem_def) ``` krauss@26056 ` 398` ```done ``` krauss@26056 ` 399` krauss@26056 ` 400` krauss@26056 ` 401` ```subsection{*Correctness of posDivAlg, ``` krauss@26056 ` 402` ``` the Division Algorithm for @{text "a\0"} and @{text "b>0"} *} ``` krauss@26056 ` 403` krauss@26056 ` 404` ```lemma adjust_eq [simp]: ``` krauss@26056 ` 405` ``` "adjust(b, ) = (let diff = r\$-b in ``` krauss@26056 ` 406` ``` if #0 \$<= diff then <#2\$*q \$+ #1,diff> ``` krauss@26056 ` 407` ``` else <#2\$*q,r>)" ``` krauss@26056 ` 408` ```by (simp add: Let_def adjust_def) ``` krauss@26056 ` 409` krauss@26056 ` 410` krauss@26056 ` 411` ```lemma posDivAlg_termination: ``` krauss@26056 ` 412` ``` "[| #0 \$< b; ~ a \$< b |] ``` krauss@26056 ` 413` ``` ==> nat_of(a \$- #2 \$\ b \$+ #1) < nat_of(a \$- b \$+ #1)" ``` krauss@26056 ` 414` ```apply (simp (no_asm) add: zless_nat_conj) ``` krauss@26056 ` 415` ```apply (simp add: not_zless_iff_zle zless_add1_iff_zle zcompare_rls) ``` krauss@26056 ` 416` ```done ``` krauss@26056 ` 417` krauss@26056 ` 418` ```lemmas posDivAlg_unfold = def_wfrec [OF posDivAlg_def wf_measure] ``` krauss@26056 ` 419` krauss@26056 ` 420` ```lemma posDivAlg_eqn: ``` krauss@26056 ` 421` ``` "[| #0 \$< b; a \ int; b \ int |] ==> ``` krauss@26056 ` 422` ``` posDivAlg() = ``` krauss@26056 ` 423` ``` (if a\$ else adjust(b, posDivAlg ()))" ``` krauss@26056 ` 424` ```apply (rule posDivAlg_unfold [THEN trans]) ``` krauss@26056 ` 425` ```apply (simp add: vimage_iff not_zless_iff_zle [THEN iff_sym]) ``` krauss@26056 ` 426` ```apply (blast intro: posDivAlg_termination) ``` krauss@26056 ` 427` ```done ``` krauss@26056 ` 428` krauss@26056 ` 429` ```lemma posDivAlg_induct_lemma [rule_format]: ``` krauss@26056 ` 430` ``` assumes prem: ``` krauss@26056 ` 431` ``` "!!a b. [| a \ int; b \ int; ``` krauss@26056 ` 432` ``` ~ (a \$< b | b \$<= #0) --> P() |] ==> P()" ``` krauss@26056 ` 433` ``` shows " \ int*int --> P()" ``` krauss@26056 ` 434` ```apply (rule_tac a = "" in wf_induct) ``` krauss@26056 ` 435` ```apply (rule_tac A = "int*int" and f = "%.nat_of (a \$- b \$+ #1)" ``` krauss@26056 ` 436` ``` in wf_measure) ``` krauss@26056 ` 437` ```apply clarify ``` krauss@26056 ` 438` ```apply (rule prem) ``` krauss@26056 ` 439` ```apply (drule_tac [3] x = " y>" in spec) ``` krauss@26056 ` 440` ```apply auto ``` krauss@26056 ` 441` ```apply (simp add: not_zle_iff_zless posDivAlg_termination) ``` krauss@26056 ` 442` ```done ``` krauss@26056 ` 443` krauss@26056 ` 444` krauss@26056 ` 445` ```lemma posDivAlg_induct [consumes 2]: ``` krauss@26056 ` 446` ``` assumes u_int: "u \ int" ``` krauss@26056 ` 447` ``` and v_int: "v \ int" ``` krauss@26056 ` 448` ``` and ih: "!!a b. [| a \ int; b \ int; ``` krauss@26056 ` 449` ``` ~ (a \$< b | b \$<= #0) --> P(a, #2 \$* b) |] ==> P(a,b)" ``` krauss@26056 ` 450` ``` shows "P(u,v)" ``` krauss@26056 ` 451` ```apply (subgoal_tac "(%. P (x,y)) ()") ``` krauss@26056 ` 452` ```apply simp ``` krauss@26056 ` 453` ```apply (rule posDivAlg_induct_lemma) ``` krauss@26056 ` 454` ```apply (simp (no_asm_use)) ``` krauss@26056 ` 455` ```apply (rule ih) ``` krauss@26056 ` 456` ```apply (auto simp add: u_int v_int) ``` krauss@26056 ` 457` ```done ``` krauss@26056 ` 458` krauss@26056 ` 459` ```(*FIXME: use intify in integ_of so that we always have integ_of w \ int. ``` krauss@26056 ` 460` ``` then this rewrite can work for ALL constants!!*) ``` krauss@26056 ` 461` ```lemma intify_eq_0_iff_zle: "intify(m) = #0 <-> (m \$<= #0 & #0 \$<= m)" ``` krauss@26056 ` 462` ```apply (simp (no_asm) add: int_eq_iff_zle) ``` krauss@26056 ` 463` ```done ``` krauss@26056 ` 464` krauss@26056 ` 465` krauss@26056 ` 466` ```subsection{* Some convenient biconditionals for products of signs *} ``` krauss@26056 ` 467` krauss@26056 ` 468` ```lemma zmult_pos: "[| #0 \$< i; #0 \$< j |] ==> #0 \$< i \$* j" ``` krauss@26056 ` 469` ```apply (drule zmult_zless_mono1) ``` krauss@26056 ` 470` ```apply auto ``` krauss@26056 ` 471` ```done ``` krauss@26056 ` 472` krauss@26056 ` 473` ```lemma zmult_neg: "[| i \$< #0; j \$< #0 |] ==> #0 \$< i \$* j" ``` krauss@26056 ` 474` ```apply (drule zmult_zless_mono1_neg) ``` krauss@26056 ` 475` ```apply auto ``` krauss@26056 ` 476` ```done ``` krauss@26056 ` 477` krauss@26056 ` 478` ```lemma zmult_pos_neg: "[| #0 \$< i; j \$< #0 |] ==> i \$* j \$< #0" ``` krauss@26056 ` 479` ```apply (drule zmult_zless_mono1_neg) ``` krauss@26056 ` 480` ```apply auto ``` krauss@26056 ` 481` ```done ``` krauss@26056 ` 482` krauss@26056 ` 483` ```(** Inequality reasoning **) ``` krauss@26056 ` 484` krauss@26056 ` 485` ```lemma int_0_less_lemma: ``` krauss@26056 ` 486` ``` "[| x \ int; y \ int |] ``` krauss@26056 ` 487` ``` ==> (#0 \$< x \$* y) <-> (#0 \$< x & #0 \$< y | x \$< #0 & y \$< #0)" ``` krauss@26056 ` 488` ```apply (auto simp add: zle_def not_zless_iff_zle zmult_pos zmult_neg) ``` krauss@26056 ` 489` ```apply (rule ccontr) ``` krauss@26056 ` 490` ```apply (rule_tac [2] ccontr) ``` krauss@26056 ` 491` ```apply (auto simp add: zle_def not_zless_iff_zle) ``` krauss@26056 ` 492` ```apply (erule_tac P = "#0\$< x\$* y" in rev_mp) ``` krauss@26056 ` 493` ```apply (erule_tac [2] P = "#0\$< x\$* y" in rev_mp) ``` krauss@26056 ` 494` ```apply (drule zmult_pos_neg, assumption) ``` krauss@26056 ` 495` ``` prefer 2 ``` krauss@26056 ` 496` ``` apply (drule zmult_pos_neg, assumption) ``` krauss@26056 ` 497` ```apply (auto dest: zless_not_sym simp add: zmult_commute) ``` krauss@26056 ` 498` ```done ``` krauss@26056 ` 499` krauss@26056 ` 500` ```lemma int_0_less_mult_iff: ``` krauss@26056 ` 501` ``` "(#0 \$< x \$* y) <-> (#0 \$< x & #0 \$< y | x \$< #0 & y \$< #0)" ``` krauss@26056 ` 502` ```apply (cut_tac x = "intify (x)" and y = "intify (y)" in int_0_less_lemma) ``` krauss@26056 ` 503` ```apply auto ``` krauss@26056 ` 504` ```done ``` krauss@26056 ` 505` krauss@26056 ` 506` ```lemma int_0_le_lemma: ``` krauss@26056 ` 507` ``` "[| x \ int; y \ int |] ``` krauss@26056 ` 508` ``` ==> (#0 \$<= x \$* y) <-> (#0 \$<= x & #0 \$<= y | x \$<= #0 & y \$<= #0)" ``` krauss@26056 ` 509` ```by (auto simp add: zle_def not_zless_iff_zle int_0_less_mult_iff) ``` krauss@26056 ` 510` krauss@26056 ` 511` ```lemma int_0_le_mult_iff: ``` krauss@26056 ` 512` ``` "(#0 \$<= x \$* y) <-> ((#0 \$<= x & #0 \$<= y) | (x \$<= #0 & y \$<= #0))" ``` krauss@26056 ` 513` ```apply (cut_tac x = "intify (x)" and y = "intify (y)" in int_0_le_lemma) ``` krauss@26056 ` 514` ```apply auto ``` krauss@26056 ` 515` ```done ``` krauss@26056 ` 516` krauss@26056 ` 517` ```lemma zmult_less_0_iff: ``` krauss@26056 ` 518` ``` "(x \$* y \$< #0) <-> (#0 \$< x & y \$< #0 | x \$< #0 & #0 \$< y)" ``` krauss@26056 ` 519` ```apply (auto simp add: int_0_le_mult_iff not_zle_iff_zless [THEN iff_sym]) ``` krauss@26056 ` 520` ```apply (auto dest: zless_not_sym simp add: not_zle_iff_zless) ``` krauss@26056 ` 521` ```done ``` krauss@26056 ` 522` krauss@26056 ` 523` ```lemma zmult_le_0_iff: ``` krauss@26056 ` 524` ``` "(x \$* y \$<= #0) <-> (#0 \$<= x & y \$<= #0 | x \$<= #0 & #0 \$<= y)" ``` krauss@26056 ` 525` ```by (auto dest: zless_not_sym ``` krauss@26056 ` 526` ``` simp add: int_0_less_mult_iff not_zless_iff_zle [THEN iff_sym]) ``` krauss@26056 ` 527` krauss@26056 ` 528` krauss@26056 ` 529` ```(*Typechecking for posDivAlg*) ``` krauss@26056 ` 530` ```lemma posDivAlg_type [rule_format]: ``` krauss@26056 ` 531` ``` "[| a \ int; b \ int |] ==> posDivAlg() \ int * int" ``` krauss@26056 ` 532` ```apply (rule_tac u = "a" and v = "b" in posDivAlg_induct) ``` krauss@26056 ` 533` ```apply assumption+ ``` krauss@26056 ` 534` ```apply (case_tac "#0 \$< ba") ``` krauss@26056 ` 535` ``` apply (simp add: posDivAlg_eqn adjust_def integ_of_type ``` krauss@26056 ` 536` ``` split add: split_if_asm) ``` krauss@26056 ` 537` ``` apply clarify ``` krauss@26056 ` 538` ``` apply (simp add: int_0_less_mult_iff not_zle_iff_zless) ``` krauss@26056 ` 539` ```apply (simp add: not_zless_iff_zle) ``` krauss@26056 ` 540` ```apply (subst posDivAlg_unfold) ``` krauss@26056 ` 541` ```apply simp ``` krauss@26056 ` 542` ```done ``` krauss@26056 ` 543` krauss@26056 ` 544` ```(*Correctness of posDivAlg: it computes quotients correctly*) ``` krauss@26056 ` 545` ```lemma posDivAlg_correct [rule_format]: ``` krauss@26056 ` 546` ``` "[| a \ int; b \ int |] ``` krauss@26056 ` 547` ``` ==> #0 \$<= a --> #0 \$< b --> quorem (, posDivAlg())" ``` krauss@26056 ` 548` ```apply (rule_tac u = "a" and v = "b" in posDivAlg_induct) ``` krauss@26056 ` 549` ```apply auto ``` krauss@26056 ` 550` ``` apply (simp_all add: quorem_def) ``` krauss@26056 ` 551` ``` txt{*base case: a0*} ``` krauss@26056 ` 568` krauss@26056 ` 569` ```lemma negDivAlg_termination: ``` krauss@26056 ` 570` ``` "[| #0 \$< b; a \$+ b \$< #0 |] ``` krauss@26056 ` 571` ``` ==> nat_of(\$- a \$- #2 \$* b) < nat_of(\$- a \$- b)" ``` krauss@26056 ` 572` ```apply (simp (no_asm) add: zless_nat_conj) ``` krauss@26056 ` 573` ```apply (simp add: zcompare_rls not_zle_iff_zless zless_zdiff_iff [THEN iff_sym] ``` krauss@26056 ` 574` ``` zless_zminus) ``` krauss@26056 ` 575` ```done ``` krauss@26056 ` 576` krauss@26056 ` 577` ```lemmas negDivAlg_unfold = def_wfrec [OF negDivAlg_def wf_measure] ``` krauss@26056 ` 578` krauss@26056 ` 579` ```lemma negDivAlg_eqn: ``` krauss@26056 ` 580` ``` "[| #0 \$< b; a : int; b : int |] ==> ``` krauss@26056 ` 581` ``` negDivAlg() = ``` krauss@26056 ` 582` ``` (if #0 \$<= a\$+b then <#-1,a\$+b> ``` krauss@26056 ` 583` ``` else adjust(b, negDivAlg ()))" ``` krauss@26056 ` 584` ```apply (rule negDivAlg_unfold [THEN trans]) ``` krauss@26056 ` 585` ```apply (simp (no_asm_simp) add: vimage_iff not_zless_iff_zle [THEN iff_sym]) ``` krauss@26056 ` 586` ```apply (blast intro: negDivAlg_termination) ``` krauss@26056 ` 587` ```done ``` krauss@26056 ` 588` krauss@26056 ` 589` ```lemma negDivAlg_induct_lemma [rule_format]: ``` krauss@26056 ` 590` ``` assumes prem: ``` krauss@26056 ` 591` ``` "!!a b. [| a \ int; b \ int; ``` krauss@26056 ` 592` ``` ~ (#0 \$<= a \$+ b | b \$<= #0) --> P() |] ``` krauss@26056 ` 593` ``` ==> P()" ``` krauss@26056 ` 594` ``` shows " \ int*int --> P()" ``` krauss@26056 ` 595` ```apply (rule_tac a = "" in wf_induct) ``` krauss@26056 ` 596` ```apply (rule_tac A = "int*int" and f = "%.nat_of (\$- a \$- b)" ``` krauss@26056 ` 597` ``` in wf_measure) ``` krauss@26056 ` 598` ```apply clarify ``` krauss@26056 ` 599` ```apply (rule prem) ``` krauss@26056 ` 600` ```apply (drule_tac [3] x = " y>" in spec) ``` krauss@26056 ` 601` ```apply auto ``` krauss@26056 ` 602` ```apply (simp add: not_zle_iff_zless negDivAlg_termination) ``` krauss@26056 ` 603` ```done ``` krauss@26056 ` 604` krauss@26056 ` 605` ```lemma negDivAlg_induct [consumes 2]: ``` krauss@26056 ` 606` ``` assumes u_int: "u \ int" ``` krauss@26056 ` 607` ``` and v_int: "v \ int" ``` krauss@26056 ` 608` ``` and ih: "!!a b. [| a \ int; b \ int; ``` krauss@26056 ` 609` ``` ~ (#0 \$<= a \$+ b | b \$<= #0) --> P(a, #2 \$* b) |] ``` krauss@26056 ` 610` ``` ==> P(a,b)" ``` krauss@26056 ` 611` ``` shows "P(u,v)" ``` krauss@26056 ` 612` ```apply (subgoal_tac " (%. P (x,y)) ()") ``` krauss@26056 ` 613` ```apply simp ``` krauss@26056 ` 614` ```apply (rule negDivAlg_induct_lemma) ``` krauss@26056 ` 615` ```apply (simp (no_asm_use)) ``` krauss@26056 ` 616` ```apply (rule ih) ``` krauss@26056 ` 617` ```apply (auto simp add: u_int v_int) ``` krauss@26056 ` 618` ```done ``` krauss@26056 ` 619` krauss@26056 ` 620` krauss@26056 ` 621` ```(*Typechecking for negDivAlg*) ``` krauss@26056 ` 622` ```lemma negDivAlg_type: ``` krauss@26056 ` 623` ``` "[| a \ int; b \ int |] ==> negDivAlg() \ int * int" ``` krauss@26056 ` 624` ```apply (rule_tac u = "a" and v = "b" in negDivAlg_induct) ``` krauss@26056 ` 625` ```apply assumption+ ``` krauss@26056 ` 626` ```apply (case_tac "#0 \$< ba") ``` krauss@26056 ` 627` ``` apply (simp add: negDivAlg_eqn adjust_def integ_of_type ``` krauss@26056 ` 628` ``` split add: split_if_asm) ``` krauss@26056 ` 629` ``` apply clarify ``` krauss@26056 ` 630` ``` apply (simp add: int_0_less_mult_iff not_zle_iff_zless) ``` krauss@26056 ` 631` ```apply (simp add: not_zless_iff_zle) ``` krauss@26056 ` 632` ```apply (subst negDivAlg_unfold) ``` krauss@26056 ` 633` ```apply simp ``` krauss@26056 ` 634` ```done ``` krauss@26056 ` 635` krauss@26056 ` 636` krauss@26056 ` 637` ```(*Correctness of negDivAlg: it computes quotients correctly ``` krauss@26056 ` 638` ``` It doesn't work if a=0 because the 0/b=0 rather than -1*) ``` krauss@26056 ` 639` ```lemma negDivAlg_correct [rule_format]: ``` krauss@26056 ` 640` ``` "[| a \ int; b \ int |] ``` krauss@26056 ` 641` ``` ==> a \$< #0 --> #0 \$< b --> quorem (, negDivAlg())" ``` krauss@26056 ` 642` ```apply (rule_tac u = "a" and v = "b" in negDivAlg_induct) ``` krauss@26056 ` 643` ``` apply auto ``` krauss@26056 ` 644` ``` apply (simp_all add: quorem_def) ``` krauss@26056 ` 645` ``` txt{*base case: @{term "0\$<=a\$+b"}*} ``` krauss@26056 ` 646` ``` apply (simp add: negDivAlg_eqn) ``` krauss@26056 ` 647` ``` apply (simp add: not_zless_iff_zle [THEN iff_sym]) ``` krauss@26056 ` 648` ``` apply (simp add: int_0_less_mult_iff) ``` krauss@26056 ` 649` ```txt{*main argument*} ``` krauss@26056 ` 650` ```apply (subst negDivAlg_eqn) ``` krauss@26056 ` 651` ```apply (simp_all (no_asm_simp)) ``` krauss@26056 ` 652` ```apply (erule splitE) ``` krauss@26056 ` 653` ```apply (rule negDivAlg_type) ``` krauss@26056 ` 654` ```apply (simp_all add: int_0_less_mult_iff) ``` krauss@26056 ` 655` ```apply (auto simp add: zadd_zmult_distrib2 Let_def) ``` krauss@26056 ` 656` ```txt{*now just linear arithmetic*} ``` krauss@26056 ` 657` ```apply (simp add: not_zle_iff_zless zdiff_zless_iff) ``` krauss@26056 ` 658` ```done ``` krauss@26056 ` 659` krauss@26056 ` 660` krauss@26056 ` 661` ```subsection{* Existence shown by proving the division algorithm to be correct *} ``` krauss@26056 ` 662` krauss@26056 ` 663` ```(*the case a=0*) ``` krauss@26056 ` 664` ```lemma quorem_0: "[|b \ #0; b \ int|] ==> quorem (<#0,b>, <#0,#0>)" ``` krauss@26056 ` 665` ```by (force simp add: quorem_def neq_iff_zless) ``` krauss@26056 ` 666` krauss@26056 ` 667` ```lemma posDivAlg_zero_divisor: "posDivAlg() = <#0,a>" ``` krauss@26056 ` 668` ```apply (subst posDivAlg_unfold) ``` krauss@26056 ` 669` ```apply simp ``` krauss@26056 ` 670` ```done ``` krauss@26056 ` 671` krauss@26056 ` 672` ```lemma posDivAlg_0 [simp]: "posDivAlg (<#0,b>) = <#0,#0>" ``` krauss@26056 ` 673` ```apply (subst posDivAlg_unfold) ``` krauss@26056 ` 674` ```apply (simp add: not_zle_iff_zless) ``` krauss@26056 ` 675` ```done ``` krauss@26056 ` 676` krauss@26056 ` 677` krauss@26056 ` 678` ```(*Needed below. Actually it's an equivalence.*) ``` krauss@26056 ` 679` ```lemma linear_arith_lemma: "~ (#0 \$<= #-1 \$+ b) ==> (b \$<= #0)" ``` krauss@26056 ` 680` ```apply (simp add: not_zle_iff_zless) ``` krauss@26056 ` 681` ```apply (drule zminus_zless_zminus [THEN iffD2]) ``` krauss@26056 ` 682` ```apply (simp add: zadd_commute zless_add1_iff_zle zle_zminus) ``` krauss@26056 ` 683` ```done ``` krauss@26056 ` 684` krauss@26056 ` 685` ```lemma negDivAlg_minus1 [simp]: "negDivAlg (<#-1,b>) = <#-1, b\$-#1>" ``` krauss@26056 ` 686` ```apply (subst negDivAlg_unfold) ``` krauss@26056 ` 687` ```apply (simp add: linear_arith_lemma integ_of_type vimage_iff) ``` krauss@26056 ` 688` ```done ``` krauss@26056 ` 689` krauss@26056 ` 690` ```lemma negateSnd_eq [simp]: "negateSnd () = " ``` krauss@26056 ` 691` ```apply (unfold negateSnd_def) ``` krauss@26056 ` 692` ```apply auto ``` krauss@26056 ` 693` ```done ``` krauss@26056 ` 694` krauss@26056 ` 695` ```lemma negateSnd_type: "qr \ int * int ==> negateSnd (qr) \ int * int" ``` krauss@26056 ` 696` ```apply (unfold negateSnd_def) ``` krauss@26056 ` 697` ```apply auto ``` krauss@26056 ` 698` ```done ``` krauss@26056 ` 699` krauss@26056 ` 700` ```lemma quorem_neg: ``` krauss@26056 ` 701` ``` "[|quorem (<\$-a,\$-b>, qr); a \ int; b \ int; qr \ int * int|] ``` krauss@26056 ` 702` ``` ==> quorem (, negateSnd(qr))" ``` krauss@26056 ` 703` ```apply clarify ``` krauss@26056 ` 704` ```apply (auto elim: zless_asym simp add: quorem_def zless_zminus) ``` krauss@26056 ` 705` ```txt{*linear arithmetic from here on*} ``` krauss@26056 ` 706` ```apply (simp_all add: zminus_equation [of a] zminus_zless) ``` krauss@26056 ` 707` ```apply (cut_tac [2] z = "b" and w = "#0" in zless_linear) ``` krauss@26056 ` 708` ```apply (cut_tac [1] z = "b" and w = "#0" in zless_linear) ``` krauss@26056 ` 709` ```apply auto ``` krauss@26056 ` 710` ```apply (blast dest: zle_zless_trans)+ ``` krauss@26056 ` 711` ```done ``` krauss@26056 ` 712` krauss@26056 ` 713` ```lemma divAlg_correct: ``` krauss@26056 ` 714` ``` "[|b \ #0; a \ int; b \ int|] ==> quorem (, divAlg())" ``` krauss@26056 ` 715` ```apply (auto simp add: quorem_0 divAlg_def) ``` krauss@26056 ` 716` ```apply (safe intro!: quorem_neg posDivAlg_correct negDivAlg_correct ``` krauss@26056 ` 717` ``` posDivAlg_type negDivAlg_type) ``` krauss@26056 ` 718` ```apply (auto simp add: quorem_def neq_iff_zless) ``` krauss@26056 ` 719` ```txt{*linear arithmetic from here on*} ``` krauss@26056 ` 720` ```apply (auto simp add: zle_def) ``` krauss@26056 ` 721` ```done ``` krauss@26056 ` 722` krauss@26056 ` 723` ```lemma divAlg_type: "[|a \ int; b \ int|] ==> divAlg() \ int * int" ``` krauss@26056 ` 724` ```apply (auto simp add: divAlg_def) ``` krauss@26056 ` 725` ```apply (auto simp add: posDivAlg_type negDivAlg_type negateSnd_type) ``` krauss@26056 ` 726` ```done ``` krauss@26056 ` 727` krauss@26056 ` 728` krauss@26056 ` 729` ```(** intify cancellation **) ``` krauss@26056 ` 730` krauss@26056 ` 731` ```lemma zdiv_intify1 [simp]: "intify(x) zdiv y = x zdiv y" ``` krauss@26056 ` 732` ```apply (simp (no_asm) add: zdiv_def) ``` krauss@26056 ` 733` ```done ``` krauss@26056 ` 734` krauss@26056 ` 735` ```lemma zdiv_intify2 [simp]: "x zdiv intify(y) = x zdiv y" ``` krauss@26056 ` 736` ```apply (simp (no_asm) add: zdiv_def) ``` krauss@26056 ` 737` ```done ``` krauss@26056 ` 738` krauss@26056 ` 739` ```lemma zdiv_type [iff,TC]: "z zdiv w \ int" ``` krauss@26056 ` 740` ```apply (unfold zdiv_def) ``` krauss@26056 ` 741` ```apply (blast intro: fst_type divAlg_type) ``` krauss@26056 ` 742` ```done ``` krauss@26056 ` 743` krauss@26056 ` 744` ```lemma zmod_intify1 [simp]: "intify(x) zmod y = x zmod y" ``` krauss@26056 ` 745` ```apply (simp (no_asm) add: zmod_def) ``` krauss@26056 ` 746` ```done ``` krauss@26056 ` 747` krauss@26056 ` 748` ```lemma zmod_intify2 [simp]: "x zmod intify(y) = x zmod y" ``` krauss@26056 ` 749` ```apply (simp (no_asm) add: zmod_def) ``` krauss@26056 ` 750` ```done ``` krauss@26056 ` 751` krauss@26056 ` 752` ```lemma zmod_type [iff,TC]: "z zmod w \ int" ``` krauss@26056 ` 753` ```apply (unfold zmod_def) ``` krauss@26056 ` 754` ```apply (rule snd_type) ``` krauss@26056 ` 755` ```apply (blast intro: divAlg_type) ``` krauss@26056 ` 756` ```done ``` krauss@26056 ` 757` krauss@26056 ` 758` krauss@26056 ` 759` ```(** Arbitrary definitions for division by zero. Useful to simplify ``` krauss@26056 ` 760` ``` certain equations **) ``` krauss@26056 ` 761` krauss@26056 ` 762` ```lemma DIVISION_BY_ZERO_ZDIV: "a zdiv #0 = #0" ``` krauss@26056 ` 763` ```apply (simp (no_asm) add: zdiv_def divAlg_def posDivAlg_zero_divisor) ``` krauss@26056 ` 764` ```done (*NOT for adding to default simpset*) ``` krauss@26056 ` 765` krauss@26056 ` 766` ```lemma DIVISION_BY_ZERO_ZMOD: "a zmod #0 = intify(a)" ``` krauss@26056 ` 767` ```apply (simp (no_asm) add: zmod_def divAlg_def posDivAlg_zero_divisor) ``` krauss@26056 ` 768` ```done (*NOT for adding to default simpset*) ``` krauss@26056 ` 769` krauss@26056 ` 770` krauss@26056 ` 771` krauss@26056 ` 772` ```(** Basic laws about division and remainder **) ``` krauss@26056 ` 773` krauss@26056 ` 774` ```lemma raw_zmod_zdiv_equality: ``` krauss@26056 ` 775` ``` "[| a \ int; b \ int |] ==> a = b \$* (a zdiv b) \$+ (a zmod b)" ``` krauss@26056 ` 776` ```apply (case_tac "b = #0") ``` krauss@26056 ` 777` ``` apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) ``` krauss@26056 ` 778` ```apply (cut_tac a = "a" and b = "b" in divAlg_correct) ``` krauss@26056 ` 779` ```apply (auto simp add: quorem_def zdiv_def zmod_def split_def) ``` krauss@26056 ` 780` ```done ``` krauss@26056 ` 781` krauss@26056 ` 782` ```lemma zmod_zdiv_equality: "intify(a) = b \$* (a zdiv b) \$+ (a zmod b)" ``` krauss@26056 ` 783` ```apply (rule trans) ``` krauss@26056 ` 784` ```apply (rule_tac b = "intify (b)" in raw_zmod_zdiv_equality) ``` krauss@26056 ` 785` ```apply auto ``` krauss@26056 ` 786` ```done ``` krauss@26056 ` 787` krauss@26056 ` 788` ```lemma pos_mod: "#0 \$< b ==> #0 \$<= a zmod b & a zmod b \$< b" ``` krauss@26056 ` 789` ```apply (cut_tac a = "intify (a)" and b = "intify (b)" in divAlg_correct) ``` krauss@26056 ` 790` ```apply (auto simp add: intify_eq_0_iff_zle quorem_def zmod_def split_def) ``` krauss@26056 ` 791` ```apply (blast dest: zle_zless_trans)+ ``` krauss@26056 ` 792` ```done ``` krauss@26056 ` 793` krauss@26056 ` 794` ```lemmas pos_mod_sign = pos_mod [THEN conjunct1, standard] ``` krauss@26056 ` 795` ```and pos_mod_bound = pos_mod [THEN conjunct2, standard] ``` krauss@26056 ` 796` krauss@26056 ` 797` ```lemma neg_mod: "b \$< #0 ==> a zmod b \$<= #0 & b \$< a zmod b" ``` krauss@26056 ` 798` ```apply (cut_tac a = "intify (a)" and b = "intify (b)" in divAlg_correct) ``` krauss@26056 ` 799` ```apply (auto simp add: intify_eq_0_iff_zle quorem_def zmod_def split_def) ``` krauss@26056 ` 800` ```apply (blast dest: zle_zless_trans) ``` krauss@26056 ` 801` ```apply (blast dest: zless_trans)+ ``` krauss@26056 ` 802` ```done ``` krauss@26056 ` 803` krauss@26056 ` 804` ```lemmas neg_mod_sign = neg_mod [THEN conjunct1, standard] ``` krauss@26056 ` 805` ```and neg_mod_bound = neg_mod [THEN conjunct2, standard] ``` krauss@26056 ` 806` krauss@26056 ` 807` krauss@26056 ` 808` ```(** proving general properties of zdiv and zmod **) ``` krauss@26056 ` 809` krauss@26056 ` 810` ```lemma quorem_div_mod: ``` krauss@26056 ` 811` ``` "[|b \ #0; a \ int; b \ int |] ``` krauss@26056 ` 812` ``` ==> quorem (, )" ``` krauss@26056 ` 813` ```apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality) ``` krauss@26056 ` 814` ```apply (auto simp add: quorem_def neq_iff_zless pos_mod_sign pos_mod_bound ``` krauss@26056 ` 815` ``` neg_mod_sign neg_mod_bound) ``` krauss@26056 ` 816` ```done ``` krauss@26056 ` 817` krauss@26056 ` 818` ```(*Surely quorem(,) implies a \ int, but it doesn't matter*) ``` krauss@26056 ` 819` ```lemma quorem_div: ``` krauss@26056 ` 820` ``` "[| quorem(,); b \ #0; a \ int; b \ int; q \ int |] ``` krauss@26056 ` 821` ``` ==> a zdiv b = q" ``` krauss@26056 ` 822` ```by (blast intro: quorem_div_mod [THEN unique_quotient]) ``` krauss@26056 ` 823` krauss@26056 ` 824` ```lemma quorem_mod: ``` krauss@26056 ` 825` ``` "[| quorem(,); b \ #0; a \ int; b \ int; q \ int; r \ int |] ``` krauss@26056 ` 826` ``` ==> a zmod b = r" ``` krauss@26056 ` 827` ```by (blast intro: quorem_div_mod [THEN unique_remainder]) ``` krauss@26056 ` 828` krauss@26056 ` 829` ```lemma zdiv_pos_pos_trivial_raw: ``` krauss@26056 ` 830` ``` "[| a \ int; b \ int; #0 \$<= a; a \$< b |] ==> a zdiv b = #0" ``` krauss@26056 ` 831` ```apply (rule quorem_div) ``` krauss@26056 ` 832` ```apply (auto simp add: quorem_def) ``` krauss@26056 ` 833` ```(*linear arithmetic*) ``` krauss@26056 ` 834` ```apply (blast dest: zle_zless_trans)+ ``` krauss@26056 ` 835` ```done ``` krauss@26056 ` 836` krauss@26056 ` 837` ```lemma zdiv_pos_pos_trivial: "[| #0 \$<= a; a \$< b |] ==> a zdiv b = #0" ``` krauss@26056 ` 838` ```apply (cut_tac a = "intify (a)" and b = "intify (b)" ``` krauss@26056 ` 839` ``` in zdiv_pos_pos_trivial_raw) ``` krauss@26056 ` 840` ```apply auto ``` krauss@26056 ` 841` ```done ``` krauss@26056 ` 842` krauss@26056 ` 843` ```lemma zdiv_neg_neg_trivial_raw: ``` krauss@26056 ` 844` ``` "[| a \ int; b \ int; a \$<= #0; b \$< a |] ==> a zdiv b = #0" ``` krauss@26056 ` 845` ```apply (rule_tac r = "a" in quorem_div) ``` krauss@26056 ` 846` ```apply (auto simp add: quorem_def) ``` krauss@26056 ` 847` ```(*linear arithmetic*) ``` krauss@26056 ` 848` ```apply (blast dest: zle_zless_trans zless_trans)+ ``` krauss@26056 ` 849` ```done ``` krauss@26056 ` 850` krauss@26056 ` 851` ```lemma zdiv_neg_neg_trivial: "[| a \$<= #0; b \$< a |] ==> a zdiv b = #0" ``` krauss@26056 ` 852` ```apply (cut_tac a = "intify (a)" and b = "intify (b)" ``` krauss@26056 ` 853` ``` in zdiv_neg_neg_trivial_raw) ``` krauss@26056 ` 854` ```apply auto ``` krauss@26056 ` 855` ```done ``` krauss@26056 ` 856` krauss@26056 ` 857` ```lemma zadd_le_0_lemma: "[| a\$+b \$<= #0; #0 \$< a; #0 \$< b |] ==> False" ``` krauss@26056 ` 858` ```apply (drule_tac z' = "#0" and z = "b" in zadd_zless_mono) ``` krauss@26056 ` 859` ```apply (auto simp add: zle_def) ``` krauss@26056 ` 860` ```apply (blast dest: zless_trans) ``` krauss@26056 ` 861` ```done ``` krauss@26056 ` 862` krauss@26056 ` 863` ```lemma zdiv_pos_neg_trivial_raw: ``` krauss@26056 ` 864` ``` "[| a \ int; b \ int; #0 \$< a; a\$+b \$<= #0 |] ==> a zdiv b = #-1" ``` krauss@26056 ` 865` ```apply (rule_tac r = "a \$+ b" in quorem_div) ``` krauss@26056 ` 866` ```apply (auto simp add: quorem_def) ``` krauss@26056 ` 867` ```(*linear arithmetic*) ``` krauss@26056 ` 868` ```apply (blast dest: zadd_le_0_lemma zle_zless_trans)+ ``` krauss@26056 ` 869` ```done ``` krauss@26056 ` 870` krauss@26056 ` 871` ```lemma zdiv_pos_neg_trivial: "[| #0 \$< a; a\$+b \$<= #0 |] ==> a zdiv b = #-1" ``` krauss@26056 ` 872` ```apply (cut_tac a = "intify (a)" and b = "intify (b)" ``` krauss@26056 ` 873` ``` in zdiv_pos_neg_trivial_raw) ``` krauss@26056 ` 874` ```apply auto ``` krauss@26056 ` 875` ```done ``` krauss@26056 ` 876` krauss@26056 ` 877` ```(*There is no zdiv_neg_pos_trivial because #0 zdiv b = #0 would supersede it*) ``` krauss@26056 ` 878` krauss@26056 ` 879` krauss@26056 ` 880` ```lemma zmod_pos_pos_trivial_raw: ``` krauss@26056 ` 881` ``` "[| a \ int; b \ int; #0 \$<= a; a \$< b |] ==> a zmod b = a" ``` krauss@26056 ` 882` ```apply (rule_tac q = "#0" in quorem_mod) ``` krauss@26056 ` 883` ```apply (auto simp add: quorem_def) ``` krauss@26056 ` 884` ```(*linear arithmetic*) ``` krauss@26056 ` 885` ```apply (blast dest: zle_zless_trans)+ ``` krauss@26056 ` 886` ```done ``` krauss@26056 ` 887` krauss@26056 ` 888` ```lemma zmod_pos_pos_trivial: "[| #0 \$<= a; a \$< b |] ==> a zmod b = intify(a)" ``` krauss@26056 ` 889` ```apply (cut_tac a = "intify (a)" and b = "intify (b)" ``` krauss@26056 ` 890` ``` in zmod_pos_pos_trivial_raw) ``` krauss@26056 ` 891` ```apply auto ``` krauss@26056 ` 892` ```done ``` krauss@26056 ` 893` krauss@26056 ` 894` ```lemma zmod_neg_neg_trivial_raw: ``` krauss@26056 ` 895` ``` "[| a \ int; b \ int; a \$<= #0; b \$< a |] ==> a zmod b = a" ``` krauss@26056 ` 896` ```apply (rule_tac q = "#0" in quorem_mod) ``` krauss@26056 ` 897` ```apply (auto simp add: quorem_def) ``` krauss@26056 ` 898` ```(*linear arithmetic*) ``` krauss@26056 ` 899` ```apply (blast dest: zle_zless_trans zless_trans)+ ``` krauss@26056 ` 900` ```done ``` krauss@26056 ` 901` krauss@26056 ` 902` ```lemma zmod_neg_neg_trivial: "[| a \$<= #0; b \$< a |] ==> a zmod b = intify(a)" ``` krauss@26056 ` 903` ```apply (cut_tac a = "intify (a)" and b = "intify (b)" ``` krauss@26056 ` 904` ``` in zmod_neg_neg_trivial_raw) ``` krauss@26056 ` 905` ```apply auto ``` krauss@26056 ` 906` ```done ``` krauss@26056 ` 907` krauss@26056 ` 908` ```lemma zmod_pos_neg_trivial_raw: ``` krauss@26056 ` 909` ``` "[| a \ int; b \ int; #0 \$< a; a\$+b \$<= #0 |] ==> a zmod b = a\$+b" ``` krauss@26056 ` 910` ```apply (rule_tac q = "#-1" in quorem_mod) ``` krauss@26056 ` 911` ```apply (auto simp add: quorem_def) ``` krauss@26056 ` 912` ```(*linear arithmetic*) ``` krauss@26056 ` 913` ```apply (blast dest: zadd_le_0_lemma zle_zless_trans)+ ``` krauss@26056 ` 914` ```done ``` krauss@26056 ` 915` krauss@26056 ` 916` ```lemma zmod_pos_neg_trivial: "[| #0 \$< a; a\$+b \$<= #0 |] ==> a zmod b = a\$+b" ``` krauss@26056 ` 917` ```apply (cut_tac a = "intify (a)" and b = "intify (b)" ``` krauss@26056 ` 918` ``` in zmod_pos_neg_trivial_raw) ``` krauss@26056 ` 919` ```apply auto ``` krauss@26056 ` 920` ```done ``` krauss@26056 ` 921` krauss@26056 ` 922` ```(*There is no zmod_neg_pos_trivial...*) ``` krauss@26056 ` 923` krauss@26056 ` 924` krauss@26056 ` 925` ```(*Simpler laws such as -a zdiv b = -(a zdiv b) FAIL*) ``` krauss@26056 ` 926` krauss@26056 ` 927` ```lemma zdiv_zminus_zminus_raw: ``` krauss@26056 ` 928` ``` "[|a \ int; b \ int|] ==> (\$-a) zdiv (\$-b) = a zdiv b" ``` krauss@26056 ` 929` ```apply (case_tac "b = #0") ``` krauss@26056 ` 930` ``` apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) ``` krauss@26056 ` 931` ```apply (subst quorem_div_mod [THEN quorem_neg, simplified, THEN quorem_div]) ``` krauss@26056 ` 932` ```apply auto ``` krauss@26056 ` 933` ```done ``` krauss@26056 ` 934` krauss@26056 ` 935` ```lemma zdiv_zminus_zminus [simp]: "(\$-a) zdiv (\$-b) = a zdiv b" ``` krauss@26056 ` 936` ```apply (cut_tac a = "intify (a)" and b = "intify (b)" in zdiv_zminus_zminus_raw) ``` krauss@26056 ` 937` ```apply auto ``` krauss@26056 ` 938` ```done ``` krauss@26056 ` 939` krauss@26056 ` 940` ```(*Simpler laws such as -a zmod b = -(a zmod b) FAIL*) ``` krauss@26056 ` 941` ```lemma zmod_zminus_zminus_raw: ``` krauss@26056 ` 942` ``` "[|a \ int; b \ int|] ==> (\$-a) zmod (\$-b) = \$- (a zmod b)" ``` krauss@26056 ` 943` ```apply (case_tac "b = #0") ``` krauss@26056 ` 944` ``` apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) ``` krauss@26056 ` 945` ```apply (subst quorem_div_mod [THEN quorem_neg, simplified, THEN quorem_mod]) ``` krauss@26056 ` 946` ```apply auto ``` krauss@26056 ` 947` ```done ``` krauss@26056 ` 948` krauss@26056 ` 949` ```lemma zmod_zminus_zminus [simp]: "(\$-a) zmod (\$-b) = \$- (a zmod b)" ``` krauss@26056 ` 950` ```apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_zminus_zminus_raw) ``` krauss@26056 ` 951` ```apply auto ``` krauss@26056 ` 952` ```done ``` krauss@26056 ` 953` krauss@26056 ` 954` krauss@26056 ` 955` ```subsection{* division of a number by itself *} ``` krauss@26056 ` 956` krauss@26056 ` 957` ```lemma self_quotient_aux1: "[| #0 \$< a; a = r \$+ a\$*q; r \$< a |] ==> #1 \$<= q" ``` krauss@26056 ` 958` ```apply (subgoal_tac "#0 \$< a\$*q") ``` krauss@26056 ` 959` ```apply (cut_tac w = "#0" and z = "q" in add1_zle_iff) ``` krauss@26056 ` 960` ```apply (simp add: int_0_less_mult_iff) ``` krauss@26056 ` 961` ```apply (blast dest: zless_trans) ``` krauss@26056 ` 962` ```(*linear arithmetic...*) ``` krauss@26056 ` 963` ```apply (drule_tac t = "%x. x \$- r" in subst_context) ``` krauss@26056 ` 964` ```apply (drule sym) ``` krauss@26056 ` 965` ```apply (simp add: zcompare_rls) ``` krauss@26056 ` 966` ```done ``` krauss@26056 ` 967` krauss@26056 ` 968` ```lemma self_quotient_aux2: "[| #0 \$< a; a = r \$+ a\$*q; #0 \$<= r |] ==> q \$<= #1" ``` krauss@26056 ` 969` ```apply (subgoal_tac "#0 \$<= a\$* (#1\$-q)") ``` krauss@26056 ` 970` ``` apply (simp add: int_0_le_mult_iff zcompare_rls) ``` krauss@26056 ` 971` ``` apply (blast dest: zle_zless_trans) ``` krauss@26056 ` 972` ```apply (simp add: zdiff_zmult_distrib2) ``` krauss@26056 ` 973` ```apply (drule_tac t = "%x. x \$- a \$* q" in subst_context) ``` krauss@26056 ` 974` ```apply (simp add: zcompare_rls) ``` krauss@26056 ` 975` ```done ``` krauss@26056 ` 976` krauss@26056 ` 977` ```lemma self_quotient: ``` krauss@26056 ` 978` ``` "[| quorem(,); a \ int; q \ int; a \ #0|] ==> q = #1" ``` krauss@26056 ` 979` ```apply (simp add: split_ifs quorem_def neq_iff_zless) ``` krauss@26056 ` 980` ```apply (rule zle_anti_sym) ``` krauss@26056 ` 981` ```apply safe ``` krauss@26056 ` 982` ```apply auto ``` krauss@26056 ` 983` ```prefer 4 apply (blast dest: zless_trans) ``` krauss@26056 ` 984` ```apply (blast dest: zless_trans) ``` krauss@26056 ` 985` ```apply (rule_tac [3] a = "\$-a" and r = "\$-r" in self_quotient_aux1) ``` krauss@26056 ` 986` ```apply (rule_tac a = "\$-a" and r = "\$-r" in self_quotient_aux2) ``` krauss@26056 ` 987` ```apply (rule_tac [6] zminus_equation [THEN iffD1]) ``` krauss@26056 ` 988` ```apply (rule_tac [2] zminus_equation [THEN iffD1]) ``` krauss@26056 ` 989` ```apply (force intro: self_quotient_aux1 self_quotient_aux2 ``` krauss@26056 ` 990` ``` simp add: zadd_commute zmult_zminus)+ ``` krauss@26056 ` 991` ```done ``` krauss@26056 ` 992` krauss@26056 ` 993` ```lemma self_remainder: ``` krauss@26056 ` 994` ``` "[|quorem(,); a \ int; q \ int; r \ int; a \ #0|] ==> r = #0" ``` krauss@26056 ` 995` ```apply (frule self_quotient) ``` krauss@26056 ` 996` ```apply (auto simp add: quorem_def) ``` krauss@26056 ` 997` ```done ``` krauss@26056 ` 998` krauss@26056 ` 999` ```lemma zdiv_self_raw: "[|a \ #0; a \ int|] ==> a zdiv a = #1" ``` krauss@26056 ` 1000` ```apply (blast intro: quorem_div_mod [THEN self_quotient]) ``` krauss@26056 ` 1001` ```done ``` krauss@26056 ` 1002` krauss@26056 ` 1003` ```lemma zdiv_self [simp]: "intify(a) \ #0 ==> a zdiv a = #1" ``` krauss@26056 ` 1004` ```apply (drule zdiv_self_raw) ``` krauss@26056 ` 1005` ```apply auto ``` krauss@26056 ` 1006` ```done ``` krauss@26056 ` 1007` krauss@26056 ` 1008` ```(*Here we have 0 zmod 0 = 0, also assumed by Knuth (who puts m zmod 0 = 0) *) ``` krauss@26056 ` 1009` ```lemma zmod_self_raw: "a \ int ==> a zmod a = #0" ``` krauss@26056 ` 1010` ```apply (case_tac "a = #0") ``` krauss@26056 ` 1011` ``` apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) ``` krauss@26056 ` 1012` ```apply (blast intro: quorem_div_mod [THEN self_remainder]) ``` krauss@26056 ` 1013` ```done ``` krauss@26056 ` 1014` krauss@26056 ` 1015` ```lemma zmod_self [simp]: "a zmod a = #0" ``` krauss@26056 ` 1016` ```apply (cut_tac a = "intify (a)" in zmod_self_raw) ``` krauss@26056 ` 1017` ```apply auto ``` krauss@26056 ` 1018` ```done ``` krauss@26056 ` 1019` krauss@26056 ` 1020` krauss@26056 ` 1021` ```subsection{* Computation of division and remainder *} ``` krauss@26056 ` 1022` krauss@26056 ` 1023` ```lemma zdiv_zero [simp]: "#0 zdiv b = #0" ``` krauss@26056 ` 1024` ```apply (simp (no_asm) add: zdiv_def divAlg_def) ``` krauss@26056 ` 1025` ```done ``` krauss@26056 ` 1026` krauss@26056 ` 1027` ```lemma zdiv_eq_minus1: "#0 \$< b ==> #-1 zdiv b = #-1" ``` krauss@26056 ` 1028` ```apply (simp (no_asm_simp) add: zdiv_def divAlg_def) ``` krauss@26056 ` 1029` ```done ``` krauss@26056 ` 1030` krauss@26056 ` 1031` ```lemma zmod_zero [simp]: "#0 zmod b = #0" ``` krauss@26056 ` 1032` ```apply (simp (no_asm) add: zmod_def divAlg_def) ``` krauss@26056 ` 1033` ```done ``` krauss@26056 ` 1034` krauss@26056 ` 1035` ```lemma zdiv_minus1: "#0 \$< b ==> #-1 zdiv b = #-1" ``` krauss@26056 ` 1036` ```apply (simp (no_asm_simp) add: zdiv_def divAlg_def) ``` krauss@26056 ` 1037` ```done ``` krauss@26056 ` 1038` krauss@26056 ` 1039` ```lemma zmod_minus1: "#0 \$< b ==> #-1 zmod b = b \$- #1" ``` krauss@26056 ` 1040` ```apply (simp (no_asm_simp) add: zmod_def divAlg_def) ``` krauss@26056 ` 1041` ```done ``` krauss@26056 ` 1042` krauss@26056 ` 1043` ```(** a positive, b positive **) ``` krauss@26056 ` 1044` krauss@26056 ` 1045` ```lemma zdiv_pos_pos: "[| #0 \$< a; #0 \$<= b |] ``` krauss@26056 ` 1046` ``` ==> a zdiv b = fst (posDivAlg())" ``` krauss@26056 ` 1047` ```apply (simp (no_asm_simp) add: zdiv_def divAlg_def) ``` krauss@26056 ` 1048` ```apply (auto simp add: zle_def) ``` krauss@26056 ` 1049` ```done ``` krauss@26056 ` 1050` krauss@26056 ` 1051` ```lemma zmod_pos_pos: ``` krauss@26056 ` 1052` ``` "[| #0 \$< a; #0 \$<= b |] ``` krauss@26056 ` 1053` ``` ==> a zmod b = snd (posDivAlg())" ``` krauss@26056 ` 1054` ```apply (simp (no_asm_simp) add: zmod_def divAlg_def) ``` krauss@26056 ` 1055` ```apply (auto simp add: zle_def) ``` krauss@26056 ` 1056` ```done ``` krauss@26056 ` 1057` krauss@26056 ` 1058` ```(** a negative, b positive **) ``` krauss@26056 ` 1059` krauss@26056 ` 1060` ```lemma zdiv_neg_pos: ``` krauss@26056 ` 1061` ``` "[| a \$< #0; #0 \$< b |] ``` krauss@26056 ` 1062` ``` ==> a zdiv b = fst (negDivAlg())" ``` krauss@26056 ` 1063` ```apply (simp (no_asm_simp) add: zdiv_def divAlg_def) ``` krauss@26056 ` 1064` ```apply (blast dest: zle_zless_trans) ``` krauss@26056 ` 1065` ```done ``` krauss@26056 ` 1066` krauss@26056 ` 1067` ```lemma zmod_neg_pos: ``` krauss@26056 ` 1068` ``` "[| a \$< #0; #0 \$< b |] ``` krauss@26056 ` 1069` ``` ==> a zmod b = snd (negDivAlg())" ``` krauss@26056 ` 1070` ```apply (simp (no_asm_simp) add: zmod_def divAlg_def) ``` krauss@26056 ` 1071` ```apply (blast dest: zle_zless_trans) ``` krauss@26056 ` 1072` ```done ``` krauss@26056 ` 1073` krauss@26056 ` 1074` ```(** a positive, b negative **) ``` krauss@26056 ` 1075` krauss@26056 ` 1076` ```lemma zdiv_pos_neg: ``` krauss@26056 ` 1077` ``` "[| #0 \$< a; b \$< #0 |] ``` krauss@26056 ` 1078` ``` ==> a zdiv b = fst (negateSnd(negDivAlg (<\$-a, \$-b>)))" ``` krauss@26056 ` 1079` ```apply (simp (no_asm_simp) add: zdiv_def divAlg_def intify_eq_0_iff_zle) ``` krauss@26056 ` 1080` ```apply auto ``` krauss@26056 ` 1081` ```apply (blast dest: zle_zless_trans)+ ``` krauss@26056 ` 1082` ```apply (blast dest: zless_trans) ``` krauss@26056 ` 1083` ```apply (blast intro: zless_imp_zle) ``` krauss@26056 ` 1084` ```done ``` krauss@26056 ` 1085` krauss@26056 ` 1086` ```lemma zmod_pos_neg: ``` krauss@26056 ` 1087` ``` "[| #0 \$< a; b \$< #0 |] ``` krauss@26056 ` 1088` ``` ==> a zmod b = snd (negateSnd(negDivAlg (<\$-a, \$-b>)))" ``` krauss@26056 ` 1089` ```apply (simp (no_asm_simp) add: zmod_def divAlg_def intify_eq_0_iff_zle) ``` krauss@26056 ` 1090` ```apply auto ``` krauss@26056 ` 1091` ```apply (blast dest: zle_zless_trans)+ ``` krauss@26056 ` 1092` ```apply (blast dest: zless_trans) ``` krauss@26056 ` 1093` ```apply (blast intro: zless_imp_zle) ``` krauss@26056 ` 1094` ```done ``` krauss@26056 ` 1095` krauss@26056 ` 1096` ```(** a negative, b negative **) ``` krauss@26056 ` 1097` krauss@26056 ` 1098` ```lemma zdiv_neg_neg: ``` krauss@26056 ` 1099` ``` "[| a \$< #0; b \$<= #0 |] ``` krauss@26056 ` 1100` ``` ==> a zdiv b = fst (negateSnd(posDivAlg(<\$-a, \$-b>)))" ``` krauss@26056 ` 1101` ```apply (simp (no_asm_simp) add: zdiv_def divAlg_def) ``` krauss@26056 ` 1102` ```apply auto ``` krauss@26056 ` 1103` ```apply (blast dest!: zle_zless_trans)+ ``` krauss@26056 ` 1104` ```done ``` krauss@26056 ` 1105` krauss@26056 ` 1106` ```lemma zmod_neg_neg: ``` krauss@26056 ` 1107` ``` "[| a \$< #0; b \$<= #0 |] ``` krauss@26056 ` 1108` ``` ==> a zmod b = snd (negateSnd(posDivAlg(<\$-a, \$-b>)))" ``` krauss@26056 ` 1109` ```apply (simp (no_asm_simp) add: zmod_def divAlg_def) ``` krauss@26056 ` 1110` ```apply auto ``` krauss@26056 ` 1111` ```apply (blast dest!: zle_zless_trans)+ ``` krauss@26056 ` 1112` ```done ``` krauss@26056 ` 1113` krauss@26056 ` 1114` ```declare zdiv_pos_pos [of "integ_of (v)" "integ_of (w)", standard, simp] ``` krauss@26056 ` 1115` ```declare zdiv_neg_pos [of "integ_of (v)" "integ_of (w)", standard, simp] ``` krauss@26056 ` 1116` ```declare zdiv_pos_neg [of "integ_of (v)" "integ_of (w)", standard, simp] ``` krauss@26056 ` 1117` ```declare zdiv_neg_neg [of "integ_of (v)" "integ_of (w)", standard, simp] ``` krauss@26056 ` 1118` ```declare zmod_pos_pos [of "integ_of (v)" "integ_of (w)", standard, simp] ``` krauss@26056 ` 1119` ```declare zmod_neg_pos [of "integ_of (v)" "integ_of (w)", standard, simp] ``` krauss@26056 ` 1120` ```declare zmod_pos_neg [of "integ_of (v)" "integ_of (w)", standard, simp] ``` krauss@26056 ` 1121` ```declare zmod_neg_neg [of "integ_of (v)" "integ_of (w)", standard, simp] ``` krauss@26056 ` 1122` ```declare posDivAlg_eqn [of concl: "integ_of (v)" "integ_of (w)", standard, simp] ``` krauss@26056 ` 1123` ```declare negDivAlg_eqn [of concl: "integ_of (v)" "integ_of (w)", standard, simp] ``` krauss@26056 ` 1124` krauss@26056 ` 1125` krauss@26056 ` 1126` ```(** Special-case simplification **) ``` krauss@26056 ` 1127` krauss@26056 ` 1128` ```lemma zmod_1 [simp]: "a zmod #1 = #0" ``` krauss@26056 ` 1129` ```apply (cut_tac a = "a" and b = "#1" in pos_mod_sign) ``` krauss@26056 ` 1130` ```apply (cut_tac [2] a = "a" and b = "#1" in pos_mod_bound) ``` krauss@26056 ` 1131` ```apply auto ``` krauss@26056 ` 1132` ```(*arithmetic*) ``` krauss@26056 ` 1133` ```apply (drule add1_zle_iff [THEN iffD2]) ``` krauss@26056 ` 1134` ```apply (rule zle_anti_sym) ``` krauss@26056 ` 1135` ```apply auto ``` krauss@26056 ` 1136` ```done ``` krauss@26056 ` 1137` krauss@26056 ` 1138` ```lemma zdiv_1 [simp]: "a zdiv #1 = intify(a)" ``` krauss@26056 ` 1139` ```apply (cut_tac a = "a" and b = "#1" in zmod_zdiv_equality) ``` krauss@26056 ` 1140` ```apply auto ``` krauss@26056 ` 1141` ```done ``` krauss@26056 ` 1142` krauss@26056 ` 1143` ```lemma zmod_minus1_right [simp]: "a zmod #-1 = #0" ``` krauss@26056 ` 1144` ```apply (cut_tac a = "a" and b = "#-1" in neg_mod_sign) ``` krauss@26056 ` 1145` ```apply (cut_tac [2] a = "a" and b = "#-1" in neg_mod_bound) ``` krauss@26056 ` 1146` ```apply auto ``` krauss@26056 ` 1147` ```(*arithmetic*) ``` krauss@26056 ` 1148` ```apply (drule add1_zle_iff [THEN iffD2]) ``` krauss@26056 ` 1149` ```apply (rule zle_anti_sym) ``` krauss@26056 ` 1150` ```apply auto ``` krauss@26056 ` 1151` ```done ``` krauss@26056 ` 1152` krauss@26056 ` 1153` ```lemma zdiv_minus1_right_raw: "a \ int ==> a zdiv #-1 = \$-a" ``` krauss@26056 ` 1154` ```apply (cut_tac a = "a" and b = "#-1" in zmod_zdiv_equality) ``` krauss@26056 ` 1155` ```apply auto ``` krauss@26056 ` 1156` ```apply (rule equation_zminus [THEN iffD2]) ``` krauss@26056 ` 1157` ```apply auto ``` krauss@26056 ` 1158` ```done ``` krauss@26056 ` 1159` krauss@26056 ` 1160` ```lemma zdiv_minus1_right: "a zdiv #-1 = \$-a" ``` krauss@26056 ` 1161` ```apply (cut_tac a = "intify (a)" in zdiv_minus1_right_raw) ``` krauss@26056 ` 1162` ```apply auto ``` krauss@26056 ` 1163` ```done ``` krauss@26056 ` 1164` ```declare zdiv_minus1_right [simp] ``` krauss@26056 ` 1165` krauss@26056 ` 1166` krauss@26056 ` 1167` ```subsection{* Monotonicity in the first argument (divisor) *} ``` krauss@26056 ` 1168` krauss@26056 ` 1169` ```lemma zdiv_mono1: "[| a \$<= a'; #0 \$< b |] ==> a zdiv b \$<= a' zdiv b" ``` krauss@26056 ` 1170` ```apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality) ``` krauss@26056 ` 1171` ```apply (cut_tac a = "a'" and b = "b" in zmod_zdiv_equality) ``` krauss@26056 ` 1172` ```apply (rule unique_quotient_lemma) ``` krauss@26056 ` 1173` ```apply (erule subst) ``` krauss@26056 ` 1174` ```apply (erule subst) ``` krauss@26056 ` 1175` ```apply (simp_all (no_asm_simp) add: pos_mod_sign pos_mod_bound) ``` krauss@26056 ` 1176` ```done ``` krauss@26056 ` 1177` krauss@26056 ` 1178` ```lemma zdiv_mono1_neg: "[| a \$<= a'; b \$< #0 |] ==> a' zdiv b \$<= a zdiv b" ``` krauss@26056 ` 1179` ```apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality) ``` krauss@26056 ` 1180` ```apply (cut_tac a = "a'" and b = "b" in zmod_zdiv_equality) ``` krauss@26056 ` 1181` ```apply (rule unique_quotient_lemma_neg) ``` krauss@26056 ` 1182` ```apply (erule subst) ``` krauss@26056 ` 1183` ```apply (erule subst) ``` krauss@26056 ` 1184` ```apply (simp_all (no_asm_simp) add: neg_mod_sign neg_mod_bound) ``` krauss@26056 ` 1185` ```done ``` krauss@26056 ` 1186` krauss@26056 ` 1187` krauss@26056 ` 1188` ```subsection{* Monotonicity in the second argument (dividend) *} ``` krauss@26056 ` 1189` krauss@26056 ` 1190` ```lemma q_pos_lemma: ``` krauss@26056 ` 1191` ``` "[| #0 \$<= b'\$*q' \$+ r'; r' \$< b'; #0 \$< b' |] ==> #0 \$<= q'" ``` krauss@26056 ` 1192` ```apply (subgoal_tac "#0 \$< b'\$* (q' \$+ #1)") ``` krauss@26056 ` 1193` ``` apply (simp add: int_0_less_mult_iff) ``` krauss@26056 ` 1194` ``` apply (blast dest: zless_trans intro: zless_add1_iff_zle [THEN iffD1]) ``` krauss@26056 ` 1195` ```apply (simp add: zadd_zmult_distrib2) ``` krauss@26056 ` 1196` ```apply (erule zle_zless_trans) ``` krauss@26056 ` 1197` ```apply (erule zadd_zless_mono2) ``` krauss@26056 ` 1198` ```done ``` krauss@26056 ` 1199` krauss@26056 ` 1200` ```lemma zdiv_mono2_lemma: ``` krauss@26056 ` 1201` ``` "[| b\$*q \$+ r = b'\$*q' \$+ r'; #0 \$<= b'\$*q' \$+ r'; ``` krauss@26056 ` 1202` ``` r' \$< b'; #0 \$<= r; #0 \$< b'; b' \$<= b |] ``` krauss@26056 ` 1203` ``` ==> q \$<= q'" ``` krauss@26056 ` 1204` ```apply (frule q_pos_lemma, assumption+) ``` krauss@26056 ` 1205` ```apply (subgoal_tac "b\$*q \$< b\$* (q' \$+ #1)") ``` krauss@26056 ` 1206` ``` apply (simp add: zmult_zless_cancel1) ``` krauss@26056 ` 1207` ``` apply (force dest: zless_add1_iff_zle [THEN iffD1] zless_trans zless_zle_trans) ``` krauss@26056 ` 1208` ```apply (subgoal_tac "b\$*q = r' \$- r \$+ b'\$*q'") ``` krauss@26056 ` 1209` ``` prefer 2 apply (simp add: zcompare_rls) ``` krauss@26056 ` 1210` ```apply (simp (no_asm_simp) add: zadd_zmult_distrib2) ``` krauss@26056 ` 1211` ```apply (subst zadd_commute [of "b \$\ q'"], rule zadd_zless_mono) ``` krauss@26056 ` 1212` ``` prefer 2 apply (blast intro: zmult_zle_mono1) ``` krauss@26056 ` 1213` ```apply (subgoal_tac "r' \$+ #0 \$< b \$+ r") ``` krauss@26056 ` 1214` ``` apply (simp add: zcompare_rls) ``` krauss@26056 ` 1215` ```apply (rule zadd_zless_mono) ``` krauss@26056 ` 1216` ``` apply auto ``` krauss@26056 ` 1217` ```apply (blast dest: zless_zle_trans) ``` krauss@26056 ` 1218` ```done ``` krauss@26056 ` 1219` krauss@26056 ` 1220` krauss@26056 ` 1221` ```lemma zdiv_mono2_raw: ``` krauss@26056 ` 1222` ``` "[| #0 \$<= a; #0 \$< b'; b' \$<= b; a \ int |] ``` krauss@26056 ` 1223` ``` ==> a zdiv b \$<= a zdiv b'" ``` krauss@26056 ` 1224` ```apply (subgoal_tac "#0 \$< b") ``` krauss@26056 ` 1225` ``` prefer 2 apply (blast dest: zless_zle_trans) ``` krauss@26056 ` 1226` ```apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality) ``` krauss@26056 ` 1227` ```apply (cut_tac a = "a" and b = "b'" in zmod_zdiv_equality) ``` krauss@26056 ` 1228` ```apply (rule zdiv_mono2_lemma) ``` krauss@26056 ` 1229` ```apply (erule subst) ``` krauss@26056 ` 1230` ```apply (erule subst) ``` krauss@26056 ` 1231` ```apply (simp_all add: pos_mod_sign pos_mod_bound) ``` krauss@26056 ` 1232` ```done ``` krauss@26056 ` 1233` krauss@26056 ` 1234` ```lemma zdiv_mono2: ``` krauss@26056 ` 1235` ``` "[| #0 \$<= a; #0 \$< b'; b' \$<= b |] ``` krauss@26056 ` 1236` ``` ==> a zdiv b \$<= a zdiv b'" ``` krauss@26056 ` 1237` ```apply (cut_tac a = "intify (a)" in zdiv_mono2_raw) ``` krauss@26056 ` 1238` ```apply auto ``` krauss@26056 ` 1239` ```done ``` krauss@26056 ` 1240` krauss@26056 ` 1241` ```lemma q_neg_lemma: ``` krauss@26056 ` 1242` ``` "[| b'\$*q' \$+ r' \$< #0; #0 \$<= r'; #0 \$< b' |] ==> q' \$< #0" ``` krauss@26056 ` 1243` ```apply (subgoal_tac "b'\$*q' \$< #0") ``` krauss@26056 ` 1244` ``` prefer 2 apply (force intro: zle_zless_trans) ``` krauss@26056 ` 1245` ```apply (simp add: zmult_less_0_iff) ``` krauss@26056 ` 1246` ```apply (blast dest: zless_trans) ``` krauss@26056 ` 1247` ```done ``` krauss@26056 ` 1248` krauss@26056 ` 1249` krauss@26056 ` 1250` krauss@26056 ` 1251` ```lemma zdiv_mono2_neg_lemma: ``` krauss@26056 ` 1252` ``` "[| b\$*q \$+ r = b'\$*q' \$+ r'; b'\$*q' \$+ r' \$< #0; ``` krauss@26056 ` 1253` ``` r \$< b; #0 \$<= r'; #0 \$< b'; b' \$<= b |] ``` krauss@26056 ` 1254` ``` ==> q' \$<= q" ``` krauss@26056 ` 1255` ```apply (subgoal_tac "#0 \$< b") ``` krauss@26056 ` 1256` ``` prefer 2 apply (blast dest: zless_zle_trans) ``` krauss@26056 ` 1257` ```apply (frule q_neg_lemma, assumption+) ``` krauss@26056 ` 1258` ```apply (subgoal_tac "b\$*q' \$< b\$* (q \$+ #1)") ``` krauss@26056 ` 1259` ``` apply (simp add: zmult_zless_cancel1) ``` krauss@26056 ` 1260` ``` apply (blast dest: zless_trans zless_add1_iff_zle [THEN iffD1]) ``` krauss@26056 ` 1261` ```apply (simp (no_asm_simp) add: zadd_zmult_distrib2) ``` krauss@26056 ` 1262` ```apply (subgoal_tac "b\$*q' \$<= b'\$*q'") ``` krauss@26056 ` 1263` ``` prefer 2 ``` krauss@26056 ` 1264` ``` apply (simp add: zmult_zle_cancel2) ``` krauss@26056 ` 1265` ``` apply (blast dest: zless_trans) ``` krauss@26056 ` 1266` ```apply (subgoal_tac "b'\$*q' \$+ r \$< b \$+ (b\$*q \$+ r)") ``` krauss@26056 ` 1267` ``` prefer 2 ``` krauss@26056 ` 1268` ``` apply (erule ssubst) ``` krauss@26056 ` 1269` ``` apply simp ``` krauss@26056 ` 1270` ``` apply (drule_tac w' = "r" and z' = "#0" in zadd_zless_mono) ``` krauss@26056 ` 1271` ``` apply (assumption) ``` krauss@26056 ` 1272` ``` apply simp ``` krauss@26056 ` 1273` ```apply (simp (no_asm_use) add: zadd_commute) ``` krauss@26056 ` 1274` ```apply (rule zle_zless_trans) ``` krauss@26056 ` 1275` ``` prefer 2 apply (assumption) ``` krauss@26056 ` 1276` ```apply (simp (no_asm_simp) add: zmult_zle_cancel2) ``` krauss@26056 ` 1277` ```apply (blast dest: zless_trans) ``` krauss@26056 ` 1278` ```done ``` krauss@26056 ` 1279` krauss@26056 ` 1280` ```lemma zdiv_mono2_neg_raw: ``` krauss@26056 ` 1281` ``` "[| a \$< #0; #0 \$< b'; b' \$<= b; a \ int |] ``` krauss@26056 ` 1282` ``` ==> a zdiv b' \$<= a zdiv b" ``` krauss@26056 ` 1283` ```apply (subgoal_tac "#0 \$< b") ``` krauss@26056 ` 1284` ``` prefer 2 apply (blast dest: zless_zle_trans) ``` krauss@26056 ` 1285` ```apply (cut_tac a = "a" and b = "b" in zmod_zdiv_equality) ``` krauss@26056 ` 1286` ```apply (cut_tac a = "a" and b = "b'" in zmod_zdiv_equality) ``` krauss@26056 ` 1287` ```apply (rule zdiv_mono2_neg_lemma) ``` krauss@26056 ` 1288` ```apply (erule subst) ``` krauss@26056 ` 1289` ```apply (erule subst) ``` krauss@26056 ` 1290` ```apply (simp_all add: pos_mod_sign pos_mod_bound) ``` krauss@26056 ` 1291` ```done ``` krauss@26056 ` 1292` krauss@26056 ` 1293` ```lemma zdiv_mono2_neg: "[| a \$< #0; #0 \$< b'; b' \$<= b |] ``` krauss@26056 ` 1294` ``` ==> a zdiv b' \$<= a zdiv b" ``` krauss@26056 ` 1295` ```apply (cut_tac a = "intify (a)" in zdiv_mono2_neg_raw) ``` krauss@26056 ` 1296` ```apply auto ``` krauss@26056 ` 1297` ```done ``` krauss@26056 ` 1298` krauss@26056 ` 1299` krauss@26056 ` 1300` krauss@26056 ` 1301` ```subsection{* More algebraic laws for zdiv and zmod *} ``` krauss@26056 ` 1302` krauss@26056 ` 1303` ```(** proving (a*b) zdiv c = a \$* (b zdiv c) \$+ a * (b zmod c) **) ``` krauss@26056 ` 1304` krauss@26056 ` 1305` ```lemma zmult1_lemma: ``` krauss@26056 ` 1306` ``` "[| quorem(, ); c \ int; c \ #0 |] ``` krauss@26056 ` 1307` ``` ==> quorem (, )" ``` krauss@26056 ` 1308` ```apply (auto simp add: split_ifs quorem_def neq_iff_zless zadd_zmult_distrib2 ``` krauss@26056 ` 1309` ``` pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound) ``` krauss@26056 ` 1310` ```apply (auto intro: raw_zmod_zdiv_equality) ``` krauss@26056 ` 1311` ```done ``` krauss@26056 ` 1312` krauss@26056 ` 1313` ```lemma zdiv_zmult1_eq_raw: ``` krauss@26056 ` 1314` ``` "[|b \ int; c \ int|] ``` krauss@26056 ` 1315` ``` ==> (a\$*b) zdiv c = a\$*(b zdiv c) \$+ a\$*(b zmod c) zdiv c" ``` krauss@26056 ` 1316` ```apply (case_tac "c = #0") ``` krauss@26056 ` 1317` ``` apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) ``` krauss@26056 ` 1318` ```apply (rule quorem_div_mod [THEN zmult1_lemma, THEN quorem_div]) ``` krauss@26056 ` 1319` ```apply auto ``` krauss@26056 ` 1320` ```done ``` krauss@26056 ` 1321` krauss@26056 ` 1322` ```lemma zdiv_zmult1_eq: "(a\$*b) zdiv c = a\$*(b zdiv c) \$+ a\$*(b zmod c) zdiv c" ``` krauss@26056 ` 1323` ```apply (cut_tac b = "intify (b)" and c = "intify (c)" in zdiv_zmult1_eq_raw) ``` krauss@26056 ` 1324` ```apply auto ``` krauss@26056 ` 1325` ```done ``` krauss@26056 ` 1326` krauss@26056 ` 1327` ```lemma zmod_zmult1_eq_raw: ``` krauss@26056 ` 1328` ``` "[|b \ int; c \ int|] ==> (a\$*b) zmod c = a\$*(b zmod c) zmod c" ``` krauss@26056 ` 1329` ```apply (case_tac "c = #0") ``` krauss@26056 ` 1330` ``` apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) ``` krauss@26056 ` 1331` ```apply (rule quorem_div_mod [THEN zmult1_lemma, THEN quorem_mod]) ``` krauss@26056 ` 1332` ```apply auto ``` krauss@26056 ` 1333` ```done ``` krauss@26056 ` 1334` krauss@26056 ` 1335` ```lemma zmod_zmult1_eq: "(a\$*b) zmod c = a\$*(b zmod c) zmod c" ``` krauss@26056 ` 1336` ```apply (cut_tac b = "intify (b)" and c = "intify (c)" in zmod_zmult1_eq_raw) ``` krauss@26056 ` 1337` ```apply auto ``` krauss@26056 ` 1338` ```done ``` krauss@26056 ` 1339` krauss@26056 ` 1340` ```lemma zmod_zmult1_eq': "(a\$*b) zmod c = ((a zmod c) \$* b) zmod c" ``` krauss@26056 ` 1341` ```apply (rule trans) ``` krauss@26056 ` 1342` ```apply (rule_tac b = " (b \$* a) zmod c" in trans) ``` krauss@26056 ` 1343` ```apply (rule_tac [2] zmod_zmult1_eq) ``` krauss@26056 ` 1344` ```apply (simp_all (no_asm) add: zmult_commute) ``` krauss@26056 ` 1345` ```done ``` krauss@26056 ` 1346` krauss@26056 ` 1347` ```lemma zmod_zmult_distrib: "(a\$*b) zmod c = ((a zmod c) \$* (b zmod c)) zmod c" ``` krauss@26056 ` 1348` ```apply (rule zmod_zmult1_eq' [THEN trans]) ``` krauss@26056 ` 1349` ```apply (rule zmod_zmult1_eq) ``` krauss@26056 ` 1350` ```done ``` krauss@26056 ` 1351` krauss@26056 ` 1352` ```lemma zdiv_zmult_self1 [simp]: "intify(b) \ #0 ==> (a\$*b) zdiv b = intify(a)" ``` krauss@26056 ` 1353` ```apply (simp (no_asm_simp) add: zdiv_zmult1_eq) ``` krauss@26056 ` 1354` ```done ``` krauss@26056 ` 1355` krauss@26056 ` 1356` ```lemma zdiv_zmult_self2 [simp]: "intify(b) \ #0 ==> (b\$*a) zdiv b = intify(a)" ``` krauss@26056 ` 1357` ```apply (subst zmult_commute , erule zdiv_zmult_self1) ``` krauss@26056 ` 1358` ```done ``` krauss@26056 ` 1359` krauss@26056 ` 1360` ```lemma zmod_zmult_self1 [simp]: "(a\$*b) zmod b = #0" ``` krauss@26056 ` 1361` ```apply (simp (no_asm) add: zmod_zmult1_eq) ``` krauss@26056 ` 1362` ```done ``` krauss@26056 ` 1363` krauss@26056 ` 1364` ```lemma zmod_zmult_self2 [simp]: "(b\$*a) zmod b = #0" ``` krauss@26056 ` 1365` ```apply (simp (no_asm) add: zmult_commute zmod_zmult1_eq) ``` krauss@26056 ` 1366` ```done ``` krauss@26056 ` 1367` krauss@26056 ` 1368` krauss@26056 ` 1369` ```(** proving (a\$+b) zdiv c = ``` krauss@26056 ` 1370` ``` a zdiv c \$+ b zdiv c \$+ ((a zmod c \$+ b zmod c) zdiv c) **) ``` krauss@26056 ` 1371` krauss@26056 ` 1372` ```lemma zadd1_lemma: ``` krauss@26056 ` 1373` ``` "[| quorem(, ); quorem(, ); ``` krauss@26056 ` 1374` ``` c \ int; c \ #0 |] ``` krauss@26056 ` 1375` ``` ==> quorem (, )" ``` krauss@26056 ` 1376` ```apply (auto simp add: split_ifs quorem_def neq_iff_zless zadd_zmult_distrib2 ``` krauss@26056 ` 1377` ``` pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound) ``` krauss@26056 ` 1378` ```apply (auto intro: raw_zmod_zdiv_equality) ``` krauss@26056 ` 1379` ```done ``` krauss@26056 ` 1380` krauss@26056 ` 1381` ```(*NOT suitable for rewriting: the RHS has an instance of the LHS*) ``` krauss@26056 ` 1382` ```lemma zdiv_zadd1_eq_raw: ``` krauss@26056 ` 1383` ``` "[|a \ int; b \ int; c \ int|] ==> ``` krauss@26056 ` 1384` ``` (a\$+b) zdiv c = a zdiv c \$+ b zdiv c \$+ ((a zmod c \$+ b zmod c) zdiv c)" ``` krauss@26056 ` 1385` ```apply (case_tac "c = #0") ``` krauss@26056 ` 1386` ``` apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) ``` krauss@26056 ` 1387` ```apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod, ``` krauss@26056 ` 1388` ``` THEN quorem_div]) ``` krauss@26056 ` 1389` ```done ``` krauss@26056 ` 1390` krauss@26056 ` 1391` ```lemma zdiv_zadd1_eq: ``` krauss@26056 ` 1392` ``` "(a\$+b) zdiv c = a zdiv c \$+ b zdiv c \$+ ((a zmod c \$+ b zmod c) zdiv c)" ``` krauss@26056 ` 1393` ```apply (cut_tac a = "intify (a)" and b = "intify (b)" and c = "intify (c)" ``` krauss@26056 ` 1394` ``` in zdiv_zadd1_eq_raw) ``` krauss@26056 ` 1395` ```apply auto ``` krauss@26056 ` 1396` ```done ``` krauss@26056 ` 1397` krauss@26056 ` 1398` ```lemma zmod_zadd1_eq_raw: ``` krauss@26056 ` 1399` ``` "[|a \ int; b \ int; c \ int|] ``` krauss@26056 ` 1400` ``` ==> (a\$+b) zmod c = (a zmod c \$+ b zmod c) zmod c" ``` krauss@26056 ` 1401` ```apply (case_tac "c = #0") ``` krauss@26056 ` 1402` ``` apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) ``` krauss@26056 ` 1403` ```apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod, ``` krauss@26056 ` 1404` ``` THEN quorem_mod]) ``` krauss@26056 ` 1405` ```done ``` krauss@26056 ` 1406` krauss@26056 ` 1407` ```lemma zmod_zadd1_eq: "(a\$+b) zmod c = (a zmod c \$+ b zmod c) zmod c" ``` krauss@26056 ` 1408` ```apply (cut_tac a = "intify (a)" and b = "intify (b)" and c = "intify (c)" ``` krauss@26056 ` 1409` ``` in zmod_zadd1_eq_raw) ``` krauss@26056 ` 1410` ```apply auto ``` krauss@26056 ` 1411` ```done ``` krauss@26056 ` 1412` krauss@26056 ` 1413` ```lemma zmod_div_trivial_raw: ``` krauss@26056 ` 1414` ``` "[|a \ int; b \ int|] ==> (a zmod b) zdiv b = #0" ``` krauss@26056 ` 1415` ```apply (case_tac "b = #0") ``` krauss@26056 ` 1416` ``` apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) ``` krauss@26056 ` 1417` ```apply (auto simp add: neq_iff_zless pos_mod_sign pos_mod_bound ``` krauss@26056 ` 1418` ``` zdiv_pos_pos_trivial neg_mod_sign neg_mod_bound zdiv_neg_neg_trivial) ``` krauss@26056 ` 1419` ```done ``` krauss@26056 ` 1420` krauss@26056 ` 1421` ```lemma zmod_div_trivial [simp]: "(a zmod b) zdiv b = #0" ``` krauss@26056 ` 1422` ```apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_div_trivial_raw) ``` krauss@26056 ` 1423` ```apply auto ``` krauss@26056 ` 1424` ```done ``` krauss@26056 ` 1425` krauss@26056 ` 1426` ```lemma zmod_mod_trivial_raw: ``` krauss@26056 ` 1427` ``` "[|a \ int; b \ int|] ==> (a zmod b) zmod b = a zmod b" ``` krauss@26056 ` 1428` ```apply (case_tac "b = #0") ``` krauss@26056 ` 1429` ``` apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) ``` krauss@26056 ` 1430` ```apply (auto simp add: neq_iff_zless pos_mod_sign pos_mod_bound ``` krauss@26056 ` 1431` ``` zmod_pos_pos_trivial neg_mod_sign neg_mod_bound zmod_neg_neg_trivial) ``` krauss@26056 ` 1432` ```done ``` krauss@26056 ` 1433` krauss@26056 ` 1434` ```lemma zmod_mod_trivial [simp]: "(a zmod b) zmod b = a zmod b" ``` krauss@26056 ` 1435` ```apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_mod_trivial_raw) ``` krauss@26056 ` 1436` ```apply auto ``` krauss@26056 ` 1437` ```done ``` krauss@26056 ` 1438` krauss@26056 ` 1439` ```lemma zmod_zadd_left_eq: "(a\$+b) zmod c = ((a zmod c) \$+ b) zmod c" ``` krauss@26056 ` 1440` ```apply (rule trans [symmetric]) ``` krauss@26056 ` 1441` ```apply (rule zmod_zadd1_eq) ``` krauss@26056 ` 1442` ```apply (simp (no_asm)) ``` krauss@26056 ` 1443` ```apply (rule zmod_zadd1_eq [symmetric]) ``` krauss@26056 ` 1444` ```done ``` krauss@26056 ` 1445` krauss@26056 ` 1446` ```lemma zmod_zadd_right_eq: "(a\$+b) zmod c = (a \$+ (b zmod c)) zmod c" ``` krauss@26056 ` 1447` ```apply (rule trans [symmetric]) ``` krauss@26056 ` 1448` ```apply (rule zmod_zadd1_eq) ``` krauss@26056 ` 1449` ```apply (simp (no_asm)) ``` krauss@26056 ` 1450` ```apply (rule zmod_zadd1_eq [symmetric]) ``` krauss@26056 ` 1451` ```done ``` krauss@26056 ` 1452` krauss@26056 ` 1453` krauss@26056 ` 1454` ```lemma zdiv_zadd_self1 [simp]: ``` krauss@26056 ` 1455` ``` "intify(a) \ #0 ==> (a\$+b) zdiv a = b zdiv a \$+ #1" ``` krauss@26056 ` 1456` ```by (simp (no_asm_simp) add: zdiv_zadd1_eq) ``` krauss@26056 ` 1457` krauss@26056 ` 1458` ```lemma zdiv_zadd_self2 [simp]: ``` krauss@26056 ` 1459` ``` "intify(a) \ #0 ==> (b\$+a) zdiv a = b zdiv a \$+ #1" ``` krauss@26056 ` 1460` ```by (simp (no_asm_simp) add: zdiv_zadd1_eq) ``` krauss@26056 ` 1461` krauss@26056 ` 1462` ```lemma zmod_zadd_self1 [simp]: "(a\$+b) zmod a = b zmod a" ``` krauss@26056 ` 1463` ```apply (case_tac "a = #0") ``` krauss@26056 ` 1464` ``` apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) ``` krauss@26056 ` 1465` ```apply (simp (no_asm_simp) add: zmod_zadd1_eq) ``` krauss@26056 ` 1466` ```done ``` krauss@26056 ` 1467` krauss@26056 ` 1468` ```lemma zmod_zadd_self2 [simp]: "(b\$+a) zmod a = b zmod a" ``` krauss@26056 ` 1469` ```apply (case_tac "a = #0") ``` krauss@26056 ` 1470` ``` apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) ``` krauss@26056 ` 1471` ```apply (simp (no_asm_simp) add: zmod_zadd1_eq) ``` krauss@26056 ` 1472` ```done ``` krauss@26056 ` 1473` krauss@26056 ` 1474` krauss@26056 ` 1475` ```subsection{* proving a zdiv (b*c) = (a zdiv b) zdiv c *} ``` krauss@26056 ` 1476` krauss@26056 ` 1477` ```(*The condition c>0 seems necessary. Consider that 7 zdiv ~6 = ~2 but ``` krauss@26056 ` 1478` ``` 7 zdiv 2 zdiv ~3 = 3 zdiv ~3 = ~1. The subcase (a zdiv b) zmod c = 0 seems ``` krauss@26056 ` 1479` ``` to cause particular problems.*) ``` krauss@26056 ` 1480` krauss@26056 ` 1481` ```(** first, four lemmas to bound the remainder for the cases b<0 and b>0 **) ``` krauss@26056 ` 1482` krauss@26056 ` 1483` ```lemma zdiv_zmult2_aux1: ``` krauss@26056 ` 1484` ``` "[| #0 \$< c; b \$< r; r \$<= #0 |] ==> b\$*c \$< b\$*(q zmod c) \$+ r" ``` krauss@26056 ` 1485` ```apply (subgoal_tac "b \$* (c \$- q zmod c) \$< r \$* #1") ``` krauss@26056 ` 1486` ```apply (simp add: zdiff_zmult_distrib2 zadd_commute zcompare_rls) ``` krauss@26056 ` 1487` ```apply (rule zle_zless_trans) ``` krauss@26056 ` 1488` ```apply (erule_tac [2] zmult_zless_mono1) ``` krauss@26056 ` 1489` ```apply (rule zmult_zle_mono2_neg) ``` krauss@26056 ` 1490` ```apply (auto simp add: zcompare_rls zadd_commute add1_zle_iff pos_mod_bound) ``` krauss@26056 ` 1491` ```apply (blast intro: zless_imp_zle dest: zless_zle_trans) ``` krauss@26056 ` 1492` ```done ``` krauss@26056 ` 1493` krauss@26056 ` 1494` ```lemma zdiv_zmult2_aux2: ``` krauss@26056 ` 1495` ``` "[| #0 \$< c; b \$< r; r \$<= #0 |] ==> b \$* (q zmod c) \$+ r \$<= #0" ``` krauss@26056 ` 1496` ```apply (subgoal_tac "b \$* (q zmod c) \$<= #0") ``` krauss@26056 ` 1497` ``` prefer 2 ``` krauss@26056 ` 1498` ``` apply (simp add: zmult_le_0_iff pos_mod_sign) ``` krauss@26056 ` 1499` ``` apply (blast intro: zless_imp_zle dest: zless_zle_trans) ``` krauss@26056 ` 1500` ```(*arithmetic*) ``` krauss@26056 ` 1501` ```apply (drule zadd_zle_mono) ``` krauss@26056 ` 1502` ```apply assumption ``` krauss@26056 ` 1503` ```apply (simp add: zadd_commute) ``` krauss@26056 ` 1504` ```done ``` krauss@26056 ` 1505` krauss@26056 ` 1506` ```lemma zdiv_zmult2_aux3: ``` krauss@26056 ` 1507` ``` "[| #0 \$< c; #0 \$<= r; r \$< b |] ==> #0 \$<= b \$* (q zmod c) \$+ r" ``` krauss@26056 ` 1508` ```apply (subgoal_tac "#0 \$<= b \$* (q zmod c)") ``` krauss@26056 ` 1509` ``` prefer 2 ``` krauss@26056 ` 1510` ``` apply (simp add: int_0_le_mult_iff pos_mod_sign) ``` krauss@26056 ` 1511` ``` apply (blast intro: zless_imp_zle dest: zle_zless_trans) ``` krauss@26056 ` 1512` ```(*arithmetic*) ``` krauss@26056 ` 1513` ```apply (drule zadd_zle_mono) ``` krauss@26056 ` 1514` ```apply assumption ``` krauss@26056 ` 1515` ```apply (simp add: zadd_commute) ``` krauss@26056 ` 1516` ```done ``` krauss@26056 ` 1517` krauss@26056 ` 1518` ```lemma zdiv_zmult2_aux4: ``` krauss@26056 ` 1519` ``` "[| #0 \$< c; #0 \$<= r; r \$< b |] ==> b \$* (q zmod c) \$+ r \$< b \$* c" ``` krauss@26056 ` 1520` ```apply (subgoal_tac "r \$* #1 \$< b \$* (c \$- q zmod c)") ``` krauss@26056 ` 1521` ```apply (simp add: zdiff_zmult_distrib2 zadd_commute zcompare_rls) ``` krauss@26056 ` 1522` ```apply (rule zless_zle_trans) ``` krauss@26056 ` 1523` ```apply (erule zmult_zless_mono1) ``` krauss@26056 ` 1524` ```apply (rule_tac [2] zmult_zle_mono2) ``` krauss@26056 ` 1525` ```apply (auto simp add: zcompare_rls zadd_commute add1_zle_iff pos_mod_bound) ``` krauss@26056 ` 1526` ```apply (blast intro: zless_imp_zle dest: zle_zless_trans) ``` krauss@26056 ` 1527` ```done ``` krauss@26056 ` 1528` krauss@26056 ` 1529` ```lemma zdiv_zmult2_lemma: ``` krauss@26056 ` 1530` ``` "[| quorem (, ); a \ int; b \ int; b \ #0; #0 \$< c |] ``` krauss@26056 ` 1531` ``` ==> quorem (, )" ``` krauss@26056 ` 1532` ```apply (auto simp add: zmult_ac zmod_zdiv_equality [symmetric] quorem_def ``` krauss@26056 ` 1533` ``` neq_iff_zless int_0_less_mult_iff ``` krauss@26056 ` 1534` ``` zadd_zmult_distrib2 [symmetric] zdiv_zmult2_aux1 zdiv_zmult2_aux2 ``` krauss@26056 ` 1535` ``` zdiv_zmult2_aux3 zdiv_zmult2_aux4) ``` krauss@26056 ` 1536` ```apply (blast dest: zless_trans)+ ``` krauss@26056 ` 1537` ```done ``` krauss@26056 ` 1538` krauss@26056 ` 1539` ```lemma zdiv_zmult2_eq_raw: ``` krauss@26056 ` 1540` ``` "[|#0 \$< c; a \ int; b \ int|] ==> a zdiv (b\$*c) = (a zdiv b) zdiv c" ``` krauss@26056 ` 1541` ```apply (case_tac "b = #0") ``` krauss@26056 ` 1542` ``` apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) ``` krauss@26056 ` 1543` ```apply (rule quorem_div_mod [THEN zdiv_zmult2_lemma, THEN quorem_div]) ``` krauss@26056 ` 1544` ```apply (auto simp add: intify_eq_0_iff_zle) ``` krauss@26056 ` 1545` ```apply (blast dest: zle_zless_trans) ``` krauss@26056 ` 1546` ```done ``` krauss@26056 ` 1547` krauss@26056 ` 1548` ```lemma zdiv_zmult2_eq: "#0 \$< c ==> a zdiv (b\$*c) = (a zdiv b) zdiv c" ``` krauss@26056 ` 1549` ```apply (cut_tac a = "intify (a)" and b = "intify (b)" in zdiv_zmult2_eq_raw) ``` krauss@26056 ` 1550` ```apply auto ``` krauss@26056 ` 1551` ```done ``` krauss@26056 ` 1552` krauss@26056 ` 1553` ```lemma zmod_zmult2_eq_raw: ``` krauss@26056 ` 1554` ``` "[|#0 \$< c; a \ int; b \ int|] ``` krauss@26056 ` 1555` ``` ==> a zmod (b\$*c) = b\$*(a zdiv b zmod c) \$+ a zmod b" ``` krauss@26056 ` 1556` ```apply (case_tac "b = #0") ``` krauss@26056 ` 1557` ``` apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) ``` krauss@26056 ` 1558` ```apply (rule quorem_div_mod [THEN zdiv_zmult2_lemma, THEN quorem_mod]) ``` krauss@26056 ` 1559` ```apply (auto simp add: intify_eq_0_iff_zle) ``` krauss@26056 ` 1560` ```apply (blast dest: zle_zless_trans) ``` krauss@26056 ` 1561` ```done ``` krauss@26056 ` 1562` krauss@26056 ` 1563` ```lemma zmod_zmult2_eq: ``` krauss@26056 ` 1564` ``` "#0 \$< c ==> a zmod (b\$*c) = b\$*(a zdiv b zmod c) \$+ a zmod b" ``` krauss@26056 ` 1565` ```apply (cut_tac a = "intify (a)" and b = "intify (b)" in zmod_zmult2_eq_raw) ``` krauss@26056 ` 1566` ```apply auto ``` krauss@26056 ` 1567` ```done ``` krauss@26056 ` 1568` krauss@26056 ` 1569` ```subsection{* Cancellation of common factors in "zdiv" *} ``` krauss@26056 ` 1570` krauss@26056 ` 1571` ```lemma zdiv_zmult_zmult1_aux1: ``` krauss@26056 ` 1572` ``` "[| #0 \$< b; intify(c) \ #0 |] ==> (c\$*a) zdiv (c\$*b) = a zdiv b" ``` krauss@26056 ` 1573` ```apply (subst zdiv_zmult2_eq) ``` krauss@26056 ` 1574` ```apply auto ``` krauss@26056 ` 1575` ```done ``` krauss@26056 ` 1576` krauss@26056 ` 1577` ```lemma zdiv_zmult_zmult1_aux2: ``` krauss@26056 ` 1578` ``` "[| b \$< #0; intify(c) \ #0 |] ==> (c\$*a) zdiv (c\$*b) = a zdiv b" ``` krauss@26056 ` 1579` ```apply (subgoal_tac " (c \$* (\$-a)) zdiv (c \$* (\$-b)) = (\$-a) zdiv (\$-b)") ``` krauss@26056 ` 1580` ```apply (rule_tac [2] zdiv_zmult_zmult1_aux1) ``` krauss@26056 ` 1581` ```apply auto ``` krauss@26056 ` 1582` ```done ``` krauss@26056 ` 1583` krauss@26056 ` 1584` ```lemma zdiv_zmult_zmult1_raw: ``` krauss@26056 ` 1585` ``` "[|intify(c) \ #0; b \ int|] ==> (c\$*a) zdiv (c\$*b) = a zdiv b" ``` krauss@26056 ` 1586` ```apply (case_tac "b = #0") ``` krauss@26056 ` 1587` ``` apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) ``` krauss@26056 ` 1588` ```apply (auto simp add: neq_iff_zless [of b] ``` krauss@26056 ` 1589` ``` zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2) ``` krauss@26056 ` 1590` ```done ``` krauss@26056 ` 1591` krauss@26056 ` 1592` ```lemma zdiv_zmult_zmult1: "intify(c) \ #0 ==> (c\$*a) zdiv (c\$*b) = a zdiv b" ``` krauss@26056 ` 1593` ```apply (cut_tac b = "intify (b)" in zdiv_zmult_zmult1_raw) ``` krauss@26056 ` 1594` ```apply auto ``` krauss@26056 ` 1595` ```done ``` krauss@26056 ` 1596` krauss@26056 ` 1597` ```lemma zdiv_zmult_zmult2: "intify(c) \ #0 ==> (a\$*c) zdiv (b\$*c) = a zdiv b" ``` krauss@26056 ` 1598` ```apply (drule zdiv_zmult_zmult1) ``` krauss@26056 ` 1599` ```apply (auto simp add: zmult_commute) ``` krauss@26056 ` 1600` ```done ``` krauss@26056 ` 1601` krauss@26056 ` 1602` krauss@26056 ` 1603` ```subsection{* Distribution of factors over "zmod" *} ``` krauss@26056 ` 1604` krauss@26056 ` 1605` ```lemma zmod_zmult_zmult1_aux1: ``` krauss@26056 ` 1606` ``` "[| #0 \$< b; intify(c) \ #0 |] ``` krauss@26056 ` 1607` ``` ==> (c\$*a) zmod (c\$*b) = c \$* (a zmod b)" ``` krauss@26056 ` 1608` ```apply (subst zmod_zmult2_eq) ``` krauss@26056 ` 1609` ```apply auto ``` krauss@26056 ` 1610` ```done ``` krauss@26056 ` 1611` krauss@26056 ` 1612` ```lemma zmod_zmult_zmult1_aux2: ``` krauss@26056 ` 1613` ``` "[| b \$< #0; intify(c) \ #0 |] ``` krauss@26056 ` 1614` ``` ==> (c\$*a) zmod (c\$*b) = c \$* (a zmod b)" ``` krauss@26056 ` 1615` ```apply (subgoal_tac " (c \$* (\$-a)) zmod (c \$* (\$-b)) = c \$* ((\$-a) zmod (\$-b))") ``` krauss@26056 ` 1616` ```apply (rule_tac [2] zmod_zmult_zmult1_aux1) ``` krauss@26056 ` 1617` ```apply auto ``` krauss@26056 ` 1618` ```done ``` krauss@26056 ` 1619` krauss@26056 ` 1620` ```lemma zmod_zmult_zmult1_raw: ``` krauss@26056 ` 1621` ``` "[|b \ int; c \ int|] ==> (c\$*a) zmod (c\$*b) = c \$* (a zmod b)" ``` krauss@26056 ` 1622` ```apply (case_tac "b = #0") ``` krauss@26056 ` 1623` ``` apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) ``` krauss@26056 ` 1624` ```apply (case_tac "c = #0") ``` krauss@26056 ` 1625` ``` apply (simp add: DIVISION_BY_ZERO_ZDIV DIVISION_BY_ZERO_ZMOD) ``` krauss@26056 ` 1626` ```apply (auto simp add: neq_iff_zless [of b] ``` krauss@26056 ` 1627` ``` zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2) ``` krauss@26056 ` 1628` ```done ``` krauss@26056 ` 1629` krauss@26056 ` 1630` ```lemma zmod_zmult_zmult1: "(c\$*a) zmod (c\$*b) = c \$* (a zmod b)" ``` krauss@26056 ` 1631` ```apply (cut_tac b = "intify (b)" and c = "intify (c)" in zmod_zmult_zmult1_raw) ``` krauss@26056 ` 1632` ```apply auto ``` krauss@26056 ` 1633` ```done ``` krauss@26056 ` 1634` krauss@26056 ` 1635` ```lemma zmod_zmult_zmult2: "(a\$*c) zmod (b\$*c) = (a zmod b) \$* c" ``` krauss@26056 ` 1636` ```apply (cut_tac c = "c" in zmod_zmult_zmult1) ``` krauss@26056 ` 1637` ```apply (auto simp add: zmult_commute) ``` krauss@26056 ` 1638` ```done ``` krauss@26056 ` 1639` krauss@26056 ` 1640` krauss@26056 ` 1641` ```(** Quotients of signs **) ``` krauss@26056 ` 1642` krauss@26056 ` 1643` ```lemma zdiv_neg_pos_less0: "[| a \$< #0; #0 \$< b |] ==> a zdiv b \$< #0" ``` krauss@26056 ` 1644` ```apply (subgoal_tac "a zdiv b \$<= #-1") ``` krauss@26056 ` 1645` ```apply (erule zle_zless_trans) ``` krauss@26056 ` 1646` ```apply (simp (no_asm)) ``` krauss@26056 ` 1647` ```apply (rule zle_trans) ``` krauss@26056 ` 1648` ```apply (rule_tac a' = "#-1" in zdiv_mono1) ``` krauss@26056 ` 1649` ```apply (rule zless_add1_iff_zle [THEN iffD1]) ``` krauss@26056 ` 1650` ```apply (simp (no_asm)) ``` krauss@26056 ` 1651` ```apply (auto simp add: zdiv_minus1) ``` krauss@26056 ` 1652` ```done ``` krauss@26056 ` 1653` krauss@26056 ` 1654` ```lemma zdiv_nonneg_neg_le0: "[| #0 \$<= a; b \$< #0 |] ==> a zdiv b \$<= #0" ``` krauss@26056 ` 1655` ```apply (drule zdiv_mono1_neg) ``` krauss@26056 ` 1656` ```apply auto ``` krauss@26056 ` 1657` ```done ``` krauss@26056 ` 1658` krauss@26056 ` 1659` ```lemma pos_imp_zdiv_nonneg_iff: "#0 \$< b ==> (#0 \$<= a zdiv b) <-> (#0 \$<= a)" ``` krauss@26056 ` 1660` ```apply auto ``` krauss@26056 ` 1661` ```apply (drule_tac [2] zdiv_mono1) ``` krauss@26056 ` 1662` ```apply (auto simp add: neq_iff_zless) ``` krauss@26056 ` 1663` ```apply (simp (no_asm_use) add: not_zless_iff_zle [THEN iff_sym]) ``` krauss@26056 ` 1664` ```apply (blast intro: zdiv_neg_pos_less0) ``` krauss@26056 ` 1665` ```done ``` krauss@26056 ` 1666` krauss@26056 ` 1667` ```lemma neg_imp_zdiv_nonneg_iff: "b \$< #0 ==> (#0 \$<= a zdiv b) <-> (a \$<= #0)" ``` krauss@26056 ` 1668` ```apply (subst zdiv_zminus_zminus [symmetric]) ``` krauss@26056 ` 1669` ```apply (rule iff_trans) ``` krauss@26056 ` 1670` ```apply (rule pos_imp_zdiv_nonneg_iff) ``` krauss@26056 ` 1671` ```apply auto ``` krauss@26056 ` 1672` ```done ``` krauss@26056 ` 1673` krauss@26056 ` 1674` ```(*But not (a zdiv b \$<= 0 iff a\$<=0); consider a=1, b=2 when a zdiv b = 0.*) ``` krauss@26056 ` 1675` ```lemma pos_imp_zdiv_neg_iff: "#0 \$< b ==> (a zdiv b \$< #0) <-> (a \$< #0)" ``` krauss@26056 ` 1676` ```apply (simp (no_asm_simp) add: not_zle_iff_zless [THEN iff_sym]) ``` krauss@26056 ` 1677` ```apply (erule pos_imp_zdiv_nonneg_iff) ``` krauss@26056 ` 1678` ```done ``` krauss@26056 ` 1679` krauss@26056 ` 1680` ```(*Again the law fails for \$<=: consider a = -1, b = -2 when a zdiv b = 0*) ``` krauss@26056 ` 1681` ```lemma neg_imp_zdiv_neg_iff: "b \$< #0 ==> (a zdiv b \$< #0) <-> (#0 \$< a)" ``` krauss@26056 ` 1682` ```apply (simp (no_asm_simp) add: not_zle_iff_zless [THEN iff_sym]) ``` krauss@26056 ` 1683` ```apply (erule neg_imp_zdiv_nonneg_iff) ``` krauss@26056 ` 1684` ```done ``` krauss@26056 ` 1685` krauss@26056 ` 1686` ```(* ``` krauss@26056 ` 1687` ``` THESE REMAIN TO BE CONVERTED -- but aren't that useful! ``` krauss@26056 ` 1688` krauss@26056 ` 1689` ``` subsection{* Speeding up the division algorithm with shifting *} ``` krauss@26056 ` 1690` krauss@26056 ` 1691` ``` (** computing "zdiv" by shifting **) ``` krauss@26056 ` 1692` krauss@26056 ` 1693` ``` lemma pos_zdiv_mult_2: "#0 \$<= a ==> (#1 \$+ #2\$*b) zdiv (#2\$*a) = b zdiv a" ``` krauss@26056 ` 1694` ``` apply (case_tac "a = #0") ``` krauss@26056 ` 1695` ``` apply (subgoal_tac "#1 \$<= a") ``` krauss@26056 ` 1696` ``` apply (arith_tac 2) ``` krauss@26056 ` 1697` ``` apply (subgoal_tac "#1 \$< a \$* #2") ``` krauss@26056 ` 1698` ``` apply (arith_tac 2) ``` krauss@26056 ` 1699` ``` apply (subgoal_tac "#2\$* (#1 \$+ b zmod a) \$<= #2\$*a") ``` krauss@26056 ` 1700` ``` apply (rule_tac [2] zmult_zle_mono2) ``` krauss@26056 ` 1701` ``` apply (auto simp add: zadd_commute zmult_commute add1_zle_iff pos_mod_bound) ``` krauss@26056 ` 1702` ``` apply (subst zdiv_zadd1_eq) ``` krauss@26056 ` 1703` ``` apply (simp (no_asm_simp) add: zdiv_zmult_zmult2 zmod_zmult_zmult2 zdiv_pos_pos_trivial) ``` krauss@26056 ` 1704` ``` apply (subst zdiv_pos_pos_trivial) ``` krauss@26056 ` 1705` ``` apply (simp (no_asm_simp) add: [zmod_pos_pos_trivial pos_mod_sign [THEN zadd_zle_mono1] RSN (2,zle_trans) ]) ``` krauss@26056 ` 1706` ``` apply (auto simp add: zmod_pos_pos_trivial) ``` krauss@26056 ` 1707` ``` apply (subgoal_tac "#0 \$<= b zmod a") ``` krauss@26056 ` 1708` ``` apply (asm_simp_tac (simpset () add: pos_mod_sign) 2) ``` krauss@26056 ` 1709` ``` apply arith ``` krauss@26056 ` 1710` ``` done ``` krauss@26056 ` 1711` krauss@26056 ` 1712` krauss@26056 ` 1713` ``` lemma neg_zdiv_mult_2: "a \$<= #0 ==> (#1 \$+ #2\$*b) zdiv (#2\$*a) <-> (b\$+#1) zdiv a" ``` krauss@26056 ` 1714` ``` apply (subgoal_tac " (#1 \$+ #2\$* (\$-b-#1)) zdiv (#2 \$* (\$-a)) <-> (\$-b-#1) zdiv (\$-a)") ``` krauss@26056 ` 1715` ``` apply (rule_tac [2] pos_zdiv_mult_2) ``` krauss@26056 ` 1716` ``` apply (auto simp add: zmult_zminus_right) ``` krauss@26056 ` 1717` ``` apply (subgoal_tac " (#-1 - (#2 \$* b)) = - (#1 \$+ (#2 \$* b))") ``` krauss@26056 ` 1718` ``` apply (Simp_tac 2) ``` krauss@26056 ` 1719` ``` apply (asm_full_simp_tac (HOL_ss add: zdiv_zminus_zminus zdiff_def zminus_zadd_distrib [symmetric]) ``` krauss@26056 ` 1720` ``` done ``` krauss@26056 ` 1721` krauss@26056 ` 1722` krauss@26056 ` 1723` ``` (*Not clear why this must be proved separately; probably integ_of causes ``` krauss@26056 ` 1724` ``` simplification problems*) ``` krauss@26056 ` 1725` ``` lemma lemma: "~ #0 \$<= x ==> x \$<= #0" ``` krauss@26056 ` 1726` ``` apply auto ``` krauss@26056 ` 1727` ``` done ``` krauss@26056 ` 1728` krauss@26056 ` 1729` ``` lemma zdiv_integ_of_BIT: "integ_of (v BIT b) zdiv integ_of (w BIT False) = ``` krauss@26056 ` 1730` ``` (if ~b | #0 \$<= integ_of w ``` krauss@26056 ` 1731` ``` then integ_of v zdiv (integ_of w) ``` krauss@26056 ` 1732` ``` else (integ_of v \$+ #1) zdiv (integ_of w))" ``` wenzelm@32149 ` 1733` ``` apply (simp_tac (global_simpset_of Int.thy add: zadd_assoc integ_of_BIT) ``` krauss@26056 ` 1734` ``` apply (simp (no_asm_simp) del: bin_arith_extra_simps@bin_rel_simps add: zdiv_zmult_zmult1 pos_zdiv_mult_2 lemma neg_zdiv_mult_2) ``` krauss@26056 ` 1735` ``` done ``` krauss@26056 ` 1736` krauss@26056 ` 1737` ``` declare zdiv_integ_of_BIT [simp] ``` krauss@26056 ` 1738` krauss@26056 ` 1739` krauss@26056 ` 1740` ``` (** computing "zmod" by shifting (proofs resemble those for "zdiv") **) ``` krauss@26056 ` 1741` krauss@26056 ` 1742` ``` lemma pos_zmod_mult_2: "#0 \$<= a ==> (#1 \$+ #2\$*b) zmod (#2\$*a) = #1 \$+ #2 \$* (b zmod a)" ``` krauss@26056 ` 1743` ``` apply (case_tac "a = #0") ``` krauss@26056 ` 1744` ``` apply (subgoal_tac "#1 \$<= a") ``` krauss@26056 ` 1745` ``` apply (arith_tac 2) ``` krauss@26056 ` 1746` ``` apply (subgoal_tac "#1 \$< a \$* #2") ``` krauss@26056 ` 1747` ``` apply (arith_tac 2) ``` krauss@26056 ` 1748` ``` apply (subgoal_tac "#2\$* (#1 \$+ b zmod a) \$<= #2\$*a") ``` krauss@26056 ` 1749` ``` apply (rule_tac [2] zmult_zle_mono2) ``` krauss@26056 ` 1750` ``` apply (auto simp add: zadd_commute zmult_commute add1_zle_iff pos_mod_bound) ``` krauss@26056 ` 1751` ``` apply (subst zmod_zadd1_eq) ``` krauss@26056 ` 1752` ``` apply (simp (no_asm_simp) add: zmod_zmult_zmult2 zmod_pos_pos_trivial) ``` krauss@26056 ` 1753` ``` apply (rule zmod_pos_pos_trivial) ``` krauss@26056 ` 1754` ``` apply (simp (no_asm_simp) # add: [zmod_pos_pos_trivial pos_mod_sign [THEN zadd_zle_mono1] RSN (2,zle_trans) ]) ``` krauss@26056 ` 1755` ``` apply (auto simp add: zmod_pos_pos_trivial) ``` krauss@26056 ` 1756` ``` apply (subgoal_tac "#0 \$<= b zmod a") ``` krauss@26056 ` 1757` ``` apply (asm_simp_tac (simpset () add: pos_mod_sign) 2) ``` krauss@26056 ` 1758` ``` apply arith ``` krauss@26056 ` 1759` ``` done ``` krauss@26056 ` 1760` krauss@26056 ` 1761` krauss@26056 ` 1762` ``` lemma neg_zmod_mult_2: "a \$<= #0 ==> (#1 \$+ #2\$*b) zmod (#2\$*a) = #2 \$* ((b\$+#1) zmod a) - #1" ``` krauss@26056 ` 1763` ``` apply (subgoal_tac " (#1 \$+ #2\$* (\$-b-#1)) zmod (#2\$* (\$-a)) = #1 \$+ #2\$* ((\$-b-#1) zmod (\$-a))") ``` krauss@26056 ` 1764` ``` apply (rule_tac [2] pos_zmod_mult_2) ``` krauss@26056 ` 1765` ``` apply (auto simp add: zmult_zminus_right) ``` krauss@26056 ` 1766` ``` apply (subgoal_tac " (#-1 - (#2 \$* b)) = - (#1 \$+ (#2 \$* b))") ``` krauss@26056 ` 1767` ``` apply (Simp_tac 2) ``` krauss@26056 ` 1768` ``` apply (asm_full_simp_tac (HOL_ss add: zmod_zminus_zminus zdiff_def zminus_zadd_distrib [symmetric]) ``` krauss@26056 ` 1769` ``` apply (dtac (zminus_equation [THEN iffD1, symmetric]) ``` krauss@26056 ` 1770` ``` apply auto ``` krauss@26056 ` 1771` ``` done ``` krauss@26056 ` 1772` krauss@26056 ` 1773` ``` lemma zmod_integ_of_BIT: "integ_of (v BIT b) zmod integ_of (w BIT False) = ``` krauss@26056 ` 1774` ``` (if b then ``` krauss@26056 ` 1775` ``` if #0 \$<= integ_of w ``` krauss@26056 ` 1776` ``` then #2 \$* (integ_of v zmod integ_of w) \$+ #1 ``` krauss@26056 ` 1777` ``` else #2 \$* ((integ_of v \$+ #1) zmod integ_of w) - #1 ``` krauss@26056 ` 1778` ``` else #2 \$* (integ_of v zmod integ_of w))" ``` wenzelm@32149 ` 1779` ``` apply (simp_tac (global_simpset_of Int.thy add: zadd_assoc integ_of_BIT) ``` krauss@26056 ` 1780` ``` apply (simp (no_asm_simp) del: bin_arith_extra_simps@bin_rel_simps add: zmod_zmult_zmult1 pos_zmod_mult_2 lemma neg_zmod_mult_2) ``` krauss@26056 ` 1781` ``` done ``` krauss@26056 ` 1782` krauss@26056 ` 1783` ``` declare zmod_integ_of_BIT [simp] ``` krauss@26056 ` 1784` ```*) ``` krauss@26056 ` 1785` krauss@26056 ` 1786` ```end ``` krauss@26056 ` 1787`