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