author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 10195  325b6279ae4f 
child 10559  d3fd54fc659b 
permissions  rwrr 
3366  1 
(* Title: HOL/Divides.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1993 University of Cambridge 

5 

6 
The division operators div, mod and the divides relation "dvd" 

7 
*) 

8 

9 

10 
(** Lessthen properties **) 

11 

9108  12 
bind_thm ("wf_less_trans", [eq_reflection, wf_pred_nat RS wf_trancl] MRS 
13 
def_wfrec RS trans); 

3366  14 

5069  15 
Goal "(%m. m mod n) = wfrec (trancl pred_nat) \ 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

16 
\ (%f j. if j<n  n=0 then j else f (jn))"; 
4089  17 
by (simp_tac (simpset() addsimps [mod_def]) 1); 
3366  18 
qed "mod_eq"; 
19 

7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

20 
Goal "(%m. m div n) = wfrec (trancl pred_nat) \ 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

21 
\ (%f j. if j<n  n=0 then 0 else Suc (f (jn)))"; 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

22 
by (simp_tac (simpset() addsimps [div_def]) 1); 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

23 
qed "div_eq"; 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

24 

08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

25 

08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

26 
(** Aribtrary definitions for division by zero. Useful to simplify 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

27 
certain equations **) 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

28 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

29 
Goal "a div 0 = (0::nat)"; 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

30 
by (rtac (div_eq RS wf_less_trans) 1); 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

31 
by (Asm_simp_tac 1); 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

32 
qed "DIVISION_BY_ZERO_DIV"; (*NOT for adding to default simpset*) 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

33 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

34 
Goal "a mod 0 = (a::nat)"; 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

35 
by (rtac (mod_eq RS wf_less_trans) 1); 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

36 
by (Asm_simp_tac 1); 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

37 
qed "DIVISION_BY_ZERO_MOD"; (*NOT for adding to default simpset*) 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

38 

08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

39 
fun div_undefined_case_tac s i = 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

40 
case_tac s i THEN 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

41 
Full_simp_tac (i+1) THEN 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

42 
asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO_DIV, 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

43 
DIVISION_BY_ZERO_MOD]) i; 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

44 

08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

45 
(*** Remainder ***) 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

46 

6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset

47 
Goal "m<n ==> m mod n = (m::nat)"; 
3366  48 
by (rtac (mod_eq RS wf_less_trans) 1); 
49 
by (Asm_simp_tac 1); 

50 
qed "mod_less"; 

8393  51 
Addsimps [mod_less]; 
3366  52 

7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

53 
Goal "~ m < (n::nat) ==> m mod n = (mn) mod n"; 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

54 
by (div_undefined_case_tac "n=0" 1); 
3366  55 
by (rtac (mod_eq RS wf_less_trans) 1); 
4089  56 
by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1); 
3366  57 
qed "mod_geq"; 
58 

5415  59 
(*Avoids the ugly ~m<n above*) 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

60 
Goal "(n::nat) <= m ==> m mod n = (mn) mod n"; 
5415  61 
by (asm_simp_tac (simpset() addsimps [mod_geq, not_less_iff_le]) 1); 
62 
qed "le_mod_geq"; 

63 

7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

64 
Goal "m mod (n::nat) = (if m<n then m else (mn) mod n)"; 
8393  65 
by (asm_simp_tac (simpset() addsimps [mod_geq]) 1); 
4774  66 
qed "mod_if"; 
67 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

68 
Goal "m mod 1 = (0::nat)"; 
3366  69 
by (induct_tac "m" 1); 
8393  70 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_geq]))); 
3366  71 
qed "mod_1"; 
72 
Addsimps [mod_1]; 

73 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

74 
Goal "n mod n = (0::nat)"; 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

75 
by (div_undefined_case_tac "n=0" 1); 
8393  76 
by (asm_simp_tac (simpset() addsimps [mod_geq]) 1); 
3366  77 
qed "mod_self"; 
78 

7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

79 
Goal "(m+n) mod n = m mod (n::nat)"; 
3366  80 
by (subgoal_tac "(n + m) mod n = (n+mn) mod n" 1); 
81 
by (stac (mod_geq RS sym) 2); 

4089  82 
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute]))); 
4811  83 
qed "mod_add_self2"; 
4810  84 

7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

85 
Goal "(n+m) mod n = m mod (n::nat)"; 
4811  86 
by (asm_simp_tac (simpset() addsimps [add_commute, mod_add_self2]) 1); 
87 
qed "mod_add_self1"; 

4810  88 

8783  89 
Addsimps [mod_add_self1, mod_add_self2]; 
90 

7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

91 
Goal "(m + k*n) mod n = m mod (n::nat)"; 
4810  92 
by (induct_tac "k" 1); 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

93 
by (ALLGOALS 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

94 
(asm_simp_tac 
8783  95 
(simpset() addsimps [read_instantiate [("y","n")] add_left_commute]))); 
4811  96 
qed "mod_mult_self1"; 
4810  97 

7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

98 
Goal "(m + n*k) mod n = m mod (n::nat)"; 
4811  99 
by (asm_simp_tac (simpset() addsimps [mult_commute, mod_mult_self1]) 1); 
100 
qed "mod_mult_self2"; 

4810  101 

4811  102 
Addsimps [mod_mult_self1, mod_mult_self2]; 
3366  103 

7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

104 
Goal "(m mod n) * (k::nat) = (m*k) mod (n*k)"; 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

105 
by (div_undefined_case_tac "n=0" 1); 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

106 
by (div_undefined_case_tac "k=0" 1); 
9870  107 
by (induct_thm_tac nat_less_induct "m" 1); 
4774  108 
by (stac mod_if 1); 
109 
by (Asm_simp_tac 1); 

8393  110 
by (asm_simp_tac (simpset() addsimps [mod_geq, 
4774  111 
diff_less, diff_mult_distrib]) 1); 
3366  112 
qed "mod_mult_distrib"; 
113 

7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

114 
Goal "(k::nat) * (m mod n) = (k*m) mod (k*n)"; 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

115 
by (asm_simp_tac 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

116 
(simpset() addsimps [read_instantiate [("m","k")] mult_commute, 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

117 
mod_mult_distrib]) 1); 
3366  118 
qed "mod_mult_distrib2"; 
119 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

120 
Goal "(m*n) mod n = (0::nat)"; 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

121 
by (div_undefined_case_tac "n=0" 1); 
3366  122 
by (induct_tac "m" 1); 
8393  123 
by (Asm_simp_tac 1); 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

124 
by (rename_tac "k" 1); 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

125 
by (cut_inst_tac [("m","k*n"),("n","n")] mod_add_self2 1); 
4089  126 
by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1); 
3366  127 
qed "mod_mult_self_is_0"; 
7082  128 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

129 
Goal "(n*m) mod n = (0::nat)"; 
7082  130 
by (simp_tac (simpset() addsimps [mult_commute, mod_mult_self_is_0]) 1); 
131 
qed "mod_mult_self1_is_0"; 

132 
Addsimps [mod_mult_self_is_0, mod_mult_self1_is_0]; 

3366  133 

7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

134 

3366  135 
(*** Quotient ***) 
136 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

137 
Goal "m<n ==> m div n = (0::nat)"; 
3366  138 
by (rtac (div_eq RS wf_less_trans) 1); 
139 
by (Asm_simp_tac 1); 

140 
qed "div_less"; 

8393  141 
Addsimps [div_less]; 
3366  142 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

143 
Goal "[ 0<n; ~m<n ] ==> m div n = Suc((mn) div n)"; 
3366  144 
by (rtac (div_eq RS wf_less_trans) 1); 
4089  145 
by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1); 
3366  146 
qed "div_geq"; 
147 

5415  148 
(*Avoids the ugly ~m<n above*) 
149 
Goal "[ 0<n; n<=m ] ==> m div n = Suc((mn) div n)"; 

150 
by (asm_simp_tac (simpset() addsimps [div_geq, not_less_iff_le]) 1); 

151 
qed "le_div_geq"; 

152 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

153 
Goal "0<n ==> m div n = (if m<n then 0 else Suc((mn) div n))"; 
8393  154 
by (asm_simp_tac (simpset() addsimps [div_geq]) 1); 
4774  155 
qed "div_if"; 
156 

7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

157 

3366  158 
(*Main Result about quotient and remainder.*) 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

159 
Goal "(m div n)*n + m mod n = (m::nat)"; 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

160 
by (div_undefined_case_tac "n=0" 1); 
9870  161 
by (induct_thm_tac nat_less_induct "m" 1); 
4774  162 
by (stac mod_if 1); 
163 
by (ALLGOALS (asm_simp_tac 

8393  164 
(simpset() addsimps [add_assoc, div_geq, 
5537  165 
add_diff_inverse, diff_less]))); 
3366  166 
qed "mod_div_equality"; 
167 

4358  168 
(* a simple rearrangement of mod_div_equality: *) 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

169 
Goal "(n::nat) * (m div n) = m  (m mod n)"; 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

170 
by (cut_inst_tac [("m","m"),("n","n")] mod_div_equality 1); 
9912  171 
by (full_simp_tac (simpset() addsimps mult_ac) 1); 
172 
by (arith_tac 1); 

4358  173 
qed "mult_div_cancel"; 
174 

5069  175 
Goal "m div 1 = m"; 
3366  176 
by (induct_tac "m" 1); 
8393  177 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [div_geq]))); 
3366  178 
qed "div_1"; 
179 
Addsimps [div_1]; 

180 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

181 
Goal "0<n ==> n div n = (1::nat)"; 
8393  182 
by (asm_simp_tac (simpset() addsimps [div_geq]) 1); 
3366  183 
qed "div_self"; 
184 

4811  185 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

186 
Goal "0<n ==> (m+n) div n = Suc (m div n)"; 
4811  187 
by (subgoal_tac "(n + m) div n = Suc ((n+mn) div n)" 1); 
188 
by (stac (div_geq RS sym) 2); 

189 
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute]))); 

190 
qed "div_add_self2"; 

191 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

192 
Goal "0<n ==> (n+m) div n = Suc (m div n)"; 
4811  193 
by (asm_simp_tac (simpset() addsimps [add_commute, div_add_self2]) 1); 
194 
qed "div_add_self1"; 

195 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

196 
Goal "!!n::nat. 0<n ==> (m + k*n) div n = k + m div n"; 
4811  197 
by (induct_tac "k" 1); 
5537  198 
by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac @ [div_add_self1]))); 
4811  199 
qed "div_mult_self1"; 
200 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

201 
Goal "0<n ==> (m + n*k) div n = k + m div (n::nat)"; 
4811  202 
by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self1]) 1); 
203 
qed "div_mult_self2"; 

204 

205 
Addsimps [div_mult_self1, div_mult_self2]; 

206 

7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

207 
(** A dividend of zero **) 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

208 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

209 
Goal "0 div m = (0::nat)"; 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

210 
by (div_undefined_case_tac "m=0" 1); 
8393  211 
by (Asm_simp_tac 1); 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

212 
qed "div_0"; 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

213 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

214 
Goal "0 mod m = (0::nat)"; 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

215 
by (div_undefined_case_tac "m=0" 1); 
8393  216 
by (Asm_simp_tac 1); 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

217 
qed "mod_0"; 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

218 
Addsimps [div_0, mod_0]; 
4811  219 

3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

220 
(* Monotonicity of div in first argument *) 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

221 
Goal "ALL m::nat. m <= n > (m div k) <= (n div k)"; 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

222 
by (div_undefined_case_tac "k=0" 1); 
9870  223 
by (induct_thm_tac nat_less_induct "n" 1); 
3718  224 
by (Clarify_tac 1); 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

225 
by (case_tac "n<k" 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

226 
(* 1 case n<k *) 
8393  227 
by (Asm_simp_tac 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

228 
(* 2 case n >= k *) 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

229 
by (case_tac "m<k" 1); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

230 
(* 2.1 case m<k *) 
8393  231 
by (Asm_simp_tac 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

232 
(* 2.2 case m>=k *) 
4089  233 
by (asm_simp_tac (simpset() addsimps [div_geq, diff_less, diff_le_mono]) 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

234 
qed_spec_mp "div_le_mono"; 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

235 

1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

236 
(* Antimonotonicity of div in second argument *) 
8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

237 
Goal "!!m::nat. [ 0<m; m<=n ] ==> (k div n) <= (k div m)"; 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

238 
by (subgoal_tac "0<n" 1); 
6073  239 
by (Asm_simp_tac 2); 
9870  240 
by (induct_thm_tac nat_less_induct "k" 1); 
3496  241 
by (rename_tac "k" 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

242 
by (case_tac "k<n" 1); 
8393  243 
by (Asm_simp_tac 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

244 
by (subgoal_tac "~(k<m)" 1); 
6073  245 
by (Asm_simp_tac 2); 
4089  246 
by (asm_simp_tac (simpset() addsimps [div_geq]) 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

247 
by (subgoal_tac "(kn) div n <= (km) div n" 1); 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

248 
by (REPEAT (ares_tac [div_le_mono,diff_le_mono2] 2)); 
5318  249 
by (rtac le_trans 1); 
5316  250 
by (Asm_simp_tac 1); 
251 
by (asm_simp_tac (simpset() addsimps [diff_less]) 1); 

3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

252 
qed "div_le_mono2"; 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

253 

7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

254 
Goal "m div n <= (m::nat)"; 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

255 
by (div_undefined_case_tac "n=0" 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

256 
by (subgoal_tac "m div n <= m div 1" 1); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

257 
by (Asm_full_simp_tac 1); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

258 
by (rtac div_le_mono2 1); 
6073  259 
by (ALLGOALS Asm_simp_tac); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

260 
qed "div_le_dividend"; 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

261 
Addsimps [div_le_dividend]; 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

262 

1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

263 
(* Similar for "less than" *) 
8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

264 
Goal "!!n::nat. 1<n ==> (0 < m) > (m div n < m)"; 
9870  265 
by (induct_thm_tac nat_less_induct "m" 1); 
3496  266 
by (rename_tac "m" 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

267 
by (case_tac "m<n" 1); 
8393  268 
by (Asm_full_simp_tac 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

269 
by (subgoal_tac "0<n" 1); 
6073  270 
by (Asm_simp_tac 2); 
4089  271 
by (asm_full_simp_tac (simpset() addsimps [div_geq]) 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

272 
by (case_tac "n<m" 1); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

273 
by (subgoal_tac "(mn) div n < (mn)" 1); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

274 
by (REPEAT (ares_tac [impI,less_trans_Suc] 1)); 
4089  275 
by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1); 
276 
by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1); 

3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

277 
(* case n=m *) 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

278 
by (subgoal_tac "m=n" 1); 
6073  279 
by (Asm_simp_tac 2); 
8393  280 
by (Asm_simp_tac 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

281 
qed_spec_mp "div_less_dividend"; 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

282 
Addsimps [div_less_dividend]; 
3366  283 

284 
(*** Further facts about mod (mainly for the mutilated chess board ***) 

285 

5278  286 
Goal "0<n ==> Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"; 
9870  287 
by (induct_thm_tac nat_less_induct "m" 1); 
8860  288 
by (case_tac "Suc(na)<n" 1); 
3366  289 
(* case Suc(na) < n *) 
8860  290 
by (forward_tac [lessI RS less_trans] 1 
291 
THEN asm_simp_tac (simpset() addsimps [less_not_refl3]) 1); 

3366  292 
(* case n <= Suc(na) *) 
5415  293 
by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, le_Suc_eq, 
294 
mod_geq]) 1); 

8860  295 
by (auto_tac (claset(), 
296 
simpset() addsimps [Suc_diff_le, diff_less, le_mod_geq])); 

3366  297 
qed "mod_Suc"; 
298 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

299 
Goal "0<n ==> m mod n < (n::nat)"; 
9870  300 
by (induct_thm_tac nat_less_induct "m" 1); 
5498  301 
by (case_tac "na<n" 1); 
302 
(*case n le na*) 

303 
by (asm_full_simp_tac (simpset() addsimps [mod_geq, diff_less]) 2); 

3366  304 
(*case na<n*) 
8393  305 
by (Asm_simp_tac 1); 
3366  306 
qed "mod_less_divisor"; 
8698  307 
Addsimps [mod_less_divisor]; 
3366  308 

309 
(*** More division laws ***) 

310 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

311 
Goal "0<n ==> (m*n) div n = (m::nat)"; 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

312 
by (cut_inst_tac [("m", "m*n"),("n","n")] mod_div_equality 1); 
9912  313 
by Auto_tac; 
3366  314 
qed "div_mult_self_is_m"; 
7082  315 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

316 
Goal "0<n ==> (n*m) div n = (m::nat)"; 
7082  317 
by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self_is_m]) 1); 
318 
qed "div_mult_self1_is_m"; 

319 
Addsimps [div_mult_self_is_m, div_mult_self1_is_m]; 

3366  320 

321 
(*Cancellation law for division*) 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

322 
Goal "0<k ==> (k*m) div (k*n) = m div (n::nat)"; 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

323 
by (div_undefined_case_tac "n=0" 1); 
9870  324 
by (induct_thm_tac nat_less_induct "m" 1); 
3366  325 
by (case_tac "na<n" 1); 
8393  326 
by (asm_simp_tac (simpset() addsimps [zero_less_mult_iff, mult_less_mono2]) 1); 
3366  327 
by (subgoal_tac "~ k*na < k*n" 1); 
328 
by (asm_simp_tac 

4089  329 
(simpset() addsimps [zero_less_mult_iff, div_geq, 
5415  330 
diff_mult_distrib2 RS sym, diff_less]) 1); 
4089  331 
by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, 
3366  332 
le_refl RS mult_le_mono]) 1); 
333 
qed "div_cancel"; 

334 
Addsimps [div_cancel]; 

335 

7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

336 
(*mod_mult_distrib2 above is the counterpart for remainder*) 
3366  337 

338 

339 
(************************************************) 

340 
(** Divides Relation **) 

341 
(************************************************) 

342 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

343 
Goalw [dvd_def] "m dvd (0::nat)"; 
4089  344 
by (blast_tac (claset() addIs [mult_0_right RS sym]) 1); 
3366  345 
qed "dvd_0_right"; 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

346 
AddIffs [dvd_0_right]; 
3366  347 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

348 
Goalw [dvd_def] "0 dvd m ==> m = (0::nat)"; 
6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset

349 
by Auto_tac; 
3366  350 
qed "dvd_0_left"; 
351 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

352 
Goalw [dvd_def] "1 dvd (k::nat)"; 
3366  353 
by (Simp_tac 1); 
354 
qed "dvd_1_left"; 

355 
AddIffs [dvd_1_left]; 

356 

6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset

357 
Goalw [dvd_def] "m dvd (m::nat)"; 
4089  358 
by (blast_tac (claset() addIs [mult_1_right RS sym]) 1); 
3366  359 
qed "dvd_refl"; 
360 
Addsimps [dvd_refl]; 

361 

6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset

362 
Goalw [dvd_def] "[ m dvd n; n dvd p ] ==> m dvd (p::nat)"; 
4089  363 
by (blast_tac (claset() addIs [mult_assoc] ) 1); 
3366  364 
qed "dvd_trans"; 
365 

6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset

366 
Goalw [dvd_def] "[ m dvd n; n dvd m ] ==> m = (n::nat)"; 
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset

367 
by (force_tac (claset() addDs [mult_eq_self_implies_10], 
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset

368 
simpset() addsimps [mult_assoc, mult_eq_1_iff]) 1); 
3366  369 
qed "dvd_anti_sym"; 
370 

6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset

371 
Goalw [dvd_def] "[ k dvd m; k dvd n ] ==> k dvd (m+n :: nat)"; 
4089  372 
by (blast_tac (claset() addIs [add_mult_distrib2 RS sym]) 1); 
3366  373 
qed "dvd_add"; 
374 

6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset

375 
Goalw [dvd_def] "[ k dvd m; k dvd n ] ==> k dvd (mn :: nat)"; 
4089  376 
by (blast_tac (claset() addIs [diff_mult_distrib2 RS sym]) 1); 
3366  377 
qed "dvd_diff"; 
378 

6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset

379 
Goal "[ k dvd (mn); k dvd n; n<=m ] ==> k dvd (m::nat)"; 
3457  380 
by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1); 
4089  381 
by (blast_tac (claset() addIs [dvd_add]) 1); 
3366  382 
qed "dvd_diffD"; 
383 

6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset

384 
Goalw [dvd_def] "k dvd n ==> k dvd (m*n :: nat)"; 
4089  385 
by (blast_tac (claset() addIs [mult_left_commute]) 1); 
3366  386 
qed "dvd_mult"; 
387 

6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset

388 
Goal "k dvd m ==> k dvd (m*n :: nat)"; 
3366  389 
by (stac mult_commute 1); 
390 
by (etac dvd_mult 1); 

391 
qed "dvd_mult2"; 

392 

393 
(* k dvd (m*k) *) 

394 
AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2]; 

395 

7493  396 
Goal "k dvd (n + k) = k dvd (n::nat)"; 
7499  397 
by (rtac iffI 1); 
398 
by (etac dvd_add 2); 

399 
by (rtac dvd_refl 2); 

7493  400 
by (subgoal_tac "n = (n+k)k" 1); 
401 
by (Simp_tac 2); 

7499  402 
by (etac ssubst 1); 
403 
by (etac dvd_diff 1); 

404 
by (rtac dvd_refl 1); 

7493  405 
qed "dvd_reduce"; 
406 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

407 
Goalw [dvd_def] "!!n::nat. [ f dvd m; f dvd n; 0<n ] ==> f dvd (m mod n)"; 
3718  408 
by (Clarify_tac 1); 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

409 
by (Full_simp_tac 1); 
3366  410 
by (res_inst_tac 
411 
[("x", "(((k div ka)*ka + k mod ka)  ((f*k) div (f*ka)) * ka)")] 

412 
exI 1); 

7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

413 
by (asm_simp_tac 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

414 
(simpset() addsimps [diff_mult_distrib2, mod_mult_distrib2 RS sym, 
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

415 
add_mult_distrib2]) 1); 
3366  416 
qed "dvd_mod"; 
417 

7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

418 
Goal "[ (k::nat) dvd (m mod n); k dvd n ] ==> k dvd m"; 
3366  419 
by (subgoal_tac "k dvd ((m div n)*n + m mod n)" 1); 
4089  420 
by (asm_simp_tac (simpset() addsimps [dvd_add, dvd_mult]) 2); 
4356  421 
by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1); 
3366  422 
qed "dvd_mod_imp_dvd"; 
423 

9881  424 
Goalw [dvd_def] "!!n::nat. [ f dvd m; f dvd n ] ==> f dvd (m mod n)"; 
425 
by (div_undefined_case_tac "n=0" 1); 

426 
by (Clarify_tac 1); 

427 
by (Full_simp_tac 1); 

428 
by (rename_tac "j" 1); 

429 
by (res_inst_tac 

430 
[("x", "(((k div j)*j + k mod j)  ((f*k) div (f*j)) * j)")] 

431 
exI 1); 

432 
by (asm_simp_tac 

433 
(simpset() addsimps [diff_mult_distrib2, mod_mult_distrib2 RS sym, 

434 
add_mult_distrib2]) 1); 

435 
qed "dvd_mod"; 

436 

437 
Goal "k dvd n ==> (k::nat) dvd (m mod n) = k dvd m"; 

438 
by (blast_tac (claset() addIs [dvd_mod_imp_dvd, dvd_mod]) 1); 

439 
qed "dvd_mod_iff"; 

440 

6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset

441 
Goalw [dvd_def] "!!k::nat. [ (k*m) dvd (k*n); 0<k ] ==> m dvd n"; 
3366  442 
by (etac exE 1); 
4089  443 
by (asm_full_simp_tac (simpset() addsimps mult_ac) 1); 
3366  444 
qed "dvd_mult_cancel"; 
445 

6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset

446 
Goalw [dvd_def] "[ i dvd m; j dvd n] ==> (i*j) dvd (m*n :: nat)"; 
3718  447 
by (Clarify_tac 1); 
3366  448 
by (res_inst_tac [("x","k*ka")] exI 1); 
4089  449 
by (asm_simp_tac (simpset() addsimps mult_ac) 1); 
3366  450 
qed "mult_dvd_mono"; 
451 

6865
5577ffe4c2f1
now div and mod are overloaded; dvd is polymorphic
paulson
parents:
6073
diff
changeset

452 
Goalw [dvd_def] "(i*j :: nat) dvd k ==> i dvd k"; 
4089  453 
by (full_simp_tac (simpset() addsimps [mult_assoc]) 1); 
3366  454 
by (Blast_tac 1); 
455 
qed "dvd_mult_left"; 

456 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

457 
Goalw [dvd_def] "[ k dvd n; 0 < n ] ==> k <= (n::nat)"; 
3718  458 
by (Clarify_tac 1); 
4089  459 
by (ALLGOALS (full_simp_tac (simpset() addsimps [zero_less_mult_iff]))); 
3457  460 
by (etac conjE 1); 
461 
by (rtac le_trans 1); 

462 
by (rtac (le_refl RS mult_le_mono) 2); 

3366  463 
by (etac Suc_leI 2); 
464 
by (Simp_tac 1); 

465 
qed "dvd_imp_le"; 

466 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8860
diff
changeset

467 
Goalw [dvd_def] "!!k::nat. (k dvd n) = (n mod k = 0)"; 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

468 
by (div_undefined_case_tac "k=0" 1); 
3724  469 
by Safe_tac; 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

470 
by (asm_simp_tac (simpset() addsimps [mult_commute]) 1); 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

471 
by (res_inst_tac [("t","n"),("n1","k")] (mod_div_equality RS subst) 1); 
3366  472 
by (stac mult_commute 1); 
473 
by (Asm_simp_tac 1); 

474 
qed "dvd_eq_mod_eq_0"; 

10195
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset

475 

325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset

476 
Goal "(m mod d = 0) = (EX q::nat. m = d*q)"; 
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset

477 
by (auto_tac (claset(), 
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset

478 
simpset() addsimps [dvd_eq_mod_eq_0 RS sym, dvd_def])); 
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset

479 
qed "mod_eq_0_iff"; 
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset

480 
AddSDs [mod_eq_0_iff RS iffD1]; 
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset

481 

325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset

482 
(*Loses information, namely we also have r<d provided d is nonzero*) 
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset

483 
Goal "(m mod d = r) ==> EX q::nat. m = r + q*d"; 
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset

484 
by (cut_inst_tac [("m","m")] mod_div_equality 1); 
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset

485 
by (full_simp_tac (simpset() addsimps add_ac) 1); 
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset

486 
by (blast_tac (claset() addIs [sym]) 1); 
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset

487 
qed "mod_eqD"; 
325b6279ae4f
new theorems mod_eq_0_iff and mod_eqD; also new SD rule
paulson
parents:
9912
diff
changeset

488 