author  oheimb 
Mon, 06 Sep 1999 18:18:30 +0200  
changeset 7493  e6f74eebfab3 
parent 7082  f444e632cdf5 
child 7499  23e090051cb8 
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 

12 
val wf_less_trans = [eq_reflection, wf_pred_nat RS wf_trancl] MRS 

13 
def_wfrec RS trans; 

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 

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

29 
Goal "a div 0 = 0"; 
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 

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

34 
Goal "a mod 0 = a"; 
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"; 

51 

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

52 
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

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

5415  58 
(*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

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

62 

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

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

66 

5069  67 
Goal "m mod 1 = 0"; 
3366  68 
by (induct_tac "m" 1); 
4089  69 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_less, mod_geq]))); 
3366  70 
qed "mod_1"; 
71 
Addsimps [mod_1]; 

72 

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

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

74 
by (div_undefined_case_tac "n=0" 1); 
4089  75 
by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq]) 1); 
3366  76 
qed "mod_self"; 
77 

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

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

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

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

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

4810  87 

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

88 
Goal "(m + k*n) mod n = m mod (n::nat)"; 
4810  89 
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

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

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

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

93 
mod_add_self1]))); 
4811  94 
qed "mod_mult_self1"; 
4810  95 

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

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

4810  99 

4811  100 
Addsimps [mod_mult_self1, mod_mult_self2]; 
3366  101 

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

102 
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

103 
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

104 
by (div_undefined_case_tac "k=0" 1); 
3366  105 
by (res_inst_tac [("n","m")] less_induct 1); 
4774  106 
by (stac mod_if 1); 
107 
by (Asm_simp_tac 1); 

108 
by (asm_simp_tac (simpset() addsimps [mod_less, mod_geq, 

109 
diff_less, diff_mult_distrib]) 1); 

3366  110 
qed "mod_mult_distrib"; 
111 

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

112 
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

113 
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

114 
(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

115 
mod_mult_distrib]) 1); 
3366  116 
qed "mod_mult_distrib2"; 
117 

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

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

119 
by (div_undefined_case_tac "n=0" 1); 
3366  120 
by (induct_tac "m" 1); 
4089  121 
by (asm_simp_tac (simpset() addsimps [mod_less]) 1); 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

122 
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

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

127 
Goal "(n*m) mod n = 0"; 

128 
by (simp_tac (simpset() addsimps [mult_commute, mod_mult_self_is_0]) 1); 

129 
qed "mod_mult_self1_is_0"; 

130 
Addsimps [mod_mult_self_is_0, mod_mult_self1_is_0]; 

3366  131 

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

132 

3366  133 
(*** Quotient ***) 
134 

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

135 
Goal "m<n ==> m div n = 0"; 
3366  136 
by (rtac (div_eq RS wf_less_trans) 1); 
137 
by (Asm_simp_tac 1); 

138 
qed "div_less"; 

139 

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

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

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

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

148 
qed "le_div_geq"; 

149 

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

150 
Goal "0<n ==> m div n = (if m<n then 0 else Suc((mn) div n))"; 
4774  151 
by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1); 
152 
qed "div_if"; 

153 

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

154 

3366  155 
(*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

156 
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

157 
by (div_undefined_case_tac "n=0" 1); 
3366  158 
by (res_inst_tac [("n","m")] less_induct 1); 
4774  159 
by (stac mod_if 1); 
160 
by (ALLGOALS (asm_simp_tac 

5537  161 
(simpset() addsimps [add_assoc, div_less, div_geq, 
162 
add_diff_inverse, diff_less]))); 

3366  163 
qed "mod_div_equality"; 
164 

4358  165 
(* 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

166 
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

167 
by (cut_inst_tac [("m","m"),("n","n")] mod_div_equality 1); 
4358  168 
by (EVERY1[etac subst, simp_tac (simpset() addsimps mult_ac), 
169 
K(IF_UNSOLVED no_tac)]); 

170 
qed "mult_div_cancel"; 

171 

5069  172 
Goal "m div 1 = m"; 
3366  173 
by (induct_tac "m" 1); 
4089  174 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [div_less, div_geq]))); 
3366  175 
qed "div_1"; 
176 
Addsimps [div_1]; 

177 

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

178 
Goal "0<n ==> n div n = 1"; 
4089  179 
by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1); 
3366  180 
qed "div_self"; 
181 

4811  182 

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

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

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

187 
qed "div_add_self2"; 

188 

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

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

192 

5069  193 
Goal "!!n. 0<n ==> (m + k*n) div n = k + m div n"; 
4811  194 
by (induct_tac "k" 1); 
5537  195 
by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac @ [div_add_self1]))); 
4811  196 
qed "div_mult_self1"; 
197 

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

198 
Goal "0<n ==> (m + n*k) div n = k + m div n"; 
4811  199 
by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self1]) 1); 
200 
qed "div_mult_self2"; 

201 

202 
Addsimps [div_mult_self1, div_mult_self2]; 

203 

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

204 
(** 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

205 

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

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

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

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

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

210 

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

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

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

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

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

215 
Addsimps [div_0, mod_0]; 
4811  216 

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

217 
(* 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

218 
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

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

220 
by (res_inst_tac [("n","n")] less_induct 1); 
3718  221 
by (Clarify_tac 1); 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

222 
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

223 
(* 1 case n<k *) 
4089  224 
by (asm_simp_tac (simpset() addsimps [div_less]) 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

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

226 
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

227 
(* 2.1 case m<k *) 
4089  228 
by (asm_simp_tac (simpset() addsimps [div_less]) 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

229 
(* 2.2 case m>=k *) 
4089  230 
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

231 
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

232 

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

233 
(* Antimonotonicity of div in second argument *) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

234 
Goal "[ 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

235 
by (subgoal_tac "0<n" 1); 
6073  236 
by (Asm_simp_tac 2); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

237 
by (res_inst_tac [("n","k")] less_induct 1); 
3496  238 
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

239 
by (case_tac "k<n" 1); 
4089  240 
by (asm_simp_tac (simpset() addsimps [div_less]) 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

241 
by (subgoal_tac "~(k<m)" 1); 
6073  242 
by (Asm_simp_tac 2); 
4089  243 
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

244 
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

245 
by (REPEAT (ares_tac [div_le_mono,diff_le_mono2] 2)); 
5318  246 
by (rtac le_trans 1); 
5316  247 
by (Asm_simp_tac 1); 
248 
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

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

250 

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

251 
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

252 
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

253 
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

254 
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

255 
by (rtac div_le_mono2 1); 
6073  256 
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

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

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

259 

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

260 
(* Similar for "less than" *) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset

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

262 
by (res_inst_tac [("n","m")] less_induct 1); 
3496  263 
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

264 
by (case_tac "m<n" 1); 
4089  265 
by (asm_full_simp_tac (simpset() addsimps [div_less]) 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

266 
by (subgoal_tac "0<n" 1); 
6073  267 
by (Asm_simp_tac 2); 
4089  268 
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

269 
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

270 
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

271 
by (REPEAT (ares_tac [impI,less_trans_Suc] 1)); 
4089  272 
by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1); 
273 
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

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

275 
by (subgoal_tac "m=n" 1); 
6073  276 
by (Asm_simp_tac 2); 
4089  277 
by (asm_simp_tac (simpset() addsimps [div_less]) 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

278 
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

279 
Addsimps [div_less_dividend]; 
3366  280 

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

282 

5278  283 
Goal "0<n ==> Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"; 
3366  284 
by (res_inst_tac [("n","m")] less_induct 1); 
285 
by (excluded_middle_tac "Suc(na)<n" 1); 

286 
(* case Suc(na) < n *) 

287 
by (forward_tac [lessI RS less_trans] 2); 

5355  288 
by (asm_simp_tac (simpset() addsimps [mod_less, less_not_refl3]) 2); 
3366  289 
(* case n <= Suc(na) *) 
5415  290 
by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, le_Suc_eq, 
291 
mod_geq]) 1); 

292 
by (etac disjE 1); 

293 
by (asm_simp_tac (simpset() addsimps [mod_less]) 2); 

7059  294 
by (asm_simp_tac (simpset() addsimps [Suc_diff_le, diff_less, 
5415  295 
le_mod_geq]) 1); 
3366  296 
qed "mod_Suc"; 
297 

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

298 
Goal "0<n ==> m mod n < n"; 
3366  299 
by (res_inst_tac [("n","m")] less_induct 1); 
5498  300 
by (case_tac "na<n" 1); 
301 
(*case n le na*) 

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

3366  303 
(*case na<n*) 
5498  304 
by (asm_simp_tac (simpset() addsimps [mod_less]) 1); 
3366  305 
qed "mod_less_divisor"; 
306 

307 

308 
(** Evens and Odds **) 

309 

310 
(*With less_zeroE, causes case analysis on b<2*) 

311 
AddSEs [less_SucE]; 

312 

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

313 
Goal "b<2 ==> (k mod 2 = b)  (k mod 2 = (if b=1 then 0 else 1))"; 
3366  314 
by (subgoal_tac "k mod 2 < 2" 1); 
4089  315 
by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2); 
4686  316 
by (Asm_simp_tac 1); 
4356  317 
by Safe_tac; 
3366  318 
qed "mod2_cases"; 
319 

5069  320 
Goal "Suc(Suc(m)) mod 2 = m mod 2"; 
3366  321 
by (subgoal_tac "m mod 2 < 2" 1); 
4089  322 
by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2); 
3724  323 
by Safe_tac; 
4089  324 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_Suc]))); 
3366  325 
qed "mod2_Suc_Suc"; 
326 
Addsimps [mod2_Suc_Suc]; 

327 

5069  328 
Goal "(0 < m mod 2) = (m mod 2 = 1)"; 
3366  329 
by (subgoal_tac "m mod 2 < 2" 1); 
4089  330 
by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4423
diff
changeset

331 
by Auto_tac; 
4356  332 
qed "mod2_gr_0"; 
333 
Addsimps [mod2_gr_0]; 

334 

5069  335 
Goal "(m+m) mod 2 = 0"; 
3366  336 
by (induct_tac "m" 1); 
4089  337 
by (simp_tac (simpset() addsimps [mod_less]) 1); 
3427
e7cef2081106
Removed a few redundant additions of simprules or classical rules
paulson
parents:
3366
diff
changeset

338 
by (Asm_simp_tac 1); 
4385  339 
qed "mod2_add_self_eq_0"; 
340 
Addsimps [mod2_add_self_eq_0]; 

341 

5069  342 
Goal "((m+m)+n) mod 2 = n mod 2"; 
4385  343 
by (induct_tac "m" 1); 
344 
by (simp_tac (simpset() addsimps [mod_less]) 1); 

345 
by (Asm_simp_tac 1); 

3366  346 
qed "mod2_add_self"; 
347 
Addsimps [mod2_add_self]; 

348 

5498  349 
(*Restore the default*) 
3366  350 
Delrules [less_SucE]; 
351 

352 
(*** More division laws ***) 

353 

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

355 
by (cut_inst_tac [("m", "m*n"),("n","n")] mod_div_equality 1); 
4089  356 
by (asm_full_simp_tac (simpset() addsimps [mod_mult_self_is_0]) 1); 
3366  357 
qed "div_mult_self_is_m"; 
7082  358 

359 
Goal "0<n ==> (n*m) div n = m"; 

360 
by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self_is_m]) 1); 

361 
qed "div_mult_self1_is_m"; 

362 
Addsimps [div_mult_self_is_m, div_mult_self1_is_m]; 

3366  363 

364 
(*Cancellation law for division*) 

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

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

366 
by (div_undefined_case_tac "n=0" 1); 
3366  367 
by (res_inst_tac [("n","m")] less_induct 1); 
368 
by (case_tac "na<n" 1); 

4089  369 
by (asm_simp_tac (simpset() addsimps [div_less, zero_less_mult_iff, 
7029
08d4eb8500dd
new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents:
7007
diff
changeset

370 
mult_less_mono2]) 1); 
3366  371 
by (subgoal_tac "~ k*na < k*n" 1); 
372 
by (asm_simp_tac 

4089  373 
(simpset() addsimps [zero_less_mult_iff, div_geq, 
5415  374 
diff_mult_distrib2 RS sym, diff_less]) 1); 
4089  375 
by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, 
3366  376 
le_refl RS mult_le_mono]) 1); 
377 
qed "div_cancel"; 

378 
Addsimps [div_cancel]; 

379 

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

380 
(*mod_mult_distrib2 above is the counterpart for remainder*) 
3366  381 

382 

383 
(************************************************) 

384 
(** Divides Relation **) 

385 
(************************************************) 

386 

5069  387 
Goalw [dvd_def] "m dvd 0"; 
4089  388 
by (blast_tac (claset() addIs [mult_0_right RS sym]) 1); 
3366  389 
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

390 
AddIffs [dvd_0_right]; 
3366  391 

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

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

393 
by Auto_tac; 
3366  394 
qed "dvd_0_left"; 
395 

5069  396 
Goalw [dvd_def] "1 dvd k"; 
3366  397 
by (Simp_tac 1); 
398 
qed "dvd_1_left"; 

399 
AddIffs [dvd_1_left]; 

400 

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

401 
Goalw [dvd_def] "m dvd (m::nat)"; 
4089  402 
by (blast_tac (claset() addIs [mult_1_right RS sym]) 1); 
3366  403 
qed "dvd_refl"; 
404 
Addsimps [dvd_refl]; 

405 

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

406 
Goalw [dvd_def] "[ m dvd n; n dvd p ] ==> m dvd (p::nat)"; 
4089  407 
by (blast_tac (claset() addIs [mult_assoc] ) 1); 
3366  408 
qed "dvd_trans"; 
409 

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

410 
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

411 
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

412 
simpset() addsimps [mult_assoc, mult_eq_1_iff]) 1); 
3366  413 
qed "dvd_anti_sym"; 
414 

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

415 
Goalw [dvd_def] "[ k dvd m; k dvd n ] ==> k dvd (m+n :: nat)"; 
4089  416 
by (blast_tac (claset() addIs [add_mult_distrib2 RS sym]) 1); 
3366  417 
qed "dvd_add"; 
418 

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

419 
Goalw [dvd_def] "[ k dvd m; k dvd n ] ==> k dvd (mn :: nat)"; 
4089  420 
by (blast_tac (claset() addIs [diff_mult_distrib2 RS sym]) 1); 
3366  421 
qed "dvd_diff"; 
422 

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

423 
Goal "[ k dvd (mn); k dvd n; n<=m ] ==> k dvd (m::nat)"; 
3457  424 
by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1); 
4089  425 
by (blast_tac (claset() addIs [dvd_add]) 1); 
3366  426 
qed "dvd_diffD"; 
427 

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

428 
Goalw [dvd_def] "k dvd n ==> k dvd (m*n :: nat)"; 
4089  429 
by (blast_tac (claset() addIs [mult_left_commute]) 1); 
3366  430 
qed "dvd_mult"; 
431 

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

432 
Goal "k dvd m ==> k dvd (m*n :: nat)"; 
3366  433 
by (stac mult_commute 1); 
434 
by (etac dvd_mult 1); 

435 
qed "dvd_mult2"; 

436 

437 
(* k dvd (m*k) *) 

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

439 

7493  440 
Goal "k dvd (n + k) = k dvd (n::nat)"; 
441 
br iffI 1; 

442 
be dvd_add 2; 

443 
br dvd_refl 2; 

444 
by (subgoal_tac "n = (n+k)k" 1); 

445 
by (Simp_tac 2); 

446 
be ssubst 1; 

447 
be dvd_diff 1; 

448 
br dvd_refl 1; 

449 
qed "dvd_reduce"; 

450 

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

451 
Goalw [dvd_def] "[ f dvd m; f dvd n; 0<n ] ==> f dvd (m mod n)"; 
3718  452 
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

453 
by (Full_simp_tac 1); 
3366  454 
by (res_inst_tac 
455 
[("x", "(((k div ka)*ka + k mod ka)  ((f*k) div (f*ka)) * ka)")] 

456 
exI 1); 

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

457 
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

458 
(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

459 
add_mult_distrib2]) 1); 
3366  460 
qed "dvd_mod"; 
461 

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

462 
Goal "[ (k::nat) dvd (m mod n); k dvd n ] ==> k dvd m"; 
3366  463 
by (subgoal_tac "k dvd ((m div n)*n + m mod n)" 1); 
4089  464 
by (asm_simp_tac (simpset() addsimps [dvd_add, dvd_mult]) 2); 
4356  465 
by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1); 
3366  466 
qed "dvd_mod_imp_dvd"; 
467 

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

468 
Goalw [dvd_def] "!!k::nat. [ (k*m) dvd (k*n); 0<k ] ==> m dvd n"; 
3366  469 
by (etac exE 1); 
4089  470 
by (asm_full_simp_tac (simpset() addsimps mult_ac) 1); 
3366  471 
by (Blast_tac 1); 
472 
qed "dvd_mult_cancel"; 

473 

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

474 
Goalw [dvd_def] "[ i dvd m; j dvd n] ==> (i*j) dvd (m*n :: nat)"; 
3718  475 
by (Clarify_tac 1); 
3366  476 
by (res_inst_tac [("x","k*ka")] exI 1); 
4089  477 
by (asm_simp_tac (simpset() addsimps mult_ac) 1); 
3366  478 
qed "mult_dvd_mono"; 
479 

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

480 
Goalw [dvd_def] "(i*j :: nat) dvd k ==> i dvd k"; 
4089  481 
by (full_simp_tac (simpset() addsimps [mult_assoc]) 1); 
3366  482 
by (Blast_tac 1); 
483 
qed "dvd_mult_left"; 

484 

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

485 
Goalw [dvd_def] "[ k dvd n; 0 < n ] ==> k <= n"; 
3718  486 
by (Clarify_tac 1); 
4089  487 
by (ALLGOALS (full_simp_tac (simpset() addsimps [zero_less_mult_iff]))); 
3457  488 
by (etac conjE 1); 
489 
by (rtac le_trans 1); 

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

3366  491 
by (etac Suc_leI 2); 
492 
by (Simp_tac 1); 

493 
qed "dvd_imp_le"; 

494 

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

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

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

498 
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

499 
by (res_inst_tac [("t","n"),("n1","k")] (mod_div_equality RS subst) 1); 
3366  500 
by (stac mult_commute 1); 
501 
by (Asm_simp_tac 1); 

502 
qed "dvd_eq_mod_eq_0"; 