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