src/HOL/Integ/IntDiv.thy
 author chaieb Fri, 19 Jan 2007 15:13:47 +0100 changeset 22091 d13ad9a479f9 parent 22026 cc60e54aa7cb child 22744 5cbe966d67a2 permissions -rw-r--r--
Theorem "(x::int) dvd 1 = ( ¦x¦ = 1)" added to default simpset. This solves the goals like "~ 4 dvd 1". This used to fail before.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
 6917 eba301caceea Introduction of integer division algorithm paulson parents: diff changeset  1 (* Title: HOL/IntDiv.thy  eba301caceea Introduction of integer division algorithm paulson parents: diff changeset  2  ID: $Id$  eba301caceea Introduction of integer division algorithm paulson parents: diff changeset  3  Author: Lawrence C Paulson, Cambridge University Computer Laboratory  eba301caceea Introduction of integer division algorithm paulson parents: diff changeset  4  Copyright 1999 University of Cambridge  eba301caceea Introduction of integer division algorithm paulson parents: diff changeset  5 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  6 *)  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  7 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  8 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  9 header{*The Division Operators div and mod; the Divides Relation dvd*}  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  10 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  11 theory IntDiv  21409 6aa28caa96c5 clarified module dependencies haftmann parents: 20485 diff changeset  12 imports "../Divides" "../SetInterval" "../Recdef"  16417 9bc16273c2d4 migrated theory headers to new format haftmann parents: 16413 diff changeset  13 uses ("IntDiv_setup.ML")  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  14 begin  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  15 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  16 declare zless_nat_conj [simp]  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  17 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  18 constdefs  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  19  quorem :: "(int*int) * (int*int) => bool"  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  20  --{*definition of quotient and remainder*}  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  21  "quorem == %((a,b), (q,r)).  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  22  a = b*q + r &  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  23  (if 0 < b then 0\r & r 0)"  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  24 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  25  adjust :: "[int, int*int] => int*int"  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  26  --{*for the division algorithm*}  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  27  "adjust b == %(q,r). if 0 \ r-b then (2*q + 1, r-b)  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  28  else (2*q, r)"  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  29 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  30 text{*algorithm for the case @{text "a\0, b>0"}*}  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  31 consts posDivAlg :: "int*int => int*int"  15620 8ccdc8bc66a2 replaced bool by a new datatype "bit" for binary numerals paulson parents: 15320 diff changeset  32 recdef posDivAlg "measure (%(a,b). nat(a - b + 1))"  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  33  "posDivAlg (a,b) =  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  34  (if (a0) then (0,a)  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  35  else adjust b (posDivAlg(a, 2*b)))"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  36 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  37 text{*algorithm for the case @{text "a<0, b>0"}*}  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  38 consts negDivAlg :: "int*int => int*int"  15620 8ccdc8bc66a2 replaced bool by a new datatype "bit" for binary numerals paulson parents: 15320 diff changeset  39 recdef negDivAlg "measure (%(a,b). nat(- a - b))"  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  40  "negDivAlg (a,b) =  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  41  (if (0\a+b | b\0) then (-1,a+b)  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  42  else adjust b (negDivAlg(a, 2*b)))"  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  43 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  44 text{*algorithm for the general case @{term "b\0"}*}  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  45 constdefs  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  46  negateSnd :: "int*int => int*int"  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  47  "negateSnd == %(q,r). (q,-r)"  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  48 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  49  divAlg :: "int*int => int*int"  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  50  --{*The full division algorithm considers all possible signs for a, b  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  51  including the special case @{text "a=0, b<0"} because  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  52  @{term negDivAlg} requires @{term "a<0"}.*}  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  53  "divAlg ==  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  54  %(a,b). if 0\a then  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  55  if 0\b then posDivAlg (a,b)  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  56  else if a=0 then (0,0)  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  57  else negateSnd (negDivAlg (-a,-b))  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  58  else  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  59  if 0r-b then (2*q+1, r-b) else (2*q, r)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  80  end  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  81 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  82  fun negDivAlg (a,b) =  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  83  if 0\a+b then (~1,a+b)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  84  else let val (q,r) = negDivAlg(a, 2*b)  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  85  in if 0\r-b then (2*q+1, r-b) else (2*q, r)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  86  end;  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  87 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  88  fun negateSnd (q,r:int) = (q,~r);  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  89 14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  90  fun divAlg (a,b) = if 0\a then  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  91  if b>0 then posDivAlg (a,b)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  92  else if a=0 then (0,0)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  93  else negateSnd (negDivAlg (~a,~b))  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  94  else  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  95  if 0 b*q + r; 0 \ r'; r' < b; r < b |]  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  106  ==> q' \ (q::int)"  d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  107 apply (subgoal_tac "r' + b * (q'-q) \ r")  14479 0eca4aabf371 streamlined treatment of quotients for the integers paulson parents: 14473 diff changeset  108  prefer 2 apply (simp add: right_diff_distrib)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  109 apply (subgoal_tac "0 < b * (1 + q - q') ")  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  110 apply (erule_tac [2] order_le_less_trans)  14479 0eca4aabf371 streamlined treatment of quotients for the integers paulson parents: 14473 diff changeset  111  prefer 2 apply (simp add: right_diff_distrib right_distrib)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  112 apply (subgoal_tac "b * q' < b * (1 + q) ")  14479 0eca4aabf371 streamlined treatment of quotients for the integers paulson parents: 14473 diff changeset  113  prefer 2 apply (simp add: right_diff_distrib right_distrib)  14387 e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses paulson parents: 14378 diff changeset  114 apply (simp add: mult_less_cancel_left)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  115 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  116 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  117 lemma unique_quotient_lemma_neg:  16733 236dfafbeb63 linear arithmetic now takes "&" in assumptions apart. nipkow parents: 16417 diff changeset  118  "[| b*q' + r' \ b*q + r; r \ 0; b < r; b < r' |]  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  119  ==> q \ (q'::int)"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  120 by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma,  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  121  auto)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  122 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  123 lemma unique_quotient:  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  124  "[| quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); b \ 0 |]  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  125  ==> q = q'"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  126 apply (simp add: quorem_def linorder_neq_iff split: split_if_asm)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  127 apply (blast intro: order_antisym  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  128  dest: order_eq_refl [THEN unique_quotient_lemma]  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  129  order_eq_refl [THEN unique_quotient_lemma_neg] sym)+  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  130 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  131 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  132 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  133 lemma unique_remainder:  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  134  "[| quorem ((a,b), (q,r)); quorem ((a,b), (q',r')); b \ 0 |]  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  135  ==> r = r'"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  136 apply (subgoal_tac "q = q'")  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  137  apply (simp add: quorem_def)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  138 apply (blast intro: unique_quotient)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  139 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  140 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  141 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  142 subsection{*Correctness of @{term posDivAlg}, the Algorithm for Non-Negative Dividends*}  14271 8ed6989228bb Simplification of the development of Integers paulson parents: 13837 diff changeset  143 8ed6989228bb Simplification of the development of Integers paulson parents: 13837 diff changeset  144 text{*And positive divisors*}  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  145 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  146 lemma adjust_eq [simp]:  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  147  "adjust b (q,r) =  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  148  (let diff = r-b in  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  149  if 0 \ diff then (2*q + 1, diff)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  150  else (2*q, r))"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  151 by (simp add: Let_def adjust_def)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  152 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  153 declare posDivAlg.simps [simp del]  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  154 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  155 text{*use with a simproc to avoid repeatedly proving the premise*}  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  156 lemma posDivAlg_eqn:  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  157  "0 < b ==>  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  158  posDivAlg (a,b) = (if a a --> 0 < b --> quorem ((a, b), posDivAlg (a, b))"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  164 apply (induct_tac a b rule: posDivAlg.induct, auto)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  165  apply (simp_all add: quorem_def)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  166  (*base case: a  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  184  negDivAlg (a,b) =  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  185  (if 0\a+b then (-1,a+b) else adjust b (negDivAlg(a, 2*b)))"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  186 by (rule negDivAlg.simps [THEN trans], simp)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  187 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  188 (*Correctness of negDivAlg: it computes quotients correctly  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  189  It doesn't work if a=0 because the 0/b equals 0, not -1*)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  190 lemma negDivAlg_correct [rule_format]:  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  191  "a < 0 --> 0 < b --> quorem ((a, b), negDivAlg (a, b))"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  192 apply (induct_tac a b rule: negDivAlg.induct, auto)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  193  apply (simp_all add: quorem_def)  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  194  (*base case: 0\a+b*)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  195  apply (simp add: negDivAlg_eqn)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  196 (*main argument*)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  197 apply (subst negDivAlg_eqn, assumption)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  198 apply (erule splitE)  14479 0eca4aabf371 streamlined treatment of quotients for the integers paulson parents: 14473 diff changeset  199 apply (auto simp add: right_distrib Let_def)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  200 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  201 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  202 14271 8ed6989228bb Simplification of the development of Integers paulson parents: 13837 diff changeset  203 subsection{*Existence Shown by Proving the Division Algorithm to be Correct*}  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  204 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  205 (*the case a=0*)  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  206 lemma quorem_0: "b \ 0 ==> quorem ((0,b), (0,0))"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  207 by (auto simp add: quorem_def linorder_neq_iff)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  208 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  209 lemma posDivAlg_0 [simp]: "posDivAlg (0, b) = (0, 0)"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  210 by (subst posDivAlg.simps, auto)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  211 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  212 lemma negDivAlg_minus1 [simp]: "negDivAlg (-1, b) = (-1, b - 1)"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  213 by (subst negDivAlg.simps, auto)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  214 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  215 lemma negateSnd_eq [simp]: "negateSnd(q,r) = (q,-r)"  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  216 by (simp add: negateSnd_def)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  217 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  218 lemma quorem_neg: "quorem ((-a,-b), qr) ==> quorem ((a,b), negateSnd qr)"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  219 by (auto simp add: split_ifs quorem_def)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  220 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  221 lemma divAlg_correct: "b \ 0 ==> quorem ((a,b), divAlg(a,b))"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  222 by (force simp add: linorder_neq_iff quorem_0 divAlg_def quorem_neg  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  223  posDivAlg_correct negDivAlg_correct)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  224 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  225 text{*Arbitrary definitions for division by zero. Useful to simplify  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  226  certain equations.*}  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  227 14271 8ed6989228bb Simplification of the development of Integers paulson parents: 13837 diff changeset  228 lemma DIVISION_BY_ZERO [simp]: "a div (0::int) = 0 & a mod (0::int) = a"  8ed6989228bb Simplification of the development of Integers paulson parents: 13837 diff changeset  229 by (simp add: div_def mod_def divAlg_def posDivAlg.simps)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  230 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  231 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  232 text{*Basic laws about division and remainder*}  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  233 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  234 lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"  15013 34264f5e4691 new treatment of binary numerals paulson parents: 15003 diff changeset  235 apply (case_tac "b = 0", simp)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  236 apply (cut_tac a = a and b = b in divAlg_correct)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  237 apply (auto simp add: quorem_def div_def mod_def)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  238 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  239 13517 42efec18f5b2 Added div+mod cancelling simproc nipkow parents: 13266 diff changeset  240 lemma zdiv_zmod_equality: "(b * (a div b) + (a mod b)) + k = (a::int)+k"  42efec18f5b2 Added div+mod cancelling simproc nipkow parents: 13266 diff changeset  241 by(simp add: zmod_zdiv_equality[symmetric])  42efec18f5b2 Added div+mod cancelling simproc nipkow parents: 13266 diff changeset  242 42efec18f5b2 Added div+mod cancelling simproc nipkow parents: 13266 diff changeset  243 lemma zdiv_zmod_equality2: "((a div b) * b + (a mod b)) + k = (a::int)+k"  15234 ec91a90c604e simplification tweaks for better arithmetic reasoning paulson parents: 15221 diff changeset  244 by(simp add: mult_commute zmod_zdiv_equality[symmetric])  13517 42efec18f5b2 Added div+mod cancelling simproc nipkow parents: 13266 diff changeset  245 42efec18f5b2 Added div+mod cancelling simproc nipkow parents: 13266 diff changeset  246 use "IntDiv_setup.ML"  42efec18f5b2 Added div+mod cancelling simproc nipkow parents: 13266 diff changeset  247 14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  248 lemma pos_mod_conj : "(0::int) < b ==> 0 \ a mod b & a mod b < b"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  249 apply (cut_tac a = a and b = b in divAlg_correct)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  250 apply (auto simp add: quorem_def mod_def)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  251 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  252 18648 22f96cd085d5 tidied, and giving theorems names paulson parents: 17508 diff changeset  253 lemmas pos_mod_sign = pos_mod_conj [THEN conjunct1, standard]  22f96cd085d5 tidied, and giving theorems names paulson parents: 17508 diff changeset  254  and pos_mod_bound = pos_mod_conj [THEN conjunct2, standard]  22f96cd085d5 tidied, and giving theorems names paulson parents: 17508 diff changeset  255 22f96cd085d5 tidied, and giving theorems names paulson parents: 17508 diff changeset  256 declare pos_mod_sign[simp] pos_mod_bound[simp]  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  257 14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  258 lemma neg_mod_conj : "b < (0::int) ==> a mod b \ 0 & b < a mod b"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  259 apply (cut_tac a = a and b = b in divAlg_correct)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  260 apply (auto simp add: quorem_def div_def mod_def)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  261 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  262 18648 22f96cd085d5 tidied, and giving theorems names paulson parents: 17508 diff changeset  263 lemmas neg_mod_sign = neg_mod_conj [THEN conjunct1, standard]  22f96cd085d5 tidied, and giving theorems names paulson parents: 17508 diff changeset  264  and neg_mod_bound = neg_mod_conj [THEN conjunct2, standard]  22f96cd085d5 tidied, and giving theorems names paulson parents: 17508 diff changeset  265 declare neg_mod_sign[simp] neg_mod_bound[simp]  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  266 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  267 13260 ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  268 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  269 subsection{*General Properties of div and mod*}  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  270 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  271 lemma quorem_div_mod: "b \ 0 ==> quorem ((a, b), (a div b, a mod b))"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  272 apply (cut_tac a = a and b = b in zmod_zdiv_equality)  13788 fd03c4ab89d4 pos/neg_mod_sign/bound are now simp rules. nipkow parents: 13716 diff changeset  273 apply (force simp add: quorem_def linorder_neq_iff)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  274 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  275 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  276 lemma quorem_div: "[| quorem((a,b),(q,r)); b \ 0 |] ==> a div b = q"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  277 by (simp add: quorem_div_mod [THEN unique_quotient])  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  278 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  279 lemma quorem_mod: "[| quorem((a,b),(q,r)); b \ 0 |] ==> a mod b = r"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  280 by (simp add: quorem_div_mod [THEN unique_remainder])  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  281 14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  282 lemma div_pos_pos_trivial: "[| (0::int) \ a; a < b |] ==> a div b = 0"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  283 apply (rule quorem_div)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  284 apply (auto simp add: quorem_def)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  285 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  286 14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  287 lemma div_neg_neg_trivial: "[| a \ (0::int); b < a |] ==> a div b = 0"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  288 apply (rule quorem_div)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  289 apply (auto simp add: quorem_def)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  290 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  291 14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  292 lemma div_pos_neg_trivial: "[| (0::int) < a; a+b \ 0 |] ==> a div b = -1"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  293 apply (rule quorem_div)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  294 apply (auto simp add: quorem_def)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  295 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  296 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  297 (*There is no div_neg_pos_trivial because 0 div b = 0 would supersede it*)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  298 14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  299 lemma mod_pos_pos_trivial: "[| (0::int) \ a; a < b |] ==> a mod b = a"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  300 apply (rule_tac q = 0 in quorem_mod)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  301 apply (auto simp add: quorem_def)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  302 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  303 14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  304 lemma mod_neg_neg_trivial: "[| a \ (0::int); b < a |] ==> a mod b = a"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  305 apply (rule_tac q = 0 in quorem_mod)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  306 apply (auto simp add: quorem_def)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  307 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  308 14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  309 lemma mod_pos_neg_trivial: "[| (0::int) < a; a+b \ 0 |] ==> a mod b = a+b"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  310 apply (rule_tac q = "-1" in quorem_mod)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  311 apply (auto simp add: quorem_def)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  312 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  313 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  314 text{*There is no @{text mod_neg_pos_trivial}.*}  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  315 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  316 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  317 (*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  318 lemma zdiv_zminus_zminus [simp]: "(-a) div (-b) = a div (b::int)"  15013 34264f5e4691 new treatment of binary numerals paulson parents: 15003 diff changeset  319 apply (case_tac "b = 0", simp)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  320 apply (simp add: quorem_div_mod [THEN quorem_neg, simplified,  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  321  THEN quorem_div, THEN sym])  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  322 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  323 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  324 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  325 (*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  326 lemma zmod_zminus_zminus [simp]: "(-a) mod (-b) = - (a mod (b::int))"  15013 34264f5e4691 new treatment of binary numerals paulson parents: 15003 diff changeset  327 apply (case_tac "b = 0", simp)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  328 apply (subst quorem_div_mod [THEN quorem_neg, simplified, THEN quorem_mod],  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  329  auto)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  330 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  331 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  332 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  333 subsection{*Laws for div and mod with Unary Minus*}  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  334 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  335 lemma zminus1_lemma:  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  336  "quorem((a,b),(q,r))  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  337  ==> quorem ((-a,b), (if r=0 then -q else -q - 1),  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  338  (if r=0 then 0 else b-r))"  14479 0eca4aabf371 streamlined treatment of quotients for the integers paulson parents: 14473 diff changeset  339 by (force simp add: split_ifs quorem_def linorder_neq_iff right_diff_distrib)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  340 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  341 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  342 lemma zdiv_zminus1_eq_if:  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  343  "b \ (0::int)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  344  ==> (-a) div b =  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  345  (if a mod b = 0 then - (a div b) else - (a div b) - 1)"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  346 by (blast intro: quorem_div_mod [THEN zminus1_lemma, THEN quorem_div])  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  347 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  348 lemma zmod_zminus1_eq_if:  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  349  "(-a::int) mod b = (if a mod b = 0 then 0 else b - (a mod b))"  15013 34264f5e4691 new treatment of binary numerals paulson parents: 15003 diff changeset  350 apply (case_tac "b = 0", simp)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  351 apply (blast intro: quorem_div_mod [THEN zminus1_lemma, THEN quorem_mod])  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  352 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  353 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  354 lemma zdiv_zminus2: "a div (-b) = (-a::int) div b"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  355 by (cut_tac a = "-a" in zdiv_zminus_zminus, auto)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  356 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  357 lemma zmod_zminus2: "a mod (-b) = - ((-a::int) mod b)"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  358 by (cut_tac a = "-a" and b = b in zmod_zminus_zminus, auto)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  359 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  360 lemma zdiv_zminus2_eq_if:  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  361  "b \ (0::int)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  362  ==> a div (-b) =  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  363  (if a mod b = 0 then - (a div b) else - (a div b) - 1)"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  364 by (simp add: zdiv_zminus1_eq_if zdiv_zminus2)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  365 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  366 lemma zmod_zminus2_eq_if:  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  367  "a mod (-b::int) = (if a mod b = 0 then 0 else (a mod b) - b)"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  368 by (simp add: zmod_zminus1_eq_if zmod_zminus2)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  369 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  370 14271 8ed6989228bb Simplification of the development of Integers paulson parents: 13837 diff changeset  371 subsection{*Division of a Number by Itself*}  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  372 14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  373 lemma self_quotient_aux1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 \ q"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  374 apply (subgoal_tac "0 < a*q")  14353 79f9fbef9106 Added lemmas to Ring_and_Field with slightly modified simplification rules paulson parents: 14288 diff changeset  375  apply (simp add: zero_less_mult_iff, arith)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  376 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  377 14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  378 lemma self_quotient_aux2: "[| (0::int) < a; a = r + a*q; 0 \ r |] ==> q \ 1"  d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  379 apply (subgoal_tac "0 \ a* (1-q) ")  14353 79f9fbef9106 Added lemmas to Ring_and_Field with slightly modified simplification rules paulson parents: 14288 diff changeset  380  apply (simp add: zero_le_mult_iff)  14479 0eca4aabf371 streamlined treatment of quotients for the integers paulson parents: 14473 diff changeset  381 apply (simp add: right_diff_distrib)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  382 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  383 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  384 lemma self_quotient: "[| quorem((a,a),(q,r)); a \ (0::int) |] ==> q = 1"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  385 apply (simp add: split_ifs quorem_def linorder_neq_iff)  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  386 apply (rule order_antisym, safe, simp_all)  13524 604d0f3622d6 *** empty log message *** wenzelm parents: 13517 diff changeset  387 apply (rule_tac [3] a = "-a" and r = "-r" in self_quotient_aux1)  604d0f3622d6 *** empty log message *** wenzelm parents: 13517 diff changeset  388 apply (rule_tac a = "-a" and r = "-r" in self_quotient_aux2)  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  389 apply (force intro: self_quotient_aux1 self_quotient_aux2 simp add: add_commute)+  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  390 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  391 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  392 lemma self_remainder: "[| quorem((a,a),(q,r)); a \ (0::int) |] ==> r = 0"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  393 apply (frule self_quotient, assumption)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  394 apply (simp add: quorem_def)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  395 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  396 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  397 lemma zdiv_self [simp]: "a \ 0 ==> a div a = (1::int)"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  398 by (simp add: quorem_div_mod [THEN self_quotient])  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  399 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  400 (*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  401 lemma zmod_self [simp]: "a mod a = (0::int)"  15013 34264f5e4691 new treatment of binary numerals paulson parents: 15003 diff changeset  402 apply (case_tac "a = 0", simp)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  403 apply (simp add: quorem_div_mod [THEN self_remainder])  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  404 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  405 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  406 14271 8ed6989228bb Simplification of the development of Integers paulson parents: 13837 diff changeset  407 subsection{*Computation of Division and Remainder*}  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  408 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  409 lemma zdiv_zero [simp]: "(0::int) div b = 0"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  410 by (simp add: div_def divAlg_def)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  411 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  412 lemma div_eq_minus1: "(0::int) < b ==> -1 div b = -1"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  413 by (simp add: div_def divAlg_def)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  414 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  415 lemma zmod_zero [simp]: "(0::int) mod b = 0"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  416 by (simp add: mod_def divAlg_def)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  417 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  418 lemma zdiv_minus1: "(0::int) < b ==> -1 div b = -1"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  419 by (simp add: div_def divAlg_def)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  420 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  421 lemma zmod_minus1: "(0::int) < b ==> -1 mod b = b - 1"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  422 by (simp add: mod_def divAlg_def)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  423 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  424 text{*a positive, b positive *}  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  425 14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  426 lemma div_pos_pos: "[| 0 < a; 0 \ b |] ==> a div b = fst (posDivAlg(a,b))"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  427 by (simp add: div_def divAlg_def)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  428 14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  429 lemma mod_pos_pos: "[| 0 < a; 0 \ b |] ==> a mod b = snd (posDivAlg(a,b))"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  430 by (simp add: mod_def divAlg_def)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  431 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  432 text{*a negative, b positive *}  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  433 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  434 lemma div_neg_pos: "[| a < 0; 0 < b |] ==> a div b = fst (negDivAlg(a,b))"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  435 by (simp add: div_def divAlg_def)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  436 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  437 lemma mod_neg_pos: "[| a < 0; 0 < b |] ==> a mod b = snd (negDivAlg(a,b))"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  438 by (simp add: mod_def divAlg_def)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  439 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  440 text{*a positive, b negative *}  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  441 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  442 lemma div_pos_neg:  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  443  "[| 0 < a; b < 0 |] ==> a div b = fst (negateSnd(negDivAlg(-a,-b)))"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  444 by (simp add: div_def divAlg_def)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  445 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  446 lemma mod_pos_neg:  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  447  "[| 0 < a; b < 0 |] ==> a mod b = snd (negateSnd(negDivAlg(-a,-b)))"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  448 by (simp add: mod_def divAlg_def)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  449 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  450 text{*a negative, b negative *}  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  451 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  452 lemma div_neg_neg:  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  453  "[| a < 0; b \ 0 |] ==> a div b = fst (negateSnd(posDivAlg(-a,-b)))"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  454 by (simp add: div_def divAlg_def)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  455 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  456 lemma mod_neg_neg:  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  457  "[| a < 0; b \ 0 |] ==> a mod b = snd (negateSnd(posDivAlg(-a,-b)))"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  458 by (simp add: mod_def divAlg_def)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  459 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  460 text {*Simplify expresions in which div and mod combine numerical constants*}  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  461 17085 5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  462 lemmas div_pos_pos_number_of =  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  463  div_pos_pos [of "number_of v" "number_of w", standard]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  464 declare div_pos_pos_number_of [simp]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  465 5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  466 lemmas div_neg_pos_number_of =  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  467  div_neg_pos [of "number_of v" "number_of w", standard]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  468 declare div_neg_pos_number_of [simp]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  469 5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  470 lemmas div_pos_neg_number_of =  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  471  div_pos_neg [of "number_of v" "number_of w", standard]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  472 declare div_pos_neg_number_of [simp]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  473 5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  474 lemmas div_neg_neg_number_of =  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  475  div_neg_neg [of "number_of v" "number_of w", standard]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  476 declare div_neg_neg_number_of [simp]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  477 5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  478 5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  479 lemmas mod_pos_pos_number_of =  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  480  mod_pos_pos [of "number_of v" "number_of w", standard]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  481 declare mod_pos_pos_number_of [simp]  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  482 17085 5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  483 lemmas mod_neg_pos_number_of =  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  484  mod_neg_pos [of "number_of v" "number_of w", standard]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  485 declare mod_neg_pos_number_of [simp]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  486 5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  487 lemmas mod_pos_neg_number_of =  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  488  mod_pos_neg [of "number_of v" "number_of w", standard]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  489 declare mod_pos_neg_number_of [simp]  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  490 17085 5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  491 lemmas mod_neg_neg_number_of =  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  492  mod_neg_neg [of "number_of v" "number_of w", standard]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  493 declare mod_neg_neg_number_of [simp]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  494 5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  495 5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  496 lemmas posDivAlg_eqn_number_of =  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  497  posDivAlg_eqn [of "number_of v" "number_of w", standard]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  498 declare posDivAlg_eqn_number_of [simp]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  499 5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  500 lemmas negDivAlg_eqn_number_of =  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  501  negDivAlg_eqn [of "number_of v" "number_of w", standard]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  502 declare negDivAlg_eqn_number_of [simp]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  503 13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  504 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  505 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  506 text{*Special-case simplification *}  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  507 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  508 lemma zmod_1 [simp]: "a mod (1::int) = 0"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  509 apply (cut_tac a = a and b = 1 in pos_mod_sign)  13788 fd03c4ab89d4 pos/neg_mod_sign/bound are now simp rules. nipkow parents: 13716 diff changeset  510 apply (cut_tac [2] a = a and b = 1 in pos_mod_bound)  fd03c4ab89d4 pos/neg_mod_sign/bound are now simp rules. nipkow parents: 13716 diff changeset  511 apply (auto simp del:pos_mod_bound pos_mod_sign)  fd03c4ab89d4 pos/neg_mod_sign/bound are now simp rules. nipkow parents: 13716 diff changeset  512 done  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  513 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  514 lemma zdiv_1 [simp]: "a div (1::int) = a"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  515 by (cut_tac a = a and b = 1 in zmod_zdiv_equality, auto)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  516 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  517 lemma zmod_minus1_right [simp]: "a mod (-1::int) = 0"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  518 apply (cut_tac a = a and b = "-1" in neg_mod_sign)  13788 fd03c4ab89d4 pos/neg_mod_sign/bound are now simp rules. nipkow parents: 13716 diff changeset  519 apply (cut_tac [2] a = a and b = "-1" in neg_mod_bound)  fd03c4ab89d4 pos/neg_mod_sign/bound are now simp rules. nipkow parents: 13716 diff changeset  520 apply (auto simp del: neg_mod_sign neg_mod_bound)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  521 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  522 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  523 lemma zdiv_minus1_right [simp]: "a div (-1::int) = -a"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  524 by (cut_tac a = a and b = "-1" in zmod_zdiv_equality, auto)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  525 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  526 (** The last remaining special cases for constant arithmetic:  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  527  1 div z and 1 mod z **)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  528 17085 5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  529 lemmas div_pos_pos_1_number_of =  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  530  div_pos_pos [OF int_0_less_1, of "number_of w", standard]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  531 declare div_pos_pos_1_number_of [simp]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  532 5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  533 lemmas div_pos_neg_1_number_of =  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  534  div_pos_neg [OF int_0_less_1, of "number_of w", standard]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  535 declare div_pos_neg_1_number_of [simp]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  536 5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  537 lemmas mod_pos_pos_1_number_of =  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  538  mod_pos_pos [OF int_0_less_1, of "number_of w", standard]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  539 declare mod_pos_pos_1_number_of [simp]  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  540 17085 5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  541 lemmas mod_pos_neg_1_number_of =  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  542  mod_pos_neg [OF int_0_less_1, of "number_of w", standard]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  543 declare mod_pos_neg_1_number_of [simp]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  544 5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  545 5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  546 lemmas posDivAlg_eqn_1_number_of =  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  547  posDivAlg_eqn [of concl: 1 "number_of w", standard]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  548 declare posDivAlg_eqn_1_number_of [simp]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  549 5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  550 lemmas negDivAlg_eqn_1_number_of =  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  551  negDivAlg_eqn [of concl: 1 "number_of w", standard]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  552 declare negDivAlg_eqn_1_number_of [simp]  5b57f995a179 more simprules now have names paulson parents: 17084 diff changeset  553 13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  554 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  555 14271 8ed6989228bb Simplification of the development of Integers paulson parents: 13837 diff changeset  556 subsection{*Monotonicity in the First Argument (Dividend)*}  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  557 14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  558 lemma zdiv_mono1: "[| a \ a'; 0 < (b::int) |] ==> a div b \ a' div b"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  559 apply (cut_tac a = a and b = b in zmod_zdiv_equality)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  560 apply (cut_tac a = a' and b = b in zmod_zdiv_equality)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  561 apply (rule unique_quotient_lemma)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  562 apply (erule subst)  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  563 apply (erule subst, simp_all)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  564 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  565 14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  566 lemma zdiv_mono1_neg: "[| a \ a'; (b::int) < 0 |] ==> a' div b \ a div b"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  567 apply (cut_tac a = a and b = b in zmod_zdiv_equality)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  568 apply (cut_tac a = a' and b = b in zmod_zdiv_equality)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  569 apply (rule unique_quotient_lemma_neg)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  570 apply (erule subst)  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  571 apply (erule subst, simp_all)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  572 done  6917 eba301caceea Introduction of integer division algorithm paulson parents: diff changeset  573 eba301caceea Introduction of integer division algorithm paulson parents: diff changeset  574 14271 8ed6989228bb Simplification of the development of Integers paulson parents: 13837 diff changeset  575 subsection{*Monotonicity in the Second Argument (Divisor)*}  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  576 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  577 lemma q_pos_lemma:  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  578  "[| 0 \ b'*q' + r'; r' < b'; 0 < b' |] ==> 0 \ (q'::int)"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  579 apply (subgoal_tac "0 < b'* (q' + 1) ")  14353 79f9fbef9106 Added lemmas to Ring_and_Field with slightly modified simplification rules paulson parents: 14288 diff changeset  580  apply (simp add: zero_less_mult_iff)  14479 0eca4aabf371 streamlined treatment of quotients for the integers paulson parents: 14473 diff changeset  581 apply (simp add: right_distrib)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  582 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  583 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  584 lemma zdiv_mono2_lemma:  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  585  "[| b*q + r = b'*q' + r'; 0 \ b'*q' + r';  d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  586  r' < b'; 0 \ r; 0 < b'; b' \ b |]  d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  587  ==> q \ (q'::int)"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  588 apply (frule q_pos_lemma, assumption+)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  589 apply (subgoal_tac "b*q < b* (q' + 1) ")  14387 e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses paulson parents: 14378 diff changeset  590  apply (simp add: mult_less_cancel_left)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  591 apply (subgoal_tac "b*q = r' - r + b'*q'")  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  592  prefer 2 apply simp  14479 0eca4aabf371 streamlined treatment of quotients for the integers paulson parents: 14473 diff changeset  593 apply (simp (no_asm_simp) add: right_distrib)  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  594 apply (subst add_commute, rule zadd_zless_mono, arith)  14378 69c4d5997669 generic of_nat and of_int functions, and generalization of iszero paulson parents: 14353 diff changeset  595 apply (rule mult_right_mono, auto)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  596 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  597 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  598 lemma zdiv_mono2:  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  599  "[| (0::int) \ a; 0 < b'; b' \ b |] ==> a div b \ a div b'"  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  600 apply (subgoal_tac "b \ 0")  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  601  prefer 2 apply arith  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  602 apply (cut_tac a = a and b = b in zmod_zdiv_equality)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  603 apply (cut_tac a = a and b = b' in zmod_zdiv_equality)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  604 apply (rule zdiv_mono2_lemma)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  605 apply (erule subst)  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  606 apply (erule subst, simp_all)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  607 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  608 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  609 lemma q_neg_lemma:  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  610  "[| b'*q' + r' < 0; 0 \ r'; 0 < b' |] ==> q' \ (0::int)"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  611 apply (subgoal_tac "b'*q' < 0")  14353 79f9fbef9106 Added lemmas to Ring_and_Field with slightly modified simplification rules paulson parents: 14288 diff changeset  612  apply (simp add: mult_less_0_iff, arith)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  613 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  614 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  615 lemma zdiv_mono2_neg_lemma:  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  616  "[| b*q + r = b'*q' + r'; b'*q' + r' < 0;  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  617  r < b; 0 \ r'; 0 < b'; b' \ b |]  d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  618  ==> q' \ (q::int)"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  619 apply (frule q_neg_lemma, assumption+)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  620 apply (subgoal_tac "b*q' < b* (q + 1) ")  14387 e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses paulson parents: 14378 diff changeset  621  apply (simp add: mult_less_cancel_left)  14479 0eca4aabf371 streamlined treatment of quotients for the integers paulson parents: 14473 diff changeset  622 apply (simp add: right_distrib)  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  623 apply (subgoal_tac "b*q' \ b'*q'")  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  624  prefer 2 apply (simp add: mult_right_mono_neg, arith)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  625 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  626 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  627 lemma zdiv_mono2_neg:  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  628  "[| a < (0::int); 0 < b'; b' \ b |] ==> a div b' \ a div b"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  629 apply (cut_tac a = a and b = b in zmod_zdiv_equality)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  630 apply (cut_tac a = a and b = b' in zmod_zdiv_equality)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  631 apply (rule zdiv_mono2_neg_lemma)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  632 apply (erule subst)  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  633 apply (erule subst, simp_all)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  634 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  635 14271 8ed6989228bb Simplification of the development of Integers paulson parents: 13837 diff changeset  636 subsection{*More Algebraic Laws for div and mod*}  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  637 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  638 text{*proving (a*b) div c = a * (b div c) + a * (b mod c) *}  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  639 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  640 lemma zmult1_lemma:  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  641  "[| quorem((b,c),(q,r)); c \ 0 |]  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  642  ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"  14479 0eca4aabf371 streamlined treatment of quotients for the integers paulson parents: 14473 diff changeset  643 by (force simp add: split_ifs quorem_def linorder_neq_iff right_distrib)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  644 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  645 lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"  15013 34264f5e4691 new treatment of binary numerals paulson parents: 15003 diff changeset  646 apply (case_tac "c = 0", simp)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  647 apply (blast intro: quorem_div_mod [THEN zmult1_lemma, THEN quorem_div])  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  648 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  649 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  650 lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)"  15013 34264f5e4691 new treatment of binary numerals paulson parents: 15003 diff changeset  651 apply (case_tac "c = 0", simp)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  652 apply (blast intro: quorem_div_mod [THEN zmult1_lemma, THEN quorem_mod])  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  653 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  654 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  655 lemma zmod_zmult1_eq': "(a*b) mod (c::int) = ((a mod c) * b) mod c"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  656 apply (rule trans)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  657 apply (rule_tac s = "b*a mod c" in trans)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  658 apply (rule_tac [2] zmod_zmult1_eq)  15234 ec91a90c604e simplification tweaks for better arithmetic reasoning paulson parents: 15221 diff changeset  659 apply (simp_all add: mult_commute)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  660 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  661 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  662 lemma zmod_zmult_distrib: "(a*b) mod (c::int) = ((a mod c) * (b mod c)) mod c"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  663 apply (rule zmod_zmult1_eq' [THEN trans])  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  664 apply (rule zmod_zmult1_eq)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  665 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  666 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  667 lemma zdiv_zmult_self1 [simp]: "b \ (0::int) ==> (a*b) div b = a"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  668 by (simp add: zdiv_zmult1_eq)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  669 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  670 lemma zdiv_zmult_self2 [simp]: "b \ (0::int) ==> (b*a) div b = a"  15234 ec91a90c604e simplification tweaks for better arithmetic reasoning paulson parents: 15221 diff changeset  671 by (subst mult_commute, erule zdiv_zmult_self1)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  672 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  673 lemma zmod_zmult_self1 [simp]: "(a*b) mod b = (0::int)"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  674 by (simp add: zmod_zmult1_eq)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  675 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  676 lemma zmod_zmult_self2 [simp]: "(b*a) mod b = (0::int)"  15234 ec91a90c604e simplification tweaks for better arithmetic reasoning paulson parents: 15221 diff changeset  677 by (simp add: mult_commute zmod_zmult1_eq)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  678 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  679 lemma zmod_eq_0_iff: "(m mod d = 0) = (EX q::int. m = d*q)"  13517 42efec18f5b2 Added div+mod cancelling simproc nipkow parents: 13266 diff changeset  680 proof  42efec18f5b2 Added div+mod cancelling simproc nipkow parents: 13266 diff changeset  681  assume "m mod d = 0"  14473 846c237bd9b3 stylistic tweaks paulson parents: 14387 diff changeset  682  with zmod_zdiv_equality[of m d] show "EX q::int. m = d*q" by auto  13517 42efec18f5b2 Added div+mod cancelling simproc nipkow parents: 13266 diff changeset  683 next  42efec18f5b2 Added div+mod cancelling simproc nipkow parents: 13266 diff changeset  684  assume "EX q::int. m = d*q"  42efec18f5b2 Added div+mod cancelling simproc nipkow parents: 13266 diff changeset  685  thus "m mod d = 0" by auto  42efec18f5b2 Added div+mod cancelling simproc nipkow parents: 13266 diff changeset  686 qed  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  687 17084 fb0a80aef0be classical rules must have names for ATP integration paulson parents: 16733 diff changeset  688 lemmas zmod_eq_0D = zmod_eq_0_iff [THEN iffD1]  fb0a80aef0be classical rules must have names for ATP integration paulson parents: 16733 diff changeset  689 declare zmod_eq_0D [dest!]  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  690 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  691 text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  692 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  693 lemma zadd1_lemma:  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  694  "[| quorem((a,c),(aq,ar)); quorem((b,c),(bq,br)); c \ 0 |]  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  695  ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"  14479 0eca4aabf371 streamlined treatment of quotients for the integers paulson parents: 14473 diff changeset  696 by (force simp add: split_ifs quorem_def linorder_neq_iff right_distrib)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  697 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  698 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  699 lemma zdiv_zadd1_eq:  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  700  "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"  15013 34264f5e4691 new treatment of binary numerals paulson parents: 15003 diff changeset  701 apply (case_tac "c = 0", simp)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  702 apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_div)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  703 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  704 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  705 lemma zmod_zadd1_eq: "(a+b) mod (c::int) = (a mod c + b mod c) mod c"  15013 34264f5e4691 new treatment of binary numerals paulson parents: 15003 diff changeset  706 apply (case_tac "c = 0", simp)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  707 apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  708 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  709 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  710 lemma mod_div_trivial [simp]: "(a mod b) div b = (0::int)"  15013 34264f5e4691 new treatment of binary numerals paulson parents: 15003 diff changeset  711 apply (case_tac "b = 0", simp)  13788 fd03c4ab89d4 pos/neg_mod_sign/bound are now simp rules. nipkow parents: 13716 diff changeset  712 apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  713 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  714 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  715 lemma mod_mod_trivial [simp]: "(a mod b) mod b = a mod (b::int)"  15013 34264f5e4691 new treatment of binary numerals paulson parents: 15003 diff changeset  716 apply (case_tac "b = 0", simp)  13788 fd03c4ab89d4 pos/neg_mod_sign/bound are now simp rules. nipkow parents: 13716 diff changeset  717 apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  718 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  719 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  720 lemma zmod_zadd_left_eq: "(a+b) mod (c::int) = ((a mod c) + b) mod c"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  721 apply (rule trans [symmetric])  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  722 apply (rule zmod_zadd1_eq, simp)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  723 apply (rule zmod_zadd1_eq [symmetric])  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  724 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  725 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  726 lemma zmod_zadd_right_eq: "(a+b) mod (c::int) = (a + (b mod c)) mod c"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  727 apply (rule trans [symmetric])  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  728 apply (rule zmod_zadd1_eq, simp)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  729 apply (rule zmod_zadd1_eq [symmetric])  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  730 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  731 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  732 lemma zdiv_zadd_self1[simp]: "a \ (0::int) ==> (a+b) div a = b div a + 1"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  733 by (simp add: zdiv_zadd1_eq)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  734 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  735 lemma zdiv_zadd_self2[simp]: "a \ (0::int) ==> (b+a) div a = b div a + 1"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  736 by (simp add: zdiv_zadd1_eq)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  737 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  738 lemma zmod_zadd_self1[simp]: "(a+b) mod a = b mod (a::int)"  15013 34264f5e4691 new treatment of binary numerals paulson parents: 15003 diff changeset  739 apply (case_tac "a = 0", simp)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  740 apply (simp add: zmod_zadd1_eq)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  741 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  742 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  743 lemma zmod_zadd_self2[simp]: "(b+a) mod a = b mod (a::int)"  15013 34264f5e4691 new treatment of binary numerals paulson parents: 15003 diff changeset  744 apply (case_tac "a = 0", simp)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  745 apply (simp add: zmod_zadd1_eq)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  746 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  747 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  748 14271 8ed6989228bb Simplification of the development of Integers paulson parents: 13837 diff changeset  749 subsection{*Proving @{term "a div (b*c) = (a div b) div c"} *}  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  750 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  751 (*The condition c>0 seems necessary. Consider that 7 div ~6 = ~2 but  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  752  7 div 2 div ~3 = 3 div ~3 = ~1. The subcase (a div b) mod c = 0 seems  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  753  to cause particular problems.*)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  754 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  755 text{*first, four lemmas to bound the remainder for the cases b<0 and b>0 *}  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  756 14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  757 lemma zmult2_lemma_aux1: "[| (0::int) < c; b < r; r \ 0 |] ==> b*c < b*(q mod c) + r"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  758 apply (subgoal_tac "b * (c - q mod c) < r * 1")  14479 0eca4aabf371 streamlined treatment of quotients for the integers paulson parents: 14473 diff changeset  759 apply (simp add: right_diff_distrib)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  760 apply (rule order_le_less_trans)  14378 69c4d5997669 generic of_nat and of_int functions, and generalization of iszero paulson parents: 14353 diff changeset  761 apply (erule_tac [2] mult_strict_right_mono)  69c4d5997669 generic of_nat and of_int functions, and generalization of iszero paulson parents: 14353 diff changeset  762 apply (rule mult_left_mono_neg)  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  763 apply (auto simp add: compare_rls add_commute [of 1]  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  764  add1_zle_eq pos_mod_bound)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  765 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  766 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  767 lemma zmult2_lemma_aux2:  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  768  "[| (0::int) < c; b < r; r \ 0 |] ==> b * (q mod c) + r \ 0"  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  769 apply (subgoal_tac "b * (q mod c) \ 0")  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  770  apply arith  14353 79f9fbef9106 Added lemmas to Ring_and_Field with slightly modified simplification rules paulson parents: 14288 diff changeset  771 apply (simp add: mult_le_0_iff)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  772 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  773 14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  774 lemma zmult2_lemma_aux3: "[| (0::int) < c; 0 \ r; r < b |] ==> 0 \ b * (q mod c) + r"  d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  775 apply (subgoal_tac "0 \ b * (q mod c) ")  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  776 apply arith  14353 79f9fbef9106 Added lemmas to Ring_and_Field with slightly modified simplification rules paulson parents: 14288 diff changeset  777 apply (simp add: zero_le_mult_iff)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  778 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  779 14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  780 lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 \ r; r < b |] ==> b * (q mod c) + r < b * c"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  781 apply (subgoal_tac "r * 1 < b * (c - q mod c) ")  14479 0eca4aabf371 streamlined treatment of quotients for the integers paulson parents: 14473 diff changeset  782 apply (simp add: right_diff_distrib)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  783 apply (rule order_less_le_trans)  14378 69c4d5997669 generic of_nat and of_int functions, and generalization of iszero paulson parents: 14353 diff changeset  784 apply (erule mult_strict_right_mono)  14387 e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses paulson parents: 14378 diff changeset  785 apply (rule_tac [2] mult_left_mono)  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  786 apply (auto simp add: compare_rls add_commute [of 1]  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  787  add1_zle_eq pos_mod_bound)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  788 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  789 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  790 lemma zmult2_lemma: "[| quorem ((a,b), (q,r)); b \ 0; 0 < c |]  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  791  ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"  14271 8ed6989228bb Simplification of the development of Integers paulson parents: 13837 diff changeset  792 by (auto simp add: mult_ac quorem_def linorder_neq_iff  14479 0eca4aabf371 streamlined treatment of quotients for the integers paulson parents: 14473 diff changeset  793  zero_less_mult_iff right_distrib [symmetric]  13524 604d0f3622d6 *** empty log message *** wenzelm parents: 13517 diff changeset  794  zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  795 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  796 lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c"  15013 34264f5e4691 new treatment of binary numerals paulson parents: 15003 diff changeset  797 apply (case_tac "b = 0", simp)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  798 apply (force simp add: quorem_div_mod [THEN zmult2_lemma, THEN quorem_div])  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  799 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  800 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  801 lemma zmod_zmult2_eq:  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  802  "(0::int) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b"  15013 34264f5e4691 new treatment of binary numerals paulson parents: 15003 diff changeset  803 apply (case_tac "b = 0", simp)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  804 apply (force simp add: quorem_div_mod [THEN zmult2_lemma, THEN quorem_mod])  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  805 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  806 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  807 14271 8ed6989228bb Simplification of the development of Integers paulson parents: 13837 diff changeset  808 subsection{*Cancellation of Common Factors in div*}  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  809 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  810 lemma zdiv_zmult_zmult1_aux1:  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  811  "[| (0::int) < b; c \ 0 |] ==> (c*a) div (c*b) = a div b"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  812 by (subst zdiv_zmult2_eq, auto)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  813 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  814 lemma zdiv_zmult_zmult1_aux2:  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  815  "[| b < (0::int); c \ 0 |] ==> (c*a) div (c*b) = a div b"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  816 apply (subgoal_tac " (c * (-a)) div (c * (-b)) = (-a) div (-b) ")  13524 604d0f3622d6 *** empty log message *** wenzelm parents: 13517 diff changeset  817 apply (rule_tac [2] zdiv_zmult_zmult1_aux1, auto)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  818 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  819 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  820 lemma zdiv_zmult_zmult1: "c \ (0::int) ==> (c*a) div (c*b) = a div b"  15013 34264f5e4691 new treatment of binary numerals paulson parents: 15003 diff changeset  821 apply (case_tac "b = 0", simp)  13524 604d0f3622d6 *** empty log message *** wenzelm parents: 13517 diff changeset  822 apply (auto simp add: linorder_neq_iff zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  823 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  824 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  825 lemma zdiv_zmult_zmult2: "c \ (0::int) ==> (a*c) div (b*c) = a div b"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  826 apply (drule zdiv_zmult_zmult1)  15234 ec91a90c604e simplification tweaks for better arithmetic reasoning paulson parents: 15221 diff changeset  827 apply (auto simp add: mult_commute)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  828 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  829 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  830 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  831 14271 8ed6989228bb Simplification of the development of Integers paulson parents: 13837 diff changeset  832 subsection{*Distribution of Factors over mod*}  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  833 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  834 lemma zmod_zmult_zmult1_aux1:  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  835  "[| (0::int) < b; c \ 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  836 by (subst zmod_zmult2_eq, auto)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  837 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  838 lemma zmod_zmult_zmult1_aux2:  8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  839  "[| b < (0::int); c \ 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  840 apply (subgoal_tac " (c * (-a)) mod (c * (-b)) = c * ((-a) mod (-b))")  13524 604d0f3622d6 *** empty log message *** wenzelm parents: 13517 diff changeset  841 apply (rule_tac [2] zmod_zmult_zmult1_aux1, auto)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  842 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  843 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  844 lemma zmod_zmult_zmult1: "(c*a) mod (c*b) = (c::int) * (a mod b)"  15013 34264f5e4691 new treatment of binary numerals paulson parents: 15003 diff changeset  845 apply (case_tac "b = 0", simp)  34264f5e4691 new treatment of binary numerals paulson parents: 15003 diff changeset  846 apply (case_tac "c = 0", simp)  13524 604d0f3622d6 *** empty log message *** wenzelm parents: 13517 diff changeset  847 apply (auto simp add: linorder_neq_iff zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  848 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  849 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  850 lemma zmod_zmult_zmult2: "(a*c) mod (b*c) = (a mod b) * (c::int)"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  851 apply (cut_tac c = c in zmod_zmult_zmult1)  15234 ec91a90c604e simplification tweaks for better arithmetic reasoning paulson parents: 15221 diff changeset  852 apply (auto simp add: mult_commute)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  853 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  854 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  855 14271 8ed6989228bb Simplification of the development of Integers paulson parents: 13837 diff changeset  856 subsection {*Splitting Rules for div and mod*}  13260 ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  857 ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  858 text{*The proofs of the two lemmas below are essentially identical*}  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  859 ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  860 lemma split_pos_lemma:  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  861  "0  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  862  P(n div k :: int)(n mod k) = (\i j. 0\j & j P i j)"  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  863 apply (rule iffI, clarify)  13260 ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  864  apply (erule_tac P="P ?x ?y" in rev_mp)  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  865  apply (subst zmod_zadd1_eq)  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  866  apply (subst zdiv_zadd1_eq)  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  867  apply (simp add: div_pos_pos_trivial mod_pos_pos_trivial)  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  868 txt{*converse direction*}  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  869 apply (drule_tac x = "n div k" in spec)  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  870 apply (drule_tac x = "n mod k" in spec, simp)  13260 ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  871 done  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  872 ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  873 lemma split_neg_lemma:  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  874  "k<0 ==>  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  875  P(n div k :: int)(n mod k) = (\i j. k0 & n = k*i + j --> P i j)"  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  876 apply (rule iffI, clarify)  13260 ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  877  apply (erule_tac P="P ?x ?y" in rev_mp)  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  878  apply (subst zmod_zadd1_eq)  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  879  apply (subst zdiv_zadd1_eq)  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  880  apply (simp add: div_neg_neg_trivial mod_neg_neg_trivial)  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  881 txt{*converse direction*}  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  882 apply (drule_tac x = "n div k" in spec)  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  883 apply (drule_tac x = "n mod k" in spec, simp)  13260 ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  884 done  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  885 ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  886 lemma split_zdiv:  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  887  "P(n div k :: int) =  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  888  ((k = 0 --> P 0) &  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  889  (0 (\i j. 0\j & j P i)) &  d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  890  (k<0 --> (\i j. k0 & n = k*i + j --> P i)))"  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  891 apply (case_tac "k=0", simp)  13260 ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  892 apply (simp only: linorder_neq_iff)  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  893 apply (erule disjE)  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  894  apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"]  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  895  split_neg_lemma [of concl: "%x y. P x"])  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  896 done  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  897 ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  898 lemma split_zmod:  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  899  "P(n mod k :: int) =  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  900  ((k = 0 --> P n) &  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  901  (0 (\i j. 0\j & j P j)) &  d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  902  (k<0 --> (\i j. k0 & n = k*i + j --> P j)))"  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  903 apply (case_tac "k=0", simp)  13260 ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  904 apply (simp only: linorder_neq_iff)  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  905 apply (erule disjE)  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  906  apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"]  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  907  split_neg_lemma [of concl: "%x y. P y"])  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  908 done  ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  909 ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  910 (* Enable arith to deal with div 2 and mod 2: *)  13266 2a6ad4357d72 modified Larry's changes to make div/mod a numeral work in arith. nipkow parents: 13260 diff changeset  911 declare split_zdiv [of _ _ "number_of k", simplified, standard, arith_split]  2a6ad4357d72 modified Larry's changes to make div/mod a numeral work in arith. nipkow parents: 13260 diff changeset  912 declare split_zmod [of _ _ "number_of k", simplified, standard, arith_split]  13260 ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  913 ea36a40c004f new splitting rules for zdiv, zmod paulson parents: 13183 diff changeset  914 14271 8ed6989228bb Simplification of the development of Integers paulson parents: 13837 diff changeset  915 subsection{*Speeding up the Division Algorithm with Shifting*}  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  916 15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  917 text{*computing div by shifting *}  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  918 14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  919 lemma pos_zdiv_mult_2: "(0::int) \ a ==> (1 + 2*b) div (2*a) = b div a"  d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  920 proof cases  d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  921  assume "a=0"  d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  922  thus ?thesis by simp  d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  923 next  d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  924  assume "a\0" and le_a: "0\a"  d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  925  hence a_pos: "1 \ a" by arith  d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  926  hence one_less_a2: "1 < 2*a" by arith  d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  927  hence le_2a: "2 * (1 + b mod a) \ 2 * a"  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  928  by (simp add: mult_le_cancel_left add_commute [of 1] add1_zle_eq)  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  929  with a_pos have "0 \ b mod a" by simp  d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  930  hence le_addm: "0 \ 1 mod (2*a) + 2*(b mod a)"  d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  931  by (simp add: mod_pos_pos_trivial one_less_a2)  d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  932  with le_2a  d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  933  have "(1 mod (2*a) + 2*(b mod a)) div (2*a) = 0"  d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  934  by (simp add: div_pos_pos_trivial le_addm mod_pos_pos_trivial one_less_a2  d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  935  right_distrib)  d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  936  thus ?thesis  d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  937  by (subst zdiv_zadd1_eq,  d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  938  simp add: zdiv_zmult_zmult1 zmod_zmult_zmult1 one_less_a2  d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  939  div_pos_pos_trivial)  d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  940 qed  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  941 14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  942 lemma neg_zdiv_mult_2: "a \ (0::int) ==> (1 + 2*b) div (2*a) = (b+1) div a"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  943 apply (subgoal_tac " (1 + 2* (-b - 1)) div (2 * (-a)) = (-b - 1) div (-a) ")  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  944 apply (rule_tac [2] pos_zdiv_mult_2)  14479 0eca4aabf371 streamlined treatment of quotients for the integers paulson parents: 14473 diff changeset  945 apply (auto simp add: minus_mult_right [symmetric] right_diff_distrib)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  946 apply (subgoal_tac " (-1 - (2 * b)) = - (1 + (2 * b))")  14479 0eca4aabf371 streamlined treatment of quotients for the integers paulson parents: 14473 diff changeset  947 apply (simp only: zdiv_zminus_zminus diff_minus minus_add_distrib [symmetric],  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  948  simp)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  949 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  950 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  951 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  952 (*Not clear why this must be proved separately; probably number_of causes  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  953  simplification problems*)  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  954 lemma not_0_le_lemma: "~ 0 \ x ==> x \ (0::int)"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  955 by auto  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  956 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  957 lemma zdiv_number_of_BIT[simp]:  15620 8ccdc8bc66a2 replaced bool by a new datatype "bit" for binary numerals paulson parents: 15320 diff changeset  958  "number_of (v BIT b) div number_of (w BIT bit.B0) =  8ccdc8bc66a2 replaced bool by a new datatype "bit" for binary numerals paulson parents: 15320 diff changeset  959  (if b=bit.B0 | (0::int) \ number_of w  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  960  then number_of v div (number_of w)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  961  else (number_of v + (1::int)) div (number_of w))"  20485 3078fd2eec7b got rid of Numeral.bin type haftmann parents: 18984 diff changeset  962 apply (simp only: number_of_eq numeral_simps UNIV_I split: split_if)  15620 8ccdc8bc66a2 replaced bool by a new datatype "bit" for binary numerals paulson parents: 15320 diff changeset  963 apply (simp add: zdiv_zmult_zmult1 pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac  8ccdc8bc66a2 replaced bool by a new datatype "bit" for binary numerals paulson parents: 15320 diff changeset  964  split: bit.split)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  965 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  966 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  967 15013 34264f5e4691 new treatment of binary numerals paulson parents: 15003 diff changeset  968 subsection{*Computing mod by Shifting (proofs resemble those for div)*}  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  969 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  970 lemma pos_zmod_mult_2:  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  971  "(0::int) \ a ==> (1 + 2*b) mod (2*a) = 1 + 2 * (b mod a)"  15013 34264f5e4691 new treatment of binary numerals paulson parents: 15003 diff changeset  972 apply (case_tac "a = 0", simp)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  973 apply (subgoal_tac "1 < a * 2")  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  974  prefer 2 apply arith  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  975 apply (subgoal_tac "2* (1 + b mod a) \ 2*a")  14387 e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses paulson parents: 14378 diff changeset  976  apply (rule_tac [2] mult_left_mono)  15234 ec91a90c604e simplification tweaks for better arithmetic reasoning paulson parents: 15221 diff changeset  977 apply (auto simp add: add_commute [of 1] mult_commute add1_zle_eq  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  978  pos_mod_bound)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  979 apply (subst zmod_zadd1_eq)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  980 apply (simp add: zmod_zmult_zmult2 mod_pos_pos_trivial)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  981 apply (rule mod_pos_pos_trivial)  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  982 apply (auto simp add: mod_pos_pos_trivial left_distrib)  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  983 apply (subgoal_tac "0 \ b mod a", arith, simp)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  984 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  985 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  986 lemma neg_zmod_mult_2:  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  987  "a \ (0::int) ==> (1 + 2*b) mod (2*a) = 2 * ((b+1) mod a) - 1"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  988 apply (subgoal_tac "(1 + 2* (-b - 1)) mod (2* (-a)) =  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  989  1 + 2* ((-b - 1) mod (-a))")  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  990 apply (rule_tac [2] pos_zmod_mult_2)  14479 0eca4aabf371 streamlined treatment of quotients for the integers paulson parents: 14473 diff changeset  991 apply (auto simp add: minus_mult_right [symmetric] right_diff_distrib)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  992 apply (subgoal_tac " (-1 - (2 * b)) = - (1 + (2 * b))")  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  993  prefer 2 apply simp  14479 0eca4aabf371 streamlined treatment of quotients for the integers paulson parents: 14473 diff changeset  994 apply (simp only: zmod_zminus_zminus diff_minus minus_add_distrib [symmetric])  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  995 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  996 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  997 lemma zmod_number_of_BIT [simp]:  15620 8ccdc8bc66a2 replaced bool by a new datatype "bit" for binary numerals paulson parents: 15320 diff changeset  998  "number_of (v BIT b) mod number_of (w BIT bit.B0) =  8ccdc8bc66a2 replaced bool by a new datatype "bit" for binary numerals paulson parents: 15320 diff changeset  999  (case b of  8ccdc8bc66a2 replaced bool by a new datatype "bit" for binary numerals paulson parents: 15320 diff changeset  1000  bit.B0 => 2 * (number_of v mod number_of w)  8ccdc8bc66a2 replaced bool by a new datatype "bit" for binary numerals paulson parents: 15320 diff changeset  1001  | bit.B1 => if (0::int) \ number_of w  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1002  then 2 * (number_of v mod number_of w) + 1  15620 8ccdc8bc66a2 replaced bool by a new datatype "bit" for binary numerals paulson parents: 15320 diff changeset  1003  else 2 * ((number_of v + (1::int)) mod number_of w) - 1)"  20485 3078fd2eec7b got rid of Numeral.bin type haftmann parents: 18984 diff changeset  1004 apply (simp only: number_of_eq numeral_simps UNIV_I split: bit.split)  15013 34264f5e4691 new treatment of binary numerals paulson parents: 15003 diff changeset  1005 apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2  34264f5e4691 new treatment of binary numerals paulson parents: 15003 diff changeset  1006  not_0_le_lemma neg_zmod_mult_2 add_ac)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1007 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1008 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1009 15013 34264f5e4691 new treatment of binary numerals paulson parents: 15003 diff changeset  1010 subsection{*Quotients of Signs*}  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1011 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1012 lemma div_neg_pos_less0: "[| a < (0::int); 0 < b |] ==> a div b < 0"  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  1013 apply (subgoal_tac "a div b \ -1", force)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1014 apply (rule order_trans)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1015 apply (rule_tac a' = "-1" in zdiv_mono1)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1016 apply (auto simp add: zdiv_minus1)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1017 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1018 14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  1019 lemma div_nonneg_neg_le0: "[| (0::int) \ a; b < 0 |] ==> a div b \ 0"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1020 by (drule zdiv_mono1_neg, auto)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1021 14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  1022 lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \ a div b) = (0 \ a)"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1023 apply auto  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1024 apply (drule_tac [2] zdiv_mono1)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1025 apply (auto simp add: linorder_neq_iff)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1026 apply (simp (no_asm_use) add: linorder_not_less [symmetric])  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1027 apply (blast intro: div_neg_pos_less0)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1028 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1029 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1030 lemma neg_imp_zdiv_nonneg_iff:  14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  1031  "b < (0::int) ==> (0 \ a div b) = (a \ (0::int))"  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1032 apply (subst zdiv_zminus_zminus [symmetric])  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1033 apply (subst pos_imp_zdiv_nonneg_iff, auto)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1034 done  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1035 14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  1036 (*But not (a div b \ 0 iff a\0); consider a=1, b=2 when a div b = 0.*)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1037 lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1038 by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1039 14288 d149e3cbdb39 Moving some theorems from Real/RealArith0.ML paulson parents: 14271 diff changeset  1040 (*Again the law fails for \: consider a = -1, b = -2 when a div b = 0*)  13183 c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1041 lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)"  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1042 by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)  c7290200b3f4 conversion of IntDiv.thy to Isar format paulson parents: 11868 diff changeset  1043 13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1044 14271 8ed6989228bb Simplification of the development of Integers paulson parents: 13837 diff changeset  1045 subsection {* The Divides Relation *}  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1046 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1047 lemma zdvd_iff_zmod_eq_0: "(m dvd n) = (n mod m = (0::int))"  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1048 by(simp add:dvd_def zmod_eq_0_iff)  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1049 18984 4301eb0f051f names for simprules paulson parents: 18978 diff changeset  1050 lemmas zdvd_iff_zmod_eq_0_number_of =  4301eb0f051f names for simprules paulson parents: 18978 diff changeset  1051  zdvd_iff_zmod_eq_0 [of "number_of x" "number_of y", standard]  4301eb0f051f names for simprules paulson parents: 18978 diff changeset  1052 4301eb0f051f names for simprules paulson parents: 18978 diff changeset  1053 declare zdvd_iff_zmod_eq_0_number_of [simp]  18978 8971c306b94f made "dvd" on numbers executable by simp. nipkow parents: 18648 diff changeset  1054 13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1055 lemma zdvd_0_right [iff]: "(m::int) dvd 0"  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  1056 by (simp add: dvd_def)  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1057 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1058 lemma zdvd_0_left [iff]: "(0 dvd (m::int)) = (m = 0)"  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  1059  by (simp add: dvd_def)  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1060 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1061 lemma zdvd_1_left [iff]: "1 dvd (m::int)"  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  1062  by (simp add: dvd_def)  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1063 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1064 lemma zdvd_refl [simp]: "m dvd (m::int)"  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  1065 by (auto simp add: dvd_def intro: zmult_1_right [symmetric])  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1066 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1067 lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)"  15234 ec91a90c604e simplification tweaks for better arithmetic reasoning paulson parents: 15221 diff changeset  1068 by (auto simp add: dvd_def intro: mult_assoc)  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1069 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1070 lemma zdvd_zminus_iff: "(m dvd -n) = (m dvd (n::int))"  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  1071  apply (simp add: dvd_def, auto)  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1072  apply (rule_tac [!] x = "-k" in exI, auto)  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1073  done  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1074 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1075 lemma zdvd_zminus2_iff: "(-m dvd n) = (m dvd (n::int))"  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  1076  apply (simp add: dvd_def, auto)  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1077  apply (rule_tac [!] x = "-k" in exI, auto)  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1078  done  22026 cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1079 lemma zdvd_abs1: "( \i::int\ dvd j) = (i dvd j)"  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1080  apply (cases "i > 0", simp)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1081  apply (simp add: dvd_def)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1082  apply (rule iffI)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1083  apply (erule exE)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1084  apply (rule_tac x="- k" in exI, simp)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1085  apply (erule exE)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1086  apply (rule_tac x="- k" in exI, simp)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1087  done  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1088 lemma zdvd_abs2: "( (i::int) dvd \j\) = (i dvd j)"  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1089  apply (cases "j > 0", simp)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1090  apply (simp add: dvd_def)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1091  apply (rule iffI)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1092  apply (erule exE)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1093  apply (rule_tac x="- k" in exI, simp)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1094  apply (erule exE)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1095  apply (rule_tac x="- k" in exI, simp)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1096  done  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1097 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1098 lemma zdvd_anti_sym:  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1099  "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  1100  apply (simp add: dvd_def, auto)  15234 ec91a90c604e simplification tweaks for better arithmetic reasoning paulson parents: 15221 diff changeset  1101  apply (simp add: mult_assoc zero_less_mult_iff zmult_eq_1_iff)  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1102  done  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1103 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1104 lemma zdvd_zadd: "k dvd m ==> k dvd n ==> k dvd (m + n :: int)"  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  1105  apply (simp add: dvd_def)  14479 0eca4aabf371 streamlined treatment of quotients for the integers paulson parents: 14473 diff changeset  1106  apply (blast intro: right_distrib [symmetric])  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1107  done  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1108 22026 cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1109 lemma zdvd_dvd_eq: assumes anz:"a \ 0" and ab: "(a::int) dvd b" and ba:"b dvd a"  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1110  shows "\a\ = \b\"  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1111 proof-  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1112  from ab obtain k where k:"b = a*k" unfolding dvd_def by blast  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1113  from ba obtain k' where k':"a = b*k'" unfolding dvd_def by blast  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1114  from k k' have "a = a*k*k'" by simp  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1115  with mult_cancel_left1[where c="a" and b="k*k'"]  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1116  have kk':"k*k' = 1" using anz by (simp add: mult_assoc)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1117  hence "k = 1 \ k' = 1 \ k = -1 \ k' = -1" by (simp add: zmult_eq_1_iff)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1118  thus ?thesis using k k' by auto  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1119 qed  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1120 13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1121 lemma zdvd_zdiff: "k dvd m ==> k dvd n ==> k dvd (m - n :: int)"  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  1122  apply (simp add: dvd_def)  14479 0eca4aabf371 streamlined treatment of quotients for the integers paulson parents: 14473 diff changeset  1123  apply (blast intro: right_diff_distrib [symmetric])  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1124  done  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1125 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1126 lemma zdvd_zdiffD: "k dvd m - n ==> k dvd n ==> k dvd (m::int)"  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1127  apply (subgoal_tac "m = n + (m - n)")  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1128  apply (erule ssubst)  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1129  apply (blast intro: zdvd_zadd, simp)  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1130  done  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1131 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1132 lemma zdvd_zmult: "k dvd (n::int) ==> k dvd m * n"  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  1133  apply (simp add: dvd_def)  14271 8ed6989228bb Simplification of the development of Integers paulson parents: 13837 diff changeset  1134  apply (blast intro: mult_left_commute)  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1135  done  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1136 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1137 lemma zdvd_zmult2: "k dvd (m::int) ==> k dvd m * n"  15234 ec91a90c604e simplification tweaks for better arithmetic reasoning paulson parents: 15221 diff changeset  1138  apply (subst mult_commute)  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1139  apply (erule zdvd_zmult)  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1140  done  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1141 17084 fb0a80aef0be classical rules must have names for ATP integration paulson parents: 16733 diff changeset  1142 lemma zdvd_triv_right [iff]: "(k::int) dvd m * k"  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1143  apply (rule zdvd_zmult)  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1144  apply (rule zdvd_refl)  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1145  done  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1146 17084 fb0a80aef0be classical rules must have names for ATP integration paulson parents: 16733 diff changeset  1147 lemma zdvd_triv_left [iff]: "(k::int) dvd k * m"  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1148  apply (rule zdvd_zmult2)  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1149  apply (rule zdvd_refl)  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1150  done  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1151 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1152 lemma zdvd_zmultD2: "j * k dvd n ==> j dvd (n::int)"  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  1153  apply (simp add: dvd_def)  15234 ec91a90c604e simplification tweaks for better arithmetic reasoning paulson parents: 15221 diff changeset  1154  apply (simp add: mult_assoc, blast)  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1155  done  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1156 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1157 lemma zdvd_zmultD: "j * k dvd n ==> k dvd (n::int)"  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1158  apply (rule zdvd_zmultD2)  15234 ec91a90c604e simplification tweaks for better arithmetic reasoning paulson parents: 15221 diff changeset  1159  apply (subst mult_commute, assumption)  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1160  done  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1161 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1162 lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n"  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  1163  apply (simp add: dvd_def, clarify)  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1164  apply (rule_tac x = "k * ka" in exI)  14271 8ed6989228bb Simplification of the development of Integers paulson parents: 13837 diff changeset  1165  apply (simp add: mult_ac)  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1166  done  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1167 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1168 lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))"  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1169  apply (rule iffI)  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1170  apply (erule_tac [2] zdvd_zadd)  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1171  apply (subgoal_tac "n = (n + k * m) - k * m")  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1172  apply (erule ssubst)  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1173  apply (erule zdvd_zdiff, simp_all)  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1174  done  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1175 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1176 lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  1177  apply (simp add: dvd_def)  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1178  apply (auto simp add: zmod_zmult_zmult1)  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1179  done  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1180 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1181 lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1182  apply (subgoal_tac "k dvd n * (m div n) + m mod n")  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1183  apply (simp add: zmod_zdiv_equality [symmetric])  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1184  apply (simp only: zdvd_zadd zdvd_zmult2)  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1185  done  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1186 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1187 lemma zdvd_not_zless: "0 < m ==> m < n ==> \ n dvd (m::int)"  15221 8412cfdf3287 tweaking of arithmetic proofs paulson parents: 15140 diff changeset  1188  apply (simp add: dvd_def, auto)  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1189  apply (subgoal_tac "0 < n")  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1190  prefer 2  14378 69c4d5997669 generic of_nat and of_int functions, and generalization of iszero paulson parents: 14353 diff changeset  1191  apply (blast intro: order_less_trans)  14353 79f9fbef9106 Added lemmas to Ring_and_Field with slightly modified simplification rules paulson parents: 14288 diff changeset  1192  apply (simp add: zero_less_mult_iff)  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1193  apply (subgoal_tac "n * k < n * 1")  14387 e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses paulson parents: 14378 diff changeset  1194  apply (drule mult_less_cancel_left [THEN iffD1], auto)  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1195  done  22026 cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1196 lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1197  using zmod_zdiv_equality[where a="m" and b="n"]  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1198  by (simp add: ring_eq_simps)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1199 cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1200 lemma zdvd_mult_div_cancel:"(n::int) dvd m \ n * (m div n) = m"  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1201 apply (subgoal_tac "m mod n = 0")  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1202  apply (simp add: zmult_div_cancel)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1203 apply (simp only: zdvd_iff_zmod_eq_0)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1204 done  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1205 cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1206 lemma zdvd_mult_cancel: assumes d:"k * m dvd k * n" and kz:"k \ (0::int)"  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1207  shows "m dvd n"  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1208 proof-  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1209  from d obtain h where h: "k*n = k*m * h" unfolding dvd_def by blast  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1210  {assume "n \ m*h" hence "k* n \ k* (m*h)" using kz by simp  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1211  with h have False by (simp add: mult_assoc)}  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1212  hence "n = m * h" by blast  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1213  thus ?thesis by blast  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1214 qed  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1215 cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1216 theorem ex_nat: "(\x::nat. P x) = (\x::int. 0 <= x \ P (nat x))"  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1217  apply (simp split add: split_nat)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1218  apply (rule iffI)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1219  apply (erule exE)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1220  apply (rule_tac x = "int x" in exI)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1221  apply simp  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1222  apply (erule exE)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1223  apply (rule_tac x = "nat x" in exI)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1224  apply (erule conjE)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1225  apply (erule_tac x = "nat x" in allE)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1226  apply simp  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1227  done  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1228 cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1229 theorem zdvd_int: "(x dvd y) = (int x dvd int y)"  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1230  apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1231  nat_0_le cong add: conj_cong)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1232  apply (rule iffI)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1233  apply iprover  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1234  apply (erule exE)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1235  apply (case_tac "x=0")  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1236  apply (rule_tac x=0 in exI)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1237  apply simp  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1238  apply (case_tac "0 \ k")  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1239  apply iprover  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1240  apply (simp add: linorder_not_le)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1241  apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1242  apply assumption  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1243  apply (simp add: mult_ac)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1244  done  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1245 22091 d13ad9a479f9 Theorem "(x::int) dvd 1 = ( ¦x¦ = 1)" added to default simpset. chaieb parents: 22026 diff changeset  1246 lemma zdvd1_eq[simp]: "(x::int) dvd 1 = ( \x\ = 1)"  22026 cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1247 proof  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1248  assume d: "x dvd 1" hence "int (nat \x\) dvd int (nat 1)" by (simp add: zdvd_abs1)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1249  hence "nat \x\ dvd 1" by (simp add: zdvd_int)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1250  hence "nat \x\ = 1" by simp  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1251  thus "\x\ = 1" by (cases "x < 0", auto)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1252 next  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1253  assume "\x\=1" thus "x dvd 1"  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1254  by(cases "x < 0",simp_all add: minus_equation_iff zdvd_iff_zmod_eq_0)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1255 qed  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1256 lemma zdvd_mult_cancel1:  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1257  assumes mp:"m \(0::int)" shows "(m * n dvd m) = (\n\ = 1)"  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1258 proof  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1259  assume n1: "\n\ = 1" thus "m * n dvd m"  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1260  by (cases "n >0", auto simp add: zdvd_zminus2_iff minus_equation_iff)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1261 next  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1262  assume H: "m * n dvd m" hence H2: "m * n dvd m * 1" by simp  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1263  from zdvd_mult_cancel[OF H2 mp] show "\n\ = 1" by (simp only: zdvd1_eq)  cc60e54aa7cb A few theorems on integer divisibily. chaieb parents: 21409 diff changeset  1264 qed  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1265 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1266 lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1267  apply (auto simp add: dvd_def nat_abs_mult_distrib)  14353 79f9fbef9106 Added lemmas to Ring_and_Field with slightly modified simplification rules paulson parents: 14288 diff changeset  1268  apply (auto simp add: nat_eq_iff abs_if split add: split_if_asm)  79f9fbef9106 Added lemmas to Ring_and_Field with slightly modified simplification rules paulson parents: 14288 diff changeset  1269  apply (rule_tac x = "-(int k)" in exI)  16413 47ffc49c7d7b a few new integer lemmas paulson parents: 15620 diff changeset  1270  apply (auto simp add: int_mult)  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1271  done  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1272 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1273 lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"  16413 47ffc49c7d7b a few new integer lemmas paulson parents: 15620 diff changeset  1274  apply (auto simp add: dvd_def abs_if int_mult)  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1275  apply (rule_tac [3] x = "nat k" in exI)  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1276  apply (rule_tac [2] x = "-(int k)" in exI)  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1277  apply (rule_tac x = "nat (-k)" in exI)  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1278  apply (cut_tac [3] k = m in int_less_0_conv)  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1279  apply (cut_tac k = m in int_less_0_conv)  14353 79f9fbef9106 Added lemmas to Ring_and_Field with slightly modified simplification rules paulson parents: 14288 diff changeset  1280  apply (auto simp add: zero_le_mult_iff mult_less_0_iff  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1281  nat_mult_distrib [symmetric] nat_eq_iff2)  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1282  done  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1283 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1284 lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \ z then (z dvd int m) else m = 0)"  16413 47ffc49c7d7b a few new integer lemmas paulson parents: 15620 diff changeset  1285  apply (auto simp add: dvd_def int_mult)  13837 8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1286  apply (rule_tac x = "nat k" in exI)  8dd150d36c65 Reorganized, moving many results about the integer dvd relation from IntPrimes paulson parents: 13788 diff changeset  1287  apply (cut_tac k = m in int_less_0_conv)  14353 79f9fbef9106 Added lemmas to Ring_and_Field with slightly modified simplification rules paulson parents: 14288 diff changeset